:: 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 b₁ being Real st a >= 0 & n >= 1 & a < 0 & n is odd holds
( b₁ = n -Root a iff b₁ = - (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 b₁ being Real holds
( ( a > 0 & a = 0 & b > 0 implies ( b₁ = a #R b iff b₁ = 0 ) ) & ( a > 0 & b is Integer implies ( b₁ = a #R b iff ex k being Integer st
( k = b & b₁ = a #Z k ) ) ) & ( a = 0 & b > 0 & b is Integer implies ( b₁ = 0 iff ex k being Integer st
( k = b & b₁ = a #Z k ) ) ) )

proof end;

existence
( ( a > 0 implies ex b₁ being Real st b₁ = a #R b ) & ( a = 0 & b > 0 implies ex b₁ being Real st b₁ = 0 ) & ( b is Integer implies ex b₁ being Real ex k being Integer st
( k = b & b₁ = a #Z k ) ) )

proof end;

uniqueness
for b₁, b₂ being Real holds
( ( a > 0 & b₁ = a #R b & b₂ = a #R b implies b₁ = b₂ ) & ( a = 0 & b > 0 & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) & ( b is Integer & ex k being Integer st
( k = b & b₁ = a #Z k ) & ex k being Integer st
( k = b & b₂ = a #Z k ) implies b₁ = b₂ ) ) ;

end;

:: deftheorem Def2 defines to_power POWER:def 2 :
for a, b, b₃ being Real holds
( ( a > 0 implies ( b₃ = a to_power b iff b₃ = a #R b ) ) & ( a = 0 & b > 0 implies ( b₃ = a to_power b iff b₃ = 0 ) ) & ( b is Integer implies ( b₃ = a to_power b iff ex k being Integer st
( k = b & b₃ = 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 b₁ being Real st a to_power b₁ = b

proof end;

uniqueness
for b₁, b₂ being Real st a to_power b₁ = b & a to_power b₂ = b holds
b₁ = b₂ 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 b₃ being Real holds
( b₃ = log (a,b) iff a to_power b₃ = 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 b₁ 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
b₁ = lim s

proof end;

uniqueness
for b₁, b₂ 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
b₁ = lim s ) & ( for s being Real_Sequence st ( for n being Nat holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds
b₂ = lim s ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines number_e POWER:def 4 :
for b₁ being Real holds
( b₁ = 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
b₁ = 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;