:: by Konrad Raczkowski

::

:: Received September 21, 1990

:: Copyright (c) 1990-2017 Association of Mizar Users

theorem Th1: :: PREPOWER:1

for a being Real

for s1 being Real_Sequence st s1 is convergent & ( for n being Nat holds s1 . n >= a ) holds

lim s1 >= a

for s1 being Real_Sequence st s1 is convergent & ( for n being Nat holds s1 . n >= a ) holds

lim s1 >= a

proof end;

theorem Th2: :: PREPOWER:2

for a being Real

for s1 being Real_Sequence st s1 is convergent & ( for n being Nat holds s1 . n <= a ) holds

lim s1 <= a

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;

ex b_{1} being Real_Sequence st

for m being Nat holds b_{1} . m = a |^ m

for b_{1}, b_{2} being Real_Sequence st ( for m being Nat holds b_{1} . m = a |^ m ) & ( for m being Nat holds b_{2} . m = a |^ m ) holds

b_{1} = b_{2}

end;
func a GeoSeq -> Real_Sequence means :Def1: :: PREPOWER:def 1

for m being Nat holds it . m = a |^ m;

existence for m being Nat holds it . m = a |^ m;

ex b

for m being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines GeoSeq PREPOWER:def 1 :

for a being Real

for b_{2} being Real_Sequence holds

( b_{2} = a GeoSeq iff for m being Nat holds b_{2} . m = a |^ m );

for a being Real

for b

( b

theorem Th3: :: PREPOWER:3

for a being Real

for s1 being Real_Sequence holds

( s1 = a GeoSeq iff ( s1 . 0 = 1 & ( for m being Nat holds s1 . (m + 1) = (s1 . m) * a ) ) )

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;

Lm1: for a, b being Real

for n being natural Number st 0 < a & a < b & 1 <= n holds

a |^ n < b |^ n

proof end;

theorem Th17: :: PREPOWER:17

for a being Real

for n being natural Number st 0 < a & a < 1 holds

(1 + a) |^ n <= 1 + ((3 |^ n) * a)

for n being natural Number st 0 < a & a < 1 holds

(1 + a) |^ n <= 1 + ((3 |^ n) * a)

proof end;

reconsider j = 1 as Element of REAL by NUMBERS:19;

theorem Th18: :: PREPOWER:18

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 )

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;

assume A1: 1 <= n ;

for b_{1} being Real st a > 0 & a = 0 holds

( ( b_{1} |^ n = a & b_{1} > 0 ) iff b_{1} = 0 )
;

existence

( ( a > 0 implies ex b_{1} being Real st

( b_{1} |^ n = a & b_{1} > 0 ) ) & ( a = 0 implies ex b_{1} being Real st b_{1} = 0 ) )

for b_{1}, b_{2} being Real holds

( ( a > 0 & b_{1} |^ n = a & b_{1} > 0 & b_{2} |^ n = a & b_{2} > 0 implies b_{1} = b_{2} ) & ( a = 0 & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) )

end;
let a be Real;

assume A1: 1 <= n ;

func n -Root a -> Real means :Def2: :: PREPOWER:def 2

( it |^ n = a & it > 0 ) if a > 0

it = 0 if a = 0

;

consistency ( it |^ n = a & it > 0 ) if a > 0

it = 0 if a = 0

;

for b

( ( b

existence

( ( a > 0 implies ex b

( b

proof end;

uniqueness for b

( ( a > 0 & b

proof end;

:: deftheorem Def2 defines -Root PREPOWER:def 2 :

for n being natural Number

for a being Real st 1 <= n holds

for b_{3} being Real holds

( ( a > 0 implies ( b_{3} = n -Root a iff ( b_{3} |^ n = a & b_{3} > 0 ) ) ) & ( a = 0 implies ( b_{3} = n -Root a iff b_{3} = 0 ) ) );

for n being natural Number

for a being Real st 1 <= n holds

for b

( ( a > 0 implies ( b

Lm2: for a being Real

for n being Nat st a > 0 & n >= 1 holds

( (n -Root a) |^ n = a & n -Root (a |^ n) = a )

proof end;

theorem Th19: :: PREPOWER:19

for a being Real

for n being Nat st a >= 0 & n >= 1 holds

( (n -Root a) |^ n = a & n -Root (a |^ n) = a )

for n being Nat st a >= 0 & n >= 1 holds

( (n -Root a) |^ n = a & n -Root (a |^ n) = a )

proof end;

theorem Th22: :: PREPOWER:22

for a, b being Real

for n being Nat st a >= 0 & b >= 0 & n >= 1 holds

n -Root (a * b) = (n -Root a) * (n -Root b)

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 :: PREPOWER:24

for a, b being Real

for n being Nat st a >= 0 & b > 0 & n >= 1 holds

n -Root (a / b) = (n -Root a) / (n -Root b)

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 Th25: :: PREPOWER:25

for a being Real

for m, n being Nat st a >= 0 & n >= 1 & m >= 1 holds

n -Root (m -Root a) = (n * m) -Root a

for m, n being Nat st a >= 0 & n >= 1 & m >= 1 holds

n -Root (m -Root a) = (n * m) -Root a

proof end;

theorem Th26: :: PREPOWER:26

for a being Real

for m, n being Nat st a >= 0 & n >= 1 & m >= 1 holds

(n -Root a) * (m -Root a) = (n * m) -Root (a |^ (n + m))

for m, n 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 Th30: :: PREPOWER:30

for a being Real

for n being Nat st 0 <= a & a < 1 & n >= 1 holds

( a <= n -Root a & n -Root a < 1 )

for n being Nat st 0 <= a & a < 1 & n >= 1 holds

( a <= n -Root a & n -Root a < 1 )

proof end;

Lm3: for s being Real_Sequence

for a being Real 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:33

for a being Real

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 )

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;

let k be Integer;

consistency

for b_{1} being number st k >= 0 & k < 0 holds

( b_{1} = a |^ |.k.| iff b_{1} = (a |^ |.k.|) " )
;

coherence

( ( k >= 0 implies a |^ |.k.| is number ) & ( k < 0 implies (a |^ |.k.|) " is number ) ) by TARSKI:1;

end;
let k be Integer;

consistency

for b

( b

coherence

( ( k >= 0 implies a |^ |.k.| is number ) & ( k < 0 implies (a |^ |.k.|) " is number ) ) by TARSKI:1;

:: deftheorem Def3 defines #Z PREPOWER:def 3 :

for a being Real

for k being Integer holds

( ( k >= 0 implies a #Z k = a |^ |.k.| ) & ( k < 0 implies a #Z k = (a |^ |.k.|) " ) );

for a being Real

for k being Integer holds

( ( k >= 0 implies a #Z k = a |^ |.k.| ) & ( k < 0 implies a #Z k = (a |^ |.k.|) " ) );

registration
end;

Lm4: 1 " = 1

;

theorem Th46: :: PREPOWER:46

for a being Real

for n being Nat

for k being Integer st a > 0 & n >= 1 holds

(n -Root a) #Z k = n -Root (a #Z k)

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;

let p be Rational;

coherence

(denominator p) -Root (a #Z (numerator p)) is number by TARSKI:1;

end;
let p be Rational;

coherence

(denominator p) -Root (a #Z (numerator p)) is number by TARSKI:1;

:: deftheorem defines #Q PREPOWER:def 4 :

for a being Real

for p being Rational holds a #Q p = (denominator p) -Root (a #Z (numerator p));

for a being Real

for p being Rational holds a #Q p = (denominator p) -Root (a #Z (numerator p));

registration
end;

Lm5: for a being Real

for k being Integer st a >= 0 holds

a #Z k >= 0

proof end;

registration

ex b_{1} being Real_Sequence st b_{1} is RAT -valued
end;

cluster Relation-like omega -defined REAL -valued RAT -valued Function-like V11() V14( omega ) V18( omega , REAL ) complex-valued ext-real-valued real-valued for Element of K19(K20(omega,REAL));

existence ex b

proof end;

theorem Th67: :: PREPOWER:67

for a being Real ex s being Rational_Sequence st

( s is convergent & lim s = a & ( for n being Nat holds s . n <= a ) )

( s is convergent & lim s = a & ( for n being Nat holds s . n <= a ) )

proof end;

theorem Th68: :: PREPOWER:68

for a being Real ex s being Rational_Sequence st

( s is convergent & lim s = a & ( for n being Nat holds s . n >= a ) )

( s is convergent & lim s = a & ( for n being Nat holds s . n >= a ) )

proof end;

definition

let a be Real;

let s be Rational_Sequence;

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = a #Q (s . n)

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = a #Q (s . n) ) & ( for n being Nat holds b_{2} . n = a #Q (s . n) ) holds

b_{1} = b_{2}

end;
let s be Rational_Sequence;

func a #Q s -> Real_Sequence means :Def5: :: PREPOWER:def 6

for n being Nat holds it . n = a #Q (s . n);

existence for n being Nat holds it . n = a #Q (s . n);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

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

for a being Real

for s being Rational_Sequence

for b_{3} being Real_Sequence holds

( b_{3} = a #Q s iff for n being Nat holds b_{3} . n = a #Q (s . n) );

for a being Real

for s being Rational_Sequence

for b

( b

Lm6: for s being Rational_Sequence

for a being Real st s is convergent & a >= 1 holds

a #Q s is convergent

proof end;

theorem Th69: :: PREPOWER:69

for a being Real

for s being Rational_Sequence st s is convergent & a > 0 holds

a #Q s is convergent

for s being Rational_Sequence st s is convergent & a > 0 holds

a #Q s is convergent

proof end;

Lm7: for s1, s2 being Rational_Sequence

for a being Real 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 Th70: :: PREPOWER:70

for s1, s2 being Rational_Sequence

for a being Real 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) )

for a being Real 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;

assume A1: a > 0 ;

ex b_{1} being Real ex s being Rational_Sequence st

( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = b_{1} )

for b_{1}, b_{2} being Real st ex s being Rational_Sequence st

( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = b_{1} ) & ex s being Rational_Sequence st

( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = b_{2} ) holds

b_{1} = b_{2}
by A1, Th70;

end;
assume A1: a > 0 ;

func a #R b -> Real means :Def6: :: PREPOWER:def 7

ex s being Rational_Sequence st

( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = it );

existence ex s being Rational_Sequence st

( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = it );

ex b

( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = b

proof end;

uniqueness for b

( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = b

( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = b

b

:: deftheorem Def6 defines #R PREPOWER:def 7 :

for a, b being Real st a > 0 holds

for b_{3} being Real holds

( b_{3} = 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) = b_{3} ) );

for a, b being Real st a > 0 holds

for b

( b

( s is convergent & lim s = b & a #Q s is convergent & lim (a #Q s) = b

Lm8: for a, b being Real st a > 0 holds

a #R b >= 0

proof end;

Lm9: for a, b being Real st a > 0 holds

a #R b <> 0

proof end;

Lm10: 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 Th89: :: PREPOWER:89

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

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;

Lm11: for a, b being Real

for p being Rational st a > 0 holds

(a #R b) #Q p = a #R (b * p)

proof end;

Lm12: for a being Real

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 Th90: :: PREPOWER:90

for a being Real

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)

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;

:: from SCPINVAR, 2006.03.14, A.T.

:: missing, 2008.03.05, A.T.

:: missing, 2010.02.13, A.T.