:: POWER semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: POWER:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being Nat st ex m being Nat st n = 2 * m holds
(- a) |^ n = a |^ n
proof end;

theorem Th2: :: POWER:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being Nat st ex m being Nat st n = (2 * m) + 1 holds
(- a) |^ n = - (a |^ n)
proof end;

theorem Th3: :: POWER:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being Nat st ( a >= 0 or ex m being Nat st n = 2 * m ) holds
a |^ n >= 0
proof end;

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

:: deftheorem Def1 defines -root POWER:def 1 :
for n being Nat
for a being real number holds
( ( a >= 0 & n >= 1 implies n -root a = n -Root a ) & ( a < 0 & ex m being Nat st n = (2 * m) + 1 implies n -root a = - (n -Root (- a)) ) );

definition
let n be Nat;
let a be Real;
:: original: -root
redefine func n -root a -> Real;
coherence
n -root a is Real
by XREAL_0:def 1;
end;

theorem :: POWER:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: POWER:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being Nat st ( ( n >= 1 & a >= 0 ) or ex m being Nat st n = (2 * m) + 1 ) holds
( (n -root a) |^ n = a & n -root (a |^ n) = a )
proof end;

theorem Th6: :: POWER:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat st n >= 1 holds
n -root 0 = 0
proof end;

theorem :: POWER:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat st n >= 1 holds
n -root 1 = 1
proof end;

theorem Th8: :: POWER:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being Nat st a >= 0 & n >= 1 holds
n -root a >= 0
proof end;

theorem :: POWER:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat st ex m being Nat st n = (2 * m) + 1 holds
n -root (- 1) = - 1
proof end;

theorem :: POWER:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number holds 1 -root a = a
proof end;

theorem Th11: :: POWER:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being Nat st ex m being Nat st n = (2 * m) + 1 holds
n -root a = - (n -root (- a))
proof end;

theorem Th12: :: POWER:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number
for n being Nat st ( ( n >= 1 & a >= 0 & b >= 0 ) or ex m being Nat st n = (2 * m) + 1 ) holds
n -root (a * b) = (n -root a) * (n -root b)
proof end;

theorem Th13: :: POWER:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being Nat st ( ( a > 0 & n >= 1 ) or ( a <> 0 & ex m being Nat st n = (2 * m) + 1 ) ) holds
n -root (1 / a) = 1 / (n -root a)
proof end;

theorem :: POWER:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number
for n being Nat st ( ( a >= 0 & b > 0 & n >= 1 ) or ( b <> 0 & ex m being Nat st n = (2 * m) + 1 ) ) holds
n -root (a / b) = (n -root a) / (n -root b)
proof end;

theorem :: POWER:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n, m being Nat st ( ( a >= 0 & n >= 1 & m >= 1 ) or ex m1, m2 being Nat st
( n = (2 * m1) + 1 & m = (2 * m2) + 1 ) ) holds
n -root (m -root a) = (n * m) -root a
proof end;

theorem :: POWER:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n, m being Nat st ( ( a >= 0 & n >= 1 & m >= 1 ) or ex m1, m2 being Nat st
( n = (2 * m1) + 1 & m = (2 * m2) + 1 ) ) holds
(n -root a) * (m -root a) = (n * m) -root (a |^ (n + m))
proof end;

theorem :: POWER:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number
for n being Nat st a <= b & ( ( 0 <= a & n >= 1 ) or ex m being Nat st n = (2 * m) + 1 ) holds
n -root a <= n -root b
proof end;

theorem :: POWER:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number
for n being Nat st a < b & ( ( a >= 0 & n >= 1 ) or ex m being Nat st n = (2 * m) + 1 ) holds
n -root a < n -root b
proof end;

theorem Th19: :: POWER:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being Nat st a >= 1 & n >= 1 holds
( n -root a >= 1 & a >= n -root a )
proof end;

theorem :: POWER:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being Nat st a <= - 1 & ex m being Nat st n = (2 * m) + 1 holds
( n -root a <= - 1 & a <= n -root a )
proof end;

theorem Th21: :: POWER:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being Nat st a >= 0 & a < 1 & n >= 1 holds
( a <= n -root a & n -root a < 1 )
proof end;

theorem :: POWER:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being Nat st a > - 1 & a <= 0 & ex m being Nat st n = (2 * m) + 1 holds
( a >= n -root a & n -root a > - 1 )
proof end;

theorem Th23: :: POWER:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being Nat st a > 0 & n >= 1 holds
(n -root a) - 1 <= (a - 1) / n
proof end;

theorem Th24: :: POWER:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being Real_Sequence
for a being real number st a > 0 & ( for n being Nat st n >= 1 holds
s . n = n -root a ) holds
( s is convergent & lim s = 1 )
proof end;

definition
let a, b be real number ;
func a to_power b -> real number means :Def2: :: POWER:def 2
it = a #R b if a > 0
it = 0 if ( a = 0 & b > 0 )
it = 1 if ( a = 0 & b = 0 )
ex k being Integer st
( k = b & it = a #Z k ) if ( a < 0 & b is Integer )
;
consistency
for b1 being real number holds
( ( a > 0 & a = 0 & b > 0 implies ( b1 = a #R b iff b1 = 0 ) ) & ( a > 0 & a = 0 & b = 0 implies ( b1 = a #R b iff b1 = 1 ) ) & ( a > 0 & a < 0 & b is Integer implies ( b1 = a #R b iff ex k being Integer st
( k = b & b1 = a #Z k ) ) ) & ( a = 0 & b > 0 & a = 0 & b = 0 implies ( b1 = 0 iff b1 = 1 ) ) & ( a = 0 & b > 0 & a < 0 & b is Integer implies ( b1 = 0 iff ex k being Integer st
( k = b & b1 = a #Z k ) ) ) & ( a = 0 & b = 0 & a < 0 & b is Integer implies ( b1 = 1 iff ex k being Integer st
( k = b & b1 = a #Z k ) ) ) )
;
existence
( ( a > 0 implies ex b1 being real number st b1 = a #R b ) & ( a = 0 & b > 0 implies ex b1 being real number st b1 = 0 ) & ( a = 0 & b = 0 implies ex b1 being real number st b1 = 1 ) & ( a < 0 & b is Integer implies ex b1 being real number ex k being Integer st
( k = b & b1 = a #Z k ) ) )
proof end;
uniqueness
for b1, b2 being real number holds
( ( a > 0 & b1 = a #R b & b2 = a #R b implies b1 = b2 ) & ( a = 0 & b > 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) & ( a = 0 & b = 0 & b1 = 1 & b2 = 1 implies b1 = b2 ) & ( a < 0 & b is Integer & ex k being Integer st
( k = b & b1 = a #Z k ) & ex k being Integer st
( k = b & b2 = a #Z k ) implies b1 = b2 ) )
;
end;

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

definition
let a, b be Real;
:: original: to_power
redefine func a to_power b -> Real;
coherence
a to_power b is Real
by XREAL_0:def 1;
end;

theorem :: POWER:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: POWER:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: POWER:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: POWER:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th29: :: POWER:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number holds a to_power 0 = 1
proof end;

theorem Th30: :: POWER:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number holds a to_power 1 = a
proof end;

theorem Th31: :: POWER:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number holds 1 to_power a = 1
proof end;

theorem Th32: :: POWER:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a > 0 holds
a to_power (b + c) = (a to_power b) * (a to_power c)
proof end;

theorem Th33: :: POWER:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, c being real number st a > 0 holds
a to_power (- c) = 1 / (a to_power c)
proof end;

theorem Th34: :: POWER:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a > 0 holds
a to_power (b - c) = (a to_power b) / (a to_power c)
proof end;

theorem :: POWER:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a > 0 & b > 0 holds
(a * b) to_power c = (a to_power c) * (b to_power c)
proof end;

theorem Th36: :: POWER:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a > 0 & b > 0 holds
(a / b) to_power c = (a to_power c) / (b to_power c)
proof end;

theorem Th37: :: POWER:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a > 0 holds
(1 / a) to_power b = a to_power (- b)
proof end;

theorem Th38: :: POWER:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a > 0 holds
(a to_power b) to_power c = a to_power (b * c)
proof end;

theorem Th39: :: POWER:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a > 0 holds
a to_power b > 0
proof end;

theorem Th40: :: POWER:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a > 1 & b > 0 holds
a to_power b > 1
proof end;

theorem Th41: :: POWER:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a > 1 & b < 0 holds
a to_power b < 1
proof end;

theorem :: POWER:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a > 0 & a < b & c > 0 holds
a to_power c < b to_power c
proof end;

theorem :: POWER:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a > 0 & a < b & c < 0 holds
a to_power c > b to_power c
proof end;

theorem Th44: :: POWER:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a < b & c > 1 holds
c to_power a < c to_power b
proof end;

theorem Th45: :: POWER:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a < b & c > 0 & c < 1 holds
c to_power a > c to_power b
proof end;

theorem Th46: :: POWER:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being Nat st a <> 0 holds
a to_power n = a |^ n
proof end;

theorem :: POWER:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being Nat st n >= 1 holds
a to_power n = a |^ n
proof end;

theorem :: POWER:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being Nat st a <> 0 holds
a to_power n = a |^ n by Th46;

theorem :: POWER:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being Nat st n >= 1 holds
a to_power n = a |^ n
proof end;

theorem Th50: :: POWER:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for k being Integer st a <> 0 holds
a to_power k = a #Z k
proof end;

theorem Th51: :: POWER:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for p being Rational st a > 0 holds
a to_power p = a #Q p
proof end;

theorem Th52: :: POWER:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being Nat st a >= 0 & n >= 1 holds
a to_power (1 / n) = n -root a
proof end;

theorem Th53: :: POWER:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number holds a to_power 2 = a ^2
proof end;

theorem Th54: :: POWER:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for k being Integer st a <> 0 & ex l being Integer st k = 2 * l holds
(- a) to_power k = a to_power k
proof end;

theorem :: POWER:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for k being Integer st a <> 0 & ex l being Integer st k = (2 * l) + 1 holds
(- a) to_power k = - (a to_power k)
proof end;

theorem Th56: :: POWER:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being Nat st - 1 < a holds
(1 + a) to_power n >= 1 + (n * a)
proof end;

theorem Th57: :: POWER:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, c, d being real number st a > 0 & a <> 1 & c <> d holds
a to_power c <> a to_power d
proof end;

definition
let a, b be real number ;
assume that
A1: ( a > 0 & a <> 1 ) and
A2: b > 0 ;
func log a,b -> real number means :Def3: :: POWER:def 3
a to_power it = b;
existence
ex b1 being real number st a to_power b1 = b
proof end;
uniqueness
for b1, b2 being real number st a to_power b1 = b & a to_power b2 = b holds
b1 = b2
by A1, Th57;
end;

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

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

theorem :: POWER:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: POWER:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number st a > 0 & a <> 1 holds
log a,1 = 0
proof end;

theorem :: POWER:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number st a > 0 & a <> 1 holds
log a,a = 1
proof end;

theorem :: POWER:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a > 0 & a <> 1 & b > 0 & c > 0 holds
(log a,b) + (log a,c) = log a,(b * c)
proof end;

theorem :: POWER:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a > 0 & a <> 1 & b > 0 & c > 0 holds
(log a,b) - (log a,c) = log a,(b / c)
proof end;

theorem :: POWER:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a > 0 & a <> 1 & b > 0 holds
log a,(b to_power c) = c * (log a,b)
proof end;

theorem :: POWER:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a > 0 & a <> 1 & b > 0 & b <> 1 & c > 0 holds
log a,c = (log a,b) * (log b,c)
proof end;

theorem :: POWER:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a > 1 & b > 0 & c > b holds
log a,c > log a,b
proof end;

theorem :: POWER:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a > 0 & a < 1 & b > 0 & c > b holds
log a,c < log a,b
proof end;

theorem :: POWER:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being Real_Sequence st ( for n being Nat holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds
s is convergent
proof end;

definition
func number_e -> real number means :: POWER:def 4
for s being Real_Sequence st ( for n being Nat holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds
it = lim s;
existence
ex b1 being real number st
for s being Real_Sequence st ( for n being Nat holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds
b1 = lim s
proof end;
uniqueness
for b1, b2 being real number st ( for s being Real_Sequence st ( for n being Nat holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds
b1 = lim s ) & ( for s being Real_Sequence st ( for n being Nat holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds
b2 = lim s ) holds
b1 = b2
proof end;
end;

:: deftheorem defines number_e POWER:def 4 :
for b1 being real number holds
( b1 = number_e iff for s being Real_Sequence st ( for n being Nat holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds
b1 = lim s );

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