series_1.miz



    begin

    reserve n,m,k for Nat;

    reserve a,p,r for Real;

    reserve s,s1,s2,s3 for Real_Sequence;

    theorem :: SERIES_1:1

    

     Th1: 0 < a & a < 1 & (for n holds (s . n) = (a to_power (n + 1))) implies s is convergent & ( lim s) = 0

    proof

      assume that

       A1: 0 < a and

       A2: a < 1 and

       A3: for n holds (s . n) = (a to_power (n + 1));

      set r = ((1 / a) - 1);

      (1 / a) > (1 / 1) by A1, A2, XREAL_1: 88;

      then

       A4: r > 0 by XREAL_1: 50;

      

       A5: for p be Real st 0 < p holds ex m st for n st m <= n holds |.((s . n) - 0 ).| < p

      proof

        let p be Real;

        

         A6: (1 / (p * r)) <= ( [\(1 / (p * r))/] + 1) by INT_1: 29;

        assume

         A7: 0 < p;

        then (p * r) > 0 by A4;

        then (1 / (p * r)) > 0 ;

        then 0 < ( [\(1 / (p * r))/] + 1) by A6;

        then [\(1 / (p * r))/] is Element of NAT by INT_1: 3, INT_1: 7;

        then

        consider m such that

         A8: m = [\(1 / (p * r))/];

        take m;

        

         A9: (1 / (p * r)) = ((1 / p) / r) by XCMPLX_1: 78;

        now

          

           A10: [\(1 / (p * r))/] > ((1 / (p * r)) - 1) by INT_1:def 6;

          let n;

          assume m <= n;

          then n > ((1 / (p * r)) - 1) by A8, A10, XXREAL_0: 2;

          then (n + 1) > ((1 / p) / r) by A9, XREAL_1: 19;

          then

           A11: ((n + 1) * r) > (1 / p) by A4, XREAL_1: 77;

          ( 0 + ((n + 1) * r)) < (1 + ((n + 1) * r)) by XREAL_1: 6;

          then

           A12: (1 / p) < (1 + ((n + 1) * r)) by A11, XXREAL_0: 2;

          

           A13: ((1 + r) to_power (n + 1)) = ((1 to_power (n + 1)) / (a to_power (n + 1))) by A1, POWER: 31

          .= (1 / (a to_power (n + 1)));

          (a to_power (n + 1)) > 0 by A1, POWER: 34;

          then

           A14: |.(a to_power (n + 1)).| = (a to_power (n + 1)) by ABSVALUE:def 1;

          (1 + ((n + 1) * r)) <= ((1 + r) to_power (n + 1)) by A4, POWER: 49;

          then (1 / p) < (1 / (a to_power (n + 1))) by A13, A12, XXREAL_0: 2;

          then |.(a to_power (n + 1)).| < p by A7, A14, XREAL_1: 91;

          hence |.((s . n) - 0 ).| < p by A3;

        end;

        hence thesis;

      end;

      hence s is convergent by SEQ_2:def 6;

      hence thesis by A5, SEQ_2:def 7;

    end;

    theorem :: SERIES_1:2

    

     Th2: for n be Nat holds ( |.a.| to_power n) = |.(a to_power n).|

    proof

      let n be Nat;

      per cases ;

        suppose

         A1: a <> 0 ;

        then

         A2: |.a.| > 0 by COMPLEX1: 47;

        now

          per cases by A1;

            suppose a > 0 ;

            then (a to_power n) = ( |.a.| to_power n) & (a to_power n) > 0 by ABSVALUE:def 1, POWER: 34;

            hence thesis by ABSVALUE:def 1;

          end;

            suppose

             A3: a < 0 ;

            reconsider m = n as Integer;

            now

              per cases ;

                suppose

                 A4: m is even;

                

                 A5: ( |.a.| to_power n) > 0 by A2, POWER: 34;

                ( |.a.| to_power n) = (( - a) to_power m) by A3, ABSVALUE:def 1

                .= (a to_power m) by A4, POWER: 47;

                hence thesis by A5, ABSVALUE:def 1;

              end;

                suppose

                 A6: m is odd;

                

                 A7: ( |.a.| to_power n) > 0 by A2, POWER: 34;

                ( |.a.| to_power n) = (( - a) to_power m) by A3, ABSVALUE:def 1

                .= ( - (a to_power m)) by A6, POWER: 48;

                

                hence ( |.a.| to_power n) = |.( - (a to_power n)).| by A7, ABSVALUE:def 1

                .= |.(a to_power n).| by COMPLEX1: 52;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

        suppose

         A8: a = 0 ;

        per cases ;

          suppose n = 0 ;

          then (a to_power n) = 1 by NEWTON: 4;

          hence thesis by A8, COMPLEX1: 44, COMPLEX1: 48;

        end;

          suppose n > 0 ;

          then ( |.a.| to_power n) = 0 by A8, COMPLEX1: 44, POWER:def 2;

          hence thesis by A8, COMPLEX1: 44;

        end;

      end;

    end;

    theorem :: SERIES_1:3

    

     Th3: |.a.| < 1 & (for n holds (s . n) = (a to_power (n + 1))) implies s is convergent & ( lim s) = 0

    proof

      assume that

       A1: |.a.| < 1 and

       A2: for n holds (s . n) = (a to_power (n + 1));

      now

        per cases ;

          suppose |.a.| = 0 ;

          then

           A3: a = 0 by ABSVALUE: 2;

          now

            let n be Nat;

            n in NAT & (a to_power (n + 1)) = 0 by A3, ORDINAL1:def 12, POWER:def 2;

            hence (s . n) = ( In ( 0 , REAL )) by A2;

          end;

          then s is constant & (s . 0 ) = ( In ( 0 , REAL ));

          hence thesis by SEQ_4: 26;

        end;

          suppose

           A4: not |.a.| = 0 ;

          deffunc U( Nat) = ( |.a.| to_power ($1 + 1));

          consider s1 such that

           A5: for n holds (s1 . n) = U(n) from SEQ_1:sch 1;

           A6:

          now

            let n;

            

            thus (s1 . n) = ( |.a.| to_power (n + 1)) by A5

            .= |.(a to_power (n + 1)).| by Th2

            .= |.(s . n).| by A2;

          end;

          

           A7: |.a.| > 0 by A4, COMPLEX1: 46;

          then ( lim s1) = 0 by A1, A5, Th1;

          then

           A8: ( lim ( abs s)) = 0 by A6, SEQ_1: 12;

          s1 is convergent by A1, A7, A5, Th1;

          then ( abs s) is convergent by A6, SEQ_1: 12;

          hence thesis by A8, SEQ_4: 15;

        end;

      end;

      hence thesis;

    end;

    definition

      let X be non empty add-closed complex-membered set;

      let s1,s2 be sequence of X;

      :: original: +

      redefine

      func s1 + s2 -> sequence of X ;

      coherence

      proof

        

         A1: ( dom (s1 + s2)) = (( dom s1) /\ ( dom s2)) by VALUED_1:def 1

        .= ( NAT /\ ( dom s2)) by FUNCT_2:def 1

        .= ( NAT /\ NAT ) by FUNCT_2:def 1;

        now

          let x be object such that

           A2: x in NAT ;

          

           A3: (s1 . x) in X & (s2 . x) in X by A2, FUNCT_2: 5;

          ((s1 + s2) . x) = ((s1 . x) + (s2 . x)) by A1, A2, VALUED_1:def 1;

          hence ((s1 + s2) . x) in X by A3, MEMBERED:def 25;

        end;

        hence thesis by A1, FUNCT_2: 3;

      end;

    end

    definition

      let s be complex-valued ManySortedSet of NAT ;

      :: SERIES_1:def1

      func Partial_Sums (s) -> complex-valued ManySortedSet of NAT means

      : Def1: (it . 0 ) = (s . 0 ) & for n holds (it . (n + 1)) = ((it . n) + (s . (n + 1)));

      existence

      proof

        set X = COMPLEX ;

        

         A1: ( dom s) = NAT by PARTFUN1:def 2;

        ( rng s) c= X by VALUED_0:def 1;

        then

        reconsider ss = s as sequence of X by A1, RELSET_1: 4;

        defpred P[ Nat, Element of X, set] means $3 = ($2 + (ss . ($1 + 1)));

        

         A2: for n be Nat holds for x be Element of X holds ex y be Element of X st P[n, x, y]

        proof

          let n be Nat, x be Element of X;

          reconsider y = (x + (ss . (n + 1))) as Element of COMPLEX by XCMPLX_0:def 2;

          take y;

          thus thesis;

        end;

        consider f be sequence of X such that

         A3: (f . 0 ) = (ss . 0 ) and

         A4: for n be Nat holds P[n, (f . n), (f . (n + 1))] from RECDEF_1:sch 2( A2);

        take f;

        thus (f . 0 ) = (s . 0 ) by A3;

        let n;

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

         P[n, (f . n), (f . (n + 1))] by A4;

        hence thesis;

      end;

      uniqueness

      proof

        let s1,s2 be complex-valued ManySortedSet of NAT ;

        assume that

         A5: (s1 . 0 ) = (s . 0 ) and

         A6: for n holds (s1 . (n + 1)) = ((s1 . n) + (s . (n + 1))) and

         A7: (s2 . 0 ) = (s . 0 ) and

         A8: for n holds (s2 . (n + 1)) = ((s2 . n) + (s . (n + 1)));

        defpred X[ Nat] means (s1 . $1) = (s2 . $1);

        

         A9: for k be Nat st X[k] holds X[(k + 1)]

        proof

          let k be Nat;

          assume (s1 . k) = (s2 . k);

          

          hence (s1 . (k + 1)) = ((s2 . k) + (s . (k + 1))) by A6

          .= (s2 . (k + 1)) by A8;

        end;

        

         A10: X[ 0 ] by A5, A7;

        for n be Nat holds X[n] from NAT_1:sch 2( A10, A9);

        hence thesis;

      end;

    end

    registration

      let s be real-valued ManySortedSet of NAT ;

      cluster ( Partial_Sums s) -> real-valued;

      coherence

      proof

        set f = ( Partial_Sums s);

        let x be object;

        assume x in ( dom f);

        then

        reconsider n = x as Element of NAT ;

        defpred P[ Nat] means (f . $1) is real;

        (f . 0 ) = (s . 0 ) by Def1;

        then

         A1: P[ 0 ];

        

         A2: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          assume

           A3: P[k];

          reconsider k as Element of NAT by ORDINAL1:def 12;

          (f . (k + 1)) = ((f . k) + (s . (k + 1))) by Def1;

          hence thesis by A3;

        end;

        for k be Nat holds P[k] from NAT_1:sch 2( A1, A2);

        then (f . n) is real;

        hence thesis;

      end;

    end

    definition

      let s be Real_Sequence;

      :: original: Partial_Sums

      redefine

      func Partial_Sums s -> Real_Sequence ;

      coherence

      proof

        

         A1: ( dom ( Partial_Sums s)) = NAT by PARTFUN1:def 2;

        ( rng ( Partial_Sums s)) c= REAL by VALUED_0:def 3;

        then ( Partial_Sums s) is Relation of NAT , REAL by A1, RELSET_1: 4;

        hence ( Partial_Sums s) is Real_Sequence;

      end;

    end

    definition

      let s;

      :: SERIES_1:def2

      attr s is summable means

      : Def2: ( Partial_Sums s) is convergent;

      :: SERIES_1:def3

      func Sum (s) -> Real equals ( lim ( Partial_Sums s));

      correctness ;

    end

    theorem :: SERIES_1:4

    

     Th4: s is summable implies s is convergent & ( lim s) = 0

    proof

      assume s is summable;

      then

       A1: ( Partial_Sums s) is convergent;

      now

        let n;

        (( Partial_Sums s) . (n + 1)) = ((( Partial_Sums s) . n) + (s . (n + 1))) by Def1;

        then (( Partial_Sums s) . (n + 1)) = ((( Partial_Sums s) . n) + ((s ^\ 1) . n)) by NAT_1:def 3;

        hence ((( Partial_Sums s) ^\ 1) . n) = ((( Partial_Sums s) . n) + ((s ^\ 1) . n)) by NAT_1:def 3;

      end;

      then

       A2: (( Partial_Sums s) ^\ 1) = (( Partial_Sums s) + (s ^\ 1)) by SEQ_1: 7;

      now

        let n be Element of NAT ;

        

        thus (((s ^\ 1) + (( Partial_Sums s) - ( Partial_Sums s))) . n) = (((s ^\ 1) . n) + ((( Partial_Sums s) + ( - ( Partial_Sums s))) . n)) by SEQ_1: 7

        .= (((s ^\ 1) . n) + ((( Partial_Sums s) . n) + (( - ( Partial_Sums s)) . n))) by SEQ_1: 7

        .= (((s ^\ 1) . n) + ((( Partial_Sums s) . n) + ( - (( Partial_Sums s) . n)))) by SEQ_1: 10

        .= ((s ^\ 1) . n);

      end;

      then ((s ^\ 1) + (( Partial_Sums s) - ( Partial_Sums s))) = (s ^\ 1);

      then

       A3: (s ^\ 1) = ((( Partial_Sums s) ^\ 1) - ( Partial_Sums s)) by A2, SEQ_1: 31;

      then

       A4: (s ^\ 1) qua Real_Sequence is convergent by A1;

      hence s is convergent by SEQ_4: 21;

      ( lim (( Partial_Sums s) ^\ 1)) = ( lim ( Partial_Sums s)) by A1, SEQ_4: 20;

      

      then ( lim ((( Partial_Sums s) ^\ 1) - ( Partial_Sums s))) = (( lim ( Partial_Sums s)) - ( lim ( Partial_Sums s))) by A1, SEQ_2: 12

      .= 0 ;

      hence thesis by A3, A4, SEQ_4: 22;

    end;

    

     Lm1: for seq,seq1,seq2 be complex-valued ManySortedSet of NAT holds seq = (seq1 + seq2) iff for n holds (seq . n) = ((seq1 . n) + (seq2 . n))

    proof

      let seq,seq1,seq2 be complex-valued ManySortedSet of NAT ;

      thus seq = (seq1 + seq2) implies for n holds (seq . n) = ((seq1 . n) + (seq2 . n))

      proof

        assume

         A1: seq = (seq1 + seq2);

        let n;

        

         A2: n in NAT by ORDINAL1:def 12;

        ( dom seq) = NAT by PARTFUN1:def 2;

        hence thesis by A1, VALUED_1:def 1, A2;

      end;

      assume for n holds (seq . n) = ((seq1 . n) + (seq2 . n));

      then

       A3: for n be object st n in ( dom seq) holds (seq . n) = ((seq1 . n) + (seq2 . n));

      ( dom seq) = ( NAT /\ NAT ) by PARTFUN1:def 2

      .= ( NAT /\ ( dom seq2)) by PARTFUN1:def 2

      .= (( dom seq1) /\ ( dom seq2)) by PARTFUN1:def 2;

      hence thesis by A3, VALUED_1:def 1;

    end;

    theorem :: SERIES_1:5

    

     Th5: for X be non empty add-closed complex-membered set holds for s1,s2 be sequence of X holds (( Partial_Sums s1) + ( Partial_Sums s2)) = ( Partial_Sums (s1 + s2))

    proof

      let X be non empty add-closed complex-membered set;

      let s1,s2 be sequence of X;

       A1:

      now

        let n;

        

        thus ((( Partial_Sums s1) + ( Partial_Sums s2)) . (n + 1)) = ((( Partial_Sums s1) . (n + 1)) + (( Partial_Sums s2) . (n + 1))) by Lm1

        .= (((( Partial_Sums s1) . n) + (s1 . (n + 1))) + (( Partial_Sums s2) . (n + 1))) by Def1

        .= (((( Partial_Sums s1) . n) + (s1 . (n + 1))) + ((s2 . (n + 1)) + (( Partial_Sums s2) . n))) by Def1

        .= (((( Partial_Sums s1) . n) + ((s1 . (n + 1)) + (s2 . (n + 1)))) + (( Partial_Sums s2) . n))

        .= (((( Partial_Sums s1) . n) + ((s1 + s2) . (n + 1))) + (( Partial_Sums s2) . n)) by Lm1

        .= (((( Partial_Sums s1) . n) + (( Partial_Sums s2) . n)) + ((s1 + s2) . (n + 1)))

        .= (((( Partial_Sums s1) + ( Partial_Sums s2)) . n) + ((s1 + s2) . (n + 1))) by Lm1;

      end;

      ((( Partial_Sums s1) + ( Partial_Sums s2)) . 0 ) = ((( Partial_Sums s1) . 0 ) + (( Partial_Sums s2) . 0 )) by Lm1

      .= ((s1 . 0 ) + (( Partial_Sums s2) . 0 )) by Def1

      .= ((s1 . 0 ) + (s2 . 0 )) by Def1

      .= ((s1 + s2) . 0 ) by Lm1;

      hence thesis by A1, Def1;

    end;

    theorem :: SERIES_1:6

    

     Th6: (( Partial_Sums s1) - ( Partial_Sums s2)) = ( Partial_Sums (s1 - s2))

    proof

       A1:

      now

        let n;

        

        thus ((( Partial_Sums s1) - ( Partial_Sums s2)) . (n + 1)) = ((( Partial_Sums s1) . (n + 1)) - (( Partial_Sums s2) . (n + 1))) by RFUNCT_2: 1

        .= (((( Partial_Sums s1) . n) + (s1 . (n + 1))) - (( Partial_Sums s2) . (n + 1))) by Def1

        .= (((( Partial_Sums s1) . n) + (s1 . (n + 1))) - ((s2 . (n + 1)) + (( Partial_Sums s2) . n))) by Def1

        .= (((( Partial_Sums s1) . n) + ((s1 . (n + 1)) - (s2 . (n + 1)))) - (( Partial_Sums s2) . n))

        .= ((((s1 - s2) . (n + 1)) + (( Partial_Sums s1) . n)) - (( Partial_Sums s2) . n)) by RFUNCT_2: 1

        .= (((s1 - s2) . (n + 1)) + ((( Partial_Sums s1) . n) - (( Partial_Sums s2) . n)))

        .= (((( Partial_Sums s1) - ( Partial_Sums s2)) . n) + ((s1 - s2) . (n + 1))) by RFUNCT_2: 1;

      end;

      ((( Partial_Sums s1) - ( Partial_Sums s2)) . 0 ) = ((( Partial_Sums s1) . 0 ) - (( Partial_Sums s2) . 0 )) by RFUNCT_2: 1

      .= ((s1 . 0 ) - (( Partial_Sums s2) . 0 )) by Def1

      .= ((s1 . 0 ) - (s2 . 0 )) by Def1

      .= ((s1 - s2) . 0 ) by RFUNCT_2: 1;

      hence thesis by A1, Def1;

    end;

    theorem :: SERIES_1:7

    s1 is summable & s2 is summable implies (s1 + s2) is summable & ( Sum (s1 + s2)) = (( Sum s1) + ( Sum s2))

    proof

      assume s1 is summable & s2 is summable;

      then

       A1: ( Partial_Sums s1) is convergent & ( Partial_Sums s2) is convergent;

      then (( Partial_Sums s1) + ( Partial_Sums s2)) is convergent;

      then ( Partial_Sums (s1 + s2)) is convergent by Th5;

      hence (s1 + s2) is summable;

      

      thus ( Sum (s1 + s2)) = ( lim (( Partial_Sums s1) + ( Partial_Sums s2))) by Th5

      .= (( Sum s1) + ( Sum s2)) by A1, SEQ_2: 6;

    end;

    theorem :: SERIES_1:8

    s1 is summable & s2 is summable implies (s1 - s2) is summable & ( Sum (s1 - s2)) = (( Sum s1) - ( Sum s2))

    proof

      assume s1 is summable & s2 is summable;

      then

       A1: ( Partial_Sums s1) is convergent & ( Partial_Sums s2) is convergent;

      then (( Partial_Sums s1) - ( Partial_Sums s2)) is convergent;

      then ( Partial_Sums (s1 - s2)) is convergent by Th6;

      hence (s1 - s2) is summable;

      

      thus ( Sum (s1 - s2)) = ( lim (( Partial_Sums s1) - ( Partial_Sums s2))) by Th6

      .= (( Sum s1) - ( Sum s2)) by A1, SEQ_2: 12;

    end;

    theorem :: SERIES_1:9

    

     Th9: ( Partial_Sums (r (#) s)) = (r (#) ( Partial_Sums s))

    proof

       A1:

      now

        let n;

        

        thus ((r (#) ( Partial_Sums s)) . (n + 1)) = (r * (( Partial_Sums s) . (n + 1))) by SEQ_1: 9

        .= (r * ((( Partial_Sums s) . n) + (s . (n + 1)))) by Def1

        .= ((r * (( Partial_Sums s) . n)) + (r * (s . (n + 1))))

        .= (((r (#) ( Partial_Sums s)) . n) + (r * (s . (n + 1)))) by SEQ_1: 9

        .= (((r (#) ( Partial_Sums s)) . n) + ((r (#) s) . (n + 1))) by SEQ_1: 9;

      end;

      ((r (#) ( Partial_Sums s)) . 0 ) = (r * (( Partial_Sums s) . 0 )) by SEQ_1: 9

      .= (r * (s . 0 )) by Def1

      .= ((r (#) s) . 0 ) by SEQ_1: 9;

      hence thesis by A1, Def1;

    end;

    theorem :: SERIES_1:10

    

     Th10: s is summable implies (r (#) s) is summable & ( Sum (r (#) s)) = (r * ( Sum s))

    proof

      assume s is summable;

      then

       A1: ( Partial_Sums s) is convergent;

      then (r (#) ( Partial_Sums s)) is convergent;

      then ( Partial_Sums (r (#) s)) is convergent by Th9;

      hence (r (#) s) is summable;

      

      thus ( Sum (r (#) s)) = ( lim (r (#) ( Partial_Sums s))) by Th9

      .= (r * ( Sum s)) by A1, SEQ_2: 8;

    end;

    theorem :: SERIES_1:11

    

     Th11: for s, s1 st for n holds (s1 . n) = (s . 0 ) holds ( Partial_Sums (s ^\ 1)) = ((( Partial_Sums s) ^\ 1) - s1)

    proof

      let s, s1;

      assume

       A1: for n holds (s1 . n) = (s . 0 );

       A2:

      now

        let k;

        

        thus (((( Partial_Sums s) ^\ 1) - s1) . (k + 1)) = (((( Partial_Sums s) ^\ 1) . (k + 1)) - (s1 . (k + 1))) by RFUNCT_2: 1

        .= (((( Partial_Sums s) ^\ 1) . (k + 1)) - (s . 0 )) by A1

        .= ((( Partial_Sums s) . ((k + 1) + 1)) - (s . 0 )) by NAT_1:def 3

        .= (((s . ((k + 1) + 1)) + (( Partial_Sums s) . (k + 1))) - (s . 0 )) by Def1

        .= (((s . ((k + 1) + 1)) + (( Partial_Sums s) . (k + 1))) - (s1 . k)) by A1

        .= ((s . ((k + 1) + 1)) + ((( Partial_Sums s) . (k + 1)) - (s1 . k)))

        .= ((s . ((k + 1) + 1)) + (((( Partial_Sums s) ^\ 1) . k) - (s1 . k))) by NAT_1:def 3

        .= ((s . ((k + 1) + 1)) + (((( Partial_Sums s) ^\ 1) - s1) . k)) by RFUNCT_2: 1

        .= ((((( Partial_Sums s) ^\ 1) - s1) . k) + ((s ^\ 1) . (k + 1))) by NAT_1:def 3;

      end;

      (((( Partial_Sums s) ^\ 1) - s1) . 0 ) = (((( Partial_Sums s) ^\ 1) . 0 ) - (s1 . 0 )) by RFUNCT_2: 1

      .= (((( Partial_Sums s) ^\ 1) . 0 ) - (s . 0 )) by A1

      .= ((( Partial_Sums s) . ( 0 + 1)) - (s . 0 )) by NAT_1:def 3

      .= (((( Partial_Sums s) . 0 ) + (s . ( 0 + 1))) - (s . 0 )) by Def1

      .= (((s . ( 0 + 1)) + (s . 0 )) - (s . 0 )) by Def1

      .= ((s ^\ 1) . 0 ) by NAT_1:def 3;

      hence thesis by A2, Def1;

    end;

    theorem :: SERIES_1:12

    

     Th12: s is summable implies for n holds (s ^\ n) is summable

    proof

      defpred X[ Nat] means (s ^\ $1) is summable;

      

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

      proof

        let n;

        set s1 = ( seq_const ((s ^\ n) . 0 ));

        for k holds (s1 . k) = ((s ^\ n) . 0 ) by SEQ_1: 57;

        then

         A2: ( Partial_Sums ((s ^\ n) ^\ 1)) = ((( Partial_Sums (s ^\ n)) ^\ 1) - s1) by Th11;

        assume (s ^\ n) is summable;

        then ( Partial_Sums (s ^\ n)) is convergent;

        then (s ^\ (n + 1)) = ((s ^\ n) ^\ 1) & ( Partial_Sums ((s ^\ n) ^\ 1)) is convergent by A2, NAT_1: 48;

        hence thesis by Def2;

      end;

      assume s is summable;

      then

       A3: X[ 0 ] by NAT_1: 47;

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

    end;

    theorem :: SERIES_1:13

    

     Th13: (ex n st (s ^\ n) is summable) implies s is summable

    proof

      given n such that

       A1: (s ^\ n) is summable;

      reconsider PS = (( Partial_Sums s) . n) as Element of REAL ;

      set s1 = ( seq_const (( Partial_Sums s) . n));

      for k holds ((( Partial_Sums s) ^\ (n + 1)) . k) = ((( Partial_Sums (s ^\ (n + 1))) . k) + (s1 . k))

      proof

        defpred X[ Nat] means ((( Partial_Sums s) ^\ (n + 1)) . $1) = ((( Partial_Sums (s ^\ (n + 1))) . $1) + (s1 . $1));

        

         A2: (( Partial_Sums (s ^\ (n + 1))) . 0 ) = ((s ^\ (n + 1)) . 0 ) by Def1

        .= (s . ( 0 + (n + 1))) by NAT_1:def 3

        .= (s . (n + 1));

        

         A3: for k st X[k] holds X[(k + 1)]

        proof

          let k;

          assume

           A4: ((( Partial_Sums s) ^\ (n + 1)) . k) = ((( Partial_Sums (s ^\ (n + 1))) . k) + (s1 . k));

          ((( Partial_Sums (s ^\ (n + 1))) . (k + 1)) + (s1 . (k + 1))) = ((s1 . (k + 1)) + ((( Partial_Sums (s ^\ (n + 1))) . k) + ((s ^\ (n + 1)) . (k + 1)))) by Def1

          .= (((s1 . (k + 1)) + (( Partial_Sums (s ^\ (n + 1))) . k)) + ((s ^\ (n + 1)) . (k + 1)))

          .= (((( Partial_Sums s) . n) + (( Partial_Sums (s ^\ (n + 1))) . k)) + ((s ^\ (n + 1)) . (k + 1))) by SEQ_1: 57

          .= (((( Partial_Sums s) ^\ (n + 1)) . k) + ((s ^\ (n + 1)) . (k + 1))) by A4, SEQ_1: 57

          .= ((( Partial_Sums s) . (k + (n + 1))) + ((s ^\ (n + 1)) . (k + 1))) by NAT_1:def 3

          .= ((( Partial_Sums s) . (k + (n + 1))) + (s . ((k + 1) + (n + 1)))) by NAT_1:def 3

          .= (( Partial_Sums s) . ((k + (n + 1)) + 1)) by Def1

          .= (( Partial_Sums s) . ((k + 1) + (n + 1)))

          .= ((( Partial_Sums s) ^\ (n + 1)) . (k + 1)) by NAT_1:def 3;

          hence thesis;

        end;

        ((( Partial_Sums s) ^\ (n + 1)) . 0 ) = (( Partial_Sums s) . ( 0 + (n + 1))) by NAT_1:def 3

        .= ((s . (n + 1)) + (( Partial_Sums s) . n)) by Def1

        .= ((( Partial_Sums (s ^\ (n + 1))) . 0 ) + (s1 . 0 )) by A2, SEQ_1: 57;

        then

         A5: X[ 0 ];

        thus for k holds X[k] from NAT_1:sch 2( A5, A3);

      end;

      

      then

       A6: (( Partial_Sums s) ^\ (n + 1)) = (( Partial_Sums (s ^\ (n + 1))) + s1) by SEQ_1: 7

      .= (( Partial_Sums ((s ^\ n) ^\ 1)) + s1) by NAT_1: 48;

      ((s ^\ n) ^\ 1) is summable by A1, Th12;

      then ( Partial_Sums ((s ^\ n) ^\ 1)) is convergent;

      then (( Partial_Sums s) ^\ (n + 1)) is convergent by A6;

      then ( Partial_Sums s) is convergent by SEQ_4: 21;

      hence thesis;

    end;

    theorem :: SERIES_1:14

    

     Th14: (for n holds (s1 . n) <= (s2 . n)) implies for n holds (( Partial_Sums s1) . n) <= (( Partial_Sums s2) . n)

    proof

      defpred X[ Nat] means (( Partial_Sums s1) . $1) <= (( Partial_Sums s2) . $1);

      assume

       A1: for n holds (s1 . n) <= (s2 . n);

      

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

      proof

        let n such that

         A3: (( Partial_Sums s1) . n) <= (( Partial_Sums s2) . n);

        

         A4: (s1 . (n + 1)) <= (s2 . (n + 1)) by A1;

        (( Partial_Sums s1) . (n + 1)) = ((( Partial_Sums s1) . n) + (s1 . (n + 1))) & (( Partial_Sums s2) . (n + 1)) = ((( Partial_Sums s2) . n) + (s2 . (n + 1))) by Def1;

        hence thesis by A3, A4, XREAL_1: 7;

      end;

      (( Partial_Sums s2) . 0 ) = (s2 . 0 ) & (( Partial_Sums s1) . 0 ) = (s1 . 0 ) by Def1;

      then

       A5: X[ 0 ] by A1;

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

    end;

    theorem :: SERIES_1:15

    s is summable implies for n holds ( Sum s) = ((( Partial_Sums s) . n) + ( Sum (s ^\ (n + 1))))

    proof

      defpred X[ Nat] means ( Sum s) = ((( Partial_Sums s) . $1) + ( Sum (s ^\ ($1 + 1))));

      assume

       A1: s is summable;

      

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

      proof

        let n;

        assume

         A3: ( Sum s) = ((( Partial_Sums s) . n) + ( Sum (s ^\ (n + 1))));

        set s1 = ( seq_const ((s ^\ (n + 1)) . 0 ));

        for k holds (s1 . k) = ((s ^\ (n + 1)) . 0 ) by SEQ_1: 57;

        then

         A4: ( Partial_Sums ((s ^\ (n + 1)) ^\ 1)) = ((( Partial_Sums (s ^\ (n + 1))) ^\ 1) - s1) by Th11;

        (s ^\ (n + 1)) is summable by A1, Th12;

        then

         A5: ( Partial_Sums (s ^\ (n + 1))) is convergent;

        ( lim ( Partial_Sums (s ^\ ((n + 1) + 1)))) = ( lim ( Partial_Sums ((s ^\ (n + 1)) ^\ 1))) by NAT_1: 48

        .= (( lim (( Partial_Sums (s ^\ (n + 1))) ^\ 1)) - ( lim s1)) by A5, A4, SEQ_2: 12

        .= (( lim ( Partial_Sums (s ^\ (n + 1)))) - ( lim s1)) by A5, SEQ_4: 20

        .= (( Sum (s ^\ (n + 1))) - (s1 . 0 )) by SEQ_4: 26

        .= (( Sum (s ^\ (n + 1))) - ((s ^\ (n + 1)) . 0 )) by SEQ_1: 57;

        

        then ( Sum (s ^\ ((n + 1) + 1))) = (( Sum s) - ((( Partial_Sums s) . n) + ((s ^\ (n + 1)) . 0 ))) by A3

        .= (( Sum s) - ((( Partial_Sums s) . n) + (s . ( 0 + (n + 1))))) by NAT_1:def 3

        .= (( Sum s) - (( Partial_Sums s) . (n + 1))) by Def1;

        hence thesis;

      end;

      

       A6: X[ 0 ]

      proof

        set s1 = ( seq_const (s . 0 ));

        

         A7: ( Partial_Sums s) is convergent by A1;

        for k holds (s1 . k) = (s . 0 ) by SEQ_1: 57;

        then ( Partial_Sums (s ^\ 1)) = ((( Partial_Sums s) ^\ 1) - s1) by Th11;

        

        then ( lim ( Partial_Sums (s ^\ 1))) = (( lim (( Partial_Sums s) ^\ 1)) - ( lim s1)) by A7, SEQ_2: 12

        .= (( lim ( Partial_Sums s)) - ( lim s1)) by A7, SEQ_4: 20

        .= (( Sum s) - (s1 . 0 )) by SEQ_4: 26

        .= (( Sum s) - (s . 0 )) by SEQ_1: 57;

        then ( Sum s) = (( Sum (s ^\ 1)) + ( - ( - (s . 0 ))));

        hence thesis by Def1;

      end;

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

    end;

    theorem :: SERIES_1:16

    

     Th16: (for n holds 0 <= (s . n)) implies ( Partial_Sums s) is non-decreasing

    proof

      assume

       A1: for n holds 0 <= (s . n);

      now

        let n;

         0 <= (s . (n + 1)) by A1;

        then ( 0 + (( Partial_Sums s) . n)) <= ((s . (n + 1)) + (( Partial_Sums s) . n)) by XREAL_1: 6;

        hence (( Partial_Sums s) . n) <= (( Partial_Sums s) . (n + 1)) by Def1;

      end;

      hence thesis;

    end;

    theorem :: SERIES_1:17

    

     Th17: (for n holds 0 <= (s . n)) implies (( Partial_Sums s) is bounded_above iff s is summable)

    proof

      assume for n holds 0 <= (s . n);

      then ( Partial_Sums s) is non-decreasing by Th16;

      hence ( Partial_Sums s) is bounded_above implies s is summable;

      assume s is summable;

      then ( Partial_Sums s) is convergent;

      then ( Partial_Sums s) is bounded;

      hence thesis;

    end;

    theorem :: SERIES_1:18

    s is summable & (for n holds 0 <= (s . n)) implies 0 <= ( Sum s)

    proof

      assume that

       A1: s is summable and

       A2: for n holds 0 <= (s . n);

       A3:

      now

        let n;

        

         A4: (( Partial_Sums s) . 0 ) = (s . 0 ) by Def1;

        (( Partial_Sums s) . 0 ) <= (( Partial_Sums s) . n) & 0 <= (s . 0 ) by A2, Th16, SEQM_3: 11;

        hence 0 <= (( Partial_Sums s) . n) by A4;

      end;

      ( Partial_Sums s) is convergent by A1;

      hence thesis by A3, SEQ_2: 17;

    end;

    theorem :: SERIES_1:19

    

     Th19: (for n holds 0 <= (s2 . n)) & s1 is summable & (ex m st for n st m <= n holds (s2 . n) <= (s1 . n)) implies s2 is summable

    proof

      assume that

       A1: for n holds 0 <= (s2 . n) and

       A2: s1 is summable;

      given m such that

       A3: for n st m <= n holds (s2 . n) <= (s1 . n);

      (s1 ^\ m) is summable by A2, Th12;

      then ( Partial_Sums (s1 ^\ m)) is bounded_above;

      then

      consider r be Real such that

       A4: for n holds (( Partial_Sums (s1 ^\ m)) . n) < r by SEQ_2:def 3;

       A5:

      now

        let n;

        (s2 . (n + m)) <= (s1 . (n + m)) by A3, NAT_1: 12;

        then ((s2 ^\ m) . n) <= (s1 . (n + m)) by NAT_1:def 3;

        hence ((s2 ^\ m) . n) <= ((s1 ^\ m) . n) by NAT_1:def 3;

      end;

      now

        let n;

        (( Partial_Sums (s2 ^\ m)) . n) <= (( Partial_Sums (s1 ^\ m)) . n) by A5, Th14;

        hence (( Partial_Sums (s2 ^\ m)) . n) < r by A4, XXREAL_0: 2;

      end;

      then

       A6: ( Partial_Sums (s2 ^\ m)) is bounded_above by SEQ_2:def 3;

      now

        let n;

        ((s2 ^\ m) . n) = (s2 . (n + m)) by NAT_1:def 3;

        hence 0 <= ((s2 ^\ m) . n) by A1;

      end;

      then (s2 ^\ m) is summable by A6, Th17;

      hence thesis by Th13;

    end;

    theorem :: SERIES_1:20

    (for n holds 0 <= (s1 . n) & (s1 . n) <= (s2 . n)) & s2 is summable implies s1 is summable & ( Sum s1) <= ( Sum s2)

    proof

      assume that

       A1: for n holds 0 <= (s1 . n) & (s1 . n) <= (s2 . n) and

       A2: s2 is summable;

      for n holds 0 <= n implies (s1 . n) <= (s2 . n) by A1;

      hence s1 is summable by A1, A2, Th19;

      then

       A3: ( Partial_Sums s1) is convergent;

      ( Partial_Sums s2) is convergent & for n holds (( Partial_Sums s1) . n) <= (( Partial_Sums s2) . n) by A1, A2, Th14;

      hence thesis by A3, SEQ_2: 18;

    end;

    theorem :: SERIES_1:21

    

     Th21: s is summable iff for r st 0 < r holds ex n st for m st n <= m holds |.((( Partial_Sums s) . m) - (( Partial_Sums s) . n)).| < r by SEQ_4: 41;

    ::$Notion-Name

    theorem :: SERIES_1:22

    

     Th22: a <> 1 implies (( Partial_Sums (a GeoSeq )) . n) = ((1 - (a to_power (n + 1))) / (1 - a))

    proof

      defpred X[ Nat] means (( Partial_Sums (a GeoSeq )) . $1) = ((1 - (a to_power ($1 + 1))) / (1 - a));

      assume a <> 1;

      then

       A1: (1 - a) <> 0 ;

      

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

      proof

        let n;

        assume (( Partial_Sums (a GeoSeq )) . n) = ((1 - (a to_power (n + 1))) / (1 - a));

        

        hence (( Partial_Sums (a GeoSeq )) . (n + 1)) = (((1 - (a to_power (n + 1))) / (1 - a)) + ((a GeoSeq ) . (n + 1))) by Def1

        .= (((1 - (a to_power (n + 1))) / (1 - a)) + ((a to_power (n + 1)) * 1)) by PREPOWER:def 1

        .= (((1 - (a to_power (n + 1))) / (1 - a)) + ((a to_power (n + 1)) * ((1 - a) / (1 - a)))) by A1, XCMPLX_1: 60

        .= (((1 - (a to_power (n + 1))) / (1 - a)) + (((a to_power (n + 1)) * (1 - a)) / (1 - a)))

        .= (((1 - (a to_power (n + 1))) + ((a to_power (n + 1)) - ((a |^ (n + 1)) * a))) / (1 - a))

        .= (((1 - (a to_power (n + 1))) + ((a to_power (n + 1)) - (a |^ ((n + 1) + 1)))) / (1 - a)) by NEWTON: 6

        .= ((1 - (a to_power ((n + 1) + 1))) / (1 - a));

      end;

      (( Partial_Sums (a GeoSeq )) . 0 ) = ((a GeoSeq ) . 0 ) by Def1

      .= 1 by PREPOWER: 3

      .= ((1 - a) / (1 - a)) by A1, XCMPLX_1: 60

      .= ((1 - (a to_power ( 0 + 1))) / (1 - a));

      then

       A3: X[ 0 ];

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

      hence thesis;

    end;

    theorem :: SERIES_1:23

    a <> 1 & (for n holds (s . (n + 1)) = (a * (s . n))) implies for n holds (( Partial_Sums s) . n) = (((s . 0 ) * (1 - (a to_power (n + 1)))) / (1 - a))

    proof

      assume that

       A1: a <> 1 and

       A2: for n holds (s . (n + 1)) = (a * (s . n));

      defpred X[ Nat] means (s . $1) = ((s . 0 ) * ((a GeoSeq ) . $1));

      

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

      proof

        let n;

        assume (s . n) = ((s . 0 ) * ((a GeoSeq ) . n));

        

        then (s . (n + 1)) = (a * ((s . 0 ) * ((a GeoSeq ) . n))) by A2

        .= ((s . 0 ) * (((a GeoSeq ) . n) * a))

        .= ((s . 0 ) * ((a GeoSeq ) . (n + 1))) by PREPOWER: 3;

        hence thesis;

      end;

      ((a GeoSeq ) . 0 ) = 1 by PREPOWER: 3;

      then

       A4: X[ 0 ];

      for n holds X[n] from NAT_1:sch 2( A4, A3);

      then s = ((s . 0 ) (#) (a GeoSeq )) by SEQ_1: 9;

      then

       A5: ( Partial_Sums s) = ((s . 0 ) (#) ( Partial_Sums (a GeoSeq ))) by Th9;

      now

        let n;

        

        thus (( Partial_Sums s) . n) = ((s . 0 ) * (( Partial_Sums (a GeoSeq )) . n)) by A5, SEQ_1: 9

        .= ((s . 0 ) * ((1 - (a to_power (n + 1))) / (1 - a))) by A1, Th22

        .= (((s . 0 ) * (1 - (a to_power (n + 1)))) / (1 - a));

      end;

      hence thesis;

    end;

    theorem :: SERIES_1:24

    

     Th24: |.a.| < 1 implies (a GeoSeq ) is summable & ( Sum (a GeoSeq )) = (1 / (1 - a))

    proof

      deffunc U( Nat) = (a to_power ($1 + 1));

      consider s such that

       A1: for n holds (s . n) = U(n) from SEQ_1:sch 1;

      assume

       A2: |.a.| < 1;

      then

       A3: s is convergent & ( lim s) = 0 by A1, Th3;

       A4:

      now

        a < 1 by A2, SEQ_2: 1;

        then

         A5: (1 - a) > 0 by XREAL_1: 50;

        let r be Real;

        assume r > 0 ;

        then (r * (1 - a)) > ( 0 * r) by A5;

        then

        consider m such that

         A6: for n st n >= m holds |.((s . n) - 0 ).| < (r * (1 - a)) by A3, SEQ_2:def 7;

        take m;

        let n;

        assume n >= m;

        then |.((s . n) - 0 ).| < (r * (1 - a)) by A6;

        then |.((a to_power (n + 1)) - 0 ).| < (r * (1 - a)) by A1;

        then

         A7: ( |.(a to_power (n + 1)).| / (1 - a)) < ((r * (1 - a)) / (1 - a)) by A5, XREAL_1: 74;

        a <> 1 by A2, SEQ_2: 1;

        

        then

         A8: |.((( Partial_Sums (a GeoSeq )) . n) - (1 / (1 - a))).| = |.(((1 - (a to_power (n + 1))) / (1 - a)) - (1 / (1 - a))).| by Th22

        .= |.(((1 + ( - (a to_power (n + 1)))) - 1) / (1 - a)).|

        .= |.( - ((a to_power (n + 1)) / (1 - a))).|

        .= |.((a to_power (n + 1)) / (1 - a)).| by COMPLEX1: 52

        .= ( |.(a to_power (n + 1)).| / |.(1 - a).|) by COMPLEX1: 67

        .= ( |.(a to_power (n + 1)).| / (1 - a)) by A5, ABSVALUE:def 1;

        (1 - a) <> 0 by A2, SEQ_2: 1;

        hence |.((( Partial_Sums (a GeoSeq )) . n) - (1 / (1 - a))).| < r by A8, A7, XCMPLX_1: 89;

      end;

      then

       A9: ( Partial_Sums (a GeoSeq )) is convergent by SEQ_2:def 6;

      hence (a GeoSeq ) is summable;

      thus thesis by A4, A9, SEQ_2:def 7;

    end;

    theorem :: SERIES_1:25

     |.a.| < 1 & (for n holds (s . (n + 1)) = (a * (s . n))) implies s is summable & ( Sum s) = ((s . 0 ) / (1 - a))

    proof

      assume that

       A1: |.a.| < 1 and

       A2: for n holds (s . (n + 1)) = (a * (s . n));

      defpred X[ Nat] means (s . $1) = ((s . 0 ) * ((a GeoSeq ) . $1));

      

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

      proof

        let n;

        assume (s . n) = ((s . 0 ) * ((a GeoSeq ) . n));

        

        then (s . (n + 1)) = (a * ((s . 0 ) * ((a GeoSeq ) . n))) by A2

        .= ((s . 0 ) * (((a GeoSeq ) . n) * a))

        .= ((s . 0 ) * ((a GeoSeq ) . (n + 1))) by PREPOWER: 3;

        hence thesis;

      end;

      ((a GeoSeq ) . 0 ) = 1 by PREPOWER: 3;

      then

       A4: X[ 0 ];

      for n holds X[n] from NAT_1:sch 2( A4, A3);

      then s = ((s . 0 ) (#) (a GeoSeq )) by SEQ_1: 9;

      then

       A5: ( Partial_Sums s) = ((s . 0 ) (#) ( Partial_Sums (a GeoSeq ))) by Th9;

      (a GeoSeq ) is summable by A1, Th24;

      then

       A6: ( Partial_Sums (a GeoSeq )) is convergent;

      then ( Partial_Sums s) is convergent by A5;

      hence s is summable;

      ( Sum (a GeoSeq )) = (1 / (1 - a)) by A1, Th24;

      

      then ( lim ( Partial_Sums s)) = ((s . 0 ) * (1 / (1 - a))) by A5, A6, SEQ_2: 8

      .= (((s . 0 ) * 1) / (1 - a))

      .= ((s . 0 ) / (1 - a));

      hence thesis;

    end;

    theorem :: SERIES_1:26

    

     Th26: (for n holds (s . n) > 0 & (s1 . n) = ((s . (n + 1)) / (s . n))) & s1 is convergent & ( lim s1) < 1 implies s is summable

    proof

      assume that

       A1: for n holds (s . n) > 0 & (s1 . n) = ((s . (n + 1)) / (s . n)) and

       A2: s1 is convergent and

       A3: ( lim s1) < 1;

      set r = ((1 - ( lim s1)) / 2);

      ( 0 + ( lim s1)) < 1 by A3;

      then 0 < (1 - ( lim s1)) by XREAL_1: 20;

      then r > 0 ;

      then

      consider m such that

       A4: for n st m <= n holds |.((s1 . n) - ( lim s1)).| < r by A2, SEQ_2:def 7;

      set s2 = (((s . m) * ((1 - r) to_power ( - m))) (#) ((1 - r) GeoSeq ));

      defpred X[ Nat] means (s . (m + $1)) <= (s2 . (m + $1));

       A5:

      now

        let n;

        (s . n) > 0 & (s . (n + 1)) > 0 by A1;

        then ((s . (n + 1)) / (s . n)) > 0 ;

        hence (s1 . n) >= 0 by A1;

      end;

      then

       A6: ( lim s1) >= 0 by A2, PREPOWER: 1;

      then (1 + ( - ( lim s1))) < (1 + 1) by XREAL_1: 6;

      then

       A7: ((1 - ( lim s1)) / 2) < (2 / 2) by XREAL_1: 74;

      

       A8: (r + ( lim s1)) = (1 - r);

      

       A9: for k holds X[k] implies X[(k + 1)]

      proof

        set X = ((s . m) * ((1 - r) to_power ( - m)));

        let k such that

         A10: (s . (m + k)) <= (s2 . (m + k));

         |.((s1 . (m + k)) - ( lim s1)).| < r by A4, NAT_1: 11;

        then ((s1 . (m + k)) - ( lim s1)) < r by SEQ_2: 1;

        then

         A11: (s1 . (m + k)) <= (1 - r) by A8, XREAL_1: 19;

        (s2 . (m + k)) >= 0 by A1, A10;

        then

         A12: ((s1 . (m + k)) * (s2 . (m + k))) <= ((1 - r) * (s2 . (m + k))) by A11, XREAL_1: 64;

        (s . (m + k)) <> 0 by A1;

        

        then

         A13: (s . (m + (k + 1))) = (((s . ((m + k) + 1)) / (s . (m + k))) * (s . (m + k))) by XCMPLX_1: 87

        .= ((s1 . (m + k)) * (s . (m + k))) by A1;

        (s1 . (m + k)) >= 0 by A5;

        then

         A14: (s . (m + (k + 1))) <= ((s1 . (m + k)) * (s2 . (m + k))) by A10, A13, XREAL_1: 64;

        ((1 - r) * (s2 . (m + k))) = ((1 - r) * (X * (((1 - r) GeoSeq ) . (m + k)))) by SEQ_1: 9

        .= (X * ((((1 - r) GeoSeq ) . (m + k)) * (1 - r)))

        .= (X * (((1 - r) GeoSeq ) . ((m + k) + 1))) by PREPOWER: 3

        .= (s2 . (m + (k + 1))) by SEQ_1: 9;

        hence thesis by A14, A12, XXREAL_0: 2;

      end;

      (s2 . (m + 0 )) = (((s . m) * ((1 - r) to_power ( - m))) * (((1 - r) GeoSeq ) . m)) by SEQ_1: 9

      .= (((s . m) * ((1 - r) to_power ( - m))) * ((1 - r) |^ m)) by PREPOWER:def 1

      .= ((s . m) * (((1 - r) to_power ( - m)) * ((1 - r) to_power m)))

      .= ((s . m) * ((1 - r) to_power (( - m) + m))) by A7, POWER: 27, XREAL_1: 50

      .= ((s . m) * 1) by POWER: 24

      .= (s . (m + 0 ));

      then

       A15: X[ 0 ];

      

       A16: for k holds X[k] from NAT_1:sch 2( A15, A9);

       A17:

      now

        let n;

        assume m <= n;

        then

        consider k be Nat such that

         A18: n = (m + k) by NAT_1: 10;

        reconsider k as Element of NAT by ORDINAL1:def 12;

        n = (m + k) by A18;

        hence (s . n) <= (s2 . n) by A16;

      end;

      (1 - ( lim s1)) <= (1 - 0 ) by A6, XREAL_1: 6;

      then (1 - ( lim s1)) < (2 * 2) by XXREAL_0: 2;

      then r < ((2 * 2) / 2) by XREAL_1: 74;

      then r < (1 + 1);

      then (r - 1) < 1 by XREAL_1: 19;

      then

       A19: ( - (r - 1)) > ( - 1) by XREAL_1: 24;

      (1 - ( lim s1)) > 0 by A3, XREAL_1: 50;

      then r > 0 ;

      then (1 - r) < (1 - 0 ) by XREAL_1: 10;

      then |.(1 - r).| < 1 by A19, SEQ_2: 1;

      then ((1 - r) GeoSeq ) is summable by Th24;

      then

       A20: s2 is summable by Th10;

      for n holds 0 <= (s . n) by A1;

      hence thesis by A20, A17, Th19;

    end;

    theorem :: SERIES_1:27

    (for n holds (s . n) > 0 ) & (ex m st for n st n >= m holds ((s . (n + 1)) / (s . n)) >= 1) implies not s is summable

    proof

      assume that

       A1: for n holds (s . n) > 0 and

       A2: ex m st for n st n >= m holds ((s . (n + 1)) / (s . n)) >= 1;

      consider m such that

       A3: for n st n >= m holds ((s . (n + 1)) / (s . n)) >= 1 by A2;

      defpred X[ Nat] means (s . (m + $1)) >= (s . m);

      

       A4: for k st X[k] holds X[(k + 1)]

      proof

        let k such that

         A5: (s . (m + k)) >= (s . m);

        (s . (m + k)) > 0 & ((s . ((m + k) + 1)) / (s . (m + k))) >= 1 by A1, A3, NAT_1: 11;

        then (s . ((m + k) + 1)) >= (s . (m + k)) by XREAL_1: 191;

        hence thesis by A5, XXREAL_0: 2;

      end;

      

       A6: X[ 0 ];

      

       A7: for k holds X[k] from NAT_1:sch 2( A6, A4);

      

       A8: for k holds ex n st n >= k & not |.((s . n) - 0 ).| < (s . m)

      proof

        let k;

        take n = (m + k);

        (s . n) >= (s . m) by A7;

        hence thesis by NAT_1: 11, SEQ_2: 1;

      end;

      (s . m) > 0 by A1;

      then not ( lim s) = 0 or not s is convergent by A8, SEQ_2:def 7;

      hence thesis by Th4;

    end;

    theorem :: SERIES_1:28

    

     Th28: (for n holds (s . n) >= 0 & (s1 . n) = (n -root (s . n))) & s1 is convergent & ( lim s1) < 1 implies s is summable

    proof

      assume that

       A1: for n holds (s . n) >= 0 & (s1 . n) = (n -root (s . n)) and

       A2: s1 is convergent and

       A3: ( lim s1) < 1;

       A4:

      now

        let n;

        

         A5: ((s1 ^\ 1) . n) = (s1 . (n + 1)) by NAT_1:def 3

        .= ((n + 1) -root (s . (n + 1))) by A1;

        (s . (n + 1)) >= 0 by A1;

        hence ((s1 ^\ 1) . n) >= 0 by A5, NAT_1: 11, POWER: 7;

      end;

      set r = ((1 - ( lim s1)) / 2);

      ( 0 + ( lim s1)) < 1 by A3;

      then 0 < (1 - ( lim s1)) by XREAL_1: 20;

      then r > 0 ;

      then

      consider m such that

       A6: for n st m <= n holds |.((s1 . n) - ( lim s1)).| < r by A2, SEQ_2:def 7;

      ( lim (s1 ^\ 1)) = ( lim s1) by A2, SEQ_4: 20;

      then

       A7: ( lim s1) >= 0 by A2, A4, PREPOWER: 1;

      then (1 + ( - ( lim s1))) < (1 + 1) by XREAL_1: 6;

      then ((1 - ( lim s1)) / 2) < (2 / 2) by XREAL_1: 74;

      then

       A8: (1 - r) > 0 by XREAL_1: 50;

      set s2 = ((1 - r) GeoSeq );

      

       A9: (r + ( lim s1)) = (1 - r);

      

       A10: for n st (m + 1) <= n holds (s . n) <= ((1 - r) to_power n)

      proof

        let n;

        assume

         A11: (m + 1) <= n;

        1 <= (m + 1) by NAT_1: 11;

        then

         A12: 1 <= n by A11, XXREAL_0: 2;

        

         A13: (s . n) >= 0 by A1;

        m <= n by A11, NAT_1: 13;

        then |.((s1 . n) - ( lim s1)).| < r by A6;

        then ((s1 . n) - ( lim s1)) < r by SEQ_2: 1;

        then (s1 . n) < (1 - r) by A9, XREAL_1: 19;

        then

         A14: (n -root (s . n)) < (1 - r) by A1;

        now

          per cases ;

            suppose (s . n) = 0 ;

            hence (s . n) < ((1 - r) to_power n) by A8, POWER: 34;

          end;

            suppose (s . n) <> 0 ;

            then (n -Root (s . n)) > 0 by A12, A13, PREPOWER:def 2;

            then (n -root (s . n)) > 0 by A12, A13, POWER:def 1;

            then ((n -root (s . n)) to_power n) < ((1 - r) to_power n) by A11, A14, POWER: 37;

            hence (s . n) < ((1 - r) to_power n) by A12, A13, POWER: 4;

          end;

        end;

        hence thesis;

      end;

      

       A15: for n st (m + 1) <= n holds (s . n) <= (s2 . n)

      proof

        let n;

        (s2 . n) = ((1 - r) to_power n) by PREPOWER:def 1;

        hence thesis by A10;

      end;

      (1 - ( lim s1)) <= (1 - 0 ) by A7, XREAL_1: 6;

      then (1 - ( lim s1)) < (2 * 2) by XXREAL_0: 2;

      then r < ((2 * 2) / 2) by XREAL_1: 74;

      then r < (1 + 1);

      then (r - 1) < 1 by XREAL_1: 19;

      then

       A16: ( - (r - 1)) > ( - 1) by XREAL_1: 24;

      (1 - ( lim s1)) > 0 by A3, XREAL_1: 50;

      then r > 0 ;

      then (1 - r) < (1 - 0 ) by XREAL_1: 10;

      then |.(1 - r).| < 1 by A16, SEQ_2: 1;

      then s2 is summable by Th24;

      hence thesis by A1, A15, Th19;

    end;

    theorem :: SERIES_1:29

    

     Th29: (for n holds (s . n) >= 0 & (s1 . n) = (n -root (s . n))) & (ex m st for n st m <= n holds (s1 . n) >= 1) implies not s is summable

    proof

      assume that

       A1: for n holds (s . n) >= 0 & (s1 . n) = (n -root (s . n)) and

       A2: ex m st for n st m <= n holds (s1 . n) >= 1;

      consider m such that

       A3: for n st m <= n holds (s1 . n) >= 1 by A2;

      

       A4: for n st (m + 1) <= n holds (s . n) >= 1

      proof

        let n such that

         A5: (m + 1) <= n;

        1 <= (1 + m) by NAT_1: 11;

        then

         A6: 1 <= n by A5, XXREAL_0: 2;

        

         A7: (s . n) >= 0 by A1;

        m <= (m + 1) by NAT_1: 11;

        then m <= n by A5, XXREAL_0: 2;

        then (s1 . n) >= 1 by A3;

        then

         A8: (n -root (s . n)) >= 1 by A1;

        now

          per cases by A8, XXREAL_0: 1;

            suppose (n -root (s . n)) = 1;

            then (s . n) = (1 |^ n) by A6, A7, POWER: 4;

            hence thesis;

          end;

            suppose (n -root (s . n)) > 1;

            then ((n -root (s . n)) to_power n) > 1 by A5, POWER: 35;

            hence thesis by A6, A7, POWER: 4;

          end;

        end;

        hence thesis;

      end;

      for k holds ex n st k <= n & not |.((s . n) - 0 ).| < 1

      proof

        let k;

        take n = ((m + 1) + k);

         not (s . n) < 1 by A4, NAT_1: 11;

        hence thesis by NAT_1: 11, SEQ_2: 1;

      end;

      then not s is convergent or not ( lim s) = 0 by SEQ_2:def 7;

      hence thesis by Th4;

    end;

    theorem :: SERIES_1:30

    (for n holds (s . n) >= 0 & (s1 . n) = (n -root (s . n))) & s1 is convergent & ( lim s1) > 1 implies not s is summable

    proof

      assume that

       A1: for n holds (s . n) >= 0 & (s1 . n) = (n -root (s . n)) and

       A2: s1 is convergent and

       A3: ( lim s1) > 1;

      set r = (( lim s1) - 1);

      r > 0 by A3, XREAL_1: 50;

      then

      consider m such that

       A4: for n st m <= n holds |.((s1 . n) - ( lim s1)).| < r by A2, SEQ_2:def 7;

      for n st m <= n holds (s1 . n) >= 1

      proof

        let n;

        assume m <= n;

        then |.((s1 . n) - ( lim s1)).| < r by A4;

        then ((s1 . n) - ( lim s1)) > ( - r) by SEQ_2: 1;

        then (((s1 . n) - ( lim s1)) + ( lim s1)) > (( - r) + ( lim s1)) by XREAL_1: 6;

        hence thesis;

      end;

      hence thesis by A1, Th29;

    end;

    registration

      let k,n be Nat;

      cluster (k to_power n) -> natural;

      coherence ;

    end

    definition

      let k,n be Nat;

      :: original: to_power

      redefine

      func k to_power n -> Element of NAT ;

      coherence by ORDINAL1:def 12;

    end

    theorem :: SERIES_1:31

    

     Th31: s is non-increasing & (for n holds (s . n) >= 0 & (s1 . n) = ((2 to_power n) * (s . (2 to_power n)))) implies (s is summable iff s1 is summable)

    proof

      assume that

       A1: s is non-increasing and

       A2: for n holds (s . n) >= 0 & (s1 . n) = ((2 to_power n) * (s . (2 to_power n)));

      

       A3: (( Partial_Sums s) . (2 to_power ( 0 + 1))) = (( Partial_Sums s) . (1 + 1))

      .= ((( Partial_Sums s) . ( 0 + 1)) + (s . 2)) by Def1

      .= (((( Partial_Sums s) . 0 ) + (s . 1)) + (s . 2)) by Def1

      .= (((s . 0 ) + (s . 1)) + (s . 2)) by Def1;

       A4:

      now

        let n;

        (s . (2 to_power n)) >= 0 by A2;

        then ((2 to_power n) * (s . (2 to_power n))) >= 0 ;

        hence (s1 . n) >= 0 by A2;

      end;

      thus s is summable implies s1 is summable

      proof

        defpred Y[ Nat] means (( Partial_Sums s1) . $1) <= (2 * (( Partial_Sums s) . (2 to_power $1)));

        

         A5: (s . 0 ) >= 0 by A2;

        

         A6: for n st Y[n] holds Y[(n + 1)]

        proof

          let n;

          deffunc U( Nat) = ((( Partial_Sums s) . ((2 to_power n) + $1)) - (( Partial_Sums s) . (2 to_power n)));

          consider a be Real_Sequence such that

           A7: for m holds (a . m) = U(m) from SEQ_1:sch 1;

          defpred X[ Nat] means $1 > (2 to_power n) or ($1 * (s . (2 to_power (n + 1)))) <= (a . $1);

          

           A8: for m st X[m] holds X[(m + 1)]

          proof

            let m;

            assume

             A9: m > (2 to_power n) or (m * (s . (2 to_power (n + 1)))) <= (a . m);

            now

              per cases by A9;

                suppose m > (2 to_power n);

                hence thesis by NAT_1: 13;

              end;

                suppose

                 A10: (m * (s . (2 to_power (n + 1)))) <= (a . m);

                now

                  per cases ;

                    suppose m < (2 to_power n);

                    then (m + 1) <= (2 to_power n) by NAT_1: 13;

                    then ((2 to_power n) + (m + 1)) <= ((2 to_power n) + (2 to_power n)) by XREAL_1: 7;

                    then (((2 to_power n) + m) + 1) <= (2 * (2 to_power n));

                    then (((2 to_power n) + m) + 1) <= ((2 to_power 1) * (2 to_power n));

                    then (((2 to_power n) + m) + 1) <= (2 to_power (n + 1)) by POWER: 27;

                    then (s . (((2 to_power n) + m) + 1)) >= (s . (2 to_power (n + 1))) by A1, SEQM_3: 8;

                    then ((m * (s . (2 to_power (n + 1)))) + (1 * (s . (2 to_power (n + 1))))) <= ((a . m) + (s . (((2 to_power n) + m) + 1))) by A10, XREAL_1: 7;

                    then ((m + 1) * (s . (2 to_power (n + 1)))) <= (((( Partial_Sums s) . ((2 to_power n) + m)) - (( Partial_Sums s) . (2 to_power n))) + (s . (((2 to_power n) + m) + 1))) by A7;

                    then ((m + 1) * (s . (2 to_power (n + 1)))) <= (((( Partial_Sums s) . ((2 to_power n) + m)) + (s . (((2 to_power n) + m) + 1))) - (( Partial_Sums s) . (2 to_power n)));

                    then ((m + 1) * (s . (2 to_power (n + 1)))) <= ((( Partial_Sums s) . ((2 to_power n) + (m + 1))) - (( Partial_Sums s) . (2 to_power n))) by Def1;

                    hence thesis by A7;

                  end;

                    suppose m >= (2 to_power n);

                    hence thesis by NAT_1: 13;

                  end;

                end;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

          (a . 0 ) = ((( Partial_Sums s) . ((2 to_power n) + 0 )) - (( Partial_Sums s) . (2 to_power n))) by A7

          .= 0 ;

          then

           A11: X[ 0 ];

          for m holds X[m] from NAT_1:sch 2( A11, A8);

          then (2 * ((2 to_power n) * (s . (2 to_power (n + 1))))) <= (2 * (a . (2 to_power n))) by XREAL_1: 64;

          then ((2 * (2 to_power n)) * (s . (2 to_power (n + 1)))) <= (2 * (a . (2 to_power n)));

          then (((2 to_power 1) * (2 to_power n)) * (s . (2 to_power (n + 1)))) <= (2 * (a . (2 to_power n)));

          then ((2 to_power (n + 1)) * (s . (2 to_power (n + 1)))) <= (2 * (a . (2 to_power n))) by POWER: 27;

          then (s1 . (n + 1)) <= (2 * (a . (2 to_power n))) by A2;

          then (s1 . (n + 1)) <= (2 * ((( Partial_Sums s) . ((2 to_power n) + (2 to_power n))) - (( Partial_Sums s) . (2 to_power n)))) by A7;

          then

           A12: ((2 * (( Partial_Sums s) . (2 to_power n))) + (s1 . (n + 1))) <= ((2 * (( Partial_Sums s) . (2 to_power n))) + (2 * ((( Partial_Sums s) . ((2 to_power n) + (2 to_power n))) - (( Partial_Sums s) . (2 to_power n))))) by XREAL_1: 7;

          assume (( Partial_Sums s1) . n) <= (2 * (( Partial_Sums s) . (2 to_power n)));

          then ((( Partial_Sums s1) . n) + (s1 . (n + 1))) <= ((2 * (( Partial_Sums s) . (2 to_power n))) + (s1 . (n + 1))) by XREAL_1: 6;

          then

           A13: (( Partial_Sums s1) . (n + 1)) <= ((2 * (( Partial_Sums s) . (2 to_power n))) + (s1 . (n + 1))) by Def1;

          ((2 to_power n) + (2 to_power n)) = (2 * (2 to_power n))

          .= ((2 to_power 1) * (2 to_power n))

          .= (2 to_power (n + 1)) by POWER: 27;

          hence thesis by A13, A12, XXREAL_0: 2;

        end;

        

         A14: (2 to_power 0 ) = ( 0 + 1) by POWER: 24;

        

        then

         A15: (2 * (( Partial_Sums s) . (2 to_power 0 ))) = (2 * ((( Partial_Sums s) . 0 ) + (s . 1))) by Def1

        .= (2 * ((s . 0 ) + (s . 1))) by Def1

        .= ((2 * (s . 0 )) + (2 * (s . 1)));

        assume s is summable;

        then ( Partial_Sums s) is bounded_above;

        then

        consider r be Real such that

         A16: for n holds (( Partial_Sums s) . n) < r by SEQ_2:def 3;

        (s . 1) >= 0 by A2;

        then

         A17: ((s . 1) + (s . 1)) >= ((s . 1) + 0 ) by XREAL_1: 7;

        (( Partial_Sums s1) . 0 ) = (s1 . 0 ) by Def1

        .= (1 * (s . 1)) by A2, A14

        .= (s . 1);

        then

         A18: Y[ 0 ] by A15, A17, A5, XREAL_1: 7;

        

         A19: for n holds Y[n] from NAT_1:sch 2( A18, A6);

        now

          let n;

          (2 * (( Partial_Sums s) . (2 to_power n))) < (2 * r) & (( Partial_Sums s1) . n) <= (2 * (( Partial_Sums s) . (2 to_power n))) by A19, A16, XREAL_1: 68;

          hence (( Partial_Sums s1) . n) < (2 * r) by XXREAL_0: 2;

        end;

        then ( Partial_Sums s1) is bounded_above by SEQ_2:def 3;

        hence thesis by A4, Th17;

      end;

      assume s1 is summable;

      then ( Partial_Sums s1) is bounded_above;

      then

      consider r be Real such that

       A20: for n holds (( Partial_Sums s1) . n) < r by SEQ_2:def 3;

      

       A21: (2 to_power 0 ) = 1 by POWER: 24;

      defpred Y[ Nat] means (( Partial_Sums s) . (2 to_power ($1 + 1))) <= (((( Partial_Sums s1) . $1) + (s . 0 )) + (s . 2));

      

       A22: for n st Y[n] holds Y[(n + 1)]

      proof

        let n;

        defpred X[ Nat] means ((( Partial_Sums s) . ((2 to_power (n + 1)) + $1)) - (( Partial_Sums s) . (2 to_power (n + 1)))) <= ($1 * (s . (2 to_power (n + 1))));

        

         A23: for m st X[m] holds X[(m + 1)]

        proof

          let m;

          ((2 to_power (n + 1)) + (m + 1)) >= (2 to_power (n + 1)) by NAT_1: 11;

          then

           A24: (s . ((2 to_power (n + 1)) + (m + 1))) <= (s . (2 to_power (n + 1))) by A1, SEQM_3: 8;

          assume ((( Partial_Sums s) . ((2 to_power (n + 1)) + m)) - (( Partial_Sums s) . (2 to_power (n + 1)))) <= (m * (s . (2 to_power (n + 1))));

          then (((( Partial_Sums s) . ((2 to_power (n + 1)) + m)) - (( Partial_Sums s) . (2 to_power (n + 1)))) + (s . (((2 to_power (n + 1)) + m) + 1))) <= ((m * (s . (2 to_power (n + 1)))) + (s . (2 to_power (n + 1)))) by A24, XREAL_1: 7;

          then (((( Partial_Sums s) . ((2 to_power (n + 1)) + m)) + (s . (((2 to_power (n + 1)) + m) + 1))) - (( Partial_Sums s) . (2 to_power (n + 1)))) <= ((m * (s . (2 to_power (n + 1)))) + (s . (2 to_power (n + 1))));

          hence thesis by Def1;

        end;

        

         A25: X[ 0 ];

        for m holds X[m] from NAT_1:sch 2( A25, A23);

        then ((( Partial_Sums s) . ((2 to_power (n + 1)) + (2 to_power (n + 1)))) - (( Partial_Sums s) . (2 to_power (n + 1)))) <= ((2 to_power (n + 1)) * (s . (2 to_power (n + 1))));

        then

         A26: ((( Partial_Sums s) . ((2 to_power (n + 1)) + (2 to_power (n + 1)))) - (( Partial_Sums s) . (2 to_power (n + 1)))) <= (s1 . (n + 1)) by A2;

        assume (( Partial_Sums s) . (2 to_power (n + 1))) <= (((( Partial_Sums s1) . n) + (s . 0 )) + (s . 2));

        then ((( Partial_Sums s) . (2 to_power (n + 1))) + (s1 . (n + 1))) <= ((s1 . (n + 1)) + (((( Partial_Sums s1) . n) + (s . 0 )) + (s . 2))) by XREAL_1: 7;

        then ((( Partial_Sums s) . (2 to_power (n + 1))) + (s1 . (n + 1))) <= ((((( Partial_Sums s1) . n) + (s1 . (n + 1))) + (s . 0 )) + (s . 2));

        then

         A27: ((( Partial_Sums s) . (2 to_power (n + 1))) + (s1 . (n + 1))) <= (((( Partial_Sums s1) . (n + 1)) + (s . 0 )) + (s . 2)) by Def1;

        ((2 to_power (n + 1)) + (2 to_power (n + 1))) = (2 * (2 to_power (n + 1)))

        .= ((2 to_power 1) * (2 to_power (n + 1)))

        .= (2 to_power ((n + 1) + 1)) by POWER: 27;

        then (((( Partial_Sums s) . (2 to_power ((n + 1) + 1))) - (( Partial_Sums s) . (2 to_power (n + 1)))) + (( Partial_Sums s) . (2 to_power (n + 1)))) <= ((( Partial_Sums s) . (2 to_power (n + 1))) + (s1 . (n + 1))) by A26, XREAL_1: 7;

        hence thesis by A27, XXREAL_0: 2;

      end;

      (((( Partial_Sums s1) . 0 ) + (s . 0 )) + (s . 2)) = (((s1 . 0 ) + (s . 0 )) + (s . 2)) by Def1

      .= ((((2 to_power 0 ) * (s . (2 to_power 0 ))) + (s . 0 )) + (s . 2)) by A2

      .= (((s . 0 ) + (s . 1)) + (s . 2)) by A21;

      then

       A28: Y[ 0 ] by A3;

      

       A29: for n holds Y[n] from NAT_1:sch 2( A28, A22);

      

       A30: ( Partial_Sums s) is non-decreasing by A2, Th16;

      now

        let n;

        (( Partial_Sums s1) . n) < r by A20;

        then

         A31: ((( Partial_Sums s1) . n) + ((s . 0 ) + (s . 2))) < (r + ((s . 0 ) + (s . 2))) by XREAL_1: 6;

        ((1 + 1) to_power n) >= (1 + (n * 1)) & (1 + n) >= n by NAT_1: 11, POWER: 49;

        then (2 to_power n) >= n by XXREAL_0: 2;

        then ((2 to_power n) + (2 to_power n)) >= (n + n) by XREAL_1: 7;

        then (2 * (2 to_power n)) >= (n + n);

        then ((2 to_power 1) * (2 to_power n)) >= (n + n);

        then

         A32: (2 to_power (n + 1)) >= (n + n) by POWER: 27;

        (n + n) >= n by NAT_1: 11;

        then (2 to_power (n + 1)) >= n by A32, XXREAL_0: 2;

        then

         A33: (( Partial_Sums s) . (2 to_power (n + 1))) >= (( Partial_Sums s) . n) by A30, SEQM_3: 6;

        (( Partial_Sums s) . (2 to_power (n + 1))) <= (((( Partial_Sums s1) . n) + (s . 0 )) + (s . 2)) by A29;

        then (( Partial_Sums s) . n) <= (((( Partial_Sums s1) . n) + (s . 0 )) + (s . 2)) by A33, XXREAL_0: 2;

        hence (( Partial_Sums s) . n) < (r + ((s . 0 ) + (s . 2))) by A31, XXREAL_0: 2;

      end;

      then ( Partial_Sums s) is bounded_above by SEQ_2:def 3;

      hence thesis by A2, Th17;

    end;

    

     Lm2: 1 in REAL by XREAL_0:def 1;

    theorem :: SERIES_1:32

    p > 1 & (for n st n >= 1 holds (s . n) = (1 / (n to_power p))) implies s is summable

    proof

      assume that

       A1: p > 1 and

       A2: for n st n >= 1 holds (s . n) = (1 / (n to_power p));

      defpred X[ Nat, Real] means ($1 = 0 & $2 = 1) or ($1 >= 1 & $2 = (1 / ($1 to_power p)));

      

       A3: for n be Element of NAT holds ex r be Element of REAL st X[n, r]

      proof

        let n be Element of NAT ;

        

         A4: n <> 0 implies n >= ( 0 + 1) by NAT_1: 13;

        per cases ;

          suppose

           A5: n = 0 ;

          reconsider jj = 1 as Real;

          take jj;

          thus thesis by A5, Lm2;

        end;

          suppose

           A6: n > 0 ;

          reconsider n1 = (1 / (n to_power p)) as Element of REAL by XREAL_0:def 1;

          take n1;

          thus thesis by A6, A4;

        end;

      end;

      consider s1 such that

       A7: for n be Element of NAT holds X[n, (s1 . n)] from FUNCT_2:sch 3( A3);

      deffunc V( Nat) = ((2 to_power $1) * (s1 . (2 to_power $1)));

      consider s2 such that

       A8: for n holds (s2 . n) = V(n) from SEQ_1:sch 1;

      

       A9: (s1 . 0 ) = 1 by A7;

      now

        let n;

        now

          per cases by NAT_1: 6;

            suppose

             A10: n = 0 ;

            then ((n + 1) #R p) >= 1 by A1, PREPOWER: 85;

            then

             A11: ((n + 1) to_power p) >= 1 by POWER:def 2;

            (s1 . (n + 1)) = (1 / ((n + 1) to_power p)) by A7;

            hence (s1 . (n + 1)) <= (s1 . n) by A9, A10, A11, XREAL_1: 211;

          end;

            suppose

             A12: ex m be Nat st n = (m + 1);

            

             A13: n in NAT by ORDINAL1:def 12;

            (n to_power p) > 0 by POWER: 34, A12;

            then (1 / (n to_power p)) > 0 ;

            then

             A14: (s1 . n) > 0 by A7, A13;

            

             A15: (n / (n + 1)) <= 1 by NAT_1: 11, XREAL_1: 183;

            

             A16: (n / (n + 1)) > 0 by A12;

            ((s1 . (n + 1)) / (s1 . n)) = ((1 / ((n + 1) to_power p)) / (s1 . n)) by A7

            .= ((1 / ((n + 1) to_power p)) / (1 / (n to_power p))) by A7, A12

            .= ((1 / ((n + 1) to_power p)) * (n to_power p))

            .= ((n to_power p) / ((n + 1) to_power p))

            .= ((n / (n + 1)) to_power p) by A12, POWER: 31

            .= ((n / (n + 1)) #R p) by A16, POWER:def 2;

            then ((s1 . (n + 1)) / (s1 . n)) <= ((n / (n + 1)) #R 0 ) by A1, A16, A15, PREPOWER: 84;

            then ((s1 . (n + 1)) / (s1 . n)) <= 1 by A12, PREPOWER: 71;

            hence (s1 . (n + 1)) <= (s1 . n) by A14, XREAL_1: 187;

          end;

        end;

        hence (s1 . (n + 1)) <= (s1 . n);

      end;

      then

       A17: s1 is non-increasing;

       A18:

      now

        let n;

        assume n >= 0 ;

        

         A19: (n + 1) >= ( 0 + 1) by XREAL_1: 6;

        ((s ^\ 1) . n) = (s . (n + 1)) by NAT_1:def 3

        .= (1 / ((n + 1) to_power p)) by A2, A19

        .= (s1 . (n + 1)) by A7

        .= ((s1 ^\ 1) . n) by NAT_1:def 3;

        hence ((s1 ^\ 1) . n) >= ((s ^\ 1) . n);

      end;

      deffunc U( Nat) = ($1 -root (s2 . $1));

      consider s3 such that

       A20: for n holds (s3 . n) = U(n) from SEQ_1:sch 1;

       A21:

      now

        let n;

        

         A22: (2 to_power n) > 0 by POWER: 34;

        

        thus

         A23: (s2 . n) = ((2 to_power n) * (s1 . (2 to_power n))) by A8

        .= ((2 to_power n) * (1 / ((2 to_power n) to_power p))) by A7, A22

        .= ((2 to_power n) * (1 / (2 to_power (n * p)))) by POWER: 33

        .= ((2 to_power n) * (2 to_power ( - (n * p)))) by POWER: 28

        .= (2 to_power (n + ( - (n * p)))) by POWER: 27

        .= (2 to_power ((1 - p) * n));

        hence (s2 . n) >= 0 by POWER: 34;

        (s2 . n) = ((2 to_power (1 - p)) to_power n) by A23, POWER: 33;

        hence (s3 . n) = (n -root ((2 to_power (1 - p)) to_power n)) by A20;

      end;

      

       A0: (2 to_power (1 - p)) is set by TARSKI: 1;

       A24:

      now

        let n be Nat;

        

         A25: (n + 1) >= ( 0 + 1) & (2 to_power (1 - p)) >= 0 by POWER: 34, XREAL_1: 6;

        

        thus ((s3 ^\ 1) . n) = (s3 . (n + 1)) by NAT_1:def 3

        .= ((n + 1) -root ((2 to_power (1 - p)) to_power (n + 1))) by A21

        .= (2 to_power (1 - p)) by A25, POWER: 4;

      end;

      then

       A26: (s3 ^\ 1) is constant by A0;

      

      then ( lim (s3 ^\ 1)) = ((s3 ^\ 1) . 0 ) by SEQ_4: 26

      .= (2 to_power (1 - p)) by A24;

      then

       A27: ( lim s3) = (2 to_power (1 - p)) by A26, SEQ_4: 22;

       A28:

      now

        let n;

        now

          per cases by NAT_1: 6;

            suppose n = 0 ;

            hence (s1 . n) >= 0 by A7;

          end;

            suppose

             A29: ex m be Nat st n = (m + 1);

            

             A30: n in NAT by ORDINAL1:def 12;

            (n to_power p) > 0 by POWER: 34, A29;

            then (1 / (n to_power p)) >= 0 ;

            hence (s1 . n) >= 0 by A7, A30;

          end;

        end;

        hence (s1 . n) >= 0 & (s2 . n) = ((2 to_power n) * (s1 . (2 to_power n))) by A8;

      end;

       A31:

      now

        let n;

        

         A32: (n + 1) >= ( 0 + 1) by XREAL_1: 6;

        

         A33: (s1 . (n + 1)) >= 0 by A28;

        ((s ^\ 1) . n) = (s . (n + 1)) by NAT_1:def 3

        .= (1 / ((n + 1) to_power p)) by A2, A32

        .= (s1 . (n + 1)) by A7

        .= ((s1 ^\ 1) . n) by NAT_1:def 3;

        hence ((s ^\ 1) . n) >= 0 by A33, NAT_1:def 3;

      end;

      

       A34: s3 is convergent by A26, SEQ_4: 21;

      (1 - p) < 0 by A1, XREAL_1: 49;

      then ( lim s3) < 1 by A27, POWER: 36;

      then s2 is summable by A20, A21, A34, Th28;

      then s1 is summable by A17, A28, Th31;

      then (s1 ^\ 1) is summable by Th12;

      then (s ^\ 1) is summable by A31, A18, Th19;

      hence thesis by Th13;

    end;

    ::$Notion-Name

    theorem :: SERIES_1:33

    p <= 1 & (for n st n >= 1 holds (s . n) = (1 / (n to_power p))) implies not s is summable

    proof

      assume that

       A1: p <= 1 and

       A2: for n st n >= 1 holds (s . n) = (1 / (n to_power p));

      per cases ;

        suppose

         A3: p < 0 ;

        now

          assume s is convergent & ( lim s) = 0 ;

          then

          consider m such that

           A4: for n st n >= m holds |.((s . n) - 0 ).| < 1 by SEQ_2:def 7;

          consider k such that

           A5: k > m by SEQ_4: 3;

          now

            let n such that

             A6: n >= k;

            

             A7: n > 0 by A5, A6;

            then

             A8: n >= ( 0 + 1) by NAT_1: 13;

            n >= m by A5, A6, XXREAL_0: 2;

            then |.((s . n) - 0 ).| < 1 by A4;

            then |.(1 / (n to_power p)).| < 1 by A2, A8;

            then |.(n to_power ( - p)).| < 1 by A7, POWER: 28;

            then

             A9: (n to_power ( - p)) < 1 by ABSVALUE:def 1;

            (n #R ( - p)) >= 1 by A3, A8, PREPOWER: 85;

            hence contradiction by A7, A9, POWER:def 2;

          end;

          hence contradiction;

        end;

        hence thesis by Th4;

      end;

        suppose

         A10: p >= 0 ;

        defpred X[ Element of NAT , Real] means ($1 = 0 & $2 = 1) or ($1 >= 1 & $2 = (1 / ($1 to_power p)));

        

         A11: for n be Element of NAT holds ex r be Element of REAL st X[n, r]

        proof

          let n be Element of NAT ;

          

           A12: n <> 0 implies n >= ( 0 + 1) by NAT_1: 13;

          per cases ;

            suppose

             A13: n = 0 ;

            reconsider jj = 1 as Real;

            take jj;

            thus thesis by A13, Lm2;

          end;

            suppose

             A14: n > 0 ;

            reconsider n1 = (1 / (n to_power p)) as Element of REAL by XREAL_0:def 1;

            take n1;

            thus thesis by A14, A12;

          end;

        end;

        consider s1 such that

         A15: for n be Element of NAT holds X[n, (s1 . n)] from FUNCT_2:sch 3( A11);

        

         A16: (s1 . 0 ) = 1 by A15;

        now

          let n;

          now

            per cases by NAT_1: 6;

              suppose

               A17: n = 0 ;

              then ((n + 1) #R p) >= 1 by A10, PREPOWER: 85;

              then

               A18: ((n + 1) to_power p) >= 1 by POWER:def 2;

              (s1 . (n + 1)) = (1 / ((n + 1) to_power p)) by A15;

              hence (s1 . (n + 1)) <= (s1 . n) by A16, A17, A18, XREAL_1: 211;

            end;

              suppose

               A19: ex m be Nat st n = (m + 1);

              

               A20: n in NAT by ORDINAL1:def 12;

              (n to_power p) > 0 by POWER: 34, A19;

              then (1 / (n to_power p)) > 0 ;

              then

               A21: (s1 . n) > 0 by A15, A20;

              

               A22: (n / (n + 1)) <= 1 by NAT_1: 11, XREAL_1: 183;

              

               A23: (n / (n + 1)) > 0 by A19;

              ((s1 . (n + 1)) / (s1 . n)) = ((1 / ((n + 1) to_power p)) / (s1 . n)) by A15

              .= ((1 / ((n + 1) to_power p)) / (1 / (n to_power p))) by A15, A19

              .= ((1 / ((n + 1) to_power p)) * (n to_power p))

              .= ((n to_power p) / ((n + 1) to_power p))

              .= ((n / (n + 1)) to_power p) by A19, POWER: 31

              .= ((n / (n + 1)) #R p) by A23, POWER:def 2;

              then ((s1 . (n + 1)) / (s1 . n)) <= ((n / (n + 1)) #R 0 ) by A10, A23, A22, PREPOWER: 84;

              then ((s1 . (n + 1)) / (s1 . n)) <= 1 by A19, PREPOWER: 71;

              hence (s1 . (n + 1)) <= (s1 . n) by A21, XREAL_1: 187;

            end;

          end;

          hence (s1 . (n + 1)) <= (s1 . n);

        end;

        then

         A24: s1 is non-increasing;

         A25:

        now

          let n;

          

           A26: n in NAT by ORDINAL1:def 12;

          assume

           A27: n >= 1;

          

          then (s . n) = (1 / (n to_power p)) by A2

          .= (s1 . n) by A15, A27, A26;

          hence (s . n) >= (s1 . n);

        end;

        deffunc U( Nat) = ((2 to_power $1) * (s1 . (2 to_power $1)));

        consider s2 such that

         A28: for n holds (s2 . n) = U(n) from SEQ_1:sch 1;

         A29:

        now

          let n;

          now

            per cases by NAT_1: 6;

              suppose n = 0 ;

              hence (s1 . n) >= 0 by A15;

            end;

              suppose

               A30: ex m be Nat st n = (m + 1);

              

               A31: n in NAT by ORDINAL1:def 12;

              (n to_power p) > 0 by POWER: 34, A30;

              then (1 / (n to_power p)) >= 0 ;

              hence (s1 . n) >= 0 by A15, A31;

            end;

          end;

          hence (s1 . n) >= 0 & (s2 . n) = ((2 to_power n) * (s1 . (2 to_power n))) by A28;

        end;

        now

          assume s2 is convergent & ( lim s2) = 0 ;

          then

          consider m such that

           A32: for n st n >= m holds |.((s2 . n) - 0 ).| < (1 / 2) by SEQ_2:def 7;

          now

            let n;

            assume n >= m;

            then |.((s2 . n) - 0 ).| < (1 / 2) by A32;

            then

             A33: |.((2 to_power n) * (s1 . (2 to_power n))).| < (1 / 2) by A28;

            (2 to_power n) >= 1 by PREPOWER: 11;

            then |.((2 to_power n) * (1 / ((2 to_power n) to_power p))).| < (1 / 2) by A15, A33;

            then |.((2 to_power n) * (1 / (2 to_power (n * p)))).| < (1 / 2) by POWER: 33;

            then |.((2 to_power n) * (2 to_power ( - (n * p)))).| < (1 / 2) by POWER: 28;

            then |.(2 to_power (n + ( - (n * p)))).| < (1 / 2) by POWER: 27;

            then (2 to_power (n - (n * p))) < (1 / 2) by ABSVALUE:def 1;

            then ((2 to_power (n - (n * p))) * 2) < ((1 / 2) * 2) by XREAL_1: 68;

            then ((2 to_power (n - (n * p))) * (2 to_power 1)) < 1;

            then

             A34: (2 to_power ((n - (n * p)) + 1)) < 1 by POWER: 27;

            (1 - p) >= 0 by A1, XREAL_1: 48;

            then (n * (1 - p)) >= 0 ;

            then (2 #R ((n - (n * p)) + 1)) >= 1 by PREPOWER: 85;

            hence contradiction by A34, POWER:def 2;

          end;

          hence contradiction;

        end;

        then not s2 is summable by Th4;

        then not s1 is summable by A24, A29, Th31;

        hence thesis by A29, A25, Th19;

      end;

    end;

    definition

      let s;

      :: SERIES_1:def4

      attr s is absolutely_summable means ( abs s) is summable;

    end

    theorem :: SERIES_1:34

    

     Th34: for n, m st n <= m holds |.((( Partial_Sums s) . m) - (( Partial_Sums s) . n)).| <= |.((( Partial_Sums |.s.|) . m) - (( Partial_Sums |.s.|) . n)).|

    proof

      let n, m such that

       A1: n <= m;

      reconsider u = n, v = m as Integer;

      set s2 = ( Partial_Sums ( abs s));

      set s1 = ( Partial_Sums s);

      defpred X[ Nat] means |.((s1 . (n + $1)) - (s1 . n)).| <= |.((s2 . (n + $1)) - (s2 . n)).|;

      now

        let k;

         |.(s . k).| >= 0 by COMPLEX1: 46;

        hence (( abs s) . k) >= 0 by SEQ_1: 12;

      end;

      then

       A2: s2 is non-decreasing by Th16;

      

       A3: for k st X[k] holds X[(k + 1)]

      proof

        let k;

        

         A4: |.(s . ((n + k) + 1)).| >= 0 by COMPLEX1: 46;

        assume |.((s1 . (n + k)) - (s1 . n)).| <= |.((s2 . (n + k)) - (s2 . n)).|;

        then

         A5: ( |.(s . ((n + k) + 1)).| + |.((s1 . (n + k)) - (s1 . n)).|) <= ( |.(s . ((n + k) + 1)).| + |.((s2 . (n + k)) - (s2 . n)).|) by XREAL_1: 7;

        

         A6: |.((s2 . (n + (k + 1))) - (s2 . n)).| = |.(((s2 . (n + k)) + (( abs s) . ((n + k) + 1))) - (s2 . n)).| by Def1

        .= |.(( |.(s . ((n + k) + 1)).| + (s2 . (n + k))) - (s2 . n)).| by SEQ_1: 12

        .= |.( |.(s . ((n + k) + 1)).| + ((s2 . (n + k)) - (s2 . n))).|;

        (s2 . (n + k)) >= (s2 . n) by A2, SEQM_3: 5;

        then

         A7: ((s2 . (n + k)) - (s2 . n)) >= 0 by XREAL_1: 48;

         |.((s1 . (n + (k + 1))) - (s1 . n)).| = |.(((s . ((n + k) + 1)) + (s1 . (n + k))) - (s1 . n)).| by Def1

        .= |.((s . ((n + k) + 1)) + ((s1 . (n + k)) - (s1 . n))).|;

        then |.((s1 . (n + (k + 1))) - (s1 . n)).| <= ( |.(s . ((n + k) + 1)).| + |.((s1 . (n + k)) - (s1 . n)).|) by COMPLEX1: 56;

        then |.((s1 . (n + (k + 1))) - (s1 . n)).| <= ( |.(s . ((n + k) + 1)).| + |.((s2 . (n + k)) - (s2 . n)).|) by A5, XXREAL_0: 2;

        then |.((s1 . (n + (k + 1))) - (s1 . n)).| <= ( |.(s . ((n + k) + 1)).| + ((s2 . (n + k)) - (s2 . n))) by A7, ABSVALUE:def 1;

        hence thesis by A7, A4, A6, ABSVALUE:def 1;

      end;

      reconsider k = (v - u) as Element of NAT by A1, INT_1: 5;

      

       A8: (n + k) = m;

      

       A9: X[ 0 ];

      for k holds X[k] from NAT_1:sch 2( A9, A3);

      hence thesis by A8;

    end;

    registration

      cluster absolutely_summable -> summable for Real_Sequence;

      coherence

      proof

        let s be Real_Sequence;

        assume s is absolutely_summable;

        then

         A1: ( abs s) is summable;

        now

          let r;

          assume 0 < r;

          then

          consider n such that

           A2: for m st n <= m holds |.((( Partial_Sums ( abs s)) . m) - (( Partial_Sums ( abs s)) . n)).| < r by A1, Th21;

          take n;

          let m;

          assume

           A3: n <= m;

          then

           A4: |.((( Partial_Sums s) . m) - (( Partial_Sums s) . n)).| <= |.((( Partial_Sums ( abs s)) . m) - (( Partial_Sums ( abs s)) . n)).| by Th34;

           |.((( Partial_Sums ( abs s)) . m) - (( Partial_Sums ( abs s)) . n)).| < r by A2, A3;

          hence |.((( Partial_Sums s) . m) - (( Partial_Sums s) . n)).| < r by A4, XXREAL_0: 2;

        end;

        hence thesis by Th21;

      end;

    end

    theorem :: SERIES_1:35

    s is absolutely_summable implies s is summable;

    theorem :: SERIES_1:36

    (for n holds 0 <= (s . n)) & s is summable implies s is absolutely_summable

    proof

      assume that

       A1: for n holds 0 <= (s . n) and

       A2: s is summable;

      

       A3: for n holds (s . n) = |.(s . n).| by A1, ABSVALUE:def 1;

      ( Partial_Sums s) is convergent by A2;

      then ( Partial_Sums ( abs s)) is convergent by A3, SEQ_1: 12;

      then ( abs s) is summable;

      hence thesis;

    end;

    theorem :: SERIES_1:37

    (for n holds (s . n) <> 0 & (s1 . n) = ((( abs s) . (n + 1)) / (( abs s) . n))) & s1 is convergent & ( lim s1) < 1 implies s is absolutely_summable

    proof

      assume that

       A1: for n holds (s . n) <> 0 & (s1 . n) = ((( abs s) . (n + 1)) / (( abs s) . n)) and

       A2: s1 is convergent & ( lim s1) < 1;

      now

        let n;

        (( abs s) . n) = |.(s . n).| & (s . n) <> 0 by A1, SEQ_1: 12;

        hence (( abs s) . n) > 0 by COMPLEX1: 47;

        thus (s1 . n) = ((( abs s) . (n + 1)) / (( abs s) . n)) by A1;

      end;

      then ( abs s) is summable by A2, Th26;

      hence thesis;

    end;

    theorem :: SERIES_1:38

    

     Th38: r > 0 & (ex m st for n st n >= m holds |.(s . n).| >= r) implies not s is convergent or ( lim s) <> 0

    proof

      assume

       A1: r > 0 ;

      given m such that

       A2: for n st n >= m holds |.(s . n).| >= r;

      now

        per cases ;

          suppose not s is convergent;

          hence thesis;

        end;

          suppose

           A3: s is convergent;

          now

            assume ( lim s) = 0 ;

            then

            consider k such that

             A4: for n st n >= k holds |.((s . n) - 0 ).| < r by A1, A3, SEQ_2:def 7;

            now

              let n such that

               A5: n >= (m + k);

              (m + k) >= k by NAT_1: 11;

              then n >= k by A5, XXREAL_0: 2;

              then

               A6: |.((s . n) - 0 ).| < r by A4;

              (m + k) >= m by NAT_1: 11;

              then n >= m by A5, XXREAL_0: 2;

              hence contradiction by A2, A6;

            end;

            hence contradiction;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: SERIES_1:39

    (for n holds (s . n) <> 0 ) & (ex m st for n st n >= m holds ((( abs s) . (n + 1)) / (( abs s) . n)) >= 1) implies not s is summable

    proof

      assume

       A1: for n holds (s . n) <> 0 ;

      given m such that

       A2: for n st n >= m holds ((( abs s) . (n + 1)) / (( abs s) . n)) >= 1;

       A3:

      now

        defpred X[ Nat] means |.(s . (m + $1)).| >= |.(s . m).|;

        

         A4: for k st X[k] holds X[(k + 1)]

        proof

          let k such that

           A5: |.(s . (m + k)).| >= |.(s . m).|;

          ((( abs s) . ((m + k) + 1)) / (( abs s) . (m + k))) >= 1 by A2, NAT_1: 11;

          then ( |.(s . ((m + k) + 1)).| / (( abs s) . (m + k))) >= 1 by SEQ_1: 12;

          then

           A6: ( |.(s . ((m + k) + 1)).| / |.(s . (m + k)).|) >= 1 by SEQ_1: 12;

          (s . (m + k)) <> 0 by A1;

          then |.(s . (m + k)).| > 0 by COMPLEX1: 47;

          then |.(s . ((m + k) + 1)).| >= |.(s . (m + k)).| by A6, XREAL_1: 191;

          hence thesis by A5, XXREAL_0: 2;

        end;

        let n;

        assume n >= m;

        then

        consider k be Nat such that

         A7: n = (m + k) by NAT_1: 10;

        reconsider k as Element of NAT by ORDINAL1:def 12;

        

         A8: n = (m + k) by A7;

        

         A9: X[ 0 ];

        for k holds X[k] from NAT_1:sch 2( A9, A4);

        hence |.(s . n).| >= |.(s . m).| by A8;

      end;

      (s . m) <> 0 by A1;

      then |.(s . m).| > 0 by COMPLEX1: 47;

      then not s is convergent or ( lim s) <> 0 by A3, Th38;

      hence thesis by Th4;

    end;

    theorem :: SERIES_1:40

    (for n holds (s1 . n) = (n -root (( abs s) . n))) & s1 is convergent & ( lim s1) < 1 implies s is absolutely_summable

    proof

      assume that

       A1: for n holds (s1 . n) = (n -root (( abs s) . n)) and

       A2: s1 is convergent & ( lim s1) < 1;

      now

        let n;

        (( abs s) . n) = |.(s . n).| by SEQ_1: 12;

        hence (( abs s) . n) >= 0 by COMPLEX1: 46;

        thus (s1 . n) = (n -root (( abs s) . n)) by A1;

      end;

      then ( abs s) is summable by A2, Th28;

      hence thesis;

    end;

    theorem :: SERIES_1:41

    (for n holds (s1 . n) = (n -root (( abs s) . n))) & (ex m st for n st m <= n holds (s1 . n) >= 1) implies not s is summable

    proof

      assume

       A1: for n holds (s1 . n) = (n -root (( abs s) . n));

      given m such that

       A2: for n st m <= n holds (s1 . n) >= 1;

      now

        let n such that

         A3: n >= (m + 1);

        (m + 1) >= 1 by NAT_1: 11;

        then

         A4: n >= 1 by A3, XXREAL_0: 2;

        (m + 1) >= m by NAT_1: 11;

        then

         A5: n >= m by A3, XXREAL_0: 2;

        (s1 . n) = (n -root (( abs s) . n)) by A1

        .= (n -root |.(s . n).|) by SEQ_1: 12;

        then |.(s . n).| >= 0 & ((n -root |.(s . n).|) |^ n) >= 1 by A2, A5, COMPLEX1: 46, PREPOWER: 11;

        hence |.(s . n).| >= 1 by A4, POWER: 4;

      end;

      then not s is convergent or ( lim s) <> 0 by Th38;

      hence thesis by Th4;

    end;

    theorem :: SERIES_1:42

    (for n holds (s1 . n) = (n -root (( abs s) . n))) & s1 is convergent & ( lim s1) > 1 implies not s is summable

    proof

      assume that

       A1: for n holds (s1 . n) = (n -root (( abs s) . n)) and

       A2: s1 is convergent and

       A3: ( lim s1) > 1;

      (( lim s1) - 1) > 0 by A3, XREAL_1: 50;

      then

      consider m such that

       A4: for n st n >= m holds |.((s1 . n) - ( lim s1)).| < (( lim s1) - 1) by A2, SEQ_2:def 7;

      now

        let n such that

         A5: n >= (m + 1);

        

         A6: (s1 . n) = (n -root (( abs s) . n)) by A1

        .= (n -root |.(s . n).|) by SEQ_1: 12;

        (m + 1) >= m by NAT_1: 11;

        then n >= m by A5, XXREAL_0: 2;

        then |.((n -root |.(s . n).|) - ( lim s1)).| < (( lim s1) - 1) by A4, A6;

        then ( - (( lim s1) - 1)) < ((n -root |.(s . n).|) - ( lim s1)) by SEQ_2: 1;

        then ((1 - ( lim s1)) + ( lim s1)) < (((n -root |.(s . n).|) - ( lim s1)) + ( lim s1)) by XREAL_1: 6;

        then

         A7: |.(s . n).| >= 0 & ((n -root |.(s . n).|) |^ n) >= 1 by COMPLEX1: 46, PREPOWER: 11;

        (m + 1) >= 1 by NAT_1: 11;

        then n >= 1 by A5, XXREAL_0: 2;

        hence |.(s . n).| >= 1 by A7, POWER: 4;

      end;

      then not s is convergent or ( lim s) <> 0 by Th38;

      hence thesis by Th4;

    end;

    begin

    definition

      let s;

      let n be Nat;

      :: SERIES_1:def5

      func Sum (s,n) -> Real equals (( Partial_Sums s) . n);

      coherence ;

    end

    definition

      let s;

      let n,m be Nat;

      :: SERIES_1:def6

      func Sum (s,n,m) -> Real equals (( Sum (s,n)) - ( Sum (s,m)));

      coherence ;

    end