:: by Konrad Raczkowski

::

:: Received September 21, 1990

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

begin

theorem Th1: :: PREPOWER:1

for a being real number

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

lim s1 >= a

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

lim s1 >= a

proof end;

theorem Th2: :: PREPOWER:2

for a being real number

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

lim s1 <= a

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

lim s1 <= a

proof end;

definition

let a be real number ;

ex b_{1} being Real_Sequence st

for m being Element of NAT holds b_{1} . m = a |^ m

for b_{1}, b_{2} being Real_Sequence st ( for m being Element of NAT holds b_{1} . m = a |^ m ) & ( for m being Element of 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 Element of NAT holds it . m = a |^ m;

existence for m being Element of NAT holds it . m = a |^ m;

ex b

for m being Element of NAT holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines GeoSeq PREPOWER:def 1 :

for a being real number

for b_{2} being Real_Sequence holds

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

for a being real number

for b

( b

theorem Th3: :: PREPOWER:3

for a being real number

for s1 being Real_Sequence holds

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

for s1 being Real_Sequence holds

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

proof end;

Lm1: for a, b being real number

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

a |^ n < b |^ n

proof end;

theorem Th18: :: PREPOWER:18

for m being Element of NAT

for s1, s2 being Real_Sequence st s1 is convergent & ( for n being Element of 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 Element of NAT holds s2 . n = (s1 . n) |^ m ) holds

( s2 is convergent & lim s2 = (lim s1) |^ m )

proof end;

definition

let n be Nat;

let a be real number ;

assume A1: 1 <= n ;

for b_{1} being real number 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 number st

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

for b_{1}, b_{2} being real number 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 number ;

assume A1: 1 <= n ;

func n -Root a -> real number 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 Nat

for a being real number st 1 <= n holds

for b_{3} being real number 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 Nat

for a being real number st 1 <= n holds

for b

( ( a > 0 implies ( b

definition

let n be Element of 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;
let a be Real;

:: original: -Root

redefine func n -Root a -> Real;

coherence

n -Root a is Real by XREAL_0:def 1;

Lm2: 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 Th19: :: PREPOWER:19

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 )

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 number

for n being Element of NAT st a >= 0 & b >= 0 & n >= 1 holds

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

for n being Element of NAT st a >= 0 & b >= 0 & n >= 1 holds

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

proof end;

theorem Th23: :: PREPOWER:23

for a being real number

for n being Element of NAT st a > 0 & n >= 1 holds

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

for n being Element of NAT st a > 0 & n >= 1 holds

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

proof end;

theorem :: PREPOWER:24

for a, b being real number

for n being Element of NAT st a >= 0 & b > 0 & n >= 1 holds

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

for n being Element of 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 number

for n, m being Element of NAT st a >= 0 & n >= 1 & m >= 1 holds

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

for n, m being Element of 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 number

for n, m being Element of NAT st a >= 0 & n >= 1 & m >= 1 holds

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

for n, m being Element of NAT st a >= 0 & n >= 1 & m >= 1 holds

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

proof end;

theorem Th27: :: PREPOWER:27

for a, b being real number

for n being Element of NAT st 0 <= a & a <= b & n >= 1 holds

n -Root a <= n -Root b

for n being Element of NAT st 0 <= a & a <= b & n >= 1 holds

n -Root a <= n -Root b

proof end;

theorem Th28: :: PREPOWER:28

for a, b being real number

for n being Element of NAT st a >= 0 & a < b & n >= 1 holds

n -Root a < n -Root b

for n being Element of NAT st a >= 0 & a < b & n >= 1 holds

n -Root a < n -Root b

proof end;

theorem Th29: :: PREPOWER:29

for a being real number

for n being Element of NAT st a >= 1 & n >= 1 holds

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

for n being Element of NAT st a >= 1 & n >= 1 holds

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

proof end;

theorem Th30: :: PREPOWER:30

for a being real number

for n being Element of NAT st 0 <= a & a < 1 & n >= 1 holds

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

for n being Element of NAT st 0 <= a & a < 1 & n >= 1 holds

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

proof end;

theorem Th31: :: PREPOWER:31

for a being real number

for n being Element of NAT st a > 0 & n >= 1 holds

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

for n being Element of NAT st a > 0 & n >= 1 holds

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

proof end;

Lm3: for s being Real_Sequence

for a being real number st a >= 1 & ( for n being Element of 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 number

for s being Real_Sequence st a > 0 & ( for n being Element of 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 Element of 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;

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

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

coherence

( ( k >= 0 implies a |^ (abs k) is set ) & ( k < 0 implies (a |^ (abs k)) " is set ) ) ;

end;
let k be Integer;

func a #Z k -> set equals :Def3: :: PREPOWER:def 3

a |^ (abs k) if k >= 0

(a |^ (abs k)) " if k < 0

;

consistency a |^ (abs k) if k >= 0

(a |^ (abs k)) " if k < 0

;

for b

( b

coherence

( ( k >= 0 implies a |^ (abs k) is set ) & ( k < 0 implies (a |^ (abs k)) " is set ) ) ;

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

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)) " ) );

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)) " ) );

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;
let k be Integer;

:: original: #Z

redefine func a #Z k -> Real;

coherence

a #Z k is Real by XREAL_0:def 1;

Lm4: 1 " = 1

;

theorem Th46: :: PREPOWER:46

for a being real number

for n being Element of NAT

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

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

for n being Element of 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;

coherence

(denominator p) -Root (a #Z (numerator p)) is set ;

end;
let p be Rational;

coherence

(denominator p) -Root (a #Z (numerator p)) is set ;

:: deftheorem defines #Q PREPOWER:def 4 :

for a being real number

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

for a being real number

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

registration
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;
let p be Rational;

:: original: #Q

redefine func a #Q p -> Real;

coherence

a #Q p is Real by XREAL_0:def 1;

Lm5: for a being real number

for k being Integer st a >= 0 holds

a #Z k >= 0

proof end;

theorem Th50: :: PREPOWER:50

for a being real number

for p being Rational

for n being Nat st n >= 1 & p = n " holds

a #Q p = n -Root a

for p being Rational

for n being Nat st n >= 1 & p = n " holds

a #Q p = n -Root a

proof end;

theorem Th56: :: PREPOWER:56

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)

for p being Rational st a > 0 & b > 0 holds

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

proof end;

theorem Th58: :: PREPOWER:58

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)

for p being Rational st a > 0 & b > 0 holds

(a / b) #Q p = (a #Q p) / (b #Q p)

proof end;

registration

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

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

existence ex b

proof end;

theorem Th67: :: PREPOWER:67

for a being real number ex s being Rational_Sequence st

( s is convergent & lim s = a & ( for n being Element of NAT holds s . n <= a ) )

( s is convergent & lim s = a & ( for n being Element of NAT holds s . n <= a ) )

proof end;

theorem Th68: :: PREPOWER:68

for a being real number ex s being Rational_Sequence st

( s is convergent & lim s = a & ( for n being Element of NAT holds s . n >= a ) )

( s is convergent & lim s = a & ( for n being Element of NAT holds s . n >= a ) )

proof end;

definition

let a be real number ;

let s be Rational_Sequence;

ex b_{1} being Real_Sequence st

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

for b_{1}, b_{2} being Real_Sequence st ( for n being Element of NAT holds b_{1} . n = a #Q (s . n) ) & ( for n being Element of 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 :Def6: :: PREPOWER:def 6

for n being Element of NAT holds it . n = a #Q (s . n);

existence for n being Element of NAT holds it . n = a #Q (s . n);

ex b

for n being Element of NAT holds b

proof end;

uniqueness for b

b

proof end;

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

for a being real number

for s being Rational_Sequence

for b_{3} being Real_Sequence holds

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

for a being real number

for s being Rational_Sequence

for b

( b

Lm6: 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 Th69: :: PREPOWER:69

for a being real number

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 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 Th70: :: PREPOWER:70

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) )

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 ;

ex b_{1} being real number 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 number 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 number means :Def7: :: 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 Def7 defines #R PREPOWER:def 7 :

for a, b being real number st a > 0 holds

for b_{3} being real number 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 number st a > 0 holds

for b

( b

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

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;
:: original: #R

redefine func a #R b -> Real;

coherence

a #R b is Real by XREAL_0:def 1;

Lm8: for a, b being real number st a > 0 holds

a #R b >= 0

proof end;

Lm9: for a, b being real number 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 Element of 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 Element of 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 Element of 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 number

for p being Rational st a > 0 holds

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

proof end;

Lm12: for a being real number

for s1, s2 being Real_Sequence st a >= 1 & s1 is convergent & s2 is convergent & ( for n being Element of 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 number

for s1, s2 being Real_Sequence st a > 0 & s1 is convergent & s2 is convergent & ( for n being Element of 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 Element of NAT holds s2 . n = a #R (s1 . n) ) holds

lim s2 = a #R (lim s1)

proof end;

begin

theorem :: PREPOWER:93

for n being Element of NAT

for r being real number

for k being Nat st k >= n & r >= 1 holds

r |^ k >= r |^ n

for r being real number

for k being Nat st k >= n & r >= 1 holds

r |^ k >= r |^ n

proof end;

:: from SCPINVAR, 2006.03.14, A.T.

:: missing, 2008.03.05, A.T.

theorem :: PREPOWER:98

:: missing, 2010.02.13, A.T.