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


theorem Th1: :: POWER:1
for a being Real
for n being Nat st n is even holds
(- a) |^ n = a |^ n
proof end;

theorem Th2: :: POWER:2
for a being Real
for n being Nat st n is odd holds
(- a) |^ n = - (a |^ n)
proof end;

theorem Th3: :: POWER:3
for a being Real
for n being Nat st ( a >= 0 or n is even ) holds
a |^ n >= 0
proof end;

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

:: deftheorem Def1 defines -root POWER:def 1 :
for n being natural Number
for a being Real holds
( ( a >= 0 & n >= 1 implies n -root a = n -Root a ) & ( a < 0 & n is odd implies n -root a = - (n -Root (- a)) ) );

theorem :: POWER:4
for a being Real
for n being Nat st ( ( n >= 1 & a >= 0 ) or n is odd ) holds
( (n -root a) |^ n = a & n -root (a |^ n) = a )
proof end;

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

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

theorem Th7: :: POWER:7
for a being Real
for n being Nat st a >= 0 & n >= 1 holds
n -root a >= 0
proof end;

theorem :: POWER:8
for n being Nat st n is odd holds
n -root (- 1) = - 1
proof end;

theorem :: POWER:9
for a being Real holds 1 -root a = a
proof end;

theorem Th10: :: POWER:10
for a being Real
for n being Nat st n is odd holds
n -root a = - (n -root (- a))
proof end;

theorem Th11: :: POWER:11
for a, b being Real
for n being Nat st ( ( n >= 1 & a >= 0 & b >= 0 ) or n is odd ) holds
n -root (a * b) = (n -root a) * (n -root b)
proof end;

theorem Th12: :: POWER:12
for a being Real
for n being Nat st ( ( a > 0 & n >= 1 ) or ( a <> 0 & n is odd ) ) holds
n -root (1 / a) = 1 / (n -root a)
proof end;

theorem :: POWER:13
for a, b being Real
for n being Nat st ( ( a >= 0 & b > 0 & n >= 1 ) or ( b <> 0 & n is odd ) ) holds
n -root (a / b) = (n -root a) / (n -root b)
proof end;

theorem :: POWER:14
for a being Real
for m, n being Nat st ( ( a >= 0 & n >= 1 & m >= 1 ) or ( n is odd & m is odd ) ) holds
n -root (m -root a) = (n * m) -root a
proof end;

theorem :: POWER:15
for a being Real
for m, n being Nat st ( ( a >= 0 & n >= 1 & m >= 1 ) or ( n is odd & m is odd ) ) holds
(n -root a) * (m -root a) = (n * m) -root (a |^ (n + m))
proof end;

theorem :: POWER:16
for a, b being Real
for n being Nat st a <= b & ( ( 0 <= a & n >= 1 ) or n is odd ) holds
n -root a <= n -root b
proof end;

theorem :: POWER:17
for a, b being Real
for n being Nat st a < b & ( ( a >= 0 & n >= 1 ) or n is odd ) holds
n -root a < n -root b
proof end;

theorem Th18: :: POWER:18
for a being Real
for n being Nat st a >= 1 & n >= 1 holds
( n -root a >= 1 & a >= n -root a )
proof end;

theorem :: POWER:19
for a being Real
for n being Nat st a <= - 1 & n is odd holds
( n -root a <= - 1 & a <= n -root a )
proof end;

theorem Th20: :: POWER:20
for a being Real
for n being Nat st a >= 0 & a < 1 & n >= 1 holds
( a <= n -root a & n -root a < 1 )
proof end;

theorem :: POWER:21
for a being Real
for n being Nat st a > - 1 & a <= 0 & n is odd holds
( a >= n -root a & n -root a > - 1 )
proof end;

theorem Th22: :: POWER:22
for a being Real
for n being Nat st a > 0 & n >= 1 holds
(n -root a) - 1 <= (a - 1) / n
proof end;

theorem Th23: :: POWER:23
for s being Real_Sequence
for a being Real 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;
func a to_power b -> Real 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 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 st b1 = a #R b ) & ( a = 0 & b > 0 implies ex b1 being Real st b1 = 0 ) & ( b is Integer implies ex b1 being Real ex k being Integer st
( k = b & b1 = a #Z k ) ) )
proof end;
uniqueness
for b1, b2 being Real 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 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 ) ) ) );

theorem Th24: :: POWER:24
for a being Real holds a to_power 0 = 1
proof end;

theorem :: POWER:25
for a being Real holds a to_power 1 = a
proof end;

theorem Th26: :: POWER:26
for a being Real holds 1 to_power a = 1
proof end;

theorem Th27: :: POWER:27
for a, b, c being Real st a > 0 holds
a to_power (b + c) = (a to_power b) * (a to_power c)
proof end;

theorem Th28: :: POWER:28
for a, c being Real st a > 0 holds
a to_power (- c) = 1 / (a to_power c)
proof end;

theorem Th29: :: POWER:29
for a, b, c being Real st a > 0 holds
a to_power (b - c) = (a to_power b) / (a to_power c)
proof end;

theorem :: POWER:30
for a, b, c being Real st a > 0 & b > 0 holds
(a * b) to_power c = (a to_power c) * (b to_power c)
proof end;

theorem Th31: :: POWER:31
for a, b, c being Real st a > 0 & b > 0 holds
(a / b) to_power c = (a to_power c) / (b to_power c)
proof end;

theorem Th32: :: POWER:32
for a, b being Real st a > 0 holds
(1 / a) to_power b = a to_power (- b)
proof end;

theorem Th33: :: POWER:33
for a, b, c being Real st a > 0 holds
(a to_power b) to_power c = a to_power (b * c)
proof end;

theorem Th34: :: POWER:34
for a, b being Real st a > 0 holds
a to_power b > 0
proof end;

theorem Th35: :: POWER:35
for a, b being Real st a > 1 & b > 0 holds
a to_power b > 1
proof end;

theorem Th36: :: POWER:36
for a, b being Real st a > 1 & b < 0 holds
a to_power b < 1
proof end;

theorem :: POWER:37
for a, b, c being Real st a > 0 & a < b & c > 0 holds
a to_power c < b to_power c
proof end;

theorem :: POWER:38
for a, b, c being Real st a > 0 & a < b & c < 0 holds
a to_power c > b to_power c
proof end;

theorem Th39: :: POWER:39
for a, b, c being Real st a < b & c > 1 holds
c to_power a < c to_power b
proof end;

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

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

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

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

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

theorem Th44: :: POWER:44
for a being Real
for p being Rational st a > 0 holds
a to_power p = a #Q p
proof end;

theorem Th45: :: POWER:45
for a being Real
for n being Nat st a >= 0 & n >= 1 holds
a to_power (1 / n) = n -root a
proof end;

theorem Th46: :: POWER:46
for a being Real holds a to_power 2 = a ^2
proof end;

theorem Th47: :: POWER:47
for a being Real
for k being Integer st k is even holds
(- a) to_power k = a to_power k
proof end;

theorem :: POWER:48
for a being Real
for k being Integer st k is odd holds
(- a) to_power k = - (a to_power k)
proof end;

theorem :: POWER:49
for a being Real
for n being Nat st - 1 < a holds
(1 + a) to_power n >= 1 + (n * a) by PREPOWER:16;

theorem Th50: :: POWER:50
for a, c, d being Real st a > 0 & a <> 1 & c <> d holds
a to_power c <> a to_power d
proof end;

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

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

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

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

theorem :: POWER:53
for a, b, c being Real st a > 0 & a <> 1 & b > 0 & c > 0 holds
(log (a,b)) + (log (a,c)) = log (a,(b * c))
proof end;

theorem :: POWER:54
for a, b, c being Real st a > 0 & a <> 1 & b > 0 & c > 0 holds
(log (a,b)) - (log (a,c)) = log (a,(b / c))
proof end;

theorem :: POWER:55
for a, b, c being Real st a > 0 & a <> 1 & b > 0 holds
log (a,(b to_power c)) = c * (log (a,b))
proof end;

theorem :: POWER:56
for a, b, c being Real 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:57
for a, b, c being Real st a > 1 & b > 0 & c > b holds
log (a,c) > log (a,b)
proof end;

theorem :: POWER:58
for a, b, c being Real st a > 0 & a < 1 & b > 0 & c > b holds
log (a,c) < log (a,b)
proof end;

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

theorem Th60: :: POWER:60
2 to_power 2 = 4
proof end;

theorem Th61: :: POWER:61
2 to_power 3 = 8
proof end;

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

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

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