toprns_1.miz



    begin

    definition

      let N be Nat;

      mode Real_Sequence of N is sequence of ( TOP-REAL N);

    end

    reserve N for Nat;

    reserve n,m,n1,n2 for Nat;

    reserve q,r,r1,r2 for Real;

    reserve x,y for set;

    reserve w,w1,w2,g,g1,g2 for Point of ( TOP-REAL N);

    reserve seq,seq1,seq2,seq3,seq9 for Real_Sequence of N;

    theorem :: TOPRNS_1:1

    

     Th1: for f be Function holds f is Real_Sequence of N iff (( dom f) = NAT & for n holds (f . n) is Point of ( TOP-REAL N))

    proof

      let f be Function;

      thus f is Real_Sequence of N implies (( dom f) = NAT & for n be Nat holds (f . n) is Point of ( TOP-REAL N)) by NORMSP_1: 12, ORDINAL1:def 12;

      assume that

       A1: ( dom f) = NAT and

       A2: for n holds (f . n) is Point of ( TOP-REAL N);

      for x holds x in NAT implies (f . x) is Point of ( TOP-REAL N) by A2;

      hence thesis by A1, NORMSP_1: 12;

    end;

    definition

      let N;

      let IT be Real_Sequence of N;

      :: TOPRNS_1:def1

      attr IT is non-zero means ( rng IT) c= ( NonZero ( TOP-REAL N));

    end

    theorem :: TOPRNS_1:2

    

     Th2: seq is non-zero iff for x st x in NAT holds (seq . x) <> ( 0. ( TOP-REAL N))

    proof

      thus seq is non-zero implies for x st x in NAT holds (seq . x) <> ( 0. ( TOP-REAL N))

      proof

        assume seq is non-zero;

        then

         A1: ( rng seq) c= ( NonZero ( TOP-REAL N));

        let x;

        assume x in NAT ;

        then x in ( dom seq) by Th1;

        then (seq . x) in ( rng seq) by FUNCT_1:def 3;

        then not (seq . x) in {( 0. ( TOP-REAL N))} by A1, XBOOLE_0:def 5;

        hence thesis by TARSKI:def 1;

      end;

      assume

       A2: for x st x in NAT holds (seq . x) <> ( 0. ( TOP-REAL N));

      now

        let y be object;

        assume y in ( rng seq);

        then

        consider x be object such that

         A3: x in ( dom seq) and

         A4: (seq . x) = y by FUNCT_1:def 3;

        

         A5: x in NAT by A3, NORMSP_1: 12;

        then y <> ( 0. ( TOP-REAL N)) by A2, A4;

        then

         A6: not y in {( 0. ( TOP-REAL N))} by TARSKI:def 1;

        y is Point of ( TOP-REAL N) by A4, A5, NORMSP_1: 12;

        hence y in ( NonZero ( TOP-REAL N)) by A6, XBOOLE_0:def 5;

      end;

      then ( rng seq) c= ( NonZero ( TOP-REAL N)) by TARSKI:def 3;

      hence thesis;

    end;

    theorem :: TOPRNS_1:3

    

     Th3: seq is non-zero iff for n holds (seq . n) <> ( 0. ( TOP-REAL N))

    proof

      thus seq is non-zero implies for n holds (seq . n) <> ( 0. ( TOP-REAL N)) by ORDINAL1:def 12, Th2;

      assume for n holds (seq . n) <> ( 0. ( TOP-REAL N));

      then for x holds x in NAT implies (seq . x) <> ( 0. ( TOP-REAL N));

      hence thesis by Th2;

    end;

    definition

      let N be Nat, seq1,seq2 be Real_Sequence of N;

      :: TOPRNS_1:def2

      func seq1 + seq2 -> Real_Sequence of N equals (seq1 + seq2);

      coherence

      proof

        

         A1: ( dom seq1) = NAT & ( dom seq2) = NAT by FUNCT_2:def 1;

        ( dom (seq1 + seq2)) = (( dom seq1) /\ ( dom seq2)) by VFUNCT_1:def 1;

        hence thesis by A1, FUNCT_2: 67;

      end;

    end

    definition

      let r be Real;

      let N be Nat, seq be Real_Sequence of N;

      :: TOPRNS_1:def3

      func r * seq -> Real_Sequence of N equals (r (#) seq);

      coherence

      proof

        

         A1: ( dom seq) = NAT by FUNCT_2:def 1;

        ( dom (r (#) seq)) = ( dom seq) by VFUNCT_1:def 4;

        hence thesis by A1, FUNCT_2: 67;

      end;

    end

    definition

      let N be Nat, seq be Real_Sequence of N;

      :: TOPRNS_1:def4

      func - seq -> Real_Sequence of N equals ( - seq);

      coherence

      proof

        

         A1: ( dom seq) = NAT by FUNCT_2:def 1;

        ( dom ( - seq)) = ( dom seq) by VFUNCT_1:def 5;

        hence thesis by A1, FUNCT_2: 67;

      end;

    end

    definition

      let N be Nat, seq1,seq2 be Real_Sequence of N;

      :: TOPRNS_1:def5

      func seq1 - seq2 -> Real_Sequence of N equals (seq1 + ( - seq2));

      correctness ;

    end

    definition

      let N be Nat, seq be Real_Sequence of N;

      :: TOPRNS_1:def6

      func |.seq.| -> Real_Sequence means

      : Def6: for n be Nat holds (it . n) = |.(seq . n).|;

      existence

      proof

        deffunc U( Nat) = |.(seq . $1).|;

        thus ex s be Real_Sequence st for n be Nat holds (s . n) = U(n) from SEQ_1:sch 1;

      end;

      uniqueness

      proof

        let seq8,seq9 be Real_Sequence such that

         A1: for n be Nat holds (seq8 . n) = |.(seq . n).| and

         A2: for n be Nat holds (seq9 . n) = |.(seq . n).|;

        let n be Element of NAT ;

        (seq9 . n) = |.(seq . n).| by A2;

        hence (seq8 . n) = (seq9 . n) by A1;

      end;

    end

    theorem :: TOPRNS_1:4

    

     Th4: for N,n be Nat, seq1,seq2 be Real_Sequence of N holds ((seq1 + seq2) . n) = ((seq1 . n) + (seq2 . n))

    proof

      let N,n be Nat, seq1,seq2 be Real_Sequence of N;

      reconsider m = n as Element of NAT by ORDINAL1:def 12;

      

       A1: ( dom (seq1 + seq2)) = NAT by FUNCT_2:def 1;

      

      thus ((seq1 + seq2) . n) = ((seq1 + seq2) /. m)

      .= ((seq1 /. m) + (seq2 /. m)) by A1, VFUNCT_1:def 1

      .= ((seq1 . n) + (seq2 . n));

    end;

    theorem :: TOPRNS_1:5

    

     Th5: for N,n be Nat, seq be Real_Sequence of N holds ((r * seq) . n) = (r * (seq . n))

    proof

      let N,n be Nat, seq be Real_Sequence of N;

      reconsider m = n as Element of NAT by ORDINAL1:def 12;

      

       A1: ( dom (r * seq)) = NAT by FUNCT_2:def 1;

      

      thus ((r * seq) . n) = ((r * seq) /. m)

      .= (r * (seq /. m)) by A1, VFUNCT_1:def 4

      .= (r * (seq . n));

    end;

    theorem :: TOPRNS_1:6

    

     Th6: for N,n be Nat, seq be Real_Sequence of N holds (( - seq) . n) = ( - (seq . n))

    proof

      let N,n be Nat, seq be Real_Sequence of N;

      reconsider m = n as Element of NAT by ORDINAL1:def 12;

      

       A1: ( dom ( - seq)) = NAT by FUNCT_2:def 1;

      

      thus (( - seq) . n) = (( - seq) /. m)

      .= ( - (seq /. m)) by A1, VFUNCT_1:def 5

      .= ( - (seq . n));

    end;

    theorem :: TOPRNS_1:7

    

     Th7: ( |.r.| * |.w.|) = |.(r * w).| by EUCLID: 11;

    theorem :: TOPRNS_1:8

     |.(r * seq).| = ( |.r.| (#) |.seq.|)

    proof

      let n be Element of NAT ;

      

      thus ( |.(r * seq).| . n) = |.((r * seq) . n).| by Def6

      .= |.(r * (seq . n)).| by Th5

      .= ( |.r.| * |.(seq . n).|) by Th7

      .= ( |.r.| * ( |.seq.| . n)) by Def6

      .= (( |.r.| (#) |.seq.|) . n) by SEQ_1: 9;

    end;

    theorem :: TOPRNS_1:9

    (seq1 + seq2) = (seq2 + seq1);

    theorem :: TOPRNS_1:10

    

     Th10: ((seq1 + seq2) + seq3) = (seq1 + (seq2 + seq3))

    proof

      let n be Element of NAT ;

      

      thus (((seq1 + seq2) + seq3) . n) = (((seq1 + seq2) . n) + (seq3 . n)) by Th4

      .= (((seq1 . n) + (seq2 . n)) + (seq3 . n)) by Th4

      .= ((seq1 . n) + ((seq2 . n) + (seq3 . n))) by RLVECT_1:def 3

      .= ((seq1 . n) + ((seq2 + seq3) . n)) by Th4

      .= ((seq1 + (seq2 + seq3)) . n) by Th4;

    end;

    theorem :: TOPRNS_1:11

    

     Th11: ( - seq) = (( - 1) * seq)

    proof

      let n be Element of NAT ;

      

      thus ((( - 1) * seq) . n) = (( - 1) * (seq . n)) by Th5

      .= ( - (seq . n)) by RLVECT_1: 16

      .= (( - seq) . n) by Th6;

    end;

    theorem :: TOPRNS_1:12

    

     Th12: (r * (seq1 + seq2)) = ((r * seq1) + (r * seq2))

    proof

      let n be Element of NAT ;

      

      thus ((r * (seq1 + seq2)) . n) = (r * ((seq1 + seq2) . n)) by Th5

      .= (r * ((seq1 . n) + (seq2 . n))) by Th4

      .= ((r * (seq1 . n)) + (r * (seq2 . n))) by RLVECT_1:def 5

      .= (((r * seq1) . n) + (r * (seq2 . n))) by Th5

      .= (((r * seq1) . n) + ((r * seq2) . n)) by Th5

      .= (((r * seq1) + (r * seq2)) . n) by Th4;

    end;

    theorem :: TOPRNS_1:13

    

     Th13: ((r * q) * seq) = (r * (q * seq))

    proof

      let n be Element of NAT ;

      

      thus (((r * q) * seq) . n) = ((r * q) * (seq . n)) by Th5

      .= (r * (q * (seq . n))) by RLVECT_1:def 7

      .= (r * ((q * seq) . n)) by Th5

      .= ((r * (q * seq)) . n) by Th5;

    end;

    theorem :: TOPRNS_1:14

    

     Th14: (r * (seq1 - seq2)) = ((r * seq1) - (r * seq2))

    proof

      

      thus (r * (seq1 - seq2)) = ((r * seq1) + (r * ( - seq2))) by Th12

      .= ((r * seq1) + (r * (( - 1) * seq2))) by Th11

      .= ((r * seq1) + ((( - 1) * r) * seq2)) by Th13

      .= ((r * seq1) + (( - 1) * (r * seq2))) by Th13

      .= ((r * seq1) - (r * seq2)) by Th11;

    end;

    theorem :: TOPRNS_1:15

    (seq1 - (seq2 + seq3)) = ((seq1 - seq2) - seq3)

    proof

      

      thus (seq1 - (seq2 + seq3)) = (seq1 + (( - 1) * (seq2 + seq3))) by Th11

      .= (seq1 + ((( - 1) * seq2) + (( - 1) * seq3))) by Th12

      .= (seq1 + (( - seq2) + (( - 1) * seq3))) by Th11

      .= (seq1 + (( - seq2) + ( - seq3))) by Th11

      .= ((seq1 - seq2) - seq3) by Th10;

    end;

    theorem :: TOPRNS_1:16

    

     Th16: (1 * seq) = seq

    proof

      let n be Element of NAT ;

      

      thus ((1 * seq) . n) = (1 * (seq . n)) by Th5

      .= (seq . n) by RLVECT_1:def 8;

    end;

    theorem :: TOPRNS_1:17

    

     Th17: ( - ( - seq)) = seq

    proof

      

      thus ( - ( - seq)) = (( - 1) * ( - seq)) by Th11

      .= (( - 1) * (( - 1) * seq)) by Th11

      .= ((( - 1) * ( - 1)) * seq) by Th13

      .= seq by Th16;

    end;

    theorem :: TOPRNS_1:18

    (seq1 - ( - seq2)) = (seq1 + seq2) by Th17;

    theorem :: TOPRNS_1:19

    (seq1 - (seq2 - seq3)) = ((seq1 - seq2) + seq3)

    proof

      

      thus (seq1 - (seq2 - seq3)) = (seq1 + (( - 1) * (seq2 - seq3))) by Th11

      .= (seq1 + ((( - 1) * seq2) - (( - 1) * seq3))) by Th14

      .= (seq1 + (( - seq2) - (( - 1) * seq3))) by Th11

      .= (seq1 + (( - seq2) - ( - seq3))) by Th11

      .= (seq1 + (( - seq2) + seq3)) by Th17

      .= ((seq1 - seq2) + seq3) by Th10;

    end;

    theorem :: TOPRNS_1:20

    (seq1 + (seq2 - seq3)) = ((seq1 + seq2) - seq3) by Th10;

    theorem :: TOPRNS_1:21

    

     Th21: r <> 0 & seq is non-zero implies (r * seq) is non-zero

    proof

      assume that

       A1: r <> 0 and

       A2: seq is non-zero and

       A3: not (r * seq) is non-zero;

      consider n1 such that

       A4: ((r * seq) . n1) = ( 0. ( TOP-REAL N)) by A3, Th3;

      

       A5: (seq . n1) <> ( 0. ( TOP-REAL N)) by A2, Th3;

      (r * (seq . n1)) = ( 0. ( TOP-REAL N)) by A4, Th5;

      hence contradiction by A1, A5, RLVECT_1: 11;

    end;

    theorem :: TOPRNS_1:22

    seq is non-zero implies ( - seq) is non-zero

    proof

      assume seq is non-zero;

      then (( - 1) * seq) is non-zero by Th21;

      hence thesis by Th11;

    end;

    theorem :: TOPRNS_1:23

    

     Th23: |.( 0. ( TOP-REAL N)).| = 0

    proof

      

      thus |.( 0. ( TOP-REAL N)).| = |.( 0* N).| by EUCLID: 70

      .= 0 by EUCLID: 7;

    end;

    theorem :: TOPRNS_1:24

    

     Th24: |.w.| = 0 implies w = ( 0. ( TOP-REAL N))

    proof

      reconsider s = w as Element of ( REAL N) by EUCLID: 22;

      assume |.w.| = 0 ;

      

      then s = ( 0* N) by EUCLID: 8

      .= ( 0. ( TOP-REAL N)) by EUCLID: 70;

      hence thesis;

    end;

    theorem :: TOPRNS_1:25

     |.w.| >= 0 ;

    theorem :: TOPRNS_1:26

     |.( - w).| = |.w.| by EUCLID: 71;

    theorem :: TOPRNS_1:27

    

     Th27: |.(w1 - w2).| = |.(w2 - w1).|

    proof

      

      thus |.(w1 - w2).| = |.( - (w1 - w2)).| by EUCLID: 71

      .= |.(w2 - w1).| by RLVECT_1: 33;

    end;

    

     Lm1: |.(w1 - w2).| = 0 implies w1 = w2

    proof

      assume |.(w1 - w2).| = 0 ;

      then (w1 - w2) = ( 0. ( TOP-REAL N)) by Th24;

      hence thesis by RLVECT_1: 21;

    end;

    

     Lm2: w1 = w2 implies |.(w1 - w2).| = 0

    proof

      assume w1 = w2;

      

      then |.(w1 - w2).| = |.( 0. ( TOP-REAL N)).| by RLVECT_1: 5

      .= 0 by Th23;

      hence thesis;

    end;

    theorem :: TOPRNS_1:28

     |.(w1 - w2).| = 0 iff w1 = w2 by Lm1, Lm2;

    theorem :: TOPRNS_1:29

    

     Th29: |.(w1 + w2).| <= ( |.w1.| + |.w2.|)

    proof

      reconsider s1 = w1, s2 = w2 as Element of ( REAL N) by EUCLID: 22;

      (w1 + w2) = (s1 + s2);

      hence thesis by EUCLID: 12;

    end;

    theorem :: TOPRNS_1:30

     |.(w1 - w2).| <= ( |.w1.| + |.w2.|)

    proof

      reconsider s1 = w1, s2 = w2 as Element of ( REAL N) by EUCLID: 22;

      (w1 - w2) = (s1 - s2);

      hence thesis by EUCLID: 13;

    end;

    theorem :: TOPRNS_1:31

    ( |.w1.| - |.w2.|) <= |.(w1 + w2).|

    proof

      reconsider s1 = w1, s2 = w2 as Element of ( REAL N) by EUCLID: 22;

      (w1 + w2) = (s1 + s2);

      hence thesis by EUCLID: 14;

    end;

    theorem :: TOPRNS_1:32

    

     Th32: ( |.w1.| - |.w2.|) <= |.(w1 - w2).|

    proof

      reconsider s1 = w1, s2 = w2 as Element of ( REAL N) by EUCLID: 22;

      (w1 - w2) = (s1 - s2);

      hence thesis by EUCLID: 15;

    end;

    theorem :: TOPRNS_1:33

    w1 <> w2 implies |.(w1 - w2).| > 0

    proof

      reconsider s1 = w1, s2 = w2 as Element of ( REAL N) by EUCLID: 22;

      (s1 - s2) = (w1 - w2);

      hence thesis by EUCLID: 17;

    end;

    theorem :: TOPRNS_1:34

     |.(w1 - w2).| <= ( |.(w1 - w).| + |.(w - w2).|)

    proof

      ( 0. ( TOP-REAL N)) = (w - w) by RLVECT_1: 5

      .= (( - w) + w);

      

      then |.(w1 - w2).| = |.((w1 + (( - w) + w)) - w2).| by RLVECT_1: 4

      .= |.(((w1 + ( - w)) + w) - w2).| by RLVECT_1:def 3

      .= |.(((w1 - w) + w) - w2).|

      .= |.((w1 - w) + (w - w2)).| by RLVECT_1:def 3;

      hence thesis by Th29;

    end;

    definition

      let N;

      let IT be Real_Sequence of N;

      :: TOPRNS_1:def7

      attr IT is bounded means ex r st for n holds |.(IT . n).| < r;

    end

    theorem :: TOPRNS_1:35

    

     Th35: 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: for n st X[n] holds X[(n + 1)]

      proof

        let n;

        given r1 such that

         A2: 0 < r1 and

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

         A4:

        now

          assume

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

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

          thus 0 < r;

          let m such that

           A6: m <= (n + 1);

           A7:

          now

            assume m <= n;

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

            then |.(seq . m).| < |.(seq . (n + 1)).| by A5, 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 A6, A7, NAT_1: 8;

        end;

        now

          assume

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

          take r = (r1 + 1);

          thus 0 < r by A2;

          let m such that

           A9: m <= (n + 1);

           A10:

          now

            assume m <= n;

            then

             A11: |.(seq . m).| < r1 by A3;

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

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

          end;

          now

            

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

            assume m = (n + 1);

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

          end;

          hence |.(seq . m).| < r by A9, A10, NAT_1: 8;

        end;

        hence thesis by A4;

      end;

      

       A13: X[ 0 ]

      proof

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

        thus 0 < r;

        let m;

        assume m <= 0 ;

        then 0 = m;

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

        hence thesis;

      end;

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

    end;

    definition

      let N;

      let IT be Real_Sequence of N;

      :: TOPRNS_1:def8

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

    end

    definition

      let N, seq;

      assume

       A1: seq is convergent;

      :: TOPRNS_1:def9

      func lim seq -> Point of ( TOP-REAL N) means

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

      existence by A1;

      uniqueness

      proof

        given g1, g2 such that

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

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

         A4: g1 <> g2;

         A5:

        now

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

          then (( 0. ( TOP-REAL N)) + g2) = ((g1 - g2) + g2) by Th24;

          

          then g2 = ((g1 - g2) + g2) by RLVECT_1: 4

          .= (g1 - (g2 - g2)) by RLVECT_1: 29

          .= (g1 - ( 0. ( TOP-REAL N))) by RLVECT_1: 5

          .= (g1 + ( - ( 0. ( TOP-REAL N))))

          .= (g1 + (( - 1) * ( 0. ( TOP-REAL N)))) by RLVECT_1: 16

          .= (g1 + ( 0. ( TOP-REAL N))) by RLVECT_1: 10

          .= g1 by RLVECT_1: 4;

          hence contradiction by A4;

        end;

        then

        consider n1 such that

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

        consider n2 such that

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

        

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

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

        then

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

         |.(g1 - g2).| = |.((g1 - g2) + ( 0. ( TOP-REAL N))).| by RLVECT_1: 4

        .= |.((g1 - g2) + (( - 1) * ( 0. ( TOP-REAL N)))).| by RLVECT_1: 10

        .= |.((g1 - g2) + ( - ( 0. ( TOP-REAL N)))).| by RLVECT_1: 16

        .= |.((g1 - g2) - ( 0. ( TOP-REAL N))).|

        .= |.((g1 - g2) - ((seq . (n1 + n2)) - (seq . (n1 + n2)))).| by RLVECT_1: 5

        .= |.(((g1 - g2) - (seq . (n1 + n2))) + (seq . (n1 + n2))).| by RLVECT_1: 29

        .= |.((g1 - ((seq . (n1 + n2)) + g2)) + (seq . (n1 + n2))).| by RLVECT_1: 27

        .= |.(((g1 - (seq . (n1 + n2))) - g2) + (seq . (n1 + n2))).| by RLVECT_1: 27

        .= |.((g1 - (seq . (n1 + n2))) - (g2 - (seq . (n1 + n2)))).| by RLVECT_1: 29

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

        .= |.((g1 - (seq . (n1 + n2))) + ((seq . (n1 + n2)) - g2)).| by RLVECT_1: 33

        .= |.(( - ((seq . (n1 + n2)) - g1)) + ((seq . (n1 + n2)) - g2)).| by RLVECT_1: 33;

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

        then

         A10: |.(g1 - g2).| <= ( |.((seq . (n1 + n2)) - g1).| + |.((seq . (n1 + n2)) - g2).|) by EUCLID: 71;

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

        hence contradiction by A9, A10, XXREAL_0: 2;

      end;

    end

    theorem :: TOPRNS_1:36

    

     Th36: 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 r st 0 < r holds ex n st for m st n <= m holds |.((seq . m) - g1).| < r by A1;

      consider g2 such that

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

      take g = (g1 + g2);

      let r;

      assume

       A5: 0 < r;

      then

      consider n1 such that

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

      consider n2 such that

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

      take k = (n1 + n2);

      let m;

      assume

       A8: k <= m;

      n2 <= k by NAT_1: 12;

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

      then

       A9: |.((seq9 . m) - g2).| < (r / 2) by A7;

      

       A10: |.(((seq + seq9) . m) - g).| = |.(((seq . m) + (seq9 . m)) - (g1 + g2)).| by Th4

      .= |.((seq . m) + ((seq9 . m) - (g1 + g2))).| by RLVECT_1:def 3

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

      .= |.(((seq . m) + ( - (g1 + g2))) + (seq9 . m)).| by RLVECT_1:def 3

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

      .= |.((((seq . m) - g1) - g2) + (seq9 . m)).| by RLVECT_1: 27

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

      .= |.(((seq . m) - g1) + ((seq9 . m) + ( - g2))).| by RLVECT_1:def 3

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

      

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

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

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

      then |.((seq . m) - g1).| < (r / 2) by A6;

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

      hence thesis by A10, A11, XXREAL_0: 2;

    end;

    theorem :: TOPRNS_1:37

    

     Th37: 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;

       A3:

      now

        let r;

        assume 0 < r;

        then

         A4: 0 < (r / 2) by XREAL_1: 215;

        then

        consider n1 such that

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

        consider n2 such that

         A6: for m st n2 <= m holds |.((seq9 . m) - ( lim seq9)).| < (r / 2) by A2, A4, Def9;

        take k = (n1 + n2);

        let m such that

         A7: k <= m;

        n2 <= k by NAT_1: 12;

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

        then

         A8: |.((seq9 . m) - ( lim seq9)).| < (r / 2) by A6;

        

         A9: |.(((seq + seq9) . m) - (( lim seq) + ( lim seq9))).| = |.((((seq + seq9) . m) - ( lim seq)) - ( lim seq9)).| by RLVECT_1: 27

        .= |.((((seq . m) + (seq9 . m)) - ( lim seq)) - ( lim seq9)).| by Th4

        .= |.(((seq . m) + ((seq9 . m) - ( lim seq))) - ( lim seq9)).| by RLVECT_1:def 3

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

        .= |.((((seq . m) + ( - ( lim seq))) + (seq9 . m)) - ( lim seq9)).| by RLVECT_1:def 3

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

        .= |.(((seq . m) - ( lim seq)) + ((seq9 . m) - ( lim seq9))).| by RLVECT_1:def 3;

        

         A10: |.(((seq . m) - ( lim seq)) + ((seq9 . m) - ( lim seq9))).| <= ( |.((seq . m) - ( lim seq)).| + |.((seq9 . m) - ( lim seq9)).|) by Th29;

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

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

        then |.((seq . m) - ( lim seq)).| < (r / 2) by A5;

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

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

      end;

      (seq + seq9) is convergent by A1, A2, Th36;

      hence thesis by A3, Def9;

    end;

    theorem :: TOPRNS_1:38

    

     Th38: seq is convergent implies (r * seq) is convergent

    proof

      assume seq is convergent;

      then

      consider g1 such that

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

      set g = (r * g1);

       A2:

      now

        

         A3: ( 0 / |.r.|) = 0 ;

        assume

         A4: r <> 0 ;

        then

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

        let q;

        assume 0 < q;

        then

        consider n1 such that

         A6: for m st n1 <= m holds |.((seq . m) - g1).| < (q / |.r.|) by A1, A5, A3, XREAL_1: 74;

        take k = n1;

        let m;

        assume k <= m;

        then

         A7: |.((seq . m) - g1).| < (q / |.r.|) by A6;

        

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

        

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

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

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

        .= q;

         |.(((r * seq) . m) - g).| = |.((r * (seq . m)) - (r * g1)).| by Th5

        .= |.(r * ((seq . m) - g1)).| by RLVECT_1: 34

        .= ( |.r.| * |.((seq . m) - g1).|) by Th7;

        hence |.(((r * seq) . m) - g).| < q by A5, A7, A9, XREAL_1: 68;

      end;

      now

        assume

         A10: r = 0 ;

        let q such that

         A11: 0 < q;

        reconsider k = 0 as Nat;

        take k;

        let m such that k <= m;

         |.(((r * seq) . m) - g).| = |.((( 0 * seq) . m) - ( 0. ( TOP-REAL N))).| by A10, RLVECT_1: 10

        .= |.(( 0. ( TOP-REAL N)) - (( 0 * seq) . m)).| by Th27

        .= |.(( 0. ( TOP-REAL N)) + ( - (( 0 * seq) . m))).|

        .= |.( - (( 0 * seq) . m)).| by RLVECT_1: 4

        .= |.(( 0 * seq) . m).| by EUCLID: 71

        .= |.( 0 * (seq . m)).| by Th5

        .= |.( 0. ( TOP-REAL N)).| by RLVECT_1: 10

        .= 0 by Th23;

        hence |.(((r * seq) . m) - g).| < q by A11;

      end;

      hence thesis by A2;

    end;

    theorem :: TOPRNS_1:39

    

     Th39: seq is convergent implies ( lim (r * seq)) = (r * ( lim seq))

    proof

       A1:

      now

        assume

         A2: r = 0 ;

        let q such that

         A3: 0 < q;

        reconsider k = 0 as Nat;

        take k;

        let m such that k <= m;

        (r * ( lim seq)) = ( 0. ( TOP-REAL N)) by A2, RLVECT_1: 10;

        

        then |.(((r * seq) . m) - (r * ( lim seq))).| = |.(( 0 * (seq . m)) - ( 0. ( TOP-REAL N))).| by A2, Th5

        .= |.(( 0. ( TOP-REAL N)) - ( 0 * (seq . m))).| by Th27

        .= |.(( 0. ( TOP-REAL N)) + ( - ( 0 * (seq . m)))).|

        .= |.( - ( 0 * (seq . m))).| by RLVECT_1: 4

        .= |.( 0 * (seq . m)).| by EUCLID: 71

        .= |.( 0. ( TOP-REAL N)).| by RLVECT_1: 10

        .= 0 by Th23;

        hence |.(((r * seq) . m) - (r * ( lim seq))).| < q by A3;

      end;

      assume

       A4: seq is convergent;

       A5:

      now

        

         A6: ( 0 / |.r.|) = 0 ;

        assume

         A7: r <> 0 ;

        then

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

        let q;

        assume 0 < q;

        then 0 < (q / |.r.|) by A8, A6, XREAL_1: 74;

        then

        consider n1 such that

         A9: for m st n1 <= m holds |.((seq . m) - ( lim seq)).| < (q / |.r.|) by A4, Def9;

        take k = n1;

        let m;

        assume k <= m;

        then

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

        

         A11: 0 <> |.r.| by A7, COMPLEX1: 47;

        

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

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

        .= (1 * q) by A11, XCMPLX_0:def 7

        .= q;

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

        .= |.(r * ((seq . m) - ( lim seq))).| by RLVECT_1: 34

        .= ( |.r.| * |.((seq . m) - ( lim seq)).|) by Th7;

        hence |.(((r * seq) . m) - (r * ( lim seq))).| < q by A8, A10, A12, XREAL_1: 68;

      end;

      (r * seq) is convergent by A4, Th38;

      hence thesis by A1, A5, Def9;

    end;

    theorem :: TOPRNS_1:40

    

     Th40: seq is convergent implies ( - seq) is convergent

    proof

      assume seq is convergent;

      then (( - 1) * seq) is convergent by Th38;

      hence thesis by Th11;

    end;

    theorem :: TOPRNS_1:41

    

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

    proof

      assume seq is convergent;

      

      then ( lim (( - 1) * seq)) = (( - 1) * ( lim seq)) by Th39

      .= ( - (1 * ( lim seq))) by RLVECT_1: 79

      .= ( - ( lim seq)) by RLVECT_1:def 8;

      hence thesis by Th11;

    end;

    theorem :: TOPRNS_1:42

    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, Th40;

      hence thesis by A1, Th36;

    end;

    theorem :: TOPRNS_1:43

    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;

      ( - seq9) is convergent by A2, Th40;

      

      hence ( lim (seq - seq9)) = (( lim seq) + ( lim ( - seq9))) by A1, Th37

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

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

    end;

    theorem :: TOPRNS_1:44

    seq is convergent implies seq is bounded

    proof

      assume seq is convergent;

      then

      consider g such that

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

      consider n1 such that

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

       A3:

      now

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

        thus 0 < r;

        let m;

        

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

        assume n1 <= m;

        then

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

        ( |.(seq . m).| - |.g.|) <= |.((seq . m) - g).| by Th32;

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

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

      end;

      now

        consider r2 such that

         A6: 0 < r2 and

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

        consider r1 such that

         A8: 0 < r1 and

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

        take r = (r1 + r2);

        thus 0 < r by A8, A6;

        let m;

        

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

         A11:

        now

          assume m <= n1;

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

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

        end;

        

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

        now

          assume n1 <= m;

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

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

        end;

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

      end;

      hence thesis;

    end;

    theorem :: TOPRNS_1:45

    seq is convergent implies (( lim seq) <> ( 0. ( TOP-REAL N)) 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. ( TOP-REAL N));

       0 <> |.( lim seq).| by A2, Th24;

      then 0 < ( |.( lim seq).| / 2) by XREAL_1: 215;

      then

      consider n1 such that

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

      take n = n1;

      let m;

      assume n <= m;

      then

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

      ( |.( lim seq).| - |.(seq . m).|) <= |.(( lim seq) - (seq . m)).| & |.(( lim seq) - (seq . m)).| = |.((seq . m) - ( lim seq)).| by Th27, Th32;

      then

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

      (( |.( 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 A5, XREAL_1: 6;

    end;