power.miz

begin

 reserve x for set;

 reserve a,b,c,d,e for Real;

 reserve m,n,m1,m2 for Nat;

 reserve k,l for Integer;

 reserve p for Rational;

 theorem :: POWER:1



 Th1: n is even implies (( - a) |^ n) = (a |^ n)

 proof

 given m such that

 A1: n = (2 * m);



 thus (( - a) |^ n) = ((( - a) |^ (1 + 1)) |^ m) by A1, NEWTON: 9

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

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

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

 .= (((((( - a) GeoSeq ) . 0 ) * ( - a)) * ((( - a) |^ 0 ) * ( - a))) |^ m) by PREPOWER:def 1

 .= (((((( - a) GeoSeq ) . 0 ) * ( - a)) * (((( - a) GeoSeq ) . 0 ) * ( - a))) |^ m) by PREPOWER:def 1

 .= (((((( - a) GeoSeq ) . 0 ) * ( - a)) * (1 * ( - a))) |^ m) by PREPOWER: 3

 .= (((1 * ( - a)) * (1 * ( - a))) |^ m) by PREPOWER: 3

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

 .= (((((a GeoSeq ) . 0 ) * a) * (1 * a)) |^ m) by PREPOWER: 3

 .= (((((a GeoSeq ) . 0 ) * a) * (((a GeoSeq ) . 0 ) * a)) |^ m) by PREPOWER: 3

 .= (((((a GeoSeq ) . 0 ) * a) * ((a |^ 0 ) * a)) |^ m) by PREPOWER:def 1

 .= ((((a |^ 0 ) * a) * ((a |^ 0 ) * a)) |^ m) by PREPOWER:def 1

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

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

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

 .= (a |^ n) by A1, NEWTON: 9;

 end;

 theorem :: POWER:2



 Th2: n is odd implies (( - a) |^ n) = ( - (a |^ n))

 proof

 assume n is odd;

 then

 consider m such that

 A1: n = ((2 * m) + 1) by ABIAN: 9;



 thus (( - a) |^ n) = ((( - a) |^ (2 * m)) * ( - a)) by A1, NEWTON: 6

 .= ((a |^ (2 * m)) * ( - a)) by Th1

 .= ( - ((a |^ (2 * m)) * a))

 .= ( - (a |^ n)) by A1, NEWTON: 6;

 end;

 theorem :: POWER:3



 Th3: a >= 0 or n is even implies (a |^ n) >= 0

 proof

 assume

 A1: a >= 0 or n is even;

 A2:

 now

 let a, n such that

 A3: a >= 0 ;

 now

 per cases by A3;

 suppose a > 0 ;

 hence (a |^ n) >= 0 by PREPOWER: 6;

 end;

 suppose

 A4: a = 0 ;

 now

 per cases by NAT_1: 6;

 suppose

 A5: n = 0 ;

 (a |^ n) = ((a GeoSeq ) . n) by PREPOWER:def 1

 .= 1 by A5, PREPOWER: 3;

 hence (a |^ n) >= 0 ;

 end;

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

 then

 consider m be Nat such that

 A6: n = (m + 1);

 (a |^ n) = ((a |^ m) * a) by A6, NEWTON: 6

 .= 0 by A4;

 hence (a |^ n) >= 0 ;

 end;

 end;

 hence (a |^ n) >= 0 ;

 end;

 end;

 hence (a |^ n) >= 0 ;

 end;

 now

 assume

 A7: n is even;

 now

 per cases ;

 suppose a >= 0 ;

 hence thesis by A2;

 end;

 suppose a < 0 ;

 then (( - a) |^ n) >= 0 by A2;

 hence thesis by A7, Th1;

 end;

 end;

 hence thesis;

 end;

 hence thesis by A1, A2;

 end;

 definition

 let n be natural Number;

 let a be Real;

 :: POWER:def1

 func n -root a -> Real equals

 : Def1: (n -Root a) if a >= 0 & n >= 1,

( - (n -Root ( - a))) if a < 0 & n is odd;

 consistency ;

 coherence ;

 end

 theorem :: POWER:4

 for n be Nat st n >= 1 & a >= 0 or n is odd holds ((n -root a) |^ n) = a & (n -root (a |^ n)) = a

 proof

 let n be Nat;

 assume

 A1: n >= 1 & a >= 0 or n is odd;

 A2:

 now

 assume that

 A3: n >= 1 and

 A4: a >= 0 ;



 A5: (n -root a) = (n -Root a) by A3, A4, Def1;

 now

 per cases by A4;

 suppose a > 0 ;

 hence (a |^ n) >= 0 by PREPOWER: 6;

 end;

 suppose a = 0 ;

 hence (a |^ n) >= 0 ;

 end;

 end;

 then (n -root (a |^ n)) = (n -Root (a |^ n)) by A3, Def1;

 hence thesis by A3, A4, A5, PREPOWER: 19;

 end;

 now

 assume

 A6: n is odd;

 then

 A7: ex m st n = ((2 * m) + 1) by ABIAN: 9;



 A8: n >= 1 by A6, ABIAN: 12;

 now

 per cases ;

 suppose a >= 0 ;

 hence thesis by A2, A8;

 end;

 suppose

 A9: a < 0 ;

 then

 A10: ( - a) > 0 by XREAL_1: 58;



 thus ((n -root a) |^ n) = (( - (n -Root ( - a))) |^ n) by A7, A9, Def1

 .= ( - ((n -Root ( - a)) |^ n)) by A7, Th2

 .= ( - ( - a)) by A8, A9, PREPOWER: 19

 .= a;

 (( - a) |^ n) > 0 by A10, PREPOWER: 6;

 then ( - (a |^ n)) > 0 by A7, Th2;

 then (a |^ n) < 0 ;



 hence (n -root (a |^ n)) = ( - (n -Root ( - (a |^ n)))) by A7, Def1

 .= ( - (n -Root (( - a) |^ n))) by A7, Th2

 .= ( - ( - a)) by A8, A9, PREPOWER: 19

 .= a;

 end;

 end;

 hence thesis;

 end;

 hence thesis by A1, A2;

 end;

 theorem :: POWER:5



 Th5: for n be Nat st n >= 1 holds (n -root 0 ) = 0

 proof

 let n be Nat;

 assume

 A1: n >= 1;



 hence (n -root 0 ) = (n -Root 0 ) by Def1

 .= 0 by A1, PREPOWER:def 2;

 end;

 theorem :: POWER:6

 n >= 1 implies (n -root 1) = 1

 proof

 assume

 A1: n >= 1;



 hence (n -root 1) = (n -Root 1) by Def1

 .= 1 by A1, PREPOWER: 20;

 end;

 theorem :: POWER:7



 Th7: a >= 0 & n >= 1 implies (n -root a) >= 0

 proof

 assume that

 A1: a >= 0 and

 A2: n >= 1;

 now

 per cases by A1;

 suppose

 A3: a > 0 ;

 (n -root a) = (n -Root a) by A1, A2, Def1;

 hence thesis by A2, A3, PREPOWER:def 2;

 end;

 suppose

 A4: a = 0 ;

 (n -root a) = (n -Root a) by A1, A2, Def1

 .= 0 by A2, A4, PREPOWER:def 2;

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 theorem :: POWER:8

 n is odd implies (n -root ( - 1)) = ( - 1)

 proof

 assume

 A1: n is odd;

 then

 A2: n >= 1 by ABIAN: 12;



 thus (n -root ( - 1)) = ( - (n -Root ( - ( - 1)))) by A1, Def1

 .= ( - 1) by A2, PREPOWER: 20;

 end;

 theorem :: POWER:9

 (1 -root a) = a

 proof

 now

 per cases ;

 suppose

 A1: a >= 0 ;



 hence (1 -root a) = (1 -Root a) by Def1

 .= a by A1, PREPOWER: 21;

 end;

 suppose

 A2: a < 0 ;

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



 hence (1 -root a) = ( - (1 -Root ( - a))) by A2, Def1

 .= ( - ( - a)) by A2, PREPOWER: 21

 .= a;

 end;

 end;

 hence thesis;

 end;

 theorem :: POWER:10



 Th10: n is odd implies (n -root a) = ( - (n -root ( - a)))

 proof

 assume

 A1: n is odd;

 then

 A2: ex m st n = ((2 * m) + 1) by ABIAN: 9;



 A3: n >= 1 by A1, ABIAN: 12;

 now

 per cases ;

 suppose

 A4: a < 0 ;



 hence (n -root a) = ( - (n -Root ( - a))) by A2, Def1

 .= ( - (n -root ( - a))) by A3, A4, Def1;

 end;

 suppose

 A5: a = 0 ;



 hence (n -root a) = 0 by A3, Th5

 .= ( - (n -root ( - a))) by A3, A5, Th5;

 end;

 suppose

 A6: a > 0 ;

 then ( - a) < ( - 0 ) by XREAL_1: 24;



 hence ( - (n -root ( - a))) = ( - ( - (n -Root ( - ( - a))))) by A2, Def1

 .= (n -root a) by A3, A6, Def1;

 end;

 end;

 hence thesis;

 end;

 theorem :: POWER:11



 Th11: n >= 1 & a >= 0 & b >= 0 or n is odd implies (n -root (a * b)) = ((n -root a) * (n -root b))

 proof

 assume

 A1: n >= 1 & a >= 0 & b >= 0 or n is odd;

 A2:

 now

 let a, b, n;

 assume that

 A3: n >= 1 and

 A4: a >= 0 and

 A5: b >= 0 ;



 thus (n -root (a * b)) = (n -Root (a * b)) by A3, A4, A5, Def1

 .= ((n -Root a) * (n -Root b)) by A3, A4, A5, PREPOWER: 22

 .= ((n -root a) * (n -Root b)) by A3, A4, Def1

 .= ((n -root a) * (n -root b)) by A3, A5, Def1;

 end;

 now

 assume

 A6: n is odd;

 then

 A7: n >= 1 by ABIAN: 12;

 now

 per cases ;

 suppose a >= 0 & b >= 0 ;

 hence thesis by A2, A7;

 end;

 suppose

 A8: a < 0 & b < 0 ;



 hence (n -root (a * b)) = (n -Root (( - a) * ( - b))) by A7, Def1

 .= (( - ( - (n -Root ( - a)))) * (n -Root ( - b))) by A7, A8, PREPOWER: 22

 .= (( - (n -root a)) * ( - ( - (n -Root ( - b))))) by A6, A8, Def1

 .= (( - (n -root a)) * ( - (n -root b))) by A6, A8, Def1

 .= ((n -root a) * (n -root b));

 end;

 suppose

 A9: a >= 0 & b < 0 ;



 thus (n -root (a * b)) = ( - (n -root ( - (a * b)))) by A6, Th10

 .= ( - (n -root (a * ( - b))))

 .= ( - ((n -root a) * (n -root ( - b)))) by A2, A7, A9

 .= ((n -root a) * ( - (n -root ( - b))))

 .= ((n -root a) * (n -root b)) by A6, Th10;

 end;

 suppose

 A10: a < 0 & b >= 0 ;



 thus (n -root (a * b)) = ( - (n -root ( - (a * b)))) by A6, Th10

 .= ( - (n -root (( - a) * b)))

 .= ( - ((n -root ( - a)) * (n -root b))) by A2, A7, A10

 .= (( - (n -root ( - a))) * (n -root b))

 .= ((n -root a) * (n -root b)) by A6, Th10;

 end;

 end;

 hence thesis;

 end;

 hence thesis by A1, A2;

 end;

 theorem :: POWER:12



 Th12: a > 0 & n >= 1 or a <> 0 & n is odd implies (n -root (1 / a)) = (1 / (n -root a))

 proof

 assume

 A1: a > 0 & n >= 1 or a <> 0 & n is odd;

 A2:

 now

 let a, n;

 assume

 A3: a > 0 & n >= 1;



 hence (n -root (1 / a)) = (n -Root (1 / a)) by Def1

 .= (1 / (n -Root a)) by A3, PREPOWER: 23

 .= (1 / (n -root a)) by A3, Def1;

 end;

 now

 assume that

 A4: a <> 0 and

 A5: n is odd;



 A6: n >= 1 by A5, ABIAN: 12;

 now

 per cases by A4;

 suppose a > 0 ;

 hence thesis by A2, A6;

 end;

 suppose a < 0 ;

 then

 A7: ( - a) > 0 by XREAL_1: 58;



 thus (1 / (n -root a)) = (1 / ( - (n -root ( - a)))) by A5, Th10

 .= ( - (1 / (n -root ( - a)))) by XCMPLX_1: 188

 .= ( - (n -root (1 / ( - a)))) by A2, A6, A7

 .= ( - (n -root ( - (1 / a)))) by XCMPLX_1: 188

 .= (n -root (1 / a)) by A5, Th10;

 end;

 end;

 hence thesis;

 end;

 hence thesis by A1, A2;

 end;

 theorem :: POWER:13

 a >= 0 & b > 0 & n >= 1 or b <> 0 & n is odd implies (n -root (a / b)) = ((n -root a) / (n -root b))

 proof

 assume

 A1: a >= 0 & b > 0 & n >= 1 or b <> 0 & n is odd;

 now

 per cases by A1;

 suppose

 A2: a >= 0 & b > 0 & n >= 1;



 hence (n -root (a / b)) = (n -Root (a / b)) by Def1

 .= ((n -Root a) / (n -Root b)) by A2, PREPOWER: 24

 .= ((n -root a) / (n -Root b)) by A2, Def1

 .= ((n -root a) / (n -root b)) by A2, Def1;

 end;

 suppose

 A3: b <> 0 & n is odd;



 thus (n -root (a / b)) = (n -root (a * (1 / b)))

 .= ((n -root a) * (n -root (1 / b))) by A3, Th11

 .= ((n -root a) * (1 / (n -root b))) by A3, Th12

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

 end;

 end;

 hence thesis;

 end;

 theorem :: POWER:14

 a >= 0 & n >= 1 & m >= 1 or n is odd & m is odd implies (n -root (m -root a)) = ((n * m) -root a)

 proof

 assume

 A1: a >= 0 & n >= 1 & m >= 1 or n is odd & m is odd;

 A2:

 now

 let a, n, m;

 assume that

 A3: a >= 0 and

 A4: n >= 1 and

 A5: m >= 1;



 A6: (n * m) >= 1 by A4, A5, XREAL_1: 159;

 (m -root a) >= 0 by A3, A5, Th7;

 then

 A7: (m -Root a) >= 0 by A3, A5, Def1;



 thus (n -root (m -root a)) = (n -root (m -Root a)) by A3, A5, Def1

 .= (n -Root (m -Root a)) by A4, A7, Def1

 .= ((n * m) -Root a) by A3, A4, A5, PREPOWER: 25

 .= ((n * m) -root a) by A3, A6, Def1;

 end;

 now

 assume n is odd;

 then

 consider m1 such that

 A8: n = ((2 * m1) + 1) by ABIAN: 9;

 assume m is odd;

 then

 consider m2 such that

 A9: m = ((2 * m2) + 1) by ABIAN: 9;



 A10: n >= ( 0 + 1) by A8, XREAL_1: 6;



 A11: m >= ( 0 + 1) by A9, XREAL_1: 6;

 then

 A12: (n * m) >= 1 by A10, XREAL_1: 159;



 A13: (n * m) = ((2 * (((m1 * (2 * m2)) + m1) + m2)) + 1) by A8, A9;

 now

 per cases ;

 suppose a >= 0 ;

 hence thesis by A2, A10, A11;

 end;

 suppose

 A14: a < 0 ;

 then (m -root ( - a)) >= 0 by A11, Th7;

 then

 A15: (m -Root ( - a)) >= 0 by A11, A14, Def1;



 thus (n -root (m -root a)) = (n -root ( - (m -Root ( - a)))) by A9, A14, Def1

 .= ( - (n -root ( - ( - (m -Root ( - a)))))) by A8, Th10

 .= ( - (n -Root (m -Root ( - a)))) by A10, A15, Def1

 .= ( - ((n * m) -Root ( - a))) by A10, A11, A14, PREPOWER: 25

 .= ( - ((n * m) -root ( - a))) by A12, A14, Def1

 .= ((n * m) -root a) by A13, Th10;

 end;

 end;

 hence thesis;

 end;

 hence thesis by A1, A2;

 end;

 theorem :: POWER:15

 a >= 0 & n >= 1 & m >= 1 or n is odd & m is odd implies ((n -root a) * (m -root a)) = ((n * m) -root (a |^ (n + m)))

 proof

 assume

 A1: a >= 0 & n >= 1 & m >= 1 or n is odd & m is odd;

 A2:

 now

 let a, n, m;

 assume that

 A3: a >= 0 and

 A4: n >= 1 and

 A5: m >= 1;



 A6: (n * m) >= 1 & (a |^ (n + m)) >= 0 by A3, A4, A5, Th3, XREAL_1: 159;



 thus ((n -root a) * (m -root a)) = ((n -root a) * (m -Root a)) by A3, A5, Def1

 .= ((n -Root a) * (m -Root a)) by A3, A4, Def1

 .= ((n * m) -Root (a |^ (n + m))) by A3, A4, A5, PREPOWER: 26

 .= ((n * m) -root (a |^ (n + m))) by A6, Def1;

 end;

 now

 assume n is odd;

 then

 consider m1 such that

 A7: n = ((2 * m1) + 1) by ABIAN: 9;

 assume m is odd;

 then

 consider m2 such that

 A8: m = ((2 * m2) + 1) by ABIAN: 9;



 A9: n >= ( 0 + 1) & m >= ( 0 + 1) by A7, A8, XREAL_1: 6;

 then

 A10: (n * m) >= 1 by XREAL_1: 159;



 A11: (n + m) = (2 * (m1 + (1 + m2))) by A7, A8;

 now

 per cases ;

 suppose a >= 0 ;

 hence thesis by A2, A9;

 end;

 suppose

 A12: a < 0 ;



 A13: (a |^ (n + m)) >= 0 by A11, Th3;



 thus ((n -root a) * (m -root a)) = ((n -root a) * ( - (m -Root ( - a)))) by A8, A12, Def1

 .= (( - (n -Root ( - a))) * ( - (m -Root ( - a)))) by A7, A12, Def1

 .= ((n -Root ( - a)) * (m -Root ( - a)))

 .= ((n * m) -Root (( - a) |^ (n + m))) by A9, A12, PREPOWER: 26

 .= ((n * m) -Root (a |^ (n + m))) by A11, Th1

 .= ((n * m) -root (a |^ (n + m))) by A10, A13, Def1;

 end;

 end;

 hence thesis;

 end;

 hence thesis by A1, A2;

 end;

 theorem :: POWER:16

 a <= b & ( 0 <= a & n >= 1 or n is odd) implies (n -root a) <= (n -root b)

 proof

 assume that

 A1: a <= b and

 A2: 0 <= a & n >= 1 or n is odd;

 A3:

 now

 let a, b, n;

 assume that

 A4: 0 <= a & n >= 1 and

 A5: a <= b;

 (n -Root a) <= (n -Root b) by A4, A5, PREPOWER: 27;

 then (n -Root a) <= (n -root b) by A4, A5, Def1;

 hence (n -root a) <= (n -root b) by A4, Def1;

 end;

 now

 assume

 A6: n is odd;

 then

 A7: n >= 1 by ABIAN: 12;

 now

 per cases ;

 suppose a >= 0 ;

 hence thesis by A1, A3, A7;

 end;

 suppose

 A8: a < 0 ;

 now

 per cases ;

 suppose b >= 0 ;

 then

 A9: (n -root b) >= 0 by A7, Th7;

 (n -root ( - a)) >= 0 by A7, A8, Th7;

 then ( - (n -root ( - a))) <= ( - 0 );

 hence thesis by A6, A9, Th10;

 end;

 suppose

 A10: b < 0 ;

 ( - a) >= ( - b) by A1, XREAL_1: 24;

 then (n -root ( - a)) >= (n -root ( - b)) by A3, A7, A10;

 then ( - (n -root ( - a))) <= ( - (n -root ( - b))) by XREAL_1: 24;

 then (n -root a) <= ( - (n -root ( - b))) by A6, Th10;

 hence thesis by A6, Th10;

 end;

 end;

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 hence thesis by A1, A2, A3;

 end;

 theorem :: POWER:17

 a = 0 & n >= 1 or n is odd) implies (n -root a) < (n -root b)

 proof

 assume that

 A1: a = 1 or n is odd;

 A3:

 now

 let a, b, n;

 assume that

 A4: 0 <= a & n >= 1 and

 A5: a < b;

 (n -Root a) < (n -Root b) by A4, A5, PREPOWER: 28;

 then (n -Root a) < (n -root b) by A4, A5, Def1;

 hence (n -root a) < (n -root b) by A4, Def1;

 end;

 now

 assume

 A6: n is odd;

 then

 A7: n >= 1 by ABIAN: 12;

 now

 per cases ;

 suppose a >= 0 ;

 hence thesis by A1, A3, A7;

 end;

 suppose

 A8: a < 0 ;

 then

 A9: ( - a) > 0 by XREAL_1: 58;

 now

 per cases ;

 suppose b >= 0 ;

 then

 A10: (n -root b) >= 0 by A7, Th7;

 (n -Root ( - a)) > 0 by A7, A9, PREPOWER:def 2;

 then ( - (n -Root ( - a))) < ( - 0 ) by XREAL_1: 24;

 hence thesis by A6, A8, A10, Def1;

 end;

 suppose

 A11: b < 0 ;

 ( - a) > ( - b) by A1, XREAL_1: 24;

 then (n -root ( - a)) > (n -root ( - b)) by A3, A7, A11;

 then ( - (n -root ( - a))) < ( - (n -root ( - b))) by XREAL_1: 24;

 then (n -root a) < ( - (n -root ( - b))) by A6, Th10;

 hence thesis by A6, Th10;

 end;

 end;

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 hence thesis by A1, A2, A3;

 end;

 theorem :: POWER:18



 Th18: 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) >= 1 & a >= (n -Root a) by A1, A2, PREPOWER: 29;

 hence thesis by A2, Def1;

 end;

 theorem :: POWER:19

 a <= ( - 1) & n is odd implies (n -root a) <= ( - 1) & a <= (n -root a)

 proof

 assume that

 A1: a <= ( - 1) and

 A2: n is odd;



 A3: n >= 1 & ( - a) >= 1 by A1, A2, ABIAN: 12, XREAL_1: 25;

 then

 A4: (n -root ( - a)) >= 1 by Th18;



 A5: ( - a) >= (n -root ( - a)) by A3, Th18;



 A6: ( - (n -root ( - a))) <= ( - 1) by A4, XREAL_1: 24;

 a <= ( - (n -root ( - a))) by A5, XREAL_1: 25;

 hence thesis by A2, A6, Th10;

 end;

 theorem :: POWER:20



 Th20: a >= 0 & a < 1 & n >= 1 implies a <= (n -root a) & (n -root a) < 1

 proof

 assume that

 A1: a >= 0 and

 A2: a < 1 and

 A3: n >= 1;

 a <= (n -Root a) & (n -Root a) < 1 by A1, A2, A3, PREPOWER: 30;

 hence thesis by A1, A3, Def1;

 end;

 theorem :: POWER:21

 a > ( - 1) & a <= 0 & n is odd implies a >= (n -root a) & (n -root a) > ( - 1)

 proof

 assume that

 A1: a > ( - 1) and

 A2: a <= 0 ;

 assume n is odd;

 then

 A3: ex m st n = ((2 * m) + 1) by ABIAN: 9;

 then

 A4: n >= 1 & ( - a) < 1 by A1, ABIAN: 12, XREAL_1: 25;

 then

 A5: (n -root ( - a)) < 1 by A2, Th20;



 A6: ( - a) <= (n -root ( - a)) by A2, A4, Th20;



 A7: ( - (n -root ( - a))) > ( - 1) by A5, XREAL_1: 24;

 a >= ( - (n -root ( - a))) by A6, XREAL_1: 26;

 hence thesis by A3, A7, Th10;

 end;

 theorem :: POWER:22



 Th22: a > 0 & n >= 1 implies ((n -root a) - 1) <= ((a - 1) / n)

 proof

 assume

 A1: a > 0 & n >= 1;

 then ((n -Root a) - 1) <= ((a - 1) / n) by PREPOWER: 31;

 hence thesis by A1, Def1;

 end;

 theorem :: POWER:23



 Th23: for s be Real_Sequence, a 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, a;

 assume that

 A1: a > 0 and

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

 now

 let n be Nat;

 assume

 A3: n >= 1;



 hence (s . n) = (n -root a) by A2

 .= (n -Root a) by A1, A3, Def1;

 end;

 hence thesis by A1, PREPOWER: 33;

 end;

 definition

 let a,b be Real;

 :: POWER:def2

 func a to_power b -> Real means

 : Def2: it = (a #R b) if a > 0 ,

it = 0 if a = 0 & b > 0 ,

ex k st k = b & it = (a #Z k) if b is Integer;

 consistency

 proof

 let IT be Real;

 thus a > 0 & a = 0 & b > 0 implies (IT = (a #R b) iff IT = 0 );

 thus a > 0 & b is Integer implies (IT = (a #R b) iff ex k st k = b & IT = (a #Z k))

 proof

 assume

 A1: a > 0 ;

 assume b is Integer;

 then

 reconsider b as Integer;

 (a #R b) = (a #Q b) by A1, PREPOWER: 74

 .= (a #Z b) by A1, PREPOWER: 99;

 hence thesis;

 end;

 a = 0 & b > 0 & b is Integer implies (IT = 0 iff ex k st k = b & IT = (a #Z k))

 proof

 assume

 A2: a = 0 ;

 assume that

 A3: b > 0 and

 A4: b is Integer;

 b in NAT by A3, A4, INT_1: 3;

 then

 reconsider b as Nat;

 (a #Z b) = (a |^ b) by PREPOWER: 36

 .= 0 by A2, A3, NAT_1: 14, NEWTON: 11;

 hence thesis;

 end;

 hence thesis;

 end;

 existence

 proof

 now

 assume b is Integer;

 then

 reconsider k = b as Integer;

 take c = (a #Z k);

 thus ex k st k = b & c = (a #Z k);

 end;

 hence thesis;

 end;

 uniqueness ;

 end

 theorem :: POWER:24



 Th24: (a to_power 0 ) = 1

 proof



 thus (a to_power 0 ) = (a #Z 0 ) by Def2

 .= 1 by PREPOWER: 34;

 end;

 theorem :: POWER:25

 (a to_power 1) = a

 proof



 thus (a to_power 1) = (a #Z 1) by Def2

 .= a by PREPOWER: 35;

 end;

 theorem :: POWER:26



 Th26: (1 to_power a) = 1

 proof



 A1: (1 #R a) <> 0 by PREPOWER: 81;



 thus (1 to_power a) = ((1 / 1) #R a) by Def2

 .= ((1 #R a) / (1 #R a)) by PREPOWER: 80

 .= 1 by A1, XCMPLX_1: 60;

 end;

 theorem :: POWER:27



 Th27: a > 0 implies (a to_power (b + c)) = ((a to_power b) * (a to_power c))

 proof

 assume

 A1: a > 0 ;

 then (a #R (b + c)) = ((a #R b) * (a #R c)) by PREPOWER: 75;

 then (a #R (b + c)) = ((a #R b) * (a to_power c)) by A1, Def2;

 then (a #R (b + c)) = ((a to_power b) * (a to_power c)) by A1, Def2;

 hence thesis by A1, Def2;

 end;

 theorem :: POWER:28



 Th28: a > 0 implies (a to_power ( - c)) = (1 / (a to_power c))

 proof

 assume

 A1: a > 0 ;

 then (a #R ( - c)) = (1 / (a #R c)) by PREPOWER: 76;

 then (a #R ( - c)) = (1 / (a to_power c)) by A1, Def2;

 hence thesis by A1, Def2;

 end;

 theorem :: POWER:29



 Th29: a > 0 implies (a to_power (b - c)) = ((a to_power b) / (a to_power c))

 proof

 assume

 A1: a > 0 ;

 then (a #R (b - c)) = ((a #R b) / (a #R c)) by PREPOWER: 77;

 then (a #R (b - c)) = ((a #R b) / (a to_power c)) by A1, Def2;

 then (a #R (b - c)) = ((a to_power b) / (a to_power c)) by A1, Def2;

 hence thesis by A1, Def2;

 end;

 theorem :: POWER:30

 a > 0 & b > 0 implies ((a * b) to_power c) = ((a to_power c) * (b to_power c))

 proof

 assume that

 A1: a > 0 and

 A2: b > 0 ;



 A3: (a * b) > 0 by A1, A2, XREAL_1: 129;

 ((a * b) #R c) = ((a #R c) * (b #R c)) by A1, A2, PREPOWER: 78;

 then ((a * b) #R c) = ((a #R c) * (b to_power c)) by A2, Def2;

 then ((a * b) #R c) = ((a to_power c) * (b to_power c)) by A1, Def2;

 hence thesis by A3, Def2;

 end;

 theorem :: POWER:31



 Th31: a > 0 & b > 0 implies ((a / b) to_power c) = ((a to_power c) / (b to_power c))

 proof

 assume that

 A1: a > 0 and

 A2: b > 0 ;



 A3: (a / b) > 0 by A1, A2, XREAL_1: 139;

 ((a / b) #R c) = ((a #R c) / (b #R c)) by A1, A2, PREPOWER: 80;

 then ((a / b) #R c) = ((a #R c) / (b to_power c)) by A2, Def2;

 then ((a / b) #R c) = ((a to_power c) / (b to_power c)) by A1, Def2;

 hence thesis by A3, Def2;

 end;

 theorem :: POWER:32



 Th32: a > 0 implies ((1 / a) to_power b) = (a to_power ( - b))

 proof

 assume

 A1: a > 0 ;



 hence ((1 / a) to_power b) = ((1 / a) #R b) by Def2

 .= (1 / (a #R b)) by A1, PREPOWER: 79

 .= (1 / (a to_power b)) by A1, Def2

 .= (a to_power ( - b)) by A1, Th28;

 end;

 theorem :: POWER:33



 Th33: a > 0 implies ((a to_power b) to_power c) = (a to_power (b * c))

 proof

 assume

 A1: a > 0 ;

 then

 A2: (a #R b) > 0 by PREPOWER: 81;

 ((a #R b) #R c) = (a #R (b * c)) by A1, PREPOWER: 91;

 then ((a #R b) #R c) = (a to_power (b * c)) by A1, Def2;

 then ((a #R b) to_power c) = (a to_power (b * c)) by A2, Def2;

 hence thesis by A1, Def2;

 end;

 theorem :: POWER:34



 Th34: a > 0 implies (a to_power b) > 0

 proof

 assume

 A1: a > 0 ;

 then (a #R b) > 0 by PREPOWER: 81;

 hence thesis by A1, Def2;

 end;

 theorem :: POWER:35



 Th35: a > 1 & b > 0 implies (a to_power b) > 1

 proof

 assume that

 A1: a > 1 and

 A2: b > 0 ;

 (a #R b) > 1 by A1, A2, PREPOWER: 86;

 hence thesis by A1, Def2;

 end;

 theorem :: POWER:36



 Th36: a > 1 & b < 0 implies (a to_power b) < 1

 proof

 assume that

 A1: a > 1 and

 A2: b < 0 ;

 (a #R b) < 1 by A1, A2, PREPOWER: 88;

 hence thesis by A1, Def2;

 end;

 theorem :: POWER:37

 a > 0 & a 0 implies (a to_power c) < (b to_power c)

 proof

 assume that

 A1: a > 0 and

 A2: a 0 ;



 A4: (a to_power c) > 0 by A1, Th34;



 A5: (a to_power c) <> 0 by A1, Th34;

 (a / a) < (b / a) by A1, A2, XREAL_1: 74;

 then 1 < (b / a) by A1, XCMPLX_1: 60;

 then ((b / a) to_power c) > 1 by A3, Th35;

 then ((b to_power c) / (a to_power c)) > 1 by A1, A2, Th31;

 then (((b to_power c) / (a to_power c)) * (a to_power c)) > (1 * (a to_power c)) by A4, XREAL_1: 68;

 hence thesis by A5, XCMPLX_1: 87;

 end;

 theorem :: POWER:38

 a > 0 & a (b to_power c)

 proof

 assume that

 A1: a > 0 and

 A2: a 0 by A1, Th34;



 A5: (a to_power c) <> 0 by A1, Th34;

 (a / a) < (b / a) by A1, A2, XREAL_1: 74;

 then 1 < (b / a) by A1, XCMPLX_1: 60;

 then ((b / a) to_power c) < 1 by A3, Th36;

 then ((b to_power c) / (a to_power c)) < 1 by A1, A2, Th31;

 then (((b to_power c) / (a to_power c)) * (a to_power c)) < (1 * (a to_power c)) by A4, XREAL_1: 68;

 hence thesis by A5, XCMPLX_1: 87;

 end;

 theorem :: POWER:39



 Th39: a 1 implies (c to_power a) < (c to_power b)

 proof

 assume that

 A1: a 1;



 A3: (c to_power a) > 0 by A2, Th34;



 A4: (c to_power a) <> 0 by A2, Th34;

 (b - a) > 0 by A1, XREAL_1: 50;

 then (c to_power (b - a)) > 1 by A2, Th35;

 then ((c to_power b) / (c to_power a)) > 1 by A2, Th29;

 then (((c to_power b) / (c to_power a)) * (c to_power a)) > (1 * (c to_power a)) by A3, XREAL_1: 68;

 hence thesis by A4, XCMPLX_1: 87;

 end;

 theorem :: POWER:40



 Th40: a 0 & c < 1 implies (c to_power a) > (c to_power b)

 proof

 assume that

 A1: a 0 and

 A3: c < 1;



 A4: ((1 / c) to_power a) > 0 by A2, Th34;



 A5: ((1 / c) to_power a) <> 0 by A2, Th34;



 A6: (c to_power a) > 0 by A2, Th34;

 (c / c) < (1 / c) by A2, A3, XREAL_1: 74;

 then

 A7: 1 < (1 / c) by A2, XCMPLX_1: 60;

 (b - a) > 0 by A1, XREAL_1: 50;

 then ((1 / c) to_power (b - a)) > 1 by A7, Th35;

 then (((1 / c) to_power b) / ((1 / c) to_power a)) > 1 by A2, Th29;

 then ((((1 / c) to_power b) / ((1 / c) to_power a)) * ((1 / c) to_power a)) > (1 * ((1 / c) to_power a)) by A4, XREAL_1: 68;

 then ((1 / c) to_power b) > ((1 / c) to_power a) by A5, XCMPLX_1: 87;

 then ((1 to_power b) / (c to_power b)) > ((1 / c) to_power a) by A2, Th31;

 then (1 / (c to_power b)) > ((1 / c) to_power a) by Th26;

 then (1 / (c to_power b)) > ((1 to_power a) / (c to_power a)) by A2, Th31;

 then (1 / (c to_power b)) > (1 / (c to_power a)) by Th26;

 hence thesis by A6, XREAL_1: 91;

 end;

 registration

 let a be Real, n be Nat;

 identify a |^ n with a to_power n;

 compatibility

 proof



 thus (a to_power n) = (a #Z n) by Def2

 .= (a |^ n) by PREPOWER: 36;

 end;

 end

 theorem :: POWER:41

 for n be Nat holds (a to_power n) = (a |^ n);

 theorem :: POWER:42



 Th42: k <> 0 implies ( 0 to_power k) = 0

 proof

 ( 0 to_power k) = ( 0 #Z k) by Def2;

 hence thesis by PREPOWER: 100;

 end;

 theorem :: POWER:43

 (a to_power k) = (a #Z k) by Def2;

 theorem :: POWER:44



 Th44: a > 0 implies (a to_power p) = (a #Q p)

 proof

 assume

 A1: a > 0 ;



 hence (a to_power p) = (a #R p) by Def2

 .= (a #Q p) by A1, PREPOWER: 74;

 end;

 theorem :: POWER:45



 Th45: a >= 0 & n >= 1 implies (a to_power (1 / n)) = (n -root a)

 proof

 assume that

 A1: a >= 0 and

 A2: n >= 1;

 reconsider p = (n " ) as Rational;

 now

 per cases by A1;

 suppose a > 0 ;



 hence (a to_power (1 / n)) = (a #Q p) by Th44

 .= (n -Root a) by A2, PREPOWER: 50;

 end;

 suppose

 A3: a = 0 ;



 hence (a to_power (1 / n)) = 0 by A2, Def2

 .= (n -Root a) by A2, A3, PREPOWER:def 2;

 end;

 end;

 hence thesis by A1, A2, Def1;

 end;

 theorem :: POWER:46



 Th46: (a to_power 2) = (a ^2 )

 proof

 now

 per cases ;

 suppose

 A1: a > 0 ;



 thus (a to_power 2) = (a to_power (1 + 1))

 .= ((a to_power 1) * (a to_power 1)) by A1, Th27

 .= ((a to_power 1) * a)

 .= (a ^2 );

 end;

 suppose a = 0 ;

 hence thesis by Def2;

 end;

 suppose

 A2: a < 0 ;

 reconsider l = 1 as Integer;



 thus (a to_power 2) = (a #Z (l + l)) by Def2

 .= ((a #Z l) * (a #Z l)) by A2, PREPOWER: 44

 .= (a * (a #Z l)) by PREPOWER: 35

 .= (a ^2 ) by PREPOWER: 35;

 end;

 end;

 hence thesis;

 end;

 theorem :: POWER:47



 Th47: k is even implies (( - a) to_power k) = (a to_power k)

 proof

 given l such that

 A1: k = (2 * l);

 per cases ;

 suppose a = 0 ;

 hence thesis;

 end;

 suppose a > 0 ;



 hence (a to_power k) = ((a to_power 2) to_power l) by A1, Th33

 .= ((a ^2 ) to_power l) by Th46

 .= ((( - a) ^2 ) to_power l)

 .= ((( - a) to_power 2) to_power l) by Th46

 .= ((( - a) #Z 2) to_power l) by Def2

 .= ((( - a) #Z 2) #Z l) by Def2

 .= (( - a) #Z (2 * l)) by PREPOWER: 45

 .= (( - a) to_power k) by A1, Def2;

 end;

 suppose a < 0 ;

 then ( - a) > 0 by XREAL_1: 58;



 hence (( - a) to_power k) = ((( - a) to_power 2) to_power l) by A1, Th33

 .= ((( - a) ^2 ) to_power l) by Th46

 .= ((a ^2 ) to_power l)

 .= ((a to_power 2) to_power l) by Th46

 .= ((a #Z 2) to_power l) by Def2

 .= ((a #Z 2) #Z l) by Def2

 .= (a #Z (2 * l)) by PREPOWER: 45

 .= (a to_power k) by A1, Def2;

 end;

 end;

 theorem :: POWER:48

 k is odd implies (( - a) to_power k) = ( - (a to_power k))

 proof

 assume

 A1: k is odd;

 then

 consider l such that

 A2: k = ((2 * l) + 1) by ABIAN: 1;

 per cases ;

 suppose

 A3: a = 0 ;

 k <> 0 by A1;

 then (a to_power k) = 0 by A3, Th42;

 hence thesis by A3;

 end;

 suppose

 A4: a > 0 ;

 then

 A5: ( - a) <> ( - 0 );

 (a to_power k) = ((a to_power (2 * l)) * (a to_power 1)) by A2, A4, Th27

 .= ((a to_power (2 * l)) * a)

 .= ((( - a) to_power (2 * l)) * a) by Th47

 .= ( - ((( - a) to_power (2 * l)) * ( - a)))

 .= ( - ((( - a) #Z (2 * l)) * ( - a))) by Def2

 .= ( - ((( - a) #Z (2 * l)) * (( - a) #Z 1))) by PREPOWER: 35

 .= ( - (( - a) #Z k)) by A2, A5, PREPOWER: 44

 .= ( - (( - a) to_power k)) by Def2;

 hence thesis;

 end;

 suppose

 A6: a < 0 ;

 then ( - a) > 0 by XREAL_1: 58;



 hence (( - a) to_power k) = ((( - a) to_power (2 * l)) * (( - a) to_power 1)) by A2, Th27

 .= ((( - a) to_power (2 * l)) * ( - a))

 .= ((a to_power (2 * l)) * ( - a)) by Th47

 .= ( - ((a to_power (2 * l)) * a))

 .= ( - ((a #Z (2 * l)) * a)) by Def2

 .= ( - ((a #Z (2 * l)) * (a #Z 1))) by PREPOWER: 35

 .= ( - (a #Z k)) by A2, A6, PREPOWER: 44

 .= ( - (a to_power k)) by Def2;

 end;

 end;

 theorem :: POWER:49

 ( - 1) < a implies ((1 + a) to_power n) >= (1 + (n * a)) by PREPOWER: 16;

 theorem :: POWER:50



 Th50: a > 0 & a <> 1 & c <> d implies (a to_power c) <> (a to_power d)

 proof

 assume that

 A1: a > 0 and

 A2: a <> 1 and

 A3: c <> d;

 now

 per cases by A3, XXREAL_0: 1;

 suppose

 A4: c < d;

 now

 per cases by A2, XXREAL_0: 1;

 suppose a < 1;

 hence thesis by A1, A4, Th40;

 end;

 suppose a > 1;

 hence thesis by A4, Th39;

 end;

 end;

 hence thesis;

 end;

 suppose

 A5: c > d;

 now

 per cases by A2, XXREAL_0: 1;

 suppose a < 1;

 hence thesis by A1, A5, Th40;

 end;

 suppose a > 1;

 hence thesis by A5, Th39;

 end;

 end;

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 definition

 let a,b be Real;

 assume that

 A1: a > 0 and

 A2: a <> 1 and

 A3: b > 0 ;

 :: POWER:def3

 func log (a,b) -> Real means

 : Def3: (a to_power it ) = b;

 existence

 proof

 reconsider a1 = a, b1 = b as Real;

 set X = { c where c be Real : (a to_power c) <= b };

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

 proof

 let x be object;

 assume x in X;

 then ex c be Real st x = c & (a to_power c) <= b;

 hence thesis by XREAL_0:def 1;

 end;

 then

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



 A4: ex d st d in X

 proof

 A5:

 now

 let a,b be Real such that

 A6: a > 1 and

 A7: b > 0 ;

 reconsider a1 = a, b1 = b as Real;

 set e = (a1 - 1);

 consider n be Nat such that

 A8: n > (1 / (b * e)) by SEQ_4: 3;

 e > ( 0 - 1) by A6, XREAL_1: 9;

 then

 A9: ((1 + e) to_power n) >= (1 + (n * e)) by PREPOWER: 16;

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

 then

 A10: ((1 + e) to_power n) >= (n * e) by A9, XXREAL_0: 2;



 A11: e > (1 - 1) by A6, XREAL_1: 9;

 then (n * e) > ((1 / (b * e)) * e) by A8, XREAL_1: 68;

 then (n * e) >= (1 / b) by A11, XCMPLX_1: 92;

 then (a to_power n) >= (1 / b) by A10, XXREAL_0: 2;

 then (1 / (a to_power n)) <= (1 / (1 / b)) by A7, XREAL_1: 85;

 then (a1 to_power ( - n)) <= b1 by A6, Th28;

 hence ex d st (a to_power d) <= b;

 end;

 now

 per cases by A2, XXREAL_0: 1;

 suppose a > 1;

 hence ex d st (a to_power d) <= b by A3, A5;

 end;

 suppose a < 1;

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

 then

 consider d such that

 A12: ((1 / a) to_power d) <= b by A3, A5;

 (a1 to_power ( - d)) <= b1 by A1, A12, Th32;

 hence ex e st (a to_power e) <= b;

 end;

 end;

 then

 consider d such that

 A13: (a to_power d) <= b;

 take d;

 thus thesis by A13;

 end;

 now

 per cases by A2, XXREAL_0: 1;

 suppose

 A14: a > 1;



 A15: X is bounded_above

 proof

 consider n be Nat such that

 A16: n > ((b1 - 1) / (a1 - 1)) by SEQ_4: 3;

 (a - 1) > (1 - 1) by A14, XREAL_1: 9;

 then (n * (a - 1)) > (b - 1) by A16, XREAL_1: 77;

 then

 A17: (1 + (n * (a - 1))) > (1 + (b - 1)) by XREAL_1: 6;

 (a - 1) > ( 0 - 1) by A1, XREAL_1: 9;

 then ((1 + (a1 - 1)) to_power n) >= (1 + (n * (a1 - 1))) by PREPOWER: 16;

 then

 A18: (a to_power n) > b by A17, XXREAL_0: 2;

 take n;

 let c be ExtReal;

 assume c in X;

 then

 consider d be Real such that

 A19: d = c & (a to_power d) <= b;

 (a1 to_power d) <= (a1 to_power n) by A18, A19, XXREAL_0: 2;

 hence c <= n by A14, Th39, A19;

 end;

 take d = ( upper_bound X);



 A20: not b < (a to_power d)

 proof

 assume (a to_power d) > b;

 then

 consider e be Real such that

 A21: b < e and

 A22: e < (a to_power d) by XREAL_1: 5;

 reconsider e as Real;

 consider n be Nat such that

 A23: n > ((a1 - 1) / ((e / b1) - 1)) by SEQ_4: 3;

 reconsider m = ( max (1,n)) as Element of NAT by ORDINAL1:def 12;

 n <= m by XXREAL_0: 25;

 then

 A24: ((a - 1) / ((e / b) - 1)) < m by A23, XXREAL_0: 2;

 (e / b) > 1 by A3, A21, XREAL_1: 187;

 then ((e / b) - 1) > (1 - 1) by XREAL_1: 9;

 then

 A25: (a - 1) < (m * ((e / b) - 1)) by A24, XREAL_1: 77;



 A26: 1 <= m by XXREAL_0: 25;

 then ((a - 1) / m) < ((e / b) - 1) by A25, XREAL_1: 83;

 then

 A27: (((a - 1) / m) + 1) < (((e / b) - 1) + 1) by XREAL_1: 6;

 ((m -root a1) - 1) <= ((a1 - 1) / m) by A1, Th22, XXREAL_0: 25;

 then (((m -root a) - 1) + 1) <= (((a - 1) / m) + 1) by XREAL_1: 6;

 then (m -root a) <= (e / b) by A27, XXREAL_0: 2;

 then (a1 to_power (1 / m)) <= (e / b1) by A1, Th45, XXREAL_0: 25;

 then

 A28: ((a to_power (1 / m)) * b) <= e by A3, XREAL_1: 83;

 consider c be Real such that

 A29: c in X and

 A30: (d - (1 / m)) < c by A4, A15, A26, SEQ_4:def 1;

 reconsider c as Real;



 A31: ex g be Real st g = c & (a to_power g) <= b by A29;

 (a1 to_power (1 / m)) >= 0 by A1, Th34;

 then ((a to_power c) * (a to_power (1 / m))) <= ((a to_power (1 / m)) * b) by A31, XREAL_1: 64;

 then ((a to_power c) * (a to_power (1 / m))) <= e by A28, XXREAL_0: 2;

 then

 A32: (a1 to_power (c + (1 / m))) <= e by A1, Th27;

 d < (c + (1 / m)) by A30, XREAL_1: 19;

 then (a1 to_power d) <= (a1 to_power (c + (1 / m))) by A14, Th39;

 hence contradiction by A22, A32, XXREAL_0: 2;

 end;

 not (a to_power d) < b

 proof

 assume (a to_power d) < b;

 then

 consider e be Real such that

 A33: (a to_power d) < e and

 A34: e 0 by A1, Th34;

 then (b / e) > 1 by A33, A34, XREAL_1: 187;

 then

 A36: ((b / e) - 1) > (1 - 1) by XREAL_1: 9;

 deffunc F( Nat) = ($1 -root a);

 consider s be Real_Sequence such that

 A37: for n be Nat holds (s . n) = F(n) from SEQ_1:sch 1;

 for n st n >= 1 holds (s . n) = (n -root a1) by A37;

 then s is convergent & ( lim s) = 1 by A1, Th23;

 then

 consider n be Nat such that

 A38: for m be Nat st m >= n holds |.((s . m) - 1).| < ((b / e) - 1) by A36, SEQ_2:def 7;

 reconsider m = ( max (1,n)) as Element of NAT by ORDINAL1:def 12;

 |.((s . m) - 1).| < ((b / e) - 1) by A38, XXREAL_0: 25;

 then

 A39: |.((m -root a) - 1).| < ((b / e) - 1) by A37;

 ((m -root a) - 1) <= |.((m -root a) - 1).| by ABSVALUE: 4;

 then ((m -root a) - 1) < ((b / e) - 1) by A39, XXREAL_0: 2;

 then (m -root a) < (b / e) by XREAL_1: 9;

 then (a1 to_power (1 / m)) < (b1 / e) by A1, Th45, XXREAL_0: 25;

 then ((a to_power d) * (a to_power (1 / m))) < ((b / e) * (a to_power d)) by A35, XREAL_1: 68;

 then

 A40: (a to_power (d + (1 / m))) < ((b * (a to_power d)) / e) by A1, Th27;

 ((a to_power d) / e) < 1 by A33, A35, XREAL_1: 189;

 then (((a to_power d) / e) * b) < (1 * b) by A3, XREAL_1: 68;

 then (a to_power (d + (1 / m))) <= b by A40, XXREAL_0: 2;

 then (d + (1 / m)) in X;

 then m >= 1 & (d + (1 / m)) <= d by A15, SEQ_4:def 1, XXREAL_0: 25;

 hence contradiction by XREAL_1: 29;

 end;

 hence b = (a to_power d) by A20, XXREAL_0: 1;

 end;

 suppose

 A41: a < 1;



 A42: X is bounded_below

 proof

 consider n be Nat such that

 A43: n > ((b1 - 1) / ((1 / a1) - 1)) by SEQ_4: 3;

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

 then ((1 / a) - 1) > (1 - 1) by XREAL_1: 9;

 then (n * ((1 / a) - 1)) > (b - 1) by A43, XREAL_1: 77;

 then

 A44: (1 + (n * ((1 / a) - 1))) > (1 + (b - 1)) by XREAL_1: 6;

 ((1 / a) - 1) > ( 0 - 1) by A1, XREAL_1: 9;

 then ((1 + ((1 / a1) - 1)) to_power n) >= (1 + (n * ((1 / a1) - 1))) by PREPOWER: 16;

 then ((1 / a) to_power n) > b by A44, XXREAL_0: 2;

 then

 A45: (a1 to_power ( - n)) > b1 by A1, Th32;

 take ( - n);

 let c be ExtReal;

 assume c in X;

 then

 consider d be Real such that

 A46: d = c & (a to_power d) <= b;

 (a1 to_power d) <= (a1 to_power ( - n)) by A45, A46, XXREAL_0: 2;

 hence c >= ( - n) by A1, A41, Th40, A46;

 end;

 take d = ( lower_bound X);



 A47: not b < (a to_power d)

 proof

 assume (a to_power d) > b;

 then

 consider e be Real such that

 A48: b < e and

 A49: e < (a to_power d) by XREAL_1: 5;

 reconsider e as Real;

 consider n be Nat such that

 A50: n > (((1 / a1) - 1) / ((e / b1) - 1)) by SEQ_4: 3;

 reconsider m = ( max (1,n)) as Element of NAT by ORDINAL1:def 12;

 n <= m by XXREAL_0: 25;

 then

 A51: (((1 / a) - 1) / ((e / b) - 1)) < m by A50, XXREAL_0: 2;

 (e / b) > 1 by A3, A48, XREAL_1: 187;

 then ((e / b) - 1) > (1 - 1) by XREAL_1: 9;

 then

 A52: ((1 / a) - 1) < (m * ((e / b) - 1)) by A51, XREAL_1: 77;



 A53: 1 <= m by XXREAL_0: 25;

 then (((1 / a) - 1) / m) < ((e / b) - 1) by A52, XREAL_1: 83;

 then

 A54: ((((1 / a) - 1) / m) + 1) < (((e / b) - 1) + 1) by XREAL_1: 6;

 ((m -root (1 / a1)) - 1) <= (((1 / a1) - 1) / m) by A1, Th22, XXREAL_0: 25;

 then (((m -root (1 / a)) - 1) + 1) <= ((((1 / a) - 1) / m) + 1) by XREAL_1: 6;

 then (m -root (1 / a)) <= (e / b) by A54, XXREAL_0: 2;

 then ((1 / a1) to_power (1 / m)) <= (e / b1) by A1, Th45, XXREAL_0: 25;

 then (((1 / a) to_power (1 / m)) * b) <= e by A3, XREAL_1: 83;

 then

 A55: ((a1 to_power ( - (1 / m))) * b1) <= e by A1, Th32;

 consider c be Real such that

 A56: c in X and

 A57: c < (d + (1 / m)) by A4, A42, A53, SEQ_4:def 2;

 reconsider c as Real;



 A58: ex g be Real st g = c & (a to_power g) <= b by A56;

 (a1 to_power ( - (1 / m))) >= 0 by A1, Th34;

 then ((a to_power c) * (a to_power ( - (1 / m)))) <= ((a to_power ( - (1 / m))) * b) by A58, XREAL_1: 64;

 then ((a to_power c) * (a to_power ( - (1 / m)))) <= e by A55, XXREAL_0: 2;

 then

 A59: (a1 to_power (c + ( - (1 / m)))) <= e by A1, Th27;

 d > (c - (1 / m)) by A57, XREAL_1: 19;

 then (a1 to_power d) <= (a1 to_power (c - (1 / m))) by A1, A41, Th40;

 hence contradiction by A49, A59, XXREAL_0: 2;

 end;

 not (a to_power d) < b

 proof

 assume (a to_power d) < b;

 then

 consider e be Real such that

 A60: (a to_power d) < e and

 A61: e 0 by A1, Th34;

 then (b / e) > 1 by A60, A61, XREAL_1: 187;

 then

 A63: ((b / e) - 1) > (1 - 1) by XREAL_1: 9;

 deffunc F( Nat) = ($1 -root (1 / a));

 consider s be Real_Sequence such that

 A64: for n be Nat holds (s . n) = F(n) from SEQ_1:sch 1;

 for n st n >= 1 holds (s . n) = (n -root (1 / a1)) by A64;

 then s is convergent & ( lim s) = 1 by A1, Th23;

 then

 consider n be Nat such that

 A65: for m be Nat st m >= n holds |.((s . m) - 1).| < ((b / e) - 1) by A63, SEQ_2:def 7;

 reconsider m = ( max (1,n)) as Element of NAT by ORDINAL1:def 12;

 |.((s . m) - 1).| < ((b / e) - 1) by A65, XXREAL_0: 25;

 then

 A66: |.((m -root (1 / a)) - 1).| < ((b / e) - 1) by A64;

 ((m -root (1 / a)) - 1) <= |.((m -root (1 / a)) - 1).| by ABSVALUE: 4;

 then ((m -root (1 / a)) - 1) < ((b / e) - 1) by A66, XXREAL_0: 2;

 then (m -root (1 / a)) < (b / e) by XREAL_1: 9;

 then ((1 / a1) to_power (1 / m)) < (b1 / e) by A1, Th45, XXREAL_0: 25;

 then ((a to_power d) * ((1 / a) to_power (1 / m))) < ((b / e) * (a to_power d)) by A62, XREAL_1: 68;

 then ((a1 to_power d) * (a1 to_power ( - (1 / m)))) < ((b1 / e) * (a1 to_power d)) by A1, Th32;

 then

 A67: (a to_power (d - (1 / m))) < ((b * (a to_power d)) / e) by A1, Th27;

 ((a to_power d) / e) < 1 by A60, A62, XREAL_1: 189;

 then (((a to_power d) / e) * b) < (1 * b) by A3, XREAL_1: 68;

 then (a to_power (d - (1 / m))) = 1 & (d - (1 / m)) >= d by A42, SEQ_4:def 2, XXREAL_0: 25;

 hence contradiction by XREAL_1: 44;

 end;

 hence b = (a to_power d) by A47, XXREAL_0: 1;

 end;

 end;

 hence thesis;

 end;

 uniqueness by A1, A2, Th50;

 end

 theorem :: POWER:51

 a > 0 & a <> 1 implies ( log (a,1)) = 0

 proof

 assume

 A1: a > 0 & a <> 1;

 (a to_power 0 ) = 1 by Th24;

 hence thesis by A1, Def3;

 end;

 theorem :: POWER:52

 a > 0 & a <> 1 implies ( log (a,a)) = 1

 proof

 assume

 A1: a > 0 & a <> 1;

 (a to_power 1) = a;

 hence thesis by A1, Def3;

 end;

 theorem :: POWER:53

 a > 0 & a <> 1 & b > 0 & c > 0 implies (( log (a,b)) + ( log (a,c))) = ( log (a,(b * c)))

 proof

 assume that

 A1: a > 0 and

 A2: a <> 1 and

 A3: b > 0 and

 A4: c > 0 ;



 A5: (a to_power (( log (a,b)) + ( log (a,c)))) = ((a to_power ( log (a,b))) * (a to_power ( log (a,c)))) by A1, Th27

 .= (b * (a to_power ( log (a,c)))) by A1, A2, A3, Def3

 .= (b * c) by A1, A2, A4, Def3;

 (b * c) > 0 by A3, A4, XREAL_1: 129;

 hence thesis by A1, A2, A5, Def3;

 end;

 theorem :: POWER:54

 a > 0 & a <> 1 & b > 0 & c > 0 implies (( log (a,b)) - ( log (a,c))) = ( log (a,(b / c)))

 proof

 assume that

 A1: a > 0 and

 A2: a <> 1 and

 A3: b > 0 and

 A4: c > 0 ;



 A5: (a to_power (( log (a,b)) - ( log (a,c)))) = ((a to_power ( log (a,b))) / (a to_power ( log (a,c)))) by A1, Th29

 .= (b / (a to_power ( log (a,c)))) by A1, A2, A3, Def3

 .= (b / c) by A1, A2, A4, Def3;

 (b / c) > 0 by A3, A4, XREAL_1: 139;

 hence thesis by A1, A2, A5, Def3;

 end;

 theorem :: POWER:55

 a > 0 & a <> 1 & b > 0 implies ( log (a,(b to_power c))) = (c * ( log (a,b)))

 proof

 assume that

 A1: a > 0 and

 A2: a <> 1 and

 A3: b > 0 ;



 A4: (b to_power c) > 0 by A3, Th34;

 (a to_power (c * ( log (a,b)))) = ((a to_power ( log (a,b))) to_power c) by A1, Th33

 .= (b to_power c) by A1, A2, A3, Def3;

 hence thesis by A1, A2, A4, Def3;

 end;

 theorem :: POWER:56

 a > 0 & a <> 1 & b > 0 & b <> 1 & c > 0 implies ( log (a,c)) = (( log (a,b)) * ( log (b,c)))

 proof

 assume that

 A1: a > 0 and

 A2: a <> 1 and

 A3: b > 0 and

 A4: b <> 1 and

 A5: c > 0 ;

 (a to_power (( log (a,b)) * ( log (b,c)))) = ((a to_power ( log (a,b))) to_power ( log (b,c))) by A1, Th33

 .= (b to_power ( log (b,c))) by A1, A2, A3, Def3

 .= c by A3, A4, A5, Def3;

 hence thesis by A1, A2, A5, Def3;

 end;

 theorem :: POWER:57

 a > 1 & b > 0 & c > b implies ( log (a,c)) > ( log (a,b))

 proof

 assume that

 A1: a > 1 and

 A2: b > 0 and

 A3: c > b and

 A4: ( log (a,c)) <= ( log (a,b));



 A5: (a to_power ( log (a,b))) = b by A1, A2, Def3;



 A6: (a to_power ( log (a,c))) = c by A1, A2, A3, Def3;

 now

 per cases by A4, XXREAL_0: 1;

 suppose ( log (a,c)) < ( log (a,b));

 hence contradiction by A1, A3, A5, A6, Th39;

 end;

 suppose ( log (a,c)) = ( log (a,b));

 hence contradiction by A1, A2, A3, A6, Def3;

 end;

 end;

 hence contradiction;

 end;

 theorem :: POWER:58

 a > 0 & a < 1 & b > 0 & c > b implies ( log (a,c)) < ( log (a,b))

 proof

 assume that

 A1: a > 0 & a < 1 and

 A2: b > 0 and

 A3: c > b and

 A4: ( log (a,c)) >= ( log (a,b));



 A5: (a to_power ( log (a,b))) = b by A1, A2, Def3;



 A6: (a to_power ( log (a,c))) = c by A1, A2, A3, Def3;

 now

 per cases by A4, XXREAL_0: 1;

 suppose ( log (a,c)) > ( log (a,b));

 hence contradiction by A1, A3, A5, A6, Th40;

 end;

 suppose ( log (a,c)) = ( log (a,b));

 hence contradiction by A1, A2, A3, A6, Def3;

 end;

 end;

 hence contradiction;

 end;

 theorem :: POWER:59

 for s be Real_Sequence st for n be Nat holds (s . n) = ((1 + (1 / (n + 1))) to_power (n + 1)) holds s is convergent

 proof

 let s be Real_Sequence such that

 A1: for n be Nat holds (s . n) = ((1 + (1 / (n + 1))) to_power (n + 1));

 now

 let n be Nat;



 A2: ((1 + (1 / (n + 1))) to_power (n + 1)) > 0 by Th34;



 A3: ((s . (n + 1)) / (s . n)) = (((1 + (1 / ((n + 1) + 1))) to_power ((n + 1) + 1)) / (s . n)) by A1

 .= ((((1 + (1 / ((n + 1) + 1))) to_power ((n + 1) + 1)) / ((1 + (1 / (n + 1))) to_power (n + 1))) * 1) by A1

 .= ((((1 + (1 / ((n + 1) + 1))) to_power ((n + 1) + 1)) / ((1 + (1 / (n + 1))) to_power (n + 1))) * ((1 + (1 / (n + 1))) / (1 + (1 / (n + 1))))) by XCMPLX_1: 60

 .= (((1 + (1 / (n + 1))) * ((1 + (1 / ((n + 1) + 1))) to_power ((n + 1) + 1))) / (((1 + (1 / (n + 1))) to_power (n + 1)) * (1 + (1 / (n + 1))))) by XCMPLX_1: 76

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

 .= (((1 + (1 / (n + 1))) * ((1 + (1 / ((n + 1) + 1))) to_power ((n + 1) + 1))) / ((1 + (1 / (n + 1))) to_power ((n + 1) + 1))) by Th27

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

 .= ((1 + (1 / (n + 1))) * (((1 + (1 / ((n + 1) + 1))) / (1 + (1 / (n + 1)))) to_power ((n + 1) + 1))) by Th31;



 A4: ((1 + (1 / ((n + 1) + 1))) / (1 + (1 / (n + 1)))) = ((((1 * ((n + 1) + 1)) + 1) / ((n + 1) + 1)) / (1 + (1 / (n + 1)))) by XCMPLX_1: 113

 .= (((((n + 1) + 1) + 1) / ((n + 1) + 1)) / (((1 * (n + 1)) + 1) / (n + 1))) by XCMPLX_1: 113

 .= ((((n + (1 + 1)) + 1) * (n + 1)) / ((n + 2) * (n + 2))) by XCMPLX_1: 84

 .= (((((((n * n) + (n * 2)) + (2 * n)) + 3) + 1) - 1) / ((n + 2) * (n + 2)))

 .= ((((n + 2) * (n + 2)) / ((n + 2) * (n + 2))) - (1 / ((n + 2) * (n + 2))))

 .= (1 - (1 / ((n + 2) * (n + 2)))) by XCMPLX_1: 6, XCMPLX_1: 60;

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

 then ((n + 2) * (n + 2)) > 1 by XREAL_1: 161;

 then (1 / ((n + 2) * (n + 2))) < 1 by XREAL_1: 212;

 then ( - (1 / ((n + 2) * (n + 2)))) > ( - 1) by XREAL_1: 24;

 then ((1 + ( - (1 / ((n + 2) * (n + 2))))) to_power ((n + 1) + 1)) >= (1 + (((n + 1) + 1) * ( - (1 / ((n + 2) * (n + 2)))))) by PREPOWER: 16;

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

 then ((1 - (1 / ((n + 2) * (n + 2)))) to_power ((n + 1) + 1)) >= (1 - ((((n + 2) / (n + 2)) * 1) / (n + 2))) by XCMPLX_1: 83;

 then ((1 - (1 / ((n + 2) * (n + 2)))) to_power ((n + 1) + 1)) >= (1 - ((1 * 1) / (n + 2))) by XCMPLX_1: 60;

 then ((s . (n + 1)) / (s . n)) >= ((1 + (1 / (n + 1))) * (1 - (1 / (n + 2)))) by A3, A4, XREAL_1: 64;

 then ((s . (n + 1)) / (s . n)) >= ((((1 * (n + 1)) + 1) / (n + 1)) * (1 - (1 / (n + 2)))) by XCMPLX_1: 113;

 then ((s . (n + 1)) / (s . n)) >= (((n + 2) / (n + 1)) * (((1 * (n + 2)) - 1) / (n + 2))) by XCMPLX_1: 127;

 then ((s . (n + 1)) / (s . n)) >= (((n + 1) * (n + 2)) / ((n + 1) * (n + 2))) by XCMPLX_1: 76;

 then

 A5: ((s . (n + 1)) / (s . n)) >= 1 by XCMPLX_1: 6, XCMPLX_1: 60;

 (s . n) > 0 by A1, A2;

 hence (s . (n + 1)) >= (s . n) by A5, XREAL_1: 191;

 end;

 then

 A6: s is non-decreasing by SEQM_3:def 8;

 now

 let n be Nat;



 A7: (2 * (n + 1)) > 0 by XREAL_1: 129;



 A8: (2 * (n + 1)) <> 0 ;



 A9: (s . (n + (n + 1))) = ((1 + (1 / ((2 * n) + (1 + 1)))) to_power (((2 * n) + 1) + 1)) by A1

 .= (((1 + (1 / (2 * (n + 1)))) to_power (n + 1)) to_power 2) by Th33;

 ((2 * (n + 1)) + 1) > ( 0 + 1) by A7, XREAL_1: 6;

 then (1 / ((2 * (n + 1)) + 1)) < 1 by XREAL_1: 212;

 then

 A10: ( - (1 / ((2 * (n + 1)) + 1))) > ( - 1) by XREAL_1: 24;

 then

 A11: (( - (1 / ((2 * (n + 1)) + 1))) + 1) > (( - 1) + 1) by XREAL_1: 6;



 A12: ((1 + (1 / (2 * (n + 1)))) to_power (n + 1)) = ((1 / (1 / (1 + (1 / (2 * (n + 1)))))) to_power (n + 1))

 .= ((1 / (1 + (1 / (2 * (n + 1))))) to_power ( - (n + 1))) by Th32

 .= ((1 / (((1 * (2 * (n + 1))) + 1) / (2 * (n + 1)))) to_power ( - (n + 1))) by A8, XCMPLX_1: 113

 .= (((((2 * (n + 1)) + 1) - 1) / ((2 * (n + 1)) + 1)) to_power ( - (n + 1))) by XCMPLX_1: 77

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

 .= ((1 - (1 / ((2 * (n + 1)) + 1))) to_power ( - (n + 1))) by XCMPLX_1: 60

 .= (1 / ((1 - (1 / ((2 * (n + 1)) + 1))) to_power (n + 1))) by A11, Th28;

 ((1 + ( - (1 / ((2 * (n + 1)) + 1)))) to_power (n + 1)) >= (1 + ((n + 1) * ( - (1 / ((2 * (n + 1)) + 1))))) by A10, PREPOWER: 16;

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

 then

 A13: ((1 - (1 / ((2 * (n + 1)) + 1))) to_power (n + 1)) >= (((1 * ((2 * (n + 1)) + 1)) - (n + 1)) / ((2 * (n + 1)) + 1)) by XCMPLX_1: 127;

 now

 assume (((2 * (n + 1)) - n) / ((2 * (n + 1)) + 1)) < (1 / 2);

 then (((2 * (n + 1)) - n) * 2) < (((2 * (n + 1)) + 1) * 1) by XREAL_1: 102;

 then ((2 * (n + 1)) + (( - n) + ((2 * (n + 1)) - n))) < ((2 * (n + 1)) + 1);

 hence contradiction by XREAL_1: 6;

 end;

 then ((1 - (1 / ((2 * (n + 1)) + 1))) to_power (n + 1)) >= (1 / 2) by A13, XXREAL_0: 2;

 then

 A14: ((1 + (1 / (2 * (n + 1)))) to_power (n + 1)) <= (1 / (1 / 2)) by A12, XREAL_1: 85;

 ((1 + (1 / (2 * (n + 1)))) to_power (n + 1)) > 0 by Th34;

 then (((1 + (1 / (2 * (n + 1)))) to_power (n + 1)) ^2 ) <= (2 * 2) by A14, XREAL_1: 66;

 then

 A15: (s . (n + (n + 1))) <= (2 * 2) by A9, Th46;

 (s . n) <= (s . (n + (n + 1))) by A6, SEQM_3: 5;

 then (s . n) <= (2 * 2) by A15, XXREAL_0: 2;

 hence (s . n) < ((2 * 2) + 1) by XXREAL_0: 2;

 end;

 then s is bounded_above by SEQ_2:def 3;

 hence thesis by A6;

 end;

 definition

 :: POWER:def4

 func number_e -> Real means for s be Real_Sequence st for n holds (s . n) = ((1 + (1 / (n + 1))) to_power (n + 1)) holds it = ( lim s);

 existence

 proof

 deffunc F( Nat) = ((1 + (1 / ($1 + 1))) to_power ($1 + 1));

 consider s1 be Real_Sequence such that

 A1: for n be Nat holds (s1 . n) = F(n) from SEQ_1:sch 1;

 take ( lim s1);

 let s be Real_Sequence such that

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

 now

 let n be Element of NAT ;



 thus (s1 . n) = ((1 + (1 / (n + 1))) to_power (n + 1)) by A1

 .= (s . n) by A2;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 uniqueness

 proof

 let a, b;

 assume that

 A3: for s be Real_Sequence st for n holds (s . n) = ((1 + (1 / (n + 1))) to_power (n + 1)) holds a = ( lim s) and

 A4: for s be Real_Sequence st for n holds (s . n) = ((1 + (1 / (n + 1))) to_power (n + 1)) holds b = ( lim s);

 deffunc F( Nat) = ((1 + (1 / ($1 + 1))) to_power ($1 + 1));

 consider s1 be Real_Sequence such that

 A5: for n be Nat holds (s1 . n) = F(n) from SEQ_1:sch 1;



 A6: for n holds (s1 . n) = F(n) by A5;

 ( lim s1) = a by A3, A6;

 hence thesis by A4, A6;

 end;

 end

 theorem :: POWER:60



 Th60: (2 to_power 2) = 4

 proof



 thus (2 to_power 2) = (2 ^2 ) by Th46

 .= 4;

 end;

 theorem :: POWER:61



 Th61: (2 to_power 3) = 8

 proof



 thus (2 to_power 3) = (2 to_power (2 + 1))

 .= ((2 to_power 2) * (2 to_power 1)) by Th27

 .= (4 * 2) by Th60

 .= 8;

 end;

 theorem :: POWER:62

 (2 to_power 4) = 16

 proof



 thus (2 to_power 4) = (2 to_power (2 + 2))

 .= ((2 to_power 2) * (2 to_power 2)) by Th27

 .= 16 by Th60;

 end;

 theorem :: POWER:63

 (2 to_power 5) = 32

 proof



 thus (2 to_power 5) = (2 to_power (3 + 2))

 .= ((2 to_power 3) * (2 to_power 2)) by Th27

 .= 32 by Th60, Th61;

 end;

 theorem :: POWER:64

 (2 to_power 6) = 64

 proof



 thus (2 to_power 6) = (2 to_power (3 + 3))

 .= ((2 to_power 3) * (2 to_power 3)) by Th27

 .= 64 by Th61;

 end;