:: PREPOWER semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for i being Integer holds abs i is Integer
proof end;

registration
let i be Integer;
cluster abs i -> natural ;
coherence
abs i is natural
proof end;
end;

definition
let i be Integer;
:: original: abs
redefine func abs i -> Nat;
coherence
abs i is Nat
by ORDINAL2:def 21;
end;

theorem :: PREPOWER:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th2: :: PREPOWER:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for s1 being Real_Sequence st s1 is convergent & ( for n being Nat holds s1 . n >= a ) holds
lim s1 >= a
proof end;

theorem Th3: :: PREPOWER:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for s1 being Real_Sequence st s1 is convergent & ( for n being Nat holds s1 . n <= a ) holds
lim s1 <= a
proof end;

definition
let a be real number ;
func a GeoSeq -> Real_Sequence means :Def1: :: PREPOWER:def 1
for m being Nat holds it . m = a |^ m;
existence
ex b1 being Real_Sequence st
for m being Nat holds b1 . m = a |^ m
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for m being Nat holds b1 . m = a |^ m ) & ( for m being Nat holds b2 . m = a |^ m ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines GeoSeq PREPOWER:def 1 :
for a being real number
for b2 being Real_Sequence holds
( b2 = a GeoSeq iff for m being Nat holds b2 . m = a |^ m );

theorem Th4: :: PREPOWER:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for s1 being Real_Sequence holds
( s1 = a GeoSeq iff ( s1 . 0 = 1 & ( for m being Nat holds s1 . (m + 1) = (s1 . m) * a ) ) )
proof end;

theorem :: PREPOWER:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number st a <> 0 holds
for m being Nat holds (a GeoSeq ) . m <> 0
proof end;

definition
let a be Real;
let n be Nat;
:: original: |^
redefine func a |^ n -> Real;
coherence
a |^ n is Real
by XREAL_0:def 1;
end;

Lm2: for a being real number holds a |^ 2 = a ^2
by NEWTON:100;

theorem :: PREPOWER:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PREPOWER:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PREPOWER:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PREPOWER:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PREPOWER:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PREPOWER:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th12: :: PREPOWER:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being natural number st 0 <> a holds
0 <> a |^ n
proof end;

theorem Th13: :: PREPOWER:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being natural number st 0 < a holds
0 < a |^ n
proof end;

theorem Th14: :: PREPOWER:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being natural number holds (1 / a) |^ n = 1 / (a |^ n)
proof end;

theorem :: PREPOWER:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b, a being real number
for n being natural number holds (b / a) |^ n = (b |^ n) / (a |^ n)
proof end;

theorem :: PREPOWER:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th17: :: PREPOWER:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number
for n being natural number st 0 < a & a <= b holds
a |^ n <= b |^ n
proof end;

Lm3: for a, b being real number
for n being natural number st 0 < a & a < b & 1 <= n holds
a |^ n < b |^ n
proof end;

theorem Th18: :: PREPOWER:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number
for n being natural number st 0 <= a & a < b & 1 <= n holds
a |^ n < b |^ n
proof end;

theorem Th19: :: PREPOWER:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being natural number st a >= 1 holds
a |^ n >= 1
proof end;

theorem Th20: :: PREPOWER:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being natural number st 1 <= a & 1 <= n holds
a <= a |^ n
proof end;

theorem :: PREPOWER:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being natural number st 1 < a & 2 <= n holds
a < a |^ n
proof end;

theorem Th22: :: PREPOWER:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being natural number st 0 < a & a <= 1 & 1 <= n holds
a |^ n <= a
proof end;

theorem :: PREPOWER:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being natural number st 0 < a & a < 1 & 2 <= n holds
a |^ n < a
proof end;

theorem Th24: :: PREPOWER:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being natural number st - 1 < a holds
(1 + a) |^ n >= 1 + (n * a)
proof end;

theorem Th25: :: PREPOWER:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being natural number st 0 < a & a < 1 holds
(1 + a) |^ n <= 1 + ((3 |^ n) * a)
proof end;

theorem Th26: :: PREPOWER:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being Nat
for s1, s2 being Real_Sequence st s1 is convergent & ( for n being Nat holds s2 . n = (s1 . n) |^ m ) holds
( s2 is convergent & lim s2 = (lim s1) |^ m )
proof end;

definition
let n be natural number ;
let a be real number ;
assume A1: 1 <= n ;
canceled;
func n -Root a -> real number means :Def3: :: PREPOWER:def 3
( it |^ n = a & it > 0 ) if a > 0
it = 0 if a = 0
;
consistency
for b1 being real number st a > 0 & a = 0 holds
( ( b1 |^ n = a & b1 > 0 ) iff b1 = 0 )
;
existence
( ( a > 0 implies ex b1 being real number st
( b1 |^ n = a & b1 > 0 ) ) & ( a = 0 implies ex b1 being real number st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being real number holds
( ( a > 0 & b1 |^ n = a & b1 > 0 & b2 |^ n = a & b2 > 0 implies b1 = b2 ) & ( a = 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof end;
end;

:: deftheorem PREPOWER:def 2 :
canceled;

:: deftheorem Def3 defines -Root PREPOWER:def 3 :
for n being natural number
for a being real number st 1 <= n holds
for b3 being real number holds
( ( a > 0 implies ( b3 = n -Root a iff ( b3 |^ n = a & b3 > 0 ) ) ) & ( a = 0 implies ( b3 = n -Root a iff b3 = 0 ) ) );

definition
let n be Nat;
let a be Real;
:: original: -Root
redefine func n -Root a -> Real;
coherence
n -Root a is Real
by XREAL_0:def 1;
end;

Lm4: for a being real number
for n being Nat st a > 0 & n >= 1 holds
( (n -Root a) |^ n = a & n -Root (a |^ n) = a )
proof end;

theorem :: PREPOWER:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th28: :: PREPOWER:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being Nat st a >= 0 & n >= 1 holds
( (n -Root a) |^ n = a & n -Root (a |^ n) = a )
proof end;

theorem Th29: :: PREPOWER:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat st n >= 1 holds
n -Root 1 = 1
proof end;

theorem Th30: :: PREPOWER:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number st a >= 0 holds
1 -Root a = a
proof end;

theorem Th31: :: PREPOWER:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number
for n being Nat st a >= 0 & b >= 0 & n >= 1 holds
n -Root (a * b) = (n -Root a) * (n -Root b)
proof end;

theorem Th32: :: PREPOWER:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being Nat st a > 0 & n >= 1 holds
n -Root (1 / a) = 1 / (n -Root a)
proof end;

theorem :: PREPOWER:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number
for n being Nat st a >= 0 & b > 0 & n >= 1 holds
n -Root (a / b) = (n -Root a) / (n -Root b)
proof end;

theorem Th34: :: PREPOWER:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n, m being Nat st a >= 0 & n >= 1 & m >= 1 holds
n -Root (m -Root a) = (n * m) -Root a
proof end;

theorem Th35: :: PREPOWER:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n, m being Nat st a >= 0 & n >= 1 & m >= 1 holds
(n -Root a) * (m -Root a) = (n * m) -Root (a |^ (n + m))
proof end;

theorem Th36: :: PREPOWER:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number
for n being Nat st 0 <= a & a <= b & n >= 1 holds
n -Root a <= n -Root b
proof end;

theorem Th37: :: PREPOWER:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number
for n being Nat st a >= 0 & a < b & n >= 1 holds
n -Root a < n -Root b
proof end;

theorem Th38: :: PREPOWER:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th39: :: PREPOWER:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being Nat st 0 <= a & a < 1 & n >= 1 holds
( a <= n -Root a & n -Root a < 1 )
proof end;

theorem Th40: :: PREPOWER:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :: PREPOWER:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number st a >= 0 holds
2 -Root a = sqrt a
proof end;

Lm5: for s being Real_Sequence
for a being real number st a >= 1 & ( for n being Nat st n >= 1 holds
s . n = n -Root a ) holds
( s is convergent & lim s = 1 )
proof end;

theorem :: PREPOWER:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for s being Real_Sequence 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 be real number ;
let k be Integer;
func a #Z k -> set equals :Def4: :: PREPOWER:def 4
a |^ (abs k) if k >= 0
(a |^ (abs k)) " if k < 0
;
consistency
for b1 being set st k >= 0 & k < 0 holds
( b1 = a |^ (abs k) iff b1 = (a |^ (abs k)) " )
;
coherence
( ( k >= 0 implies a |^ (abs k) is set ) & ( k < 0 implies (a |^ (abs k)) " is set ) )
;
end;

:: deftheorem Def4 defines #Z PREPOWER:def 4 :
for a being real number
for k being Integer holds
( ( k >= 0 implies a #Z k = a |^ (abs k) ) & ( k < 0 implies a #Z k = (a |^ (abs k)) " ) );

registration
let a be real number ;
let k be Integer;
cluster a #Z k -> real ;
coherence
a #Z k is real
proof end;
end;

definition
let a be Real;
let k be Integer;
:: original: #Z
redefine func a #Z k -> Real;
coherence
a #Z k is Real
by XREAL_0:def 1;
end;

theorem :: PREPOWER:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th44: :: PREPOWER:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number holds a #Z 0 = 1
proof end;

theorem Th45: :: PREPOWER:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number holds a #Z 1 = a
proof end;

theorem Th46: :: PREPOWER:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being natural number holds a #Z n = a |^ n
proof end;

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

theorem Th47: :: PREPOWER:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Integer holds 1 #Z k = 1
proof end;

theorem :: PREPOWER:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for k being Integer st a <> 0 holds
a #Z k <> 0
proof end;

theorem Th49: :: PREPOWER:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for k being Integer st a > 0 holds
a #Z k > 0
proof end;

theorem Th50: :: PREPOWER:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number
for k being Integer holds (a * b) #Z k = (a #Z k) * (b #Z k)
proof end;

theorem Th51: :: PREPOWER:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for k being Integer st a <> 0 holds
a #Z (- k) = 1 / (a #Z k)
proof end;

theorem Th52: :: PREPOWER:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for k being Integer holds (1 / a) #Z k = 1 / (a #Z k)
proof end;

theorem Th53: :: PREPOWER:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for m, n being natural number st a <> 0 holds
a #Z (m - n) = (a |^ m) / (a |^ n)
proof end;

theorem Th54: :: PREPOWER:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for k, l being Integer st a <> 0 holds
a #Z (k + l) = (a #Z k) * (a #Z l)
proof end;

theorem Th55: :: PREPOWER:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for k, l being Integer holds (a #Z k) #Z l = a #Z (k * l)
proof end;

theorem Th56: :: PREPOWER:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being Nat
for k being Integer st a > 0 & n >= 1 holds
(n -Root a) #Z k = n -Root (a #Z k)
proof end;

definition
let a be real number ;
let p be Rational;
func a #Q p -> set equals :: PREPOWER:def 5
(denominator p) -Root (a #Z (numerator p));
coherence
(denominator p) -Root (a #Z (numerator p)) is set
;
end;

:: deftheorem defines #Q PREPOWER:def 5 :
for a being real number
for p being Rational holds a #Q p = (denominator p) -Root (a #Z (numerator p));

registration
let a be real number ;
let p be Rational;
cluster a #Q p -> real ;
coherence
a #Q p is real
;
end;

definition
let a be Real;
let p be Rational;
:: original: #Q
redefine func a #Q p -> Real;
coherence
a #Q p is Real
by XREAL_0:def 1;
end;

theorem :: PREPOWER:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th58: :: PREPOWER:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for p being Rational st a > 0 & p = 0 holds
a #Q p = 1
proof end;

theorem Th59: :: PREPOWER:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for p being Rational st a > 0 & p = 1 holds
a #Q p = a
proof end;

theorem Th60: :: PREPOWER:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being Nat
for p being Rational st a > 0 & p = n holds
a #Q p = a |^ n
proof end;

theorem Th61: :: PREPOWER:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for n being Nat
for p being Rational st a > 0 & n >= 1 & p = n " holds
a #Q p = n -Root a
proof end;

theorem Th62: :: PREPOWER:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Rational holds 1 #Q p = 1
proof end;

theorem Th63: :: PREPOWER:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for p being Rational st a > 0 holds
a #Q p > 0
proof end;

theorem Th64: :: PREPOWER:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for p, q being Rational st a > 0 holds
(a #Q p) * (a #Q q) = a #Q (p + q)
proof end;

theorem Th65: :: PREPOWER:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for p being Rational st a > 0 holds
1 / (a #Q p) = a #Q (- p)
proof end;

theorem Th66: :: PREPOWER:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for p, q being Rational st a > 0 holds
(a #Q p) / (a #Q q) = a #Q (p - q)
proof end;

theorem Th67: :: PREPOWER:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number
for p being Rational st a > 0 & b > 0 holds
(a * b) #Q p = (a #Q p) * (b #Q p)
proof end;

theorem Th68: :: PREPOWER:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for p being Rational st a > 0 holds
(1 / a) #Q p = 1 / (a #Q p)
proof end;

theorem Th69: :: PREPOWER:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number
for p being Rational st a > 0 & b > 0 holds
(a / b) #Q p = (a #Q p) / (b #Q p)
proof end;

theorem Th70: :: PREPOWER:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for p, q being Rational st a > 0 holds
(a #Q p) #Q q = a #Q (p * q)
proof end;

theorem Th71: :: PREPOWER:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for p being Rational st a >= 1 & p >= 0 holds
a #Q p >= 1
proof end;

theorem Th72: :: PREPOWER:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for p being Rational st a >= 1 & p <= 0 holds
a #Q p <= 1
proof end;

theorem Th73: :: PREPOWER:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for p being Rational st a > 1 & p > 0 holds
a #Q p > 1
proof end;

theorem Th74: :: PREPOWER:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for p, q being Rational st a >= 1 & p >= q holds
a #Q p >= a #Q q
proof end;

theorem Th75: :: PREPOWER:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for p, q being Rational st a > 1 & p > q holds
a #Q p > a #Q q
proof end;

theorem Th76: :: PREPOWER:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for p being Rational st a > 0 & a < 1 & p > 0 holds
a #Q p < 1
proof end;

theorem :: PREPOWER:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for p being Rational st a > 0 & a <= 1 & p <= 0 holds
a #Q p >= 1
proof end;

definition
let IT be Real_Sequence;
attr IT is Rational_Sequence-like means :Def6: :: PREPOWER:def 6
for n being Nat holds IT . n is Rational;
end;

:: deftheorem Def6 defines Rational_Sequence-like PREPOWER:def 6 :
for IT being Real_Sequence holds
( IT is Rational_Sequence-like iff for n being Nat holds IT . n is Rational );

registration
cluster Rational_Sequence-like M5( NAT , REAL );
existence
ex b1 being Real_Sequence st b1 is Rational_Sequence-like
proof end;
end;

definition
mode Rational_Sequence is Rational_Sequence-like Real_Sequence;
end;

definition
let s be Rational_Sequence;
let n be Nat;
:: original: .
redefine func s . n -> Rational;
coherence
s . n is Rational
by Def6;
end;

theorem :: PREPOWER:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th79: :: PREPOWER:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number ex s being Rational_Sequence st
( s is convergent & lim s = a & ( for n being Nat holds s . n <= a ) )
proof end;

theorem Th80: :: PREPOWER:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number ex s being Rational_Sequence st
( s is convergent & lim s = a & ( for n being Nat holds s . n >= a ) )
proof end;

definition
let a be real number ;
let s be Rational_Sequence;
func a #Q s -> Real_Sequence means :Def7: :: PREPOWER:def 7
for n being Nat holds it . n = a #Q (s . n);
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = a #Q (s . n)
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = a #Q (s . n) ) & ( for n being Nat holds b2 . n = a #Q (s . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines #Q PREPOWER:def 7 :
for a being real number
for s being Rational_Sequence
for b3 being Real_Sequence holds
( b3 = a #Q s iff for n being Nat holds b3 . n = a #Q (s . n) );

Lm7: for s being Rational_Sequence
for a being real number st s is convergent & a >= 1 holds
a #Q s is convergent
proof end;

theorem :: PREPOWER:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th82: :: PREPOWER:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for s being Rational_Sequence st s is convergent & a > 0 holds
a #Q s is convergent
proof end;

Lm8: for s1, s2 being Rational_Sequence
for a being real number st s1 is convergent & s2 is convergent & lim s1 = lim s2 & a >= 1 holds
lim (a #Q s1) = lim (a #Q s2)
proof end;

theorem Th83: :: PREPOWER:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s2 being Rational_Sequence
for a being real number st s1 is convergent & s2 is convergent & lim s1 = lim s2 & a > 0 holds
( a #Q s1 is convergent & a #Q s2 is convergent & lim (a #Q s1) = lim (a #Q s2) )
proof end;

definition
let a, b be real number ;
assume A1: a > 0 ;
func a #R b -> real number means :Def8: :: PREPOWER:def 8
ex s being Rational_Sequence st
( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = it );
existence
ex b1 being real number ex s being Rational_Sequence st
( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = b1 )
proof end;
uniqueness
for b1, b2 being real number st ex s being Rational_Sequence st
( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = b1 ) & ex s being Rational_Sequence st
( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = b2 ) holds
b1 = b2
by A1, Th83;
end;

:: deftheorem Def8 defines #R PREPOWER:def 8 :
for a, b being real number st a > 0 holds
for b3 being real number holds
( b3 = a #R b iff ex s being Rational_Sequence st
( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = b3 ) );

definition
let a, b be Real;
:: original: #R
redefine func a #R b -> Real;
coherence
a #R b is Real
by XREAL_0:def 1;
end;

theorem :: PREPOWER:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th85: :: PREPOWER:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number st a > 0 holds
a #R 0 = 1
proof end;

theorem :: PREPOWER:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number st a > 0 holds
a #R 1 = a
proof end;

theorem Th87: :: PREPOWER:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number holds 1 #R a = 1
proof end;

theorem Th88: :: PREPOWER:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for p being Rational st a > 0 holds
a #R p = a #Q p
proof end;

theorem Th89: :: PREPOWER:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a > 0 holds
a #R (b + c) = (a #R b) * (a #R c)
proof end;

Lm9: for a, b being real number st a > 0 holds
a #R b >= 0
proof end;

Lm10: for a, b being real number st a > 0 holds
a #R b <> 0
proof end;

theorem Th90: :: PREPOWER:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, c being real number st a > 0 holds
a #R (- c) = 1 / (a #R c)
proof end;

theorem Th91: :: PREPOWER:91  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a > 0 holds
a #R (b - c) = (a #R b) / (a #R c)
proof end;

theorem Th92: :: PREPOWER:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a > 0 & b > 0 holds
(a * b) #R c = (a #R c) * (b #R c)
proof end;

theorem Th93: :: PREPOWER:93  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, c being real number st a > 0 holds
(1 / a) #R c = 1 / (a #R c)
proof end;

theorem :: PREPOWER:94  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a > 0 & b > 0 holds
(a / b) #R c = (a #R c) / (b #R c)
proof end;

theorem Th95: :: PREPOWER:95  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a > 0 holds
a #R b > 0
proof end;

theorem Th96: :: PREPOWER:96  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, c, b being real number st a >= 1 & c >= b holds
a #R c >= a #R b
proof end;

theorem Th97: :: PREPOWER:97  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, c, b being real number st a > 1 & c > b holds
a #R c > a #R b
proof end;

theorem Th98: :: PREPOWER:98  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, c, b being real number st a > 0 & a <= 1 & c >= b holds
a #R c <= a #R b
proof end;

theorem Th99: :: PREPOWER:99  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a >= 1 & b >= 0 holds
a #R b >= 1
proof end;

theorem Th100: :: PREPOWER:100  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a > 1 & b > 0 holds
a #R b > 1
proof end;

theorem Th101: :: PREPOWER:101  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a >= 1 & b <= 0 holds
a #R b <= 1
proof end;

theorem :: PREPOWER:102  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being real number st a > 1 & b < 0 holds
a #R b < 1
proof end;

Lm11: for p being Rational
for s1, s2 being Real_Sequence st s1 is convergent & s2 is convergent & lim s1 > 0 & p >= 0 & ( for n being Nat holds
( s1 . n > 0 & s2 . n = (s1 . n) #Q p ) ) holds
lim s2 = (lim s1) #Q p
proof end;

theorem Th103: :: PREPOWER:103  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Rational
for s1, s2 being Real_Sequence st s1 is convergent & s2 is convergent & lim s1 > 0 & ( for n being Nat holds
( s1 . n > 0 & s2 . n = (s1 . n) #Q p ) ) holds
lim s2 = (lim s1) #Q p
proof end;

Lm12: for a, b being real number
for p being Rational st a > 0 holds
(a #R b) #Q p = a #R (b * p)
proof end;

Lm13: for a being real number
for s1, s2 being Real_Sequence st a >= 1 & s1 is convergent & s2 is convergent & ( for n being Nat holds s2 . n = a #R (s1 . n) ) holds
lim s2 = a #R (lim s1)
proof end;

theorem Th104: :: PREPOWER:104  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for s1, s2 being Real_Sequence st a > 0 & s1 is convergent & s2 is convergent & ( for n being Nat holds s2 . n = a #R (s1 . n) ) holds
lim s2 = a #R (lim s1)
proof end;

theorem :: PREPOWER:105  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being real number st a > 0 holds
(a #R b) #R c = a #R (b * c)
proof end;