The abstract of the Mizar article:

Real Exponents and Logarithms

by

Konrad Raczkowski, and

Andrzej Nedzusiak

Received October 1, 1990

MML identifier: POWER

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM, INT_1, RAT_1, ARYTM_1, PREPOWER, FUNCT_1, ARYTM_3, SEQ_1,
      SEQ_2, ORDINAL2, GROUP_1, RELAT_1, SQUARE_1, SEQ_4, ABSVALUE, PROB_1,
      POWER;
 notation SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, ABSVALUE,
      NAT_1, SEQ_1, SEQ_2, SEQM_3, INT_1, SQUARE_1, SEQ_4, RAT_1, PREPOWER;
 constructors REAL_1, NAT_1, SEQ_2, SEQM_3, SQUARE_1, SEQ_4, PREPOWER,
      MEMBERED, XBOOLE_0;
 clusters INT_1, XREAL_0, NEWTON, SQUARE_1, PREPOWER, RAT_1, NAT_1, MEMBERED,
      ZFMISC_1, XBOOLE_0, ORDINAL2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

reserve x for set;
reserve a, b, c, d, e for real number;
reserve m, n, m1, m2 for Nat;
reserve k, l for Integer;
reserve p for Rational;

theorem :: POWER:1
(ex m st n=2*m) implies (-a) |^ n = a |^ n;

theorem :: POWER:2
(ex m st n=2*m+1) implies (-a) |^ n = - a |^ n;

theorem :: POWER:3
a>=0 or (ex m st n=2*m) implies a |^ n >= 0;

definition let n; let a be real number;
func n-root a -> real number equals
:: POWER:def 1
  n -Root a if a>=0 & n>=1,
        - n -Root (-a) if a<0 & ex m st n=2*m+1;
end;

definition let n; let a be Real;
 redefine func n-root a -> Real;
end;

canceled;

theorem :: POWER:5
  n>=1 & a>=0 or (ex m st n=2*m+1) implies
(n-root a) |^ n = a & n-root (a |^ n) = a;


theorem :: POWER:6
n>=1 implies n-root 0 = 0;

theorem :: POWER:7
  n>=1 implies n-root 1 = 1;

theorem :: POWER:8
a>=0 & n>=1 implies n-root a >= 0;

theorem :: POWER:9
  (ex m st n=2*m+1) implies n-root (-1) = -1;

theorem :: POWER:10
  1-root a = a;

theorem :: POWER:11
(ex m st n = 2*m + 1) implies n-root a = - n-root (-a);

theorem :: POWER:12
n>=1 & a>=0 & b>=0 or (ex m st n=2*m+1) implies
  n-root (a*b) = n-root a * n-root b;

theorem :: POWER:13
a>0 & n>=1 or (a<>0 & ex m st n = 2*m+1) implies n-root (1/a) = 1/(n-root a);

theorem :: POWER:14
  (a>=0 & b>0 & n>=1) or (b<>0 & ex m st n=2*m+1) implies
n-root (a/b) = n-root a / n-root b;

theorem :: POWER:15
  (a>=0 & n>=1 & m>=1) or (ex m1,m2 st n=2*m1+1 & m=2*m2+1) implies
n-root (m-root a) = (n*m)-root a;

theorem :: POWER:16
  (a>=0 & n>=1 & m>=1) or (ex m1,m2 st n=2*m1+1 & m=2*m2+1) implies
n-root a * m-root a = (n*m)-root (a |^ (n+m));

theorem :: POWER:17
  a<=b & (0<=a & n>=1 or ex m st n=2*m+1) implies n-root a <= n-root b;

theorem :: POWER:18
  a<b & (a>=0 & n>=1 or ex m st n=2*m+1) implies n-root a < n-root b;

theorem :: POWER:19
a>=1 & n>=1 implies n-root a >= 1 & a >= n-root a;

theorem :: POWER:20
  a<=-1 & (ex m st n=2*m+1) implies n-root a <= -1 & a <= n-root a;

theorem :: POWER:21
a>=0 & a<1 & n>=1 implies a <= n-root a & n-root a < 1;

theorem :: POWER:22
  a>-1 & a<=0 & (ex m st n=2*m+1) implies a >= n-root a & n-root a > -1;

theorem :: POWER:23
a>0 & n>=1 implies n-root a - 1 <= (a-1)/n;

theorem :: POWER:24
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 number;
  func a to_power b -> real number means
:: POWER:def 2
  it = a #R b if a > 0,
  it = 0 if a = 0 & b > 0,
  it = 1 if a = 0 & b = 0,
  ex k st k = b & it = a #Z k if a < 0 & b is Integer;
end;

definition let a,b be Real;
 redefine func a to_power b -> Real;
end;

canceled 4;

theorem :: POWER:29
  a to_power 0 = 1;

theorem :: POWER:30
  a to_power 1 = a;

theorem :: POWER:31
 1 to_power a = 1;

theorem :: POWER:32
a > 0 implies a to_power (b+c) = a to_power b * a to_power c;

theorem :: POWER:33
a > 0 implies a to_power (-c) = 1 / a to_power c;

theorem :: POWER:34
a > 0 implies a to_power (b-c) = a to_power b / a to_power c;

theorem :: POWER:35
  a>0 & b>0 implies (a*b) to_power c = a to_power c*b to_power c;

theorem :: POWER:36
a>0 & b>0 implies (a/b) to_power c = a to_power c/b to_power c;

theorem :: POWER:37
a>0 implies (1/a) to_power b = a to_power (-b);

theorem :: POWER:38
a > 0 implies a to_power b to_power c = a to_power (b * c);

theorem :: POWER:39
 a > 0 implies a to_power b > 0;

theorem :: POWER:40
a > 1 & b > 0 implies a to_power b > 1;

theorem :: POWER:41
 a > 1 & b < 0 implies a to_power b < 1;

theorem :: POWER:42
  a > 0 & a < b & c > 0 implies a to_power c < b to_power c;

theorem :: POWER:43
  a > 0 & a < b & c < 0 implies a to_power c > b to_power c;

theorem :: POWER:44
a < b & c > 1 implies c to_power a < c to_power b;

theorem :: POWER:45
a < b & c > 0 & c < 1 implies c to_power a > c to_power b;

theorem :: POWER:46
a<>0 implies a to_power n = a |^ n;

theorem :: POWER:47
  n>=1 implies a to_power n = a |^ n;

theorem :: POWER:48
 a<>0 implies a to_power n = a|^n;

theorem :: POWER:49
  n>=1 implies a to_power n = a|^n;

theorem :: POWER:50
a<>0 implies a to_power k = a #Z k;

theorem :: POWER:51
a>0 implies a to_power p = a #Q p;

theorem :: POWER:52
a>=0 & n>=1 implies a to_power (1/n) = n-root a;

theorem :: POWER:53
a to_power 2 = a^2;

theorem :: POWER:54
a<>0 & (ex l st k = 2*l) implies (-a) to_power k = a to_power k;

theorem :: POWER:55
  a<>0 & (ex l st k = 2*l + 1) implies (-a) to_power k = -(a to_power k);

theorem :: POWER:56
-1 < a implies (1 + a) to_power n >= 1 + n * a;

theorem :: POWER:57
a>0 & a<>1 & c <>d implies a to_power c <> a to_power d;

definition let a,b be real number;
assume that  a>0 & a<>1 and  b>0;
func log(a,b) -> real number means
:: POWER:def 3
a to_power it = b;
end;

definition let a,b be Real;
 redefine func log(a,b) -> Real;
end;

canceled;

theorem :: POWER:59
   a>0 & a<>1 implies log(a,1) = 0;

theorem :: POWER:60
   a>0 & a<>1 implies log(a,a) = 1;

theorem :: POWER:61
   a>0 & a<>1 & b>0 & c>0 implies log(a,b) + log(a,c) = log(a,b*c);

theorem :: POWER:62
   a>0 & a<>1 & b>0 & c>0 implies log(a,b) - log(a,c) = log(a,b/c);

theorem :: POWER:63
   a>0 & a<>1 & b>0 implies log(a,b to_power c) = c * log(a,b);

theorem :: POWER:64
   a>0 & a<>1 & b>0 & b<>1 & c>0 implies log(a,c) = log(a,b)*log(b,c);

theorem :: POWER:65
   a>1 & b>0 & c>b implies log(a,c) > log(a,b);

theorem :: POWER:66
   a>0 & a<1 & b>0 & c>b implies log(a,c) < log(a,b);

theorem :: POWER:67
  for s being Real_Sequence st for n holds s.n = (1 + 1/(n+1)) to_power (n+1)
holds s is convergent;

definition
func number_e -> real number 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;

definition
 redefine func number_e -> Real;
end;