:: POWER semantic presentation

theorem Th1: :: POWER:1

for b₁ being real number
for b₂ being Nat st ex b₃ being Nat st b₂ = 2 * b₃ holds
(- b₁) |^ b₂ = b₁ |^ b₂

proof end;

theorem Th2: :: POWER:2

for b₁ being real number
for b₂ being Nat st ex b₃ being Nat st b₂ = (2 * b₃) + 1 holds
(- b₁) |^ b₂ = - (b₁ |^ b₂)

proof end;

theorem Th3: :: POWER:3

for b₁ being real number
for b₂ being Nat st ( b₁ >= 0 or ex b₃ being Nat st b₂ = 2 * b₃ ) holds
b₁ |^ b₂ >= 0

proof end;

definition

let c₁ be Nat;
let c₂ be real number ;
func c₁ -root c₂ -> real number equals :Def1: :: POWER:def 1
a₁ -Root a₂ if ( a₂ >= 0 & a₁ >= 1 )
- (a₁ -Root (- a₂)) if ( a₂ < 0 & ex b₁ being Nat st a₁ = (2 * b₁) + 1 )
;
consistency ;
coherence ;

end;

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

definition

let c₁ be Nat;
let c₂ be Real;
redefine func -root as c₁ -root c₂ -> Real;
coherence by XREAL_0:def 1;

end;

theorem Th4: :: POWER:4

canceled;

theorem Th5: :: POWER:5

for b₁ being real number
for b₂ being Nat st ( ( b₂ >= 1 & b₁ >= 0 ) or ex b₃ being Nat st b₂ = (2 * b₃) + 1 ) holds
( (b₂ -root b₁) |^ b₂ = b₁ & b₂ -root (b₁ |^ b₂) = b₁ )

proof end;

theorem Th6: :: POWER:6

for b₁ being Nat st b₁ >= 1 holds
b₁ -root 0 = 0

proof end;

theorem Th7: :: POWER:7

for b₁ being Nat st b₁ >= 1 holds
b₁ -root 1 = 1

proof end;

theorem Th8: :: POWER:8

for b₁ being real number
for b₂ being Nat st b₁ >= 0 & b₂ >= 1 holds
b₂ -root b₁ >= 0

proof end;

theorem Th9: :: POWER:9

for b₁ being Nat st ex b₂ being Nat st b₁ = (2 * b₂) + 1 holds
b₁ -root (- 1) = - 1

proof end;

theorem Th10: :: POWER:10

for b₁ being real number holds 1 -root b₁ = b₁

proof end;

theorem Th11: :: POWER:11

for b₁ being real number
for b₂ being Nat st ex b₃ being Nat st b₂ = (2 * b₃) + 1 holds
b₂ -root b₁ = - (b₂ -root (- b₁))

proof end;

theorem Th12: :: POWER:12

for b₁, b₂ being real number
for b₃ being Nat st ( ( b₃ >= 1 & b₁ >= 0 & b₂ >= 0 ) or ex b₄ being Nat st b₃ = (2 * b₄) + 1 ) holds
b₃ -root (b₁ * b₂) = (b₃ -root b₁) * (b₃ -root b₂)

proof end;

theorem Th13: :: POWER:13

for b₁ being real number
for b₂ being Nat st ( ( b₁ > 0 & b₂ >= 1 ) or ( b₁ <> 0 & ex b₃ being Nat st b₂ = (2 * b₃) + 1 ) ) holds
b₂ -root (1 / b₁) = 1 / (b₂ -root b₁)

proof end;

theorem Th14: :: POWER:14

for b₁, b₂ being real number
for b₃ being Nat st ( ( b₁ >= 0 & b₂ > 0 & b₃ >= 1 ) or ( b₂ <> 0 & ex b₄ being Nat st b₃ = (2 * b₄) + 1 ) ) holds
b₃ -root (b₁ / b₂) = (b₃ -root b₁) / (b₃ -root b₂)

proof end;

theorem Th15: :: POWER:15

for b₁ being real number
for b₂, b₃ being Nat st ( ( b₁ >= 0 & b₂ >= 1 & b₃ >= 1 ) or ex b₄, b₅ being Nat st
( b₂ = (2 * b₄) + 1 & b₃ = (2 * b₅) + 1 ) ) holds
b₂ -root (b₃ -root b₁) = (b₂ * b₃) -root b₁

proof end;

theorem Th16: :: POWER:16

for b₁ being real number
for b₂, b₃ being Nat st ( ( b₁ >= 0 & b₂ >= 1 & b₃ >= 1 ) or ex b₄, b₅ being Nat st
( b₂ = (2 * b₄) + 1 & b₃ = (2 * b₅) + 1 ) ) holds
(b₂ -root b₁) * (b₃ -root b₁) = (b₂ * b₃) -root (b₁ |^ (b₂ + b₃))

proof end;

theorem Th17: :: POWER:17

for b₁, b₂ being real number
for b₃ being Nat st b₁ <= b₂ & ( ( 0 <= b₁ & b₃ >= 1 ) or ex b₄ being Nat st b₃ = (2 * b₄) + 1 ) holds
b₃ -root b₁ <= b₃ -root b₂

proof end;

theorem Th18: :: POWER:18

for b₁, b₂ being real number
for b₃ being Nat st b₁ < b₂ & ( ( b₁ >= 0 & b₃ >= 1 ) or ex b₄ being Nat st b₃ = (2 * b₄) + 1 ) holds
b₃ -root b₁ < b₃ -root b₂

proof end;

theorem Th19: :: POWER:19

for b₁ being real number
for b₂ being Nat st b₁ >= 1 & b₂ >= 1 holds
( b₂ -root b₁ >= 1 & b₁ >= b₂ -root b₁ )

proof end;

theorem Th20: :: POWER:20

for b₁ being real number
for b₂ being Nat st b₁ <= - 1 & ex b₃ being Nat st b₂ = (2 * b₃) + 1 holds
( b₂ -root b₁ <= - 1 & b₁ <= b₂ -root b₁ )

proof end;

theorem Th21: :: POWER:21

for b₁ being real number
for b₂ being Nat st b₁ >= 0 & b₁ < 1 & b₂ >= 1 holds
( b₁ <= b₂ -root b₁ & b₂ -root b₁ < 1 )

proof end;

theorem Th22: :: POWER:22

for b₁ being real number
for b₂ being Nat st b₁ > - 1 & b₁ <= 0 & ex b₃ being Nat st b₂ = (2 * b₃) + 1 holds
( b₁ >= b₂ -root b₁ & b₂ -root b₁ > - 1 )

proof end;

theorem Th23: :: POWER:23

for b₁ being real number
for b₂ being Nat st b₁ > 0 & b₂ >= 1 holds
(b₂ -root b₁) - 1 <= (b₁ - 1) / b₂

proof end;

theorem Th24: :: POWER:24

for b₁ being Real_Sequence
for b₂ being real number st b₂ > 0 & ( for b₃ being Nat st b₃ >= 1 holds
b₁ . b₃ = b₃ -root b₂ ) holds
( b₁ is convergent & lim b₁ = 1 )

proof end;

definition

let c₁, c₂ be real number ;
func c₁ to_power c₂ -> real number means :Def2: :: POWER:def 2
a₃ = a₁ #R a₂ if a₁ > 0
a₃ = 0 if ( a₁ = 0 & a₂ > 0 )
a₃ = 1 if ( a₁ = 0 & a₂ = 0 )
ex b₁ being Integer st
( b₁ = a₂ & a₃ = a₁ #Z b₁ ) if ( a₁ < 0 & a₂ is Integer )
;
consistency ;
existence

proof end;

uniqueness ;

end;

:: deftheorem Def2 defines to_power POWER:def 2 :

definition

let c₁, c₂ be Real;
redefine func to_power as c₁ to_power c₂ -> Real;
coherence by XREAL_0:def 1;

end;

theorem Th25: :: POWER:25

canceled;

theorem Th26: :: POWER:26

canceled;

theorem Th27: :: POWER:27

canceled;

theorem Th28: :: POWER:28

canceled;

theorem Th29: :: POWER:29

for b₁ being real number holds b₁ to_power 0 = 1

proof end;

theorem Th30: :: POWER:30

for b₁ being real number holds b₁ to_power 1 = b₁

proof end;

theorem Th31: :: POWER:31

for b₁ being real number holds 1 to_power b₁ = 1

proof end;

theorem Th32: :: POWER:32

for b₁, b₂, b₃ being real number st b₁ > 0 holds
b₁ to_power (b₂ + b₃) = (b₁ to_power b₂) * (b₁ to_power b₃)

proof end;

theorem Th33: :: POWER:33

for b₁, b₂ being real number st b₁ > 0 holds
b₁ to_power (- b₂) = 1 / (b₁ to_power b₂)

proof end;

theorem Th34: :: POWER:34

for b₁, b₂, b₃ being real number st b₁ > 0 holds
b₁ to_power (b₂ - b₃) = (b₁ to_power b₂) / (b₁ to_power b₃)

proof end;

theorem Th35: :: POWER:35

for b₁, b₂, b₃ being real number st b₁ > 0 & b₂ > 0 holds
(b₁ * b₂) to_power b₃ = (b₁ to_power b₃) * (b₂ to_power b₃)

proof end;

theorem Th36: :: POWER:36

for b₁, b₂, b₃ being real number st b₁ > 0 & b₂ > 0 holds
(b₁ / b₂) to_power b₃ = (b₁ to_power b₃) / (b₂ to_power b₃)

proof end;

theorem Th37: :: POWER:37

for b₁, b₂ being real number st b₁ > 0 holds
(1 / b₁) to_power b₂ = b₁ to_power (- b₂)

proof end;

theorem Th38: :: POWER:38

for b₁, b₂, b₃ being real number st b₁ > 0 holds
(b₁ to_power b₂) to_power b₃ = b₁ to_power (b₂ * b₃)

proof end;

theorem Th39: :: POWER:39

for b₁, b₂ being real number st b₁ > 0 holds
b₁ to_power b₂ > 0

proof end;

theorem Th40: :: POWER:40

for b₁, b₂ being real number st b₁ > 1 & b₂ > 0 holds
b₁ to_power b₂ > 1

proof end;

theorem Th41: :: POWER:41

for b₁, b₂ being real number st b₁ > 1 & b₂ < 0 holds
b₁ to_power b₂ < 1

proof end;

theorem Th42: :: POWER:42

for b₁, b₂, b₃ being real number st b₁ > 0 & b₁ < b₂ & b₃ > 0 holds
b₁ to_power b₃ < b₂ to_power b₃

proof end;

theorem Th43: :: POWER:43

for b₁, b₂, b₃ being real number st b₁ > 0 & b₁ < b₂ & b₃ < 0 holds
b₁ to_power b₃ > b₂ to_power b₃

proof end;

theorem Th44: :: POWER:44

for b₁, b₂, b₃ being real number st b₁ < b₂ & b₃ > 1 holds
b₃ to_power b₁ < b₃ to_power b₂

proof end;

theorem Th45: :: POWER:45

for b₁, b₂, b₃ being real number st b₁ < b₂ & b₃ > 0 & b₃ < 1 holds
b₃ to_power b₁ > b₃ to_power b₂

proof end;

theorem Th46: :: POWER:46

for b₁ being real number
for b₂ being Nat st b₁ <> 0 holds
b₁ to_power b₂ = b₁ |^ b₂

proof end;

theorem Th47: :: POWER:47

for b₁ being real number
for b₂ being Nat st b₂ >= 1 holds
b₁ to_power b₂ = b₁ |^ b₂

proof end;

theorem Th48: :: POWER:48

for b₁ being real number
for b₂ being Nat st b₁ <> 0 holds
b₁ to_power b₂ = b₁ |^ b₂ by Th46;

theorem Th49: :: POWER:49

for b₁ being real number
for b₂ being Nat st b₂ >= 1 holds
b₁ to_power b₂ = b₁ |^ b₂

proof end;

theorem Th50: :: POWER:50

for b₁ being real number
for b₂ being Integer st b₁ <> 0 holds
b₁ to_power b₂ = b₁ #Z b₂

proof end;

theorem Th51: :: POWER:51

for b₁ being real number
for b₂ being Rational st b₁ > 0 holds
b₁ to_power b₂ = b₁ #Q b₂

proof end;

theorem Th52: :: POWER:52

for b₁ being real number
for b₂ being Nat st b₁ >= 0 & b₂ >= 1 holds
b₁ to_power (1 / b₂) = b₂ -root b₁

proof end;

theorem Th53: :: POWER:53

for b₁ being real number holds b₁ to_power 2 = b₁ ^2

proof end;

theorem Th54: :: POWER:54

for b₁ being real number
for b₂ being Integer st b₁ <> 0 & ex b₃ being Integer st b₂ = 2 * b₃ holds
(- b₁) to_power b₂ = b₁ to_power b₂

proof end;

theorem Th55: :: POWER:55

for b₁ being real number
for b₂ being Integer st b₁ <> 0 & ex b₃ being Integer st b₂ = (2 * b₃) + 1 holds
(- b₁) to_power b₂ = - (b₁ to_power b₂)

proof end;

theorem Th56: :: POWER:56

for b₁ being real number
for b₂ being Nat st - 1 < b₁ holds
(1 + b₁) to_power b₂ >= 1 + (b₂ * b₁)

proof end;

theorem Th57: :: POWER:57

for b₁, b₂, b₃ being real number st b₁ > 0 & b₁ <> 1 & b₂ <> b₃ holds
b₁ to_power b₂ <> b₁ to_power b₃

proof end;

definition

let c₁, c₂ be real number ;
assume that
E37: ( c₁ > 0 & c₁ <> 1 ) and
E38: c₂ > 0 ;
func log c₁,c₂ -> real number means :Def3: :: POWER:def 3
a₁ to_power a₃ = a₂;
existence

proof end;

uniqueness by E37, Th57;

end;

:: deftheorem Def3 defines log POWER:def 3 :

definition

let c₁, c₂ be Real;
redefine func log as log c₁,c₂ -> Real;
coherence by XREAL_0:def 1;

end;

theorem Th58: :: POWER:58

canceled;

theorem Th59: :: POWER:59

for b₁ being real number st b₁ > 0 & b₁ <> 1 holds
log b₁,1 = 0

proof end;

theorem Th60: :: POWER:60

for b₁ being real number st b₁ > 0 & b₁ <> 1 holds
log b₁,b₁ = 1

proof end;

theorem Th61: :: POWER:61

for b₁, b₂, b₃ being real number st b₁ > 0 & b₁ <> 1 & b₂ > 0 & b₃ > 0 holds
(log b₁,b₂) + (log b₁,b₃) = log b₁,(b₂ * b₃)

proof end;

theorem Th62: :: POWER:62

for b₁, b₂, b₃ being real number st b₁ > 0 & b₁ <> 1 & b₂ > 0 & b₃ > 0 holds
(log b₁,b₂) - (log b₁,b₃) = log b₁,(b₂ / b₃)

proof end;

theorem Th63: :: POWER:63

for b₁, b₂, b₃ being real number st b₁ > 0 & b₁ <> 1 & b₂ > 0 holds
log b₁,(b₂ to_power b₃) = b₃ * (log b₁,b₂)

proof end;

theorem Th64: :: POWER:64

for b₁, b₂, b₃ being real number st b₁ > 0 & b₁ <> 1 & b₂ > 0 & b₂ <> 1 & b₃ > 0 holds
log b₁,b₃ = (log b₁,b₂) * (log b₂,b₃)

proof end;

theorem Th65: :: POWER:65

for b₁, b₂, b₃ being real number st b₁ > 1 & b₂ > 0 & b₃ > b₂ holds
log b₁,b₃ > log b₁,b₂

proof end;

theorem Th66: :: POWER:66

for b₁, b₂, b₃ being real number st b₁ > 0 & b₁ < 1 & b₂ > 0 & b₃ > b₂ holds
log b₁,b₃ < log b₁,b₂

proof end;

theorem Th67: :: POWER:67

for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ = (1 + (1 / (b₂ + 1))) to_power (b₂ + 1) ) holds
b₁ is convergent

proof end;

definition

func number_e -> real number means :: POWER:def 4
for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ = (1 + (1 / (b₂ + 1))) to_power (b₂ + 1) ) holds
a₁ = lim b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines number_e POWER:def 4 :

definition

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

end;