prepower.miz



    begin

    registration

      let i be Integer;

      cluster |.i.| -> natural;

      coherence ;

    end

    reserve x for set;

    reserve a,b,c for Real;

    reserve m,n,m1,m2 for Nat;

    reserve k,l for Integer;

    reserve p,q for Rational;

    reserve s1,s2 for Real_Sequence;

    theorem :: PREPOWER:1

    

     Th1: s1 is convergent & (for n holds (s1 . n) >= a) implies ( lim s1) >= a

    proof

      assume that

       A1: s1 is convergent and

       A2: for n holds (s1 . n) >= a;

      set s = ( seq_const a);

       A3:

      now

        let n;

        (s1 . n) >= a by A2;

        hence (s1 . n) >= (s . n) by SEQ_1: 57;

      end;

      ( lim s) = (s . 0 ) by SEQ_4: 26

      .= a by SEQ_1: 57;

      hence thesis by A1, A3, SEQ_2: 18;

    end;

    theorem :: PREPOWER:2

    

     Th2: s1 is convergent & (for n holds (s1 . n) <= a) implies ( lim s1) <= a

    proof

      assume that

       A1: s1 is convergent and

       A2: for n holds (s1 . n) <= a;

      set s = ( seq_const a);

       A3:

      now

        let n;

        (s1 . n) <= a by A2;

        hence (s1 . n) <= (s . n) by SEQ_1: 57;

      end;

      ( lim s) = (s . 0 ) by SEQ_4: 26

      .= a by SEQ_1: 57;

      hence thesis by A1, A3, SEQ_2: 18;

    end;

    definition

      let a be Real;

      :: PREPOWER:def1

      func a GeoSeq -> Real_Sequence means

      : Def1: for m holds (it . m) = (a |^ m);

      existence

      proof

        reconsider a as Real;

        deffunc F( Nat) = ( In ((a |^ $1), REAL ));

        consider f be Real_Sequence such that

         A1: for m be Element of NAT holds (f . m) = F(m) from FUNCT_2:sch 4;

        take f;

        let m;

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

        (f . m) = F(m) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let s1, s2 such that

         A2: for n holds (s1 . n) = (a |^ n) and

         A3: for n holds (s2 . n) = (a |^ n);

        for n be Element of NAT holds (s1 . n) = (s2 . n)

        proof

          let n be Element of NAT ;

          

          thus (s1 . n) = (a |^ n) by A2

          .= (s2 . n) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: PREPOWER:3

    

     Th3: s1 = (a GeoSeq ) iff (s1 . 0 ) = 1 & for m holds (s1 . (m + 1)) = ((s1 . m) * a)

    proof

      defpred P[ Nat] means (s1 . $1) = ((a GeoSeq ) . $1);

      hereby

        assume

         A1: s1 = (a GeoSeq );

        

        hence (s1 . 0 ) = (a |^ 0 ) by Def1

        .= 1 by NEWTON: 4;

        let m;

        

        thus (s1 . (m + 1)) = (a |^ (m + 1)) by A1, Def1

        .= ((a |^ m) * a) by NEWTON: 6

        .= ((s1 . m) * a) by A1, Def1;

      end;

      assume that

       A2: (s1 . 0 ) = 1 and

       A3: for m holds (s1 . (m + 1)) = ((s1 . m) * a);

      

       A4: for m st P[m] holds P[(m + 1)]

      proof

        let m such that

         A5: (s1 . m) = ((a GeoSeq ) . m);

        

        thus (s1 . (m + 1)) = ((s1 . m) * a) by A3

        .= ((a |^ m) * a) by A5, Def1

        .= (a |^ (m + 1)) by NEWTON: 6

        .= ((a GeoSeq ) . (m + 1)) by Def1;

      end;

      (s1 . 0 ) = (a |^ 0 ) by A2, NEWTON: 4

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

      then

       A6: P[ 0 ];

      for m holds P[m] from NAT_1:sch 2( A6, A4);

      then for m be Element of NAT holds P[m];

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: PREPOWER:4

    for a st a <> 0 holds for m holds ((a GeoSeq ) . m) <> 0

    proof

      let a such that

       A1: a <> 0 ;

      defpred P[ Nat] means ((a GeoSeq ) . $1) <> 0 ;

      

       A2: for n holds P[n] implies P[(n + 1)]

      proof

        let n such that

         A3: ((a GeoSeq ) . n) <> 0 ;

        ((a GeoSeq ) . (n + 1)) = (((a GeoSeq ) . n) * a) by Th3;

        hence thesis by A1, A3;

      end;

      

       A4: P[ 0 ] by Th3;

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

    end;

    theorem :: PREPOWER:5

    

     Th5: for a be Complex holds for n be natural Number holds 0 <> a implies 0 <> (a |^ n)

    proof

      let a be Complex;

      let n be natural Number;

      

       A1: n is Nat by TARSKI: 1;

      defpred P[ Nat] means (a |^ $1) <> 0 ;

      assume

       A2: 0 <> a;

      

       A3: for m be Nat st P[m] holds P[(m + 1)]

      proof

        let m be Nat;

        assume (a |^ m) <> 0 ;

        then ((a |^ m) * a) <> 0 by A2;

        hence thesis by NEWTON: 6;

      end;

      

       A4: P[ 0 ] by NEWTON: 4;

      for m be Nat holds P[m] from NAT_1:sch 2( A4, A3);

      hence thesis by A1;

    end;

    theorem :: PREPOWER:6

    

     Th6: for n be natural Number holds 0 < a implies 0 < (a |^ n)

    proof

      let n be natural Number;

      

       A1: n is Nat by TARSKI: 1;

      defpred P[ Nat] means 0 < (a |^ $1);

      assume

       A2: 0 < a;

      

       A3: for m be Nat st P[m] holds P[(m + 1)]

      proof

        let m be Nat;

        assume (a |^ m) > 0 ;

        then ((a |^ m) * a) > ( 0 * a) by A2;

        hence thesis by NEWTON: 6;

      end;

      

       A4: P[ 0 ] by NEWTON: 4;

      for m be Nat holds P[m] from NAT_1:sch 2( A4, A3);

      hence thesis by A1;

    end;

    theorem :: PREPOWER:7

    

     Th7: for a be Complex, n be natural Number holds ((1 / a) |^ n) = (1 / (a |^ n))

    proof

      let a be Complex;

      let n be natural Number;

      

       A1: n is Nat by TARSKI: 1;

      defpred P[ Nat] means ((1 / a) |^ $1) = (1 / (a |^ $1));

      

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

      proof

        let m be Nat;

        assume ((1 / a) |^ m) = (1 / (a |^ m));

        

        hence ((1 / a) |^ (m + 1)) = ((1 / (a |^ m)) * (1 / a)) by NEWTON: 6

        .= ((1 * 1) / ((a |^ m) * a)) by XCMPLX_1: 76

        .= (1 / (a |^ (m + 1))) by NEWTON: 6;

      end;

      ((1 / a) |^ 0 ) = 1 by NEWTON: 4

      .= (1 / 1)

      .= (1 / (a |^ 0 )) by NEWTON: 4;

      then

       A3: P[ 0 ];

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

      hence thesis by A1;

    end;

    theorem :: PREPOWER:8

    for a,b be Complex holds for n be natural Number holds ((b / a) |^ n) = ((b |^ n) / (a |^ n))

    proof

      let a,b be Complex;

      let n be natural Number;

      

      thus ((b / a) |^ n) = ((b * (a " )) |^ n)

      .= ((b |^ n) * ((a " ) |^ n)) by NEWTON: 7

      .= ((b |^ n) * ((1 / a) |^ n))

      .= ((b |^ n) * (1 / (a |^ n))) by Th7

      .= (((b |^ n) * 1) / (a |^ n))

      .= ((b |^ n) / (a |^ n));

    end;

    theorem :: PREPOWER:9

    

     Th9: for n be natural Number st 0 < a & a <= b holds (a |^ n) <= (b |^ n)

    proof

      let n be natural Number;

      

       A1: n is Nat by TARSKI: 1;

      assume that

       A2: 0 < a and

       A3: a <= b;

      defpred P[ Nat] means (a |^ $1) <= (b |^ $1);

      

       A4: for m1 be Nat st P[m1] holds P[(m1 + 1)]

      proof

        let m1 be Nat such that

         A5: (a |^ m1) <= (b |^ m1);

        (a |^ m1) > 0 by A2, Th6;

        then ((a |^ m1) * a) <= ((b |^ m1) * b) by A2, A3, A5, XREAL_1: 66;

        then (a |^ (m1 + 1)) <= ((b |^ m1) * b) by NEWTON: 6;

        hence thesis by NEWTON: 6;

      end;

      

       A6: (b |^ 0 ) = ((b GeoSeq ) . 0 ) by Def1

      .= 1 by Th3;

      (a |^ 0 ) = ((a GeoSeq ) . 0 ) by Def1

      .= 1 by Th3;

      then

       A7: P[ 0 ] by A6;

      for m1 be Nat holds P[m1] from NAT_1:sch 2( A7, A4);

      hence thesis by A1;

    end;

    

     Lm1: for n be natural Number holds 0 < a & a < b & 1 <= n implies (a |^ n) < (b |^ n)

    proof

      let n be natural Number;

      assume that

       A1: 0 < a and

       A2: a < b and

       A3: 1 <= n;

      consider m be Nat such that

       A4: n = (1 + m) by A3, NAT_1: 10;

      defpred P[ Nat] means (a |^ (1 + $1)) < (b |^ (1 + $1));

      

       A5: for m1 st P[m1] holds P[(m1 + 1)]

      proof

        let m1;

        assume

         A6: (a |^ (1 + m1)) < (b |^ (1 + m1));

        (a |^ (1 + m1)) > 0 by A1, Th6;

        then ((a |^ (1 + m1)) * a) < ((b |^ (1 + m1)) * b) by A1, A2, A6, XREAL_1: 97;

        then (a |^ ((1 + m1) + 1)) < ((b |^ (1 + m1)) * b) by NEWTON: 6;

        hence thesis by NEWTON: 6;

      end;

      

       A7: P[ 0 ] by A2;

      

       A8: for m1 holds P[m1] from NAT_1:sch 2( A7, A5);

      thus thesis by A4, A8;

    end;

    theorem :: PREPOWER:10

    

     Th10: for n be natural Number st 0 <= a & a < b & 1 <= n holds (a |^ n) < (b |^ n)

    proof

      let n be natural Number;

      assume that

       A1: 0 <= a and

       A2: a < b and

       A3: 1 <= n;

      per cases by A1;

        suppose a > 0 ;

        hence thesis by A2, A3, Lm1;

      end;

        suppose

         A4: a = 0 ;

        reconsider k = n, k1 = 1 as Integer;

        reconsider m = (k - k1) as Element of NAT by A3, INT_1: 5;

        (a |^ n) = (a |^ (m + 1))

        .= ((a |^ m) * (a |^ 1)) by NEWTON: 8

        .= ((a |^ m) * ((a GeoSeq ) . ( 0 + 1))) by Def1

        .= ((a |^ m) * (((a GeoSeq ) . 0 ) * 0 )) by A4, Th3

        .= 0 ;

        hence thesis by A1, A2, Th6;

      end;

    end;

    theorem :: PREPOWER:11

    

     Th11: for n be natural Number holds a >= 1 implies (a |^ n) >= 1

    proof

      let n be natural Number;

      assume a >= 1;

      then (a |^ n) >= (1 |^ n) by Th9;

      hence thesis by NEWTON: 10;

    end;

    theorem :: PREPOWER:12

    

     Th12: for n be natural Number st 1 <= a & 1 <= n holds a <= (a |^ n)

    proof

      let n be natural Number;

      assume that

       A1: 1 <= a and

       A2: 1 <= n;

      consider m be Nat such that

       A3: n = (m + 1) by A2, NAT_1: 6;

      defpred P[ Nat] means a <= (a |^ ($1 + 1));

      

       A4: for m1 st P[m1] holds P[(m1 + 1)]

      proof

        let m1;

        assume a <= (a |^ (m1 + 1));

        then (a * 1) <= ((a |^ (m1 + 1)) * a) by A1, XREAL_1: 66;

        hence thesis by NEWTON: 6;

      end;

      

       A5: P[ 0 ];

      

       A6: for m1 holds P[m1] from NAT_1:sch 2( A5, A4);

      thus thesis by A3, A6;

    end;

    theorem :: PREPOWER:13

    for n be Nat st 1 < a & 2 <= n holds a < (a |^ n)

    proof

      let n be Nat;

      assume that

       A1: 1 < a and

       A2: 2 <= n;

      consider m be Nat such that

       A3: n = (2 + m) by A2, NAT_1: 10;

      defpred P[ Nat] means a < (a |^ (2 + $1));

      

       A4: (a * a) > (a * 1) by A1, XREAL_1: 68;

      

       A5: for m1 st P[m1] holds P[(m1 + 1)]

      proof

        let m1;

        assume a < (a |^ (2 + m1));

        then ((a |^ (2 + m1)) * a) > (a * a) by A1, XREAL_1: 68;

        then (a |^ ((2 + m1) + 1)) > (a * a) by NEWTON: 6;

        hence thesis by A4, XXREAL_0: 2;

      end;

      (a |^ (2 + 0 )) = ((a GeoSeq ) . (1 + 1)) by Def1

      .= (((a GeoSeq ) . ( 0 + 1)) * a) by Th3

      .= ((((a GeoSeq ) . 0 ) * a) * a) by Th3

      .= ((1 * a) * a) by Th3

      .= (a * a);

      then

       A6: P[ 0 ] by A4;

      

       A7: for m1 holds P[m1] from NAT_1:sch 2( A6, A5);

      thus thesis by A3, A7;

    end;

    theorem :: PREPOWER:14

    

     Th14: for n be natural Number st 0 < a & a <= 1 & 1 <= n holds (a |^ n) <= a

    proof

      let n be natural Number;

      assume that

       A1: 0 < a and

       A2: a <= 1 and

       A3: 1 <= n;

      consider m be Nat such that

       A4: n = (1 + m) by A3, NAT_1: 10;

      defpred P[ Nat] means (a |^ (1 + $1)) <= a;

      

       A5: (a * a) <= (a * 1) by A1, A2, XREAL_1: 64;

      

       A6: for m1 st P[m1] holds P[(m1 + 1)]

      proof

        let m1;

        assume (a |^ (1 + m1)) <= a;

        then ((a |^ (1 + m1)) * a) <= (a * a) by A1, XREAL_1: 64;

        then (a |^ (1 + (m1 + 1))) <= (a * a) by NEWTON: 6;

        hence thesis by A5, XXREAL_0: 2;

      end;

      

       A7: P[ 0 ];

      

       A8: for m1 holds P[m1] from NAT_1:sch 2( A7, A6);

      thus thesis by A4, A8;

    end;

    theorem :: PREPOWER:15

    for n be Nat st 0 < a & a < 1 & 2 <= n holds (a |^ n) < a

    proof

      let n be Nat;

      assume that

       A1: 0 < a and

       A2: a < 1 and

       A3: 2 <= n;

      consider m be Nat such that

       A4: n = (2 + m) by A3, NAT_1: 10;

      defpred P[ Nat] means (a |^ (2 + $1)) < a;

      

       A5: (a * a) < (a * 1) by A1, A2, XREAL_1: 68;

      

       A6: for m1 st P[m1] holds P[(m1 + 1)]

      proof

        let m1;

        assume (a |^ (2 + m1)) < a;

        then ((a |^ (2 + m1)) * a) < (a * a) by A1, XREAL_1: 68;

        then (a |^ ((2 + m1) + 1)) < (a * a) by NEWTON: 6;

        hence thesis by A5, XXREAL_0: 2;

      end;

      (a |^ (2 + 0 )) = ((a GeoSeq ) . (1 + 1)) by Def1

      .= (((a GeoSeq ) . ( 0 + 1)) * a) by Th3

      .= ((((a GeoSeq ) . 0 ) * a) * a) by Th3

      .= ((1 * a) * a) by Th3

      .= (a * a);

      then

       A7: P[ 0 ] by A5;

      

       A8: for m1 holds P[m1] from NAT_1:sch 2( A7, A6);

      thus thesis by A4, A8;

    end;

    theorem :: PREPOWER:16

    

     Th16: for n be natural Number holds ( - 1) < a implies ((1 + a) |^ n) >= (1 + (n * a))

    proof

      let n be natural Number;

      

       A1: n is Nat by TARSKI: 1;

      defpred P[ Nat] means ((1 + a) |^ $1) >= (1 + ($1 * a));

      assume

       A2: ( - 1) < a;

      

       A3: for m be Nat st P[m] holds P[(m + 1)]

      proof

        

         A4: (( - 1) + 1) < (1 + a) by A2, XREAL_1: 6;

        let m be Nat;

        assume ((1 + a) |^ m) >= (1 + (m * a));

        then (((1 + a) |^ m) * (1 + a)) >= ((1 + (m * a)) * (1 + a)) by A4, XREAL_1: 64;

        then

         A5: ((1 + a) |^ (m + 1)) >= (((1 + (1 * a)) + (m * a)) + ((m * a) * a)) by NEWTON: 6;

         0 <= (a * a) by XREAL_1: 63;

        then ((1 + ((m + 1) * a)) + 0 ) <= ((1 + ((m + 1) * a)) + (m * (a * a))) by XREAL_1: 7;

        hence thesis by A5, XXREAL_0: 2;

      end;

      ((1 + a) |^ 0 ) = (((1 + a) GeoSeq ) . 0 ) by Def1

      .= 1 by Th3;

      then

       A6: P[ 0 ];

      for m be Nat holds P[m] from NAT_1:sch 2( A6, A3);

      hence thesis by A1;

    end;

    theorem :: PREPOWER:17

    

     Th17: for n be natural Number st 0 < a & a < 1 holds ((1 + a) |^ n) <= (1 + ((3 |^ n) * a))

    proof

      let n be natural Number;

      

       A1: n is Nat by TARSKI: 1;

      assume that

       A2: 0 < a and

       A3: a < 1;

      

       A4: (1 + 0 ) < (1 + a) by A2, XREAL_1: 6;

      defpred P[ Nat] means ((1 + a) |^ $1) <= (1 + ((3 |^ $1) * a));

      

       A5: for n be Nat holds P[n] implies P[(n + 1)]

      proof

        let n be Nat;

        assume ((1 + a) |^ n) <= (1 + ((3 |^ n) * a));

        then

         A6: (((1 + a) |^ n) * (1 + a)) <= ((1 + ((3 |^ n) * a)) * (1 + a)) by A2, XREAL_1: 64;

        

         A7: ((1 + ((3 |^ n) * a)) + (((3 |^ n) + (3 |^ n)) * a)) = (1 + (((3 |^ n) * (1 + 2)) * a))

        .= (1 + ((3 |^ (n + 1)) * a)) by NEWTON: 6;

        

         A8: 1 <= (3 |^ n)

        proof

          per cases ;

            suppose

             A9: 0 = n;

            (3 |^ n) = ((3 GeoSeq ) . n) by Def1

            .= 1 by A9, Th3;

            hence thesis;

          end;

            suppose 0 <> n;

            then ( 0 + 1) <= n by NAT_1: 13;

            then (1 |^ n) < (3 |^ n) by Lm1;

            hence thesis;

          end;

        end;

        then (1 * a) <= ((3 |^ n) * a) by A2, XREAL_1: 64;

        then

         A10: (1 + a) <= (1 + ((3 |^ n) * a)) by XREAL_1: 7;

        (a * a) < (1 * a) by A2, A3, XREAL_1: 68;

        then ((3 |^ n) * (a * a)) < ((3 |^ n) * a) by A8, XREAL_1: 68;

        then

         A11: (((3 |^ n) * a) + ((3 |^ n) * (a * a))) < (((3 |^ n) * a) + ((3 |^ n) * a)) by XREAL_1: 6;

        ((1 + ((3 |^ n) * a)) * (1 + a)) = ((1 + a) + (((3 |^ n) * a) + ((3 |^ n) * (a * a))));

        then ((1 + ((3 |^ n) * a)) * (1 + a)) < (1 + ((3 |^ (n + 1)) * a)) by A10, A7, A11, XREAL_1: 8;

        then (((1 + a) |^ n) * (1 + a)) <= (1 + ((3 |^ (n + 1)) * a)) by A6, XXREAL_0: 2;

        hence thesis by NEWTON: 6;

      end;

      

       A12: (1 + ((3 |^ 0 ) * a)) = (1 + (((3 GeoSeq ) . 0 ) * a)) by Def1

      .= (1 + (1 * a)) by Th3

      .= (1 + a);

      ((1 + a) |^ 0 ) = (((1 + a) GeoSeq ) . 0 ) by Def1

      .= 1 by Th3;

      then

       A13: P[ 0 ] by A12, A4;

      for n be Nat holds P[n] from NAT_1:sch 2( A13, A5);

      hence thesis by A1;

    end;

    theorem :: PREPOWER:18

    

     Th18: s1 is convergent & (for n holds (s2 . n) = ((s1 . n) |^ m)) implies s2 is convergent & ( lim s2) = (( lim s1) |^ m)

    proof

      assume that

       A1: s1 is convergent and

       A2: for n holds (s2 . n) = ((s1 . n) |^ m);

      defpred P[ Nat] means for s be Real_Sequence st (for n holds (s . n) = ((s1 . n) |^ $1)) holds s is convergent & ( lim s) = (( lim s1) |^ $1);

      

       A3: P[ 0 ]

      proof

        let s be Real_Sequence;

        assume

         A4: for n holds (s . n) = ((s1 . n) |^ 0 );

        reconsider j = 1 as Element of REAL by NUMBERS: 19;

         A5:

        now

          let n be Nat;

          

          thus (s . n) = ((s1 . n) |^ 0 ) by A4

          .= (((s1 . n) GeoSeq ) . 0 ) by Def1

          .= j by Th3;

        end;

        then

         A6: s is constant by VALUED_0:def 18;

        hence s is convergent;

        

        thus ( lim s) = (s . 0 ) by A6, SEQ_4: 26

        .= 1 by A5

        .= ((( lim s1) GeoSeq ) . 0 ) by Th3

        .= (( lim s1) |^ 0 ) by Def1;

      end;

      

       A7: for m1 holds P[m1] implies P[(m1 + 1)]

      proof

        let m1;

        assume

         A8: for s be Real_Sequence st (for n holds (s . n) = ((s1 . n) |^ m1)) holds s is convergent & ( lim s) = (( lim s1) |^ m1);

        deffunc O( Nat) = ((s1 . $1) |^ m1);

        let s be Real_Sequence;

        consider s3 be Real_Sequence such that

         A9: for n holds (s3 . n) = O(n) from SEQ_1:sch 1;

        assume

         A10: for n holds (s . n) = ((s1 . n) |^ (m1 + 1));

        now

          let n;

          

          thus (s . n) = ((s1 . n) |^ (m1 + 1)) by A10

          .= (((s1 . n) |^ m1) * (s1 . n)) by NEWTON: 6

          .= ((s3 . n) * (s1 . n)) by A9;

        end;

        then

         A11: s = (s3 (#) s1) by SEQ_1: 8;

        

         A12: s3 is convergent by A8, A9;

        hence s is convergent by A1, A11;

        ( lim s3) = (( lim s1) |^ m1) by A8, A9;

        

        hence ( lim s) = ((( lim s1) |^ m1) * ( lim s1)) by A1, A12, A11, SEQ_2: 15

        .= (( lim s1) |^ (m1 + 1)) by NEWTON: 6;

      end;

      for m1 holds P[m1] from NAT_1:sch 2( A3, A7);

      hence thesis by A2;

    end;

    definition

      let n be natural Number;

      let a be Real;

      assume

       A1: 1 <= n;

      :: PREPOWER:def2

      func n -Root a -> Real means

      : Def2: (it |^ n) = a & it > 0 if a > 0 ,

it = 0 if a = 0 ;

      consistency ;

      existence

      proof

        now

          set X = { b where b be Real : 0 < b & (b |^ n) <= a };

          for x be object holds x in X implies x in REAL

          proof

            let x be object;

            assume x in X;

            then ex b be Real st x = b & 0 < b & (b |^ n) <= a;

            hence thesis by XREAL_0:def 1;

          end;

          then

          reconsider X as Subset of REAL by TARSKI:def 3;

          reconsider a1 = a as Real;

          reconsider j = 1 as Element of REAL by NUMBERS: 19;

          

           A2: j <= a implies ex c st c in X

          proof

            assume

             A3: j <= a;

            take j;

            (j |^ n) <= a by A3, NEWTON: 10;

            hence thesis;

          end;

          

           A4: a < 1 implies ex c be Real st c is UpperBound of X

          proof

            consider c such that

             A5: c = 1;

            assume

             A6: a < 1;

            take c;

            let b be ExtReal;

            assume b in X;

            then

            consider d be Real such that

             A7: d = b & 0 < d & (d |^ n) <= a;

            assume not b <= c;

            then (1 |^ n) < (d |^ n) by A1, A5, Lm1, A7;

            then 1 < (d |^ n) by NEWTON: 10;

            hence contradiction by A6, A7, XXREAL_0: 2;

          end;

          assume

           A8: a > 0 ;

          1 <= a implies ex c be Real st c is UpperBound of X

          proof

            assume

             A9: 1 <= a;

            take a;

            let b be ExtReal;

            assume b in X;

            then

            consider d be Real such that

             A10: b = d & 0 < d & (d |^ n) <= a;

            assume a < b;

            then (a |^ n) < (d |^ n) by A1, A8, Lm1, A10;

            then (a |^ n) < a by A10, XXREAL_0: 2;

            hence contradiction by A1, A9, Th12;

          end;

          then

           A11: X is bounded_above by A4;

          take d = ( upper_bound X);

          

           A12: a < 1 implies ex c st c in X

          proof

            assume

             A13: a < 1;

            reconsider a as Real;

            take a;

            (a |^ n) <= a by A1, A8, A13, Th14;

            hence thesis by A8;

          end;

          

           A14: 0 < d

          proof

            consider c such that

             A15: c in X by A2, A12;

            ex e be Real st e = c & 0 < e & (e |^ n) <= a by A15;

            hence thesis by A11, A15, SEQ_4:def 1;

          end;

          

           A16: not a < (d |^ n)

          proof

            set b = ((d * (1 - (a / (d |^ n)))) / (n + 1));

            assume

             A17: a < (d |^ n);

            then

             A18: ((1 / (n + 1)) * (d |^ n)) > ((1 / (n + 1)) * a) by XREAL_1: 68;

            (a * ((d |^ n) " )) > ( 0 * a) by A8, A17;

            then ( - ( - (a / (d |^ n)))) > 0 ;

            then ( - (a / (d |^ n))) < 0 ;

            then (1 + ( - (a / (d |^ n)))) < (1 + 0 ) by XREAL_1: 6;

            then

             A19: ((1 - (a / (d |^ n))) * ((n + 1) " )) < (1 * ((n + 1) " )) by XREAL_1: 68;

            1 < (n + 1) by A1, NAT_1: 13;

            then ((n + 1) " ) < 1 by XREAL_1: 212;

            then ((1 - (a / (d |^ n))) / (n + 1)) < 1 by A19, XXREAL_0: 2;

            then

             A20: (d * ((1 - (a / (d |^ n))) / (n + 1))) < (d * 1) by A14, XREAL_1: 68;

            then (b / d) < (d / d) by A14, XREAL_1: 74;

            then (b / d) < 1 by A14, XCMPLX_1: 60;

            then ( - 1) < ( - (b / d)) by XREAL_1: 24;

            then

             A21: ((1 + ( - (b / d))) |^ n) >= (1 + (n * ( - (b / d)))) by Th16;

            (a / (d |^ n)) < ((d |^ n) / (d |^ n)) by A8, A17, XREAL_1: 74;

            then ( 0 + (a / (d |^ n))) < 1 by A8, A17, XCMPLX_1: 60;

            then 0 < (1 - (a / (d |^ n))) by XREAL_1: 20;

            then (d * 0 ) < (d * (1 - (a / (d |^ n)))) by A14;

            then ( 0 / (n + 1)) < ((d * (1 - (a / (d |^ n)))) / (n + 1));

            then

            consider c be Real such that

             A22: c in X and

             A23: (d - b) < c by A2, A12, A11, SEQ_4:def 1;

             0 < (d - b) by A20, XREAL_1: 50;

            then

             A24: ((d - b) |^ n) < (c |^ n) by A1, A23, Lm1;

            ((1 + (n * ( - (b / d)))) * (d |^ n)) = ((1 - (n * (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d))) * (d |^ n))

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

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

            .= ((1 - (n * ((1 - (a / (d |^ n))) / (n + 1)))) * (d |^ n)) by A14, XCMPLX_1: 87

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

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

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

            .= (((((n + 1) / (n + 1)) - (n / (n + 1))) + ((a / (d |^ n)) * (n / (n + 1)))) * (d |^ n)) by XCMPLX_1: 60

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

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

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

            .= (((1 / (n + 1)) * (d |^ n)) + ((n / (n + 1)) * a)) by A8, A17, XCMPLX_1: 87;

            then

             A25: ((1 + (n * ( - (b / d)))) * (d |^ n)) > (((1 / (n + 1)) * a) + ((n / (n + 1)) * a)) by A18, XREAL_1: 6;

            ((d - b) |^ n) = (((d - b) * 1) |^ n)

            .= (((d - b) * ((d " ) * d)) |^ n) by A14, XCMPLX_0:def 7

            .= ((((d - b) * (d " )) * d) |^ n)

            .= ((((d - b) / d) * d) |^ n)

            .= ((((d / d) - (b / d)) * d) |^ n)

            .= (((1 - (b / d)) * d) |^ n) by A14, XCMPLX_1: 60

            .= (((1 + ( - (b / d))) |^ n) * (d |^ n)) by NEWTON: 7;

            then ((d - b) |^ n) >= ((1 + (n * ( - (b / d)))) * (d |^ n)) by A8, A17, A21, XREAL_1: 64;

            then ((d - b) |^ n) > (((n + 1) / (n + 1)) * a) by A25, XXREAL_0: 2;

            then

             A26: ((d - b) |^ n) > (1 * a) by XCMPLX_1: 60;

            ex e be Real st e = c & 0 < e & (e |^ n) <= a by A22;

            hence contradiction by A24, A26, XXREAL_0: 2;

          end;

           not (d |^ n) < a

          proof

            set b = ( min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))));

            set c = ((1 + b) * d);

            

             A27: (c |^ n) = (((1 + b) |^ n) * (d |^ n)) by NEWTON: 7;

            

             A28: 0 < (3 |^ n) by Th6;

            ((3 |^ n) * b) <= ((((a / (d |^ n)) - 1) / (3 |^ n)) * (3 |^ n)) by XREAL_1: 64, XXREAL_0: 17;

            then ((3 |^ n) * b) <= ((a / (d |^ n)) - 1) by A28, XCMPLX_1: 87;

            then

             A29: (1 + ((3 |^ n) * b)) <= (a / (d |^ n)) by XREAL_1: 19;

            

             A30: (d |^ n) > 0 by A14, Th6;

            

             A31: (d |^ n) <> 0 by A14, Th6;

            assume (d |^ n) < a;

            then ((d |^ n) / (d |^ n)) < (a / (d |^ n)) by A30, XREAL_1: 74;

            then 1 < (a / (d |^ n)) by A31, XCMPLX_1: 60;

            then (1 - 1) < ((a / (d |^ n)) - 1) by XREAL_1: 9;

            then (((a / (d |^ n)) - 1) / (3 |^ n)) > ( 0 / (3 |^ n)) by A28;

            then

             A32: b > 0 by XXREAL_0: 15;

            then (1 + b) > (1 + 0 ) by XREAL_1: 6;

            then

             A33: ((1 + b) * d) > (1 * d) by A14, XREAL_1: 68;

            b <= (1 / 2) by XXREAL_0: 17;

            then b < 1 by XXREAL_0: 2;

            then ((1 + b) |^ n) <= (1 + ((3 |^ n) * b)) by A32, Th17;

            then ((1 + b) |^ n) <= (a / (d |^ n)) by A29, XXREAL_0: 2;

            then (c |^ n) <= ((a / (d |^ n)) * (d |^ n)) by A30, A27, XREAL_1: 64;

            then

             A34: (c |^ n) <= a by A31, XCMPLX_1: 87;

            ((1 + b) * d) > ( 0 * d) by A14, A32;

            then c in X by A34;

            hence contradiction by A11, A33, SEQ_4:def 1;

          end;

          hence a = (d |^ n) & d > 0 by A14, A16, XXREAL_0: 1;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        now

          let b,c be Real;

          assume that

           A35: (b |^ n) = a and

           A36: b > 0 and

           A37: (c |^ n) = a and

           A38: c > 0 and

           A39: b <> c;

          per cases by A39, XXREAL_0: 1;

            suppose b > c;

            hence contradiction by A1, A35, A37, A38, Lm1;

          end;

            suppose c > b;

            hence contradiction by A1, A35, A36, A37, Lm1;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let n;

      let a be Real;

      cluster (n -Root a) -> real;

      coherence ;

    end

    

     Lm2: for n be Nat st a > 0 & n >= 1 holds ((n -Root a) |^ n) = a & (n -Root (a |^ n)) = a

    proof

      let n be Nat;

      assume that

       A1: a > 0 and

       A2: n >= 1;

      thus ((n -Root a) |^ n) = a by A1, A2, Def2;

      assume

       A3: (n -Root (a |^ n)) <> a;

      per cases by A3, XXREAL_0: 1;

        suppose

         A4: (n -Root (a |^ n)) > a;

        (a |^ n) > 0 by A1, Th6;

        hence contradiction by A1, A2, A4, Def2;

      end;

        suppose

         A5: (n -Root (a |^ n)) < a;

        (a |^ n) > 0 by A1, Th6;

        hence contradiction by A1, A2, A5, Def2;

      end;

    end;

    theorem :: PREPOWER:19

    

     Th19: for n be Nat st a >= 0 & n >= 1 holds ((n -Root a) |^ n) = a & (n -Root (a |^ n)) = a

    proof

      let n be Nat;

      assume that

       A1: a >= 0 and

       A2: n >= 1;

      per cases by A1;

        suppose a > 0 ;

        hence thesis by A2, Lm2;

      end;

        suppose

         A3: a = 0 ;

        reconsider k = n, k1 = 1 as Integer;

        reconsider m = (k - k1) as Element of NAT by A2, INT_1: 5;

        

         A4: ( 0 |^ n) = ( 0 |^ (m + 1))

        .= (( 0 |^ m) * ( 0 |^ 1)) by NEWTON: 8

        .= (( 0 |^ m) * (( 0 GeoSeq ) . ( 0 + 1))) by Def1

        .= (( 0 |^ m) * ((( 0 GeoSeq ) . 0 ) * 0 )) by Th3

        .= 0 ;

        hence ((n -Root a) |^ n) = a by A2, A3, Def2;

        thus thesis by A2, A3, A4, Def2;

      end;

    end;

    theorem :: PREPOWER:20

    

     Th20: n >= 1 implies (n -Root 1) = 1

    proof

      

       A1: (1 |^ n) = 1;

      assume n >= 1;

      hence thesis by A1, Def2;

    end;

    theorem :: PREPOWER:21

    

     Th21: a >= 0 implies (1 -Root a) = a

    proof

      assume

       A1: a >= 0 ;

      (a |^ 1) = ((a GeoSeq ) . ( 0 + 1)) by Def1

      .= (((a GeoSeq ) . 0 ) * a) by Th3

      .= (1 * a) by Th3

      .= a;

      hence thesis by A1, Th19;

    end;

    theorem :: PREPOWER:22

    

     Th22: a >= 0 & b >= 0 & n >= 1 implies (n -Root (a * b)) = ((n -Root a) * (n -Root b))

    proof

      assume that

       A1: a >= 0 and

       A2: b >= 0 and

       A3: n >= 1 and

       A4: (n -Root (a * b)) <> ((n -Root a) * (n -Root b));

      

       A5: (((n -Root a) * (n -Root b)) |^ n) = (((n -Root a) |^ n) * ((n -Root b) |^ n)) by NEWTON: 7

      .= (a * ((n -Root b) |^ n)) by A1, A3, Th19

      .= (a * b) by A2, A3, Th19;

      per cases by A1, A2;

        suppose

         A6: a > 0 & b > 0 ;

        then

         A7: (n -Root b) > 0 by A3, Def2;

        

         A8: (n -Root a) > 0 by A3, A6, Def2;

        (a * b) > 0 by A6;

        then

         A9: (n -Root (a * b)) > 0 by A3, Def2;

        per cases by A4, XXREAL_0: 1;

          suppose (n -Root (a * b)) < ((n -Root a) * (n -Root b));

          hence contradiction by A3, A5, A9, Th19;

        end;

          suppose (n -Root (a * b)) > ((n -Root a) * (n -Root b));

          hence contradiction by A3, A5, A8, A7, Th19;

        end;

      end;

        suppose

         A10: a = 0 & b > 0 ;

        then (n -Root (a * b)) = 0 by A3, Def2;

        hence contradiction by A4, A10;

      end;

        suppose

         A11: a > 0 & b = 0 ;

        then (n -Root (a * b)) = 0 by A3, Def2;

        hence contradiction by A4, A11;

      end;

        suppose

         A12: a = 0 & b = 0 ;

        then (n -Root (a * b)) = 0 by A3, Def2;

        hence contradiction by A4, A12;

      end;

    end;

    theorem :: PREPOWER:23

    

     Th23: a > 0 & n >= 1 implies (n -Root (1 / a)) = (1 / (n -Root a))

    proof

      assume that

       A1: a > 0 and

       A2: n >= 1 and

       A3: (n -Root (1 / a)) <> (1 / (n -Root a));

      

       A4: (n -Root a) > 0 by A1, A2, Def2;

      

       A5: ((1 / (n -Root a)) |^ n) = (1 / ((n -Root a) |^ n)) by Th7

      .= (1 / a) by A1, A2, Lm2;

      

       A6: (n -Root (1 / a)) > 0 by A1, A2, Def2;

      per cases by A3, XXREAL_0: 1;

        suppose (n -Root (1 / a)) > (1 / (n -Root a));

        hence contradiction by A2, A4, A5, Lm2;

      end;

        suppose (n -Root (1 / a)) < (1 / (n -Root a));

        hence contradiction by A2, A5, A6, Lm2;

      end;

    end;

    theorem :: PREPOWER:24

    a >= 0 & b > 0 & n >= 1 implies (n -Root (a / b)) = ((n -Root a) / (n -Root b))

    proof

      assume that

       A1: a >= 0 and

       A2: b > 0 and

       A3: n >= 1;

      

      thus (n -Root (a / b)) = (n -Root (a * (b " )))

      .= ((n -Root a) * (n -Root (b " ))) by A1, A2, A3, Th22

      .= ((n -Root a) * (n -Root (1 / b)))

      .= ((n -Root a) * (1 / (n -Root b))) by A2, A3, Th23

      .= (((n -Root a) * 1) / (n -Root b))

      .= ((n -Root a) / (n -Root b));

    end;

    theorem :: PREPOWER:25

    

     Th25: a >= 0 & n >= 1 & m >= 1 implies (n -Root (m -Root a)) = ((n * m) -Root a)

    proof

      assume that

       A1: a >= 0 and

       A2: n >= 1 and

       A3: m >= 1 and

       A4: (n -Root (m -Root a)) <> ((n * m) -Root a);

      per cases by A1;

        suppose

         A5: a > 0 ;

        then

         A6: (m -Root a) > 0 by A3, Def2;

        then

         A7: (n -Root (m -Root a)) > 0 by A2, Def2;

        

         A8: ((n -Root (m -Root a)) |^ (n * m)) = (((n -Root (m -Root a)) |^ n) |^ m) by NEWTON: 9

        .= ((m -Root a) |^ m) by A2, A6, Lm2

        .= a by A1, A3, Th19;

        

         A9: (n * m) >= 1 by A2, A3, XREAL_1: 159;

        then

         A10: ((n * m) -Root a) > 0 by A5, Def2;

        per cases by A4, XXREAL_0: 1;

          suppose (n -Root (m -Root a)) < ((n * m) -Root a);

          hence contradiction by A5, A8, A9, A7, Def2;

        end;

          suppose ((n * m) -Root a) < (n -Root (m -Root a));

          hence contradiction by A5, A8, A9, A10, Def2;

        end;

      end;

        suppose

         A11: a = 0 ;

        (n * m) >= 1 by A2, A3, XREAL_1: 159;

        then

         A12: ((n * m) -Root a) = 0 by A11, Def2;

        (m -Root a) = 0 by A3, A11, Def2;

        hence contradiction by A2, A4, A12, Def2;

      end;

    end;

    theorem :: PREPOWER:26

    

     Th26: a >= 0 & n >= 1 & m >= 1 implies ((n -Root a) * (m -Root a)) = ((n * m) -Root (a |^ (n + m)))

    proof

      assume that

       A1: a >= 0 and

       A2: n >= 1 and

       A3: m >= 1 and

       A4: ((n -Root a) * (m -Root a)) <> ((n * m) -Root (a |^ (n + m)));

      

       A5: (((n -Root a) * (m -Root a)) |^ (n * m)) = (((n -Root a) |^ (n * m)) * ((m -Root a) |^ (n * m))) by NEWTON: 7

      .= ((((n -Root a) |^ n) |^ m) * ((m -Root a) |^ (n * m))) by NEWTON: 9

      .= ((a |^ m) * ((m -Root a) |^ (m * n))) by A1, A2, Th19

      .= ((a |^ m) * (((m -Root a) |^ m) |^ n)) by NEWTON: 9

      .= ((a |^ m) * (a |^ n)) by A1, A3, Th19

      .= (a |^ (n + m)) by NEWTON: 8;

      

       A6: (n * m) >= 1 by A2, A3, XREAL_1: 159;

      per cases by A1;

        suppose

         A7: a > 0 ;

        then

         A8: (m -Root a) > 0 by A3, Def2;

        (n -Root a) > 0 by A2, A7, Def2;

        then

         A9: ((n -Root a) * (m -Root a)) > 0 by A8;

        

         A10: (a |^ (n + m)) > 0 by A7, Th6;

        then

         A11: ((n * m) -Root (a |^ (n + m))) > 0 by A6, Def2;

        per cases by A4, XXREAL_0: 1;

          suppose ((n -Root a) * (m -Root a)) < ((n * m) -Root (a |^ (n + m)));

          hence contradiction by A5, A6, A10, A9, Def2;

        end;

          suppose ((n -Root a) * (m -Root a)) > ((n * m) -Root (a |^ (n + m)));

          hence contradiction by A5, A6, A10, A11, Def2;

        end;

      end;

        suppose

         A12: a = 0 ;

        reconsider k = n, k1 = 1 as Integer;

        reconsider m1 = (k - k1) as Element of NAT by A2, INT_1: 5;

        

         A13: (a |^ (n + m)) = (a |^ ((m1 + m) + 1))

        .= ((a |^ (m1 + m)) * a) by NEWTON: 6

        .= 0 by A12;

        (n -Root a) = 0 by A2, A12, Def2;

        hence contradiction by A4, A6, A13, Def2;

      end;

    end;

    theorem :: PREPOWER:27

    

     Th27: 0 <= a & a <= b & n >= 1 implies (n -Root a) <= (n -Root b)

    proof

      assume that

       A1: a >= 0 and

       A2: a <= b and

       A3: n >= 1 and

       A4: (n -Root a) > (n -Root b);

       A5:

      now

        per cases by A1, A2;

          suppose b > 0 ;

          hence (n -Root b) >= 0 by A3, Def2;

        end;

          suppose b = 0 ;

          hence (n -Root b) >= 0 by A3, Def2;

        end;

      end;

      ((n -Root a) |^ n) = a by A1, A3, Th19;

      then ((n -Root a) |^ n) <= ((n -Root b) |^ n) by A1, A2, A3, Th19;

      hence contradiction by A3, A4, A5, Th10;

    end;

    theorem :: PREPOWER:28

    

     Th28: a >= 0 & a < b & n >= 1 implies (n -Root a) < (n -Root b)

    proof

      assume that

       A1: a >= 0 and

       A2: a < b and

       A3: n >= 1 and

       A4: (n -Root a) >= (n -Root b);

      ((n -Root a) |^ n) = a by A1, A3, Th19;

      then

       A5: ((n -Root a) |^ n) < ((n -Root b) |^ n) by A1, A2, A3, Lm2;

      (n -Root b) > 0 by A1, A2, A3, Def2;

      hence contradiction by A4, A5, Th9;

    end;

    theorem :: PREPOWER:29

    

     Th29: a >= 1 & n >= 1 implies (n -Root a) >= 1 & a >= (n -Root a)

    proof

      assume that

       A1: a >= 1 and

       A2: n >= 1;

      (n -Root a) >= (n -Root 1) by A1, A2, Th27;

      hence (n -Root a) >= 1 by A2, Th20;

      (n -Root a) <= (n -Root (a |^ n)) by A1, A2, Th12, Th27;

      hence thesis by A1, A2, Lm2;

    end;

    theorem :: PREPOWER:30

    

     Th30: 0 <= a & a < 1 & n >= 1 implies a <= (n -Root a) & (n -Root a) < 1

    proof

      assume that

       A1: 0 <= a and

       A2: a < 1 and

       A3: n >= 1;

       A4:

      now

        per cases by A1;

          suppose a > 0 ;

          hence (a |^ n) >= 0 by Th6;

        end;

          suppose a = 0 ;

          hence (a |^ n) >= 0 ;

        end;

      end;

      now

        per cases by A1;

          suppose a > 0 ;

          hence (a |^ n) <= a by A2, A3, Th14;

        end;

          suppose a = 0 ;

          hence (a |^ n) <= a by A3, NEWTON: 11;

        end;

      end;

      then (n -Root (a |^ n)) <= (n -Root a) by A3, A4, Th27;

      hence a <= (n -Root a) by A1, A3, Th19;

      (n -Root a) < (n -Root 1) by A1, A2, A3, Th28;

      hence thesis by A3, Th20;

    end;

    theorem :: PREPOWER:31

    

     Th31: a > 0 & n >= 1 implies ((n -Root a) - 1) <= ((a - 1) / n)

    proof

      assume that

       A1: a > 0 and

       A2: n >= 1;

      (n -Root a) > 0 by A1, A2, Def2;

      then ((n -Root a) - 1) > ( 0 - 1) by XREAL_1: 9;

      then ((1 + ((n -Root a) - 1)) |^ n) >= (1 + (n * ((n -Root a) - 1))) by Th16;

      then a >= (1 + (n * ((n -Root a) - 1))) by A1, A2, Lm2;

      then (a - 1) >= (n * ((n -Root a) - 1)) by XREAL_1: 19;

      then ((a - 1) / n) >= ((n * ((n -Root a) - 1)) / n) by XREAL_1: 72;

      hence thesis by A2, XCMPLX_1: 89;

    end;

    theorem :: PREPOWER:32

    a >= 0 implies (2 -Root a) = ( sqrt a)

    proof

      assume that

       A1: a >= 0 and

       A2: (2 -Root a) <> ( sqrt a);

      

       A3: ( sqrt a) >= 0 by A1, SQUARE_1:def 2;

      (( sqrt a) |^ 2) = (( sqrt a) ^2 ) by NEWTON: 81

      .= a by A1, SQUARE_1:def 2;

      hence contradiction by A2, A3, Th19;

    end;

    

     Lm3: for s be Real_Sequence, a st a >= 1 & (for n st n >= 1 holds (s . n) = (n -Root a)) holds s is convergent & ( lim s) = 1

    proof

      set s2 = ( seq_const 1);

      let s be Real_Sequence;

      let a such that

       A1: a >= 1;

      deffunc O( Nat) = ((a - 1) / ($1 + 1));

      consider s1 be Real_Sequence such that

       A2: for n holds (s1 . n) = O(n) from SEQ_1:sch 1;

      set s3 = (s2 + s1);

      

       A3: s1 is convergent by A2, SEQ_4: 31;

      then

       A4: s3 is convergent;

      assume

       A5: for n st n >= 1 holds (s . n) = (n -Root a);

       A6:

      now

        let n;

        

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

        set b = (((s ^\ 1) . n) - 1);

        

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

        .= ((n + 1) -Root a) by A5, A7;

        then

         A9: ((s ^\ 1) . n) >= 1 by A1, A7, Th29;

        then (((s ^\ 1) . n) - 1) >= 0 by XREAL_1: 48;

        then

         A10: ( - 1) < b;

        a = ((1 + b) |^ (n + 1)) by A1, A7, A8, Lm2;

        then a >= (1 + ((n + 1) * b)) by A10, Th16;

        then (a - 1) >= ((1 + ((n + 1) * b)) - 1) by XREAL_1: 9;

        then ((a - 1) * ((n + 1) " )) >= (((n + 1) " ) * ((n + 1) * b)) by XREAL_1: 64;

        then ((a - 1) * ((n + 1) " )) >= ((((n + 1) " ) * (n + 1)) * b);

        then ((a - 1) * ((n + 1) " )) >= (1 * b) by XCMPLX_0:def 7;

        then (((a - 1) / (n + 1)) + 1) >= ((((s ^\ 1) . n) - 1) + 1) by XREAL_1: 6;

        then ((s2 . n) + ((a - 1) / (n + 1))) >= ((s ^\ 1) . n) by SEQ_1: 57;

        then ((s2 . n) + (s1 . n)) >= ((s ^\ 1) . n) by A2;

        hence (s2 . n) <= ((s ^\ 1) . n) & ((s ^\ 1) . n) <= (s3 . n) by A9, SEQ_1: 57, SEQ_1: 7;

      end;

      ( lim s1) = 0 by A2, SEQ_4: 31;

      

      then

       A11: ( lim s3) = ((s2 . 0 ) + 0 ) by A3, SEQ_4: 42

      .= 1 by SEQ_1: 57;

      

       A12: ( lim s2) = (s2 . 0 ) by SEQ_4: 26

      .= 1 by SEQ_1: 57;

      then

       A13: (s ^\ 1) is convergent by A4, A11, A6, SEQ_2: 19;

      hence s is convergent by SEQ_4: 21;

      ( lim (s ^\ 1)) = 1 by A4, A11, A12, A6, SEQ_2: 20;

      hence thesis by A13, SEQ_4: 22;

    end;

    theorem :: PREPOWER:33

    for s be Real_Sequence st a > 0 & (for n st n >= 1 holds (s . n) = (n -Root a)) holds s is convergent & ( lim s) = 1

    proof

      let s be Real_Sequence;

      assume

       A1: a > 0 ;

      assume

       A2: for n st n >= 1 holds (s . n) = (n -Root a);

      per cases ;

        suppose a >= 1;

        hence thesis by A2, Lm3;

      end;

        suppose

         A3: a < 1;

        then (a / a) < (1 / a) by A1, XREAL_1: 74;

        then

         A4: 1 <= (1 / a) by A1, XCMPLX_1: 60;

        deffunc O( Nat) = ($1 -Root (1 / a));

        consider s1 be Real_Sequence such that

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

        

         A6: for n holds n >= 1 implies (s1 . n) = (n -Root (1 / a)) by A5;

        then

         A7: ( lim s1) = 1 by A4, Lm3;

        

         A8: s1 is convergent by A4, A6, Lm3;

         A9:

        now

          let b be Real;

          assume b > 0 ;

          then

          consider m1 such that

           A10: for m st m1 <= m holds |.((s1 . m) - 1).| < b by A8, A7, SEQ_2:def 7;

          reconsider n = (m1 + 1) as Nat;

          take n;

          let m;

          assume

           A11: n <= m;

          

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

          then

           A13: 1 <= m by A11, XXREAL_0: 2;

          then

           A14: (m -Root a) < 1 by A1, A3, Th30;

          

           A15: (m -Root a) <> 0 by A1, A13, Def2;

          

          then

           A16: |.((1 / (m -Root a)) - 1).| = |.((1 / (m -Root a)) - ((m -Root a) / (m -Root a))).| by XCMPLX_1: 60

          .= |.((1 - (m -Root a)) / (m -Root a)).|

          .= |.((1 - (m -Root a)) * ((m -Root a) " )).|

          .= ( |.(1 - (m -Root a)).| * |.((m -Root a) " ).|) by COMPLEX1: 65;

           0 < (m -Root a) by A1, A3, A13, Th30;

          then ((m -Root a) * ((m -Root a) " )) < (1 * ((m -Root a) " )) by A14, XREAL_1: 68;

          then 1 < ((m -Root a) " ) by A15, XCMPLX_0:def 7;

          then

           A17: 1 < |.((m -Root a) " ).| by ABSVALUE:def 1;

           0 <> (1 - (m -Root a)) by A1, A3, A13, Th30;

          then |.(1 - (m -Root a)).| > 0 by COMPLEX1: 47;

          then

           A18: (1 * |.(1 - (m -Root a)).|) < ( |.(1 - (m -Root a)).| * |.((m -Root a) " ).|) by A17, XREAL_1: 68;

          m1 <= n by XREAL_1: 29;

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

          then |.((s1 . m) - 1).| < b by A10;

          then |.((m -Root (1 / a)) - 1).| < b by A5;

          then |.((1 / (m -Root a)) - 1).| < b by A1, A13, Th23;

          then |.( - ((m -Root a) - 1)).| < b by A16, A18, XXREAL_0: 2;

          then |.((m -Root a) - 1).| < b by COMPLEX1: 52;

          hence |.((s . m) - 1).| < b by A2, A12, A11, XXREAL_0: 2;

        end;

        hence s is convergent by SEQ_2:def 6;

        hence thesis by A9, SEQ_2:def 7;

      end;

    end;

    definition

      let a be Real;

      let k be Integer;

      :: PREPOWER:def3

      func a #Z k -> number equals

      : Def3: (a |^ |.k.|) if k >= 0 ,

((a |^ |.k.|) " ) if k < 0 ;

      consistency ;

      coherence by TARSKI: 1;

    end

    registration

      let a be Real;

      let k be Integer;

      cluster (a #Z k) -> real;

      coherence

      proof

        (a #Z k) = (a |^ |.k.|) or (a #Z k) = ((a |^ |.k.|) " ) by Def3;

        hence thesis;

      end;

    end

    theorem :: PREPOWER:34

    

     Th34: (a #Z 0 ) = 1

    proof

      

      thus (a #Z 0 ) = (a |^ |. 0 .|) by Def3

      .= (a |^ 0 ) by ABSVALUE: 2

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

      .= 1 by Th3;

    end;

    theorem :: PREPOWER:35

    

     Th35: (a #Z 1) = a

    proof

      

      thus (a #Z 1) = (a |^ |.1.|) by Def3

      .= (a |^ ( 0 + 1)) by ABSVALUE:def 1

      .= ((a GeoSeq ) . ( 0 + 1)) by Def1

      .= (((a GeoSeq ) . 0 ) * a) by Th3

      .= (1 * a) by Th3

      .= a;

    end;

    theorem :: PREPOWER:36

    

     Th36: for n be Nat holds (a #Z n) = (a |^ n)

    proof

      let n be Nat;

      

      thus (a #Z n) = (a |^ |.n.|) by Def3

      .= (a |^ n) by ABSVALUE:def 1;

    end;

    

     Lm4: (1 " ) = 1;

    theorem :: PREPOWER:37

    

     Th37: (1 #Z k) = 1

    proof

      per cases ;

        suppose k >= 0 ;

        

        hence (1 #Z k) = (1 |^ |.k.|) by Def3

        .= 1;

      end;

        suppose k < 0 ;

        (1 #Z k) = ((1 |^ |.k.|) " ) by Def3;

        hence thesis;

      end;

    end;

    theorem :: PREPOWER:38

    a <> 0 implies (a #Z k) <> 0

    proof

      assume

       A1: a <> 0 ;

      per cases ;

        suppose k >= 0 ;

        then (a #Z k) = (a |^ |.k.|) by Def3;

        hence thesis by A1, Th5;

      end;

        suppose k < 0 ;

        then (a #Z k) = ((a |^ |.k.|) " ) by Def3;

        hence thesis by A1, Th5, XCMPLX_1: 202;

      end;

    end;

    theorem :: PREPOWER:39

    

     Th39: a > 0 implies (a #Z k) > 0

    proof

      assume

       A1: a > 0 ;

      per cases ;

        suppose k >= 0 ;

        then (a #Z k) = (a |^ |.k.|) by Def3;

        hence thesis by A1, Th6;

      end;

        suppose

         A2: k < 0 ;

        

         A3: (a |^ |.k.|) > 0 by A1, Th6;

        (a #Z k) = ((a |^ |.k.|) " ) by A2, Def3;

        hence thesis by A3;

      end;

    end;

    theorem :: PREPOWER:40

    

     Th40: ((a * b) #Z k) = ((a #Z k) * (b #Z k))

    proof

      per cases ;

        suppose

         A1: k >= 0 ;

        

        hence ((a * b) #Z k) = ((a * b) |^ |.k.|) by Def3

        .= ((a |^ |.k.|) * (b |^ |.k.|)) by NEWTON: 7

        .= ((a #Z k) * (b |^ |.k.|)) by A1, Def3

        .= ((a #Z k) * (b #Z k)) by A1, Def3;

      end;

        suppose

         A2: k < 0 ;

        

        hence ((a * b) #Z k) = (((a * b) |^ |.k.|) " ) by Def3

        .= (((a |^ |.k.|) * (b |^ |.k.|)) " ) by NEWTON: 7

        .= (((a |^ |.k.|) " ) * ((b |^ |.k.|) " )) by XCMPLX_1: 204

        .= ((a #Z k) * ((b |^ |.k.|) " )) by A2, Def3

        .= ((a #Z k) * (b #Z k)) by A2, Def3;

      end;

    end;

    theorem :: PREPOWER:41

    

     Th41: (a #Z ( - k)) = (1 / (a #Z k))

    proof

      per cases ;

        suppose

         A1: k > 0 ;

        then ( - k) < ( - 0 );

        

        hence (a #Z ( - k)) = ((a |^ |.( - k).|) " ) by Def3

        .= ((a |^ |.k.|) " ) by COMPLEX1: 52

        .= (1 / (a |^ |.k.|))

        .= (1 / (a #Z k)) by A1, Def3;

      end;

        suppose

         A2: k = 0 ;

        

        hence (a #Z ( - k)) = (1 / 1) by Th34

        .= (1 / ((a GeoSeq ) . 0 )) by Th3

        .= (1 / (a |^ 0 )) by Def1

        .= (1 / (a #Z k)) by A2, Th36;

      end;

        suppose

         A3: k < 0 ;

        

        then (a #Z k) = ((a |^ |.k.|) " ) by Def3

        .= (1 / (a |^ |.k.|))

        .= (1 / (a |^ |.( - k).|)) by COMPLEX1: 52

        .= (1 / (a #Z ( - k))) by A3, Def3;

        hence thesis;

      end;

    end;

    theorem :: PREPOWER:42

    

     Th42: ((1 / a) #Z k) = (1 / (a #Z k))

    proof

      per cases ;

        suppose

         A1: k >= 0 ;

        

        hence ((1 / a) #Z k) = ((1 / a) |^ |.k.|) by Def3

        .= (1 / (a |^ |.k.|)) by Th7

        .= (1 / (a #Z k)) by A1, Def3;

      end;

        suppose

         A2: k < 0 ;

        

        hence ((1 / a) #Z k) = (((1 / a) |^ |.k.|) " ) by Def3

        .= ((1 / (a |^ |.k.|)) " ) by Th7

        .= (((a |^ |.k.|) " ) " )

        .= ((a #Z k) " ) by A2, Def3

        .= (1 / (a #Z k));

      end;

    end;

    theorem :: PREPOWER:43

    

     Th43: for m,n be Nat holds a <> 0 implies (a #Z (m - n)) = ((a |^ m) / (a |^ n))

    proof

      let m,n be Nat;

      assume

       A1: a <> 0 ;

      per cases ;

        suppose (m - n) >= 0 ;

        then

        reconsider m1 = (m - n) as Element of NAT by INT_1: 3;

        

         A2: ((a #Z (m - n)) * (a |^ n)) = ((a |^ m1) * (a |^ n)) by Th36

        .= (a |^ (m1 + n)) by NEWTON: 8

        .= (a |^ m);

        (a |^ n) <> 0 by A1, Th5;

        hence thesis by A2, XCMPLX_1: 89;

      end;

        suppose (m - n) < 0 ;

        then ( - (m - n)) > 0 ;

        then

        reconsider m1 = (n - m) as Element of NAT by INT_1: 3;

        

         A3: (a #Z (n - m)) = (a #Z ( - (m - n)))

        .= (1 / (a #Z (m - n))) by Th41;

        ((a #Z (n - m)) * (a |^ m)) = ((a |^ m1) * (a |^ m)) by Th36

        .= (a |^ (m1 + m)) by NEWTON: 8

        .= (a |^ n);

        then

         A4: ((a |^ m) / (a #Z (m - n))) = (a |^ n) by A3;

        (a |^ n) <> 0 by A1, Th5;

        hence thesis by A4, XCMPLX_1: 54;

      end;

    end;

    theorem :: PREPOWER:44

    

     Th44: a <> 0 implies (a #Z (k + l)) = ((a #Z k) * (a #Z l))

    proof

      assume

       A1: a <> 0 ;

      per cases ;

        suppose

         A2: k >= 0 & l >= 0 ;

        then

         A3: (k * l) >= 0 ;

        

        thus (a #Z (k + l)) = (a |^ |.(k + l).|) by A2, Def3

        .= (a |^ ( |.k.| + |.l.|)) by A3, ABSVALUE: 11

        .= ((a |^ |.k.|) * (a |^ |.l.|)) by NEWTON: 8

        .= ((a #Z k) * (a |^ |.l.|)) by A2, Def3

        .= ((a #Z k) * (a #Z l)) by A2, Def3;

      end;

        suppose

         A4: k >= 0 & l < 0 ;

        then

        reconsider m = k as Element of NAT by INT_1: 3;

        reconsider n = ( - l) as Element of NAT by A4, INT_1: 3;

        (k + l) = (m - n);

        

        hence (a #Z (k + l)) = ((a |^ m) / (a |^ n)) by A1, Th43

        .= ((a |^ m) * ((a |^ n) " ))

        .= ((a |^ |.k.|) * ((a |^ n) " )) by ABSVALUE:def 1

        .= ((a |^ |.k.|) * ((a |^ |.( - l).|) " )) by ABSVALUE:def 1

        .= ((a |^ |.k.|) * ((a |^ |.l.|) " )) by COMPLEX1: 52

        .= ((a #Z k) * ((a |^ |.l.|) " )) by A4, Def3

        .= ((a #Z k) * (a #Z l)) by A4, Def3;

      end;

        suppose

         A5: k < 0 & l >= 0 ;

        then

        reconsider m = l as Element of NAT by INT_1: 3;

        reconsider n = ( - k) as Element of NAT by A5, INT_1: 3;

        (k + l) = (m - n);

        

        hence (a #Z (k + l)) = ((a |^ m) / (a |^ n)) by A1, Th43

        .= ((a |^ m) * ((a |^ n) " ))

        .= ((a |^ |.l.|) * ((a |^ n) " )) by ABSVALUE:def 1

        .= ((a |^ |.l.|) * ((a |^ |.( - k).|) " )) by ABSVALUE:def 1

        .= ((a |^ |.l.|) * ((a |^ |.k.|) " )) by COMPLEX1: 52

        .= ((a #Z l) * ((a |^ |.k.|) " )) by A5, Def3

        .= ((a #Z k) * (a #Z l)) by A5, Def3;

      end;

        suppose

         A6: k < 0 & l < 0 ;

        then

         A7: (k * l) >= 0 ;

        

        thus (a #Z (k + l)) = ((a |^ |.(k + l).|) " ) by A6, Def3

        .= ((a |^ ( |.k.| + |.l.|)) " ) by A7, ABSVALUE: 11

        .= (((a |^ |.k.|) * (a |^ |.l.|)) " ) by NEWTON: 8

        .= (((a |^ |.k.|) " ) * ((a |^ |.l.|) " )) by XCMPLX_1: 204

        .= ((a #Z k) * ((a |^ |.l.|) " )) by A6, Def3

        .= ((a #Z k) * (a #Z l)) by A6, Def3;

      end;

    end;

    theorem :: PREPOWER:45

    

     Th45: ((a #Z k) #Z l) = (a #Z (k * l))

    proof

      per cases ;

        suppose

         A1: (k * l) > 0 ;

        per cases by A1, XREAL_1: 134;

          suppose

           A2: k > 0 & l > 0 ;

          

          hence ((a #Z k) #Z l) = ((a #Z k) |^ |.l.|) by Def3

          .= ((a |^ |.k.|) |^ |.l.|) by A2, Def3

          .= (a |^ ( |.k.| * |.l.|)) by NEWTON: 9

          .= (a |^ |.(k * l).|) by COMPLEX1: 65

          .= (a #Z (k * l)) by A1, Def3;

        end;

          suppose

           A3: k < 0 & l < 0 ;

          

          hence ((a #Z k) #Z l) = (((a #Z k) |^ |.l.|) " ) by Def3

          .= ((((a |^ |.k.|) " ) |^ |.l.|) " ) by A3, Def3

          .= (((1 / (a |^ |.k.|)) |^ |.l.|) " )

          .= ((1 / ((a |^ |.k.|) |^ |.l.|)) " ) by Th7

          .= ((((a |^ |.k.|) |^ |.l.|) " ) " )

          .= (a |^ ( |.k.| * |.l.|)) by NEWTON: 9

          .= (a |^ |.(k * l).|) by COMPLEX1: 65

          .= (a #Z (k * l)) by A1, Def3;

        end;

      end;

        suppose

         A4: (k * l) < 0 ;

        per cases by A4, XREAL_1: 133;

          suppose

           A5: k < 0 & l > 0 ;

          

          hence ((a #Z k) #Z l) = ((a #Z k) |^ |.l.|) by Def3

          .= (((a |^ |.k.|) " ) |^ |.l.|) by A5, Def3

          .= ((1 / (a |^ |.k.|)) |^ |.l.|)

          .= (1 / ((a |^ |.k.|) |^ |.l.|)) by Th7

          .= (1 / (a |^ ( |.k.| * |.l.|))) by NEWTON: 9

          .= (1 / (a |^ |.(k * l).|)) by COMPLEX1: 65

          .= ((a |^ |.(k * l).|) " )

          .= (a #Z (k * l)) by A4, Def3;

        end;

          suppose

           A6: k > 0 & l < 0 ;

          

          hence ((a #Z k) #Z l) = (((a #Z k) |^ |.l.|) " ) by Def3

          .= (((a |^ |.k.|) |^ |.l.|) " ) by A6, Def3

          .= ((a |^ ( |.k.| * |.l.|)) " ) by NEWTON: 9

          .= ((a |^ |.(k * l).|) " ) by COMPLEX1: 65

          .= (a #Z (k * l)) by A4, Def3;

        end;

      end;

        suppose

         A7: (k * l) = 0 ;

        per cases by A7;

          suppose k = 0 ;

          

          hence ((a #Z k) #Z l) = (1 #Z l) by Th34

          .= 1 by Th37

          .= (a #Z (k * l)) by A7, Th34;

        end;

          suppose l = 0 ;

          

          hence ((a #Z k) #Z l) = 1 by Th34

          .= (a #Z (k * l)) by A7, Th34;

        end;

      end;

    end;

    theorem :: PREPOWER:46

    

     Th46: a > 0 & n >= 1 implies ((n -Root a) #Z k) = (n -Root (a #Z k))

    proof

      assume that

       A1: a > 0 and

       A2: n >= 1;

      

       A3: (n -Root a) > 0 by A1, A2, Def2;

      

       A4: m >= 1 implies ((n -Root a) |^ m) = (n -Root (a |^ m))

      proof

        assume that

         A5: m >= 1 and

         A6: ((n -Root a) |^ m) <> (n -Root (a |^ m));

        

         A7: (a |^ m) > 0 by A1, Th6;

        then

         A8: (n -Root (a |^ m)) >= 0 by A2, Def2;

        

         A9: (m -Root (n -Root (a |^ m))) = ((n * m) -Root (a |^ m)) by A2, A5, A7, Th25

        .= (n -Root (m -Root (a |^ m))) by A2, A5, A7, Th25

        .= (n -Root a) by A1, A5, Lm2;

        

         A10: (m -Root ((n -Root a) |^ m)) = (n -Root a) by A3, A5, Lm2;

        

         A11: ((n -Root a) |^ m) >= 0 by A3, Th6;

        per cases by A6, XXREAL_0: 1;

          suppose ((n -Root a) |^ m) < (n -Root (a |^ m));

          hence contradiction by A5, A9, A11, Lm2;

        end;

          suppose ((n -Root a) |^ m) > (n -Root (a |^ m));

          hence contradiction by A5, A9, A10, A8, Th28;

        end;

      end;

      per cases ;

        suppose

         A12: k > 0 ;

        then |.k.| > 0 by ABSVALUE:def 1;

        then

         A13: |.k.| >= ( 0 + 1) by NAT_1: 13;

        

        thus ((n -Root a) #Z k) = ((n -Root a) |^ |.k.|) by A12, Def3

        .= (n -Root (a |^ |.k.|)) by A4, A13

        .= (n -Root (a #Z k)) by A12, Def3;

      end;

        suppose

         A14: k < 0 ;

        then |.k.| > 0 by COMPLEX1: 47;

        then

         A15: |.k.| >= ( 0 + 1) by NAT_1: 13;

        

         A16: (a |^ |.k.|) > 0 by A1, Th6;

        

        thus ((n -Root a) #Z k) = (((n -Root a) |^ |.k.|) " ) by A14, Def3

        .= ((n -Root (a |^ |.k.|)) " ) by A4, A15

        .= (1 / (n -Root (a |^ |.k.|)))

        .= (n -Root (1 / (a |^ |.k.|))) by A2, A16, Th23

        .= (n -Root ((a |^ |.k.|) " ))

        .= (n -Root (a #Z k)) by A14, Def3;

      end;

        suppose

         A17: k = 0 ;

        

        then (n -Root (a #Z k)) = (n -Root 1) by Th34

        .= 1 by A2, Th20;

        hence thesis by A17, Th34;

      end;

    end;

    definition

      let a be Real;

      let p be Rational;

      :: PREPOWER:def4

      func a #Q p -> number equals (( denominator p) -Root (a #Z ( numerator p)));

      coherence by TARSKI: 1;

    end

    registration

      let a be Real;

      let p be Rational;

      cluster (a #Q p) -> real;

      coherence ;

    end

    theorem :: PREPOWER:47

    

     Th47: p = 0 implies (a #Q p) = 1

    proof

      reconsider i = 0 as Integer;

      assume that

       A1: p = 0 ;

      ( numerator p) = 0 by A1, RAT_1: 14;

      

      hence (a #Q p) = (1 -Root (a #Z i)) by A1, RAT_1: 19

      .= (1 -Root 1) by Th34

      .= 1 by Th21;

    end;

    theorem :: PREPOWER:48

    

     Th48: a > 0 & p = 1 implies (a #Q p) = a

    proof

      assume that

       A1: a > 0 and

       A2: p = 1;

      

       A3: ( denominator p) = 1 by A2, RAT_1: 17;

      ( numerator p) = p by A2, RAT_1: 17;

      

      hence (a #Q p) = (1 -Root a) by A2, A3, Th35

      .= a by A1, Th21;

    end;

    

     Lm5: a >= 0 implies (a #Z k) >= 0

    proof

      assume

       A1: a >= 0 ;

      per cases by A1;

        suppose

         A2: a = 0 ;

         |.k.| = 0 or |.k.| >= 1 by NAT_1: 14;

        then (( 0 |^ |.k.|) " ) = ( 0 " ) or (( 0 |^ |.k.|) " ) = (1 " ) by NEWTON: 4, NEWTON: 11;

        hence thesis by A2, Def3;

      end;

        suppose a > 0 ;

        hence thesis by Th39;

      end;

    end;

    theorem :: PREPOWER:49

    

     Th49: for n be Nat st 0 <= a holds (a #Q n) = (a |^ n)

    proof

      let n be Nat;

      

       A1: ( denominator n) = 1 by RAT_1: 17;

      

       A2: ( numerator n) = n by RAT_1: 17;

      assume 0 <= a;

      

      hence (a #Q n) = (a #Z n) by A1, A2, Lm5, Th21

      .= (a |^ n) by Th36;

    end;

    theorem :: PREPOWER:50

    

     Th50: for n be Nat holds n >= 1 & p = (n " ) implies (a #Q p) = (n -Root a)

    proof

      let n be Nat;

      assume that

       A1: n >= 1 and

       A2: p = (n " );

      reconsider q = n as Rational;

      

       A3: p = (1 / n) by A2;

      then ( denominator p) = ( numerator q) by A1, RAT_1: 44;

      then

       A4: ( denominator p) = n by RAT_1: 17;

      ( numerator p) = ( denominator q) by A1, A3, RAT_1: 44;

      then ( numerator p) = 1 by RAT_1: 17;

      hence thesis by A4, Th35;

    end;

    theorem :: PREPOWER:51

    

     Th51: (1 #Q p) = 1

    proof

      

      thus (1 #Q p) = (( denominator p) -Root 1) by Th37

      .= 1 by Th20, RAT_1: 11;

    end;

    theorem :: PREPOWER:52

    

     Th52: a > 0 implies (a #Q p) > 0

    proof

      assume a > 0 ;

      then

       A1: (a #Z ( numerator p)) > 0 by Th39;

      ( denominator p) >= 1 by RAT_1: 11;

      hence thesis by A1, Def2;

    end;

    theorem :: PREPOWER:53

    

     Th53: a > 0 implies ((a #Q p) * (a #Q q)) = (a #Q (p + q))

    proof

      set dp = ( denominator p);

      set dq = ( denominator q);

      set np = ( numerator p);

      set nq = ( numerator q);

      

       A1: dp >= 1 by RAT_1: 11;

      reconsider ddq = dq as Integer;

      reconsider ddp = dp as Integer;

      

       A2: ( denominator (p + q)) >= 1 by RAT_1: 11;

      

       A3: dq >= 1 by RAT_1: 11;

      then

       A4: (dp * dq) >= 1 by A1, XREAL_1: 159;

      (p + q) = ((np / dp) + q) by RAT_1: 15

      .= ((np / dp) + (nq / dq)) by RAT_1: 15

      .= (((np * dq) + (nq * dp)) / (dp * dq)) by XCMPLX_1: 116;

      then

      consider n such that

       A5: ((np * dq) + (nq * dp)) = (( numerator (p + q)) * n) and

       A6: (dp * dq) = (( denominator (p + q)) * n) by RAT_1: 27;

      reconsider k = n as Integer;

      assume

       A7: a > 0 ;

      then

       A8: (a #Z (nq - np)) >= 0 by Th39;

      n > 0 by A6;

      then

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

      

       A10: (a #Z np) > 0 by A7, Th39;

      then

       A11: ((a #Z np) |^ (dp + dq)) >= 0 by Th6;

      

       A12: (a #Z (nq - np)) > 0 by A7, Th39;

      then

       A13: ((a #Z (nq - np)) |^ dp) >= 0 by Th6;

      

       A14: (a #Q (p + q)) > 0 by A7, Th52;

      

       A15: (a #Z ( numerator (p + q))) > 0 by A7, Th39;

      

      thus ((a #Q p) * (a #Q q)) = ((dp -Root (a #Z np)) * (dq -Root (a #Z (np + (nq - np)))))

      .= ((dp -Root (a #Z np)) * (dq -Root ((a #Z np) * (a #Z (nq - np))))) by A7, Th44

      .= ((dp -Root (a #Z np)) * ((dq -Root (a #Z np)) * (dq -Root (a #Z (nq - np))))) by A10, A8, Th22, RAT_1: 11

      .= (((dp -Root (a #Z np)) * (dq -Root (a #Z np))) * (dq -Root (a #Z (nq - np))))

      .= (((dp * dq) -Root ((a #Z np) |^ (dp + dq))) * (dq -Root (a #Z (nq - np)))) by A10, A3, A1, Th26

      .= (((dp * dq) -Root ((a #Z np) |^ (dp + dq))) * (dq -Root (dp -Root ((a #Z (nq - np)) |^ dp)))) by A12, A1, Lm2

      .= (((dp * dq) -Root ((a #Z np) |^ (dp + dq))) * ((dp * dq) -Root ((a #Z (nq - np)) |^ dp))) by A3, A1, A13, Th25

      .= ((dp * dq) -Root (((a #Z np) |^ (dp + dq)) * ((a #Z (nq - np)) |^ dp))) by A3, A1, A13, A11, Th22, XREAL_1: 159

      .= ((dp * dq) -Root (((a #Z np) #Z (ddp + ddq)) * ((a #Z (nq - np)) |^ dp))) by Th36

      .= ((dp * dq) -Root (((a #Z np) #Z (ddp + ddq)) * ((a #Z (nq - np)) #Z ddp))) by Th36

      .= ((dp * dq) -Root ((a #Z (np * (ddp + ddq))) * ((a #Z (nq - np)) #Z ddp))) by Th45

      .= ((dp * dq) -Root ((a #Z (np * (ddp + ddq))) * (a #Z ((nq - np) * ddp)))) by Th45

      .= ((dp * dq) -Root (a #Z (((np * ddp) + (np * ddq)) + ((nq - np) * ddp)))) by A7, Th44

      .= ((( denominator (p + q)) * n) -Root ((a #Z ( numerator (p + q))) #Z k)) by A5, A6, Th45

      .= (((( denominator (p + q)) * n) -Root (a #Z ( numerator (p + q)))) #Z k) by A4, A6, A15, Th46

      .= (((n * ( denominator (p + q))) -Root (a #Z ( numerator (p + q)))) |^ n) by Th36

      .= ((n -Root (a #Q (p + q))) |^ n) by A9, A2, A15, Th25

      .= (a #Q (p + q)) by A9, A14, Lm2;

    end;

    theorem :: PREPOWER:54

    

     Th54: a > 0 implies (1 / (a #Q p)) = (a #Q ( - p))

    proof

      assume a > 0 ;

      then

       A1: (a #Z ( numerator p)) > 0 by Th39;

      

      thus (a #Q ( - p)) = (( denominator ( - p)) -Root (a #Z ( - ( numerator p)))) by RAT_1: 43

      .= (( denominator p) -Root (a #Z ( - ( numerator p)))) by RAT_1: 43

      .= (( denominator p) -Root (1 / (a #Z ( numerator p)))) by Th41

      .= (1 / (a #Q p)) by A1, Th23, RAT_1: 11;

    end;

    theorem :: PREPOWER:55

    

     Th55: a > 0 implies ((a #Q p) / (a #Q q)) = (a #Q (p - q))

    proof

      assume

       A1: a > 0 ;

      

      thus (a #Q (p - q)) = (a #Q (p + ( - q)))

      .= ((a #Q p) * (a #Q ( - q))) by A1, Th53

      .= ((a #Q p) * (1 / (a #Q q))) by A1, Th54

      .= (((a #Q p) * 1) / (a #Q q))

      .= ((a #Q p) / (a #Q q));

    end;

    theorem :: PREPOWER:56

    

     Th56: a > 0 & b > 0 implies ((a * b) #Q p) = ((a #Q p) * (b #Q p))

    proof

      assume that

       A1: a > 0 and

       A2: b > 0 ;

      

       A3: (a #Z ( numerator p)) >= 0 by A1, Th39;

      

       A4: (b #Z ( numerator p)) >= 0 by A2, Th39;

      

      thus ((a * b) #Q p) = (( denominator p) -Root ((a #Z ( numerator p)) * (b #Z ( numerator p)))) by Th40

      .= ((a #Q p) * (b #Q p)) by A3, A4, Th22, RAT_1: 11;

    end;

    theorem :: PREPOWER:57

    

     Th57: a > 0 implies ((1 / a) #Q p) = (1 / (a #Q p))

    proof

      assume

       A1: a > 0 ;

      

      thus ((1 / a) #Q p) = (( denominator p) -Root (1 / (a #Z ( numerator p)))) by Th42

      .= (( denominator p) -Root (a #Z ( - ( numerator p)))) by Th41

      .= (( denominator p) -Root (a #Z ( numerator ( - p)))) by RAT_1: 43

      .= (a #Q ( - p)) by RAT_1: 43

      .= (1 / (a #Q p)) by A1, Th54;

    end;

    theorem :: PREPOWER:58

    

     Th58: a > 0 & b > 0 implies ((a / b) #Q p) = ((a #Q p) / (b #Q p))

    proof

      assume that

       A1: a > 0 and

       A2: b > 0 ;

      

      thus ((a / b) #Q p) = ((a * (1 / b)) #Q p)

      .= ((a #Q p) * ((1 / b) #Q p)) by A1, A2, Th56

      .= ((a #Q p) * (1 / (b #Q p))) by A2, Th57

      .= ((a #Q p) / (b #Q p));

    end;

    theorem :: PREPOWER:59

    

     Th59: a > 0 implies ((a #Q p) #Q q) = (a #Q (p * q))

    proof

      

       A1: ( denominator p) >= 1 by RAT_1: 11;

      p = (( numerator p) / ( denominator p)) by RAT_1: 15;

      

      then (p * q) = ((( numerator p) / ( denominator p)) * (( numerator q) / ( denominator q))) by RAT_1: 15

      .= (((( numerator p) / ( denominator p)) * ( numerator q)) / ( denominator q))

      .= ((( numerator p) * ( numerator q)) / (( denominator p) * ( denominator q))) by XCMPLX_1: 83;

      then

      consider n such that

       A2: (( numerator p) * ( numerator q)) = (( numerator (p * q)) * n) and

       A3: (( denominator p) * ( denominator q)) = (( denominator (p * q)) * n) by RAT_1: 27;

      

       A4: (( denominator (p * q)) * n) >= ( 0 + 1) by A3, NAT_1: 13;

      n > 0 by A3;

      then

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

      reconsider k = n as Integer;

      

       A6: ( denominator q) >= 1 by RAT_1: 11;

      

       A7: ( denominator (p * q)) >= 1 by RAT_1: 11;

      assume

       A8: a > 0 ;

      then

       A9: (a #Z (( numerator p) * ( numerator q))) >= 0 by Th39;

      

       A10: (a #Q (p * q)) > 0 by A8, Th52;

      

       A11: (a #Z ( numerator (p * q))) > 0 by A8, Th39;

      (a #Z ( numerator p)) > 0 by A8, Th39;

      

      hence ((a #Q p) #Q q) = (( denominator q) -Root (( denominator p) -Root ((a #Z ( numerator p)) #Z ( numerator q)))) by Th46, RAT_1: 11

      .= (( denominator q) -Root (( denominator p) -Root (a #Z (( numerator p) * ( numerator q))))) by Th45

      .= ((( denominator (p * q)) * n) -Root (a #Z (( numerator (p * q)) * k))) by A1, A6, A9, A2, A3, Th25

      .= ((( denominator (p * q)) * n) -Root ((a #Z ( numerator (p * q))) #Z k)) by Th45

      .= (((( denominator (p * q)) * n) -Root (a #Z ( numerator (p * q)))) #Z k) by A11, A4, Th46

      .= (((n * ( denominator (p * q))) -Root (a #Z ( numerator (p * q)))) |^ n) by Th36

      .= ((n -Root (a #Q (p * q))) |^ n) by A5, A7, A11, Th25

      .= (a #Q (p * q)) by A5, A10, Lm2;

    end;

    theorem :: PREPOWER:60

    

     Th60: a >= 1 & p >= 0 implies (a #Q p) >= 1

    proof

      assume that

       A1: a >= 1 and

       A2: p >= 0 ;

      ( numerator p) >= 0 by A2, RAT_1: 37;

      then

      reconsider n = ( numerator p) as Element of NAT by INT_1: 3;

      

       A3: (a #Z ( numerator p)) = (a |^ n) by Th36;

      (a |^ n) >= (1 |^ n) by A1, Th9;

      then

       A4: (a #Z ( numerator p)) >= 1 by A3;

      ( denominator p) >= 1 by RAT_1: 11;

      hence thesis by A4, Th29;

    end;

    theorem :: PREPOWER:61

    

     Th61: a >= 1 & p <= 0 implies (a #Q p) <= 1

    proof

      assume that

       A1: a >= 1 and

       A2: p <= 0 ;

      (a #Q ( - p)) >= 1 by A1, A2, Th60;

      then (1 / (a #Q p)) >= 1 by A1, Th54;

      hence thesis by XREAL_1: 191;

    end;

    theorem :: PREPOWER:62

    

     Th62: a > 1 & p > 0 implies (a #Q p) > 1

    proof

      assume that

       A1: a > 1 and

       A2: p > 0 ;

      

       A3: ( numerator p) > 0 by A2, RAT_1: 38;

      then

      reconsider n = ( numerator p) as Element of NAT by INT_1: 3;

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

      then

       A4: (a |^ n) > (1 |^ n) by A1, Lm1;

      (a #Z ( numerator p)) = (a |^ n) by Th36;

      then (a #Z ( numerator p)) > 1 by A4;

      then (( denominator p) -Root (a #Z ( numerator p))) > (( denominator p) -Root 1) by Th28, RAT_1: 11;

      hence thesis by Th20, RAT_1: 11;

    end;

    theorem :: PREPOWER:63

    

     Th63: a >= 1 & p >= q implies (a #Q p) >= (a #Q q)

    proof

      assume that

       A1: a >= 1 and

       A2: p >= q;

      per cases by A2, XXREAL_0: 1;

        suppose p = q;

        hence thesis;

      end;

        suppose p > q;

        then

         A3: (p - q) >= 0 by XREAL_1: 50;

        

         A4: (a #Q q) <> 0 by A1, Th52;

        

         A5: ((a #Q p) / (a #Q q)) = (a #Q (p - q)) by A1, Th55;

        (a #Q q) >= 0 by A1, Th52;

        then (((a #Q p) / (a #Q q)) * (a #Q q)) >= (1 * (a #Q q)) by A1, A3, A5, Th60, XREAL_1: 64;

        hence thesis by A4, XCMPLX_1: 87;

      end;

    end;

    theorem :: PREPOWER:64

    

     Th64: a > 1 & p > q implies (a #Q p) > (a #Q q)

    proof

      assume that

       A1: a > 1 and

       A2: p > q;

      

       A3: (p - q) > 0 by A2, XREAL_1: 50;

      

       A4: ((a #Q p) / (a #Q q)) = (a #Q (p - q)) by A1, Th55;

      

       A5: (a #Q q) <> 0 by A1, Th52;

      (a #Q q) > 0 by A1, Th52;

      then (((a #Q p) / (a #Q q)) * (a #Q q)) > (1 * (a #Q q)) by A1, A3, A4, Th62, XREAL_1: 68;

      hence thesis by A5, XCMPLX_1: 87;

    end;

    theorem :: PREPOWER:65

    

     Th65: a > 0 & a < 1 & p > 0 implies (a #Q p) < 1

    proof

      reconsider q = 0 as Rational;

      assume that

       A1: a > 0 and

       A2: a < 1 and

       A3: p > 0 ;

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

      then ((1 / a) #Q p) > ((1 / a) #Q q) by A3, Th64;

      then ((1 / a) #Q p) > 1 by Th47;

      then (1 / (a #Q p)) > 1 by A1, Th57;

      hence thesis by XREAL_1: 185;

    end;

    theorem :: PREPOWER:66

    a > 0 & a <= 1 & p <= 0 implies (a #Q p) >= 1

    proof

      assume that

       A1: a > 0 and

       A2: a <= 1 and

       A3: p <= 0 ;

      (1 / a) >= 1 by A1, A2, Lm4, XREAL_1: 85;

      then ((1 / a) #Q p) <= 1 by A3, Th61;

      then

       A4: (1 / (a #Q p)) <= 1 by A1, Th57;

      (a #Q p) > 0 by A1, Th52;

      hence thesis by A4, XREAL_1: 187;

    end;

    registration

      cluster RAT -valued for Real_Sequence;

      existence

      proof

        take ( seq_const 0 );

        thus thesis;

      end;

    end

    definition

      ::$Canceled

      mode Rational_Sequence is RAT -valued Real_Sequence;

    end

    theorem :: PREPOWER:67

    

     Th67: for a be Real holds ex s be Rational_Sequence st s is convergent & ( lim s) = a & for n holds (s . n) <= a

    proof

      let a be Real;

      deffunc O( Nat) = ( [\(($1 + 1) * a)/] / ($1 + 1));

      consider s be Real_Sequence such that

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

      ( rng s) c= RAT

      proof

        let y be object;

        assume y in ( rng s);

        then

        consider n be Element of NAT such that

         A2: (s . n) = y by FUNCT_2: 113;

        (s . n) = O(n) by A1;

        hence thesis by A2, RAT_1:def 2;

      end;

      then

      reconsider s as Rational_Sequence by RELAT_1:def 19;

      deffunc O( Nat) = (1 / ($1 + 1));

      consider s2 be Real_Sequence such that

       A3: for n holds (s2 . n) = O(n) from SEQ_1:sch 1;

      reconsider a1 = a as Element of REAL by XREAL_0:def 1;

      set s1 = ( seq_const a);

      take s;

      set s3 = (s1 - s2);

      

       A4: s2 is convergent by A3, SEQ_4: 31;

      then

       A5: s3 is convergent;

       A6:

      now

        let n;

        ((n + 1) * a) <= ( [\((n + 1) * a)/] + 1) by INT_1: 29;

        then (((n + 1) * a) - 1) <= (( [\((n + 1) * a)/] + 1) - 1) by XREAL_1: 9;

        then ((((n + 1) * a) - 1) * ((n + 1) " )) <= ( [\((n + 1) * a)/] / (n + 1)) by XREAL_1: 64;

        then (((a / (n + 1)) * (n + 1)) - (1 / (n + 1))) <= (s . n) by A1;

        then (a - (1 / (n + 1))) <= (s . n) by XCMPLX_1: 87;

        then ((s1 . n) - (1 / (n + 1))) <= (s . n) by SEQ_1: 57;

        then

         A7: ((s1 . n) - (s2 . n)) <= (s . n) by A3;

         [\((n + 1) * a)/] <= ((n + 1) * a) by INT_1:def 6;

        then ( [\((n + 1) * a)/] * ((n + 1) " )) <= ((a * (n + 1)) * ((n + 1) " )) by XREAL_1: 64;

        then ( [\((n + 1) * a)/] * ((n + 1) " )) <= (a * ((n + 1) * ((n + 1) " )));

        then ( [\((n + 1) * a)/] * ((n + 1) " )) <= (a * 1) by XCMPLX_0:def 7;

        then ( [\((n + 1) * a)/] / (n + 1)) <= (s1 . n) by SEQ_1: 57;

        hence (s3 . n) <= (s . n) & (s . n) <= (s1 . n) by A1, A7, RFUNCT_2: 1;

      end;

      ( lim s2) = 0 by A3, SEQ_4: 31;

      

      then

       A8: ( lim s3) = ((s1 . 0 ) - 0 ) by A4, SEQ_4: 42

      .= a by SEQ_1: 57;

      

       A9: ( lim s1) = (s1 . 0 ) by SEQ_4: 26

      .= a by SEQ_1: 57;

      hence s is convergent by A5, A8, A6, SEQ_2: 19;

      thus ( lim s) = a by A5, A8, A9, A6, SEQ_2: 20;

      let n;

      (s . n) <= (s1 . n) by A6;

      hence thesis by SEQ_1: 57;

    end;

    theorem :: PREPOWER:68

    

     Th68: ex s be Rational_Sequence st s is convergent & ( lim s) = a & for n holds (s . n) >= a

    proof

      deffunc O( Nat) = ( [/(($1 + 1) * a)\] / ($1 + 1));

      consider s be Real_Sequence such that

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

      ( rng s) c= RAT

      proof

        let y be object;

        assume y in ( rng s);

        then

        consider n be Element of NAT such that

         A2: (s . n) = y by FUNCT_2: 113;

        (s . n) = O(n) by A1;

        hence thesis by A2, RAT_1:def 2;

      end;

      then

      reconsider s as Rational_Sequence by RELAT_1:def 19;

      deffunc O( Nat) = (1 / ($1 + 1));

      consider s2 be Real_Sequence such that

       A3: for n holds (s2 . n) = O(n) from SEQ_1:sch 1;

      take s;

      set s1 = ( seq_const a);

      set s3 = (s1 + s2);

      

       A4: s2 is convergent by A3, SEQ_4: 31;

      then

       A5: s3 is convergent;

       A6:

      now

        let n;

        (((n + 1) * a) + 1) >= [/((n + 1) * a)\] by INT_1:def 7;

        then ((((n + 1) * a) + 1) * ((n + 1) " )) >= ( [/((n + 1) * a)\] / (n + 1)) by XREAL_1: 64;

        then (((a / (n + 1)) * (n + 1)) + (1 / (n + 1))) >= (s . n) by A1;

        then (a + (1 / (n + 1))) >= (s . n) by XCMPLX_1: 87;

        then ((s1 . n) + (1 / (n + 1))) >= (s . n) by SEQ_1: 57;

        then

         A7: ((s1 . n) + (s2 . n)) >= (s . n) by A3;

         [/((n + 1) * a)\] >= ((n + 1) * a) by INT_1:def 7;

        then ( [/((n + 1) * a)\] * ((n + 1) " )) >= ((a * (n + 1)) * ((n + 1) " )) by XREAL_1: 64;

        then ( [/((n + 1) * a)\] * ((n + 1) " )) >= (a * ((n + 1) * ((n + 1) " )));

        then ( [/((n + 1) * a)\] * ((n + 1) " )) >= (a * 1) by XCMPLX_0:def 7;

        then ( [/((n + 1) * a)\] / (n + 1)) >= (s1 . n) by SEQ_1: 57;

        hence (s1 . n) <= (s . n) & (s . n) <= (s3 . n) by A1, A7, SEQ_1: 7;

      end;

      ( lim s2) = 0 by A3, SEQ_4: 31;

      

      then

       A8: ( lim s3) = ((s1 . 0 ) + 0 ) by A4, SEQ_4: 42

      .= a by SEQ_1: 57;

      

       A9: ( lim s1) = (s1 . 0 ) by SEQ_4: 26

      .= a by SEQ_1: 57;

      hence s is convergent by A5, A8, A6, SEQ_2: 19;

      thus ( lim s) = a by A5, A8, A9, A6, SEQ_2: 20;

      let n;

      (s . n) >= (s1 . n) by A6;

      hence thesis by SEQ_1: 57;

    end;

    definition

      let a be Real;

      let s be Rational_Sequence;

      :: PREPOWER:def6

      func a #Q s -> Real_Sequence means

      : Def5: for n holds (it . n) = (a #Q (s . n));

      existence

      proof

        deffunc O( Nat) = (a #Q (s . $1));

        consider s1 be Real_Sequence such that

         A1: for n holds (s1 . n) = O(n) from SEQ_1:sch 1;

        take s1;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let s1,s2 be Real_Sequence;

        assume that

         A2: for n holds (s1 . n) = (a #Q (s . n)) and

         A3: for n holds (s2 . n) = (a #Q (s . n));

        now

          let n be Element of NAT ;

          

          thus (s1 . n) = (a #Q (s . n)) by A2

          .= (s2 . n) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    

     Lm6: for s be Rational_Sequence, a st s is convergent & a >= 1 holds (a #Q s) is convergent

    proof

      let s be Rational_Sequence;

      let a;

      assume that

       A1: s is convergent and

       A2: a >= 1;

      s is bounded by A1;

      then

      consider d be Real such that 0 < d and

       A3: for n holds |.(s . n).| < d by SEQ_2: 3;

      consider m2 such that

       A4: d < m2 by SEQ_4: 3;

      reconsider m2 as Rational;

      now

        

         A5: (a #Q m2) >= 0 by A2, Th52;

        let c be Real;

        assume

         A6: c > 0 ;

        consider m1 such that

         A7: (((a #Q m2) * (a - 1)) / c) < m1 by SEQ_4: 3;

        (m1 + 1) >= m1 by XREAL_1: 29;

        then (((a #Q m2) * (a - 1)) / c) < (m1 + 1) by A7, XXREAL_0: 2;

        then ((((a #Q m2) * (a - 1)) / c) * c) < (c * (m1 + 1)) by A6, XREAL_1: 68;

        then ((a #Q m2) * (a - 1)) < (c * (m1 + 1)) by A6, XCMPLX_1: 87;

        then (((a #Q m2) * (a - 1)) / (m1 + 1)) < (((m1 + 1) * c) / (m1 + 1)) by XREAL_1: 74;

        then (((a #Q m2) * (a - 1)) / (m1 + 1)) < ((c / (m1 + 1)) * (m1 + 1));

        then

         A8: (((a #Q m2) * (a - 1)) / (m1 + 1)) < c by XCMPLX_1: 87;

        consider n such that

         A9: for m st n <= m holds |.((s . m) - (s . n)).| < ((m1 + 1) " ) by A1, SEQ_4: 41;

        take n;

        let m;

        assume m >= n;

        then

         A10: |.((s . m) - (s . n)).| <= ((m1 + 1) " ) by A9;

        

         A11: (m1 + 1) >= ( 0 + 1) by NAT_1: 13;

        then (((m1 + 1) -Root a) - 1) <= ((a - 1) / (m1 + 1)) by A2, Th31;

        then

         A12: ((a #Q m2) * (((m1 + 1) -Root a) - 1)) <= ((a #Q m2) * ((a - 1) / (m1 + 1))) by A5, XREAL_1: 64;

        

         A13: (a #Q (s . n)) <> 0 by A2, Th52;

        

         A14: |.((a #Q (s . m)) - (a #Q (s . n))).| = |.(((a #Q (s . m)) - (a #Q (s . n))) * 1).|

        .= |.(((a #Q (s . m)) - (a #Q (s . n))) * ((a #Q (s . n)) / (a #Q (s . n)))).| by A13, XCMPLX_1: 60

        .= |.(((a #Q (s . n)) * ((a #Q (s . m)) - (a #Q (s . n)))) / (a #Q (s . n))).|

        .= |.((a #Q (s . n)) * (((a #Q (s . m)) - (a #Q (s . n))) / (a #Q (s . n)))).|

        .= ( |.(a #Q (s . n)).| * |.(((a #Q (s . m)) - (a #Q (s . n))) / (a #Q (s . n))).|) by COMPLEX1: 65

        .= ( |.(a #Q (s . n)).| * |.(((a #Q (s . m)) / (a #Q (s . n))) - ((a #Q (s . n)) / (a #Q (s . n)))).|)

        .= ( |.(a #Q (s . n)).| * |.(((a #Q (s . m)) / (a #Q (s . n))) - 1).|) by A13, XCMPLX_1: 60

        .= ( |.(a #Q (s . n)).| * |.((a #Q ((s . m) - (s . n))) - 1).|) by A2, Th55;

        

         A15: (s . n) <= |.(s . n).| by ABSVALUE: 4;

        reconsider m3 = ((m1 + 1) " ) as Rational;

        

         A16: |.((a #Q ((s . m) - (s . n))) - 1).| >= 0 by COMPLEX1: 46;

        

         A17: (a #Q ((s . m) - (s . n))) <> 0 by A2, Th52;

        ((s . m) - (s . n)) <= |.((s . m) - (s . n)).| by ABSVALUE: 4;

        then ((s . m) - (s . n)) <= ((m1 + 1) " ) by A10, XXREAL_0: 2;

        then (a #Q ((s . m) - (s . n))) <= (a #Q m3) by A2, Th63;

        then (a #Q ((s . m) - (s . n))) <= ((m1 + 1) -Root a) by A11, Th50;

        then

         A18: ((a #Q ((s . m) - (s . n))) - 1) <= (((m1 + 1) -Root a) - 1) by XREAL_1: 9;

        

         A19: (a #Q ((s . m) - (s . n))) > 0 by A2, Th52;

         A20:

        now

          per cases ;

            suppose ((s . m) - (s . n)) >= 0 ;

            then (a #Q ((s . m) - (s . n))) >= 1 by A2, Th60;

            then ((a #Q ((s . m) - (s . n))) - 1) >= 0 by XREAL_1: 48;

            hence |.((a #Q ((s . m) - (s . n))) - 1).| <= (((m1 + 1) -Root a) - 1) by A18, ABSVALUE:def 1;

          end;

            suppose

             A21: ((s . m) - (s . n)) < 0 ;

            

             A22: ( - ((s . m) - (s . n))) <= |.( - ((s . m) - (s . n))).| by ABSVALUE: 4;

             |.((s . m) - (s . n)).| = |.( - ((s . m) - (s . n))).| by COMPLEX1: 52;

            then ( - ((s . m) - (s . n))) <= m3 by A10, A22, XXREAL_0: 2;

            then (a #Q ( - ((s . m) - (s . n)))) <= (a #Q m3) by A2, Th63;

            then (a #Q ( - ((s . m) - (s . n)))) <= ((m1 + 1) -Root a) by A11, Th50;

            then

             A23: ((a #Q ( - ((s . m) - (s . n)))) - 1) <= (((m1 + 1) -Root a) - 1) by XREAL_1: 9;

            (a #Q ( - ((s . m) - (s . n)))) >= 1 by A2, A21, Th60;

            then ((a #Q ( - ((s . m) - (s . n)))) - 1) >= 0 by XREAL_1: 48;

            then

             A24: |.((a #Q ( - ((s . m) - (s . n)))) - 1).| <= (((m1 + 1) -Root a) - 1) by A23, ABSVALUE:def 1;

            (a #Q ((s . m) - (s . n))) <= 1 by A2, A21, Th61;

            then

             A25: |.(a #Q ((s . m) - (s . n))).| <= 1 by A19, ABSVALUE:def 1;

             |.((a #Q ( - ((s . m) - (s . n)))) - 1).| >= 0 by COMPLEX1: 46;

            then

             A26: ( |.(a #Q ((s . m) - (s . n))).| * |.((a #Q ( - ((s . m) - (s . n)))) - 1).|) <= (1 * |.((a #Q ( - ((s . m) - (s . n)))) - 1).|) by A25, XREAL_1: 64;

             |.((a #Q ((s . m) - (s . n))) - 1).| = |.(((a #Q ((s . m) - (s . n))) - 1) * 1).|

            .= |.(((a #Q ((s . m) - (s . n))) - 1) * ((a #Q ((s . m) - (s . n))) / (a #Q ((s . m) - (s . n))))).| by A17, XCMPLX_1: 60

            .= |.(((a #Q ((s . m) - (s . n))) * ((a #Q ((s . m) - (s . n))) - 1)) / (a #Q ((s . m) - (s . n)))).|

            .= |.((a #Q ((s . m) - (s . n))) * (((a #Q ((s . m) - (s . n))) - 1) / (a #Q ((s . m) - (s . n))))).|

            .= ( |.(a #Q ((s . m) - (s . n))).| * |.(((a #Q ((s . m) - (s . n))) - 1) / (a #Q ((s . m) - (s . n)))).|) by COMPLEX1: 65

            .= ( |.(a #Q ((s . m) - (s . n))).| * |.(((a #Q ((s . m) - (s . n))) / (a #Q ((s . m) - (s . n)))) - (1 / (a #Q ((s . m) - (s . n))))).|)

            .= ( |.(a #Q ((s . m) - (s . n))).| * |.(1 - (1 / (a #Q ((s . m) - (s . n))))).|) by A17, XCMPLX_1: 60

            .= ( |.(a #Q ((s . m) - (s . n))).| * |.(1 - (a #Q ( - ((s . m) - (s . n))))).|) by A2, Th54

            .= ( |.(a #Q ((s . m) - (s . n))).| * |.( - (1 - (a #Q ( - ((s . m) - (s . n)))))).|) by COMPLEX1: 52

            .= ( |.(a #Q ((s . m) - (s . n))).| * |.((a #Q ( - ((s . m) - (s . n)))) - 1).|);

            hence |.((a #Q ((s . m) - (s . n))) - 1).| <= (((m1 + 1) -Root a) - 1) by A24, A26, XXREAL_0: 2;

          end;

        end;

        

         A27: (a #Q (s . n)) > 0 by A2, Th52;

         |.(s . n).| <= m2 by A3, A4, XXREAL_0: 2;

        then (s . n) <= m2 by A15, XXREAL_0: 2;

        then (a #Q (s . n)) <= (a #Q m2) by A2, Th63;

        then

         A28: |.(a #Q (s . n)).| <= (a #Q m2) by A27, ABSVALUE:def 1;

         |.(a #Q (s . n)).| >= 0 by A27, ABSVALUE:def 1;

        then ( |.(a #Q (s . n)).| * |.((a #Q ((s . m) - (s . n))) - 1).|) <= ((a #Q m2) * (((m1 + 1) -Root a) - 1)) by A20, A16, A28, XREAL_1: 66;

        then |.((a #Q (s . m)) - (a #Q (s . n))).| <= (((a #Q m2) * (a - 1)) / (m1 + 1)) by A14, A12, XXREAL_0: 2;

        then |.((a #Q (s . m)) - (a #Q (s . n))).| < c by A8, XXREAL_0: 2;

        then |.(((a #Q s) . m) - (a #Q (s . n))).| < c by Def5;

        hence |.(((a #Q s) . m) - ((a #Q s) . n)).| < c by Def5;

      end;

      hence thesis by SEQ_4: 41;

    end;

    theorem :: PREPOWER:69

    

     Th69: for s be Rational_Sequence st s is convergent & a > 0 holds (a #Q s) is convergent

    proof

      let s be Rational_Sequence;

      assume that

       A1: s is convergent and

       A2: a > 0 ;

      per cases ;

        suppose a >= 1;

        hence thesis by A1, Lm6;

      end;

        suppose

         A3: a < 1;

        then (a / a) < (1 / a) by A2, XREAL_1: 74;

        then 1 < (1 / a) by A2, XCMPLX_1: 60;

        then

         A4: ((1 / a) #Q s) is convergent by A1, Lm6;

        s is bounded by A1;

        then

        consider d be Real such that 0 < d and

         A5: for n holds |.(s . n).| < d by SEQ_2: 3;

        reconsider d as Real;

        consider m1 such that

         A6: (2 * d) < m1 by SEQ_4: 3;

        reconsider m1 as Rational;

        

         A7: (a #Q m1) > 0 by A2, Th52;

        now

          let c be Real;

          assume

           A8: c > 0 ;

          then (c * (a #Q m1)) > 0 by A7;

          then

          consider n such that

           A9: for m st n <= m holds |.((((1 / a) #Q s) . m) - (((1 / a) #Q s) . n)).| < (c * (a #Q m1)) by A4, SEQ_4: 41;

          take n;

          let m;

          assume m >= n;

          then

           A10: |.((((1 / a) #Q s) . m) - (((1 / a) #Q s) . n)).| < (c * (a #Q m1)) by A9;

          

           A11: (a #Q (s . m)) <> 0 by A2, Th52;

          

           A12: (a #Q ((s . m) + (s . n))) > 0 by A2, Th52;

           |.(s . m).| < d by A5;

          then

           A13: ( |.(s . m).| + |.(s . n).|) < (d + d) by A5, XREAL_1: 8;

           |.((s . m) + (s . n)).| <= ( |.(s . m).| + |.(s . n).|) by COMPLEX1: 56;

          then |.((s . m) + (s . n)).| < (d + d) by A13, XXREAL_0: 2;

          then |.((s . m) + (s . n)).| < m1 by A6, XXREAL_0: 2;

          then

           A14: |.( - ((s . m) + (s . n))).| < m1 by COMPLEX1: 52;

          ( - ((s . m) + (s . n))) <= |.( - ((s . m) + (s . n))).| by ABSVALUE: 4;

          then ( - ((s . m) + (s . n))) < m1 by A14, XXREAL_0: 2;

          then

           A15: (m1 - ( - ((s . m) + (s . n)))) > 0 by XREAL_1: 50;

          

           A16: (a #Q (s . n)) <> 0 by A2, Th52;

           |.((((1 / a) #Q s) . m) - (((1 / a) #Q s) . n)).| = |.(((1 / a) #Q (s . m)) - (((1 / a) #Q s) . n)).| by Def5

          .= |.(((1 / a) #Q (s . m)) - ((1 / a) #Q (s . n))).| by Def5

          .= |.((1 / (a #Q (s . m))) - ((1 / a) #Q (s . n))).| by A2, Th57

          .= |.((1 / (a #Q (s . m))) - (1 / (a #Q (s . n)))).| by A2, Th57

          .= |.(((a #Q (s . m)) " ) - (1 / (a #Q (s . n)))).|

          .= |.(((a #Q (s . m)) " ) - ((a #Q (s . n)) " )).|

          .= ( |.((a #Q (s . m)) - (a #Q (s . n))).| / ( |.(a #Q (s . m)).| * |.(a #Q (s . n)).|)) by A11, A16, SEQ_2: 2

          .= ( |.((a #Q (s . m)) - (a #Q (s . n))).| / |.((a #Q (s . m)) * (a #Q (s . n))).|) by COMPLEX1: 65

          .= ( |.((a #Q (s . m)) - (a #Q (s . n))).| / |.(a #Q ((s . m) + (s . n))).|) by A2, Th53

          .= ( |.((a #Q (s . m)) - (a #Q (s . n))).| / (a #Q ((s . m) + (s . n)))) by A12, ABSVALUE:def 1;

          then

           A17: (( |.((a #Q (s . m)) - (a #Q (s . n))).| / (a #Q ((s . m) + (s . n)))) * (a #Q ((s . m) + (s . n)))) < ((c * (a #Q m1)) * (a #Q ((s . m) + (s . n)))) by A10, A12, XREAL_1: 68;

          (a #Q ((s . m) + (s . n))) <> 0 by A2, Th52;

          then

           A18: |.((a #Q (s . m)) - (a #Q (s . n))).| < ((c * (a #Q m1)) * (a #Q ((s . m) + (s . n)))) by A17, XCMPLX_1: 87;

          ((a #Q m1) * (a #Q ((s . m) + (s . n)))) = (a #Q (m1 + ((s . m) + (s . n)))) by A2, Th53;

          then (c * ((a #Q m1) * (a #Q ((s . m) + (s . n))))) < (1 * c) by A2, A3, A8, A15, Th65, XREAL_1: 68;

          then |.((a #Q (s . m)) - (a #Q (s . n))).| < c by A18, XXREAL_0: 2;

          then |.(((a #Q s) . m) - (a #Q (s . n))).| < c by Def5;

          hence |.(((a #Q s) . m) - ((a #Q s) . n)).| < c by Def5;

        end;

        hence thesis by SEQ_4: 41;

      end;

    end;

    

     Lm7: for s1,s2 be Rational_Sequence, a st s1 is convergent & s2 is convergent & ( lim s1) = ( lim s2) & a >= 1 holds ( lim (a #Q s1)) = ( lim (a #Q s2))

    proof

      let s1,s2 be Rational_Sequence;

      let a;

      assume that

       A1: s1 is convergent and

       A2: s2 is convergent and

       A3: ( lim s1) = ( lim s2) and

       A4: a >= 1;

      

       A5: (s1 - s2) is convergent by A1, A2;

      

       A6: (a #Q s2) is convergent by A2, A4, Th69;

       A7:

      now

        let n be Element of NAT ;

        

        thus ((((a #Q s1) - (a #Q s2)) + (a #Q s2)) . n) = ((((a #Q s1) - (a #Q s2)) . n) + ((a #Q s2) . n)) by SEQ_1: 7

        .= ((((a #Q s1) . n) - ((a #Q s2) . n)) + ((a #Q s2) . n)) by RFUNCT_2: 1

        .= ((a #Q s1) . n);

      end;

      s2 is bounded by A2;

      then

      consider d be Real such that 0 < d and

       A8: for n holds |.(s2 . n).| < d by SEQ_2: 3;

      consider m2 such that

       A9: d < m2 by SEQ_4: 3;

      reconsider m2 as Rational;

      

       A10: ( lim (s1 - s2)) = (( lim s1) - ( lim s2)) by A1, A2, SEQ_2: 12

      .= 0 by A3;

       A11:

      now

        

         A12: (a #Q m2) >= 0 by A4, Th52;

        let c be Real;

        assume

         A13: c > 0 ;

        consider m1 such that

         A14: (((a #Q m2) * (a - 1)) / c) < m1 by SEQ_4: 3;

        (m1 + 1) >= m1 by XREAL_1: 29;

        then (((a #Q m2) * (a - 1)) / c) < (m1 + 1) by A14, XXREAL_0: 2;

        then ((((a #Q m2) * (a - 1)) / c) * c) < (c * (m1 + 1)) by A13, XREAL_1: 68;

        then ((a #Q m2) * (a - 1)) < (c * (m1 + 1)) by A13, XCMPLX_1: 87;

        then (((a #Q m2) * (a - 1)) / (m1 + 1)) < (((m1 + 1) * c) / (m1 + 1)) by XREAL_1: 74;

        then (((a #Q m2) * (a - 1)) / (m1 + 1)) < ((c / (m1 + 1)) * (m1 + 1));

        then

         A15: (((a #Q m2) * (a - 1)) / (m1 + 1)) < c by XCMPLX_1: 87;

        consider n such that

         A16: for m st n <= m holds |.(((s1 - s2) . m) - 0 ).| < ((m1 + 1) " ) by A5, A10, SEQ_2:def 7;

        take n;

        let m;

        assume m >= n;

        then |.(((s1 - s2) . m) - 0 ).| < ((m1 + 1) " ) by A16;

        then

         A17: |.((s1 . m) - (s2 . m)).| <= ((m1 + 1) " ) by RFUNCT_2: 1;

        

         A18: (m1 + 1) >= ( 0 + 1) by NAT_1: 13;

        then (((m1 + 1) -Root a) - 1) <= ((a - 1) / (m1 + 1)) by A4, Th31;

        then

         A19: ((a #Q m2) * (((m1 + 1) -Root a) - 1)) <= ((a #Q m2) * ((a - 1) / (m1 + 1))) by A12, XREAL_1: 64;

        

         A20: (a #Q (s2 . m)) <> 0 by A4, Th52;

        

         A21: |.((a #Q (s1 . m)) - (a #Q (s2 . m))).| = |.(((a #Q (s1 . m)) - (a #Q (s2 . m))) * 1).|

        .= |.(((a #Q (s1 . m)) - (a #Q (s2 . m))) * ((a #Q (s2 . m)) / (a #Q (s2 . m)))).| by A20, XCMPLX_1: 60

        .= |.(((a #Q (s2 . m)) * ((a #Q (s1 . m)) - (a #Q (s2 . m)))) / (a #Q (s2 . m))).|

        .= |.((a #Q (s2 . m)) * (((a #Q (s1 . m)) - (a #Q (s2 . m))) / (a #Q (s2 . m)))).|

        .= ( |.(a #Q (s2 . m)).| * |.(((a #Q (s1 . m)) - (a #Q (s2 . m))) / (a #Q (s2 . m))).|) by COMPLEX1: 65

        .= ( |.(a #Q (s2 . m)).| * |.(((a #Q (s1 . m)) / (a #Q (s2 . m))) - ((a #Q (s2 . m)) / (a #Q (s2 . m)))).|)

        .= ( |.(a #Q (s2 . m)).| * |.(((a #Q (s1 . m)) / (a #Q (s2 . m))) - 1).|) by A20, XCMPLX_1: 60

        .= ( |.(a #Q (s2 . m)).| * |.((a #Q ((s1 . m) - (s2 . m))) - 1).|) by A4, Th55;

        

         A22: (s2 . m) <= |.(s2 . m).| by ABSVALUE: 4;

        reconsider m3 = ((m1 + 1) " ) as Rational;

        

         A23: |.((a #Q ((s1 . m) - (s2 . m))) - 1).| >= 0 by COMPLEX1: 46;

        

         A24: (a #Q ((s1 . m) - (s2 . m))) <> 0 by A4, Th52;

        ((s1 . m) - (s2 . m)) <= |.((s1 . m) - (s2 . m)).| by ABSVALUE: 4;

        then ((s1 . m) - (s2 . m)) <= ((m1 + 1) " ) by A17, XXREAL_0: 2;

        then (a #Q ((s1 . m) - (s2 . m))) <= (a #Q m3) by A4, Th63;

        then (a #Q ((s1 . m) - (s2 . m))) <= ((m1 + 1) -Root a) by A18, Th50;

        then

         A25: ((a #Q ((s1 . m) - (s2 . m))) - 1) <= (((m1 + 1) -Root a) - 1) by XREAL_1: 9;

        

         A26: (a #Q ((s1 . m) - (s2 . m))) > 0 by A4, Th52;

         A27:

        now

          per cases ;

            suppose ((s1 . m) - (s2 . m)) >= 0 ;

            then (a #Q ((s1 . m) - (s2 . m))) >= 1 by A4, Th60;

            then ((a #Q ((s1 . m) - (s2 . m))) - 1) >= 0 by XREAL_1: 48;

            hence |.((a #Q ((s1 . m) - (s2 . m))) - 1).| <= (((m1 + 1) -Root a) - 1) by A25, ABSVALUE:def 1;

          end;

            suppose

             A28: ((s1 . m) - (s2 . m)) < 0 ;

            

             A29: ( - ((s1 . m) - (s2 . m))) <= |.( - ((s1 . m) - (s2 . m))).| by ABSVALUE: 4;

             |.((s1 . m) - (s2 . m)).| = |.( - ((s1 . m) - (s2 . m))).| by COMPLEX1: 52;

            then ( - ((s1 . m) - (s2 . m))) <= m3 by A17, A29, XXREAL_0: 2;

            then (a #Q ( - ((s1 . m) - (s2 . m)))) <= (a #Q m3) by A4, Th63;

            then (a #Q ( - ((s1 . m) - (s2 . m)))) <= ((m1 + 1) -Root a) by A18, Th50;

            then

             A30: ((a #Q ( - ((s1 . m) - (s2 . m)))) - 1) <= (((m1 + 1) -Root a) - 1) by XREAL_1: 9;

            (a #Q ( - ((s1 . m) - (s2 . m)))) >= 1 by A4, A28, Th60;

            then ((a #Q ( - ((s1 . m) - (s2 . m)))) - 1) >= 0 by XREAL_1: 48;

            then

             A31: |.((a #Q ( - ((s1 . m) - (s2 . m)))) - 1).| <= (((m1 + 1) -Root a) - 1) by A30, ABSVALUE:def 1;

            (a #Q ((s1 . m) - (s2 . m))) <= 1 by A4, A28, Th61;

            then

             A32: |.(a #Q ((s1 . m) - (s2 . m))).| <= 1 by A26, ABSVALUE:def 1;

             |.((a #Q ( - ((s1 . m) - (s2 . m)))) - 1).| >= 0 by COMPLEX1: 46;

            then

             A33: ( |.(a #Q ((s1 . m) - (s2 . m))).| * |.((a #Q ( - ((s1 . m) - (s2 . m)))) - 1).|) <= (1 * |.((a #Q ( - ((s1 . m) - (s2 . m)))) - 1).|) by A32, XREAL_1: 64;

             |.((a #Q ((s1 . m) - (s2 . m))) - 1).| = |.(((a #Q ((s1 . m) - (s2 . m))) - 1) * 1).|

            .= |.(((a #Q ((s1 . m) - (s2 . m))) - 1) * ((a #Q ((s1 . m) - (s2 . m))) / (a #Q ((s1 . m) - (s2 . m))))).| by A24, XCMPLX_1: 60

            .= |.(((a #Q ((s1 . m) - (s2 . m))) * ((a #Q ((s1 . m) - (s2 . m))) - 1)) / (a #Q ((s1 . m) - (s2 . m)))).|

            .= |.((a #Q ((s1 . m) - (s2 . m))) * (((a #Q ((s1 . m) - (s2 . m))) - 1) / (a #Q ((s1 . m) - (s2 . m))))).|

            .= ( |.(a #Q ((s1 . m) - (s2 . m))).| * |.(((a #Q ((s1 . m) - (s2 . m))) - 1) / (a #Q ((s1 . m) - (s2 . m)))).|) by COMPLEX1: 65

            .= ( |.(a #Q ((s1 . m) - (s2 . m))).| * |.(((a #Q ((s1 . m) - (s2 . m))) / (a #Q ((s1 . m) - (s2 . m)))) - (1 / (a #Q ((s1 . m) - (s2 . m))))).|)

            .= ( |.(a #Q ((s1 . m) - (s2 . m))).| * |.(1 - (1 / (a #Q ((s1 . m) - (s2 . m))))).|) by A24, XCMPLX_1: 60

            .= ( |.(a #Q ((s1 . m) - (s2 . m))).| * |.(1 - (a #Q ( - ((s1 . m) - (s2 . m))))).|) by A4, Th54

            .= ( |.(a #Q ((s1 . m) - (s2 . m))).| * |.( - (1 - (a #Q ( - ((s1 . m) - (s2 . m)))))).|) by COMPLEX1: 52

            .= ( |.(a #Q ((s1 . m) - (s2 . m))).| * |.((a #Q ( - ((s1 . m) - (s2 . m)))) - 1).|);

            hence |.((a #Q ((s1 . m) - (s2 . m))) - 1).| <= (((m1 + 1) -Root a) - 1) by A31, A33, XXREAL_0: 2;

          end;

        end;

        

         A34: (a #Q (s2 . m)) > 0 by A4, Th52;

         |.(s2 . m).| <= m2 by A8, A9, XXREAL_0: 2;

        then (s2 . m) <= m2 by A22, XXREAL_0: 2;

        then (a #Q (s2 . m)) <= (a #Q m2) by A4, Th63;

        then

         A35: |.(a #Q (s2 . m)).| <= (a #Q m2) by A34, ABSVALUE:def 1;

         |.(a #Q (s2 . m)).| >= 0 by A34, ABSVALUE:def 1;

        then ( |.(a #Q (s2 . m)).| * |.((a #Q ((s1 . m) - (s2 . m))) - 1).|) <= ((a #Q m2) * (((m1 + 1) -Root a) - 1)) by A27, A23, A35, XREAL_1: 66;

        then |.((a #Q (s1 . m)) - (a #Q (s2 . m))).| <= (((a #Q m2) * (a - 1)) / (m1 + 1)) by A21, A19, XXREAL_0: 2;

        then |.((a #Q (s1 . m)) - (a #Q (s2 . m))).| < c by A15, XXREAL_0: 2;

        then |.(((a #Q s1) . m) - (a #Q (s2 . m))).| < c by Def5;

        then |.(((a #Q s1) . m) - ((a #Q s2) . m)).| < c by Def5;

        hence |.((((a #Q s1) - (a #Q s2)) . m) - 0 ).| < c by RFUNCT_2: 1;

      end;

      then

       A36: ((a #Q s1) - (a #Q s2)) is convergent by SEQ_2:def 6;

      then ( lim ((a #Q s1) - (a #Q s2))) = 0 by A11, SEQ_2:def 7;

      

      then ( lim (((a #Q s1) - (a #Q s2)) + (a #Q s2))) = ( 0 + ( lim (a #Q s2))) by A36, A6, SEQ_2: 6

      .= ( lim (a #Q s2));

      hence thesis by A7, FUNCT_2: 63;

    end;

    theorem :: PREPOWER:70

    

     Th70: for s1,s2 be Rational_Sequence, a st s1 is convergent & s2 is convergent & ( lim s1) = ( lim s2) & a > 0 holds (a #Q s1) is convergent & (a #Q s2) is convergent & ( lim (a #Q s1)) = ( lim (a #Q s2))

    proof

      let s1,s2 be Rational_Sequence;

      let a;

      assume that

       A1: s1 is convergent and

       A2: s2 is convergent and

       A3: ( lim s1) = ( lim s2) and

       A4: a > 0 ;

      thus

       A5: (a #Q s1) is convergent by A1, A4, Th69;

      s2 is bounded by A2;

      then

      consider e be Real such that 0 < e and

       A6: for n holds |.(s2 . n).| < e by SEQ_2: 3;

      s1 is bounded by A1;

      then

      consider d be Real such that 0 < d and

       A7: for n holds |.(s1 . n).| < d by SEQ_2: 3;

      consider m1 such that

       A8: (d + e) < m1 by SEQ_4: 3;

      thus

       A9: (a #Q s2) is convergent by A2, A4, Th69;

      reconsider m1 as Rational;

      

       A10: (a #Q m1) > 0 by A4, Th52;

      per cases ;

        suppose a >= 1;

        hence thesis by A1, A2, A3, Lm7;

      end;

        suppose

         A11: a < 1;

        then (a / a) < (1 / a) by A4, XREAL_1: 74;

        then 1 < (1 / a) by A4, XCMPLX_1: 60;

        then

         A12: ( lim ((1 / a) #Q s1)) = ( lim ((1 / a) #Q s2)) by A1, A2, A3, Lm7;

        

         A13: ((1 / a) #Q s2) is convergent by A2, A4, Th69;

        

         A14: ((1 / a) #Q s1) is convergent by A1, A4, Th69;

        then

         A15: (((1 / a) #Q s1) - ((1 / a) #Q s2)) is convergent by A13;

        

         A16: ( lim (((1 / a) #Q s1) - ((1 / a) #Q s2))) = (( lim ((1 / a) #Q s1)) - ( lim ((1 / a) #Q s2))) by A14, A13, SEQ_2: 12

        .= 0 by A12;

         A17:

        now

          let c be Real;

          assume

           A18: c > 0 ;

          then (c * (a #Q m1)) > 0 by A10;

          then

          consider n such that

           A19: for m st n <= m holds |.(((((1 / a) #Q s1) - ((1 / a) #Q s2)) . m) - 0 ).| < (c * (a #Q m1)) by A15, A16, SEQ_2:def 7;

          take n;

          let m;

          assume m >= n;

          then |.(((((1 / a) #Q s1) - ((1 / a) #Q s2)) . m) - 0 ).| < (c * (a #Q m1)) by A19;

          then

           A20: |.((((1 / a) #Q s1) . m) - (((1 / a) #Q s2) . m)).| < (c * (a #Q m1)) by RFUNCT_2: 1;

          

           A21: (a #Q (s1 . m)) <> 0 by A4, Th52;

           |.(s1 . m).| < d by A7;

          then

           A22: ( |.(s1 . m).| + |.(s2 . m).|) < (d + e) by A6, XREAL_1: 8;

           |.((s1 . m) + (s2 . m)).| <= ( |.(s1 . m).| + |.(s2 . m).|) by COMPLEX1: 56;

          then |.((s1 . m) + (s2 . m)).| < (d + e) by A22, XXREAL_0: 2;

          then |.((s1 . m) + (s2 . m)).| < m1 by A8, XXREAL_0: 2;

          then

           A23: |.( - ((s1 . m) + (s2 . m))).| < m1 by COMPLEX1: 52;

          ( - ((s1 . m) + (s2 . m))) <= |.( - ((s1 . m) + (s2 . m))).| by ABSVALUE: 4;

          then ( - ((s1 . m) + (s2 . m))) < m1 by A23, XXREAL_0: 2;

          then

           A24: (m1 - ( - ((s1 . m) + (s2 . m)))) > 0 by XREAL_1: 50;

          

           A25: (a #Q (s2 . m)) <> 0 by A4, Th52;

          

           A26: (a #Q ((s1 . m) + (s2 . m))) > 0 by A4, Th52;

           |.((((1 / a) #Q s1) . m) - (((1 / a) #Q s2) . m)).| = |.(((1 / a) #Q (s1 . m)) - (((1 / a) #Q s2) . m)).| by Def5

          .= |.(((1 / a) #Q (s1 . m)) - ((1 / a) #Q (s2 . m))).| by Def5

          .= |.((1 / (a #Q (s1 . m))) - ((1 / a) #Q (s2 . m))).| by A4, Th57

          .= |.((1 / (a #Q (s1 . m))) - (1 / (a #Q (s2 . m)))).| by A4, Th57

          .= |.(((a #Q (s1 . m)) " ) - (1 / (a #Q (s2 . m)))).|

          .= |.(((a #Q (s1 . m)) " ) - ((a #Q (s2 . m)) " )).|

          .= ( |.((a #Q (s1 . m)) - (a #Q (s2 . m))).| / ( |.(a #Q (s1 . m)).| * |.(a #Q (s2 . m)).|)) by A21, A25, SEQ_2: 2

          .= ( |.((a #Q (s1 . m)) - (a #Q (s2 . m))).| / |.((a #Q (s1 . m)) * (a #Q (s2 . m))).|) by COMPLEX1: 65

          .= ( |.((a #Q (s1 . m)) - (a #Q (s2 . m))).| / |.(a #Q ((s1 . m) + (s2 . m))).|) by A4, Th53

          .= ( |.((a #Q (s1 . m)) - (a #Q (s2 . m))).| / (a #Q ((s1 . m) + (s2 . m)))) by A26, ABSVALUE:def 1;

          then

           A27: (( |.((a #Q (s1 . m)) - (a #Q (s2 . m))).| / (a #Q ((s1 . m) + (s2 . m)))) * (a #Q ((s1 . m) + (s2 . m)))) < ((c * (a #Q m1)) * (a #Q ((s1 . m) + (s2 . m)))) by A20, A26, XREAL_1: 68;

          (a #Q ((s1 . m) + (s2 . m))) <> 0 by A4, Th52;

          then

           A28: |.((a #Q (s1 . m)) - (a #Q (s2 . m))).| < ((c * (a #Q m1)) * (a #Q ((s1 . m) + (s2 . m)))) by A27, XCMPLX_1: 87;

          ((a #Q m1) * (a #Q ((s1 . m) + (s2 . m)))) = (a #Q (m1 + ((s1 . m) + (s2 . m)))) by A4, Th53;

          then (c * ((a #Q m1) * (a #Q ((s1 . m) + (s2 . m))))) < (1 * c) by A4, A11, A18, A24, Th65, XREAL_1: 68;

          then |.((a #Q (s1 . m)) - (a #Q (s2 . m))).| < c by A28, XXREAL_0: 2;

          then |.(((a #Q s1) . m) - (a #Q (s2 . m))).| < c by Def5;

          then |.(((a #Q s1) . m) - ((a #Q s2) . m)).| < c by Def5;

          hence |.((((a #Q s1) - (a #Q s2)) . m) - 0 ).| < c by RFUNCT_2: 1;

        end;

        then ((a #Q s1) - (a #Q s2)) is convergent by SEQ_2:def 6;

        then ( lim ((a #Q s1) - (a #Q s2))) = 0 by A17, SEQ_2:def 7;

        then 0 = (( lim (a #Q s1)) - ( lim (a #Q s2))) by A5, A9, SEQ_2: 12;

        hence thesis;

      end;

    end;

    definition

      let a,b be Real;

      assume

       A1: a > 0 ;

      :: PREPOWER:def7

      func a #R b -> Real means

      : Def6: ex s be Rational_Sequence st s is convergent & ( lim s) = b & (a #Q s) is convergent & ( lim (a #Q s)) = it ;

      existence

      proof

        consider s be Rational_Sequence such that

         A2: s is convergent and

         A3: ( lim s) = b and for n holds (s . n) <= b by Th67;

        take IT = ( lim (a #Q s));

        thus thesis by A1, A2, A3, Th69;

      end;

      uniqueness by A1, Th70;

    end

    theorem :: PREPOWER:71

    

     Th71: a > 0 implies (a #R 0 ) = 1

    proof

      set s = ( seq_const 0 );

      reconsider s as Rational_Sequence;

      assume

       A1: a > 0 ;

      (s . 0 ) = 0 ;

      then

       A2: ( lim s) = 0 by SEQ_4: 26;

      reconsider j = 1 as Element of REAL by NUMBERS: 19;

       A3:

      now

        let n be Nat;

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

        

        thus ((a #Q s) . n) = (a #Q (s . nn)) by Def5

        .= j by Th47;

      end;

      then

       A4: (a #Q s) is constant by VALUED_0:def 18;

      ((a #Q s) . 0 ) = 1 by A3;

      then ( lim (a #Q s)) = 1 by A4, SEQ_4: 26;

      hence thesis by A1, A2, A4, Def6;

    end;

    theorem :: PREPOWER:72

    a > 0 implies (a #R 1) = a

    proof

      set s = ( seq_const 1);

      reconsider s as Rational_Sequence;

      (s . 0 ) = 1 by SEQ_1: 57;

      then

       A1: ( lim s) = 1 by SEQ_4: 26;

      assume

       A2: a > 0 ;

       A3:

      now

        let n be Nat;

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

        

        thus ((a #Q s) . n) = (a #Q (s . nn)) by Def5

        .= a by A2, Th48, SEQ_1: 57;

      end;

      a in REAL by XREAL_0:def 1;

      then

       A4: (a #Q s) is constant by A3, VALUED_0:def 18;

      ((a #Q s) . 0 ) = a by A3;

      then ( lim (a #Q s)) = a by A4, SEQ_4: 26;

      hence thesis by A2, A1, A4, Def6;

    end;

    theorem :: PREPOWER:73

    

     Th73: (1 #R a) = 1

    proof

      consider s be Rational_Sequence such that

       A1: s is convergent and

       A2: a = ( lim s) and for n holds (s . n) <= a by Th67;

      reconsider j = 1 as Element of REAL by NUMBERS: 19;

       A3:

      now

        let n be Nat;

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

        

        thus ((j #Q s) . n) = (j #Q (s . nn)) by Def5

        .= j by Th51;

      end;

      then (j #Q s) is constant by VALUED_0:def 18;

      

      then

       A4: ( lim (1 #Q s)) = ((1 #Q s) . 0 ) by SEQ_4: 26

      .= 1 by A3;

      (1 #Q s) is convergent by A1, Th69;

      hence thesis by A1, A2, A4, Def6;

    end;

    theorem :: PREPOWER:74

    

     Th74: a > 0 implies (a #R p) = (a #Q p)

    proof

      assume

       A1: a > 0 ;

      set s = ( seq_const p);

      

       A2: ( lim s) = (s . 0 ) by SEQ_4: 26

      .= p by FUNCOP_1: 7;

      reconsider s as Rational_Sequence;

       A3:

      now

        let n be Nat;

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

        

        thus ((a #Q s) . n) = (a #Q (s . nn)) by Def5

        .= (a #Q p) by FUNCOP_1: 7;

      end;

      (a #Q p) in REAL by XREAL_0:def 1;

      then

       A4: (a #Q s) is constant by A3, VALUED_0:def 18;

      

      then ( lim (a #Q s)) = ((a #Q s) . 0 ) by SEQ_4: 26

      .= (a #Q p) by A3;

      hence thesis by A1, A2, A4, Def6;

    end;

    theorem :: PREPOWER:75

    

     Th75: a > 0 implies (a #R (b + c)) = ((a #R b) * (a #R c))

    proof

      consider sb be Rational_Sequence such that

       A1: sb is convergent and

       A2: b = ( lim sb) and for n holds (sb . n) <= b by Th67;

      consider sc be Rational_Sequence such that

       A3: sc is convergent and

       A4: c = ( lim sc) and for n holds (sc . n) <= c by Th67;

      assume

       A5: a > 0 ;

      then

       A6: (a #Q sb) is convergent by A1, Th69;

      

       A7: (a #Q sc) is convergent by A5, A3, Th69;

      reconsider s = (sb + sc) as Rational_Sequence;

      

       A8: ( lim s) = (b + c) by A1, A2, A3, A4, SEQ_2: 6;

       A9:

      now

        let n;

        

        thus ((a #Q s) . n) = (a #Q (s . n)) by Def5

        .= (a #Q ((sb . n) + (sc . n))) by SEQ_1: 7

        .= ((a #Q (sb . n)) * (a #Q (sc . n))) by A5, Th53

        .= ((a #Q (sb . n)) * ((a #Q sc) . n)) by Def5

        .= (((a #Q sb) . n) * ((a #Q sc) . n)) by Def5;

      end;

      

       A10: s is convergent by A1, A3;

      then (a #Q s) is convergent by A5, Th69;

      

      hence (a #R (b + c)) = ( lim (a #Q s)) by A5, A10, A8, Def6

      .= ( lim ((a #Q sb) (#) (a #Q sc))) by A9, SEQ_1: 8

      .= (( lim (a #Q sb)) * ( lim (a #Q sc))) by A6, A7, SEQ_2: 15

      .= ((a #R b) * ( lim (a #Q sc))) by A5, A1, A2, A6, Def6

      .= ((a #R b) * (a #R c)) by A5, A3, A4, A7, Def6;

    end;

    

     Lm8: a > 0 implies (a #R b) >= 0

    proof

      consider s be Rational_Sequence such that

       A1: s is convergent and

       A2: b = ( lim s) and for n holds (s . n) <= b by Th67;

      assume

       A3: a > 0 ;

       A4:

      now

        let n;

        ((a #Q s) . n) = (a #Q (s . n)) by Def5;

        hence ((a #Q s) . n) >= 0 by A3, Th52;

      end;

      (a #Q s) is convergent by A3, A1, Th69;

      then (a #R b) = ( lim (a #Q s)) by A3, A1, A2, Def6;

      hence thesis by A3, A1, A4, Th69, SEQ_2: 17;

    end;

    

     Lm9: a > 0 implies (a #R b) <> 0

    proof

      assume

       A1: a > 0 ;

      assume (a #R b) = 0 ;

      

      then 0 = ((a #R b) * (a #R ( - b)))

      .= (a #R (b + ( - b))) by A1, Th75

      .= 1 by A1, Th71;

      hence contradiction;

    end;

    theorem :: PREPOWER:76

    

     Th76: a > 0 implies (a #R ( - c)) = (1 / (a #R c))

    proof

      assume

       A1: a > 0 ;

      

      then 1 = (a #R (c + ( - c))) by Th71

      .= ((a #R ( - c)) * (a #R c)) by A1, Th75;

      

      then (1 / (a #R c)) = ((a #R ( - c)) * ((a #R c) / (a #R c))) by XCMPLX_1: 74

      .= ((a #R ( - c)) * 1) by A1, Lm9, XCMPLX_1: 60;

      hence thesis;

    end;

    theorem :: PREPOWER:77

    

     Th77: a > 0 implies (a #R (b - c)) = ((a #R b) / (a #R c))

    proof

      assume

       A1: a > 0 ;

      

      thus (a #R (b - c)) = (a #R (b + ( - c)))

      .= ((a #R b) * (a #R ( - c))) by A1, Th75

      .= ((a #R b) * (1 / (a #R c))) by A1, Th76

      .= ((a #R b) * (1 * ((a #R c) " )))

      .= ((a #R b) / (a #R c));

    end;

    theorem :: PREPOWER:78

    

     Th78: a > 0 & b > 0 implies ((a * b) #R c) = ((a #R c) * (b #R c))

    proof

      assume that

       A1: a > 0 and

       A2: b > 0 ;

      

       A3: (a * b) > 0 by A1, A2;

      consider s1 be Rational_Sequence such that

       A4: s1 is convergent and

       A5: c = ( lim s1) and for n holds (s1 . n) >= c by Th68;

      

       A6: (a #Q s1) is convergent by A1, A4, Th69;

      

       A7: (b #Q s1) is convergent by A2, A4, Th69;

      now

        let n;

        

        thus (((a * b) #Q s1) . n) = ((a * b) #Q (s1 . n)) by Def5

        .= ((a #Q (s1 . n)) * (b #Q (s1 . n))) by A1, A2, Th56

        .= (((a #Q s1) . n) * (b #Q (s1 . n))) by Def5

        .= (((a #Q s1) . n) * ((b #Q s1) . n)) by Def5;

      end;

      then

       A8: ((a * b) #Q s1) = ((a #Q s1) (#) (b #Q s1)) by SEQ_1: 8;

      then ((a * b) #Q s1) is convergent by A6, A7;

      

      hence ((a * b) #R c) = ( lim ((a * b) #Q s1)) by A3, A4, A5, Def6

      .= (( lim (a #Q s1)) * ( lim (b #Q s1))) by A6, A7, A8, SEQ_2: 15

      .= ((a #R c) * ( lim (b #Q s1))) by A1, A4, A5, A6, Def6

      .= ((a #R c) * (b #R c)) by A2, A4, A5, A7, Def6;

    end;

    theorem :: PREPOWER:79

    

     Th79: a > 0 implies ((1 / a) #R c) = (1 / (a #R c))

    proof

      assume

       A1: a > 0 ;

      1 = (1 #R c) by Th73

      .= (((1 / a) * a) #R c) by A1, XCMPLX_1: 106

      .= (((1 / a) #R c) * (a #R c)) by A1, Th78;

      

      then (1 / (a #R c)) = (((1 / a) #R c) * ((a #R c) / (a #R c))) by XCMPLX_1: 74

      .= (((1 / a) #R c) * 1) by A1, Lm9, XCMPLX_1: 60;

      hence thesis;

    end;

    theorem :: PREPOWER:80

    a > 0 & b > 0 implies ((a / b) #R c) = ((a #R c) / (b #R c))

    proof

      assume that

       A1: a > 0 and

       A2: b > 0 ;

      

      thus ((a / b) #R c) = ((a * (b " )) #R c)

      .= ((a #R c) * ((b " ) #R c)) by A1, A2, Th78

      .= ((a #R c) * ((1 / b) #R c))

      .= ((a #R c) * (1 / (b #R c))) by A2, Th79

      .= (((a #R c) * 1) / (b #R c))

      .= ((a #R c) / (b #R c));

    end;

    theorem :: PREPOWER:81

    

     Th81: a > 0 implies (a #R b) > 0

    proof

      assume

       A1: a > 0 ;

      then (a #R b) <> 0 by Lm9;

      hence thesis by A1, Lm8;

    end;

    theorem :: PREPOWER:82

    

     Th82: a >= 1 & c >= b implies (a #R c) >= (a #R b)

    proof

      assume that

       A1: a >= 1 and

       A2: c >= b;

      consider s1 be Rational_Sequence such that

       A3: s1 is convergent and

       A4: c = ( lim s1) and

       A5: for n holds (s1 . n) >= c by Th68;

      

       A6: (a #Q s1) is convergent by A1, A3, Th69;

      consider s2 be Rational_Sequence such that

       A7: s2 is convergent and

       A8: b = ( lim s2) and

       A9: for n holds (s2 . n) <= b by Th67;

      

       A10: (a #Q s2) is convergent by A1, A7, Th69;

      now

        let n;

        (s1 . n) >= c by A5;

        then

         A11: (s1 . n) >= b by A2, XXREAL_0: 2;

        (s2 . n) <= b by A9;

        then (s1 . n) >= (s2 . n) by A11, XXREAL_0: 2;

        then (a #Q (s1 . n)) >= (a #Q (s2 . n)) by A1, Th63;

        then (a #Q (s1 . n)) >= ((a #Q s2) . n) by Def5;

        hence ((a #Q s1) . n) >= ((a #Q s2) . n) by Def5;

      end;

      then ( lim (a #Q s1)) >= ( lim (a #Q s2)) by A6, A10, SEQ_2: 18;

      then (a #R c) >= ( lim (a #Q s2)) by A1, A3, A4, A6, Def6;

      hence thesis by A1, A7, A8, A10, Def6;

    end;

    theorem :: PREPOWER:83

    

     Th83: a > 1 & c > b implies (a #R c) > (a #R b)

    proof

      assume that

       A1: a > 1 and

       A2: c > b;

      consider p such that

       A3: b < p and

       A4: p < c by A2, RAT_1: 7;

      consider q such that

       A5: b < q and

       A6: q < p by A3, RAT_1: 7;

      consider s2 be Rational_Sequence such that

       A7: s2 is convergent and

       A8: b = ( lim s2) and

       A9: for n holds (s2 . n) <= b by Th67;

      

       A10: (a #Q q) < (a #Q p) by A1, A6, Th64;

      now

        let n;

        (s2 . n) <= b by A9;

        then (s2 . n) <= q by A5, XXREAL_0: 2;

        then (a #Q (s2 . n)) <= (a #Q q) by A1, Th63;

        hence ((a #Q s2) . n) <= (a #Q q) by Def5;

      end;

      then

       A11: ( lim (a #Q s2)) <= (a #Q q) by A1, A7, Th2, Th69;

      (a #Q s2) is convergent by A1, A7, Th69;

      then (a #R b) <= (a #Q q) by A1, A7, A8, A11, Def6;

      then

       A12: (a #R b) < (a #Q p) by A10, XXREAL_0: 2;

      consider s1 be Rational_Sequence such that

       A13: s1 is convergent and

       A14: c = ( lim s1) and

       A15: for n holds (s1 . n) >= c by Th68;

      now

        let n;

        (s1 . n) >= c by A15;

        then (s1 . n) >= p by A4, XXREAL_0: 2;

        then (a #Q (s1 . n)) >= (a #Q p) by A1, Th63;

        hence ((a #Q s1) . n) >= (a #Q p) by Def5;

      end;

      then

       A16: ( lim (a #Q s1)) >= (a #Q p) by A1, A13, Th1, Th69;

      (a #Q s1) is convergent by A1, A13, Th69;

      then (a #R c) >= (a #Q p) by A1, A13, A14, A16, Def6;

      hence thesis by A12, XXREAL_0: 2;

    end;

    theorem :: PREPOWER:84

    

     Th84: a > 0 & a <= 1 & c >= b implies (a #R c) <= (a #R b)

    proof

      assume that

       A1: a > 0 and

       A2: a <= 1 and

       A3: c >= b;

      (1 / a) >= 1 by A1, A2, Lm4, XREAL_1: 85;

      then ((1 / a) #R c) >= ((1 / a) #R b) by A3, Th82;

      then (1 / (a #R c)) >= ((1 / a) #R b) by A1, Th79;

      then

       A4: (1 / (a #R c)) >= (1 / (a #R b)) by A1, Th79;

      (a #R b) > 0 by A1, Th81;

      hence thesis by A4, XREAL_1: 89;

    end;

    theorem :: PREPOWER:85

    

     Th85: a >= 1 & b >= 0 implies (a #R b) >= 1

    proof

      assume that

       A1: a >= 1 and

       A2: b >= 0 ;

      consider s be Rational_Sequence such that

       A3: s is convergent and

       A4: b = ( lim s) and

       A5: for n holds (s . n) >= b by Th68;

       A6:

      now

        let n;

        

         A7: ((a #Q s) . n) = (a #Q (s . n)) by Def5;

        (s . n) >= b by A5;

        hence ((a #Q s) . n) >= 1 by A1, A2, A7, Th60;

      end;

      (a #Q s) is convergent by A1, A3, Th69;

      then (a #R b) = ( lim (a #Q s)) by A1, A3, A4, Def6;

      hence thesis by A1, A3, A6, Th1, Th69;

    end;

    theorem :: PREPOWER:86

    

     Th86: a > 1 & b > 0 implies (a #R b) > 1

    proof

      assume that

       A1: a > 1 and

       A2: b > 0 ;

      (a #R b) > (a #R 0 ) by A1, A2, Th83;

      hence thesis by A1, Th71;

    end;

    theorem :: PREPOWER:87

    

     Th87: a >= 1 & b <= 0 implies (a #R b) <= 1

    proof

      assume that

       A1: a >= 1 and

       A2: b <= 0 ;

      (a #R ( - b)) >= 1 by A1, A2, Th85;

      then (1 / (a #R b)) >= 1 by A1, Th76;

      then (1 / (1 / (a #R b))) <= 1 by XREAL_1: 211;

      hence thesis;

    end;

    theorem :: PREPOWER:88

    a > 1 & b < 0 implies (a #R b) < 1

    proof

      assume that

       A1: a > 1 and

       A2: b < 0 ;

      ( - b) > 0 by A2;

      then (a #R ( - b)) > 1 by A1, Th86;

      then (1 / (a #R b)) > 1 by A1, Th76;

      then (1 / (1 / (a #R b))) < 1 by XREAL_1: 212;

      hence thesis;

    end;

    

     Lm10: s1 is convergent & s2 is convergent & ( lim s1) > 0 & p >= 0 & (for n holds (s1 . n) > 0 & (s2 . n) = ((s1 . n) #Q p)) implies ( lim s2) = (( lim s1) #Q p)

    proof

      assume that

       A1: s1 is convergent and

       A2: s2 is convergent and

       A3: ( lim s1) > 0 and

       A4: p >= 0 and

       A5: for n holds (s1 . n) > 0 & (s2 . n) = ((s1 . n) #Q p);

      reconsider ls = ( lim s1) as Element of REAL by XREAL_0:def 1;

      set s = ( seq_const ( lim s1));

      consider m0 be Nat such that

       A6: p < m0 by SEQ_4: 3;

      

       A7: ( lim s) = (s . 0 ) by SEQ_4: 26

      .= ( lim s1) by FUNCOP_1: 7;

      then

       A8: (s1 /" s) is convergent by A1, A3, SEQ_2: 23;

      deffunc O( Nat) = (((s /" s1) . $1) |^ m0);

      consider s3 be Real_Sequence such that

       A9: for n holds (s3 . n) = O(n) from SEQ_1:sch 1;

      for n holds (s1 . n) <> 0 by A5;

      then

       A10: s1 is non-zero by SEQ_1: 5;

      then

       A11: (s /" s1) is convergent by A1, A3, SEQ_2: 23;

      then

       A12: s3 is convergent by A9, Th18;

      reconsider q = m0 as Rational;

      deffunc O( Nat) = (((s1 /" s) . $1) |^ m0);

      consider s4 be Real_Sequence such that

       A13: for n holds (s4 . n) = O(n) from SEQ_1:sch 1;

      ( lim (s /" s1)) = (( lim s) / ( lim s1)) by A1, A3, A10, SEQ_2: 24

      .= 1 by A3, A7, XCMPLX_1: 60;

      then ( lim s3) = (1 |^ m0) by A11, A9, Th18;

      then

       A14: ( lim s3) = 1;

      ( lim (s1 /" s)) = (( lim s1) / ( lim s)) by A1, A3, A7, SEQ_2: 24

      .= 1 by A3, A7, XCMPLX_1: 60;

      then ( lim s4) = (1 |^ m0) by A8, A13, Th18;

      then

       A15: ( lim s4) = 1;

      s2 is bounded by A2;

      then

      consider d be Real such that

       A16: d > 0 and

       A17: for n holds |.(s2 . n).| < d by SEQ_2: 3;

      

       A18: s4 is convergent by A8, A13, Th18;

      now

        let c be Real;

        assume

         A19: c > 0 ;

        then (c / d) > 0 by A16;

        then

        consider m1 such that

         A20: for m st m >= m1 holds |.((s3 . m) - 1).| < (c / d) by A12, A14, SEQ_2:def 7;

        

         A21: (( lim s1) #Q p) > 0 by A3, Th52;

        then

         A22: |.(( lim s1) #Q p).| > 0 by ABSVALUE:def 1;

        then (c / |.(( lim s1) #Q p).|) > 0 by A19;

        then

        consider m2 such that

         A23: for m st m >= m2 holds |.((s4 . m) - 1).| < (c / |.(( lim s1) #Q p).|) by A18, A15, SEQ_2:def 7;

        take n = (m1 + m2);

        let m such that

         A24: m >= n;

        m2 <= n by NAT_1: 11;

        then

         A25: m >= m2 by A24, XXREAL_0: 2;

        m1 <= n by NAT_1: 11;

        then

         A26: m >= m1 by A24, XXREAL_0: 2;

        now

          per cases ;

            suppose

             A27: (s1 . m) >= ( lim s1);

            m in NAT by ORDINAL1:def 12;

            

            then

             A28: ((s1 . m) / ( lim s1)) = ((s1 . m) / (s . m)) by FUNCOP_1: 7

            .= ((s1 . m) * ((s . m) " ))

            .= ((s1 . m) * ((s " ) . m)) by VALUED_1: 10

            .= ((s1 /" s) . m) by SEQ_1: 8;

            ((s1 . m) * (( lim s1) " )) >= (( lim s1) * (( lim s1) " )) by A3, A27, XREAL_1: 64;

            then

             A29: ((s1 /" s) . m) >= 1 by A3, A28, XCMPLX_0:def 7;

            then (((s1 /" s) . m) #Q p) <= (((s1 /" s) . m) #Q q) by A6, Th63;

            then (((s1 /" s) . m) #Q p) <= (((s1 /" s) . m) |^ m0) by A29, Th49;

            then

             A30: ((((s1 /" s) . m) #Q p) - 1) <= ((((s1 /" s) . m) |^ m0) - 1) by XREAL_1: 9;

            (((s1 /" s) . m) #Q p) >= 1 by A4, A29, Th60;

            then ((((s1 /" s) . m) #Q p) - 1) >= (1 - 1) by XREAL_1: 9;

            then

             A31: ((((s1 /" s) . m) #Q p) - 1) = |.((((s1 /" s) . m) #Q p) - 1).| by ABSVALUE:def 1;

            

             A32: (( lim s1) #Q p) <> 0 by A3, Th52;

            

             A33: |.((s4 . m) - 1).| < (c / |.(( lim s1) #Q p).|) by A23, A25;

            

             A34: (s1 . m) > 0 by A5;

            (((s1 /" s) . m) |^ m0) >= 1 by A29, Th11;

            then ((((s1 /" s) . m) |^ m0) - 1) >= (1 - 1) by XREAL_1: 9;

            then |.((((s1 /" s) . m) #Q p) - 1).| <= |.((((s1 /" s) . m) |^ m0) - 1).| by A30, A31, ABSVALUE:def 1;

            then |.((((s1 /" s) . m) #Q p) - 1).| <= |.((s4 . m) - 1).| by A13;

            then

             A35: |.((((s1 /" s) . m) #Q p) - 1).| < (c / |.(( lim s1) #Q p).|) by A33, XXREAL_0: 2;

            

             A36: |.(( lim s1) #Q p).| <> 0 by A21, ABSVALUE:def 1;

             |.((s2 . m) - (( lim s1) #Q p)).| = |.((((s1 . m) #Q p) - (( lim s1) #Q p)) * 1).| by A5

            .= |.((((s1 . m) #Q p) - (( lim s1) #Q p)) * ((( lim s1) #Q p) / (( lim s1) #Q p))).| by A32, XCMPLX_1: 60

            .= |.(((( lim s1) #Q p) * (((s1 . m) #Q p) - (( lim s1) #Q p))) / (( lim s1) #Q p)).|

            .= |.((( lim s1) #Q p) * ((((s1 . m) #Q p) - (( lim s1) #Q p)) / (( lim s1) #Q p))).|

            .= ( |.(( lim s1) #Q p).| * |.((((s1 . m) #Q p) - (( lim s1) #Q p)) / (( lim s1) #Q p)).|) by COMPLEX1: 65

            .= ( |.(( lim s1) #Q p).| * |.((((s1 . m) #Q p) / (( lim s1) #Q p)) - ((( lim s1) #Q p) / (( lim s1) #Q p))).|)

            .= ( |.(( lim s1) #Q p).| * |.((((s1 . m) #Q p) / (( lim s1) #Q p)) - 1).|) by A32, XCMPLX_1: 60

            .= ( |.(( lim s1) #Q p).| * |.((((s1 . m) / ( lim s1)) #Q p) - 1).|) by A3, A34, Th58;

            then |.((s2 . m) - (( lim s1) #Q p)).| < ( |.(( lim s1) #Q p).| * (c / |.(( lim s1) #Q p).|)) by A22, A28, A35, XREAL_1: 68;

            hence |.((s2 . m) - (( lim s1) #Q p)).| < c by A36, XCMPLX_1: 87;

          end;

            suppose

             A37: (s1 . m) <= ( lim s1);

            

             A38: m in NAT by ORDINAL1:def 12;

            

             A39: (( lim s1) / (s1 . m)) = ((s . m) / (s1 . m)) by FUNCOP_1: 7, A38

            .= ((s . m) * ((s1 . m) " ))

            .= ((s . m) * ((s1 " ) . m)) by VALUED_1: 10

            .= ((s /" s1) . m) by SEQ_1: 8;

            

             A40: (s1 . m) <> 0 by A5;

            

             A41: (s1 . m) > 0 by A5;

            then ((s1 . m) * ((s1 . m) " )) <= (( lim s1) * ((s1 . m) " )) by A37, XREAL_1: 64;

            then

             A42: ((s /" s1) . m) >= 1 by A40, A39, XCMPLX_0:def 7;

            then (((s /" s1) . m) #Q p) <= (((s /" s1) . m) #Q q) by A6, Th63;

            then (((s /" s1) . m) #Q p) <= (((s /" s1) . m) |^ m0) by A42, Th49;

            then

             A43: ((((s /" s1) . m) #Q p) - 1) <= ((((s /" s1) . m) |^ m0) - 1) by XREAL_1: 9;

            ((s1 . m) #Q p) > 0 by A5, Th52;

            then

             A44: |.((s1 . m) #Q p).| > 0 by ABSVALUE:def 1;

            

             A45: |.((s3 . m) - 1).| < (c / d) by A20, A26;

            (((s /" s1) . m) #Q p) >= 1 by A4, A42, Th60;

            then ((((s /" s1) . m) #Q p) - 1) >= (1 - 1) by XREAL_1: 9;

            then

             A46: ((((s /" s1) . m) #Q p) - 1) = |.((((s /" s1) . m) #Q p) - 1).| by ABSVALUE:def 1;

            (((s /" s1) . m) |^ m0) >= 1 by A42, Th11;

            then ((((s /" s1) . m) |^ m0) - 1) >= (1 - 1) by XREAL_1: 9;

            then |.((((s /" s1) . m) #Q p) - 1).| <= |.((((s /" s1) . m) |^ m0) - 1).| by A43, A46, ABSVALUE:def 1;

            then |.((((s /" s1) . m) #Q p) - 1).| <= |.((s3 . m) - 1).| by A9;

            then

             A47: |.((((s /" s1) . m) #Q p) - 1).| < (c / d) by A45, XXREAL_0: 2;

             |.(s2 . m).| < d by A17;

            then |.((s1 . m) #Q p).| < d by A5;

            then ( |.((s1 . m) #Q p).| / d) < (d / d) by A16, XREAL_1: 74;

            then ( |.((s1 . m) #Q p).| / d) < 1 by A16, XCMPLX_1: 60;

            then

             A48: (c * ( |.((s1 . m) #Q p).| / d)) < (c * 1) by A19, XREAL_1: 68;

            

             A49: ((s1 . m) #Q p) <> 0 by A5, Th52;

             |.((s2 . m) - (( lim s1) #Q p)).| = |.((((s1 . m) #Q p) - (( lim s1) #Q p)) * 1).| by A5

            .= |.((((s1 . m) #Q p) - (( lim s1) #Q p)) * (((s1 . m) #Q p) / ((s1 . m) #Q p))).| by A49, XCMPLX_1: 60

            .= |.((((s1 . m) #Q p) * (((s1 . m) #Q p) - (( lim s1) #Q p))) / ((s1 . m) #Q p)).|

            .= |.(((s1 . m) #Q p) * ((((s1 . m) #Q p) - (( lim s1) #Q p)) / ((s1 . m) #Q p))).|

            .= ( |.((s1 . m) #Q p).| * |.((((s1 . m) #Q p) - (( lim s1) #Q p)) / ((s1 . m) #Q p)).|) by COMPLEX1: 65

            .= ( |.((s1 . m) #Q p).| * |.((((s1 . m) #Q p) / ((s1 . m) #Q p)) - ((( lim s1) #Q p) / ((s1 . m) #Q p))).|)

            .= ( |.((s1 . m) #Q p).| * |.(1 - ((( lim s1) #Q p) / ((s1 . m) #Q p))).|) by A49, XCMPLX_1: 60

            .= ( |.((s1 . m) #Q p).| * |.( - (1 - ((( lim s1) #Q p) / ((s1 . m) #Q p)))).|) by COMPLEX1: 52

            .= ( |.((s1 . m) #Q p).| * |.(((( lim s1) #Q p) / ((s1 . m) #Q p)) - 1).|)

            .= ( |.((s1 . m) #Q p).| * |.(((( lim s1) / (s1 . m)) #Q p) - 1).|) by A3, A41, Th58;

            then |.((s2 . m) - (( lim s1) #Q p)).| < ( |.((s1 . m) #Q p).| * (c / d)) by A44, A39, A47, XREAL_1: 68;

            hence |.((s2 . m) - (( lim s1) #Q p)).| < c by A48, XXREAL_0: 2;

          end;

        end;

        hence |.((s2 . m) - (( lim s1) #Q p)).| < c;

      end;

      hence thesis by A2, SEQ_2:def 7;

    end;

    theorem :: PREPOWER:89

    

     Th89: s1 is convergent & s2 is convergent & ( lim s1) > 0 & (for n holds (s1 . n) > 0 & (s2 . n) = ((s1 . n) #Q p)) implies ( lim s2) = (( lim s1) #Q p)

    proof

      assume that

       A1: s1 is convergent and

       A2: s2 is convergent and

       A3: ( lim s1) > 0 and

       A4: for n holds (s1 . n) > 0 & (s2 . n) = ((s1 . n) #Q p);

      per cases ;

        suppose p >= 0 ;

        hence thesis by A1, A2, A3, A4, Lm10;

      end;

        suppose

         A5: p <= 0 ;

        s1 is bounded by A1;

        then

        consider d be Real such that

         A6: d > 0 and

         A7: for n holds |.(s1 . n).| < d by SEQ_2: 3;

        reconsider d as Real;

        

         A8: (d #Q p) > 0 by A6, Th52;

         A9:

        now

          assume ( lim s2) = 0 ;

          then

          consider n such that

           A10: for m st m >= n holds |.((s2 . m) - 0 ).| < (d #Q p) by A2, A8, SEQ_2:def 7;

          now

            let m;

            

             A11: (s1 . m) > 0 by A4;

            

             A12: (s1 . m) <> 0 by A4;

            

             A13: ((s1 . m) #Q p) > 0 by A4, Th52;

             |.(s1 . m).| < d by A7;

            then (s1 . m) < d by A11, ABSVALUE:def 1;

            then ((s1 . m) / (s1 . m)) < (d / (s1 . m)) by A11, XREAL_1: 74;

            then 1 <= (d / (s1 . m)) by A12, XCMPLX_1: 60;

            then ((d / (s1 . m)) #Q p) <= 1 by A5, Th61;

            then ((d #Q p) / ((s1 . m) #Q p)) <= 1 by A6, A11, Th58;

            then

             A14: (((d #Q p) / ((s1 . m) #Q p)) * ((s1 . m) #Q p)) <= (1 * ((s1 . m) #Q p)) by A13, XREAL_1: 64;

            

             A15: ((s1 . m) #Q p) <> 0 by A4, Th52;

            assume m >= n;

            then |.((s2 . m) - 0 ).| < (d #Q p) by A10;

            then |.((s1 . m) #Q p).| < (d #Q p) by A4;

            then ((s1 . m) #Q p) < (d #Q p) by A13, ABSVALUE:def 1;

            hence contradiction by A15, A14, XCMPLX_1: 87;

          end;

          hence contradiction;

        end;

        now

          let n;

          ((s1 . n) #Q p) <> 0 by A4, Th52;

          hence (s2 . n) <> 0 by A4;

        end;

        then

         A16: s2 is non-zero by SEQ_1: 5;

        then

         A17: ( lim (s2 " )) = (( lim s2) " ) by A2, A9, SEQ_2: 22;

        deffunc O( Nat) = ((s2 . $1) " );

        consider s be Real_Sequence such that

         A18: for n holds (s . n) = O(n) from SEQ_1:sch 1;

         A19:

        now

          let n;

          (s . n) = ((s2 . n) " ) by A18

          .= (((s1 . n) #Q p) " ) by A4

          .= (1 / ((s1 . n) #Q p))

          .= ((s1 . n) #Q ( - p)) by A4, Th54;

          hence (s1 . n) > 0 & (s . n) = ((s1 . n) #Q ( - p)) by A4;

        end;

        

         A20: ( dom s2) = NAT by FUNCT_2:def 1;

        

         A21: ( dom s) = NAT by FUNCT_2:def 1;

        for n be object st n in ( dom s) holds (s . n) = ((s2 . n) " ) by A18;

        then

         A22: s = (s2 " ) by A21, A20, VALUED_1:def 7;

        (s2 " ) is convergent by A2, A16, A9, SEQ_2: 21;

        then (( lim s2) " ) = (( lim s1) #Q ( - p)) by A1, A3, A5, A17, A22, A19, Lm10;

        then (1 / ( lim s2)) = (1 / (( lim s1) #Q p)) by A3, Th54;

        hence thesis by XCMPLX_1: 59;

      end;

    end;

    

     Lm11: a > 0 implies ((a #R b) #Q p) = (a #R (b * p))

    proof

      consider s1 be Rational_Sequence such that

       A1: s1 is convergent and

       A2: b = ( lim s1) and for n holds (s1 . n) >= b by Th68;

      reconsider s2 = (p (#) s1) as Rational_Sequence;

      assume

       A3: a > 0 ;

       A4:

      now

        let n;

        

         A5: (a #Q (s1 . n)) > 0 by A3, Th52;

        (((a #Q s1) . n) #Q p) = ((a #Q (s1 . n)) #Q p) by Def5

        .= (a #Q (p * (s1 . n))) by A3, Th59

        .= (a #Q (s2 . n)) by SEQ_1: 9

        .= ((a #Q s2) . n) by Def5;

        hence ((a #Q s1) . n) > 0 & (((a #Q s1) . n) #Q p) = ((a #Q s2) . n) by A5, Def5;

      end;

      

       A6: s2 is convergent by A1;

      then

       A7: (a #Q s2) is convergent by A3, Th69;

      ( lim s2) = (b * p) by A1, A2, SEQ_2: 8;

      then

       A8: (a #R (b * p)) = ( lim (a #Q s2)) by A3, A6, A7, Def6;

      

       A9: (a #Q s1) is convergent by A3, A1, Th69;

      then (a #R b) = ( lim (a #Q s1)) by A3, A1, A2, Def6;

      hence thesis by A3, A9, A7, A8, A4, Th81, Th89;

    end;

    

     Lm12: a >= 1 & s1 is convergent & s2 is convergent & (for n holds (s2 . n) = (a #R (s1 . n))) implies ( lim s2) = (a #R ( lim s1))

    proof

      assume that

       A1: a >= 1 and

       A2: s1 is convergent and

       A3: s2 is convergent and

       A4: for n holds (s2 . n) = (a #R (s1 . n));

      set d = ( |.( lim s1).| + 1);

      

       A5: |.( lim s1).| < ( |.( lim s1).| + 1) by XREAL_1: 29;

      now

        ( lim s1) <= |.( lim s1).| by ABSVALUE: 4;

        then ( lim s1) <= d by A5, XXREAL_0: 2;

        then

         A6: (a #R ( lim s1)) <= (a #R d) by A1, Th82;

        (a #R ( lim s1)) > 0 by A1, Th81;

        then

         A7: |.(a #R ( lim s1)).| <= (a #R d) by A6, ABSVALUE:def 1;

        

         A8: (a #R d) >= 0 by A1, Th81;

        let c be Real;

        assume

         A9: c > 0 ;

        consider m1 such that

         A10: (((a #R d) * (a - 1)) / c) < m1 by SEQ_4: 3;

        (m1 + 1) >= m1 by XREAL_1: 29;

        then (((a #R d) * (a - 1)) / c) < (m1 + 1) by A10, XXREAL_0: 2;

        then ((((a #R d) * (a - 1)) / c) * c) < (c * (m1 + 1)) by A9, XREAL_1: 68;

        then ((a #R d) * (a - 1)) < (c * (m1 + 1)) by A9, XCMPLX_1: 87;

        then (((a #R d) * (a - 1)) / (m1 + 1)) < (((m1 + 1) * c) / (m1 + 1)) by XREAL_1: 74;

        then (((a #R d) * (a - 1)) / (m1 + 1)) < ((c / (m1 + 1)) * (m1 + 1));

        then

         A11: (((a #R d) * (a - 1)) / (m1 + 1)) < c by XCMPLX_1: 87;

        reconsider m3 = ((m1 + 1) " ) as Rational;

        

         A12: |.(a #R ( lim s1)).| >= 0 by COMPLEX1: 46;

        consider n such that

         A13: for m st n <= m holds |.((s1 . m) - ( lim s1)).| < ((m1 + 1) " ) by A2, SEQ_2:def 7;

        take n;

        let m;

        assume m >= n;

        then

         A14: |.((s1 . m) - ( lim s1)).| <= ((m1 + 1) " ) by A13;

        

         A15: (m1 + 1) >= ( 0 + 1) by NAT_1: 13;

        then (((m1 + 1) -Root a) - 1) <= ((a - 1) / (m1 + 1)) by A1, Th31;

        then

         A16: ((a #R d) * (((m1 + 1) -Root a) - 1)) <= ((a #R d) * ((a - 1) / (m1 + 1))) by A8, XREAL_1: 64;

        ((s1 . m) - ( lim s1)) <= |.((s1 . m) - ( lim s1)).| by ABSVALUE: 4;

        then ((s1 . m) - ( lim s1)) <= ((m1 + 1) " ) by A14, XXREAL_0: 2;

        then (a #R ((s1 . m) - ( lim s1))) <= (a #R m3) by A1, Th82;

        then (a #R ((s1 . m) - ( lim s1))) <= (a #Q m3) by A1, Th74;

        then (a #R ((s1 . m) - ( lim s1))) <= ((m1 + 1) -Root a) by A15, Th50;

        then

         A17: ((a #R ((s1 . m) - ( lim s1))) - 1) <= (((m1 + 1) -Root a) - 1) by XREAL_1: 9;

        

         A18: (a #R ((s1 . m) - ( lim s1))) <> 0 by A1, Th81;

        

         A19: (a #R ((s1 . m) - ( lim s1))) > 0 by A1, Th81;

         A20:

        now

          per cases ;

            suppose ((s1 . m) - ( lim s1)) >= 0 ;

            then (a #R ((s1 . m) - ( lim s1))) >= 1 by A1, Th85;

            then ((a #R ((s1 . m) - ( lim s1))) - 1) >= 0 by XREAL_1: 48;

            hence |.((a #R ((s1 . m) - ( lim s1))) - 1).| <= (((m1 + 1) -Root a) - 1) by A17, ABSVALUE:def 1;

          end;

            suppose

             A21: ((s1 . m) - ( lim s1)) < 0 ;

            

             A22: ( - ((s1 . m) - ( lim s1))) <= |.( - ((s1 . m) - ( lim s1))).| by ABSVALUE: 4;

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

            then ( - ((s1 . m) - ( lim s1))) <= m3 by A14, A22, XXREAL_0: 2;

            then (a #R ( - ((s1 . m) - ( lim s1)))) <= (a #R m3) by A1, Th82;

            then (a #R ( - ((s1 . m) - ( lim s1)))) <= (a #Q m3) by A1, Th74;

            then (a #R ( - ((s1 . m) - ( lim s1)))) <= ((m1 + 1) -Root a) by A15, Th50;

            then

             A23: ((a #R ( - ((s1 . m) - ( lim s1)))) - 1) <= (((m1 + 1) -Root a) - 1) by XREAL_1: 9;

            (a #R ( - ((s1 . m) - ( lim s1)))) >= 1 by A1, A21, Th85;

            then ((a #R ( - ((s1 . m) - ( lim s1)))) - 1) >= 0 by XREAL_1: 48;

            then

             A24: |.((a #R ( - ((s1 . m) - ( lim s1)))) - 1).| <= (((m1 + 1) -Root a) - 1) by A23, ABSVALUE:def 1;

            (a #R ((s1 . m) - ( lim s1))) <= 1 by A1, A21, Th87;

            then

             A25: |.(a #R ((s1 . m) - ( lim s1))).| <= 1 by A19, ABSVALUE:def 1;

             |.((a #R ( - ((s1 . m) - ( lim s1)))) - 1).| >= 0 by COMPLEX1: 46;

            then

             A26: ( |.(a #R ((s1 . m) - ( lim s1))).| * |.((a #R ( - ((s1 . m) - ( lim s1)))) - 1).|) <= (1 * |.((a #R ( - ((s1 . m) - ( lim s1)))) - 1).|) by A25, XREAL_1: 64;

             |.((a #R ((s1 . m) - ( lim s1))) - 1).| = |.(((a #R ((s1 . m) - ( lim s1))) - 1) * 1).|

            .= |.(((a #R ((s1 . m) - ( lim s1))) - 1) * ((a #R ((s1 . m) - ( lim s1))) / (a #R ((s1 . m) - ( lim s1))))).| by A18, XCMPLX_1: 60

            .= |.(((a #R ((s1 . m) - ( lim s1))) * ((a #R ((s1 . m) - ( lim s1))) - 1)) / (a #R ((s1 . m) - ( lim s1)))).|

            .= |.((a #R ((s1 . m) - ( lim s1))) * (((a #R ((s1 . m) - ( lim s1))) - 1) / (a #R ((s1 . m) - ( lim s1))))).|

            .= ( |.(a #R ((s1 . m) - ( lim s1))).| * |.(((a #R ((s1 . m) - ( lim s1))) - 1) / (a #R ((s1 . m) - ( lim s1)))).|) by COMPLEX1: 65

            .= ( |.(a #R ((s1 . m) - ( lim s1))).| * |.(((a #R ((s1 . m) - ( lim s1))) / (a #R ((s1 . m) - ( lim s1)))) - (1 / (a #R ((s1 . m) - ( lim s1))))).|)

            .= ( |.(a #R ((s1 . m) - ( lim s1))).| * |.(1 - (1 / (a #R ((s1 . m) - ( lim s1))))).|) by A18, XCMPLX_1: 60

            .= ( |.(a #R ((s1 . m) - ( lim s1))).| * |.(1 - (a #R ( - ((s1 . m) - ( lim s1))))).|) by A1, Th76

            .= ( |.(a #R ((s1 . m) - ( lim s1))).| * |.( - (1 - (a #R ( - ((s1 . m) - ( lim s1)))))).|) by COMPLEX1: 52

            .= ( |.(a #R ((s1 . m) - ( lim s1))).| * |.((a #R ( - ((s1 . m) - ( lim s1)))) - 1).|);

            hence |.((a #R ((s1 . m) - ( lim s1))) - 1).| <= (((m1 + 1) -Root a) - 1) by A24, A26, XXREAL_0: 2;

          end;

        end;

         |.((a #R ((s1 . m) - ( lim s1))) - 1).| >= 0 by COMPLEX1: 46;

        then

         A27: ( |.(a #R ( lim s1)).| * |.((a #R ((s1 . m) - ( lim s1))) - 1).|) <= ((a #R d) * (((m1 + 1) -Root a) - 1)) by A20, A12, A7, XREAL_1: 66;

         |.((a #R (s1 . m)) - (a #R ( lim s1))).| = |.(((a #R (s1 . m)) - (a #R ( lim s1))) * 1).|

        .= |.(((a #R (s1 . m)) - (a #R ( lim s1))) * ((a #R ( lim s1)) / (a #R ( lim s1)))).| by A1, Lm9, XCMPLX_1: 60

        .= |.(((a #R ( lim s1)) * ((a #R (s1 . m)) - (a #R ( lim s1)))) / (a #R ( lim s1))).|

        .= |.((a #R ( lim s1)) * (((a #R (s1 . m)) - (a #R ( lim s1))) / (a #R ( lim s1)))).|

        .= ( |.(a #R ( lim s1)).| * |.(((a #R (s1 . m)) - (a #R ( lim s1))) / (a #R ( lim s1))).|) by COMPLEX1: 65

        .= ( |.(a #R ( lim s1)).| * |.(((a #R (s1 . m)) / (a #R ( lim s1))) - ((a #R ( lim s1)) / (a #R ( lim s1)))).|)

        .= ( |.(a #R ( lim s1)).| * |.(((a #R (s1 . m)) / (a #R ( lim s1))) - 1).|) by A1, Lm9, XCMPLX_1: 60

        .= ( |.(a #R ( lim s1)).| * |.((a #R ((s1 . m) - ( lim s1))) - 1).|) by A1, Th77;

        then |.((a #R (s1 . m)) - (a #R ( lim s1))).| <= (((a #R d) * (a - 1)) / (m1 + 1)) by A27, A16, XXREAL_0: 2;

        then |.((a #R (s1 . m)) - (a #R ( lim s1))).| < c by A11, XXREAL_0: 2;

        hence |.((s2 . m) - (a #R ( lim s1))).| < c by A4;

      end;

      hence thesis by A3, SEQ_2:def 7;

    end;

    theorem :: PREPOWER:90

    

     Th90: a > 0 & s1 is convergent & s2 is convergent & (for n holds (s2 . n) = (a #R (s1 . n))) implies ( lim s2) = (a #R ( lim s1))

    proof

      assume that

       A1: a > 0 and

       A2: s1 is convergent and

       A3: s2 is convergent and

       A4: for n holds (s2 . n) = (a #R (s1 . n));

      per cases ;

        suppose a >= 1;

        hence thesis by A2, A3, A4, Lm12;

      end;

        suppose

         A5: a < 1;

         A6:

        now

          assume

           A7: ( lim s2) = 0 ;

          (a #R (( lim s1) + 1)) > 0 by A1, Th81;

          then

          consider n such that

           A8: for m st m >= n holds |.((s2 . m) - 0 ).| < (a #R (( lim s1) + 1)) by A3, A7, SEQ_2:def 7;

          consider n1 be Nat such that

           A9: for m st m >= n1 holds |.((s1 . m) - ( lim s1)).| < 1 by A2, SEQ_2:def 7;

          now

            let m such that

             A10: m >= (n + n1);

            (n + n1) >= n1 by NAT_1: 12;

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

            then

             A11: |.((s1 . m) - ( lim s1)).| < 1 by A9;

            ((s1 . m) - ( lim s1)) <= |.((s1 . m) - ( lim s1)).| by ABSVALUE: 4;

            then ((s1 . m) - ( lim s1)) < 1 by A11, XXREAL_0: 2;

            then

             A12: (((s1 . m) - ( lim s1)) + ( lim s1)) < (( lim s1) + 1) by XREAL_1: 6;

            (n + n1) >= n by NAT_1: 12;

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

            then |.((s2 . m) - 0 ).| < (a #R (( lim s1) + 1)) by A8;

            then

             A13: |.(a #R (s1 . m)).| < (a #R (( lim s1) + 1)) by A4;

            (a #R (s1 . m)) > 0 by A1, Th81;

            then (a #R (s1 . m)) < (a #R (( lim s1) + 1)) by A13, ABSVALUE:def 1;

            hence contradiction by A1, A5, A12, Th84;

          end;

          hence contradiction;

        end;

         A14:

        now

          let n;

          

          thus ((s2 " ) . n) = ((s2 . n) " ) by VALUED_1: 10

          .= ((a #R (s1 . n)) " ) by A4

          .= (1 / (a #R (s1 . n)))

          .= ((1 / a) #R (s1 . n)) by A1, Th79;

        end;

        (a * (1 / a)) <= (1 * (1 / a)) by A1, A5, XREAL_1: 64;

        then

         A15: 1 <= (1 / a) by A1, XCMPLX_1: 106;

        

         A16: (a #R ( lim s1)) <> 0 by A1, Th81;

        now

          let n;

          (s2 . n) = (a #R (s1 . n)) by A4;

          hence (s2 . n) <> 0 by A1, Th81;

        end;

        then

         A17: s2 is non-zero by SEQ_1: 5;

        then

         A18: ( lim (s2 " )) = (( lim s2) " ) by A3, A6, SEQ_2: 22;

        (s2 " ) is convergent by A3, A6, A17, SEQ_2: 21;

        

        then (( lim s2) " ) = ((1 / a) #R ( lim s1)) by A2, A15, A18, A14, Lm12

        .= (1 / (a #R ( lim s1))) by A1, Th79;

        then 1 = ((1 / (a #R ( lim s1))) * ( lim s2)) by A6, XCMPLX_0:def 7;

        

        then (a #R ( lim s1)) = ((a #R ( lim s1)) * ((1 / (a #R ( lim s1))) * ( lim s2)))

        .= (((a #R ( lim s1)) * (1 / (a #R ( lim s1)))) * ( lim s2))

        .= (1 * ( lim s2)) by A16, XCMPLX_1: 106;

        hence thesis;

      end;

    end;

    theorem :: PREPOWER:91

    a > 0 implies ((a #R b) #R c) = (a #R (b * c))

    proof

      consider s be Rational_Sequence such that

       A1: s is convergent and

       A2: c = ( lim s) and for n holds (s . n) <= c by Th67;

      

       A3: ( lim (b (#) s)) = (b * c) by A1, A2, SEQ_2: 8;

      

       A4: (b (#) s) is convergent by A1;

      assume

       A5: a > 0 ;

      then

       A6: ((a #R b) #Q s) is convergent by A1, Th69, Th81;

       A7:

      now

        let n;

        

        thus (((a #R b) #Q s) . n) = ((a #R b) #Q (s . n)) by Def5

        .= (a #R (b * (s . n))) by A5, Lm11

        .= (a #R ((b (#) s) . n)) by SEQ_1: 9;

      end;

      (a #R b) > 0 by A5, Th81;

      then ((a #R b) #R c) = ( lim ((a #R b) #Q s)) by A1, A2, A6, Def6;

      hence thesis by A5, A6, A4, A3, A7, Th90;

    end;

    begin

    reserve r,u for Real,

k for Nat;

    theorem :: PREPOWER:92

    r > 0 & u > 0 implies ex k be Nat st (u / (2 |^ k)) <= r

    proof

      defpred P[ Nat] means $1 <= (2 |^ $1);

      assume that

       A1: r > 0 and

       A2: u > 0 ;

      set t = (1 / r);

      reconsider t as Real;

      consider n such that

       A3: (u * t) < n by SEQ_4: 3;

      

       A4: 0 < (u * t) by A1, A2;

      then

       A5: (u / (u * t)) > (u / n) by A2, A3, XREAL_1: 76;

      

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

      proof

        let k be Nat;

        assume k <= (2 |^ k);

        then

         A7: ((2 |^ k) + 1) >= (k + 1) by XREAL_1: 7;

        (2 |^ k) >= 1 by Th11;

        then

         A8: ((2 |^ k) + (2 |^ k)) >= ((2 |^ k) + 1) by XREAL_1: 7;

        (2 |^ (k + 1)) = ((2 |^ k) * (2 |^ 1)) by NEWTON: 8

        .= ((2 |^ k) * 2)

        .= ((2 |^ k) + (2 |^ k));

        hence thesis by A8, A7, XXREAL_0: 2;

      end;

      take n;

      

       A9: r = (1 / t)

      .= ((u * 1) / (u * t)) by A2, XCMPLX_1: 91

      .= (u / (u * t));

      

       A10: P[ 0 ];

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

      then (u / n) >= (u / (2 |^ n)) by A2, A3, A4, XREAL_1: 118;

      hence thesis by A9, A5, XXREAL_0: 2;

    end;

    theorem :: PREPOWER:93

    k >= n & r >= 1 implies (r |^ k) >= (r |^ n)

    proof

      assume that

       A1: k >= n and

       A2: r >= 1;

      consider m be Nat such that

       A3: k = (n + m) by A1, NAT_1: 10;

      

       A4: (r |^ k) = ((r |^ n) * (r |^ m)) by A3, NEWTON: 8;

      (r |^ n) >= 1 by A2, Th11;

      hence thesis by A2, A4, Th11, XREAL_1: 151;

    end;

    theorem :: PREPOWER:94

    

     Th94: for n,m,l be Nat st n divides m & n divides l holds n divides (m - l)

    proof

      let n,m,l be Nat;

      assume that

       A1: n divides m and

       A2: n divides l;

      

       A3: ( - l) = ( - (n * (l div n))) by A2, NAT_D: 3

      .= (n * ( - (l div n)));

      m = (n * (m div n)) by A1, NAT_D: 3;

      then (m - l) = (n * ((m div n) + ( - (l div n)))) by A3;

      hence thesis by INT_1:def 3;

    end;

    theorem :: PREPOWER:95

    m divides n iff m divides n qua Integer;

    theorem :: PREPOWER:96

    

     Th96: (m gcd n) = (m gcd |.(n - m).|)

    proof

      set x = (m gcd n), y = (m gcd |.(n - m).|);

      

       A1: x divides m by NAT_D:def 5;

      

       A2: x divides n by NAT_D:def 5;

      

       A3: y divides m by NAT_D:def 5;

      per cases ;

        suppose (n - m) >= 0 ;

        then

        reconsider nm = (n - m) as Element of NAT by INT_1: 3;

        

         A4: |.(n - m).| = nm by ABSVALUE:def 1;

        then y divides nm by NAT_D:def 5;

        then y divides (nm + m) by A3, NAT_D: 8;

        then

         A5: y divides x by A3, NAT_D:def 5;

        x divides (n - m) by A1, A2, Th94;

        then x divides y by A1, A4, NAT_D:def 5;

        hence thesis by A5, NAT_D: 5;

      end;

        suppose

         A6: (n - m) < 0 ;

        reconsider nn = n as Integer;

        

         A7: |.(n - m).| = ( - (n - m)) by A6, ABSVALUE:def 1

        .= (m - n);

        then

        reconsider mn = (m - n) as Element of NAT ;

        y divides mn by A7, NAT_D:def 5;

        then y divides (mn - m) by A3, Th94;

        then y divides nn by INT_2: 10;

        then

         A8: y divides x by A3, NAT_D:def 5;

        x divides (m - n) by A1, A2, Th94;

        then x divides y by A1, A7, NAT_D:def 5;

        hence thesis by A8, NAT_D: 5;

      end;

    end;

    theorem :: PREPOWER:97

    for a,b be Integer st a >= 0 & b >= 0 holds (a gcd b) = (a gcd (b - a))

    proof

      let a,b be Integer;

      assume that

       A1: a >= 0 and

       A2: b >= 0 ;

      

      thus (a gcd b) = ( |.a.| gcd |.b.|) by INT_2: 34

      .= ( |.a.| gcd |.( |.b.| - |.a.|).|) by Th96

      .= ( |.a.| gcd |.(b - |.a.|).|) by A2, ABSVALUE:def 1

      .= ( |.a.| gcd |.(b - a).|) by A1, ABSVALUE:def 1

      .= (a gcd (b - a)) by INT_2: 34;

    end;

    theorem :: PREPOWER:98

    a >= 0 implies (a #Z l) >= 0 by Lm5;

    theorem :: PREPOWER:99

    a > 0 implies (a #Q l) = (a #Z l)

    proof

      assume a > 0 ;

      then (a #Z l) > 0 by Th39;

      then

       A1: (a #Z l) = ((1 -Root (a #Z l)) |^ 1) by Def2;

      ( denominator l) = 1 by RAT_1: 17;

      

      hence (a #Q l) = (1 -Root (a #Z l)) by RAT_1: 17

      .= (a #Z l) by A1;

    end;

    theorem :: PREPOWER:100

    l <> 0 implies ( 0 #Z l) = 0

    proof

      assume

       A1: l <> 0 ;

      per cases by A1;

        suppose

         A2: l > 0 ;

        then

        reconsider l as Element of NAT by INT_1: 3;

        l >= ( 0 + 1) by A2, NAT_1: 13;

        then

         A3: ( 0 |^ l) = 0 by NEWTON: 11;

         |.l.| = l by ABSVALUE:def 1;

        hence thesis by A3, Def3;

      end;

        suppose

         A4: l < 0 ;

        then

        reconsider k = ( - l) as Element of NAT by INT_1: 3;

        k > ( - 0 ) by A4;

        then k >= ( 0 + 1) by NAT_1: 13;

        then

         A5: ( 0 |^ k) = 0 by NEWTON: 11;

         |.l.| = k by A4, ABSVALUE:def 1;

        then (( 0 |^ |.l.|) " ) = 0 by A5;

        hence thesis by A4, Def3;

      end;

    end;