:: Real Exponents and Logarithms :: by Konrad Raczkowski and Andrzej N\c{e}dzusiak :: :: Received October 1, 1990 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, INT_1, RAT_1, RELAT_1, ARYTM_1, NEWTON, ARYTM_3, CARD_1, PREPOWER, FUNCT_1, XXREAL_0, NAT_1, REAL_1, SEQ_1, SEQ_2, ORDINAL2, SQUARE_1, XXREAL_2, SEQ_4, COMPLEX1, VALUED_0, POWER, ABIAN, ORDINAL1; notations SUBSET_1, NEWTON, ORDINAL1, XCMPLX_0, XREAL_0, XXREAL_0, COMPLEX1, INT_1, RAT_1, REAL_1, NUMBERS, NAT_1, SEQ_1, SEQ_2, COMSEQ_2, SEQM_3, SQUARE_1, SEQ_4, PREPOWER, ABIAN, XXREAL_2; constructors REAL_1, SQUARE_1, NAT_1, SEQ_2, SEQM_3, SEQ_4, NEWTON, PREPOWER, XXREAL_2, RELSET_1, ABIAN, BINOP_2, COMSEQ_2; registrations XREAL_0, SQUARE_1, NAT_1, INT_1, RAT_1, MEMBERED, NEWTON, PREPOWER, SEQ_4, ABIAN, ORDINAL1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve x for set; reserve a, b, c, d, e for Real; reserve m, n, m1, m2 for Nat; reserve k, l for Integer; reserve p for Rational; theorem :: POWER:1 n is even implies (-a) |^ n = a |^ n; theorem :: POWER:2 n is odd implies (-a) |^ n = - a |^ n; theorem :: POWER:3 a>=0 or n is even implies a |^ n >= 0; definition let n be natural Number; let a be Real; func n-root a -> Real equals :: POWER:def 1 n -Root a if a>=0 & n>=1, -n -Root (-a) if a<0 & n is odd; end; theorem :: POWER:4 for n being Nat st n>=1 & a>=0 or n is odd holds (n-root a) |^ n = a & n-root (a |^ n) = a; theorem :: POWER:5 for n being Nat st n>=1 holds n-root 0 = 0; theorem :: POWER:6 n>=1 implies n-root 1 = 1; theorem :: POWER:7 a>=0 & n>=1 implies n-root a >= 0; theorem :: POWER:8 n is odd implies n-root (-1) = -1; theorem :: POWER:9 1-root a = a; theorem :: POWER:10 n is odd implies n-root a = - n-root (-a); theorem :: POWER:11 n>=1 & a>=0 & b>=0 or n is odd implies n-root (a*b) = n-root a * n-root b; theorem :: POWER:12 a>0 & n>=1 or a<>0 & n is odd implies n-root (1/a) = 1/(n-root a); theorem :: POWER:13 a>=0 & b>0 & n>=1 or b<>0 & n is odd implies n-root (a/b) = n-root a / n-root b; theorem :: POWER:14 a>=0 & n>=1 & m>=1 or n is odd & m is odd implies n-root (m-root a) = (n*m)-root a; theorem :: POWER:15 a>=0 & n>=1 & m>=1 or n is odd & m is odd implies n-root a * m-root a = (n*m)-root (a |^ (n+m)); theorem :: POWER:16 a<=b & (0<=a & n>=1 or n is odd) implies n-root a <= n-root b; theorem :: POWER:17 a=0 & n>=1 or n is odd) implies n-root a < n-root b; theorem :: POWER:18 a>=1 & n>=1 implies n-root a >= 1 & a >= n-root a; theorem :: POWER:19 a<=-1 & n is odd implies n-root a <= -1 & a <= n-root a; theorem :: POWER:20 a>=0 & a<1 & n>=1 implies a <= n-root a & n-root a < 1; theorem :: POWER:21 a>-1 & a<=0 & n is odd implies a >= n-root a & n-root a > -1; theorem :: POWER:22 a>0 & n>=1 implies n-root a - 1 <= (a-1)/n; theorem :: POWER:23 for s being Real_Sequence, a st a > 0 & (for n st n>=1 holds s.n = n-root a) holds s is convergent & lim s = 1; definition let a,b be Real; func a to_power b -> Real means :: POWER:def 2 it = a #R b if a > 0, it = 0 if a = 0 & b > 0, ex k st k = b & it = a #Z k if b is Integer; end; theorem :: POWER:24 a to_power 0 = 1; theorem :: POWER:25 a to_power 1 = a; theorem :: POWER:26 1 to_power a = 1; theorem :: POWER:27 a > 0 implies a to_power (b+c) = a to_power b * a to_power c; theorem :: POWER:28 a > 0 implies a to_power (-c) = 1 / a to_power c; theorem :: POWER:29 a > 0 implies a to_power (b-c) = a to_power b / a to_power c; theorem :: POWER:30 a>0 & b>0 implies (a*b) to_power c = a to_power c*b to_power c; theorem :: POWER:31 a>0 & b>0 implies (a/b) to_power c = a to_power c/b to_power c; theorem :: POWER:32 a>0 implies (1/a) to_power b = a to_power (-b); theorem :: POWER:33 a > 0 implies a to_power b to_power c = a to_power (b * c); theorem :: POWER:34 a > 0 implies a to_power b > 0; theorem :: POWER:35 a > 1 & b > 0 implies a to_power b > 1; theorem :: POWER:36 a > 1 & b < 0 implies a to_power b < 1; theorem :: POWER:37 a > 0 & a < b & c > 0 implies a to_power c < b to_power c; theorem :: POWER:38 a > 0 & a < b & c < 0 implies a to_power c > b to_power c; theorem :: POWER:39 a < b & c > 1 implies c to_power a < c to_power b; theorem :: POWER:40 a < b & c > 0 & c < 1 implies c to_power a > c to_power b; registration let a be Real, n be Nat; identify a to_power n with a |^ n; end; theorem :: POWER:41 for n be Nat holds a to_power n = a |^ n; theorem :: POWER:42 k <> 0 implies 0 to_power k = 0; theorem :: POWER:43 a to_power k = a #Z k; theorem :: POWER:44 a>0 implies a to_power p = a #Q p; theorem :: POWER:45 a>=0 & n>=1 implies a to_power (1/n) = n-root a; theorem :: POWER:46 a to_power 2 = a^2; theorem :: POWER:47 k is even implies (-a) to_power k = a to_power k; theorem :: POWER:48 k is odd implies (-a) to_power k = -(a to_power k); theorem :: POWER:49 -1 < a implies (1 + a) to_power n >= 1 + n * a; theorem :: POWER:50 a>0 & a<>1 & c <>d implies a to_power c <> a to_power d; definition let a,b be Real; assume that a>0 and a<>1 and b>0; func log(a,b) -> Real means :: POWER:def 3 a to_power it = b; end; theorem :: POWER:51 a>0 & a<>1 implies log(a,1) = 0; theorem :: POWER:52 a>0 & a<>1 implies log(a,a) = 1; theorem :: POWER:53 a>0 & a<>1 & b>0 & c>0 implies log(a,b) + log(a,c) = log(a,b*c); theorem :: POWER:54 a>0 & a<>1 & b>0 & c>0 implies log(a,b) - log(a,c) = log(a,b/c); theorem :: POWER:55 a>0 & a<>1 & b>0 implies log(a,b to_power c) = c * log(a,b); theorem :: POWER:56 a>0 & a<>1 & b>0 & b<>1 & c>0 implies log(a,c) = log(a,b)*log(b,c); theorem :: POWER:57 a>1 & b>0 & c>b implies log(a,c) > log(a,b); theorem :: POWER:58 a>0 & a<1 & b>0 & c>b implies log(a,c) < log(a,b); 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; definition func number_e -> Real means :: POWER:def 4 for s being Real_Sequence st for n holds s.n = (1 + 1/(n+1)) to_power (n+1) holds it = lim s; end; theorem :: POWER:60 2 to_power 2 = 4; theorem :: POWER:61 2 to_power 3 = 8; theorem :: POWER:62 2 to_power 4 = 16; theorem :: POWER:63 2 to_power 5 = 32; theorem :: POWER:64 2 to_power 6 = 64;