:: POWER semantic presentation

begin

theorem :: POWER:1
for a being ( ( real ) ( V11() real ext-real ) number )
for n being ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) st n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) is even holds
(- a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( V11() ) ( V11() real ext-real ) set ) |^ n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) set ) = a : ( ( real ) ( V11() real ext-real ) number ) |^ n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: POWER:2
for a being ( ( real ) ( V11() real ext-real ) number )
for n being ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) st n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) is odd holds
(- a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( V11() ) ( V11() real ext-real ) set ) |^ n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) set ) = - (a : ( ( real ) ( V11() real ext-real ) number ) |^ n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( V11() ) ( V11() real ext-real ) set ) ;

theorem :: POWER:3
for a being ( ( real ) ( V11() real ext-real ) number )
for n being ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) st ( a : ( ( real ) ( V11() real ext-real ) number ) >= 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) or n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) is even ) holds
a : ( ( real ) ( V11() real ext-real ) number ) |^ n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) set ) >= 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ;

definition
let n be ( ( natural ) ( ordinal natural V11() real ext-real non negative integer rational ) Nat) ;
let a be ( ( real ) ( V11() real ext-real ) number ) ;
func n -root a -> ( ( real ) ( V11() real ext-real ) number ) equals :: POWER:def 1
n : ( ( V49() right_end ) ( V49() right_end ) set ) -Root a : ( ( V21() V30(n : ( ( V49() right_end ) ( V49() right_end ) set ) ,n : ( ( V49() right_end ) ( V49() right_end ) set ) ) ) ( V21() V30(n : ( ( V49() right_end ) ( V49() right_end ) set ) ,n : ( ( V49() right_end ) ( V49() right_end ) set ) ) ) Element of K6(K7(n : ( ( V49() right_end ) ( V49() right_end ) set ) ,n : ( ( V49() right_end ) ( V49() right_end ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) if ( a : ( ( V21() V30(n : ( ( V49() right_end ) ( V49() right_end ) set ) ,n : ( ( V49() right_end ) ( V49() right_end ) set ) ) ) ( V21() V30(n : ( ( V49() right_end ) ( V49() right_end ) set ) ,n : ( ( V49() right_end ) ( V49() right_end ) set ) ) ) Element of K6(K7(n : ( ( V49() right_end ) ( V49() right_end ) set ) ,n : ( ( V49() right_end ) ( V49() right_end ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) >= 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & n : ( ( V49() right_end ) ( V49() right_end ) set ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) )
- (n : ( ( V49() right_end ) ( V49() right_end ) set ) -Root (- a : ( ( V21() V30(n : ( ( V49() right_end ) ( V49() right_end ) set ) ,n : ( ( V49() right_end ) ( V49() right_end ) set ) ) ) ( V21() V30(n : ( ( V49() right_end ) ( V49() right_end ) set ) ,n : ( ( V49() right_end ) ( V49() right_end ) set ) ) ) Element of K6(K7(n : ( ( V49() right_end ) ( V49() right_end ) set ) ,n : ( ( V49() right_end ) ( V49() right_end ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V11() ) ( V11() ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) : ( ( V11() ) ( V11() real ext-real ) set ) if ( a : ( ( V21() V30(n : ( ( V49() right_end ) ( V49() right_end ) set ) ,n : ( ( V49() right_end ) ( V49() right_end ) set ) ) ) ( V21() V30(n : ( ( V49() right_end ) ( V49() right_end ) set ) ,n : ( ( V49() right_end ) ( V49() right_end ) set ) ) ) Element of K6(K7(n : ( ( V49() right_end ) ( V49() right_end ) set ) ,n : ( ( V49() right_end ) ( V49() right_end ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) < 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & n : ( ( V49() right_end ) ( V49() right_end ) set ) is odd )
;
end;

definition
let n be ( ( natural ) ( ordinal natural V11() real ext-real non negative integer rational ) Nat) ;
let a be ( ( ) ( V11() real ext-real ) Real) ;
:: original: -root
redefine func n -root a -> ( ( ) ( V11() real ext-real ) Real) ;
end;

theorem :: POWER:4
for a being ( ( real ) ( V11() real ext-real ) number )
for n being ( ( natural ) ( ordinal natural V11() real ext-real non negative integer rational ) Nat) st ( ( n : ( ( natural ) ( ordinal natural V11() real ext-real non negative integer rational ) Nat) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( real ) ( V11() real ext-real ) number ) >= 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ) or n : ( ( natural ) ( ordinal natural V11() real ext-real non negative integer rational ) Nat) is odd ) holds
( (n : ( ( natural ) ( ordinal natural V11() real ext-real non negative integer rational ) Nat) -root a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) |^ n : ( ( natural ) ( ordinal natural V11() real ext-real non negative integer rational ) Nat) : ( ( ) ( V11() real ext-real ) set ) = a : ( ( real ) ( V11() real ext-real ) number ) & n : ( ( natural ) ( ordinal natural V11() real ext-real non negative integer rational ) Nat) -root (a : ( ( real ) ( V11() real ext-real ) number ) |^ n : ( ( natural ) ( ordinal natural V11() real ext-real non negative integer rational ) Nat) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( real ) ( V11() real ext-real ) number ) = a : ( ( real ) ( V11() real ext-real ) number ) ) ;

theorem :: POWER:5
for n being ( ( natural ) ( ordinal natural V11() real ext-real non negative integer rational ) Nat) st n : ( ( natural ) ( ordinal natural V11() real ext-real non negative integer rational ) Nat) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
n : ( ( natural ) ( ordinal natural V11() real ext-real non negative integer rational ) Nat) -root 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Real) = 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: POWER:6
for n being ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) st n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Real) = 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: POWER:7
for a being ( ( real ) ( V11() real ext-real ) number )
for n being ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) st a : ( ( real ) ( V11() real ext-real ) number ) >= 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) >= 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: POWER:8
for n being ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) st n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) is odd holds
n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root (- 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real non positive integer rational ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( V11() real ext-real ) Real) = - 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real non positive integer rational ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ;

theorem :: POWER:9
for a being ( ( real ) ( V11() real ext-real ) number ) holds 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) = a : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: POWER:10
for a being ( ( real ) ( V11() real ext-real ) number )
for n being ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) st n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) is odd holds
n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) = - (n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root (- a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( V11() ) ( V11() real ext-real ) set ) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( V11() ) ( V11() real ext-real ) set ) ;

theorem :: POWER:11
for a, b being ( ( real ) ( V11() real ext-real ) number )
for n being ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) st ( ( n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( real ) ( V11() real ext-real ) number ) >= 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( V11() real ext-real ) number ) >= 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ) or n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) is odd ) holds
n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root (a : ( ( real ) ( V11() real ext-real ) number ) * b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( real ) ( V11() real ext-real ) number ) = (n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) * (n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: POWER:12
for a being ( ( real ) ( V11() real ext-real ) number )
for n being ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) st ( ( a : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ) or ( a : ( ( real ) ( V11() real ext-real ) number ) <> 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) is odd ) ) holds
n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) / a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( V11() real ext-real ) Real) = 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) / (n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ;

theorem :: POWER:13
for a, b being ( ( real ) ( V11() real ext-real ) number )
for n being ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) st ( ( a : ( ( real ) ( V11() real ext-real ) number ) >= 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ) or ( b : ( ( real ) ( V11() real ext-real ) number ) <> 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) is odd ) ) holds
n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root (a : ( ( real ) ( V11() real ext-real ) number ) / b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V48() V54() V55() ) set ) ) : ( ( real ) ( V11() real ext-real ) number ) = (n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) / (n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V48() V54() V55() ) set ) ) ;

theorem :: POWER:14
for a being ( ( real ) ( V11() real ext-real ) number )
for n, m being ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) st ( ( a : ( ( real ) ( V11() real ext-real ) number ) >= 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & m : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ) or ( n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) is odd & m : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) is odd ) ) holds
n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root (m : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) = (n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) * m : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: POWER:15
for a being ( ( real ) ( V11() real ext-real ) number )
for n, m being ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) st ( ( a : ( ( real ) ( V11() real ext-real ) number ) >= 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & m : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ) or ( n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) is odd & m : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) is odd ) ) holds
(n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) * (m : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) = (n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) * m : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root (a : ( ( real ) ( V11() real ext-real ) number ) |^ (n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) + m : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: POWER:16
for a, b being ( ( real ) ( V11() real ext-real ) number )
for n being ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) st a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) & ( ( 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) <= a : ( ( real ) ( V11() real ext-real ) number ) & n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ) or n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) is odd ) holds
n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) <= n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root b : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: POWER:17
for a, b being ( ( real ) ( V11() real ext-real ) number )
for n being ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) st a : ( ( real ) ( V11() real ext-real ) number ) < b : ( ( real ) ( V11() real ext-real ) number ) & ( ( a : ( ( real ) ( V11() real ext-real ) number ) >= 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ) or n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) is odd ) holds
n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) < n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root b : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: POWER:18
for a being ( ( real ) ( V11() real ext-real ) number )
for n being ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) st a : ( ( real ) ( V11() real ext-real ) number ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( real ) ( V11() real ext-real ) number ) >= n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) ) ;

theorem :: POWER:19
for a being ( ( real ) ( V11() real ext-real ) number )
for n being ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) st a : ( ( real ) ( V11() real ext-real ) number ) <= - 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real non positive integer rational ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) & n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) is odd holds
( n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) <= - 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real non positive integer rational ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) & a : ( ( real ) ( V11() real ext-real ) number ) <= n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) ) ;

theorem :: POWER:20
for a being ( ( real ) ( V11() real ext-real ) number )
for n being ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) st a : ( ( real ) ( V11() real ext-real ) number ) >= 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( real ) ( V11() real ext-real ) number ) < 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( a : ( ( real ) ( V11() real ext-real ) number ) <= n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) & n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) < 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: POWER:21
for a being ( ( real ) ( V11() real ext-real ) number )
for n being ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) st a : ( ( real ) ( V11() real ext-real ) number ) > - 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real non positive integer rational ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) & a : ( ( real ) ( V11() real ext-real ) number ) <= 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) is odd holds
( a : ( ( real ) ( V11() real ext-real ) number ) >= n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) & n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) > - 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real non positive integer rational ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ) ;

theorem :: POWER:22
for a being ( ( real ) ( V11() real ext-real ) number )
for n being ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) st a : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) - 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) <= (a : ( ( real ) ( V11() real ext-real ) number ) - 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) / n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ;

theorem :: POWER:23
for s being ( ( V21() V30( NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ) ( V21() V30( NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ) Real_Sequence)
for a being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & ( for n being ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) st n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
s : ( ( V21() V30( NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ) ( V21() V30( NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ) Real_Sequence) . n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) = n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) ) holds
( s : ( ( V21() V30( NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ) ( V21() V30( NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ) Real_Sequence) is convergent & lim s : ( ( V21() V30( NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ) ( V21() V30( NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ) Real_Sequence) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) = 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

definition
let a, b be ( ( real ) ( V11() real ext-real ) number ) ;
func a to_power b -> ( ( real ) ( V11() real ext-real ) number ) means :: POWER:def 2
it : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( V1() V48() V54() V55() ) set ) ) = a : ( ( V49() right_end ) ( V49() right_end ) set ) #R b : ( ( V21() V30(a : ( ( V49() right_end ) ( V49() right_end ) set ) ,a : ( ( V49() right_end ) ( V49() right_end ) set ) ) ) ( V21() V30(a : ( ( V49() right_end ) ( V49() right_end ) set ) ,a : ( ( V49() right_end ) ( V49() right_end ) set ) ) ) Element of K6(K7(a : ( ( V49() right_end ) ( V49() right_end ) set ) ,a : ( ( V49() right_end ) ( V49() right_end ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( real ) ( V11() real ext-real ) set ) if a : ( ( V49() right_end ) ( V49() right_end ) set ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) )
it : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( V1() V48() V54() V55() ) set ) ) = 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) if ( a : ( ( V49() right_end ) ( V49() right_end ) set ) = 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( V21() V30(a : ( ( V49() right_end ) ( V49() right_end ) set ) ,a : ( ( V49() right_end ) ( V49() right_end ) set ) ) ) ( V21() V30(a : ( ( V49() right_end ) ( V49() right_end ) set ) ,a : ( ( V49() right_end ) ( V49() right_end ) set ) ) ) Element of K6(K7(a : ( ( V49() right_end ) ( V49() right_end ) set ) ,a : ( ( V49() right_end ) ( V49() right_end ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) )
ex k being ( ( integer ) ( V11() real ext-real integer rational ) Integer) st
( k : ( ( integer ) ( V11() real ext-real integer rational ) Integer) = b : ( ( V21() V30(a : ( ( V49() right_end ) ( V49() right_end ) set ) ,a : ( ( V49() right_end ) ( V49() right_end ) set ) ) ) ( V21() V30(a : ( ( V49() right_end ) ( V49() right_end ) set ) ,a : ( ( V49() right_end ) ( V49() right_end ) set ) ) ) Element of K6(K7(a : ( ( V49() right_end ) ( V49() right_end ) set ) ,a : ( ( V49() right_end ) ( V49() right_end ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & it : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( V1() V48() V54() V55() ) set ) ) = a : ( ( V49() right_end ) ( V49() right_end ) set ) #Z k : ( ( integer ) ( V11() real ext-real integer rational ) Integer) : ( ( ) ( ) set ) ) if b : ( ( V21() V30(a : ( ( V49() right_end ) ( V49() right_end ) set ) ,a : ( ( V49() right_end ) ( V49() right_end ) set ) ) ) ( V21() V30(a : ( ( V49() right_end ) ( V49() right_end ) set ) ,a : ( ( V49() right_end ) ( V49() right_end ) set ) ) ) Element of K6(K7(a : ( ( V49() right_end ) ( V49() right_end ) set ) ,a : ( ( V49() right_end ) ( V49() right_end ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is ( ( integer ) ( V11() real ext-real integer rational ) Integer)
;
end;

definition
let a, b be ( ( ) ( V11() real ext-real ) Real) ;
:: original: to_power
redefine func a to_power b -> ( ( ) ( V11() real ext-real ) Real) ;
end;

theorem :: POWER:24
for a being ( ( real ) ( V11() real ext-real ) number ) holds a : ( ( real ) ( V11() real ext-real ) number ) to_power 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( real ) ( V11() real ext-real ) number ) = 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: POWER:25
for a being ( ( real ) ( V11() real ext-real ) number ) holds a : ( ( real ) ( V11() real ext-real ) number ) to_power 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( real ) ( V11() real ext-real ) number ) = a : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: POWER:26
for a being ( ( real ) ( V11() real ext-real ) number ) holds 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) to_power a : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) = 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: POWER:27
for a, b, c being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( V11() real ext-real ) number ) to_power (b : ( ( real ) ( V11() real ext-real ) number ) + c : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( real ) ( V11() real ext-real ) number ) = (a : ( ( real ) ( V11() real ext-real ) number ) to_power b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) * (a : ( ( real ) ( V11() real ext-real ) number ) to_power c : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: POWER:28
for a, c being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( V11() real ext-real ) number ) to_power (- c : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( V11() ) ( V11() real ext-real ) set ) : ( ( real ) ( V11() real ext-real ) number ) = 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) / (a : ( ( real ) ( V11() real ext-real ) number ) to_power c : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ;

theorem :: POWER:29
for a, b, c being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( V11() real ext-real ) number ) to_power (b : ( ( real ) ( V11() real ext-real ) number ) - c : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( real ) ( V11() real ext-real ) number ) = (a : ( ( real ) ( V11() real ext-real ) number ) to_power b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) / (a : ( ( real ) ( V11() real ext-real ) number ) to_power c : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V48() V54() V55() ) set ) ) ;

theorem :: POWER:30
for a, b, c being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(a : ( ( real ) ( V11() real ext-real ) number ) * b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) to_power c : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) = (a : ( ( real ) ( V11() real ext-real ) number ) to_power c : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) * (b : ( ( real ) ( V11() real ext-real ) number ) to_power c : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: POWER:31
for a, b, c being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(a : ( ( real ) ( V11() real ext-real ) number ) / b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V48() V54() V55() ) set ) ) to_power c : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) = (a : ( ( real ) ( V11() real ext-real ) number ) to_power c : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) / (b : ( ( real ) ( V11() real ext-real ) number ) to_power c : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V48() V54() V55() ) set ) ) ;

theorem :: POWER:32
for a, b being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) / a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) to_power b : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) = a : ( ( real ) ( V11() real ext-real ) number ) to_power (- b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( V11() ) ( V11() real ext-real ) set ) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: POWER:33
for a, b, c being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(a : ( ( real ) ( V11() real ext-real ) number ) to_power b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) to_power c : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) = a : ( ( real ) ( V11() real ext-real ) number ) to_power (b : ( ( real ) ( V11() real ext-real ) number ) * c : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: POWER:34
for a, b being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( V11() real ext-real ) number ) to_power b : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: POWER:35
for a, b being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) > 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( V11() real ext-real ) number ) to_power b : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) > 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: POWER:36
for a, b being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) > 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( V11() real ext-real ) number ) < 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( V11() real ext-real ) number ) to_power b : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) < 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: POWER:37
for a, b, c being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( real ) ( V11() real ext-real ) number ) < b : ( ( real ) ( V11() real ext-real ) number ) & c : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( V11() real ext-real ) number ) to_power c : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) < b : ( ( real ) ( V11() real ext-real ) number ) to_power c : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: POWER:38
for a, b, c being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( real ) ( V11() real ext-real ) number ) < b : ( ( real ) ( V11() real ext-real ) number ) & c : ( ( real ) ( V11() real ext-real ) number ) < 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( V11() real ext-real ) number ) to_power c : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) > b : ( ( real ) ( V11() real ext-real ) number ) to_power c : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: POWER:39
for a, b, c being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) < b : ( ( real ) ( V11() real ext-real ) number ) & c : ( ( real ) ( V11() real ext-real ) number ) > 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
c : ( ( real ) ( V11() real ext-real ) number ) to_power a : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) < c : ( ( real ) ( V11() real ext-real ) number ) to_power b : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: POWER:40
for a, b, c being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) < b : ( ( real ) ( V11() real ext-real ) number ) & c : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & c : ( ( real ) ( V11() real ext-real ) number ) < 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
c : ( ( real ) ( V11() real ext-real ) number ) to_power a : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) > c : ( ( real ) ( V11() real ext-real ) number ) to_power b : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) ;

registration
let a be ( ( real ) ( V11() real ext-real ) number ) ;
let n be ( ( natural ) ( ordinal natural V11() real ext-real non negative integer rational ) Nat) ;
identify ;
end;

theorem :: POWER:41
for a being ( ( real ) ( V11() real ext-real ) number )
for n being ( ( natural ) ( ordinal natural V11() real ext-real non negative integer rational ) Nat) holds a : ( ( real ) ( V11() real ext-real ) number ) to_power n : ( ( natural ) ( ordinal natural V11() real ext-real non negative integer rational ) Nat) : ( ( real ) ( V11() real ext-real ) number ) = a : ( ( real ) ( V11() real ext-real ) number ) |^ n : ( ( natural ) ( ordinal natural V11() real ext-real non negative integer rational ) Nat) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: POWER:42
for k being ( ( integer ) ( V11() real ext-real integer rational ) Integer) st k : ( ( integer ) ( V11() real ext-real integer rational ) Integer) <> 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) to_power k : ( ( integer ) ( V11() real ext-real integer rational ) Integer) : ( ( real ) ( V11() real ext-real ) number ) = 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: POWER:43
for a being ( ( real ) ( V11() real ext-real ) number )
for k being ( ( integer ) ( V11() real ext-real integer rational ) Integer) holds a : ( ( real ) ( V11() real ext-real ) number ) to_power k : ( ( integer ) ( V11() real ext-real integer rational ) Integer) : ( ( real ) ( V11() real ext-real ) number ) = a : ( ( real ) ( V11() real ext-real ) number ) #Z k : ( ( integer ) ( V11() real ext-real integer rational ) Integer) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: POWER:44
for a being ( ( real ) ( V11() real ext-real ) number )
for p being ( ( rational ) ( V11() real ext-real rational ) Rational) st a : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( V11() real ext-real ) number ) to_power p : ( ( rational ) ( V11() real ext-real rational ) Rational) : ( ( real ) ( V11() real ext-real ) number ) = a : ( ( real ) ( V11() real ext-real ) number ) #Q p : ( ( rational ) ( V11() real ext-real rational ) Rational) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: POWER:45
for a being ( ( real ) ( V11() real ext-real ) number )
for n being ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) st a : ( ( real ) ( V11() real ext-real ) number ) >= 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
a : ( ( real ) ( V11() real ext-real ) number ) to_power (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) / n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real non negative rational ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( real ) ( V11() real ext-real ) number ) = n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) -root a : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: POWER:46
for a being ( ( real ) ( V11() real ext-real ) number ) holds a : ( ( real ) ( V11() real ext-real ) number ) to_power 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( real ) ( V11() real ext-real ) number ) = a : ( ( real ) ( V11() real ext-real ) number ) ^2 : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: POWER:47
for a being ( ( real ) ( V11() real ext-real ) number )
for k being ( ( integer ) ( V11() real ext-real integer rational ) Integer) st k : ( ( integer ) ( V11() real ext-real integer rational ) Integer) is even holds
(- a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( V11() ) ( V11() real ext-real ) set ) to_power k : ( ( integer ) ( V11() real ext-real integer rational ) Integer) : ( ( real ) ( V11() real ext-real ) number ) = a : ( ( real ) ( V11() real ext-real ) number ) to_power k : ( ( integer ) ( V11() real ext-real integer rational ) Integer) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: POWER:48
for a being ( ( real ) ( V11() real ext-real ) number )
for k being ( ( integer ) ( V11() real ext-real integer rational ) Integer) st k : ( ( integer ) ( V11() real ext-real integer rational ) Integer) is odd holds
(- a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( V11() ) ( V11() real ext-real ) set ) to_power k : ( ( integer ) ( V11() real ext-real integer rational ) Integer) : ( ( real ) ( V11() real ext-real ) number ) = - (a : ( ( real ) ( V11() real ext-real ) number ) to_power k : ( ( integer ) ( V11() real ext-real integer rational ) Integer) ) : ( ( real ) ( V11() real ext-real ) number ) : ( ( V11() ) ( V11() real ext-real ) set ) ;

theorem :: POWER:49
for a being ( ( real ) ( V11() real ext-real ) number )
for n being ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) st - 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real non positive integer rational ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) < a : ( ( real ) ( V11() real ext-real ) number ) holds
(1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) + a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) to_power n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( real ) ( V11() real ext-real ) number ) >= 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) + (n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ;

theorem :: POWER:50
for a, c, d being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( real ) ( V11() real ext-real ) number ) <> 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & c : ( ( real ) ( V11() real ext-real ) number ) <> d : ( ( real ) ( V11() real ext-real ) number ) holds
a : ( ( real ) ( V11() real ext-real ) number ) to_power c : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) <> a : ( ( real ) ( V11() real ext-real ) number ) to_power d : ( ( real ) ( V11() real ext-real ) number ) : ( ( real ) ( V11() real ext-real ) number ) ;

definition
let a, b be ( ( real ) ( V11() real ext-real ) number ) ;
assume that
a : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) and
a : ( ( real ) ( V11() real ext-real ) number ) <> 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) and
b : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ;
func log (a,b) -> ( ( real ) ( V11() real ext-real ) number ) means :: POWER:def 3
a : ( ( V49() right_end ) ( V49() right_end ) set ) to_power it : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( V1() V48() V54() V55() ) set ) ) : ( ( real ) ( V11() real ext-real ) number ) = b : ( ( V21() V30(a : ( ( V49() right_end ) ( V49() right_end ) set ) ,a : ( ( V49() right_end ) ( V49() right_end ) set ) ) ) ( V21() V30(a : ( ( V49() right_end ) ( V49() right_end ) set ) ,a : ( ( V49() right_end ) ( V49() right_end ) set ) ) ) Element of K6(K7(a : ( ( V49() right_end ) ( V49() right_end ) set ) ,a : ( ( V49() right_end ) ( V49() right_end ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;
end;

definition
let a, b be ( ( ) ( V11() real ext-real ) Real) ;
:: original: log
redefine func log (a,b) -> ( ( ) ( V11() real ext-real ) Real) ;
end;

theorem :: POWER:51
for a being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( real ) ( V11() real ext-real ) number ) <> 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
log (a : ( ( real ) ( V11() real ext-real ) number ) ,1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( real ) ( V11() real ext-real ) number ) = 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: POWER:52
for a being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( real ) ( V11() real ext-real ) number ) <> 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
log (a : ( ( real ) ( V11() real ext-real ) number ) ,a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) = 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: POWER:53
for a, b, c being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( real ) ( V11() real ext-real ) number ) <> 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & c : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(log (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( real ) ( V11() real ext-real ) number ) + (log (a : ( ( real ) ( V11() real ext-real ) number ) ,c : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) = log (a : ( ( real ) ( V11() real ext-real ) number ) ,(b : ( ( real ) ( V11() real ext-real ) number ) * c : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: POWER:54
for a, b, c being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( real ) ( V11() real ext-real ) number ) <> 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & c : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(log (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( real ) ( V11() real ext-real ) number ) - (log (a : ( ( real ) ( V11() real ext-real ) number ) ,c : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) = log (a : ( ( real ) ( V11() real ext-real ) number ) ,(b : ( ( real ) ( V11() real ext-real ) number ) / c : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of COMPLEX : ( ( ) ( V1() V48() V54() V55() ) set ) ) ) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: POWER:55
for a, b, c being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( real ) ( V11() real ext-real ) number ) <> 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
log (a : ( ( real ) ( V11() real ext-real ) number ) ,(b : ( ( real ) ( V11() real ext-real ) number ) to_power c : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) = c : ( ( real ) ( V11() real ext-real ) number ) * (log (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: POWER:56
for a, b, c being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( real ) ( V11() real ext-real ) number ) <> 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( V11() real ext-real ) number ) <> 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & c : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds
log (a : ( ( real ) ( V11() real ext-real ) number ) ,c : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) = (log (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( real ) ( V11() real ext-real ) number ) * (log (b : ( ( real ) ( V11() real ext-real ) number ) ,c : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) ;

theorem :: POWER:57
for a, b, c being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) > 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & c : ( ( real ) ( V11() real ext-real ) number ) > b : ( ( real ) ( V11() real ext-real ) number ) holds
log (a : ( ( real ) ( V11() real ext-real ) number ) ,c : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) > log (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: POWER:58
for a, b, c being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & a : ( ( real ) ( V11() real ext-real ) number ) < 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & b : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) & c : ( ( real ) ( V11() real ext-real ) number ) > b : ( ( real ) ( V11() real ext-real ) number ) holds
log (a : ( ( real ) ( V11() real ext-real ) number ) ,c : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) < log (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: POWER:59
for s being ( ( V21() V30( NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ) ( V21() V30( NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ) Real_Sequence) st ( for n being ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds s : ( ( V21() V30( NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ) ( V21() V30( NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ) Real_Sequence) . n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) = (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) + (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) / (n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real non negative rational ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative rational ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) to_power (n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Real) ) holds
s : ( ( V21() V30( NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ) ( V21() V30( NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ) Real_Sequence) is convergent ;

definition
func number_e -> ( ( real ) ( V11() real ext-real ) number ) means :: POWER:def 4
 for s being ( ( V21() V30( NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ) ( V21() V30( NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ) Real_Sequence) st ( for n being ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) holds s : ( ( V21() V30( NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ) ( V21() V30( NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ) Real_Sequence) . n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) = (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) + (1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) / (n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real non negative rational ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ) : ( ( ) ( V1() V11() real ext-real positive non negative rational ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) to_power (n : ( ( ) ( ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Real) ) holds
it : ( ( V49() right_end ) ( V49() right_end ) set ) = lim s : ( ( V21() V30( NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ) ( V21() V30( NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ) Real_Sequence) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) ;
end;

definition
:: original: number_e
redefine func number_e -> ( ( ) ( V11() real ext-real ) Real) ;
end;

theorem :: POWER:60
2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) to_power 2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Real) = 4 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: POWER:61
2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) to_power 3 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Real) = 8 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: POWER:62
2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) to_power 4 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Real) = 16 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: POWER:63
2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) to_power 5 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Real) = 32 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: POWER:64
2 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) to_power 6 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Real) = 64 : ( ( ) ( V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( V48() V49() V50() V51() V52() V53() V54() ) Element of K6(REAL : ( ( ) ( V1() V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( ) set ) ) ) ;