:: Real Exponents and Logarithms :: by Konrad Raczkowski and Andrzej N\c{e}dzusiak :: :: Received October 1, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin theorem Th1: :: POWER:1 for a being real number for n being Element of NAT st n is even holds (- a) |^ n = a |^ n proofend; theorem Th2: :: POWER:2 for a being real number for n being Element of NAT st n is odd holds (- a) |^ n = - (a |^ n) proofend; theorem Th3: :: POWER:3 for a being real number for n being Element of NAT st ( a >= 0 or n is even ) holds a |^ n >= 0 proofend; definition let n be Nat; let a be real number ; funcn -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 for b1 being real number st a >= 0 & n >= 1 & a < 0 & n is odd holds ( b1 = n -Root a iff b1 = - (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; :: 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)) ) ); definition let n be Nat; let a be Real; :: original:-root redefine funcn -root a -> Real; coherence n -root a is Real by XREAL_0:def_1; end; 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 ) proofend; theorem Th5: :: POWER:5 for n being Nat st n >= 1 holds n -root 0 = 0 proofend; theorem :: POWER:6 for n being Element of NAT st n >= 1 holds n -root 1 = 1 proofend; theorem Th7: :: POWER:7 for a being real number for n being Element of NAT st a >= 0 & n >= 1 holds n -root a >= 0 proofend; theorem :: POWER:8 for n being Element of NAT st n is odd holds n -root (- 1) = - 1 proofend; theorem :: POWER:9 for a being real number holds 1 -root a = a proofend; theorem Th10: :: POWER:10 for a being real number for n being Element of NAT st n is odd holds n -root a = - (n -root (- a)) proofend; 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) proofend; 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) proofend; 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) proofend; 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 proofend; 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)) proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 proofend; 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 ) proofend; definition let a, b be real number ; funca 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 for b1 being real number holds ( ( a > 0 & a = 0 & b > 0 implies ( b1 = a #R b iff b1 = 0 ) ) & ( a > 0 & b is Integer implies ( b1 = a #R b iff ex k being Integer st ( k = b & b1 = a #Z k ) ) ) & ( a = 0 & b > 0 & b is Integer implies ( b1 = 0 iff ex k being Integer st ( k = b & b1 = a #Z k ) ) ) ) proofend; existence ( ( a > 0 implies ex b1 being real number st b1 = a #R b ) & ( a = 0 & b > 0 implies ex b1 being real number st b1 = 0 ) & ( b is Integer implies ex b1 being real number ex k being Integer st ( k = b & b1 = a #Z k ) ) ) proofend; uniqueness for b1, b2 being real number holds ( ( a > 0 & b1 = a #R b & b2 = a #R b implies b1 = b2 ) & ( a = 0 & b > 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) & ( b is Integer & ex k being Integer st ( k = b & b1 = a #Z k ) & ex k being Integer st ( k = b & b2 = a #Z k ) implies b1 = b2 ) ) ; end; :: deftheorem Def2 defines to_power POWER:def_2_:_ for a, b, b3 being real number holds ( ( a > 0 implies ( b3 = a to_power b iff b3 = a #R b ) ) & ( a = 0 & b > 0 implies ( b3 = a to_power b iff b3 = 0 ) ) & ( b is Integer implies ( b3 = a to_power b iff ex k being Integer st ( k = b & b3 = a #Z k ) ) ) ); definition let a, b be Real; :: original:to_power redefine funca to_power b -> Real; coherence a to_power b is Real by XREAL_0:def_1; end; theorem Th24: :: POWER:24 for a being real number holds a to_power 0 = 1 proofend; theorem Th25: :: POWER:25 for a being real number holds a to_power 1 = a proofend; theorem Th26: :: POWER:26 for a being real number holds 1 to_power a = 1 proofend; theorem Th27: :: POWER:27 for a, b, c being real number st a > 0 holds a to_power (b + c) = (a to_power b) * (a to_power c) proofend; theorem Th28: :: POWER:28 for a, c being real number st a > 0 holds a to_power (- c) = 1 / (a to_power c) proofend; theorem Th29: :: POWER:29 for a, b, c being real number st a > 0 holds a to_power (b - c) = (a to_power b) / (a to_power c) proofend; 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) proofend; 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) proofend; theorem Th32: :: POWER:32 for a, b being real number st a > 0 holds (1 / a) to_power b = a to_power (- b) proofend; theorem Th33: :: POWER:33 for a, b, c being real number st a > 0 holds (a to_power b) to_power c = a to_power (b * c) proofend; theorem Th34: :: POWER:34 for a, b being real number st a > 0 holds a to_power b > 0 proofend; theorem Th35: :: POWER:35 for a, b being real number st a > 1 & b > 0 holds a to_power b > 1 proofend; theorem Th36: :: POWER:36 for a, b being real number st a > 1 & b < 0 holds a to_power b < 1 proofend; theorem :: POWER:37 for a, b, c being real number st a > 0 & a < b & c > 0 holds a to_power c < b to_power c proofend; theorem :: POWER:38 for a, b, c being real number st a > 0 & a < b & c < 0 holds a to_power c > b to_power c proofend; theorem Th39: :: POWER:39 for a, b, c being real number st a < b & c > 1 holds c to_power a < c to_power b proofend; theorem Th40: :: POWER:40 for a, b, c being real number st a < b & c > 0 & c < 1 holds c to_power a > c to_power b proofend; registration let a be real number ; let n be Nat; identifya to_power n with a |^ n; compatibility a to_power n = a |^ n proofend; end; theorem :: POWER:41 for a being real number for n being Nat holds a to_power n = a |^ n ; theorem Th42: :: POWER:42 for k being Integer st k <> 0 holds 0 to_power k = 0 proofend; theorem :: POWER:43 for a being real number for k being Integer holds a to_power k = a #Z k by Def2; theorem Th44: :: POWER:44 for a being real number for p being Rational st a > 0 holds a to_power p = a #Q p proofend; 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 proofend; theorem Th46: :: POWER:46 for a being real number holds a to_power 2 = a ^2 proofend; theorem Th47: :: POWER:47 for a being real number for k being Integer st k is even holds (- a) to_power k = a to_power k proofend; theorem :: POWER:48 for a being real number for k being Integer st k is odd holds (- a) to_power k = - (a to_power k) proofend; theorem :: POWER:49 for a being real number for n being Element of NAT st - 1 < a holds (1 + a) to_power n >= 1 + (n * a) by PREPOWER:16; theorem Th50: :: POWER:50 for a, c, d being real number st a > 0 & a <> 1 & c <> d holds a to_power c <> a to_power d proofend; definition let a, b be real number ; assume that A1: a > 0 and A2: a <> 1 and A3: b > 0 ; func log (a,b) -> real number means :Def3: :: POWER:def 3 a to_power it = b; existence ex b1 being real number st a to_power b1 = b proofend; uniqueness for b1, b2 being real number st a to_power b1 = b & a to_power b2 = b holds b1 = b2 by A1, A2, Th50; end; :: deftheorem Def3 defines log POWER:def_3_:_ for a, b being real number st a > 0 & a <> 1 & b > 0 holds for b3 being real number holds ( b3 = log (a,b) iff a to_power b3 = 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; theorem :: POWER:51 for a being real number st a > 0 & a <> 1 holds log (a,1) = 0 proofend; theorem :: POWER:52 for a being real number st a > 0 & a <> 1 holds log (a,a) = 1 proofend; 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)) proofend; 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)) proofend; 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)) proofend; 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)) proofend; theorem :: POWER:57 for a, b, c being real number st a > 1 & b > 0 & c > b holds log (a,c) > log (a,b) proofend; theorem :: POWER:58 for a, b, c being real number st a > 0 & a < 1 & b > 0 & c > b holds log (a,c) < log (a,b) proofend; 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 proofend; definition 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 ex b1 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 b1 = lim s proofend; uniqueness for b1, b2 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 b1 = 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 b2 = lim s ) holds b1 = b2 proofend; end; :: deftheorem defines number_e POWER:def_4_:_ for b1 being real number holds ( b1 = 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 b1 = lim s ); definition :: original:number_e redefine func number_e -> Real; coherence number_e is Real by XREAL_0:def_1; end; theorem Th60: :: POWER:60 2 to_power 2 = 4 proofend; theorem Th61: :: POWER:61 2 to_power 3 = 8 proofend; theorem :: POWER:62 2 to_power 4 = 16 proofend; theorem :: POWER:63 2 to_power 5 = 32 proofend; theorem :: POWER:64 2 to_power 6 = 64 proofend;