:: PREPOWER semantic presentation

Lemma1: for b₁ being Integer holds abs b₁ is Integer

proof end;

registration

let c₁ be Integer;
cluster abs a₁ -> natural ;
coherence

proof end;

end;

definition

let c₁ be Integer;
redefine func abs as abs c₁ -> Nat;
coherence by ORDINAL2:def 21;

end;

theorem Th1: :: PREPOWER:1

canceled;

theorem Th2: :: PREPOWER:2

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

proof end;

theorem Th3: :: PREPOWER:3

for b₁ being real number
for b₂ being Real_Sequence st b₂ is convergent & ( for b₃ being Nat holds b₂ . b₃ <= b₁ ) holds
lim b₂ <= b₁

proof end;

definition

let c₁ be real number ;
func c₁ GeoSeq -> Real_Sequence means :Def1: :: PREPOWER:def 1
for b₁ being Nat holds a₂ . b₁ = a₁ |^ b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines GeoSeq PREPOWER:def 1 :

theorem Th4: :: PREPOWER:4

for b₁ being real number
for b₂ being Real_Sequence holds
( b₂ = b₁ GeoSeq iff ( b₂ . 0 = 1 & ( for b₃ being Nat holds b₂ . (b₃ + 1) = (b₂ . b₃) * b₁ ) ) )

proof end;

theorem Th5: :: PREPOWER:5

for b₁ being real number st b₁ <> 0 holds
for b₂ being Nat holds (b₁ GeoSeq ) . b₂ <> 0

proof end;

definition

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

end;

Lemma6: for b₁ being real number holds b₁ |^ 2 = b₁ ^2
by NEWTON:100;

theorem Th6: :: PREPOWER:6

canceled;

theorem Th7: :: PREPOWER:7

canceled;

theorem Th8: :: PREPOWER:8

canceled;

theorem Th9: :: PREPOWER:9

canceled;

theorem Th10: :: PREPOWER:10

canceled;

theorem Th11: :: PREPOWER:11

canceled;

theorem Th12: :: PREPOWER:12

for b₁ being real number
for b₂ being natural number st 0 <> b₁ holds
0 <> b₁ |^ b₂

proof end;

theorem Th13: :: PREPOWER:13

for b₁ being real number
for b₂ being natural number st 0 < b₁ holds
0 < b₁ |^ b₂

proof end;

theorem Th14: :: PREPOWER:14

for b₁ being real number
for b₂ being natural number holds (1 / b₁) |^ b₂ = 1 / (b₁ |^ b₂)

proof end;

theorem Th15: :: PREPOWER:15

for b₁, b₂ being real number
for b₃ being natural number holds (b₁ / b₂) |^ b₃ = (b₁ |^ b₃) / (b₂ |^ b₃)

proof end;

theorem Th16: :: PREPOWER:16

canceled;

theorem Th17: :: PREPOWER:17

for b₁, b₂ being real number
for b₃ being natural number st 0 < b₁ & b₁ <= b₂ holds
b₁ |^ b₃ <= b₂ |^ b₃

proof end;

Lemma11: for b₁, b₂ being real number
for b₃ being natural number st 0 < b₁ & b₁ < b₂ & 1 <= b₃ holds
b₁ |^ b₃ < b₂ |^ b₃

proof end;

theorem Th18: :: PREPOWER:18

for b₁, b₂ being real number
for b₃ being natural number st 0 <= b₁ & b₁ < b₂ & 1 <= b₃ holds
b₁ |^ b₃ < b₂ |^ b₃

proof end;

theorem Th19: :: PREPOWER:19

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

proof end;

theorem Th20: :: PREPOWER:20

for b₁ being real number
for b₂ being natural number st 1 <= b₁ & 1 <= b₂ holds
b₁ <= b₁ |^ b₂

proof end;

theorem Th21: :: PREPOWER:21

for b₁ being real number
for b₂ being natural number st 1 < b₁ & 2 <= b₂ holds
b₁ < b₁ |^ b₂

proof end;

theorem Th22: :: PREPOWER:22

for b₁ being real number
for b₂ being natural number st 0 < b₁ & b₁ <= 1 & 1 <= b₂ holds
b₁ |^ b₂ <= b₁

proof end;

theorem Th23: :: PREPOWER:23

for b₁ being real number
for b₂ being natural number st 0 < b₁ & b₁ < 1 & 2 <= b₂ holds
b₁ |^ b₂ < b₁

proof end;

theorem Th24: :: PREPOWER:24

for b₁ being real number
for b₂ being natural number st - 1 < b₁ holds
(1 + b₁) |^ b₂ >= 1 + (b₂ * b₁)

proof end;

theorem Th25: :: PREPOWER:25

for b₁ being real number
for b₂ being natural number st 0 < b₁ & b₁ < 1 holds
(1 + b₁) |^ b₂ <= 1 + ((3 |^ b₂) * b₁)

proof end;

theorem Th26: :: PREPOWER:26

for b₁ being Nat
for b₂, b₃ being Real_Sequence st b₂ is convergent & ( for b₄ being Nat holds b₃ . b₄ = (b₂ . b₄) |^ b₁ ) holds
( b₃ is convergent & lim b₃ = (lim b₂) |^ b₁ )

proof end;

definition

let c₁ be natural number ;
let c₂ be real number ;
assume E19: 1 <= c₁ ;
canceled;
func c₁ -Root c₂ -> real number means :Def3: :: PREPOWER:def 3
( a₃ |^ a₁ = a₂ & a₃ > 0 ) if a₂ > 0
a₃ = 0 if a₂ = 0
;
consistency ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 PREPOWER:def 2 :

:: deftheorem Def3 defines -Root PREPOWER:def 3 :

definition

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

end;

Lemma20: for b₁ being real number
for b₂ being Nat st b₁ > 0 & b₂ >= 1 holds
( (b₂ -Root b₁) |^ b₂ = b₁ & b₂ -Root (b₁ |^ b₂) = b₁ )

proof end;

theorem Th27: :: PREPOWER:27

canceled;

theorem Th28: :: PREPOWER:28

for b₁ being real number
for b₂ being Nat st b₁ >= 0 & b₂ >= 1 holds
( (b₂ -Root b₁) |^ b₂ = b₁ & b₂ -Root (b₁ |^ b₂) = b₁ )

proof end;

theorem Th29: :: PREPOWER:29

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

proof end;

theorem Th30: :: PREPOWER:30

for b₁ being real number st b₁ >= 0 holds
1 -Root b₁ = b₁

proof end;

theorem Th31: :: PREPOWER:31

for b₁, b₂ being real number
for b₃ being Nat st b₁ >= 0 & b₂ >= 0 & b₃ >= 1 holds
b₃ -Root (b₁ * b₂) = (b₃ -Root b₁) * (b₃ -Root b₂)

proof end;

theorem Th32: :: PREPOWER:32

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

proof end;

theorem Th33: :: PREPOWER:33

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

proof end;

theorem Th34: :: PREPOWER:34

for b₁ being real number
for b₂, b₃ being Nat st b₁ >= 0 & b₂ >= 1 & b₃ >= 1 holds
b₂ -Root (b₃ -Root b₁) = (b₂ * b₃) -Root b₁

proof end;

theorem Th35: :: PREPOWER:35

for b₁ being real number
for b₂, b₃ being Nat st b₁ >= 0 & b₂ >= 1 & b₃ >= 1 holds
(b₂ -Root b₁) * (b₃ -Root b₁) = (b₂ * b₃) -Root (b₁ |^ (b₂ + b₃))

proof end;

theorem Th36: :: PREPOWER:36

for b₁, b₂ being real number
for b₃ being Nat st 0 <= b₁ & b₁ <= b₂ & b₃ >= 1 holds
b₃ -Root b₁ <= b₃ -Root b₂

proof end;

theorem Th37: :: PREPOWER:37

for b₁, b₂ being real number
for b₃ being Nat st b₁ >= 0 & b₁ < b₂ & b₃ >= 1 holds
b₃ -Root b₁ < b₃ -Root b₂

proof end;

theorem Th38: :: PREPOWER:38

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 Th39: :: PREPOWER:39

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

proof end;

theorem Th40: :: PREPOWER:40

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 Th41: :: PREPOWER:41

for b₁ being real number st b₁ >= 0 holds
2 -Root b₁ = sqrt b₁

proof end;

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

proof end;

theorem Th42: :: PREPOWER:42

for b₁ being real number
for b₂ being Real_Sequence 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₁ be real number ;
let c₂ be Integer;
func c₁ #Z c₂ -> set equals :Def4: :: PREPOWER:def 4
a₁ |^ (abs a₂) if a₂ >= 0
(a₁ |^ (abs a₂)) " if a₂ < 0
;
consistency ;
coherence ;

end;

:: deftheorem Def4 defines #Z PREPOWER:def 4 :

registration

let c₁ be real number ;
let c₂ be Integer;
cluster a₁ #Z a₂ -> real ;
coherence

proof end;

end;

definition

let c₁ be Real;
let c₂ be Integer;
redefine func #Z as c₁ #Z c₂ -> Real;
coherence by XREAL_0:def 1;

end;

theorem Th43: :: PREPOWER:43

canceled;

theorem Th44: :: PREPOWER:44

for b₁ being real number holds b₁ #Z 0 = 1

proof end;

theorem Th45: :: PREPOWER:45

for b₁ being real number holds b₁ #Z 1 = b₁

proof end;

theorem Th46: :: PREPOWER:46

for b₁ being real number
for b₂ being natural number holds b₁ #Z b₂ = b₁ |^ b₂

proof end;

Lemma38: ( 1 " = 1 & 1 / 1 = 1 )
;

theorem Th47: :: PREPOWER:47

for b₁ being Integer holds 1 #Z b₁ = 1

proof end;

theorem Th48: :: PREPOWER:48

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

proof end;

theorem Th49: :: PREPOWER:49

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

proof end;

theorem Th50: :: PREPOWER:50

for b₁, b₂ being real number
for b₃ being Integer holds (b₁ * b₂) #Z b₃ = (b₁ #Z b₃) * (b₂ #Z b₃)

proof end;

theorem Th51: :: PREPOWER:51

for b₁ being real number
for b₂ being Integer st b₁ <> 0 holds
b₁ #Z (- b₂) = 1 / (b₁ #Z b₂)

proof end;

theorem Th52: :: PREPOWER:52

for b₁ being real number
for b₂ being Integer holds (1 / b₁) #Z b₂ = 1 / (b₁ #Z b₂)

proof end;

theorem Th53: :: PREPOWER:53

for b₁ being real number
for b₂, b₃ being natural number st b₁ <> 0 holds
b₁ #Z (b₂ - b₃) = (b₁ |^ b₂) / (b₁ |^ b₃)

proof end;

theorem Th54: :: PREPOWER:54

for b₁ being real number
for b₂, b₃ being Integer st b₁ <> 0 holds
b₁ #Z (b₂ + b₃) = (b₁ #Z b₂) * (b₁ #Z b₃)

proof end;

theorem Th55: :: PREPOWER:55

for b₁ being real number
for b₂, b₃ being Integer holds (b₁ #Z b₂) #Z b₃ = b₁ #Z (b₂ * b₃)

proof end;

theorem Th56: :: PREPOWER:56

for b₁ being real number
for b₂ being Nat
for b₃ being Integer st b₁ > 0 & b₂ >= 1 holds
(b₂ -Root b₁) #Z b₃ = b₂ -Root (b₁ #Z b₃)

proof end;

definition

let c₁ be real number ;
let c₂ be Rational;
func c₁ #Q c₂ -> set equals :: PREPOWER:def 5
(denominator a₂) -Root (a₁ #Z (numerator a₂));
coherence ;

end;

:: deftheorem Def5 defines #Q PREPOWER:def 5 :

registration

let c₁ be real number ;
let c₂ be Rational;
cluster a₁ #Q a₂ -> real ;
coherence ;

end;

definition

let c₁ be Real;
let c₂ be Rational;
redefine func #Q as c₁ #Q c₂ -> Real;
coherence by XREAL_0:def 1;

end;

theorem Th57: :: PREPOWER:57

canceled;

theorem Th58: :: PREPOWER:58

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

proof end;

theorem Th59: :: PREPOWER:59

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

proof end;

theorem Th60: :: PREPOWER:60

for b₁ being real number
for b₂ being Nat
for b₃ being Rational st b₁ > 0 & b₃ = b₂ holds
b₁ #Q b₃ = b₁ |^ b₂

proof end;

theorem Th61: :: PREPOWER:61

for b₁ being real number
for b₂ being Nat
for b₃ being Rational st b₁ > 0 & b₂ >= 1 & b₃ = b₂ " holds
b₁ #Q b₃ = b₂ -Root b₁

proof end;

theorem Th62: :: PREPOWER:62

for b₁ being Rational holds 1 #Q b₁ = 1

proof end;

theorem Th63: :: PREPOWER:63

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

proof end;

theorem Th64: :: PREPOWER:64

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

proof end;

theorem Th65: :: PREPOWER:65

for b₁ being real number
for b₂ being Rational st b₁ > 0 holds
1 / (b₁ #Q b₂) = b₁ #Q (- b₂)

proof end;

theorem Th66: :: PREPOWER:66

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

proof end;

theorem Th67: :: PREPOWER:67

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

proof end;

theorem Th68: :: PREPOWER:68

for b₁ being real number
for b₂ being Rational st b₁ > 0 holds
(1 / b₁) #Q b₂ = 1 / (b₁ #Q b₂)

proof end;

theorem Th69: :: PREPOWER:69

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

proof end;

theorem Th70: :: PREPOWER:70

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

proof end;

theorem Th71: :: PREPOWER:71

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

proof end;

theorem Th72: :: PREPOWER:72

for b₁ being real number
for b₂ being Rational st b₁ >= 1 & b₂ <= 0 holds
b₁ #Q b₂ <= 1

proof end;

theorem Th73: :: PREPOWER:73

for b₁ being real number
for b₂ being Rational st b₁ > 1 & b₂ > 0 holds
b₁ #Q b₂ > 1

proof end;

theorem Th74: :: PREPOWER:74

for b₁ being real number
for b₂, b₃ being Rational st b₁ >= 1 & b₂ >= b₃ holds
b₁ #Q b₂ >= b₁ #Q b₃

proof end;

theorem Th75: :: PREPOWER:75

for b₁ being real number
for b₂, b₃ being Rational st b₁ > 1 & b₂ > b₃ holds
b₁ #Q b₂ > b₁ #Q b₃

proof end;

theorem Th76: :: PREPOWER:76

for b₁ being real number
for b₂ being Rational st b₁ > 0 & b₁ < 1 & b₂ > 0 holds
b₁ #Q b₂ < 1

proof end;

theorem Th77: :: PREPOWER:77

for b₁ being real number
for b₂ being Rational st b₁ > 0 & b₁ <= 1 & b₂ <= 0 holds
b₁ #Q b₂ >= 1

proof end;

definition

let c₁ be Real_Sequence;
attr a₁ is Rational_Sequence-like means :Def6: :: PREPOWER:def 6
for b₁ being Nat holds a₁ . b₁ is Rational;

end;

:: deftheorem Def6 defines Rational_Sequence-like PREPOWER:def 6 :

registration

cluster Rational_Sequence-like M5( NAT , REAL );
existence

proof end;

end;

definition

mode Rational_Sequence is Rational_Sequence-like Real_Sequence;

end;

definition

let c₁ be Rational_Sequence;
let c₂ be Nat;
redefine func . as c₁ . c₂ -> Rational;
coherence by Def6;

end;

theorem Th78: :: PREPOWER:78

canceled;

theorem Th79: :: PREPOWER:79

for b₁ being real number ex b₂ being Rational_Sequence st
( b₂ is convergent & lim b₂ = b₁ & ( for b₃ being Nat holds b₂ . b₃ <= b₁ ) )

proof end;

theorem Th80: :: PREPOWER:80

for b₁ being real number ex b₂ being Rational_Sequence st
( b₂ is convergent & lim b₂ = b₁ & ( for b₃ being Nat holds b₂ . b₃ >= b₁ ) )

proof end;

definition

let c₁ be real number ;
let c₂ be Rational_Sequence;
func c₁ #Q c₂ -> Real_Sequence means :Def7: :: PREPOWER:def 7
for b₁ being Nat holds a₃ . b₁ = a₁ #Q (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines #Q PREPOWER:def 7 :

Lemma71: for b₁ being Rational_Sequence
for b₂ being real number st b₁ is convergent & b₂ >= 1 holds
b₂ #Q b₁ is convergent

proof end;

theorem Th81: :: PREPOWER:81

canceled;

theorem Th82: :: PREPOWER:82

for b₁ being real number
for b₂ being Rational_Sequence st b₂ is convergent & b₁ > 0 holds
b₁ #Q b₂ is convergent

proof end;

Lemma73: for b₁, b₂ being Rational_Sequence
for b₃ being real number st b₁ is convergent & b₂ is convergent & lim b₁ = lim b₂ & b₃ >= 1 holds
lim (b₃ #Q b₁) = lim (b₃ #Q b₂)

proof end;

theorem Th83: :: PREPOWER:83

for b₁, b₂ being Rational_Sequence
for b₃ being real number st b₁ is convergent & b₂ is convergent & lim b₁ = lim b₂ & b₃ > 0 holds
( b₃ #Q b₁ is convergent & b₃ #Q b₂ is convergent & lim (b₃ #Q b₁) = lim (b₃ #Q b₂) )

proof end;

definition

let c₁, c₂ be real number ;
assume E75: c₁ > 0 ;
func c₁ #R c₂ -> real number means :Def8: :: PREPOWER:def 8
ex b₁ being Rational_Sequence st
( b₁ is convergent & lim b₁ = a₂ & a₁ #Q b₁ is convergent & lim (a₁ #Q b₁) = a₃ );
existence

proof end;

uniqueness by E75, Th83;

end;

:: deftheorem Def8 defines #R PREPOWER:def 8 :

definition

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

end;

theorem Th84: :: PREPOWER:84

canceled;

theorem Th85: :: PREPOWER:85

for b₁ being real number st b₁ > 0 holds
b₁ #R 0 = 1

proof end;

theorem Th86: :: PREPOWER:86

for b₁ being real number st b₁ > 0 holds
b₁ #R 1 = b₁

proof end;

theorem Th87: :: PREPOWER:87

for b₁ being real number holds 1 #R b₁ = 1

proof end;

theorem Th88: :: PREPOWER:88

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

proof end;

theorem Th89: :: PREPOWER:89

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

proof end;

Lemma80: for b₁, b₂ being real number st b₁ > 0 holds
b₁ #R b₂ >= 0

proof end;

Lemma81: for b₁, b₂ being real number st b₁ > 0 holds
b₁ #R b₂ <> 0

proof end;

theorem Th90: :: PREPOWER:90

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

proof end;

theorem Th91: :: PREPOWER:91

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

proof end;

theorem Th92: :: PREPOWER:92

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

proof end;

theorem Th93: :: PREPOWER:93

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

proof end;

theorem Th94: :: PREPOWER:94

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

proof end;

theorem Th95: :: PREPOWER:95

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

proof end;

theorem Th96: :: PREPOWER:96

for b₁, b₂, b₃ being real number st b₁ >= 1 & b₂ >= b₃ holds
b₁ #R b₂ >= b₁ #R b₃

proof end;

theorem Th97: :: PREPOWER:97

for b₁, b₂, b₃ being real number st b₁ > 1 & b₂ > b₃ holds
b₁ #R b₂ > b₁ #R b₃

proof end;

theorem Th98: :: PREPOWER:98

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

proof end;

theorem Th99: :: PREPOWER:99

for b₁, b₂ being real number st b₁ >= 1 & b₂ >= 0 holds
b₁ #R b₂ >= 1

proof end;

theorem Th100: :: PREPOWER:100

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

proof end;

theorem Th101: :: PREPOWER:101

for b₁, b₂ being real number st b₁ >= 1 & b₂ <= 0 holds
b₁ #R b₂ <= 1

proof end;

theorem Th102: :: PREPOWER:102

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

proof end;

Lemma93: for b₁ being Rational
for b₂, b₃ being Real_Sequence st b₂ is convergent & b₃ is convergent & lim b₂ > 0 & b₁ >= 0 & ( for b₄ being Nat holds
( b₂ . b₄ > 0 & b₃ . b₄ = (b₂ . b₄) #Q b₁ ) ) holds
lim b₃ = (lim b₂) #Q b₁

proof end;

theorem Th103: :: PREPOWER:103

for b₁ being Rational
for b₂, b₃ being Real_Sequence st b₂ is convergent & b₃ is convergent & lim b₂ > 0 & ( for b₄ being Nat holds
( b₂ . b₄ > 0 & b₃ . b₄ = (b₂ . b₄) #Q b₁ ) ) holds
lim b₃ = (lim b₂) #Q b₁

proof end;

Lemma95: for b₁, b₂ being real number
for b₃ being Rational st b₁ > 0 holds
(b₁ #R b₂) #Q b₃ = b₁ #R (b₂ * b₃)

proof end;

Lemma96: for b₁ being real number
for b₂, b₃ being Real_Sequence st b₁ >= 1 & b₂ is convergent & b₃ is convergent & ( for b₄ being Nat holds b₃ . b₄ = b₁ #R (b₂ . b₄) ) holds
lim b₃ = b₁ #R (lim b₂)

proof end;

theorem Th104: :: PREPOWER:104

for b₁ being real number
for b₂, b₃ being Real_Sequence st b₁ > 0 & b₂ is convergent & b₃ is convergent & ( for b₄ being Nat holds b₃ . b₄ = b₁ #R (b₂ . b₄) ) holds
lim b₃ = b₁ #R (lim b₂)

proof end;

theorem Th105: :: PREPOWER:105

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

proof end;