:: by Konrad Raczkowski and Andrzej N\c{e}dzusiak

::

:: Received October 1, 1990

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

begin

definition

let n be Nat;

let a be real number ;

for b_{1} being real number st a >= 0 & n >= 1 & a < 0 & n is odd holds

( b_{1} = n -Root a iff b_{1} = - (n -Root (- a)) )
;

coherence

( ( a >= 0 & n >= 1 implies n -Root a is real number ) & ( a < 0 & n is odd implies - (n -Root (- a)) is real number ) ) ;

end;
let a be real number ;

func n -root a -> real number equals :Def1: :: POWER:def 1

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

- (n -Root (- a)) if ( a < 0 & n is odd )

;

consistency n -Root a if ( a >= 0 & n >= 1 )

- (n -Root (- a)) if ( a < 0 & n is odd )

;

for b

( b

coherence

( ( a >= 0 & n >= 1 implies n -Root a is real number ) & ( a < 0 & n is odd implies - (n -Root (- a)) is real number ) ) ;

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

for n being Nat

for a being real number holds

( ( a >= 0 & n >= 1 implies n -root a = n -Root a ) & ( a < 0 & n is odd implies n -root a = - (n -Root (- a)) ) );

for n being Nat

for a being real number holds

( ( a >= 0 & n >= 1 implies n -root a = n -Root a ) & ( a < 0 & n is odd implies n -root a = - (n -Root (- a)) ) );

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

:: original: -root

redefine func n -root a -> Real;

coherence

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

theorem :: POWER:4

for a being real number

for n being Nat st ( ( n >= 1 & a >= 0 ) or n is odd ) holds

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

for n being Nat st ( ( n >= 1 & a >= 0 ) or n is odd ) holds

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

proof end;

theorem Th11: :: POWER:11

for a, b being real number

for n being Element of NAT st ( ( n >= 1 & a >= 0 & b >= 0 ) or n is odd ) holds

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

for n being Element of NAT st ( ( n >= 1 & a >= 0 & b >= 0 ) or n is odd ) holds

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

proof end;

theorem Th12: :: POWER:12

for a being real number

for n being Element of NAT st ( ( a > 0 & n >= 1 ) or ( a <> 0 & n is odd ) ) holds

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

for n being Element of NAT st ( ( a > 0 & n >= 1 ) or ( a <> 0 & n is odd ) ) holds

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

proof end;

theorem :: POWER:13

for a, b being real number

for n being Element of NAT st ( ( a >= 0 & b > 0 & n >= 1 ) or ( b <> 0 & n is odd ) ) holds

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

for n being Element of NAT st ( ( a >= 0 & b > 0 & n >= 1 ) or ( b <> 0 & n is odd ) ) holds

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

proof end;

theorem :: POWER:14

for a being real number

for n, m being Element of NAT st ( ( a >= 0 & n >= 1 & m >= 1 ) or ( n is odd & m is odd ) ) holds

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

for n, m being Element of NAT st ( ( a >= 0 & n >= 1 & m >= 1 ) or ( n is odd & m is odd ) ) holds

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

proof end;

theorem :: POWER:15

for a being real number

for n, m being Element of NAT st ( ( a >= 0 & n >= 1 & m >= 1 ) or ( n is odd & m is odd ) ) 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 ) or ( n is odd & m is odd ) ) holds

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

proof end;

theorem :: POWER:16

for a, b being real number

for n being Element of NAT st a <= b & ( ( 0 <= a & n >= 1 ) or n is odd ) holds

n -root a <= n -root b

for n being Element of NAT st a <= b & ( ( 0 <= a & n >= 1 ) or n is odd ) holds

n -root a <= n -root b

proof end;

theorem :: POWER:17

for a, b being real number

for n being Element of NAT st a < b & ( ( a >= 0 & n >= 1 ) or n is odd ) holds

n -root a < n -root b

for n being Element of NAT st a < b & ( ( a >= 0 & n >= 1 ) or n is odd ) holds

n -root a < n -root b

proof end;

theorem Th18: :: POWER:18

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 :: POWER:19

for a being real number

for n being Element of NAT st a <= - 1 & n is odd holds

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

for n being Element of NAT st a <= - 1 & n is odd holds

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

proof end;

theorem Th20: :: POWER:20

for a being real number

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

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

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

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

proof end;

theorem :: POWER:21

for a being real number

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

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

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

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

proof end;

theorem Th22: :: POWER:22

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;

theorem Th23: :: POWER:23

for s being Real_Sequence

for a being real number 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 a being real number 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, b be real number ;

for b_{1} being real number holds

( ( a > 0 & a = 0 & b > 0 implies ( b_{1} = a #R b iff b_{1} = 0 ) ) & ( a > 0 & b is Integer implies ( b_{1} = a #R b iff ex k being Integer st

( k = b & b_{1} = a #Z k ) ) ) & ( a = 0 & b > 0 & b is Integer implies ( b_{1} = 0 iff ex k being Integer st

( k = b & b_{1} = a #Z k ) ) ) )

( ( a > 0 implies ex b_{1} being real number st b_{1} = a #R b ) & ( a = 0 & b > 0 implies ex b_{1} being real number st b_{1} = 0 ) & ( b is Integer implies ex b_{1} being real number ex k being Integer st

( k = b & b_{1} = a #Z k ) ) )

for b_{1}, b_{2} being real number holds

( ( a > 0 & b_{1} = a #R b & b_{2} = a #R b implies b_{1} = b_{2} ) & ( a = 0 & b > 0 & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) & ( b is Integer & ex k being Integer st

( k = b & b_{1} = a #Z k ) & ex k being Integer st

( k = b & b_{2} = a #Z k ) implies b_{1} = b_{2} ) )
;

end;
func a to_power b -> real number means :Def2: :: POWER:def 2

it = a #R b if a > 0

it = 0 if ( a = 0 & b > 0 )

ex k being Integer st

( k = b & it = a #Z k ) if b is Integer

;

consistency it = a #R b if a > 0

it = 0 if ( a = 0 & b > 0 )

ex k being Integer st

( k = b & it = a #Z k ) if b is Integer

;

for b

( ( a > 0 & a = 0 & b > 0 implies ( b

( k = b & b

( k = b & b

proof end;

existence ( ( a > 0 implies ex b

( k = b & b

proof end;

uniqueness for b

( ( a > 0 & b

( k = b & b

( k = b & b

:: deftheorem Def2 defines to_power POWER:def 2 :

for a, b, b_{3} being real number holds

( ( a > 0 implies ( b_{3} = a to_power b iff b_{3} = a #R b ) ) & ( a = 0 & b > 0 implies ( b_{3} = a to_power b iff b_{3} = 0 ) ) & ( b is Integer implies ( b_{3} = a to_power b iff ex k being Integer st

( k = b & b_{3} = a #Z k ) ) ) );

for a, b, b

( ( a > 0 implies ( b

( k = b & b

definition

let a, b be Real;

:: original: to_power

redefine func a to_power b -> Real;

coherence

a to_power b is Real by XREAL_0:def 1;

end;
:: original: to_power

redefine func a to_power b -> Real;

coherence

a to_power b is Real by XREAL_0:def 1;

theorem :: POWER:30

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

(a * b) to_power c = (a to_power c) * (b to_power c)

(a * b) to_power c = (a to_power c) * (b to_power c)

proof end;

theorem Th31: :: POWER:31

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

(a / b) to_power c = (a to_power c) / (b to_power c)

(a / b) to_power c = (a to_power c) / (b to_power c)

proof end;

registration
end;

theorem :: POWER:43

theorem Th45: :: POWER:45

for a being real number

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

a to_power (1 / n) = n -root a

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

a to_power (1 / n) = n -root a

proof end;

theorem :: POWER:49

definition

let a, b be real number ;

assume that

A1: a > 0 and

A2: a <> 1 and

A3: b > 0 ;

existence

ex b_{1} being real number st a to_power b_{1} = b

for b_{1}, b_{2} being real number st a to_power b_{1} = b & a to_power b_{2} = b holds

b_{1} = b_{2}
by A1, A2, Th50;

end;
assume that

A1: a > 0 and

A2: a <> 1 and

A3: b > 0 ;

existence

ex b

proof end;

uniqueness for b

b

:: deftheorem Def3 defines log POWER:def 3 :

for a, b being real number st a > 0 & a <> 1 & b > 0 holds

for b_{3} being real number holds

( b_{3} = log (a,b) iff a to_power b_{3} = b );

for a, b being real number st a > 0 & a <> 1 & b > 0 holds

for b

( b

definition

let a, b be Real;

:: original: log

redefine func log (a,b) -> Real;

coherence

log (a,b) is Real by XREAL_0:def 1;

end;
:: original: log

redefine func log (a,b) -> Real;

coherence

log (a,b) is Real by XREAL_0:def 1;

theorem :: POWER:53

for a, b, c being real number st a > 0 & a <> 1 & b > 0 & c > 0 holds

(log (a,b)) + (log (a,c)) = log (a,(b * c))

(log (a,b)) + (log (a,c)) = log (a,(b * c))

proof end;

theorem :: POWER:54

for a, b, c being real number st a > 0 & a <> 1 & b > 0 & c > 0 holds

(log (a,b)) - (log (a,c)) = log (a,(b / c))

(log (a,b)) - (log (a,c)) = log (a,(b / c))

proof end;

theorem :: POWER:55

for a, b, c being real number st a > 0 & a <> 1 & b > 0 holds

log (a,(b to_power c)) = c * (log (a,b))

log (a,(b to_power c)) = c * (log (a,b))

proof end;

theorem :: POWER:56

for a, b, c being real number st a > 0 & a <> 1 & b > 0 & b <> 1 & c > 0 holds

log (a,c) = (log (a,b)) * (log (b,c))

log (a,c) = (log (a,b)) * (log (b,c))

proof end;

theorem :: POWER:59

for s being Real_Sequence st ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds

s is convergent

s is convergent

proof end;

definition

ex b_{1} being real number st

for s being Real_Sequence st ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds

b_{1} = lim s

for b_{1}, b_{2} being real number st ( for s being Real_Sequence st ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds

b_{1} = lim s ) & ( for s being Real_Sequence st ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds

b_{2} = lim s ) holds

b_{1} = b_{2}
end;

func number_e -> real number means :: POWER:def 4

for s being Real_Sequence st ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds

it = lim s;

existence for s being Real_Sequence st ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds

it = lim s;

ex b

for s being Real_Sequence st ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines number_e POWER:def 4 :

for b_{1} being real number holds

( b_{1} = number_e iff for s being Real_Sequence st ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds

b_{1} = lim s );

for b

( b

b

definition
end;