:: POWER semantic presentation

theorem Th1: :: POWER:1

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

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

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 ;
coherence ;

end;

:: deftheorem Def1 defines -root POWER:def 1 :

definition

let n be Nat;
let a be Real;
:: original: -root
redefine func n -root a -> Real;
coherence 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 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

for n being Nat st n >= 1 holds
n -root 0 = 0

proof end;

theorem :: POWER:7

for n being Nat st n >= 1 holds
n -root 1 = 1

proof end;

theorem Th8: :: POWER:8

for a being real number
for n being Nat st a >= 0 & n >= 1 holds
n -root a >= 0

proof end;

theorem :: POWER:9

for n being Nat st ex m being Nat st n = (2 * m) + 1 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 Nat st ex m being Nat st n = (2 * m) + 1 holds
n -root a = - (n -root (- a))

proof end;

theorem Th12: :: POWER:12

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

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

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

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

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

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

for a, b being real number
for n being Nat st 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

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

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

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

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

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

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 ;
existence

proof end;

uniqueness ;

end;

:: deftheorem Def2 defines to_power POWER:def 2 :

definition

let a, b be Real;
:: original: to_power
redefine func a to_power b -> Real;
coherence 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 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 to_power c

proof end;

theorem Th44: :: POWER:44

for a, b, c being real number st a 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 0 & c < 1 holds
c to_power a > c to_power b

proof end;

theorem Th46: :: POWER:46

for a being real number
for n being Nat st a <> 0 holds
a to_power n = a |^ n

proof end;

theorem :: POWER:47

for a being real number
for n being Nat st n >= 1 holds
a to_power n = a |^ n

proof end;

theorem :: POWER:48

for a being real number
for n being Nat st a <> 0 holds
a to_power n = a |^ n by Th46;

theorem :: POWER:49

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

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

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 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 a <> 0 & ex l being Integer st k = 2 * l holds
(- a) to_power k = a to_power k

proof end;

theorem :: POWER:55

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

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

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

proof end;

uniqueness by A1, Th57;

end;

:: deftheorem Def3 defines log POWER:def 3 :

definition

let a, b be Real;
:: original: log
redefine func log a,b -> Real;
coherence 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 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

proof end;

uniqueness

proof end;

end;

:: deftheorem defines number_e POWER:def 4 :

definition

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

end;