:: POWER semantic presentation

begin


theorem Th1: :: POWER:1
for a being real number
for n being Element of NAT st n is even holds
(- a) |^ n = a |^ n
proof
let a be real number ; ::_thesis: for n being Element of NAT st n is even holds
(- a) |^ n = a |^ n
let n be Element of NAT ; ::_thesis: ( n is even implies (- a) |^ n = a |^ n )
given m being Element of NAT  such that A1: n = 2 * m ; :: according to ABIAN:def_2 ::_thesis: (- a) |^ n = a |^ n
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 ; ::_thesis: verum
end;

theorem Th2: :: POWER:2
for a being real number
for n being Element of NAT st n is odd holds
(- a) |^ n = - (a |^ n)
proof
let a be real number ; ::_thesis: for n being Element of NAT st n is odd holds
(- a) |^ n = - (a |^ n)
let n be Element of NAT ; ::_thesis: ( n is odd implies (- a) |^ n = - (a |^ n) )
assume  n is odd ; ::_thesis: (- a) |^ n = - (a |^ n)
then consider m being Element of NAT  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 ; ::_thesis: verum
end;

theorem Th3: :: POWER:3
for a being real number
for n being Element of NAT st ( a >= 0 or n is even ) holds
a |^ n >= 0
proof
let a be real number ; ::_thesis: for n being Element of NAT st ( a >= 0 or n is even ) holds
a |^ n >= 0
let n be Element of NAT ; ::_thesis: ( ( a >= 0 or n is even ) implies a |^ n >= 0 )
assume A1: ( a >= 0 or n is even ) ; ::_thesis: a |^ n >= 0
A2: now__::_thesis:_for_a_being_real_number_
for_n_being_Element_of_NAT_st_a_>=_0_holds_
a_|^_n_>=_0
let a be real number ; ::_thesis: for n being Element of NAT st a >= 0 holds
a |^ n >= 0
let n be Element of NAT ; ::_thesis: ( a >= 0 implies a |^ n >= 0 )
assume A3: a >= 0 ; ::_thesis: a |^ n >= 0
now__::_thesis:_a_|^_n_>=_0
percases ( a > 0 or a = 0 ) by A3;
suppose a > 0 ; ::_thesis: a |^ n >= 0
hence  a |^ n >= 0 by PREPOWER:6; ::_thesis: verum
end;
supposeA4: a = 0 ; ::_thesis: a |^ n >= 0
now__::_thesis:_a_|^_n_>=_0
percases ( n = 0 or ex m being Nat st n = m + 1 ) by NAT_1:6;
supposeA5: n = 0 ; ::_thesis: a |^ n >= 0
a |^ n = (a GeoSeq) . n by PREPOWER:def_1
.= 1 by A5, PREPOWER:3 ;
hence  a |^ n >= 0 ; ::_thesis: verum
end;
suppose ex m being Nat st n = m + 1 ; ::_thesis: a |^ n >= 0
then consider m being Nat such that
A6: n = m + 1 ;
a |^ n = (a |^ m) * a by A6, NEWTON:6
.= 0 by A4 ;
hence  a |^ n >= 0 ; ::_thesis: verum
end;
end;
end;
hence  a |^ n >= 0 ; ::_thesis: verum
end;
end;
end;
hence  a |^ n >= 0 ; ::_thesis: verum
end;
now__::_thesis:_(_n_is_even_implies_a_|^_n_>=_0_)
assume A7: n is even ; ::_thesis: a |^ n >= 0
now__::_thesis:_a_|^_n_>=_0
percases ( a >= 0 or a < 0 ) ;
suppose a >= 0 ; ::_thesis: a |^ n >= 0
hence  a |^ n >= 0 by A2; ::_thesis: verum
end;
suppose a < 0 ; ::_thesis: a |^ n >= 0
then  (- a) |^ n >= 0 by A2;
hence  a |^ n >= 0 by A7, Th1; ::_thesis: verum
end;
end;
end;
hence  a |^ n >= 0 ; ::_thesis: verum
end;
hence  a |^ n >= 0 by A1, A2; ::_thesis: verum
end;

definition
let n be Nat;
let a be real number ;
funcn -root a ->  real number  equals :Def1: :: POWER:def 1
n -Root a if ( a >= 0 & n >= 1 )
- (n -Root (- a)) if ( a < 0 & n is odd )
;
consistency
 for b1 being real number st a >= 0 & n >= 1 & a < 0 & n is odd holds
( b1 = n -Root a iff b1 = - (n -Root (- a)) ) ;
coherence
 ( ( a >= 0 & n >= 1 implies n -Root a is real number ) & ( a < 0 & n is odd implies - (n -Root (- a)) is real number ) ) ;
end;

:: deftheorem Def1 defines -root POWER:def_1_:_
 for n being Nat
for a being real number holds
( ( a >= 0 & n >= 1 implies n -root a = n -Root a ) & ( a < 0 & n is odd implies n -root a = - (n -Root (- a)) ) );

definition
let n be Nat;
let a be Real;
:: original: -root
redefine funcn -root a ->  Real;
coherence
 n -root a is Real by XREAL_0:def_1;
end;

theorem :: POWER:4
for a being real number
for n being Nat st ( ( n >= 1 & a >= 0 ) or n is odd ) holds
( (n -root a) |^ n = a & n -root (a |^ n) = a )
proof
let a be real number ; ::_thesis: for n being Nat st ( ( n >= 1 & a >= 0 ) or n is odd ) holds
( (n -root a) |^ n = a & n -root (a |^ n) = a )
let n be Nat; ::_thesis: ( ( ( n >= 1 & a >= 0 ) or n is odd ) implies ( (n -root a) |^ n = a & n -root (a |^ n) = a ) )
assume A1: ( ( n >= 1 & a >= 0 ) or n is odd ) ; ::_thesis: ( (n -root a) |^ n = a & n -root (a |^ n) = a )
A2: now__::_thesis:_(_n_>=_1_&_a_>=_0_implies_(_(n_-root_a)_|^_n_=_a_&_n_-root_(a_|^_n)_=_a_)_)
assume that
A3: n >= 1 and
A4: a >= 0 ; ::_thesis: ( (n -root a) |^ n = a & n -root (a |^ n) = a )
A5: n -root a = n -Root a by A3, A4, Def1;
now__::_thesis:_a_|^_n_>=_0
percases ( a > 0 or a = 0 ) by A4;
suppose a > 0 ; ::_thesis: a |^ n >= 0
hence  a |^ n >= 0 by PREPOWER:6; ::_thesis: verum
end;
suppose a = 0 ; ::_thesis: a |^ n >= 0
hence  a |^ n >= 0 ; ::_thesis: verum
end;
end;
end;
then  n -root (a |^ n) = n -Root (a |^ n) by A3, Def1;
hence  ( (n -root a) |^ n = a & n -root (a |^ n) = a ) by A3, A4, A5, PREPOWER:19; ::_thesis: verum
end;
now__::_thesis:_(_n_is_odd_implies_(_(n_-root_a)_|^_n_=_a_&_n_-root_(a_|^_n)_=_a_)_)
assume A6: n is odd ; ::_thesis: ( (n -root a) |^ n = a & n -root (a |^ n) = a )
then A7: ex m being Element of NAT st n = (2 * m) + 1 by ABIAN:9;
A8: n >= 1 by A6, ABIAN:12;
now__::_thesis:_(_(n_-root_a)_|^_n_=_a_&_n_-root_(a_|^_n)_=_a_)
percases ( a >= 0 or a < 0 ) ;
suppose a >= 0 ; ::_thesis: ( (n -root a) |^ n = a & n -root (a |^ n) = a )
hence  ( (n -root a) |^ n = a & n -root (a |^ n) = a ) by A2, A8; ::_thesis: verum
end;
supposeA9: a < 0 ; ::_thesis: ( (n -root a) |^ n = a & n -root (a |^ n) = a )
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 ; ::_thesis: n -root (a |^ n) = 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 ;
::_thesis: verum
end;
end;
end;
hence  ( (n -root a) |^ n = a & n -root (a |^ n) = a ) ; ::_thesis: verum
end;
hence  ( (n -root a) |^ n = a & n -root (a |^ n) = a ) by A1, A2; ::_thesis: verum
end;

theorem Th5: :: POWER:5
for n being Nat st n >= 1 holds
n -root 0 = 0
proof
let n be Nat; ::_thesis: ( n >= 1 implies n -root 0 = 0 )
assume A1: n >= 1 ; ::_thesis: n -root 0 = 0
hence n -root 0 = n -Root 0 by Def1
.= 0 by A1, PREPOWER:def_2 ;
::_thesis: verum
end;

theorem :: POWER:6
for n being Element of NAT st n >= 1 holds
n -root 1 = 1
proof
let n be Element of NAT ; ::_thesis: ( n >= 1 implies n -root 1 = 1 )
assume A1: n >= 1 ; ::_thesis: n -root 1 = 1
hence n -root 1 = n -Root 1 by Def1
.= 1 by A1, PREPOWER:20 ;
::_thesis: verum
end;

theorem Th7: :: POWER:7
for a being real number
for n being Element of NAT st a >= 0 & n >= 1 holds
n -root a >= 0
proof
let a be real number ; ::_thesis: for n being Element of NAT st a >= 0 & n >= 1 holds
n -root a >= 0
let n be Element of NAT ; ::_thesis: ( a >= 0 & n >= 1 implies n -root a >= 0 )
assume that
A1: a >= 0 and
A2: n >= 1 ; ::_thesis: n -root a >= 0
now__::_thesis:_n_-root_a_>=_0
percases ( a > 0 or a = 0 ) by A1;
supposeA3: a > 0 ; ::_thesis: n -root a >= 0
 n -root a = n -Root a by A1, A2, Def1;
hence  n -root a >= 0 by A2, A3, PREPOWER:def_2; ::_thesis: verum
end;
supposeA4: a = 0 ; ::_thesis: n -root a >= 0
n -root a = n -Root a by A1, A2, Def1
.= 0 by A2, A4, PREPOWER:def_2 ;
hence  n -root a >= 0 ; ::_thesis: verum
end;
end;
end;
hence  n -root a >= 0 ; ::_thesis: verum
end;

theorem :: POWER:8
for n being Element of NAT st n is odd holds
n -root (- 1) = - 1
proof
let n be Element of NAT ; ::_thesis: ( n is odd implies n -root (- 1) = - 1 )
assume A1: n is odd ; ::_thesis: n -root (- 1) = - 1
then A2: n >= 1 by ABIAN:12;
thus n -root (- 1) = - (n -Root (- (- 1))) by A1, Def1
.= - 1 by A2, PREPOWER:20 ; ::_thesis: verum
end;

theorem :: POWER:9
for a being real number holds 1 -root a = a
proof
let a be real number ; ::_thesis: 1 -root a = a
now__::_thesis:_1_-root_a_=_a
percases ( a >= 0 or a < 0 ) ;
supposeA1: a >= 0 ; ::_thesis: 1 -root a = a
hence 1 -root a = 1 -Root a by Def1
.= a by A1, PREPOWER:21 ;
::_thesis: verum
end;
supposeA2: a < 0 ; ::_thesis: 1 -root a = a
 1 = (2 * 0) + 1 ;
hence 1 -root a = - (1 -Root (- a)) by A2, Def1
.= - (- a) by A2, PREPOWER:21
.= a ;
::_thesis: verum
end;
end;
end;
hence  1 -root a = a ; ::_thesis: verum
end;

theorem Th10: :: POWER:10
for a being real number
for n being Element of NAT st n is odd holds
n -root a = - (n -root (- a))
proof
let a be real number ; ::_thesis: for n being Element of NAT st n is odd holds
n -root a = - (n -root (- a))
let n be Element of NAT ; ::_thesis: ( n is odd implies n -root a = - (n -root (- a)) )
assume A1: n is odd ; ::_thesis: n -root a = - (n -root (- a))
then A2: ex m being Element of NAT st n = (2 * m) + 1 by ABIAN:9;
A3: n >= 1 by A1, ABIAN:12;
now__::_thesis:_n_-root_a_=_-_(n_-root_(-_a))
percases ( a < 0 or a = 0 or a > 0 ) ;
supposeA4: a < 0 ; ::_thesis: n -root a = - (n -root (- a))
hence n -root a = - (n -Root (- a)) by A2, Def1
.= - (n -root (- a)) by A3, A4, Def1 ;
::_thesis: verum
end;
supposeA5: a = 0 ; ::_thesis: n -root a = - (n -root (- a))
hence n -root a = 0 by A3, Th5
.= - (n -root (- a)) by A3, A5, Th5 ;
::_thesis: verum
end;
supposeA6: a > 0 ; ::_thesis: - (n -root (- a)) = n -root a
then  - a < - 0 by XREAL_1:24;
hence  - (n -root (- a)) = - (- (n -Root (- (- a)))) by A2, Def1
.= n -root a by A3, A6, Def1 ;
::_thesis: verum
end;
end;
end;
hence  n -root a = - (n -root (- a)) ; ::_thesis: verum
end;

theorem Th11: :: POWER:11
for a, b being real number
for n being Element of NAT st ( ( n >= 1 & a >= 0 & b >= 0 ) or n is odd ) holds
n -root (a * b) = (n -root a) * (n -root b)
proof
let a, b be real number ; ::_thesis: for n being Element of NAT st ( ( n >= 1 & a >= 0 & b >= 0 ) or n is odd ) holds
n -root (a * b) = (n -root a) * (n -root b)
let n be Element of NAT ; ::_thesis: ( ( ( n >= 1 & a >= 0 & b >= 0 ) or n is odd ) implies n -root (a * b) = (n -root a) * (n -root b) )
assume A1: ( ( n >= 1 & a >= 0 & b >= 0 ) or n is odd ) ; ::_thesis: n -root (a * b) = (n -root a) * (n -root b)
A2: now__::_thesis:_for_a,_b_being_real_number_
for_n_being_Element_of_NAT_st_n_>=_1_&_a_>=_0_&_b_>=_0_holds_
n_-root_(a_*_b)_=_(n_-root_a)_*_(n_-root_b)
let a, b be real number ; ::_thesis: for n being Element of NAT st n >= 1 & a >= 0 & b >= 0 holds
n -root (a * b) = (n -root a) * (n -root b)
let n be Element of NAT ; ::_thesis: ( n >= 1 & a >= 0 & b >= 0 implies n -root (a * b) = (n -root a) * (n -root b) )
assume that
A3: n >= 1 and
A4: a >= 0 and
A5: b >= 0 ; ::_thesis: n -root (a * b) = (n -root a) * (n -root b)
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 ; ::_thesis: verum
end;
now__::_thesis:_(_n_is_odd_implies_n_-root_(a_*_b)_=_(n_-root_a)_*_(n_-root_b)_)
assume A6: n is odd ; ::_thesis: n -root (a * b) = (n -root a) * (n -root b)
then A7: n >= 1 by ABIAN:12;
now__::_thesis:_n_-root_(a_*_b)_=_(n_-root_a)_*_(n_-root_b)
percases ( ( a >= 0 & b >= 0 ) or ( a < 0 & b < 0 ) or ( a >= 0 & b < 0 ) or ( a < 0 & b >= 0 ) ) ;
suppose ( a >= 0 & b >= 0 ) ; ::_thesis: n -root (a * b) = (n -root a) * (n -root b)
hence  n -root (a * b) = (n -root a) * (n -root b) by A2, A7; ::_thesis: verum
end;
supposeA8: ( a < 0 & b < 0 ) ; ::_thesis: n -root (a * b) = (n -root a) * (n -root b)
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) ;
::_thesis: verum
end;
supposeA9: ( a >= 0 & b < 0 ) ; ::_thesis: n -root (a * b) = (n -root a) * (n -root b)
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 ; ::_thesis: verum
end;
supposeA10: ( a < 0 & b >= 0 ) ; ::_thesis: n -root (a * b) = (n -root a) * (n -root b)
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 ; ::_thesis: verum
end;
end;
end;
hence  n -root (a * b) = (n -root a) * (n -root b) ; ::_thesis: verum
end;
hence  n -root (a * b) = (n -root a) * (n -root b) by A1, A2; ::_thesis: verum
end;

theorem Th12: :: POWER:12
for a being real number
for n being Element of NAT st ( ( a > 0 & n >= 1 ) or ( a <> 0 & n is odd ) ) holds
n -root (1 / a) = 1 / (n -root a)
proof
let a be real number ; ::_thesis: for n being Element of NAT st ( ( a > 0 & n >= 1 ) or ( a <> 0 & n is odd ) ) holds
n -root (1 / a) = 1 / (n -root a)
let n be Element of NAT ; ::_thesis: ( ( ( a > 0 & n >= 1 ) or ( a <> 0 & n is odd ) ) implies n -root (1 / a) = 1 / (n -root a) )
assume A1: ( ( a > 0 & n >= 1 ) or ( a <> 0 & n is odd ) ) ; ::_thesis: n -root (1 / a) = 1 / (n -root a)
A2: now__::_thesis:_for_a_being_real_number_
for_n_being_Element_of_NAT_st_a_>_0_&_n_>=_1_holds_
n_-root_(1_/_a)_=_1_/_(n_-root_a)
let a be real number ; ::_thesis: for n being Element of NAT st a > 0 & n >= 1 holds
n -root (1 / a) = 1 / (n -root a)
let n be Element of NAT ; ::_thesis: ( a > 0 & n >= 1 implies n -root (1 / a) = 1 / (n -root a) )
assume A3: ( a > 0 & n >= 1 ) ; ::_thesis: n -root (1 / a) = 1 / (n -root a)
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 ;
::_thesis: verum
end;
now__::_thesis:_(_a_<>_0_&_n_is_odd_implies_n_-root_(1_/_a)_=_1_/_(n_-root_a)_)
assume that
A4: a <> 0 and
A5: n is odd ; ::_thesis: n -root (1 / a) = 1 / (n -root a)
A6: n >= 1 by A5, ABIAN:12;
now__::_thesis:_n_-root_(1_/_a)_=_1_/_(n_-root_a)
percases ( a > 0 or a < 0 ) by A4;
suppose a > 0 ; ::_thesis: n -root (1 / a) = 1 / (n -root a)
hence  n -root (1 / a) = 1 / (n -root a) by A2, A6; ::_thesis: verum
end;
suppose a < 0 ; ::_thesis: 1 / (n -root a) = n -root (1 / a)
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 ; ::_thesis: verum
end;
end;
end;
hence  n -root (1 / a) = 1 / (n -root a) ; ::_thesis: verum
end;
hence  n -root (1 / a) = 1 / (n -root a) by A1, A2; ::_thesis: verum
end;

theorem :: POWER:13
for a, b being real number
for n being Element of NAT st ( ( a >= 0 & b > 0 & n >= 1 ) or ( b <> 0 & n is odd ) ) holds
n -root (a / b) = (n -root a) / (n -root b)
proof
let a, b be real number ; ::_thesis: for n being Element of NAT st ( ( a >= 0 & b > 0 & n >= 1 ) or ( b <> 0 & n is odd ) ) holds
n -root (a / b) = (n -root a) / (n -root b)
let n be Element of NAT ; ::_thesis: ( ( ( a >= 0 & b > 0 & n >= 1 ) or ( b <> 0 & n is odd ) ) implies n -root (a / b) = (n -root a) / (n -root b) )
assume A1: ( ( a >= 0 & b > 0 & n >= 1 ) or ( b <> 0 & n is odd ) ) ; ::_thesis: n -root (a / b) = (n -root a) / (n -root b)
now__::_thesis:_n_-root_(a_/_b)_=_(n_-root_a)_/_(n_-root_b)
percases ( ( a >= 0 & b > 0 & n >= 1 ) or ( b <> 0 & n is odd ) ) by A1;
supposeA2: ( a >= 0 & b > 0 & n >= 1 ) ; ::_thesis: n -root (a / b) = (n -root a) / (n -root b)
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 ;
::_thesis: verum
end;
supposeA3: ( b <> 0 & n is odd ) ; ::_thesis: n -root (a / b) = (n -root a) / (n -root b)
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) ; ::_thesis: verum
end;
end;
end;
hence  n -root (a / b) = (n -root a) / (n -root b) ; ::_thesis: verum
end;

theorem :: POWER:14
for a being real number
for n, m being Element of NAT st ( ( a >= 0 & n >= 1 & m >= 1 ) or ( n is odd & m is odd ) ) holds
n -root (m -root a) = (n * m) -root a
proof
let a be real number ; ::_thesis: for n, m being Element of NAT st ( ( a >= 0 & n >= 1 & m >= 1 ) or ( n is odd & m is odd ) ) holds
n -root (m -root a) = (n * m) -root a
let n, m be Element of NAT ; ::_thesis: ( ( ( a >= 0 & n >= 1 & m >= 1 ) or ( n is odd & m is odd ) ) implies n -root (m -root a) = (n * m) -root a )
assume A1: ( ( a >= 0 & n >= 1 & m >= 1 ) or ( n is odd & m is odd ) ) ; ::_thesis: n -root (m -root a) = (n * m) -root a
A2: now__::_thesis:_for_a_being_real_number_
for_n,_m_being_Element_of_NAT_st_a_>=_0_&_n_>=_1_&_m_>=_1_holds_
n_-root_(m_-root_a)_=_(n_*_m)_-root_a
let a be real number ; ::_thesis: for n, m being Element of NAT st a >= 0 & n >= 1 & m >= 1 holds
n -root (m -root a) = (n * m) -root a
let n, m be Element of NAT ; ::_thesis: ( a >= 0 & n >= 1 & m >= 1 implies n -root (m -root a) = (n * m) -root a )
assume that
A3: a >= 0 and
A4: n >= 1 and
A5: m >= 1 ; ::_thesis: n -root (m -root a) = (n * m) -root a
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 ; ::_thesis: verum
end;
now__::_thesis:_(_n_is_odd_&_m_is_odd_implies_n_-root_(m_-root_a)_=_(n_*_m)_-root_a_)
assume  n is odd ; ::_thesis: ( m is odd implies n -root (m -root a) = (n * m) -root a )
then consider m1 being Element of NAT  such that
A8: n = (2 * m1) + 1 by ABIAN:9;
assume  m is odd ; ::_thesis: n -root (m -root a) = (n * m) -root a
then consider m2 being Element of NAT  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__::_thesis:_n_-root_(m_-root_a)_=_(n_*_m)_-root_a
percases ( a >= 0 or a < 0 ) ;
suppose a >= 0 ; ::_thesis: n -root (m -root a) = (n * m) -root a
hence  n -root (m -root a) = (n * m) -root a by A2, A10, A11; ::_thesis: verum
end;
supposeA14: a < 0 ; ::_thesis: n -root (m -root a) = (n * m) -root a
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 ; ::_thesis: verum
end;
end;
end;
hence  n -root (m -root a) = (n * m) -root a ; ::_thesis: verum
end;
hence  n -root (m -root a) = (n * m) -root a by A1, A2; ::_thesis: verum
end;

theorem :: POWER:15
for a being real number
for n, m being Element of NAT st ( ( a >= 0 & n >= 1 & m >= 1 ) or ( n is odd & m is odd ) ) holds
(n -root a) * (m -root a) = (n * m) -root (a |^ (n + m))
proof
let a be real number ; ::_thesis: for n, m being Element of NAT st ( ( a >= 0 & n >= 1 & m >= 1 ) or ( n is odd & m is odd ) ) holds
(n -root a) * (m -root a) = (n * m) -root (a |^ (n + m))
let n, m be Element of NAT ; ::_thesis: ( ( ( 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)) )
assume A1: ( ( a >= 0 & n >= 1 & m >= 1 ) or ( n is odd & m is odd ) ) ; ::_thesis: (n -root a) * (m -root a) = (n * m) -root (a |^ (n + m))
A2: now__::_thesis:_for_a_being_real_number_
for_n,_m_being_Element_of_NAT_st_a_>=_0_&_n_>=_1_&_m_>=_1_holds_
(n_-root_a)_*_(m_-root_a)_=_(n_*_m)_-root_(a_|^_(n_+_m))
let a be real number ; ::_thesis: for n, m being Element of NAT st a >= 0 & n >= 1 & m >= 1 holds
(n -root a) * (m -root a) = (n * m) -root (a |^ (n + m))
let n, m be Element of NAT ; ::_thesis: ( a >= 0 & n >= 1 & m >= 1 implies (n -root a) * (m -root a) = (n * m) -root (a |^ (n + m)) )
assume that
A3: a >= 0 and
A4: n >= 1 and
A5: m >= 1 ; ::_thesis: (n -root a) * (m -root a) = (n * m) -root (a |^ (n + m))
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 ; ::_thesis: verum
end;
now__::_thesis:_(_n_is_odd_&_m_is_odd_implies_(n_-root_a)_*_(m_-root_a)_=_(n_*_m)_-root_(a_|^_(n_+_m))_)
assume  n is odd ; ::_thesis: ( m is odd implies (n -root a) * (m -root a) = (n * m) -root (a |^ (n + m)) )
then consider m1 being Element of NAT  such that
A7: n = (2 * m1) + 1 by ABIAN:9;
assume  m is odd ; ::_thesis: (n -root a) * (m -root a) = (n * m) -root (a |^ (n + m))
then consider m2 being Element of NAT  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__::_thesis:_(n_-root_a)_*_(m_-root_a)_=_(n_*_m)_-root_(a_|^_(n_+_m))
percases ( a >= 0 or a < 0 ) ;
suppose a >= 0 ; ::_thesis: (n -root a) * (m -root a) = (n * m) -root (a |^ (n + m))
hence  (n -root a) * (m -root a) = (n * m) -root (a |^ (n + m)) by A2, A9; ::_thesis: verum
end;
supposeA12: a < 0 ; ::_thesis: (n -root a) * (m -root a) = (n * m) -root (a |^ (n + m))
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 ; ::_thesis: verum
end;
end;
end;
hence  (n -root a) * (m -root a) = (n * m) -root (a |^ (n + m)) ; ::_thesis: verum
end;
hence  (n -root a) * (m -root a) = (n * m) -root (a |^ (n + m)) by A1, A2; ::_thesis: verum
end;

theorem :: POWER:16
for a, b being real number
for n being Element of NAT st a <= b & ( ( 0 <= a & n >= 1 ) or n is odd ) holds
n -root a <= n -root b
proof
let a, b be real number ; ::_thesis: for n being Element of NAT st a <= b & ( ( 0 <= a & n >= 1 ) or n is odd ) holds
n -root a <= n -root b
let n be Element of NAT ; ::_thesis: ( a <= b & ( ( 0 <= a & n >= 1 ) or n is odd ) implies n -root a <= n -root b )
assume that
A1: a <= b and
A2: ( ( 0 <= a & n >= 1 ) or n is odd ) ; ::_thesis: n -root a <= n -root b
A3: now__::_thesis:_for_a,_b_being_real_number_
for_n_being_Element_of_NAT_st_0_<=_a_&_n_>=_1_&_a_<=_b_holds_
n_-root_a_<=_n_-root_b
let a, b be real number ; ::_thesis: for n being Element of NAT st 0 <= a & n >= 1 & a <= b holds
n -root a <= n -root b
let n be Element of NAT ; ::_thesis: ( 0 <= a & n >= 1 & a <= b implies n -root a <= n -root b )
assume that
A4: ( 0 <= a & n >= 1 ) and
A5: a <= b ; ::_thesis: n -root a <= n -root 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; ::_thesis: verum
end;
now__::_thesis:_(_n_is_odd_implies_n_-root_a_<=_n_-root_b_)
assume A6: n is odd ; ::_thesis: n -root a <= n -root b
then A7: n >= 1 by ABIAN:12;
now__::_thesis:_n_-root_a_<=_n_-root_b
percases ( a >= 0 or a < 0 ) ;
suppose a >= 0 ; ::_thesis: n -root a <= n -root b
hence  n -root a <= n -root b by A1, A3, A7; ::_thesis: verum
end;
supposeA8: a < 0 ; ::_thesis: n -root a <= n -root b
now__::_thesis:_n_-root_a_<=_n_-root_b
percases ( b >= 0 or b < 0 ) ;
suppose b >= 0 ; ::_thesis: n -root a <= n -root b
then A9: n -root b >= 0 by A7, Th7;
 n -root (- a) >= 0 by A7, A8, Th7;
then  - (n -root (- a)) <= - 0 ;
hence  n -root a <= n -root b by A6, A9, Th10; ::_thesis: verum
end;
supposeA10: b < 0 ; ::_thesis: n -root a <= n -root b
 - 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  n -root a <= n -root b by A6, Th10; ::_thesis: verum
end;
end;
end;
hence  n -root a <= n -root b ; ::_thesis: verum
end;
end;
end;
hence  n -root a <= n -root b ; ::_thesis: verum
end;
hence  n -root a <= n -root b by A1, A2, A3; ::_thesis: verum
end;

theorem :: POWER:17
for a, b being real number
for n being Element of NAT st a < b & ( ( a >= 0 & n >= 1 ) or n is odd ) holds
n -root a < n -root b
proof
let a, b be real number ; ::_thesis: for n being Element of NAT st a < b & ( ( a >= 0 & n >= 1 ) or n is odd ) holds
n -root a < n -root b
let n be Element of NAT ; ::_thesis: ( a < b & ( ( a >= 0 & n >= 1 ) or n is odd ) implies n -root a < n -root b )
assume that
A1: a < b and
A2: ( ( 0 <= a & n >= 1 ) or n is odd ) ; ::_thesis: n -root a < n -root b
A3: now__::_thesis:_for_a,_b_being_real_number_
for_n_being_Element_of_NAT_st_0_<=_a_&_n_>=_1_&_a_<_b_holds_
n_-root_a_<_n_-root_b
let a, b be real number ; ::_thesis: for n being Element of NAT st 0 <= a & n >= 1 & a < b holds
n -root a < n -root b
let n be Element of NAT ; ::_thesis: ( 0 <= a & n >= 1 & a < b implies n -root a < n -root b )
assume that
A4: ( 0 <= a & n >= 1 ) and
A5: a < b ; ::_thesis: n -root a < n -root 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; ::_thesis: verum
end;
now__::_thesis:_(_n_is_odd_implies_n_-root_a_<_n_-root_b_)
assume A6: n is odd ; ::_thesis: n -root a < n -root b
then A7: n >= 1 by ABIAN:12;
now__::_thesis:_n_-root_a_<_n_-root_b
percases ( a >= 0 or a < 0 ) ;
suppose a >= 0 ; ::_thesis: n -root a < n -root b
hence  n -root a < n -root b by A1, A3, A7; ::_thesis: verum
end;
supposeA8: a < 0 ; ::_thesis: n -root a < n -root b
then A9: - a > 0 by XREAL_1:58;
now__::_thesis:_n_-root_a_<_n_-root_b
percases ( b >= 0 or b < 0 ) ;
suppose b >= 0 ; ::_thesis: n -root a < n -root b
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  n -root a < n -root b by A6, A8, A10, Def1; ::_thesis: verum
end;
supposeA11: b < 0 ; ::_thesis: n -root a < n -root b
 - 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  n -root a < n -root b by A6, Th10; ::_thesis: verum
end;
end;
end;
hence  n -root a < n -root b ; ::_thesis: verum
end;
end;
end;
hence  n -root a < n -root b ; ::_thesis: verum
end;
hence  n -root a < n -root b by A1, A2, A3; ::_thesis: verum
end;

theorem Th18: :: POWER:18
for a being real number
for n being Element of NAT st a >= 1 & n >= 1 holds
( n -root a >= 1 & a >= n -root a )
proof
let a be real number ; ::_thesis: for n being Element of NAT st a >= 1 & n >= 1 holds
( n -root a >= 1 & a >= n -root a )
let n be Element of NAT ; ::_thesis: ( a >= 1 & n >= 1 implies ( n -root a >= 1 & a >= n -root a ) )
assume that
A1: a >= 1 and
A2: n >= 1 ; ::_thesis: ( n -root a >= 1 & a >= n -root a )
 ( n -Root a >= 1 & a >= n -Root a ) by A1, A2, PREPOWER:29;
hence  ( n -root a >= 1 & a >= n -root a ) by A2, Def1; ::_thesis: verum
end;

theorem :: POWER:19
for a being real number
for n being Element of NAT st a <= - 1 & n is odd holds
( n -root a <= - 1 & a <= n -root a )
proof
let a be real number ; ::_thesis: for n being Element of NAT st a <= - 1 & n is odd holds
( n -root a <= - 1 & a <= n -root a )
let n be Element of NAT ; ::_thesis: ( a <= - 1 & n is odd implies ( n -root a <= - 1 & a <= n -root a ) )
assume that
A1: a <= - 1 and
A2: n is odd ; ::_thesis: ( n -root a <= - 1 & a <= n -root a )
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  ( n -root a <= - 1 & a <= n -root a ) by A2, A6, Th10; ::_thesis: verum
end;

theorem Th20: :: POWER:20
for a being real number
for n being Element of NAT st a >= 0 & a < 1 & n >= 1 holds
( a <= n -root a & n -root a < 1 )
proof
let a be real number ; ::_thesis: for n being Element of NAT st a >= 0 & a < 1 & n >= 1 holds
( a <= n -root a & n -root a < 1 )
let n be Element of NAT ; ::_thesis: ( a >= 0 & a < 1 & n >= 1 implies ( a <= n -root a & n -root a < 1 ) )
assume that
A1: a >= 0 and
A2: a < 1 and
A3: n >= 1 ; ::_thesis: ( a <= n -root a & n -root a < 1 )
 ( a <= n -Root a & n -Root a < 1 ) by A1, A2, A3, PREPOWER:30;
hence  ( a <= n -root a & n -root a < 1 ) by A1, A3, Def1; ::_thesis: verum
end;

theorem :: POWER:21
for a being real number
for n being Element of NAT st a > - 1 & a <= 0 & n is odd holds
( a >= n -root a & n -root a > - 1 )
proof
let a be real number ; ::_thesis: for n being Element of NAT st a > - 1 & a <= 0 & n is odd holds
( a >= n -root a & n -root a > - 1 )
let n be Element of NAT ; ::_thesis: ( a > - 1 & a <= 0 & n is odd implies ( a >= n -root a & n -root a > - 1 ) )
assume that
A1: a > - 1 and
A2: a <= 0 ; ::_thesis: ( not n is odd or ( a >= n -root a & n -root a > - 1 ) )
assume  n is odd ; ::_thesis: ( a >= n -root a & n -root a > - 1 )
then A3: ex m being Element of NAT 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  ( a >= n -root a & n -root a > - 1 ) by A3, A7, Th10; ::_thesis: verum
end;

theorem Th22: :: POWER:22
for a being real number
for n being Element of NAT st a > 0 & n >= 1 holds
(n -root a) - 1 <= (a - 1) / n
proof
let a be real number ; ::_thesis: for n being Element of NAT st a > 0 & n >= 1 holds
(n -root a) - 1 <= (a - 1) / n
let n be Element of NAT ; ::_thesis: ( a > 0 & n >= 1 implies (n -root a) - 1 <= (a - 1) / n )
assume A1: ( a > 0 & n >= 1 ) ; ::_thesis: (n -root a) - 1 <= (a - 1) / n
then  (n -Root a) - 1 <= (a - 1) / n by PREPOWER:31;
hence  (n -root a) - 1 <= (a - 1) / n by A1, Def1; ::_thesis: verum
end;

theorem Th23: :: POWER:23
for s being Real_Sequence
for a being real number st a > 0 & ( for n being Element of NAT st n >= 1 holds
s . n = n -root a ) holds
( s is convergent & lim s = 1 )
proof
let s be Real_Sequence; ::_thesis: for a being real number st a > 0 & ( for n being Element of NAT st n >= 1 holds
s . n = n -root a ) holds
( s is convergent & lim s = 1 )
let a be real number ; ::_thesis: ( a > 0 & ( for n being Element of NAT st n >= 1 holds
s . n = n -root a ) implies ( s is convergent & lim s = 1 ) )
assume that
A1: a > 0 and
A2: for n being Element of NAT st n >= 1 holds
s . n = n -root a ; ::_thesis: ( s is convergent & lim s = 1 )
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_1_holds_
s_._n_=_n_-Root_a
let n be Element of NAT ; ::_thesis: ( n >= 1 implies s . n = n -Root a )
assume A3: n >= 1 ; ::_thesis: s . n = n -Root a
hence s . n = n -root a by A2
.= n -Root a by A1, A3, Def1 ;
::_thesis: verum
end;
hence  ( s is convergent & lim s = 1 ) by A1, PREPOWER:33; ::_thesis: verum
end;

definition
let a, b be real number ;
funca to_power b ->  real number  means :Def2: :: POWER:def 2
it = a #R b if a > 0
it = 0  if ( a = 0 & b > 0 )
ex k being Integer st
( k = b & it = a #Z k ) if b is Integer
;
consistency
 for b1 being real number holds
( ( a > 0 & a = 0 & b > 0 implies ( b1 = a #R b iff b1 = 0 ) ) & ( a > 0 & b is Integer implies ( b1 = a #R b iff ex k being Integer st
( k = b & b1 = a #Z k ) ) ) & ( a = 0 & b > 0 & b is Integer implies ( b1 = 0 iff ex k being Integer st
( k = b & b1 = a #Z k ) ) ) )
proof
let IT be real number ; ::_thesis: ( ( a > 0 & a = 0 & b > 0 implies ( IT = a #R b iff IT = 0 ) ) & ( a > 0 & b is Integer implies ( IT = a #R b iff ex k being Integer st
( k = b & IT = a #Z k ) ) ) & ( a = 0 & b > 0 & b is Integer implies ( IT = 0 iff ex k being Integer st
( k = b & IT = a #Z k ) ) ) )
thus  ( a > 0 & a = 0 & b > 0 implies ( IT = a #R b iff IT = 0 ) ) ; ::_thesis: ( ( a > 0 & b is Integer implies ( IT = a #R b iff ex k being Integer st
( k = b & IT = a #Z k ) ) ) & ( a = 0 & b > 0 & b is Integer implies ( IT = 0 iff ex k being Integer st
( k = b & IT = a #Z k ) ) ) )
thus  ( a > 0 & b is Integer implies ( IT = a #R b iff ex k being Integer st
( k = b & IT = a #Z k ) ) ) ::_thesis: ( a = 0 & b > 0 & b is Integer implies ( IT = 0 iff ex k being Integer st
( k = b & IT = a #Z k ) ) )
proof
assume A1: a > 0 ; ::_thesis: ( not b is Integer or ( IT = a #R b iff ex k being Integer st
( k = b & IT = a #Z k ) ) )
assume  b is Integer ; ::_thesis: ( IT = a #R b iff ex k being Integer st
( k = b & IT = a #Z k ) )
then reconsider b = b as Integer ;
a #R b = a #Q b by A1, PREPOWER:74
.= a #Z b by A1, PREPOWER:99 ;
hence  ( IT = a #R b iff ex k being Integer st
( k = b & IT = a #Z k ) ) ; ::_thesis: verum
end;
 ( a = 0 & b > 0 & b is Integer implies ( IT = 0 iff ex k being Integer st
( k = b & IT = a #Z k ) ) )
proof
assume A2: a = 0 ; ::_thesis: ( not b > 0 or not b is Integer or ( IT = 0 iff ex k being Integer st
( k = b & IT = a #Z k ) ) )
assume that
A3: b > 0 and
A4: b is Integer ; ::_thesis: ( IT = 0 iff ex k being Integer st
( k = b & IT = a #Z k ) )
 b in NAT by A3, A4, INT_1:3;
then reconsider b = b as Nat ;
a #Z b = a |^ b by PREPOWER:36
.= 0 by A2, A3, NAT_1:14, NEWTON:11 ;
hence  ( IT = 0 iff ex k being Integer st
( k = b & IT = a #Z k ) ) ; ::_thesis: verum
end;
hence  ( a = 0 & b > 0 & b is Integer implies ( IT = 0 iff ex k being Integer st
( k = b & IT = a #Z k ) ) ) ; ::_thesis: verum
end;
existence
 ( ( a > 0 implies ex b1 being real number st b1 = a #R b ) & ( a = 0 & b > 0 implies ex b1 being real number st b1 = 0 ) & ( b is Integer implies ex b1 being real number ex k being Integer st
( k = b & b1 = a #Z k ) ) )
proof
now__::_thesis:_(_b_is_Integer_implies_ex_c_being_set_ex_k_being_Integer_st_
(_k_=_b_&_c_=_a_#Z_k_)_)
assume  b is Integer ; ::_thesis: ex c being set ex k being Integer st
( k = b & c = a #Z k )
then reconsider k = b as Integer ;
take c = a #Z k; ::_thesis: ex k being Integer st
( k = b & c = a #Z k )
thus  ex k being Integer st
( k = b & c = a #Z k ) ; ::_thesis: verum
end;
hence  ( ( a > 0 implies ex b1 being real number st b1 = a #R b ) & ( a = 0 & b > 0 implies ex b1 being real number st b1 = 0 ) & ( b is Integer implies ex b1 being real number ex k being Integer st
( k = b & b1 = a #Z k ) ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being real number holds
( ( a > 0 & b1 = a #R b & b2 = a #R b implies b1 = b2 ) & ( a = 0 & b > 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) & ( b is Integer & ex k being Integer st
( k = b & b1 = a #Z k ) & ex k being Integer st
( k = b & b2 = a #Z k ) implies b1 = b2 ) ) ;
end;

:: deftheorem Def2 defines to_power POWER:def_2_:_
 for a, b, b3 being real number holds
( ( a > 0 implies ( b3 = a to_power b iff b3 = a #R b ) ) & ( a = 0 & b > 0 implies ( b3 = a to_power b iff b3 = 0 ) ) & ( b is Integer implies ( b3 = a to_power b iff ex k being Integer st
( k = b & b3 = a #Z k ) ) ) );

definition
let a, b be Real;
:: original: to_power
redefine funca to_power b ->  Real;
coherence
 a to_power b is Real by XREAL_0:def_1;
end;

theorem Th24: :: POWER:24
for a being real number holds a to_power 0 = 1
proof
let a be real number ; ::_thesis: a to_power 0 = 1
thus a to_power 0 = a #Z 0 by Def2
.= 1 by PREPOWER:34 ; ::_thesis: verum
end;

theorem Th25: :: POWER:25
for a being real number holds a to_power 1 = a
proof
let a be real number ; ::_thesis: a to_power 1 = a
thus a to_power 1 = a #Z 1 by Def2
.= a by PREPOWER:35 ; ::_thesis: verum
end;

theorem Th26: :: POWER:26
for a being real number holds 1 to_power a = 1
proof
let a be real number ; ::_thesis: 1 to_power a = 1
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 ; ::_thesis: verum
end;

theorem Th27: :: POWER:27
for a, b, c being real number st a > 0 holds
a to_power (b + c) = (a to_power b) * (a to_power c)
proof
let a, b, c be real number ; ::_thesis: ( a > 0 implies a to_power (b + c) = (a to_power b) * (a to_power c) )
assume A1: a > 0 ; ::_thesis: a to_power (b + c) = (a to_power b) * (a to_power c)
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  a to_power (b + c) = (a to_power b) * (a to_power c) by A1, Def2; ::_thesis: verum
end;

theorem Th28: :: POWER:28
for a, c being real number st a > 0 holds
a to_power (- c) = 1 / (a to_power c)
proof
let a, c be real number ; ::_thesis: ( a > 0 implies a to_power (- c) = 1 / (a to_power c) )
assume A1: a > 0 ; ::_thesis: a to_power (- c) = 1 / (a to_power c)
then  a #R (- c) = 1 / (a #R c) by PREPOWER:76;
then  a #R (- c) = 1 / (a to_power c) by A1, Def2;
hence  a to_power (- c) = 1 / (a to_power c) by A1, Def2; ::_thesis: verum
end;

theorem Th29: :: POWER:29
for a, b, c being real number st a > 0 holds
a to_power (b - c) = (a to_power b) / (a to_power c)
proof
let a, b, c be real number ; ::_thesis: ( a > 0 implies a to_power (b - c) = (a to_power b) / (a to_power c) )
assume A1: a > 0 ; ::_thesis: a to_power (b - c) = (a to_power b) / (a to_power c)
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  a to_power (b - c) = (a to_power b) / (a to_power c) by A1, Def2; ::_thesis: verum
end;

theorem :: POWER:30
for a, b, c being real number st a > 0 & b > 0 holds
(a * b) to_power c = (a to_power c) * (b to_power c)
proof
let a, b, c be real number ; ::_thesis: ( a > 0 & b > 0 implies (a * b) to_power c = (a to_power c) * (b to_power c) )
assume that
A1: a > 0 and
A2: b > 0 ; ::_thesis: (a * b) to_power c = (a to_power c) * (b to_power c)
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  (a * b) to_power c = (a to_power c) * (b to_power c) by A3, Def2; ::_thesis: verum
end;

theorem Th31: :: POWER:31
for a, b, c being real number st a > 0 & b > 0 holds
(a / b) to_power c = (a to_power c) / (b to_power c)
proof
let a, b, c be real number ; ::_thesis: ( a > 0 & b > 0 implies (a / b) to_power c = (a to_power c) / (b to_power c) )
assume that
A1: a > 0 and
A2: b > 0 ; ::_thesis: (a / b) to_power c = (a to_power c) / (b to_power c)
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  (a / b) to_power c = (a to_power c) / (b to_power c) by A3, Def2; ::_thesis: verum
end;

theorem Th32: :: POWER:32
for a, b being real number st a > 0 holds
(1 / a) to_power b = a to_power (- b)
proof
let a, b be real number ; ::_thesis: ( a > 0 implies (1 / a) to_power b = a to_power (- b) )
assume A1: a > 0 ; ::_thesis: (1 / a) to_power b = a to_power (- b)
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 ;
::_thesis: verum
end;

theorem Th33: :: POWER:33
for a, b, c being real number st a > 0 holds
(a to_power b) to_power c = a to_power (b * c)
proof
let a, b, c be real number ; ::_thesis: ( a > 0 implies (a to_power b) to_power c = a to_power (b * c) )
assume A1: a > 0 ; ::_thesis: (a to_power b) to_power c = a to_power (b * c)
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  (a to_power b) to_power c = a to_power (b * c) by A1, Def2; ::_thesis: verum
end;

theorem Th34: :: POWER:34
for a, b being real number st a > 0 holds
a to_power b > 0
proof
let a, b be real number ; ::_thesis: ( a > 0 implies a to_power b > 0 )
assume A1: a > 0 ; ::_thesis: a to_power b > 0
then  a #R b > 0 by PREPOWER:81;
hence  a to_power b > 0 by A1, Def2; ::_thesis: verum
end;

theorem Th35: :: POWER:35
for a, b being real number st a > 1 & b > 0 holds
a to_power b > 1
proof
let a, b be real number ; ::_thesis: ( a > 1 & b > 0 implies a to_power b > 1 )
assume that
A1: a > 1 and
A2: b > 0 ; ::_thesis: a to_power b > 1
 a #R b > 1 by A1, A2, PREPOWER:86;
hence  a to_power b > 1 by A1, Def2; ::_thesis: verum
end;

theorem Th36: :: POWER:36
for a, b being real number st a > 1 & b < 0 holds
a to_power b < 1
proof
let a, b be real number ; ::_thesis: ( a > 1 & b < 0 implies a to_power b < 1 )
assume that
A1: a > 1 and
A2: b < 0 ; ::_thesis: a to_power b < 1
 a #R b < 1 by A1, A2, PREPOWER:88;
hence  a to_power b < 1 by A1, Def2; ::_thesis: verum
end;

theorem :: POWER:37
for a, b, c being real number st a > 0 & a < b & c > 0 holds
a to_power c < b to_power c
proof
let a, b, c be real number ; ::_thesis: ( a > 0 & a < b & c > 0 implies a to_power c < b to_power c )
assume that
A1: a > 0 and
A2: a < b and
A3: c > 0 ; ::_thesis: a to_power c < b to_power c
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  a to_power c < b to_power c by A5, XCMPLX_1:87; ::_thesis: verum
end;

theorem :: POWER:38
for a, b, c being real number st a > 0 & a < b & c < 0 holds
a to_power c > b to_power c
proof
let a, b, c be real number ; ::_thesis: ( a > 0 & a < b & c < 0 implies a to_power c > b to_power c )
assume that
A1: a > 0 and
A2: a < b and
A3: c < 0 ; ::_thesis: a to_power c > b to_power c
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, 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  a to_power c > b to_power c by A5, XCMPLX_1:87; ::_thesis: verum
end;

theorem Th39: :: POWER:39
for a, b, c being real number st a < b & c > 1 holds
c to_power a < c to_power b
proof
let a, b, c be real number ; ::_thesis: ( a < b & c > 1 implies c to_power a < c to_power b )
assume that
A1: a < b and
A2: c > 1 ; ::_thesis: c to_power a < c to_power b
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  c to_power a < c to_power b by A4, XCMPLX_1:87; ::_thesis: verum
end;

theorem Th40: :: POWER:40
for a, b, c being real number st a < b & c > 0 & c < 1 holds
c to_power a > c to_power b
proof
let a, b, c be real number ; ::_thesis: ( a < b & c > 0 & c < 1 implies c to_power a > c to_power b )
assume that
A1: a < b and
A2: c > 0 and
A3: c < 1 ; ::_thesis: c to_power a > c to_power b
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  c to_power a > c to_power b by A6, XREAL_1:91; ::_thesis: verum
end;

registration
let a be real number ;
let n be Nat;
identifya to_power n with a |^ n;
compatibility
 a to_power n = a |^ n
proof
thus a to_power n = a #Z n by Def2
.= a |^ n by PREPOWER:36 ; ::_thesis: verum
end;
end;

theorem :: POWER:41
for a being real number
for n being Nat holds a to_power n = a |^ n ;

theorem Th42: :: POWER:42
for k being Integer st k <> 0 holds
0 to_power k = 0
proof
let k be Integer; ::_thesis: ( k <> 0 implies 0 to_power k = 0 )
 0 to_power k = 0 #Z k by Def2;
hence  ( k <> 0 implies 0 to_power k = 0 ) by PREPOWER:100; ::_thesis: verum
end;

theorem :: POWER:43
for a being real number
for k being Integer holds a to_power k = a #Z k by Def2;

theorem Th44: :: POWER:44
for a being real number
for p being Rational st a > 0 holds
a to_power p = a #Q p
proof
let a be real number ; ::_thesis: for p being Rational st a > 0 holds
a to_power p = a #Q p
let p be Rational; ::_thesis: ( a > 0 implies a to_power p = a #Q p )
assume A1: a > 0 ; ::_thesis: a to_power p = a #Q p
hence a to_power p = a #R p by Def2
.= a #Q p by A1, PREPOWER:74 ;
::_thesis: verum
end;

theorem Th45: :: POWER:45
for a being real number
for n being Element of NAT st a >= 0 & n >= 1 holds
a to_power (1 / n) = n -root a
proof
let a be real number ; ::_thesis: for n being Element of NAT st a >= 0 & n >= 1 holds
a to_power (1 / n) = n -root a
let n be Element of NAT ; ::_thesis: ( a >= 0 & n >= 1 implies a to_power (1 / n) = n -root a )
assume that
A1: a >= 0 and
A2: n >= 1 ; ::_thesis: a to_power (1 / n) = n -root a
reconsider p = n " as Rational ;
now__::_thesis:_a_to_power_(1_/_n)_=_n_-Root_a
percases ( a > 0 or a = 0 ) by A1;
suppose a > 0 ; ::_thesis: a to_power (1 / n) = n -Root a
hence a to_power (1 / n) = a #Q p by Th44
.= n -Root a by A2, PREPOWER:50 ;
::_thesis: verum
end;
supposeA3: a = 0 ; ::_thesis: a to_power (1 / n) = n -Root a
hence a to_power (1 / n) = 0 by A2, Def2
.= n -Root a by A2, A3, PREPOWER:def_2 ;
::_thesis: verum
end;
end;
end;
hence  a to_power (1 / n) = n -root a by A1, A2, Def1; ::_thesis: verum
end;

theorem Th46: :: POWER:46
for a being real number holds a to_power 2 = a ^2
proof
let a be real number ; ::_thesis: a to_power 2 = a ^2
now__::_thesis:_a_to_power_2_=_a_^2
percases ( a > 0 or a = 0 or a < 0 ) ;
supposeA1: a > 0 ; ::_thesis: a to_power 2 = a ^2
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 by Th25
.= a ^2 by Th25 ; ::_thesis: verum
end;
suppose a = 0 ; ::_thesis: a to_power 2 = a ^2
hence  a to_power 2 = a ^2 by Def2; ::_thesis: verum
end;
supposeA2: a < 0 ; ::_thesis: a to_power 2 = a ^2
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 ; ::_thesis: verum
end;
end;
end;
hence  a to_power 2 = a ^2 ; ::_thesis: verum
end;

theorem Th47: :: POWER:47
for a being real number
for k being Integer st k is even holds
(- a) to_power k = a to_power k
proof
let a be real number ; ::_thesis: for k being Integer st k is even holds
(- a) to_power k = a to_power k
let k be Integer; ::_thesis: ( k is even implies (- a) to_power k = a to_power k )
given l being Integer such that A1: k = 2 * l ; :: according to INT_1:def_3,ABIAN:def_1 ::_thesis: (- a) to_power k = a to_power k
percases ( a = 0 or a > 0 or a < 0 ) ;
suppose a = 0 ; ::_thesis: (- a) to_power k = a to_power k
hence  (- a) to_power k = a to_power k ; ::_thesis: verum
end;
suppose a > 0 ; ::_thesis: (- a) to_power k = a to_power k
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 ;
::_thesis: verum
end;
suppose a < 0 ; ::_thesis: (- a) to_power k = a to_power k
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 ;
::_thesis: verum
end;
end;
end;

theorem :: POWER:48
for a being real number
for k being Integer st k is odd holds
(- a) to_power k = - (a to_power k)
proof
let a be real number ; ::_thesis: for k being Integer st k is odd holds
(- a) to_power k = - (a to_power k)
let k be Integer; ::_thesis: ( k is odd implies (- a) to_power k = - (a to_power k) )
assume A1: k is odd ; ::_thesis: (- a) to_power k = - (a to_power k)
then consider l being Integer such that
A2: k = (2 * l) + 1 by ABIAN:1;
percases ( a = 0 or a > 0 or a < 0 ) ;
supposeA3: a = 0 ; ::_thesis: (- a) to_power k = - (a to_power k)
 k <> 0 by A1;
then  a to_power k = 0 by A3, Th42;
hence  (- a) to_power k = - (a to_power k) by A3; ::_thesis: verum
end;
supposeA4: a > 0 ; ::_thesis: (- a) to_power k = - (a to_power k)
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 by Th25
.= ((- 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  (- a) to_power k = - (a to_power k) ; ::_thesis: verum
end;
supposeA6: a < 0 ; ::_thesis: (- a) to_power k = - (a to_power k)
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) by Th25
.= (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 ;
::_thesis: verum
end;
end;
end;

theorem :: POWER:49
for a being real number
for n being Element of NAT st - 1 < a holds
(1 + a) to_power n >= 1 + (n * a) by PREPOWER:16;

theorem Th50: :: POWER:50
for a, c, d being real number st a > 0 & a <> 1 & c <> d holds
a to_power c <> a to_power d
proof
let a, c, d be real number ; ::_thesis: ( a > 0 & a <> 1 & c <> d implies a to_power c <> a to_power d )
assume that
A1: a > 0 and
A2: a <> 1 and
A3: c <> d ; ::_thesis: a to_power c <> a to_power d
now__::_thesis:_a_to_power_c_<>_a_to_power_d
percases ( c < d or c > d ) by A3, XXREAL_0:1;
supposeA4: c < d ; ::_thesis: a to_power c <> a to_power d
now__::_thesis:_a_to_power_c_<>_a_to_power_d
percases ( a < 1 or a > 1 ) by A2, XXREAL_0:1;
suppose a < 1 ; ::_thesis: a to_power c <> a to_power d
hence  a to_power c <> a to_power d by A1, A4, Th40; ::_thesis: verum
end;
suppose a > 1 ; ::_thesis: a to_power c <> a to_power d
hence  a to_power c <> a to_power d by A4, Th39; ::_thesis: verum
end;
end;
end;
hence  a to_power c <> a to_power d ; ::_thesis: verum
end;
supposeA5: c > d ; ::_thesis: a to_power c <> a to_power d
now__::_thesis:_a_to_power_c_<>_a_to_power_d
percases ( a < 1 or a > 1 ) by A2, XXREAL_0:1;
suppose a < 1 ; ::_thesis: a to_power c <> a to_power d
hence  a to_power c <> a to_power d by A1, A5, Th40; ::_thesis: verum
end;
suppose a > 1 ; ::_thesis: a to_power c <> a to_power d
hence  a to_power c <> a to_power d by A5, Th39; ::_thesis: verum
end;
end;
end;
hence  a to_power c <> a to_power d ; ::_thesis: verum
end;
end;
end;
hence  a to_power c <> a to_power d ; ::_thesis: verum
end;

definition
let a, b be real number ;
assume that
A1: a > 0 and
A2: a <> 1 and
A3: b > 0 ;
func log (a,b) ->  real number  means :Def3: :: POWER:def 3
a to_power it = b;
existence
 ex b1 being real number st a to_power b1 = b
proof
reconsider a1 = a, b1 = b as Real by XREAL_0:def_1;
set X =  {  c where c is Real : a to_power c <= b  }  ;
 for x being set st x in  {  c where c is Real : a to_power c <= b  }  holds
x in REAL
proof
let x be set ; ::_thesis: ( x in  {  c where c is Real : a to_power c <= b  }  implies x in REAL )
assume  x in  {  c where c is Real : a to_power c <= b  }  ; ::_thesis: x in REAL
then  ex c being Real st
( x = c & a to_power c <= b ) ;
hence  x in REAL ; ::_thesis: verum
end;
then reconsider X =  {  c where c is Real : a to_power c <= b  }  as Subset of REAL by TARSKI:def_3;
A4: ex d being real number st d in X
proof
A5: now__::_thesis:_for_a,_b_being_real_number_st_a_>_1_&_b_>_0_holds_
ex_d_being_real_number_st_a_to_power_d_<=_b
let a, b be real number ; ::_thesis: ( a > 1 & b > 0 implies ex d being real number st a to_power d <= b )
assume that
A6: a > 1 and
A7: b > 0 ; ::_thesis: ex d being real number st a to_power d <= b
reconsider a1 = a, b1 = b as Real by XREAL_0:def_1;
set e = a1 - 1;
consider n being Element of NAT  such that
A8: n > 1 / (b * (a1 - 1)) by SEQ_4:3;
 a1 - 1 > 0 - 1 by A6, XREAL_1:9;
then A9: (1 + (a1 - 1)) to_power n >= 1 + (n * (a1 - 1)) by PREPOWER:16;
 1 + (n * (a1 - 1)) >= 0 + (n * (a1 - 1)) by XREAL_1:6;
then A10: (1 + (a1 - 1)) to_power n >= n * (a1 - 1) by A9, XXREAL_0:2;
A11: a1 - 1 > 1 - 1 by A6, XREAL_1:9;
then  n * (a1 - 1) > (1 / (b * (a1 - 1))) * (a1 - 1) by A8, XREAL_1:68;
then  n * (a1 - 1) >= 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 being real number st a to_power d <= b ; ::_thesis: verum
end;
now__::_thesis:_ex_d_being_real_number_st_a_to_power_d_<=_b
percases ( a > 1 or a < 1 ) by A2, XXREAL_0:1;
suppose a > 1 ; ::_thesis: ex d being real number st a to_power d <= b
hence  ex d being real number st a to_power d <= b by A3, A5; ::_thesis: verum
end;
suppose a < 1 ; ::_thesis: ex e being real number st a to_power e <= b
then  1 / a > 1 / 1 by A1, XREAL_1:88;
then consider d being real number  such that
A12: (1 / a) to_power d <= b by A3, A5;
 a1 to_power (- d) <= b1 by A1, A12, Th32;
hence  ex e being real number st a to_power e <= b ; ::_thesis: verum
end;
end;
end;
then consider d being real number  such that
A13: a to_power d <= b ;
take  d ; ::_thesis: d in X
 d is Real by XREAL_0:def_1;
hence  d in X by A13; ::_thesis: verum
end;
now__::_thesis:_ex_d_being_Element_of_REAL_st_b_=_a_to_power_d
percases ( a > 1 or a < 1 ) by A2, XXREAL_0:1;
supposeA14: a > 1 ; ::_thesis: ex d being Element of REAL st b = a to_power d
A15: X is bounded_above
proof
consider n being Element of 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 ; :: according to XXREAL_2:def_10 ::_thesis: n is UpperBound of X
let c be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not c in X or c <= n )
assume  c in X ; ::_thesis: c <= n
then consider d being 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; ::_thesis: verum
end;
take d = upper_bound X; ::_thesis: b = a to_power d
A20: not b < a to_power d
proof
assume  a to_power d > b ; ::_thesis: contradiction
then consider e being real number  such that
A21: b < e and
A22: e < a to_power d by XREAL_1:5;
reconsider e = e as Real by XREAL_0:def_1;
consider n being Element of NAT  such that
A23: n > (a1 - 1) / ((e / b1) - 1) by SEQ_4:3;
reconsider m = max (1,n) as Element of NAT ;
 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 being real number  such that
A29: c in X and
A30: d - (1 / m) < c by A4, A15, A26, SEQ_4:def_1;
reconsider c = c as Real by XREAL_0:def_1;
A31: ex g being 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; ::_thesis: verum
end;
 not a to_power d < b
proof
assume  a to_power d < b ; ::_thesis: contradiction
then consider e being real number  such that
A33: a to_power d < e and
A34: e < b by XREAL_1:5;
reconsider e = e as Real by XREAL_0:def_1;
A35: a1 to_power d > 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 H1( Element of NAT ) ->  real number = $1 -root a;
consider s being Real_Sequence such that
A37: for n being Element of NAT holds s . n = H1(n) from SEQ_1:sch_1();
 for n being Element of NAT st n >= 1 holds
s . n = n -root a1 by A37;
then  ( s is convergent & lim s = 1 ) by A1, Th23;
then consider n being Element of NAT  such that
A38: for m being Element of NAT st m >= n holds
abs ((s . m) - 1) < (b / e) - 1 by A36, SEQ_2:def_7;
reconsider m = max (1,n) as Element of NAT ;
 abs ((s . m) - 1) < (b / e) - 1 by A38, XXREAL_0:25;
then A39: abs ((m -root a) - 1) < (b / e) - 1 by A37;
 (m -root a) - 1 <= abs ((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; ::_thesis: verum
end;
hence  b = a to_power d by A20, XXREAL_0:1; ::_thesis: verum
end;
supposeA41: a < 1 ; ::_thesis: ex d being Element of REAL st b = a to_power d
A42: X is bounded_below
proof
consider n being Element of 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 ; :: according to XXREAL_2:def_9 ::_thesis: - n is LowerBound of X
let c be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not c in X or - n <= c )
assume  c in X ; ::_thesis: - n <= c
then consider d being 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; ::_thesis: verum
end;
take d = lower_bound X; ::_thesis: b = a to_power d
A47: not b < a to_power d
proof
assume  a to_power d > b ; ::_thesis: contradiction
then consider e being real number  such that
A48: b < e and
A49: e < a to_power d by XREAL_1:5;
reconsider e = e as Real by XREAL_0:def_1;
consider n being Element of NAT  such that
A50: n > ((1 / a1) - 1) / ((e / b1) - 1) by SEQ_4:3;
reconsider m = max (1,n) as Element of NAT ;
 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 being real number  such that
A56: c in X and
A57: c < d + (1 / m) by A4, A42, A53, SEQ_4:def_2;
reconsider c = c as Real by XREAL_0:def_1;
A58: ex g being 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; ::_thesis: verum
end;
 not a to_power d < b
proof
assume  a to_power d < b ; ::_thesis: contradiction
then consider e being real number  such that
A60: a to_power d < e and
A61: e < b by XREAL_1:5;
reconsider e = e as Real by XREAL_0:def_1;
A62: a1 to_power d > 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 H1( Element of NAT ) ->  Real = $1 -root (1 / a);
consider s being Real_Sequence such that
A64: for n being Element of NAT holds s . n = H1(n) from SEQ_1:sch_1();
 for n being Element of NAT 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 being Element of NAT  such that
A65: for m being Element of NAT st m >= n holds
abs ((s . m) - 1) < (b / e) - 1 by A63, SEQ_2:def_7;
reconsider m = max (1,n) as Element of NAT ;
 abs ((s . m) - 1) < (b / e) - 1 by A65, XXREAL_0:25;
then A66: abs ((m -root (1 / a)) - 1) < (b / e) - 1 by A64;
 (m -root (1 / a)) - 1 <= abs ((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)) < b by A67, XXREAL_0:2;
then  d - (1 / m) in X ;
then  ( m >= 1 & d - (1 / m) >= d ) by A42, SEQ_4:def_2, XXREAL_0:25;
hence  contradiction by XREAL_1:44; ::_thesis: verum
end;
hence  b = a to_power d by A47, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
hence  ex b1 being real number st a to_power b1 = b ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being real number st a to_power b1 = b & a to_power b2 = b holds
b1 = b2 by A1, A2, Th50;
end;

:: deftheorem Def3 defines log POWER:def_3_:_
 for a, b being real number st a > 0 & a <> 1 & b > 0 holds
for b3 being real number holds
( b3 = log (a,b) iff a to_power b3 = b );

definition
let a, b be Real;
:: original: log
redefine func log (a,b) ->  Real;
coherence
 log (a,b) is Real by XREAL_0:def_1;
end;

theorem :: POWER:51
for a being real number st a > 0 & a <> 1 holds
log (a,1) = 0
proof
let a be real number ; ::_thesis: ( a > 0 & a <> 1 implies log (a,1) = 0 )
assume A1: ( a > 0 & a <> 1 ) ; ::_thesis: log (a,1) = 0
 a to_power 0 = 1 by Th24;
hence  log (a,1) = 0 by A1, Def3; ::_thesis: verum
end;

theorem :: POWER:52
for a being real number st a > 0 & a <> 1 holds
log (a,a) = 1
proof
let a be real number ; ::_thesis: ( a > 0 & a <> 1 implies log (a,a) = 1 )
assume A1: ( a > 0 & a <> 1 ) ; ::_thesis: log (a,a) = 1
 a to_power 1 = a by Th25;
hence  log (a,a) = 1 by A1, Def3; ::_thesis: verum
end;

theorem :: POWER:53
for a, b, c being real number st a > 0 & a <> 1 & b > 0 & c > 0 holds
(log (a,b)) + (log (a,c)) = log (a,(b * c))
proof
let a, b, c be real number ; ::_thesis: ( a > 0 & a <> 1 & b > 0 & c > 0 implies (log (a,b)) + (log (a,c)) = log (a,(b * c)) )
assume that
A1: a > 0 and
A2: a <> 1 and
A3: b > 0 and
A4: c > 0 ; ::_thesis: (log (a,b)) + (log (a,c)) = log (a,(b * c))
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  (log (a,b)) + (log (a,c)) = log (a,(b * c)) by A1, A2, A5, Def3; ::_thesis: verum
end;

theorem :: POWER:54
for a, b, c being real number st a > 0 & a <> 1 & b > 0 & c > 0 holds
(log (a,b)) - (log (a,c)) = log (a,(b / c))
proof
let a, b, c be real number ; ::_thesis: ( a > 0 & a <> 1 & b > 0 & c > 0 implies (log (a,b)) - (log (a,c)) = log (a,(b / c)) )
assume that
A1: a > 0 and
A2: a <> 1 and
A3: b > 0 and
A4: c > 0 ; ::_thesis: (log (a,b)) - (log (a,c)) = log (a,(b / c))
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  (log (a,b)) - (log (a,c)) = log (a,(b / c)) by A1, A2, A5, Def3; ::_thesis: verum
end;

theorem :: POWER:55
for a, b, c being real number st a > 0 & a <> 1 & b > 0 holds
log (a,(b to_power c)) = c * (log (a,b))
proof
let a, b, c be real number ; ::_thesis: ( a > 0 & a <> 1 & b > 0 implies log (a,(b to_power c)) = c * (log (a,b)) )
assume that
A1: a > 0 and
A2: a <> 1 and
A3: b > 0 ; ::_thesis: log (a,(b to_power c)) = c * (log (a,b))
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  log (a,(b to_power c)) = c * (log (a,b)) by A1, A2, A4, Def3; ::_thesis: verum
end;

theorem :: POWER:56
for a, b, c being real number st a > 0 & a <> 1 & b > 0 & b <> 1 & c > 0 holds
log (a,c) = (log (a,b)) * (log (b,c))
proof
let a, b, c be real number ; ::_thesis: ( a > 0 & a <> 1 & b > 0 & b <> 1 & c > 0 implies log (a,c) = (log (a,b)) * (log (b,c)) )
assume that
A1: a > 0 and
A2: a <> 1 and
A3: b > 0 and
A4: b <> 1 and
A5: c > 0 ; ::_thesis: log (a,c) = (log (a,b)) * (log (b,c))
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  log (a,c) = (log (a,b)) * (log (b,c)) by A1, A2, A5, Def3; ::_thesis: verum
end;

theorem :: POWER:57
for a, b, c being real number st a > 1 & b > 0 & c > b holds
log (a,c) > log (a,b)
proof
let a, b, c be real number ; ::_thesis: ( a > 1 & b > 0 & c > b implies log (a,c) > log (a,b) )
assume that
A1: a > 1 and
A2: b > 0 and
A3: c > b and
A4: log (a,c) <= log (a,b) ; ::_thesis: contradiction
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__::_thesis:_contradiction
percases ( log (a,c) < log (a,b) or log (a,c) = log (a,b) ) by A4, XXREAL_0:1;
suppose log (a,c) < log (a,b) ; ::_thesis: contradiction
hence  contradiction by A1, A3, A5, A6, Th39; ::_thesis: verum
end;
suppose log (a,c) = log (a,b) ; ::_thesis: contradiction
hence  contradiction by A1, A2, A3, A6, Def3; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;

theorem :: POWER:58
for a, b, c being real number st a > 0 & a < 1 & b > 0 & c > b holds
log (a,c) < log (a,b)
proof
let a, b, c be real number ; ::_thesis: ( a > 0 & a < 1 & b > 0 & c > b implies log (a,c) < log (a,b) )
assume that
A1: ( a > 0 & a < 1 ) and
A2: b > 0 and
A3: c > b and
A4: log (a,c) >= log (a,b) ; ::_thesis: contradiction
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__::_thesis:_contradiction
percases ( log (a,c) > log (a,b) or log (a,c) = log (a,b) ) by A4, XXREAL_0:1;
suppose log (a,c) > log (a,b) ; ::_thesis: contradiction
hence  contradiction by A1, A3, A5, A6, Th40; ::_thesis: verum
end;
suppose log (a,c) = log (a,b) ; ::_thesis: contradiction
hence  contradiction by A1, A2, A3, A6, Def3; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;

theorem :: POWER:59
for s being Real_Sequence st ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds
s is convergent
proof
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) implies s is convergent )
assume A1: for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ; ::_thesis: s is convergent
now__::_thesis:_for_n_being_Element_of_NAT_holds_s_._(n_+_1)_>=_s_._n
let n be Element of NAT ; ::_thesis: s . (n + 1) >= s . n
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)) by Th25
.= ((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; ::_thesis: verum
end;
then A6: s is non-decreasing by SEQM_3:def_8;
now__::_thesis:_for_n_being_Element_of_NAT_holds_s_._n_<_(2_*_2)_+_1
let n be Element of NAT ; ::_thesis: s . n < (2 * 2) + 1
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__::_thesis:_not_((2_*_(n_+_1))_-_n)_/_((2_*_(n_+_1))_+_1)_<_1_/_2
assume  ((2 * (n + 1)) - n) / ((2 * (n + 1)) + 1) < 1 / 2 ; ::_thesis: contradiction
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; ::_thesis: verum
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; ::_thesis: verum
end;
then  s is bounded_above by SEQ_2:def_3;
hence  s is convergent by A6; ::_thesis: verum
end;

definition
func number_e  ->  real number  means :: POWER:def 4
 for s being Real_Sequence st ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds
it = lim s;
existence
 ex b1 being real number st
for s being Real_Sequence st ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds
b1 = lim s
proof
deffunc H1( Element of NAT ) ->  Real = (1 + (1 / ($1 + 1))) to_power ($1 + 1);
consider s1 being Real_Sequence such that
A1: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch_1();
take  lim s1 ; ::_thesis: for s being Real_Sequence st ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds
lim s1 = lim s
let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) implies lim s1 = lim s )
assume A2: for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ; ::_thesis: lim s1 = lim s
now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_=_s_._n
let n be Element of NAT ; ::_thesis: s1 . n = s . n
thus s1 . n = (1 + (1 / (n + 1))) to_power (n + 1) by A1
.= s . n by A2 ; ::_thesis: verum
end;
hence  lim s1 = lim s by FUNCT_2:63; ::_thesis: verum
end;
uniqueness
 for b1, b2 being real number st ( for s being Real_Sequence st ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds
b1 = lim s ) & ( for s being Real_Sequence st ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds
b2 = lim s ) holds
b1 = b2
proof
let a, b be real number ; ::_thesis: ( ( for s being Real_Sequence st ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds
a = lim s ) & ( for s being Real_Sequence st ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds
b = lim s ) implies a = b )
assume that
A3: for s being Real_Sequence st ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds
a = lim s and
A4: for s being Real_Sequence st ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds
b = lim s ; ::_thesis: a = b
deffunc H1( Element of NAT ) ->  Real = (1 + (1 / ($1 + 1))) to_power ($1 + 1);
consider s1 being Real_Sequence such that
A5: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch_1();
 lim s1 = a by A3, A5;
hence  a = b by A4, A5; ::_thesis: verum
end;
end;

:: deftheorem  defines number_e POWER:def_4_:_
 for b1 being real number holds
( b1 = number_e iff for s being Real_Sequence st ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds
b1 = lim s );

definition
:: original: number_e
redefine func number_e  ->  Real;
coherence
 number_e is Real by XREAL_0:def_1;
end;

theorem Th60: :: POWER:60
2 to_power 2 = 4
proof
thus 2 to_power 2 = 2 ^2 by Th46
.= 4 ; ::_thesis: verum
end;

theorem Th61: :: POWER:61
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 Th25, Th60
.= 8 ; ::_thesis: verum
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 ; ::_thesis: verum
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 ; ::_thesis: verum
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 ; ::_thesis: verum
end;