:: Real Exponents and Logarithms
:: by Konrad Raczkowski and Andrzej N\c{e}dzusiak
::
:: Received October 1, 1990
:: Copyright (c) 1990-2011 Association of Mizar Users


begin

theorem Th1: :: POWER:1
for a being real number
for n being Element of NAT st n is even holds
(- a) |^ n = a |^ n
proof end;

theorem Th2: :: POWER:2
for a being real number
for n being Element of NAT st not n is even holds
(- a) |^ n = - (a |^ n)
proof end;

theorem Th3: :: POWER:3
for a being real number
for n being Element of NAT st ( a >= 0 or n is even ) holds
a |^ n >= 0
proof 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 & not n is even )
;
consistency
for b1 being real number st a >= 0 & n >= 1 & a < 0 & not n is even holds
( b1 = n -Root a iff b1 = - (n -Root (- a)) ) ;
coherence
( ( a >= 0 & n >= 1 implies n -Root a is real number ) & ( a < 0 & not n is even 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 & not n is even 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
canceled;

theorem :: POWER:5
for a being real number
for n being Nat st ( ( n >= 1 & a >= 0 ) or not n is even ) holds
( (n -root a) |^ n = a & n -root (a |^ n) = a )
proof end;

theorem Th6: :: POWER:6
for n being Nat st n >= 1 holds
n -root 0 = 0
proof end;

theorem :: POWER:7
for n being Element of NAT st n >= 1 holds
n -root 1 = 1
proof end;

theorem Th8: :: POWER:8
for a being real number
for n being Element of NAT st a >= 0 & n >= 1 holds
n -root a >= 0
proof end;

theorem :: POWER:9
for n being Element of NAT st not n is even holds
n -root (- 1) = - 1
proof end;

theorem :: POWER:10
for a being real number holds 1 -root a = a
proof end;

theorem Th11: :: POWER:11
for a being real number
for n being Element of NAT st not n is even holds
n -root a = - (n -root (- a))
proof end;

theorem Th12: :: POWER:12
for a, b being real number
for n being Element of NAT st ( ( n >= 1 & a >= 0 & b >= 0 ) or not n is even ) holds
n -root (a * b) = (n -root a) * (n -root b)
proof end;

theorem Th13: :: POWER:13
for a being real number
for n being Element of NAT st ( ( a > 0 & n >= 1 ) or ( a <> 0 & not n is even ) ) holds
n -root (1 / a) = 1 / (n -root a)
proof end;

theorem :: POWER:14
for a, b being real number
for n being Element of NAT st ( ( a >= 0 & b > 0 & n >= 1 ) or ( b <> 0 & not n is even ) ) holds
n -root (a / b) = (n -root a) / (n -root b)
proof end;

theorem :: POWER:15
for a being real number
for n, m being Element of NAT st ( ( a >= 0 & n >= 1 & m >= 1 ) or ( not n is even & not m is even ) ) holds
n -root (m -root a) = (n * m) -root a
proof end;

theorem :: POWER:16
for a being real number
for n, m being Element of NAT st ( ( a >= 0 & n >= 1 & m >= 1 ) or ( not n is even & not m is even ) ) holds
(n -root a) * (m -root a) = (n * m) -root (a |^ (n + m))
proof end;

theorem :: POWER:17
for a, b being real number
for n being Element of NAT st a <= b & ( ( 0 <= a & n >= 1 ) or not n is even ) holds
n -root a <= n -root b
proof end;

theorem :: POWER:18
for a, b being real number
for n being Element of NAT st a < b & ( ( a >= 0 & n >= 1 ) or not n is even ) holds
n -root a < n -root b
proof end;

theorem Th19: :: POWER:19
for a being real number
for n being Element of NAT st a >= 1 & n >= 1 holds
( n -root a >= 1 & a >= n -root a )
proof end;

theorem :: POWER:20
for a being real number
for n being Element of NAT st a <= - 1 & not n is even holds
( n -root a <= - 1 & a <= n -root a )
proof end;

theorem Th21: :: POWER:21
for a being real number
for n being Element of NAT st a >= 0 & a < 1 & n >= 1 holds
( a <= n -root a & n -root a < 1 )
proof end;

theorem :: POWER:22
for a being real number
for n being Element of NAT st a > - 1 & a <= 0 & not n is even holds
( a >= n -root a & n -root a > - 1 )
proof end;

theorem Th23: :: POWER:23
for a being real number
for n being Element of NAT st a > 0 & n >= 1 holds
(n -root a) - 1 <= (a - 1) / n
proof end;

theorem Th24: :: POWER:24
for s being Real_Sequence
for a being real number st a > 0 & ( for n being Element of NAT st n >= 1 holds
s . n = n -root a ) holds
( s is convergent & lim s = 1 )
proof 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 )
ex k being Integer st
( k = b & it = a #Z k ) if b is Integer
;
consistency
for b1 being real number holds
( ( a > 0 & a = 0 & b > 0 implies ( b1 = a #R b iff b1 = 0 ) ) & ( a > 0 & b is Integer implies ( b1 = a #R b iff ex k being Integer st
( k = b & b1 = a #Z k ) ) ) & ( a = 0 & b > 0 & b is Integer implies ( b1 = 0 iff ex k being Integer st
( k = b & b1 = a #Z k ) ) ) )
proof end;
existence
( ( a > 0 implies ex b1 being real number st b1 = a #R b ) & ( a = 0 & b > 0 implies ex b1 being real number st b1 = 0 ) & ( b is Integer implies ex b1 being real number ex k being Integer st
( k = b & b1 = a #Z k ) ) )
proof end;
uniqueness
for b1, b2 being real number holds
( ( a > 0 & b1 = a #R b & b2 = a #R b implies b1 = b2 ) & ( a = 0 & b > 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) & ( b is Integer & ex k being Integer st
( k = b & b1 = a #Z k ) & ex k being Integer st
( k = b & b2 = a #Z k ) implies b1 = b2 ) ) ;
end;

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

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

theorem :: POWER:25
canceled;

theorem :: POWER:26
canceled;

theorem :: POWER:27
canceled;

theorem :: POWER:28
canceled;

theorem Th29: :: POWER:29
for a being real number holds a to_power 0 = 1
proof end;

theorem Th30: :: POWER:30
for a being real number holds a to_power 1 = a
proof end;

theorem Th31: :: POWER:31
for a being real number holds 1 to_power a = 1
proof end;

theorem Th32: :: POWER:32
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
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
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
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
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
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
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
for a, b being real number st a > 0 holds
a to_power b > 0
proof end;

theorem Th40: :: POWER:40
for a, b being real number st a > 1 & b > 0 holds
a to_power b > 1
proof end;

theorem Th41: :: POWER:41
for a, b being real number st a > 1 & b < 0 holds
a to_power b < 1
proof end;

theorem :: POWER:42
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
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
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
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;

registration
let a be real number ;
let n be Nat;
identify a to_power n with a |^ n;
compatibility
a to_power n = a |^ n
proof end;
end;

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

theorem :: POWER:47
canceled;

theorem :: POWER:48
canceled;

theorem Th49: :: POWER:49
for k being Integer st k <> 0 holds
0 to_power k = 0
proof end;

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

theorem Th51: :: POWER:51
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
for a being real number
for n being Element of NAT st a >= 0 & n >= 1 holds
a to_power (1 / n) = n -root a
proof end;

theorem Th53: :: POWER:53
for a being real number holds a to_power 2 = a ^2
proof end;

theorem Th54: :: POWER:54
for a being real number
for k being Integer st k is even holds
(- a) to_power k = a to_power k
proof end;

theorem :: POWER:55
for a being real number
for k being Integer st not k is even holds
(- a) to_power k = - (a to_power k)
proof end;

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

theorem Th57: :: POWER:57
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 and
A2: a <> 1 and
A3: b > 0 ;
func log (a,b) -> real number means :Def3: :: POWER:def 3
a to_power it = b;
existence
ex b1 being real number st a to_power b1 = b
proof end;
uniqueness
for b1, b2 being real number st a to_power b1 = b & a to_power b2 = b holds
b1 = b2 by A1, A2, 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
canceled;

theorem :: POWER:59
for a being real number st a > 0 & a <> 1 holds
log (a,1) = 0
proof end;

theorem :: POWER:60
for a being real number st a > 0 & a <> 1 holds
log (a,a) = 1
proof end;

theorem :: POWER:61
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
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
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
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
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
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
for s being Real_Sequence st ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds
s is convergent
proof end;

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

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

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

theorem Th68: :: POWER:68
2 to_power 2 = 4
proof end;

theorem Th69: :: POWER:69
2 to_power 3 = 8
proof end;

theorem :: POWER:70
2 to_power 4 = 16
proof end;

theorem :: POWER:71
2 to_power 5 = 32
proof end;

theorem :: POWER:72
2 to_power 6 = 64
proof end;