seq_2.miz



    begin

    reserve n,n1,n2,m for Nat,

r,r1,r2,p,g1,g2,g for Real,

seq,seq9,seq1 for Real_Sequence,

y for set;

    theorem :: SEQ_2:1

    

     Th1: ( - g) < r & r < g iff |.r.| < g

    proof

      thus ( - g) < r & r < g implies |.r.| < g

      proof

        assume that

         A1: ( - g) < r and

         A2: r < g;

        

         A3: |.r.| <= g by A1, A2, ABSVALUE: 5;

        now

          assume

           A4: |.r.| = g;

          now

            assume r < 0 ;

            then g = ( - r) by A4, ABSVALUE:def 1;

            hence contradiction by A1;

          end;

          hence contradiction by A2, A4, ABSVALUE:def 1;

        end;

        hence thesis by A3, XXREAL_0: 1;

      end;

      assume

       A5: |.r.| < g;

      then

       A6: ( - g) <= r by ABSVALUE: 5;

      

       A7: 0 <= |.r.| by COMPLEX1: 46;

      

       A8: 0 < g by A5, COMPLEX1: 46;

      

       A9: ( - g) < ( - 0 ) by A5, A7;

      now

        assume r = ( - g);

        

        then |.r.| = ( - ( - g)) by A9, ABSVALUE:def 1

        .= g;

        hence contradiction by A5;

      end;

      hence ( - g) < r by A6, XXREAL_0: 1;

      thus thesis by A5, A8, ABSVALUE:def 1;

    end;

    theorem :: SEQ_2:2

    

     Th2: g <> 0 & r <> 0 implies |.((g " ) - (r " )).| = ( |.(g - r).| / ( |.g.| * |.r.|))

    proof

      assume that

       A1: g <> 0 and

       A2: r <> 0 ;

      

      thus |.((g " ) - (r " )).| = |.((1 / g) - (r " )).| by XCMPLX_1: 215

      .= |.((1 / g) - (1 / r)).| by XCMPLX_1: 215

      .= |.(((1 * r) - (1 * g)) / (g * r)).| by A1, A2, XCMPLX_1: 130

      .= ( |.(r - g).| / |.(g * r).|) by COMPLEX1: 67

      .= ( |.( - (g - r)).| / ( |.g.| * |.r.|)) by COMPLEX1: 65

      .= ( |.(g - r).| / ( |.g.| * |.r.|)) by COMPLEX1: 52;

    end;

    definition

      let f be real-valued Function;

      :: SEQ_2:def1

      attr f is bounded_above means ex r st for y be object st y in ( dom f) holds (f . y) < r;

      :: SEQ_2:def2

      attr f is bounded_below means ex r st for y be object st y in ( dom f) holds r < (f . y);

    end

    definition

      let seq;

      

       A1: ( dom seq) = NAT by SEQ_1: 1;

      :: original: bounded_above

      redefine

      :: SEQ_2:def3

      attr seq is bounded_above means

      : Def3: ex r st for n holds (seq . n) < r;

      compatibility

      proof

        thus seq is bounded_above implies ex r st for n holds (seq . n) < r

        proof

          given r such that

           A2: for y be object st y in ( dom seq) holds (seq . y) < r;

          take r;

          let n;

          n in NAT by ORDINAL1:def 12;

          hence thesis by A1, A2;

        end;

        given r such that

         A3: for n holds (seq . n) < r;

        take r;

        let y be object;

        assume y in ( dom seq);

        hence thesis by A3;

      end;

      :: original: bounded_below

      redefine

      :: SEQ_2:def4

      attr seq is bounded_below means

      : Def4: ex r st for n holds r < (seq . n);

      compatibility

      proof

        thus seq is bounded_below implies ex r st for n holds r < (seq . n)

        proof

          given r such that

           A4: for y be object st y in ( dom seq) holds r < (seq . y);

          take r;

          let n;

          n in NAT by ORDINAL1:def 12;

          hence thesis by A1, A4;

        end;

        given r such that

         A5: for n holds r < (seq . n);

        take r;

        let y be object;

        assume y in ( dom seq);

        hence thesis by A5;

      end;

    end

    registration

      cluster bounded -> bounded_above bounded_below for real-valued Function;

      coherence

      proof

        let f be real-valued Function;

        given r such that

         A1: for y st y in ( dom f) holds |.(f . y).| < r;

        thus f is bounded_above

        proof

          take r;

          let y be object;

          

           A2: (f . y) <= |.(f . y).| by ABSVALUE: 4;

          assume y in ( dom f);

          hence thesis by A1, A2, XXREAL_0: 2;

        end;

        take ( - |.r.|);

        let y be object;

        

         A3: ( - |.(f . y).|) <= (f . y) by ABSVALUE: 4;

        r <= |.r.| by ABSVALUE: 4;

        then

         A4: ( - |.r.|) <= ( - r) by XREAL_1: 24;

        assume y in ( dom f);

        then |.(f . y).| < r by A1;

        then ( - r) < ( - |.(f . y).|) by XREAL_1: 24;

        then ( - |.r.|) < ( - |.(f . y).|) by A4, XXREAL_0: 2;

        hence thesis by A3, XXREAL_0: 2;

      end;

      cluster bounded_above bounded_below -> bounded for real-valued Function;

      coherence

      proof

        let f be real-valued Function;

        assume f is bounded_above;

        then

        consider r1 such that

         A5: for y be object st y in ( dom f) holds (f . y) < r1;

        assume f is bounded_below;

        then

        consider r2 such that

         A6: for y be object st y in ( dom f) holds r2 < (f . y);

        take g = (( |.r1.| + |.r2.|) + 1);

        

         A7: 0 <= |.r1.| by COMPLEX1: 46;

        let y such that

         A8: y in ( dom f);

        r1 <= |.r1.| by ABSVALUE: 4;

        then (f . y) < |.r1.| by A5, A8, XXREAL_0: 2;

        then ((f . y) + 0 ) < ( |.r1.| + |.r2.|) by COMPLEX1: 46, XREAL_1: 8;

        then

         A9: (f . y) < g by XREAL_1: 8;

        ( - |.r2.|) <= r2 by ABSVALUE: 4;

        then ( - |.r2.|) < (f . y) by A6, A8, XXREAL_0: 2;

        then (( - |.r1.|) + ( - |.r2.|)) < ( 0 + (f . y)) by A7, XREAL_1: 8;

        then

         A10: ((( - |.r1.|) - |.r2.|) + ( - 1)) < ((f . y) + 0 ) by XREAL_1: 8;

        ((( - |.r1.|) - |.r2.|) - 1) = ( - g);

        hence |.(f . y).| < g by A9, A10, Th1;

      end;

    end

    theorem :: SEQ_2:3

    

     Th3: seq is bounded iff ex r st ( 0 < r & for n holds |.(seq . n).| < r)

    proof

      thus seq is bounded implies ex r st ( 0 < r & for n holds |.(seq . n).| < r)

      proof

        assume

         A1: seq is bounded;

        then

        consider r1 such that

         A2: for n holds (seq . n) < r1 by Def3;

        consider r2 such that

         A3: for n holds r2 < (seq . n) by A1, Def4;

        take g = (( |.r1.| + |.r2.|) + 1);

        

         A4: 0 <= |.r1.| by COMPLEX1: 46;

         0 <= |.r2.| by COMPLEX1: 46;

        hence 0 < g by A4;

        let n;

        r1 <= |.r1.| by ABSVALUE: 4;

        then (seq . n) < |.r1.| by A2, XXREAL_0: 2;

        then ((seq . n) + 0 ) < ( |.r1.| + |.r2.|) by COMPLEX1: 46, XREAL_1: 8;

        then

         A5: (seq . n) < g by XREAL_1: 8;

        ( - |.r2.|) <= r2 by ABSVALUE: 4;

        then ( - |.r2.|) < (seq . n) by A3, XXREAL_0: 2;

        then (( - |.r1.|) + ( - |.r2.|)) < ( 0 + (seq . n)) by A4, XREAL_1: 8;

        then

         A6: ((( - |.r1.|) - |.r2.|) + ( - 1)) < ((seq . n) + 0 ) by XREAL_1: 8;

        ((( - |.r1.|) - |.r2.|) - 1) = ( - g);

        hence thesis by A5, A6, Th1;

      end;

      given r such that 0 < r and

       A7: for n holds |.(seq . n).| < r;

      take r;

      let y;

      assume y in ( dom seq);

      then y is Element of NAT by FUNCT_2:def 1;

      hence thesis by A7;

    end;

    theorem :: SEQ_2:4

    

     Th4: for n holds ex r st ( 0 < r & for m st m <= n holds |.(seq . m).| < r)

    proof

      defpred X[ Nat] means ex r1 st 0 < r1 & for m st m <= $1 holds |.(seq . m).| < r1;

      

       A1: X[ 0 ]

      proof

        reconsider r = ( |.(seq . 0 ).| + 1) as Real;

        take r;

        ( 0 + 0 ) < ( |.(seq . 0 ).| + 1) by COMPLEX1: 46, XREAL_1: 8;

        hence 0 < r;

        let m;

        assume m <= 0 ;

        then 0 = m;

        then ( |.(seq . m).| + 0 ) < r by XREAL_1: 8;

        hence thesis;

      end;

      

       A2: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        given r1 such that

         A3: 0 < r1 and

         A4: for m st m <= n holds |.(seq . m).| < r1;

         A5:

        now

          assume

           A6: |.(seq . (n + 1)).| <= r1;

          take r = (r1 + 1);

          thus 0 < r by A3;

          let m such that

           A7: m <= (n + 1);

           A8:

          now

            assume m <= n;

            then

             A9: |.(seq . m).| < r1 by A4;

            (r1 + 0 ) < r by XREAL_1: 8;

            hence |.(seq . m).| < r by A9, XXREAL_0: 2;

          end;

          now

            assume

             A10: m = (n + 1);

            (r1 + 0 ) < r by XREAL_1: 8;

            hence |.(seq . m).| < r by A6, A10, XXREAL_0: 2;

          end;

          hence |.(seq . m).| < r by A7, A8, NAT_1: 8;

        end;

        now

          assume

           A11: r1 <= |.(seq . (n + 1)).|;

          take r = ( |.(seq . (n + 1)).| + 1);

          ( 0 + 0 ) < r by COMPLEX1: 46, XREAL_1: 8;

          hence 0 < r;

          let m such that

           A12: m <= (n + 1);

           A13:

          now

            assume m <= n;

            then |.(seq . m).| < r1 by A4;

            then |.(seq . m).| < |.(seq . (n + 1)).| by A11, XXREAL_0: 2;

            then ( |.(seq . m).| + 0 ) < r by XREAL_1: 8;

            hence |.(seq . m).| < r;

          end;

          now

            assume m = (n + 1);

            then ( |.(seq . m).| + 0 ) < r by XREAL_1: 8;

            hence |.(seq . m).| < r;

          end;

          hence |.(seq . m).| < r by A12, A13, NAT_1: 8;

        end;

        hence thesis by A5;

      end;

      thus for n holds X[n] from NAT_1:sch 2( A1, A2);

    end;

    definition

      ::$Canceled

      let seq;

      :: original: convergent

      redefine

      :: SEQ_2:def6

      attr seq is convergent means ex g st for p st 0 < p holds ex n st for m st n <= m holds |.((seq . m) - g).| < p;

      compatibility

      proof

        thus seq is convergent implies ex g st for p st 0 < p holds ex n st for m st n <= m holds |.((seq . m) - g).| < p

        proof

          assume seq is convergent;

          then

          consider g be Complex such that

           A1: for p be Real st 0 < p holds ex n st for m st n <= m holds |.((seq . m) - g).| < p;

          

           A2: (( Re g) + (( Im g) * <i> )) = g by COMPLEX1: 13;

          now

            assume

             A3: not g is real;

            

             A4: ( Im g) <> 0 by A2, A3;

            set p = |.( Im g).|;

            

             A5: p > 0 by A4, COMPLEX1: 47;

             not ex n st for m st n <= m holds |.((seq . m) - g).| < p

            proof

              let n;

              take n;

              thus n <= n;

              reconsider sn = (seq . n) as Element of REAL by XREAL_0:def 1;

              

               A6: ( Im sn) = 0 by COMPLEX1:def 2;

              

               A7: ( Im ((seq . n) - g)) = (( Im (seq . n)) - ( Im g)) by COMPLEX1: 19;

              

               A8: |.((seq . n) - g).| = ( sqrt ((( Re ((seq . n) - g)) ^2 ) + (( Im g) ^2 ))) by A7, A6;

              (( Re ((seq . n) - g)) ^2 ) >= 0 by XREAL_1: 63;

              then ( sqrt ((( Re ((seq . n) - g)) ^2 ) + ( |.( Im g).| ^2 ))) >= |.( Im g).| by SQUARE_1: 58;

              hence |.((seq . n) - g).| >= |.( Im g).| by A8, COMPLEX1: 75;

            end;

            hence contradiction by A1, A5;

          end;

          then

          reconsider g as Real;

          take g;

          let p;

          reconsider p as Real;

           0 < p implies ex n st for m st n <= m holds |.((seq . m) - g).| < p by A1;

          hence thesis;

        end;

        given g such that

         A9: for p st 0 < p holds ex n st for m st n <= m holds |.((seq . m) - g).| < p;

        g in REAL by XREAL_0:def 1;

        then

        reconsider g as Element of COMPLEX by NUMBERS: 11;

        take g;

        thus thesis by A9;

      end;

    end

    definition

      let seq;

      assume

       A1: seq is convergent;

      :: SEQ_2:def7

      func lim seq -> Real means

      : Def6: for p st 0 < p holds ex n st for m st n <= m holds |.((seq . m) - it ).| < p;

      existence by A1;

      uniqueness

      proof

        given g1, g2 such that

         A2: for p st 0 < p holds ex n st for m st n <= m holds |.((seq . m) - g1).| < p and

         A3: for p st 0 < p holds ex n st for m st n <= m holds |.((seq . m) - g2).| < p and

         A4: g1 <> g2;

         A5:

        now

          assume |.(g1 - g2).| = 0 ;

          then ( 0 + g2) = ((g1 - g2) + g2) by ABSVALUE: 2;

          hence contradiction by A4;

        end;

        

         A6: 0 <= |.(g1 - g2).| by COMPLEX1: 46;

        then

        consider n1 such that

         A7: for m st n1 <= m holds |.((seq . m) - g1).| < ( |.(g1 - g2).| / 4) by A2, A5;

        consider n2 such that

         A8: for m st n2 <= m holds |.((seq . m) - g2).| < ( |.(g1 - g2).| / 4) by A3, A5, A6;

        

         A9: |.((seq . (n1 + n2)) - g1).| < ( |.(g1 - g2).| / 4) by A7, NAT_1: 12;

         |.((seq . (n1 + n2)) - g2).| < ( |.(g1 - g2).| / 4) by A8, NAT_1: 12;

        then

         A10: ( |.((seq . (n1 + n2)) - g2).| + |.((seq . (n1 + n2)) - g1).|) < (( |.(g1 - g2).| / 4) + ( |.(g1 - g2).| / 4)) by A9, XREAL_1: 8;

         |.(g1 - g2).| = |.(( - ((seq . (n1 + n2)) - g1)) + ((seq . (n1 + n2)) - g2)).|;

        then |.(g1 - g2).| <= ( |.( - ((seq . (n1 + n2)) - g1)).| + |.((seq . (n1 + n2)) - g2).|) by COMPLEX1: 56;

        then

         A11: |.(g1 - g2).| <= ( |.((seq . (n1 + n2)) - g1).| + |.((seq . (n1 + n2)) - g2).|) by COMPLEX1: 52;

        ( |.(g1 - g2).| / 2) < |.(g1 - g2).| by A5, A6, XREAL_1: 216;

        hence contradiction by A10, A11, XXREAL_0: 2;

      end;

    end

    definition

      let f be real-valued Function;

      :: original: bounded

      redefine

      :: SEQ_2:def8

      attr f is bounded means f is bounded_above bounded_below;

      compatibility ;

    end

    registration

      cluster constant -> convergent for Real_Sequence;

      coherence

      proof

        let seq be Real_Sequence;

        assume seq is constant;

        then

        consider r be Element of REAL such that

         A1: for n be Nat holds (seq . n) = r by VALUED_0:def 18;

        take g = r;

        let p such that

         A2: 0 < p;

        take n = 0 ;

        let m such that n <= m;

         |.((seq . m) - g).| = |.(r - g).| by A1

        .= 0 by ABSVALUE: 2;

        hence thesis by A2;

      end;

    end

    theorem :: SEQ_2:5

    

     Th5: seq is convergent & seq9 is convergent implies (seq + seq9) is convergent

    proof

      assume that

       A1: seq is convergent and

       A2: seq9 is convergent;

      consider g1 such that

       A3: for p st 0 < p holds ex n st for m st n <= m holds |.((seq . m) - g1).| < p by A1;

      consider g2 such that

       A4: for p st 0 < p holds ex n st for m st n <= m holds |.((seq9 . m) - g2).| < p by A2;

      take g = (g1 + g2);

      let p;

      assume

       A5: 0 < p;

      then

      consider n1 such that

       A6: for m st n1 <= m holds |.((seq . m) - g1).| < (p / 2) by A3;

      consider n2 such that

       A7: for m st n2 <= m holds |.((seq9 . m) - g2).| < (p / 2) by A4, A5;

      take k = (n1 + n2);

      let m such that

       A8: k <= m;

      n1 <= (n1 + n2) by NAT_1: 12;

      then n1 <= m by A8, XXREAL_0: 2;

      then

       A9: |.((seq . m) - g1).| < (p / 2) by A6;

      n2 <= k by NAT_1: 12;

      then n2 <= m by A8, XXREAL_0: 2;

      then |.((seq9 . m) - g2).| < (p / 2) by A7;

      then

       A10: ( |.((seq . m) - g1).| + |.((seq9 . m) - g2).|) < ((p / 2) + (p / 2)) by A9, XREAL_1: 8;

      

       A11: |.(((seq + seq9) . m) - g).| = |.(((seq . m) + (seq9 . m)) - (g1 + g2)).| by SEQ_1: 7

      .= |.(((seq . m) - g1) + ((seq9 . m) - g2)).|;

       |.(((seq . m) - g1) + ((seq9 . m) - g2)).| <= ( |.((seq . m) - g1).| + |.((seq9 . m) - g2).|) by COMPLEX1: 56;

      hence thesis by A10, A11, XXREAL_0: 2;

    end;

    registration

      let seq1,seq2 be convergent Real_Sequence;

      cluster (seq1 + seq2) -> convergent;

      coherence by Th5;

    end

    theorem :: SEQ_2:6

    

     Th6: seq is convergent & seq9 is convergent implies ( lim (seq + seq9)) = (( lim seq) + ( lim seq9))

    proof

      assume that

       A1: seq is convergent and

       A2: seq9 is convergent;

      now

        let p;

        assume 0 < p;

        then

         A3: 0 < (p / 2);

        then

        consider n1 such that

         A4: for m st n1 <= m holds |.((seq . m) - ( lim seq)).| < (p / 2) by A1, Def6;

        consider n2 such that

         A5: for m st n2 <= m holds |.((seq9 . m) - ( lim seq9)).| < (p / 2) by A2, A3, Def6;

        take k = (n1 + n2);

        let m such that

         A6: k <= m;

        n1 <= (n1 + n2) by NAT_1: 12;

        then n1 <= m by A6, XXREAL_0: 2;

        then

         A7: |.((seq . m) - ( lim seq)).| < (p / 2) by A4;

        n2 <= k by NAT_1: 12;

        then n2 <= m by A6, XXREAL_0: 2;

        then |.((seq9 . m) - ( lim seq9)).| < (p / 2) by A5;

        then

         A8: ( |.((seq . m) - ( lim seq)).| + |.((seq9 . m) - ( lim seq9)).|) < ((p / 2) + (p / 2)) by A7, XREAL_1: 8;

        

         A9: |.(((seq + seq9) . m) - (( lim seq) + ( lim seq9))).| = |.(((seq . m) + (seq9 . m)) - (( lim seq) + ( lim seq9))).| by SEQ_1: 7

        .= |.(((seq . m) - ( lim seq)) + ((seq9 . m) - ( lim seq9))).|;

         |.(((seq . m) - ( lim seq)) + ((seq9 . m) - ( lim seq9))).| <= ( |.((seq . m) - ( lim seq)).| + |.((seq9 . m) - ( lim seq9)).|) by COMPLEX1: 56;

        hence |.(((seq + seq9) . m) - (( lim seq) + ( lim seq9))).| < p by A8, A9, XXREAL_0: 2;

      end;

      hence thesis by A1, A2, Def6;

    end;

    theorem :: SEQ_2:7

    

     Th7: seq is convergent implies (r (#) seq) is convergent

    proof

      assume seq is convergent;

      then

      consider g1 such that

       A1: for p st 0 < p holds ex n st for m st n <= m holds |.((seq . m) - g1).| < p;

      take g = (r * g1);

       A2:

      now

        assume

         A3: r = 0 ;

        let p such that

         A4: 0 < p;

        reconsider k = 0 as Nat;

        take k;

        let m such that k <= m;

         |.(((r (#) seq) . m) - g).| = |.(( 0 * (seq . m)) - 0 ).| by A3, SEQ_1: 9

        .= 0 by ABSVALUE: 2;

        hence |.(((r (#) seq) . m) - g).| < p by A4;

      end;

      now

        assume

         A5: r <> 0 ;

        then

         A6: 0 < |.r.| by COMPLEX1: 47;

        let p such that

         A7: 0 < p;

        

         A8: 0 <> |.r.| by A5, COMPLEX1: 47;

        consider n1 such that

         A9: for m st n1 <= m holds |.((seq . m) - g1).| < (p / |.r.|) by A1, A6, A7;

        take k = n1;

        let m;

        assume k <= m;

        then

         A10: |.((seq . m) - g1).| < (p / |.r.|) by A9;

        

         A11: |.(((r (#) seq) . m) - g).| = |.((r * (seq . m)) - (r * g1)).| by SEQ_1: 9

        .= |.(r * ((seq . m) - g1)).|

        .= ( |.r.| * |.((seq . m) - g1).|) by COMPLEX1: 65;

        ( |.r.| * (p / |.r.|)) = ( |.r.| * (( |.r.| " ) * p)) by XCMPLX_0:def 9

        .= (( |.r.| * ( |.r.| " )) * p)

        .= (1 * p) by A8, XCMPLX_0:def 7

        .= p;

        hence |.(((r (#) seq) . m) - g).| < p by A6, A10, A11, XREAL_1: 68;

      end;

      hence thesis by A2;

    end;

    registration

      let r be Real;

      let seq be convergent Real_Sequence;

      cluster (r (#) seq) -> convergent;

      coherence by Th7;

    end

    theorem :: SEQ_2:8

    

     Th8: seq is convergent implies ( lim (r (#) seq)) = (r * ( lim seq))

    proof

      assume

       A1: seq is convergent;

       A2:

      now

        assume

         A3: r = 0 ;

        let p such that

         A4: 0 < p;

        reconsider k = 0 as Nat;

        take k;

        let m such that k <= m;

         |.(((r (#) seq) . m) - (r * ( lim seq))).| = |.(( 0 * (seq . m)) - 0 ).| by A3, SEQ_1: 9

        .= 0 by ABSVALUE: 2;

        hence |.(((r (#) seq) . m) - (r * ( lim seq))).| < p by A4;

      end;

      now

        assume

         A5: r <> 0 ;

        then

         A6: 0 < |.r.| by COMPLEX1: 47;

        let p such that

         A7: 0 < p;

        

         A8: 0 <> |.r.| by A5, COMPLEX1: 47;

         0 < (p / |.r.|) by A6, A7;

        then

        consider n1 such that

         A9: for m st n1 <= m holds |.((seq . m) - ( lim seq)).| < (p / |.r.|) by A1, Def6;

        take k = n1;

        let m;

        assume k <= m;

        then

         A10: |.((seq . m) - ( lim seq)).| < (p / |.r.|) by A9;

        

         A11: |.(((r (#) seq) . m) - (r * ( lim seq))).| = |.((r * (seq . m)) - (r * ( lim seq))).| by SEQ_1: 9

        .= |.(r * ((seq . m) - ( lim seq))).|

        .= ( |.r.| * |.((seq . m) - ( lim seq)).|) by COMPLEX1: 65;

        ( |.r.| * (p / |.r.|)) = ( |.r.| * (( |.r.| " ) * p)) by XCMPLX_0:def 9

        .= (( |.r.| * ( |.r.| " )) * p)

        .= (1 * p) by A8, XCMPLX_0:def 7

        .= p;

        hence |.(((r (#) seq) . m) - (r * ( lim seq))).| < p by A6, A10, A11, XREAL_1: 68;

      end;

      hence thesis by A1, A2, Def6;

    end;

    theorem :: SEQ_2:9

    seq is convergent implies ( - seq) is convergent;

    registration

      let seq be convergent Real_Sequence;

      cluster ( - seq) -> convergent;

      coherence ;

    end

    theorem :: SEQ_2:10

    

     Th10: seq is convergent implies ( lim ( - seq)) = ( - ( lim seq))

    proof

      assume seq is convergent;

      then ( lim (( - 1) (#) seq)) = (( - 1) * ( lim seq)) by Th8;

      hence thesis;

    end;

    theorem :: SEQ_2:11

    

     Th11: seq is convergent & seq9 is convergent implies (seq - seq9) is convergent

    proof

      assume that

       A1: seq is convergent and

       A2: seq9 is convergent;

      ( - seq9) is convergent by A2;

      hence thesis by A1;

    end;

    registration

      let seq1,seq2 be convergent Real_Sequence;

      cluster (seq1 - seq2) -> convergent;

      coherence by Th11;

    end

    theorem :: SEQ_2:12

    

     Th12: seq is convergent & seq9 is convergent implies ( lim (seq - seq9)) = (( lim seq) - ( lim seq9))

    proof

      assume that

       A1: seq is convergent and

       A2: seq9 is convergent;

      

      thus ( lim (seq - seq9)) = (( lim seq) + ( lim ( - seq9))) by A1, A2, Th6

      .= (( lim seq) + ( - ( lim seq9))) by A2, Th10

      .= (( lim seq) - ( lim seq9));

    end;

    theorem :: SEQ_2:13

    

     Th13: seq is convergent implies seq is bounded

    proof

      assume seq is convergent;

      then

      consider g such that

       A1: for p st 0 < p holds ex n st for m st n <= m holds |.((seq . m) - g).| < p;

      consider n1 such that

       A2: for m st n1 <= m holds |.((seq . m) - g).| < 1 by A1;

       A3:

      now

        take r = ( |.g.| + 1);

        ( 0 + 0 ) < r by COMPLEX1: 46, XREAL_1: 8;

        hence 0 < r;

        let m;

        assume n1 <= m;

        then

         A4: |.((seq . m) - g).| < 1 by A2;

        ( |.(seq . m).| - |.g.|) <= |.((seq . m) - g).| by COMPLEX1: 59;

        then

         A5: ( |.(seq . m).| - |.g.|) < 1 by A4, XXREAL_0: 2;

        (( |.(seq . m).| - |.g.|) + |.g.|) = |.(seq . m).|;

        hence |.(seq . m).| < r by A5, XREAL_1: 6;

      end;

      now

        consider r1 such that

         A6: 0 < r1 and

         A7: for m st n1 <= m holds |.(seq . m).| < r1 by A3;

        consider r2 such that

         A8: 0 < r2 and

         A9: for m st m <= n1 holds |.(seq . m).| < r2 by Th4;

        take r = (r1 + r2);

        thus 0 < r by A6, A8;

        

         A10: (r1 + 0 ) < r by A8, XREAL_1: 8;

        

         A11: ( 0 + r2) < r by A6, XREAL_1: 8;

        let m;

         A12:

        now

          assume n1 <= m;

          then |.(seq . m).| < r1 by A7;

          hence |.(seq . m).| < r by A10, XXREAL_0: 2;

        end;

        now

          assume m <= n1;

          then |.(seq . m).| < r2 by A9;

          hence |.(seq . m).| < r by A11, XXREAL_0: 2;

        end;

        hence |.(seq . m).| < r by A12;

      end;

      hence thesis by Th3;

    end;

    registration

      cluster convergent -> bounded for Real_Sequence;

      coherence by Th13;

    end

    theorem :: SEQ_2:14

    

     Th14: seq is convergent & seq9 is convergent implies (seq (#) seq9) is convergent

    proof

      assume that

       A1: seq is convergent and

       A2: seq9 is convergent;

      consider g1 such that

       A3: for p st 0 < p holds ex n st for m st n <= m holds |.((seq . m) - g1).| < p by A1;

      consider g2 such that

       A4: for p st 0 < p holds ex n st for m st n <= m holds |.((seq9 . m) - g2).| < p by A2;

      take g = (g1 * g2);

      consider r such that

       A5: 0 < r and

       A6: for n holds |.(seq . n).| < r by A1, Th3;

      

       A7: 0 <= |.g2.| by COMPLEX1: 46;

      

       A8: ( 0 + 0 ) < ( |.g2.| + r) by A5, COMPLEX1: 46, XREAL_1: 8;

      let p;

      assume

       A9: 0 < p;

      then

      consider n1 such that

       A10: for m st n1 <= m holds |.((seq . m) - g1).| < (p / ( |.g2.| + r)) by A3, A8;

      consider n2 such that

       A11: for m st n2 <= m holds |.((seq9 . m) - g2).| < (p / ( |.g2.| + r)) by A4, A8, A9;

      take n = (n1 + n2);

      let m such that

       A12: n <= m;

      

       A13: 0 <= |.(seq . m).| by COMPLEX1: 46;

      

       A14: 0 <= |.((seq9 . m) - g2).| by COMPLEX1: 46;

      n2 <= n by NAT_1: 12;

      then n2 <= m by A12, XXREAL_0: 2;

      then

       A15: |.((seq9 . m) - g2).| < (p / ( |.g2.| + r)) by A11;

      n1 <= (n1 + n2) by NAT_1: 12;

      then n1 <= m by A12, XXREAL_0: 2;

      then

       A16: |.((seq . m) - g1).| <= (p / ( |.g2.| + r)) by A10;

       |.(((seq (#) seq9) . m) - g).| = |.((((seq . m) * (seq9 . m)) - (((seq . m) * g2) - ((seq . m) * g2))) - (g1 * g2)).| by SEQ_1: 8

      .= |.(((seq . m) * ((seq9 . m) - g2)) + (((seq . m) - g1) * g2)).|;

      then

       A17: |.(((seq (#) seq9) . m) - g).| <= ( |.((seq . m) * ((seq9 . m) - g2)).| + |.(((seq . m) - g1) * g2).|) by COMPLEX1: 56;

       |.(seq . m).| < r by A6;

      then ( |.(seq . m).| * |.((seq9 . m) - g2).|) < (r * (p / ( |.g2.| + r))) by A13, A14, A15, XREAL_1: 96;

      then

       A18: |.((seq . m) * ((seq9 . m) - g2)).| < (r * (p / ( |.g2.| + r))) by COMPLEX1: 65;

       |.(((seq . m) - g1) * g2).| = ( |.g2.| * |.((seq . m) - g1).|) by COMPLEX1: 65;

      then

       A19: |.(((seq . m) - g1) * g2).| <= ( |.g2.| * (p / ( |.g2.| + r))) by A7, A16, XREAL_1: 64;

      ((r * (p / ( |.g2.| + r))) + ( |.g2.| * (p / ( |.g2.| + r)))) = ((p / ( |.g2.| + r)) * ( |.g2.| + r))

      .= p by A8, XCMPLX_1: 87;

      then ( |.((seq . m) * ((seq9 . m) - g2)).| + |.(((seq . m) - g1) * g2).|) < p by A18, A19, XREAL_1: 8;

      hence thesis by A17, XXREAL_0: 2;

    end;

    registration

      let seq1,seq2 be convergent Real_Sequence;

      cluster (seq1 (#) seq2) -> convergent;

      coherence by Th14;

    end

    theorem :: SEQ_2:15

    

     Th15: seq is convergent & seq9 is convergent implies ( lim (seq (#) seq9)) = (( lim seq) * ( lim seq9))

    proof

      assume that

       A1: seq is convergent and

       A2: seq9 is convergent;

      consider r such that

       A3: 0 < r and

       A4: for n holds |.(seq . n).| < r by A1, Th3;

      

       A5: 0 <= |.( lim seq9).| by COMPLEX1: 46;

      

       A6: ( 0 + 0 ) < ( |.( lim seq9).| + r) by A3, COMPLEX1: 46, XREAL_1: 8;

      now

        let p;

        assume 0 < p;

        then

         A7: 0 < (p / ( |.( lim seq9).| + r)) by A6;

        then

        consider n1 such that

         A8: for m st n1 <= m holds |.((seq . m) - ( lim seq)).| < (p / ( |.( lim seq9).| + r)) by A1, Def6;

        consider n2 such that

         A9: for m st n2 <= m holds |.((seq9 . m) - ( lim seq9)).| < (p / ( |.( lim seq9).| + r)) by A2, A7, Def6;

        take n = (n1 + n2);

        let m such that

         A10: n <= m;

        

         A11: 0 <= |.(seq . m).| by COMPLEX1: 46;

        

         A12: 0 <= |.((seq9 . m) - ( lim seq9)).| by COMPLEX1: 46;

        n2 <= n by NAT_1: 12;

        then n2 <= m by A10, XXREAL_0: 2;

        then

         A13: |.((seq9 . m) - ( lim seq9)).| < (p / ( |.( lim seq9).| + r)) by A9;

        n1 <= (n1 + n2) by NAT_1: 12;

        then n1 <= m by A10, XXREAL_0: 2;

        then

         A14: |.((seq . m) - ( lim seq)).| <= (p / ( |.( lim seq9).| + r)) by A8;

         |.(((seq (#) seq9) . m) - (( lim seq) * ( lim seq9))).| = |.((((seq . m) * (seq9 . m)) - (((seq . m) * ( lim seq9)) - ((seq . m) * ( lim seq9)))) - (( lim seq) * ( lim seq9))).| by SEQ_1: 8

        .= |.(((seq . m) * ((seq9 . m) - ( lim seq9))) + (((seq . m) - ( lim seq)) * ( lim seq9))).|;

        then

         A15: |.(((seq (#) seq9) . m) - (( lim seq) * ( lim seq9))).| <= ( |.((seq . m) * ((seq9 . m) - ( lim seq9))).| + |.(((seq . m) - ( lim seq)) * ( lim seq9)).|) by COMPLEX1: 56;

         |.(seq . m).| < r by A4;

        then ( |.(seq . m).| * |.((seq9 . m) - ( lim seq9)).|) < (r * (p / ( |.( lim seq9).| + r))) by A11, A12, A13, XREAL_1: 96;

        then

         A16: |.((seq . m) * ((seq9 . m) - ( lim seq9))).| < (r * (p / ( |.( lim seq9).| + r))) by COMPLEX1: 65;

         |.(((seq . m) - ( lim seq)) * ( lim seq9)).| = ( |.( lim seq9).| * |.((seq . m) - ( lim seq)).|) by COMPLEX1: 65;

        then

         A17: |.(((seq . m) - ( lim seq)) * ( lim seq9)).| <= ( |.( lim seq9).| * (p / ( |.( lim seq9).| + r))) by A5, A14, XREAL_1: 64;

        ((r * (p / ( |.( lim seq9).| + r))) + ( |.( lim seq9).| * (p / ( |.( lim seq9).| + r)))) = ((p / ( |.( lim seq9).| + r)) * ( |.( lim seq9).| + r))

        .= p by A6, XCMPLX_1: 87;

        then ( |.((seq . m) * ((seq9 . m) - ( lim seq9))).| + |.(((seq . m) - ( lim seq)) * ( lim seq9)).|) < p by A16, A17, XREAL_1: 8;

        hence |.(((seq (#) seq9) . m) - (( lim seq) * ( lim seq9))).| < p by A15, XXREAL_0: 2;

      end;

      hence thesis by A1, A2, Def6;

    end;

    theorem :: SEQ_2:16

    

     Th16: seq is convergent implies (( lim seq) <> 0 implies ex n st for m st n <= m holds ( |.( lim seq).| / 2) < |.(seq . m).|)

    proof

      assume that

       A1: seq is convergent and

       A2: ( lim seq) <> 0 ;

       0 < |.( lim seq).| by A2, COMPLEX1: 47;

      then 0 < ( |.( lim seq).| / 2);

      then

      consider n1 such that

       A3: for m st n1 <= m holds |.((seq . m) - ( lim seq)).| < ( |.( lim seq).| / 2) by A1, Def6;

      take n = n1;

      let m;

      assume n <= m;

      then

       A4: |.((seq . m) - ( lim seq)).| < ( |.( lim seq).| / 2) by A3;

      

       A5: ( |.( lim seq).| - |.(seq . m).|) <= |.(( lim seq) - (seq . m)).| by COMPLEX1: 59;

       |.(( lim seq) - (seq . m)).| = |.( - ((seq . m) - ( lim seq))).|

      .= |.((seq . m) - ( lim seq)).| by COMPLEX1: 52;

      then

       A6: ( |.( lim seq).| - |.(seq . m).|) < ( |.( lim seq).| / 2) by A4, A5, XXREAL_0: 2;

      

       A7: (( |.( lim seq).| / 2) + ( |.(seq . m).| - ( |.( lim seq).| / 2))) = |.(seq . m).|;

      (( |.( lim seq).| - |.(seq . m).|) + ( |.(seq . m).| - ( |.( lim seq).| / 2))) = ( |.( lim seq).| / 2);

      hence thesis by A6, A7, XREAL_1: 6;

    end;

    theorem :: SEQ_2:17

    

     Th17: seq is convergent & (for n holds 0 <= (seq . n)) implies 0 <= ( lim seq)

    proof

      assume that

       A1: seq is convergent and

       A2: for n holds 0 <= (seq . n) and

       A3: not 0 <= ( lim seq);

       0 < ( - ( lim seq)) by A3;

      then

      consider n1 such that

       A4: for m st n1 <= m holds |.((seq . m) - ( lim seq)).| < ( - ( lim seq)) by A1, Def6;

       |.((seq . n1) - ( lim seq)).| <= ( - ( lim seq)) by A4;

      then ((seq . n1) - ( lim seq)) <= ( - ( lim seq)) by ABSVALUE: 5;

      then

       A5: (((seq . n1) - ( lim seq)) + ( lim seq)) <= (( - ( lim seq)) + ( lim seq)) by XREAL_1: 6;

      now

        assume (seq . n1) = 0 ;

        then |.((seq . n1) - ( lim seq)).| = ( - ( lim seq)) by A3, ABSVALUE:def 1;

        hence contradiction by A4;

      end;

      hence contradiction by A2, A5;

    end;

    theorem :: SEQ_2:18

    seq is convergent & seq9 is convergent & (for n holds (seq . n) <= (seq9 . n)) implies ( lim seq) <= ( lim seq9)

    proof

      assume that

       A1: seq is convergent and

       A2: seq9 is convergent and

       A3: for n holds (seq . n) <= (seq9 . n);

      now

        let n;

        (seq . n) <= (seq9 . n) by A3;

        then

         A4: ((seq . n) - (seq . n)) <= ((seq9 . n) - (seq . n)) by XREAL_1: 9;

        ((seq9 - seq) . n) = ((seq9 . n) + (( - seq) . n)) by SEQ_1: 7

        .= ((seq9 . n) + ( - (seq . n))) by SEQ_1: 10

        .= ((seq9 . n) - (seq . n));

        hence 0 <= ((seq9 - seq) . n) by A4;

      end;

      then

       A5: 0 <= ( lim (seq9 - seq)) by A1, A2, Th17;

      ( lim (seq9 - seq)) = (( lim seq9) - ( lim seq)) by A1, A2, Th12;

      then ( 0 + ( lim seq)) <= ((( lim seq9) - ( lim seq)) + ( lim seq)) by A5, XREAL_1: 6;

      hence thesis;

    end;

    theorem :: SEQ_2:19

    

     Th19: seq is convergent & seq9 is convergent & (for n holds (seq . n) <= (seq1 . n) & (seq1 . n) <= (seq9 . n)) & ( lim seq) = ( lim seq9) implies seq1 is convergent

    proof

      assume that

       A1: seq is convergent and

       A2: seq9 is convergent and

       A3: for n holds (seq . n) <= (seq1 . n) & (seq1 . n) <= (seq9 . n) and

       A4: ( lim seq) = ( lim seq9);

      take ( lim seq);

      let p;

      assume

       A5: 0 < p;

      then

      consider n1 such that

       A6: for m st n1 <= m holds |.((seq . m) - ( lim seq)).| < p by A1, Def6;

      consider n2 such that

       A7: for m st n2 <= m holds |.((seq9 . m) - ( lim seq)).| < p by A2, A4, A5, Def6;

      take n = (n1 + n2);

      let m such that

       A8: n <= m;

      n2 <= n by NAT_1: 12;

      then n2 <= m by A8, XXREAL_0: 2;

      then |.((seq9 . m) - ( lim seq)).| < p by A7;

      then

       A9: ((seq9 . m) - ( lim seq)) < p by Th1;

      n1 <= (n1 + n2) by NAT_1: 12;

      then n1 <= m by A8, XXREAL_0: 2;

      then |.((seq . m) - ( lim seq)).| < p by A6;

      then

       A10: ( - p) < ((seq . m) - ( lim seq)) by Th1;

      (seq . m) <= (seq1 . m) by A3;

      then ((seq . m) - ( lim seq)) <= ((seq1 . m) - ( lim seq)) by XREAL_1: 9;

      then

       A11: ( - p) < ((seq1 . m) - ( lim seq)) by A10, XXREAL_0: 2;

      (seq1 . m) <= (seq9 . m) by A3;

      then ((seq1 . m) - ( lim seq)) <= ((seq9 . m) - ( lim seq)) by XREAL_1: 9;

      then ((seq1 . m) - ( lim seq)) < p by A9, XXREAL_0: 2;

      hence thesis by A11, Th1;

    end;

    theorem :: SEQ_2:20

    seq is convergent & seq9 is convergent & (for n holds (seq . n) <= (seq1 . n) & (seq1 . n) <= (seq9 . n)) & ( lim seq) = ( lim seq9) implies ( lim seq1) = ( lim seq)

    proof

      assume that

       A1: seq is convergent and

       A2: seq9 is convergent and

       A3: for n holds (seq . n) <= (seq1 . n) & (seq1 . n) <= (seq9 . n) and

       A4: ( lim seq) = ( lim seq9);

      

       A5: seq1 is convergent by A1, A2, A3, A4, Th19;

      now

        let p;

        assume

         A6: 0 < p;

        then

        consider n1 such that

         A7: for m st n1 <= m holds |.((seq . m) - ( lim seq)).| < p by A1, Def6;

        consider n2 such that

         A8: for m st n2 <= m holds |.((seq9 . m) - ( lim seq)).| < p by A2, A4, A6, Def6;

        take n = (n1 + n2);

        let m such that

         A9: n <= m;

        n2 <= n by NAT_1: 12;

        then n2 <= m by A9, XXREAL_0: 2;

        then |.((seq9 . m) - ( lim seq)).| < p by A8;

        then

         A10: ((seq9 . m) - ( lim seq)) < p by Th1;

        n1 <= (n1 + n2) by NAT_1: 12;

        then n1 <= m by A9, XXREAL_0: 2;

        then |.((seq . m) - ( lim seq)).| < p by A7;

        then

         A11: ( - p) < ((seq . m) - ( lim seq)) by Th1;

        (seq . m) <= (seq1 . m) by A3;

        then ((seq . m) - ( lim seq)) <= ((seq1 . m) - ( lim seq)) by XREAL_1: 9;

        then

         A12: ( - p) < ((seq1 . m) - ( lim seq)) by A11, XXREAL_0: 2;

        (seq1 . m) <= (seq9 . m) by A3;

        then ((seq1 . m) - ( lim seq)) <= ((seq9 . m) - ( lim seq)) by XREAL_1: 9;

        then ((seq1 . m) - ( lim seq)) < p by A10, XXREAL_0: 2;

        hence |.((seq1 . m) - ( lim seq)).| < p by A12, Th1;

      end;

      hence thesis by A5, Def6;

    end;

    theorem :: SEQ_2:21

    

     Th21: seq is convergent & ( lim seq) <> 0 & seq is non-zero implies (seq " ) is convergent

    proof

      assume that

       A1: seq is convergent and

       A2: ( lim seq) <> 0 and

       A3: seq is non-zero;

      

       A4: 0 < |.( lim seq).| by A2, COMPLEX1: 47;

      

       A5: 0 <> |.( lim seq).| by A2, COMPLEX1: 47;

      consider n1 such that

       A6: for m st n1 <= m holds ( |.( lim seq).| / 2) < |.(seq . m).| by A1, A2, Th16;

      ( 0 * 0 ) < ( |.( lim seq).| * |.( lim seq).|) by A4;

      then

       A7: 0 < (( |.( lim seq).| * |.( lim seq).|) / 2);

      take (( lim seq) " );

      let p;

      assume

       A8: 0 < p;

      then ( 0 * 0 ) < (p * (( |.( lim seq).| * |.( lim seq).|) / 2)) by A7;

      then

      consider n2 such that

       A9: for m st n2 <= m holds |.((seq . m) - ( lim seq)).| < (p * (( |.( lim seq).| * |.( lim seq).|) / 2)) by A1, Def6;

      take n = (n1 + n2);

      let m such that

       A10: n <= m;

      n2 <= n by NAT_1: 12;

      then n2 <= m by A10, XXREAL_0: 2;

      then

       A11: |.((seq . m) - ( lim seq)).| < (p * (( |.( lim seq).| * |.( lim seq).|) / 2)) by A9;

      n1 <= (n1 + n2) by NAT_1: 12;

      then n1 <= m by A10, XXREAL_0: 2;

      then

       A12: ( |.( lim seq).| / 2) < |.(seq . m).| by A6;

      

       A13: (seq . m) <> 0 by A3, SEQ_1: 5;

      then ((seq . m) * ( lim seq)) <> 0 by A2;

      then 0 < |.((seq . m) * ( lim seq)).| by COMPLEX1: 47;

      then 0 < ( |.(seq . m).| * |.( lim seq).|) by COMPLEX1: 65;

      then

       A14: ( |.((seq . m) - ( lim seq)).| / ( |.(seq . m).| * |.( lim seq).|)) < ((p * (( |.( lim seq).| * |.( lim seq).|) / 2)) / ( |.(seq . m).| * |.( lim seq).|)) by A11, XREAL_1: 74;

      

       A15: ((p * (( |.( lim seq).| * |.( lim seq).|) / 2)) / ( |.(seq . m).| * |.( lim seq).|)) = ((p * ((2 " ) * ( |.( lim seq).| * |.( lim seq).|))) * (( |.(seq . m).| * |.( lim seq).|) " )) by XCMPLX_0:def 9

      .= ((p * (2 " )) * (( |.( lim seq).| * |.( lim seq).|) * (( |.( lim seq).| * |.(seq . m).|) " )))

      .= ((p * (2 " )) * (( |.( lim seq).| * |.( lim seq).|) * (( |.( lim seq).| " ) * ( |.(seq . m).| " )))) by XCMPLX_1: 204

      .= ((p * (2 " )) * (( |.( lim seq).| * ( |.( lim seq).| * ( |.( lim seq).| " ))) * ( |.(seq . m).| " )))

      .= ((p * (2 " )) * (( |.( lim seq).| * 1) * ( |.(seq . m).| " ))) by A5, XCMPLX_0:def 7

      .= ((p * ( |.( lim seq).| / 2)) * ( |.(seq . m).| " ))

      .= ((p * ( |.( lim seq).| / 2)) / |.(seq . m).|) by XCMPLX_0:def 9;

      

       A16: |.(((seq " ) . m) - (( lim seq) " )).| = |.(((seq . m) " ) - (( lim seq) " )).| by VALUED_1: 10

      .= ( |.((seq . m) - ( lim seq)).| / ( |.(seq . m).| * |.( lim seq).|)) by A2, A13, Th2;

      

       A17: 0 < ( |.( lim seq).| / 2) by A4;

      

       A18: 0 <> ( |.( lim seq).| / 2) by A2, COMPLEX1: 47;

      ( 0 * 0 ) < (p * ( |.( lim seq).| / 2)) by A8, A17;

      then

       A19: ((p * ( |.( lim seq).| / 2)) / |.(seq . m).|) < ((p * ( |.( lim seq).| / 2)) / ( |.( lim seq).| / 2)) by A12, A17, XREAL_1: 76;

      ((p * ( |.( lim seq).| / 2)) / ( |.( lim seq).| / 2)) = ((p * ( |.( lim seq).| / 2)) * (( |.( lim seq).| / 2) " )) by XCMPLX_0:def 9

      .= (p * (( |.( lim seq).| / 2) * (( |.( lim seq).| / 2) " )))

      .= (p * 1) by A18, XCMPLX_0:def 7

      .= p;

      hence thesis by A14, A15, A16, A19, XXREAL_0: 2;

    end;

    theorem :: SEQ_2:22

    

     Th22: seq is convergent & ( lim seq) <> 0 & seq is non-zero implies ( lim (seq " )) = (( lim seq) " )

    proof

      assume that

       A1: seq is convergent and

       A2: ( lim seq) <> 0 and

       A3: seq is non-zero;

      

       A4: (seq " ) is convergent by A1, A2, A3, Th21;

      

       A5: 0 < |.( lim seq).| by A2, COMPLEX1: 47;

      

       A6: 0 <> |.( lim seq).| by A2, COMPLEX1: 47;

      consider n1 such that

       A7: for m st n1 <= m holds ( |.( lim seq).| / 2) < |.(seq . m).| by A1, A2, Th16;

      ( 0 * 0 ) < ( |.( lim seq).| * |.( lim seq).|) by A5;

      then

       A8: 0 < (( |.( lim seq).| * |.( lim seq).|) / 2);

      now

        let p;

        assume

         A9: 0 < p;

        then ( 0 * 0 ) < (p * (( |.( lim seq).| * |.( lim seq).|) / 2)) by A8;

        then

        consider n2 such that

         A10: for m st n2 <= m holds |.((seq . m) - ( lim seq)).| < (p * (( |.( lim seq).| * |.( lim seq).|) / 2)) by A1, Def6;

        take n = (n1 + n2);

        let m such that

         A11: n <= m;

        n2 <= n by NAT_1: 12;

        then n2 <= m by A11, XXREAL_0: 2;

        then

         A12: |.((seq . m) - ( lim seq)).| < (p * (( |.( lim seq).| * |.( lim seq).|) / 2)) by A10;

        n1 <= (n1 + n2) by NAT_1: 12;

        then n1 <= m by A11, XXREAL_0: 2;

        then

         A13: ( |.( lim seq).| / 2) < |.(seq . m).| by A7;

        

         A14: (seq . m) <> 0 by A3, SEQ_1: 5;

        then ((seq . m) * ( lim seq)) <> 0 by A2;

        then 0 < |.((seq . m) * ( lim seq)).| by COMPLEX1: 47;

        then 0 < ( |.(seq . m).| * |.( lim seq).|) by COMPLEX1: 65;

        then

         A15: ( |.((seq . m) - ( lim seq)).| / ( |.(seq . m).| * |.( lim seq).|)) < ((p * (( |.( lim seq).| * |.( lim seq).|) / 2)) / ( |.(seq . m).| * |.( lim seq).|)) by A12, XREAL_1: 74;

        

         A16: ((p * (( |.( lim seq).| * |.( lim seq).|) / 2)) / ( |.(seq . m).| * |.( lim seq).|)) = ((p * ((2 " ) * ( |.( lim seq).| * |.( lim seq).|))) * (( |.(seq . m).| * |.( lim seq).|) " )) by XCMPLX_0:def 9

        .= ((p * (2 " )) * (( |.( lim seq).| * |.( lim seq).|) * (( |.( lim seq).| * |.(seq . m).|) " )))

        .= ((p * (2 " )) * (( |.( lim seq).| * |.( lim seq).|) * (( |.( lim seq).| " ) * ( |.(seq . m).| " )))) by XCMPLX_1: 204

        .= ((p * (2 " )) * (( |.( lim seq).| * ( |.( lim seq).| * ( |.( lim seq).| " ))) * ( |.(seq . m).| " )))

        .= ((p * (2 " )) * (( |.( lim seq).| * 1) * ( |.(seq . m).| " ))) by A6, XCMPLX_0:def 7

        .= ((p * ( |.( lim seq).| / 2)) * ( |.(seq . m).| " ))

        .= ((p * ( |.( lim seq).| / 2)) / |.(seq . m).|) by XCMPLX_0:def 9;

        

         A17: |.(((seq " ) . m) - (( lim seq) " )).| = |.(((seq . m) " ) - (( lim seq) " )).| by VALUED_1: 10

        .= ( |.((seq . m) - ( lim seq)).| / ( |.(seq . m).| * |.( lim seq).|)) by A2, A14, Th2;

        

         A18: 0 < ( |.( lim seq).| / 2) by A5;

        

         A19: 0 <> ( |.( lim seq).| / 2) by A2, COMPLEX1: 47;

        ( 0 * 0 ) < (p * ( |.( lim seq).| / 2)) by A9, A18;

        then

         A20: ((p * ( |.( lim seq).| / 2)) / |.(seq . m).|) < ((p * ( |.( lim seq).| / 2)) / ( |.( lim seq).| / 2)) by A13, A18, XREAL_1: 76;

        ((p * ( |.( lim seq).| / 2)) / ( |.( lim seq).| / 2)) = ((p * ( |.( lim seq).| / 2)) * (( |.( lim seq).| / 2) " )) by XCMPLX_0:def 9

        .= (p * (( |.( lim seq).| / 2) * (( |.( lim seq).| / 2) " )))

        .= (p * 1) by A19, XCMPLX_0:def 7

        .= p;

        hence |.(((seq " ) . m) - (( lim seq) " )).| < p by A15, A16, A17, A20, XXREAL_0: 2;

      end;

      hence thesis by A4, Def6;

    end;

    theorem :: SEQ_2:23

    seq9 is convergent & seq is convergent & ( lim seq) <> 0 & seq is non-zero implies (seq9 /" seq) is convergent

    proof

      assume that

       A1: seq9 is convergent and

       A2: seq is convergent and

       A3: ( lim seq) <> 0 and

       A4: seq is non-zero;

      (seq " ) is convergent by A2, A3, A4, Th21;

      hence thesis by A1;

    end;

    theorem :: SEQ_2:24

    seq9 is convergent & seq is convergent & ( lim seq) <> 0 & seq is non-zero implies ( lim (seq9 /" seq)) = (( lim seq9) / ( lim seq))

    proof

      assume that

       A1: seq9 is convergent and

       A2: seq is convergent and

       A3: ( lim seq) <> 0 and

       A4: seq is non-zero;

      (seq " ) is convergent by A2, A3, A4, Th21;

      

      then ( lim (seq9 (#) (seq " ))) = (( lim seq9) * ( lim (seq " ))) by A1, Th15

      .= (( lim seq9) * (( lim seq) " )) by A2, A3, A4, Th22

      .= (( lim seq9) / ( lim seq)) by XCMPLX_0:def 9;

      hence thesis;

    end;

    theorem :: SEQ_2:25

    

     Th25: seq is convergent & seq1 is bounded & ( lim seq) = 0 implies (seq (#) seq1) is convergent

    proof

      assume that

       A1: seq is convergent and

       A2: seq1 is bounded and

       A3: ( lim seq) = 0 ;

      reconsider g1 = 0 as Real;

      take g = g1;

      let p such that

       A4: 0 < p;

      consider r such that

       A5: 0 < r and

       A6: for m holds |.(seq1 . m).| < r by A2, Th3;

      

       A7: 0 < (p / r) by A4, A5;

      then

      consider n1 such that

       A8: for m st n1 <= m holds |.((seq . m) - 0 ).| < (p / r) by A1, A3, Def6;

      take n = n1;

      let m such that

       A9: n <= m;

       |.(seq . m).| = |.((seq . m) - 0 ).|;

      then

       A10: |.(seq . m).| < (p / r) by A8, A9;

      

       A11: |.(((seq (#) seq1) . m) - g).| = |.(((seq . m) * (seq1 . m)) - 0 ).| by SEQ_1: 8

      .= ( |.(seq . m).| * |.(seq1 . m).|) by COMPLEX1: 65;

      now

        assume

         A12: |.(seq1 . m).| <> 0 ;

        ((p / r) * r) = ((p * (r " )) * r) by XCMPLX_0:def 9

        .= (p * ((r " ) * r))

        .= (p * 1) by A5, XCMPLX_0:def 7

        .= p;

        then

         A13: ((p / r) * |.(seq1 . m).|) < p by A6, A7, XREAL_1: 68;

         0 <= |.(seq1 . m).| by COMPLEX1: 46;

        then |.(((seq (#) seq1) . m) - g).| < ((p / r) * |.(seq1 . m).|) by A10, A11, A12, XREAL_1: 68;

        hence thesis by A13, XXREAL_0: 2;

      end;

      hence thesis by A4, A11;

    end;

    theorem :: SEQ_2:26

    seq is convergent & seq1 is bounded & ( lim seq) = 0 implies ( lim (seq (#) seq1)) = 0

    proof

      assume that

       A1: seq is convergent and

       A2: seq1 is bounded and

       A3: ( lim seq) = 0 ;

      

       A4: (seq (#) seq1) is convergent by A1, A2, A3, Th25;

      now

        let p such that

         A5: 0 < p;

        consider r such that

         A6: 0 < r and

         A7: for m holds |.(seq1 . m).| < r by A2, Th3;

        

         A8: 0 < (p / r) by A5, A6;

        then

        consider n1 such that

         A9: for m st n1 <= m holds |.((seq . m) - 0 ).| < (p / r) by A1, A3, Def6;

        take n = n1;

        let m;

        assume n <= m;

        then

         A10: |.((seq . m) - 0 ).| < (p / r) by A9;

        

         A11: |.(((seq (#) seq1) . m) - 0 ).| = |.(((seq . m) * (seq1 . m)) - 0 ).| by SEQ_1: 8

        .= ( |.(seq . m).| * |.(seq1 . m).|) by COMPLEX1: 65;

        now

          assume

           A12: |.(seq1 . m).| <> 0 ;

          ((p / r) * r) = ((p * (r " )) * r) by XCMPLX_0:def 9

          .= (p * ((r " ) * r))

          .= (p * 1) by A6, XCMPLX_0:def 7;

          then

           A13: ((p / r) * |.(seq1 . m).|) < p by A7, A8, XREAL_1: 68;

           0 <= |.(seq1 . m).| by COMPLEX1: 46;

          then |.(((seq (#) seq1) . m) - 0 ).| < ((p / r) * |.(seq1 . m).|) by A10, A11, A12, XREAL_1: 68;

          hence |.(((seq (#) seq1) . m) - 0 ).| < p by A13, XXREAL_0: 2;

        end;

        hence |.(((seq (#) seq1) . m) - 0 ).| < p by A5, A11;

      end;

      hence thesis by A4, Def6;

    end;

    reserve g for Complex;

    registration

      let s be convergent Complex_Sequence;

      cluster |.s.| -> convergent;

      coherence

      proof

         |.s.| is convergent

        proof

          consider g such that

           A1: for p be Real st 0 < p holds ex n st for m st n <= m holds |.((s . m) - g).| < p by COMSEQ_2:def 5;

          take |.g.|;

          let p be Real;

          assume

           A2: 0 < p;

          consider n such that

           A3: for m st n <= m holds |.((s . m) - g).| < p by A1, A2;

          take n;

          let m;

          assume n <= m;

          then |.((s . m) - g).| < p by A3;

          then ( |.( |.(s . m).| - |.g.|).| + |.((s . m) - g).|) < (p + |.((s . m) - g).|) by COMPLEX1: 64, XREAL_1: 8;

          then (( |.( |.(s . m).| - |.g.|).| + |.((s . m) - g).|) - |.((s . m) - g).|) < ((p + |.((s . m) - g).|) - |.((s . m) - g).|) by XREAL_1: 9;

          hence thesis by VALUED_1: 18;

        end;

        hence thesis;

      end;

    end

    reserve s,s1,s9 for Complex_Sequence;

    theorem :: SEQ_2:27

    

     Th27: s is convergent implies ( lim |.s.|) = |.( lim s).|

    proof

      set g = ( lim s);

      assume

       A1: s is convergent;

      then

      reconsider s1 = s as convergent Complex_Sequence;

      reconsider w = |.s1.| as Real_Sequence;

      

       A2: w is convergent;

      reconsider w = |.( lim s).| as Real;

      now

        let p be Real;

        assume

         A3: 0 < p;

        consider n such that

         A4: for m st n <= m holds |.((s . m) - g).| < p by A1, A3, COMSEQ_2:def 6;

        take n;

        let m;

        assume n <= m;

        then |.((s . m) - g).| < p by A4;

        then ( |.( |.(s . m).| - |.g.|).| + |.((s . m) - g).|) < (p + |.((s . m) - g).|) by COMPLEX1: 64, XREAL_1: 8;

        then (( |.( |.(s . m).| - |.g.|).| + |.((s . m) - g).|) - |.((s . m) - g).|) < ((p + |.((s . m) - g).|) - |.((s . m) - g).|) by XREAL_1: 9;

        hence |.(( |.s.| . m) - w).| < p by VALUED_1: 18;

      end;

      hence thesis by A2, Def6;

    end;

    theorem :: SEQ_2:28

    for s,s9 be convergent Complex_Sequence holds ( lim |.(s + s9).|) = |.(( lim s) + ( lim s9)).|

    proof

      let s,s9 be convergent Complex_Sequence;

      

      thus ( lim |.(s + s9).|) = |.( lim (s + s9)).| by Th27

      .= |.(( lim s) + ( lim s9)).| by COMSEQ_2: 14;

    end;

    theorem :: SEQ_2:29

    for s be convergent Complex_Sequence holds ( lim |.(r (#) s).|) = ( |.r.| * |.( lim s).|)

    proof

      let s be convergent Complex_Sequence;

      

      thus ( lim |.(r (#) s).|) = |.( lim (r (#) s)).| by Th27

      .= |.(r * ( lim s)).| by COMSEQ_2: 18

      .= ( |.r.| * |.( lim s).|) by COMPLEX1: 65;

    end;

    theorem :: SEQ_2:30

    for s be convergent Complex_Sequence holds ( lim |.( - s).|) = |.( lim s).|

    proof

      let s be convergent Complex_Sequence;

      

      thus ( lim |.( - s).|) = |.( lim ( - s)).| by Th27

      .= |.( - ( lim s)).| by COMSEQ_2: 22

      .= |.( lim s).| by COMPLEX1: 52;

    end;

    theorem :: SEQ_2:31

    for s,s9 be convergent Complex_Sequence holds ( lim |.(s - s9).|) = |.(( lim s) - ( lim s9)).|

    proof

      let s,s9 be convergent Complex_Sequence;

      

      thus ( lim |.(s - s9).|) = |.( lim (s - s9)).| by Th27

      .= |.(( lim s) - ( lim s9)).| by COMSEQ_2: 26;

    end;

    theorem :: SEQ_2:32

    for s,s9 be convergent Complex_Sequence holds ( lim |.(s (#) s9).|) = ( |.( lim s).| * |.( lim s9).|)

    proof

      let s,s9 be convergent Complex_Sequence;

      

      thus ( lim |.(s (#) s9).|) = |.( lim (s (#) s9)).| by Th27

      .= |.(( lim s) * ( lim s9)).| by COMSEQ_2: 30

      .= ( |.( lim s).| * |.( lim s9).|) by COMPLEX1: 65;

    end;

    theorem :: SEQ_2:33

    s is convergent & ( lim s) <> 0c & s is non-zero implies ( lim |.(s " ).|) = ( |.( lim s).| " )

    proof

      assume

       A1: s is convergent & ( lim s) <> 0c & s is non-zero;

      then (s " ) is convergent by COMSEQ_2: 34;

      

      hence ( lim |.(s " ).|) = |.( lim (s " )).| by Th27

      .= |.(( lim s) " ).| by A1, COMSEQ_2: 35

      .= ( |.( lim s).| " ) by COMPLEX1: 66;

    end;

    theorem :: SEQ_2:34

    s9 is convergent & s is convergent & ( lim s) <> 0c & s is non-zero implies ( lim |.(s9 /" s).|) = ( |.( lim s9).| / |.( lim s).|)

    proof

      assume

       A1: s9 is convergent & s is convergent & ( lim s) <> 0c & s is non-zero;

      then (s9 /" s) is convergent by COMSEQ_2: 38;

      

      hence ( lim |.(s9 /" s).|) = |.( lim (s9 /" s)).| by Th27

      .= |.(( lim s9) / ( lim s)).| by A1, COMSEQ_2: 39

      .= ( |.( lim s9).| / |.( lim s).|) by COMPLEX1: 67;

    end;

    theorem :: SEQ_2:35

    s is convergent & s1 is bounded & ( lim s) = 0c implies ( lim |.(s (#) s1).|) = 0

    proof

      assume

       A1: s is convergent & s1 is bounded & ( lim s) = 0c ;

      then (s (#) s1) is convergent by COMSEQ_2: 42;

      

      hence ( lim |.(s (#) s1).|) = |.( lim (s (#) s1)).| by Th27

      .= 0 by A1, COMPLEX1: 44, COMSEQ_2: 43;

    end;