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

::

:: Received October 1, 1990

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

definition

let n be natural Number ;

let a be Real;

for b_{1} being Real 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 ) & ( a < 0 & n is odd implies - (n -Root (- a)) is Real ) ) ;

end;
let a be Real;

func n -root a -> Real 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 ) & ( a < 0 & n is odd implies - (n -Root (- a)) is Real ) ) ;

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

for n being natural Number

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

for a being Real holds

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

theorem :: POWER:4

for a being Real

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

for n being 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 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

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

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

for n being 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

for n being 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 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

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

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

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

n -root a <= n -root b

for n being 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

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

n -root a < n -root b

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

n -root a < n -root b

proof end;

theorem Th20: :: POWER:20

for a being Real

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

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

for n being 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

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

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

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

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

proof end;

theorem Th23: :: POWER:23

for s being Real_Sequence

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

s . n = n -root a ) holds

( s is convergent & lim s = 1 )

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

for b_{1} being Real 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 st b_{1} = a #R b ) & ( a = 0 & b > 0 implies ex b_{1} being Real st b_{1} = 0 ) & ( b is Integer implies ex b_{1} being Real ex k being Integer st

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

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

theorem :: POWER:49

definition

let a, b be Real;

assume that

A1: a > 0 and

A2: a <> 1 and

A3: b > 0 ;

existence

ex b_{1} being Real st a to_power b_{1} = b

for b_{1}, b_{2} being Real 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 st a > 0 & a <> 1 & b > 0 holds

for b_{3} being Real holds

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

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

for b

( b

theorem :: POWER:53

for a, b, c being Real 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 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:56

for a, b, c being Real 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 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 st

for s being Real_Sequence st ( for n being Nat holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds

b_{1} = lim s

for b_{1}, b_{2} being Real st ( for s being Real_Sequence st ( for n being 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 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 means :: POWER:def 4

for s being Real_Sequence st ( for n being 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 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 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 holds

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

b_{1} = lim s );

for b

( b

b