:: 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
::           (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, XREAL_0, ORDINAL1, 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;
 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,
      SEQ_1, XXREAL_2, RELSET_1, ABIAN, BINOP_2, COMSEQ_2;
 registrations NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, INT_1, RAT_1,
      MEMBERED, NEWTON, PREPOWER, XBOOLE_0, SEQ_4, ABIAN, COMSEQ_2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions SQUARE_1, XCMPLX_0, INT_1, ABIAN, XXREAL_2;
 theorems ABSVALUE, NAT_1, SEQ_2, SEQM_3, INT_1, SEQ_4, NEWTON, PREPOWER,
      TARSKI, FUNCT_2, XREAL_0, XCMPLX_1, XREAL_1, XXREAL_0, ABIAN;
 schemes SEQ_1;

begin

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

theorem Th1:
  n is even implies (-a) |^ n = a |^ n
proof
  given m such that
A1: n=2*m;
  thus
  (-a) |^ n = ((-a) |^ (1+1)) |^ m by A1,NEWTON:9
    .= ((-a) |^ (0+1) * (-a) |^ (0+1)) |^ m by NEWTON:8
    .= ((-a) |^ 0 * (-a) * (-a) |^ (0+1)) |^ m by NEWTON:6
    .= ((-a) |^ 0 * (-a) * ((-a) |^ 0*(-a))) |^ m by NEWTON:6
    .= ((-a) GeoSeq.0 * (-a) * ((-a) |^ 0 * (-a))) |^ m by PREPOWER:def 1
    .= ((-a) GeoSeq.0 * (-a) * ((-a) GeoSeq.0 * (-a))) |^ m by PREPOWER:def 1
    .= ((-a) GeoSeq.0 * (-a) * (1 * (-a))) |^ m by PREPOWER:3
    .= (1*(-a) * (1*(-a))) |^ m by PREPOWER:3
    .= (a * a) |^ m
    .= ((a GeoSeq.0*a) * (1*a)) |^ m by PREPOWER:3
    .= ((a GeoSeq.0*a) * (a GeoSeq.0*a)) |^ m by PREPOWER:3
    .= ((a GeoSeq.0*a) * (a |^ 0*a)) |^ m by PREPOWER:def 1
    .= ((a |^ 0*a) * (a |^ 0*a)) |^ m by PREPOWER:def 1
    .= ((a |^ 0*a) * a |^ (0+1)) |^ m by NEWTON:6
    .= (a |^ (0+1) * a |^ (0+1)) |^ m by NEWTON:6
    .= (a |^ (1+1)) |^ m by NEWTON:8
    .= a |^ n by A1,NEWTON:9;
end;

theorem Th2:
  n is odd implies (-a) |^ n = - a |^ n
proof
  assume n is odd;
  then consider m such that
A1: n=2*m+1 by ABIAN:9;
  thus
  (-a) |^ n = (-a) |^ (2*m) * (-a) by A1,NEWTON:6
    .= a |^ (2*m) * (-a) by Th1
    .= -a |^ (2*m) * a
    .= -a |^ n by A1,NEWTON:6;
end;

theorem Th3:
  a>=0 or n is even implies a |^ n >= 0
proof
  assume
A1: a>=0 or n is even;
A2: now
    let a,n such that
A3: a>=0;
    now per cases by A3;
      suppose a>0;
        hence a |^ n >= 0 by PREPOWER:6;
      end;
      suppose
A4:     a=0;
        now per cases by NAT_1:6;
          suppose
A5:         n=0;
            a |^ n = a GeoSeq.n by PREPOWER:def 1
              .= 1 by A5,PREPOWER:3;
            hence a |^ n >= 0;
          end;
          suppose
        ex m being Nat st n = m+1;
            then consider m being Nat such that
A6:        n = m + 1;
            a |^ n = a |^ m * a by A6,NEWTON:6
              .= 0 by A4;
            hence a |^ n >= 0;
          end;
        end;
        hence a |^ n >= 0;
      end;
    end;
    hence a |^ n >= 0;
  end;
  now
    assume
A7: n is even;
     now per cases;
      suppose a>=0;
        hence thesis by A2;
      end;
      suppose a<0;
        then (-a) |^ n >= 0 by A2;
        hence thesis by A7,Th1;
      end;
    end;
    hence thesis;
  end;
  hence thesis by A1,A2;
end;

definition
  let n be Nat;
  let a be real number;
  func n-root a -> real number equals
  :Def1:
  n -Root a if a>=0 & n>=1,
  -n -Root (-a) if a<0 & n is odd;
  consistency;
  coherence;
end;

definition
  let n be Nat;
  let a be Real;
  redefine func n-root a -> Real;
  coherence by XREAL_0:def 1;
end;

theorem
  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
  let n be Nat;
  assume
A1: n>=1 & a>=0 or n is odd;
A2: now
    assume that
A3: n>=1 and
A4: a>=0;
A5: n-root a = n -Root a by A3,A4,Def1;
 now per cases by A4;
      suppose a>0;
        hence a |^ n >= 0 by PREPOWER:6;
      end;
      suppose a=0;
        hence a |^ n >= 0;
      end;
    end;
    then n-root (a |^ n) = n -Root (a |^ n) by A3,Def1;
    hence thesis by A3,A4,A5,PREPOWER:19;
  end;
 now
    assume
A6: n is odd;
    then
A7: ex m st n=2*m+1 by ABIAN:9;
A8: n>=1 by A6,ABIAN:12;
 now per cases;
      suppose a>=0;
        hence thesis by A2,A8;
      end;
      suppose
A9:    a<0;
then A10:    -a>0 by XREAL_1:58;
        thus
        (n-root a) |^ n = (- n -Root (-a)) |^ n by A7,A9,Def1
          .= -(n -Root (-a)) |^ n by A7,Th2
          .= -(-a) by A8,A9,PREPOWER:19
          .= a;
    (-a) |^ n > 0 by A10,PREPOWER:6;
then     -a |^ n > 0 by A7,Th2;
then     a |^ n < 0;
        hence n-root (a |^ n) = - n -Root (-a |^ n) by A7,Def1
          .= - n -Root ((-a) |^ n) by A7,Th2
          .= -(-a) by A8,A9,PREPOWER:19
          .= a;
      end;
    end;
    hence thesis;
  end;
  hence thesis by A1,A2;
end;

theorem Th5:
  for n being Nat st n>=1 holds n-root 0 = 0
proof
  let n be Nat;
  assume
A1: n>=1;
  hence n-root 0 = n -Root 0 by Def1
    .= 0 by A1,PREPOWER:def 2;
end;

theorem
  n>=1 implies n-root 1 = 1
proof
  assume
A1: n>=1;
  hence n-root 1 = n -Root 1 by Def1
    .= 1 by A1,PREPOWER:20;
end;

theorem Th7:
  a>=0 & n>=1 implies n-root a >= 0
proof
  assume that
A1: a>=0 and
A2: n>=1;
 now per cases by A1;
    suppose
A3:   a>0;
   n-root a = n -Root a by A1,A2,Def1;
      hence thesis by A2,A3,PREPOWER:def 2;
    end;
    suppose
A4:   a=0;
   n-root a = n -Root a by A1,A2,Def1
        .= 0 by A2,A4,PREPOWER:def 2;
      hence thesis;
    end;
  end;
  hence thesis;
end;

theorem
  n is odd implies n-root (-1) = -1
proof
  assume
A1: n is odd;
   then
A2: n>=1 by ABIAN:12;
  thus
  n-root (-1) = - n -Root (-(-1)) by A1,Def1
    .= - 1 by A2,PREPOWER:20;
end;

theorem
  1-root a = a
proof
 now per cases;
    suppose
A1:   a>=0;
      hence 1-root a = 1 -Root a by Def1
        .= a by A1,PREPOWER:21;
    end;
    suppose
A2:   a<0;
   1 = 2*0 + 1;
      hence 1-root a = - 1 -Root (-a) by A2,Def1
        .= -(-a) by A2,PREPOWER:21
        .= a;
    end;
  end;
  hence thesis;
end;

theorem Th10:
  n is odd implies n-root a = - n-root (-a)
proof
  assume
A1: n is odd;
    then
A2: ex m st n = 2*m + 1 by ABIAN:9;
A3: n>=1 by A1,ABIAN:12;
 now per cases;
    suppose
A4:   a<0;
      thus
      then n-root a = - n -Root (-a) by A2,Def1
        .= - n-root (-a) by A3,A4,Def1;
    end;
    suppose
A5:   a=0;
      hence n-root a = 0 by A3,Th5
        .= - n-root (-a) by A3,A5,Th5;
    end;
    suppose
A6:   a>0;
then    -a<-0 by XREAL_1:24;
      hence - n-root (-a) = -(- n -Root (-(-a))) by A2,Def1
        .= n-root a by A3,A6,Def1;
    end;
  end;
  hence thesis;
end;

theorem Th11:
  n>=1 & a>=0 & b>=0 or n is odd implies n-root (a*b) = n-root a * n-root b
proof
  assume
A1: n>=1 & a>=0 & b>=0 or n is odd;
A2: now
    let a,b,n;
    assume that
A3: n>=1 and
A4: a>=0 and
A5: b>=0;
    thus n-root (a*b) = n -Root (a*b) by A3,A4,A5,Def1
      .= n -Root a * n -Root b by A3,A4,A5,PREPOWER:22
      .= n-root a * n -Root b by A3,A4,Def1
      .= n-root a * n-root b by A3,A5,Def1;
  end;
 now
    assume
A6: n is odd;
    then
A7: n>=1 by ABIAN:12;
 now per cases;
      suppose
    a>=0 & b>=0;
        hence thesis by A2,A7;
      end;
      suppose
A8:    a<0 & b<0;
        thus
        then n-root (a*b) = n -Root ((-a)*(-b)) by A7,Def1
          .= (-(-n -Root (-a))) * n -Root (-b) by A7,A8,PREPOWER:22
          .= (-(n-root a)) * (-(-n -Root (-b))) by A6,A8,Def1
          .= (-(n-root a)) * (-(n-root b)) by A6,A8,Def1
          .= n-root a * n-root b;
      end;
      suppose
A9:    a>=0 & b<0;
        thus
        n-root (a*b) = -n-root (-a*b) by A6,Th10
          .= -n-root (a*(-b))
          .= -(n-root a * n-root (-b)) by A2,A7,A9
          .= n-root a * (-n-root (-b))
          .= n-root a * n-root b by A6,Th10;
      end;
      suppose
A10:    a<0 & b>=0;
        thus
        n-root (a*b) = -n-root (-a*b) by A6,Th10
          .= -n-root ((-a)*b)
          .= -(n-root (-a) * n-root b) by A2,A7,A10
          .= (-n-root (-a)) * n-root b
          .= n-root a * n-root b by A6,Th10;
      end;
    end;
    hence thesis;
  end;
  hence thesis by A1,A2;
end;

theorem Th12:
  a>0 & n>=1 or a<>0 & n is odd implies n-root (1/a) = 1/(n-root a)
proof
  assume
A1: a>0 & n>=1 or a<>0 & n is odd;
A2: now
    let a,n;
    assume
A3: a>0 & n>=1;
    hence n-root (1/a) = n -Root (1/a) by Def1
      .= 1/(n -Root a) by A3,PREPOWER:23
      .= 1/(n-root a) by A3,Def1;
  end;
 now
    assume that
A4: a<>0 and
A5: n is odd;
A6: n>=1 by A5,ABIAN:12;
 now per cases by A4;
      suppose
     a>0;
        hence thesis by A2,A6;
      end;
      suppose
    a<0;
then A7:    -a>0 by XREAL_1:58;
        thus
        1/(n-root a) = 1/(-(n-root (-a))) by A5,Th10
          .= - 1/(n-root (-a)) by XCMPLX_1:188
          .= - n-root (1/(-a)) by A2,A6,A7
          .= - n-root (-1/a) by XCMPLX_1:188
          .= n-root (1/a) by A5,Th10;
      end;
    end;
    hence thesis;
  end;
  hence thesis by A1,A2;
end;

theorem
  a>=0 & b>0 & n>=1 or b<>0 & n is odd implies
  n-root (a/b) = n-root a / n-root b
proof
  assume
A1: a>=0 & b>0 & n>=1 or b<>0 & n is odd;
 now per cases by A1;
    suppose
A2:   a>=0 & b>0 & n>=1;
      hence n-root (a/b) = n -Root (a/b) by Def1
        .= n -Root a / n -Root b by A2,PREPOWER:24
        .= n-root a / n -Root b by A2,Def1
        .= n-root a / n-root b by A2,Def1;
    end;
    suppose
A3:   b<>0 & n is odd;
      thus n-root (a/b) = n-root (a*(1/b))
        .= n-root a * n-root (1/b) by A3,Th11
        .= n-root a * (1 / n-root b) by A3,Th12
        .= n-root a / n-root b;
    end;
  end;
  hence thesis;
end;

theorem
  a>=0 & n>=1 & m>=1 or n is odd & m is odd implies
  n-root (m-root a) = (n*m)-root a
proof
  assume
A1: a>=0 & n>=1 & m>=1 or n is odd & m is odd;
A2: now
    let a,n,m;
    assume that
A3: a>=0 and
A4: n>=1 and
A5: m>=1;
A6: n*m>= 1 by A4,A5,XREAL_1:159;
 m-root a >= 0 by A3,A5,Th7;
then A7: m -Root a >= 0 by A3,A5,Def1;
    thus
    n-root (m-root a) = n-root (m -Root a) by A3,A5,Def1
      .= n -Root (m -Root a) by A4,A7,Def1
      .= (n*m) -Root a by A3,A4,A5,PREPOWER:25
      .= (n*m)-root a by A3,A6,Def1;
  end;
 now
    assume n is odd;
    then consider m1 such that
A8: n=2*m1+1 by ABIAN:9;
    assume m is odd;
    then consider m2 such that
A9: m=2*m2+1 by ABIAN:9;
A10: n>=0+1 by A8,XREAL_1:6;
A11: m>=0+1 by A9,XREAL_1:6;
then A12: n*m >= 1 by A10,XREAL_1:159;
A13: n*m = 2*(m1*(2*m2)+m1+m2) + 1 by A8,A9;
 now per cases;
      suppose
    a>=0;
        hence thesis by A2,A10,A11;
      end;
      suppose
A14:    a<0;
then     m-root (-a) >= 0 by A11,Th7;
then A15:    m -Root (-a) >= 0 by A11,A14,Def1;
        thus
        n-root (m-root a) = n-root (-m -Root (-a)) by A9,A14,Def1
          .= -n-root (-(-m -Root (-a))) by A8,Th10
          .= -n -Root (m -Root (-a)) by A10,A15,Def1
          .= -(n*m) -Root (-a) by A10,A11,A14,PREPOWER:25
          .= -(n*m)-root (-a) by A12,A14,Def1
          .= (n*m)-root a by A13,Th10;
      end;
    end;
    hence thesis;
  end;
  hence thesis by A1,A2;
end;

theorem
  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))
proof
  assume
A1: a>=0 & n>=1 & m>=1 or n is odd & m is odd;
A2: now
    let a,n,m;
    assume that
A3: a>=0 and
A4: n>=1 and
A5: m>=1;
A6: n*m>= 1 & a |^ (n+m) >=0 by A3,A4,A5,Th3,XREAL_1:159;
    thus
    n-root a * m-root a = n-root a* m -Root a by A3,A5,Def1
      .= n -Root a * m -Root a by A3,A4,Def1
      .= (n*m) -Root (a |^ (n+m)) by A3,A4,A5,PREPOWER:26
      .= (n*m)-root (a |^ (n+m)) by A6,Def1;
  end;
 now
    assume n is odd;
    then consider m1 such that
A7: n=2*m1+1 by ABIAN:9;
    assume m is odd;
    then consider m2 such that
A8: m=2*m2+1 by ABIAN:9;
A9: n>=0+1 & m>=0+1 by A7,A8,XREAL_1:6;
then A10: n*m >= 1 by XREAL_1:159;
A11: n+m = 2*(m1+(1+m2)) by A7,A8;
 now per cases;
      suppose
    a>=0;
        hence thesis by A2,A9;
      end;
      suppose
A12:    a<0;
A13:    a |^ (n+m) >= 0 by A11,Th3;
        thus
        n-root a * m-root a = n-root a * (-m -Root (-a)) by A8,A12,Def1
          .= (-n -Root (-a)) * (-m -Root (-a)) by A7,A12,Def1
          .= n -Root (-a) * m -Root (-a)
          .= (n*m) -Root ((-a) |^ (n+m))by A9,A12,PREPOWER:26
          .= (n*m) -Root (a |^ (n+m)) by A11,Th1
          .= (n*m)-root (a |^ (n+m)) by A10,A13,Def1;
      end;
    end;
    hence thesis;
  end;
  hence thesis by A1,A2;
end;

theorem
  a<=b & (0<=a & n>=1 or n is odd) implies n-root a <= n-root b
proof
  assume that
A1: a<=b and
A2: 0<=a & n>=1 or n is odd;
A3: now
    let a,b,n;
    assume that
A4: 0<=a & n>=1 and
A5: a<=b;
 n -Root a <= n -Root b by A4,A5,PREPOWER:27;
then  n -Root a <= n-root b by A4,A5,Def1;
    hence n-root a <= n-root b by A4,Def1;
  end;
 now
    assume
A6: n is odd;
    then
A7: n>=1 by ABIAN:12;
 now per cases;
      suppose
    a>=0;
        hence thesis by A1,A3,A7;
      end;
      suppose
A8:    a<0;
    now per cases;
          suppose
        b>=0;
then A9:        n-root b >= 0 by A7,Th7;
        n-root (-a) >= 0 by A7,A8,Th7;
then         - n-root (-a) <= -0;
            hence thesis by A6,A9,Th10;
          end;
          suppose
A10:        b<0;
        -a>=-b by A1,XREAL_1:24;
then         n-root (-a) >= n-root (-b) by A3,A7,A10;
then         - n-root (-a) <= - n-root (-b) by XREAL_1:24;
then         n-root a <= - n-root (-b) by A6,Th10;
            hence thesis by A6,Th10;
          end;
        end;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  hence thesis by A1,A2,A3;
end;

theorem
  a<b & (a>=0 & n>=1 or n is odd) implies n-root a < n-root b
proof
  assume that
A1: a<b and
A2: 0<=a & n>=1 or n is odd;
A3: now
    let a,b,n;
    assume that
A4: 0<=a & n>=1 and
A5: a<b;
 n -Root a < n -Root b by A4,A5,PREPOWER:28;
then  n -Root a < n-root b by A4,A5,Def1;
    hence n-root a < n-root b by A4,Def1;
  end;
 now
    assume
A6: n is odd;
    then
A7: n>=1 by ABIAN:12;
 now per cases;
      suppose
    a>=0;
        hence thesis by A1,A3,A7;
      end;
      suppose
A8:    a<0;
then A9:    -a>0 by XREAL_1:58;
    now per cases;
          suppose
        b>=0;
then A10:        n-root b >= 0 by A7,Th7;
        n -Root (-a) > 0 by A7,A9,PREPOWER:def 2;
then         - n -Root (-a) < -0 by XREAL_1:24;
            hence thesis by A6,A8,A10,Def1;
          end;
          suppose
A11:        b<0;
        -a>-b by A1,XREAL_1:24;
then         n-root (-a) > n-root (-b) by A3,A7,A11;
then         - n-root (-a) < - n-root (-b) by XREAL_1:24;
then         n-root a < - n-root (-b) by A6,Th10;
            hence thesis by A6,Th10;
          end;
        end;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  hence thesis by A1,A2,A3;
end;

theorem Th18:
  a>=1 & n>=1 implies n-root a >= 1 & a >= n-root a
proof
  assume that
A1: a>=1 and
A2: n>=1;
   n -Root a >= 1 & a >= n -Root a by A1,A2,PREPOWER:29;
  hence thesis by A2,Def1;
end;

theorem
  a<=-1 & n is odd implies n-root a <= -1 & a <= n-root a
proof
  assume that
A1: a<=-1 and
A2: n is odd;
A3: n>=1 & -a>=1 by A1,A2,ABIAN:12,XREAL_1:25;
then A4: n-root (-a) >= 1 by Th18;
A5: -a >= n-root (-a) by A3,Th18;
A6: - n-root (-a) <= -1 by A4,XREAL_1:24;
 a <= - n-root (-a) by A5,XREAL_1:25;
  hence thesis by A2,A6,Th10;
end;

theorem Th20:
  a>=0 & a<1 & n>=1 implies a <= n-root a & n-root a < 1
proof
  assume that
A1: a>=0 and
A2: a<1 and
A3: n>=1;
  a <= n -Root a & n -Root a < 1 by A1,A2,A3,PREPOWER:30;
  hence thesis by A1,A3,Def1;
end;

theorem
  a>-1 & a<=0 & n is odd implies a >= n-root a & n-root a > -1
proof
  assume that
A1: a>-1 and
A2: a<=0;
  assume n is odd;
  then
A3: ex m st n=2*m+1 by ABIAN:9;
then A4: n>=1 & -a<1 by A1,ABIAN:12,XREAL_1:25;
then A5: n-root (-a) < 1 by A2,Th20;
A6: -a <= n-root (-a) by A2,A4,Th20;
A7: - n-root (-a) > -1 by A5,XREAL_1:24;
 a >= - n-root (-a) by A6,XREAL_1:26;
  hence thesis by A3,A7,Th10;
end;

theorem Th22:
  a>0 & n>=1 implies n-root a - 1 <= (a-1)/n
proof
  assume
A1: a>0 & n>=1;
then  n -Root a - 1 <= (a-1)/n by PREPOWER:31;
  hence thesis by A1,Def1;
end;

theorem Th23:
  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
proof
  let s be Real_Sequence, a;
  assume that
A1: a > 0 and
A2: for n st n>=1 holds s.n = n-root a;
 now
    let n be Element of NAT;
    assume
A3: n>=1;
    hence s.n = n-root a by A2
      .= n -Root a by A1,A3,Def1;
  end;
  hence thesis by A1,PREPOWER:33;
end;

definition
  let a,b be real number;
  func a to_power b -> real number means
  :Def2:
  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;
  consistency
  proof
    let IT be real number;
    thus a > 0 & a = 0 & b > 0 implies (IT = a #R b iff IT = 0);
    thus a > 0 & b is Integer implies
    (IT = a #R b iff ex k st k = b & IT = a #Z k)
    proof
      assume
A1:   a > 0;
      assume b is Integer;
      then reconsider b as Integer;
   a #R b = a #Q b by A1,PREPOWER:74
        .= a #Z b by A1,PREPOWER:99;
      hence thesis;
    end;
 a = 0 & b > 0 & b is Integer implies
    (IT = 0 iff ex k st k = b & IT = a #Z k)
    proof
      assume
A2:   a = 0;
      assume that
A3:   b > 0 and
A4:   b is Integer;
   b in NAT by A3,A4,INT_1:3;
      then reconsider b as Nat;
   a #Z b = a |^ b by PREPOWER:36
        .= 0 by A2,A3,NAT_1:14,NEWTON:11;
      hence thesis;
    end;
    hence thesis;
  end;
  existence
  proof
 now
      assume b is Integer;
      then reconsider k = b as Integer;
      take c = a #Z k;
      thus ex k st k = b & c = a #Z k;
    end;
    hence thesis;
  end;
  uniqueness;
end;

definition
  let a,b be Real;
  redefine func a to_power b -> Real;
  coherence by XREAL_0:def 1;
end;

theorem Th24:
  a to_power 0 = 1
proof
  thus a to_power 0 = a #Z 0 by Def2
    .= 1 by PREPOWER:34;
end;

theorem Th25:
  a to_power 1 = a
proof
  thus a to_power 1 = a #Z 1 by Def2
    .= a by PREPOWER:35;
end;

theorem Th26:
  1 to_power a = 1
proof
A1: 1 #R a <> 0 by PREPOWER:81;
  thus
  1 to_power a = (1/1) #R a by Def2
    .= (1 #R a) / (1 #R a) by PREPOWER:80
    .= 1 by A1,XCMPLX_1:60;
end;

theorem Th27:
  a > 0 implies a to_power (b+c) = a to_power b * a to_power c
proof
  assume
A1: a > 0;
then  a #R (b+c) = a #R b * a #R c by PREPOWER:75;
then  a #R (b+c) = a #R b * a to_power c by A1,Def2;
then  a #R (b+c) = a to_power b * a to_power c by A1,Def2;
  hence thesis by A1,Def2;
end;

theorem Th28:
  a > 0 implies a to_power (-c) = 1 / a to_power c
proof
  assume
A1: a > 0;
then  a #R (-c) = 1 / a #R c by PREPOWER:76;
then  a #R (-c) = 1 / a to_power c by A1,Def2;
  hence thesis by A1,Def2;
end;

theorem Th29:
  a > 0 implies a to_power (b-c) = a to_power b / a to_power c
proof
  assume
A1: a > 0;
then  a #R (b-c) = a #R b / a #R c by PREPOWER:77;
then  a #R (b-c) = a #R b / a to_power c by A1,Def2;
then  a #R (b-c) = a to_power b / a to_power c by A1,Def2;
  hence thesis by A1,Def2;
end;

theorem
  a>0 & b>0 implies (a*b) to_power c = a to_power c*b to_power c
proof
  assume that
A1: a > 0 and
A2: b > 0;
A3: a * b > 0 by A1,A2,XREAL_1:129;
 (a * b) #R c = a #R c * b #R c by A1,A2,PREPOWER:78;
then  (a * b) #R c = a #R c * b to_power c by A2,Def2;
then  (a * b) #R c = a to_power c * b to_power c by A1,Def2;
  hence thesis by A3,Def2;
end;

theorem Th31:
  a>0 & b>0 implies (a/b) to_power c = a to_power c/b to_power c
proof
  assume that
A1: a > 0 and
A2: b > 0;
A3: a / b > 0 by A1,A2,XREAL_1:139;
 (a / b) #R c = a #R c / b #R c by A1,A2,PREPOWER:80;
then  (a / b) #R c = a #R c / b to_power c by A2,Def2;
then  (a / b) #R c = a to_power c / b to_power c by A1,Def2;
  hence thesis by A3,Def2;
end;

theorem Th32:
  a>0 implies (1/a) to_power b = a to_power (-b)
proof
  assume
A1: a>0;
  hence (1/a) to_power b = (1/a) #R b by Def2
    .= 1/a #R b by A1,PREPOWER:79
    .= 1/a to_power b by A1,Def2
    .= a to_power (-b) by A1,Th28;
end;

theorem Th33:
  a > 0 implies a to_power b to_power c = a to_power (b * c)
proof
  assume
A1: a > 0;
then A2: a #R b > 0 by PREPOWER:81;
 a #R b #R c = a #R (b * c) by A1,PREPOWER:91;
then  a #R b #R c = a to_power (b * c) by A1,Def2;
then  a #R b to_power c = a to_power (b * c) by A2,Def2;
  hence thesis by A1,Def2;
end;

theorem Th34:
  a > 0 implies a to_power b > 0
proof
  assume
A1: a > 0;
then  a #R b > 0 by PREPOWER:81;
  hence thesis by A1,Def2;
end;

theorem Th35:
  a > 1 & b > 0 implies a to_power b > 1
proof
  assume that
A1: a > 1 and
A2: b > 0;
 a #R b > 1 by A1,A2,PREPOWER:86;
  hence thesis by A1,Def2;
end;

theorem Th36:
  a > 1 & b < 0 implies a to_power b < 1
proof
  assume that
A1: a > 1 and
A2: b < 0;
 a #R b < 1 by A1,A2,PREPOWER:88;
  hence thesis by A1,Def2;
end;

theorem
  a > 0 & a < b & c > 0 implies a to_power c < b to_power c
proof
  assume that
A1: a > 0 and
A2: a < b and
A3: c > 0;
A4: a to_power c > 0 by A1,Th34;
A5: a to_power c <> 0 by A1,Th34;
 a/a<b/a by A1,A2,XREAL_1:74;
then  1<b/a by A1,XCMPLX_1:60;
then  (b/a) to_power c > 1 by A3,Th35;
then  b to_power c / a to_power c > 1 by A1,A2,Th31;
then
 b to_power c/a to_power c*a to_power c>1*a to_power c by A4,XREAL_1:68;
  hence thesis by A5,XCMPLX_1:87;
end;

theorem
  a > 0 & a < b & c < 0 implies a to_power c > b to_power c
proof
  assume that
A1: a > 0 and
A2: a < b and
A3: c < 0;
A4: a to_power c > 0 by A1,Th34;
A5: a to_power c <> 0 by A1,Th34;
 a/a<b/a by A1,A2,XREAL_1:74;
then  1<b/a by A1,XCMPLX_1:60;
then  (b/a) to_power c < 1 by A3,Th36;
then  b to_power c / a to_power c < 1 by A1,A2,Th31;
then
 b to_power c/a to_power c*a to_power c <1*a to_power c by A4,XREAL_1:68
;
  hence thesis by A5,XCMPLX_1:87;
end;

theorem Th39:
  a < b & c > 1 implies c to_power a < c to_power b
proof
  assume that
A1: a < b and
A2: c > 1;
A3: c to_power a > 0 by A2,Th34;
A4: c to_power a <> 0 by A2,Th34;
 b-a>0 by A1,XREAL_1:50;
then  c to_power (b-a) > 1 by A2,Th35;
then  c to_power b / c to_power a > 1 by A2,Th29;
then
 c to_power b/c to_power a*c to_power a > 1*c to_power a by A3,XREAL_1:68
  ;
  hence thesis by A4,XCMPLX_1:87;
end;

theorem Th40:
  a < b & c > 0 & c < 1 implies c to_power a > c to_power b
proof
  assume that
A1: a < b and
A2: c > 0 and
A3: c < 1;
A4: (1/c) to_power a > 0 by A2,Th34;
A5: (1/c) to_power a <> 0 by A2,Th34;
A6: c to_power a > 0 by A2,Th34;
 c/c <1/c by A2,A3,XREAL_1:74;
then A7: 1<1/c by A2,XCMPLX_1:60;
 b-a>0 by A1,XREAL_1:50;
then  (1/c) to_power (b-a) > 1 by A7,Th35;
then  (1/c) to_power b / (1/c) to_power a > 1 by A2,Th29;
then  (1/c) to_power b/(1/c) to_power a*(1/c) to_power a >
  1*(1/c) to_power a by A4,XREAL_1:68;
then  (1/c) to_power b > (1/c) to_power a by A5,XCMPLX_1:87;
then  1 to_power b/c to_power b > (1/c) to_power a by A2,Th31;
then  1 / c to_power b > (1/c) to_power a by Th26;
then  1 / c to_power b > 1 to_power a/c to_power a by A2,Th31;
then  1 / c to_power b > 1 / c to_power a by Th26;
  hence thesis by A6,XREAL_1:91;
end;

registration
  let a be real number, n be Nat;
  identify a to_power n with a |^ n;
  compatibility
  proof
    thus a to_power n = a #Z n by Def2
      .= a |^ n by PREPOWER:36;
  end;
end;

theorem
  for n be Nat holds a to_power n = a |^ n;

theorem Th42:
 k <> 0 implies 0 to_power k = 0
 proof
   0 to_power k = 0 #Z k by Def2;
  hence thesis by PREPOWER:100;
 end;

theorem
  a to_power k = a #Z k by Def2;

theorem Th44:
  a>0 implies a to_power p = a #Q p
proof
  assume
A1: a>0;
  hence a to_power p = a #R p by Def2
    .= a #Q p by A1,PREPOWER:74;
end;

theorem Th45:
  a>=0 & n>=1 implies a to_power (1/n) = n-root a
proof
  assume that
A1: a>=0 and
A2: n>=1;
  reconsider p=n" as Rational;
 now per cases by A1;
    suppose
   a>0;
      hence a to_power (1/n) = a #Q p by Th44
        .= n -Root a by A2,PREPOWER:50;
    end;
    suppose
A3:   a=0;
      hence a to_power (1/n) = 0 by A2,Def2
        .= n -Root a
      by A2,A3,PREPOWER:def 2;
    end;
  end;
  hence thesis by A1,A2,Def1;
end;

theorem Th46:
  a to_power 2 = a^2
proof
 now per cases;
    suppose
A1:   a>0;
      thus
      a to_power 2 = a to_power (1+1) .= a to_power 1 * a to_power 1 by A1,Th27
        .= a to_power 1 * a by Th25
        .= a^2 by Th25;
    end;
    suppose
   a=0;
      hence thesis by Def2;
    end;
    suppose
A2:   a<0;
      reconsider l=1 as Integer;
      thus
      a to_power 2 = a #Z (l+l) by Def2
        .= a #Z l * a #Z l by A2,PREPOWER:44
        .= a * a #Z l by PREPOWER:35
        .= a^2 by PREPOWER:35;
    end;
  end;
  hence thesis;
end;

theorem Th47:
  k is even implies (-a) to_power k = a to_power k
proof
  given l such that
A1: k=2*l;
  per cases;
    suppose a = 0;
     hence thesis;
    end;
    suppose a>0;
      hence a to_power k = (a to_power 2) to_power l by A1,Th33
        .= (a^2) to_power l by Th46
        .= ((-a)^2) to_power l
        .= ((-a) to_power 2) to_power l by Th46
        .= ((-a) #Z 2) to_power l by Def2
        .= ((-a) #Z 2) #Z l by Def2
        .= (-a) #Z (2*l) by PREPOWER:45
        .= (-a) to_power k by A1,Def2;
    end;
    suppose
   a<0;
then    -a>0 by XREAL_1:58;
      hence (-a) to_power k = ((-a) to_power 2) to_power l by A1,Th33
        .= ((-a)^2) to_power l by Th46
        .= (a^2) to_power l
        .= (a to_power 2) to_power l by Th46
        .= (a #Z 2) to_power l by Def2
        .= (a #Z 2) #Z l by Def2
        .= a #Z (2*l) by PREPOWER:45
        .= a to_power k by A1,Def2;
    end;
end;

theorem
  k is odd implies (-a) to_power k = -(a to_power k)
proof
  assume
A1:  k is odd;
  then consider l such that
A2: k=2*l + 1 by ABIAN:1;
  per cases;
    suppose
A3:    a = 0;
   k <> 0 by A1;
      then a to_power k = 0 by A3,Th42;
     hence thesis by A3;
    end;
    suppose
A4:   a>0;
then A5:   -a<>-0;
   a to_power k = a to_power (2*l) * a to_power 1 by A2,A4,Th27
        .= a to_power (2*l) * a by Th25
        .= (-a) to_power (2*l) * a by Th47
        .= - (-a) to_power (2*l) * (-a)
        .= - (-a) #Z (2*l) * (-a) by Def2
        .= - (-a) #Z (2*l) * (-a) #Z 1 by PREPOWER:35
        .= - (-a) #Z k by A2,A5,PREPOWER:44
        .= - (-a) to_power k by Def2;
      hence thesis;
    end;
    suppose
A6:   a<0;
then    -a>0 by XREAL_1:58;
      hence
(-a) to_power k = (-a) to_power (2*l) * (-a) to_power 1 by A2,Th27
        .= (-a) to_power (2*l) * (-a) by Th25
        .= a to_power (2*l) * (-a) by Th47
        .= - a to_power (2*l) * a
        .= - a #Z (2*l) * a by Def2
        .= - a #Z (2*l) * a #Z 1 by PREPOWER:35
        .= - a #Z k by A2,A6,PREPOWER:44
        .= - a to_power k by Def2;
    end;
end;

theorem
  -1 < a implies (1 + a) to_power n >= 1 + n * a by PREPOWER:16;

theorem Th50:
  a>0 & a<>1 & c <>d implies a to_power c <> a to_power d
proof
  assume that
A1: a>0 and
A2: a<>1 and
A3: c <>d;
 now per cases by A3,XXREAL_0:1;
    suppose
A4:   c <d;
   now per cases by A2,XXREAL_0:1;
        suppose
       a<1;
          hence thesis by A1,A4,Th40;
        end;
        suppose
       a>1;
          hence thesis by A4,Th39;
        end;
      end;
      hence thesis;
    end;
    suppose
A5:   c>d;
  now per cases by A2,XXREAL_0:1;
        suppose
      a<1;
          hence thesis by A1,A5,Th40;
        end;
        suppose
      a>1;
          hence thesis by A5,Th39;
        end;
      end;
      hence thesis;
    end;
  end;
  hence thesis;
end;

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:
  a to_power it = b;
  existence
  proof
    reconsider a1=a, b1=b as Real by XREAL_0:def 1;
    set X = {c where c is Real: a to_power c <= b};
 for x holds x in X implies x in REAL
    proof
      let x;
      assume x in X;
then    ex c be Real st x = c & a to_power c <= b;
      hence thesis;
    end;
    then reconsider X as Subset of REAL by TARSKI:def 3;
A4: ex d st d in X
    proof
A5:   now
        let a,b be real number such that
A6:     a>1 and
A7:    b>0;
        reconsider a1=a, b1=b as Real by XREAL_0:def 1;
        set e = a1-1;
        consider n such that
A8:    n>1/(b*e) by SEQ_4:3;
    e>0-1 by A6,XREAL_1:9;
then A9:    (1 + e) to_power n >= 1 + n * e by PREPOWER:16;
    1 + n * e >= 0 + n * e by XREAL_1:6;
then A10:    (1 + e) to_power n >= n * e by A9,XXREAL_0:2;
A11:    e>1-1 by A6,XREAL_1:9;
then     n*e>1/(b*e)*e by A8,XREAL_1:68;
then     n*e>=1/b by A11,XCMPLX_1:92;
then     a to_power n >= 1/b by A10,XXREAL_0:2;
then     1/a to_power n <= 1/(1/b) by A7,XREAL_1:85;
then     a1 to_power (-n) <= b1 by A6,Th28;
        hence ex d st a to_power d <= b;
      end;
  now per cases by A2,XXREAL_0:1;
        suppose
      a>1;
          hence ex d st a to_power d <= b by A3,A5;
        end;
        suppose
      a<1;
then       1/a >1/1 by A1,XREAL_1:88;
          then consider d such that
A12:      (1/a) to_power d <= b by A3,A5;
      a1 to_power (-d) <= b1 by A1,A12,Th32;
          hence ex e st a to_power e <= b;
        end;
      end;
      then consider d such that
A13:  a to_power d <= b;
      take d;
  d is Real by XREAL_0:def 1;
      hence thesis by A13;
    end;
 now per cases by A2,XXREAL_0:1;
      suppose
A14:    a>1;
A15:    X is bounded_above proof consider n such that
A16:      n > (b1-1)/(a1-1) by SEQ_4:3;
      a-1>1-1 by A14,XREAL_1:9;
then       n*(a-1) > b-1 by A16,XREAL_1:77;
then A17:      1 + n*(a-1) > 1+(b-1) by XREAL_1:6;
      a-1>0-1 by A1,XREAL_1:9;
then       (1+(a1-1)) to_power n >= 1 + n*(a1-1) by PREPOWER:16;
then A18:      a to_power n > b by A17,XXREAL_0:2;
          take n;
            let c be ext-real number;
            assume c in X;
        then consider d being Real such that
A19: d=c & a to_power d <= b;
        a1 to_power d <= a1 to_power n by A18,A19,XXREAL_0:2;
            hence c <=n by A14,Th39,A19;
        end;
        take d = upper_bound X;
A20:    not b < a to_power d
        proof
          assume a to_power d > b;
          then consider e be real number such that
A21:      b<e and
A22:      e<a to_power d by XREAL_1:5;
          reconsider e as Real by XREAL_0:def 1;
          consider n such that
A23:      n > (a1-1)/(e/b1-1) by SEQ_4:3;
          reconsider m = max(1,n) as Element of NAT;
      n<=m by XXREAL_0:25;
then A24:      (a-1)/(e/b-1) < m by A23,XXREAL_0:2;
      e/b>1 by A3,A21,XREAL_1:187;
then       e/b-1>1-1 by XREAL_1:9;
then A25:      (a-1)<m*(e/b-1) by A24,XREAL_1:77;
A26:      1<=m by XXREAL_0:25;
then       (a-1)/m<e/b-1 by A25,XREAL_1:83;
then A27:      (a-1)/m+1<e/b-1+1 by XREAL_1:6;
      m-root a1 - 1 <= (a1-1)/m by A1,Th22,XXREAL_0:25;
then       m-root a - 1 + 1 <= (a-1)/m + 1 by XREAL_1:6;
then       m-root a <= e/b by A27,XXREAL_0:2;
then       a1 to_power (1/m) <= e/b1 by A1,Th45,XXREAL_0:25;
then A28:      a to_power (1/m) * b <= e by A3,XREAL_1:83;
          consider c be real number such that
A29:      c in X and
A30:      d-1/m < c by A4,A15,A26,SEQ_4:def 1;
          reconsider c as Real by XREAL_0:def 1;
A31:      ex g being Real st g=c & a to_power g <= b by A29;
      a1 to_power (1/m) >= 0 by A1,Th34;
then
      a to_power c * a to_power (1/m) <= a to_power (1/m)*b by A31,XREAL_1:64;
then       a to_power c * a to_power (1/m) <= e by A28,XXREAL_0:2;
then A32:      a1 to_power (c + 1/m) <= e by A1,Th27;
      d<c + 1/m by A30,XREAL_1:19;
then       a1 to_power d <= a1 to_power (c + 1/m) by A14,Th39;
          hence contradiction by A22,A32,XXREAL_0:2;
        end;
    not a to_power d < b
        proof
          assume a to_power d < b;
          then consider e being real number such that
A33:      a to_power d<e and
A34:      e<b by XREAL_1:5;
          reconsider e as Real by XREAL_0:def 1;
A35:      a1 to_power d > 0 by A1,Th34;
then       b/e>1 by A33,A34,XREAL_1:187;
then A36:      b/e-1>1-1 by XREAL_1:9;
          deffunc F(Element of NAT) = $1-root a;
          consider s being Real_Sequence such that
A37:      for n holds s.n = F(n) from SEQ_1:sch 1;
      for n st n>=1 holds s.n = n-root a1 by A37;
then       s is convergent & lim s = 1 by A1,Th23;
          then consider n such that
A38:      for m st m>=n holds abs(s.m - 1)<b/e-1 by A36,SEQ_2:def 7;
          reconsider m = max(1,n) as Element of NAT;
      abs(s.m - 1)<b/e-1 by A38,XXREAL_0:25;
then A39:      abs(m-root a - 1)<b/e-1 by A37;
      m-root a - 1<=abs(m-root a - 1) by ABSVALUE:4;
then       m-root a - 1<b/e-1 by A39,XXREAL_0:2;
then       m-root a < b/e by XREAL_1:9;
then       a1 to_power (1/m) < b1/e by A1,Th45,XXREAL_0:25;
then       a
 to_power d * a to_power (1/m) < b/e * a to_power d by A35,XREAL_1:68;
then A40:      a to_power (d + 1/m) < b * a to_power d / e by A1,Th27;
      a to_power d / e < 1 by A33,A35,XREAL_1:189;
then       a to_power d / e * b < 1*b by A3,XREAL_1:68;
then       a to_power (d + 1/m) <= b by A40,XXREAL_0:2;
then       d + 1/m in X;
then       m>=1 & d + 1/m <= d by A15,SEQ_4:def 1,XXREAL_0:25;
          hence contradiction by XREAL_1:29;
        end;
        hence b = a to_power d by A20,XXREAL_0:1;
      end;
      suppose
A41:    a<1;
A42:    X is bounded_below proof consider n such that
A43:      n > (b1-1)/(1/a1-1) by SEQ_4:3;
      1/a >1/1 by A1,A41,XREAL_1:88;
then       1/a-1>1-1 by XREAL_1:9;
then      n*(1/a-1) > b-1 by A43,XREAL_1:77;
then A44:     1 + n*(1/a-1) > 1+(b-1) by XREAL_1:6;
     1/a-1>0-1 by A1,XREAL_1:9;
then      (1+(1/a1-1)) to_power n >= 1 + n*(1/a1-1) by PREPOWER:16;
then      (1/a) to_power n > b by A44,XXREAL_0:2;
then A45:     a1 to_power (-n) > b1 by A1,Th32;
          take -n;
            let c be ext-real number;
            assume c in X;
            then consider d be Real such that
A46:        d=c & a to_power d <= b;
       a1 to_power d <= a1 to_power (-n) by A45,A46,XXREAL_0:2;
            hence c>=-n by A1,A41,Th40,A46;
        end;
        take d = lower_bound X;
A47:   not b < a to_power d
        proof
          assume a to_power d > b;
          then consider e being real number such that
A48:     b<e and
A49:     e<a to_power d by XREAL_1:5;
          reconsider e as Real by XREAL_0:def 1;
          consider n such that
A50:     n > (1/a1-1)/(e/b1-1) by SEQ_4:3;
          reconsider m = max(1,n) as Element of NAT;
     n<=m by XXREAL_0:25;
then A51:     (1/a-1)/(e/b-1) < m by A50,XXREAL_0:2;
     e/b>1 by A3,A48,XREAL_1:187;
then      e/b-1>1-1 by XREAL_1:9;
then A52:     (1/a-1)<m*(e/b-1) by A51,XREAL_1:77;
A53:     1<=m by XXREAL_0:25;
then      (1/a-1)/m<e/b-1 by A52,XREAL_1:83;
then A54:     (1/a-1)/m+1<e/b-1+1 by XREAL_1:6;
     m-root (1/a1) - 1 <= (1/a1-1)/m by A1,Th22,XXREAL_0:25;
then      m-root (1/a) - 1 + 1 <= (1/a-1)/m + 1 by XREAL_1:6;
then      m-root (1/a) <= e/b by A54,XXREAL_0:2;
then      (1/a1) to_power (1/m) <= e/b1 by A1,Th45,XXREAL_0:25;
then      (1/a) to_power (1/m) * b <= e by A3,XREAL_1:83;
then A55:     a1 to_power (-1/m) * b1 <= e by A1,Th32;
          consider c be real number such that
A56:     c in X and
A57:     c <d+1/m by A4,A42,A53,SEQ_4:def 2;
          reconsider c as Real by XREAL_0:def 1;
A58:     ex g being Real st g=c & a to_power g <= b by A56;
     a1 to_power (-1/m) >= 0 by A1,Th34;
then
     a to_power c*a to_power (-1/m) <= a to_power (-1/m)*b by A58,XREAL_1:64;
then      a to_power c * a to_power (-1/m) <= e by A55,XXREAL_0:2;
then A59:     a1 to_power (c + -1/m) <= e by A1,Th27;
     d>c - 1/m by A57,XREAL_1:19;
then      a1 to_power d <= a1 to_power (c - 1/m) by A1,A41,Th40;
          hence contradiction by A49,A59,XXREAL_0:2;
        end;
   not a to_power d < b
        proof
          assume a to_power d < b;
          then consider e being real number such that
A60:     a to_power d<e and
A61:     e<b by XREAL_1:5;
          reconsider e as Real by XREAL_0:def 1;
A62:     a1 to_power d > 0 by A1,Th34;
then      b/e>1 by A60,A61,XREAL_1:187;
then A63:     b/e-1>1-1 by XREAL_1:9;
          deffunc F(Element of NAT) = $1-root (1/a);
          consider s being Real_Sequence such that
A64:     for n holds s.n = F(n) from SEQ_1:sch 1;
     for n st n>=1 holds s.n = n-root (1/a1) by A64;
then      s is convergent & lim s = 1 by A1,Th23;
          then consider n such that
A65:     for m st m>=n holds abs(s.m - 1)<b/e-1 by A63,SEQ_2:def 7;
          reconsider m = max(1,n) as Element of NAT;
     abs(s.m - 1)<b/e-1 by A65,XXREAL_0:25;
then A66:     abs(m-root (1/a) - 1)<b/e-1 by A64;
     m-root (1/a) - 1<=abs(m-root (1/a) - 1) by ABSVALUE:4;
then      m-root (1/a) - 1<b/e-1 by A66,XXREAL_0:2;
then      m-root (1/a) < b/e by XREAL_1:9;
then      (1/a1) to_power (1/m) < b1/e by A1,Th45,XXREAL_0:25;
then      a to_power d*(1/a) to_power (1/m)<b/e*a to_power d by A62,XREAL_1:68;
then
     a1 to_power d*a1 to_power (-1/m)<b1/e*a1 to_power d by A1,Th32;
then A67:     a to_power (d - 1/m) < b * a to_power d / e by A1,Th27;
     a to_power d / e < 1 by A60,A62,XREAL_1:189;
then      a to_power d / e * b < 1*b by A3,XREAL_1:68;
then      a to_power (d - 1/m) < b by A67,XXREAL_0:2;
then      d - 1/m in X;
then      m>=1 & d - 1/m >= d by A42,SEQ_4:def 2,XXREAL_0:25;
          hence contradiction by XREAL_1:44;
        end;
        hence b = a to_power d by A47,XXREAL_0:1;
      end;
    end;
    hence thesis;
  end;
  uniqueness by A1,A2,Th50;
end;

definition
  let a,b be Real;
  redefine func log(a,b) -> Real;
  coherence by XREAL_0:def 1;
end;

theorem
  a>0 & a<>1 implies log(a,1) = 0
proof
  assume
A1: a>0 & a<>1;
 a to_power 0 = 1 by Th24;
  hence thesis by A1,Def3;
end;

theorem
  a>0 & a<>1 implies log(a,a) = 1
proof
  assume
A1: a>0 & a<>1;
 a to_power 1 = a by Th25;
  hence thesis by A1,Def3;
end;

theorem
  a>0 & a<>1 & b>0 & c>0 implies log(a,b) + log(a,c) = log(a,b*c)
proof
  assume that
A1: a>0 and
A2: a<>1 and
A3: b>0 and
A4: c>0;
A5: a to_power (log(a,b) + log(a,c))
  = a to_power log(a,b) * a to_power log(a,c) by A1,Th27
    .= b * a to_power log(a,c) by A1,A2,A3,Def3
    .= b * c by A1,A2,A4,Def3;
 b*c>0 by A3,A4,XREAL_1:129;
  hence thesis by A1,A2,A5,Def3;
end;

theorem
  a>0 & a<>1 & b>0 & c>0 implies log(a,b) - log(a,c) = log(a,b/c)
proof
  assume that
A1: a>0 and
A2: a<>1 and
A3: b>0 and
A4: c>0;
A5: a to_power (log(a,b) - log(a,c))
  = a to_power log(a,b) / a to_power log(a,c) by A1,Th29
    .= b / a to_power log(a,c) by A1,A2,A3,Def3
    .= b / c by A1,A2,A4,Def3;
 b/c>0 by A3,A4,XREAL_1:139;
  hence thesis by A1,A2,A5,Def3;
end;

theorem
  a>0 & a<>1 & b>0 implies log(a,b to_power c) = c * log(a,b)
proof
  assume that
A1: a>0 and
A2: a<>1 and
A3: b>0;
A4: b to_power c > 0 by A3,Th34;
 a to_power (c*log(a,b)) = (a to_power log(a,b)) to_power c by A1,Th33
    .= b to_power c by A1,A2,A3,Def3;
  hence thesis by A1,A2,A4,Def3;
end;

theorem
  a>0 & a<>1 & b>0 & b<>1 & c>0 implies log(a,c) = log(a,b)*log(b,c)
proof
  assume that
A1: a>0 and
A2: a<>1 and
A3: b>0 and
A4: b<>1 and
A5: c>0;
 a to_power (log(a,b)*log(b,c))
  = a to_power log(a,b) to_power log(b,c) by A1,Th33
    .= b to_power log(b,c) by A1,A2,A3,Def3
    .= c by A3,A4,A5,Def3;
  hence thesis by A1,A2,A5,Def3;
end;

theorem
  a>1 & b>0 & c>b implies log(a,c) > log(a,b)
proof
  assume that
A1: a>1 and
A2: b>0 and
A3: c>b and
A4: log(a,c) <= log(a,b);
A5: a to_power log(a,b) = b by A1,A2,Def3;
A6: a to_power log(a,c) = c by A1,A2,A3,Def3;
 now per cases by A4,XXREAL_0:1;
    suppose
   log(a,c)<log(a,b);
      hence contradiction by A1,A3,A5,A6,Th39;
    end;
    suppose
   log(a,c) = log(a,b);
      hence contradiction by A1,A2,A3,A6,Def3;
    end;
  end;
  hence contradiction;
end;

theorem
  a>0 & a<1 & b>0 & c>b implies log(a,c) < log(a,b)
proof
  assume that
A1: a>0 & a<1 and
A2: b>0 and
A3: c>b and
A4: log(a,c) >= log(a,b);
A5: a to_power log(a,b) = b by A1,A2,Def3;
A6: a to_power log(a,c) = c by A1,A2,A3,Def3;
 now per cases by A4,XXREAL_0:1;
    suppose
   log(a,c)>log(a,b);
      hence contradiction by A1,A3,A5,A6,Th40;
    end;
    suppose
   log(a,c) = log(a,b);
      hence contradiction by A1,A2,A3,A6,Def3;
    end;
  end;
  hence contradiction;
end;

theorem
  for s being Real_Sequence st for n holds s.n = (1 + 1/(n+1)) to_power (n+1 )
  holds s is convergent
proof
  let s be Real_Sequence such that
A1: for n holds s.n = (1 + 1/(n+1)) to_power (n+1);
 now
    let n be Element of NAT;
A2: (1+1/(n+1)) to_power (n+1) > 0 by Th34;
A3: s.(n+1)/s.n =(1 + 1/(n+1+1)) to_power (n+1+1) / s.n by A1
      .=(1 + 1/(n+1+1)) to_power (n+1+1)/(1+1/(n+1)) to_power (n+1)*1 by A1
      .=(1 + 1/(n+1+1)) to_power (n+1+1)/(1 + 1/(n+1)) to_power (n+1) *
    ((1+1/(n+1))/(1+1/(n+1))) by XCMPLX_1:60
      .=(1+1/(n+1)) * (1 + 1/(n+1+1)) to_power (n+1+1) /
    ((1 + 1/(n+1)) to_power (n+1) * (1+1/(n+1))) by XCMPLX_1:76
      .=(1+1/(n+1)) * (1 + 1/(n+1+1)) to_power (n+1+1) /
    ((1 + 1/(n+1)) to_power (n+1) * (1+1/(n+1)) to_power 1) by Th25
      .=(1+1/(n+1)) * (1 + 1/(n+1+1)) to_power (n+1+1) /
    (1 + 1/(n+1)) to_power (n+1+1) by Th27
      .=(1+1/(n+1)) * ((1 + 1/(n+1+1)) to_power (n+1+1) /
    (1 + 1/(n+1)) to_power (n+1+1))
      .=(1+1/(n+1)) * ((1 + 1/(n+1+1))/(1 + 1/(n+1))) to_power (n+1+1)
    by Th31;
A4: (1 + 1/(n+1+1))/(1 + 1/(n+1))
    = ((1*(n+1+1) + 1)/(n+1+1))/(1 + 1/(n+1)) by XCMPLX_1:113
      .= ((n+1+1+1)/(n+1+1))/((1*(n+1) + 1)/(n+1)) by XCMPLX_1:113
      .= ((n+(1+1)+1)*(n+1))/((n+2)*(n+2)) by XCMPLX_1:84
      .= (n*n+n*2+2*n+3+1-1)/((n+2)*(n+2))
      .= ((n+2)*(n+2))/((n+2)*(n+2)) - 1/((n+2)*(n+2))
      .= 1 - 1/((n+2)*(n+2)) by XCMPLX_1:6,60;
 n+1+1>0+1 by XREAL_1:6;
then  (n+2)*(n+2)>1 by XREAL_1:161;
then  1/((n+2)*(n+2))<1 by XREAL_1:212;
then  - 1/((n+2)*(n+2)) > -1 by XREAL_1:24;
then
 (1 + -1/((n+2)*(n+2))) to_power (n+1+1) >= 1 + (n+1+1)*(-1/((n+2)*(n+2)
    )) by PREPOWER:16;
then  (1 - 1/((n+2)*(n+2))) to_power (n+1+1) >= 1 - (n+2)*1/((n+2)*(n+2));
then  (1 - 1/((n+2)*(n+2))) to_power (n+1+1) >= 1 - ((n+2)/(n+2)*1)/(n+2)
    by XCMPLX_1:83;
then  (1 - 1/((n+2)*(n+2))) to_power (n+1+1) >= 1 - (1*1)/(n+2)
    by XCMPLX_1:60;
then  s.(n+1)/s.n >= (1 + 1/(n+1)) * (1 - 1/(n+2)) by A3,A4,XREAL_1:64;
then
 s.(n+1)/s.n >= ((1*(n+1) + 1)/(n+1)) * (1 - 1/(n+2)) by XCMPLX_1:113;
then
 s.(n+1)/s.n >= ((n+2)/(n+1)) * ((1*(n+2) - 1)/(n+2)) by XCMPLX_1:127;
then  s.(n+1)/s.n >= ((n+1)*(n+2))/((n+1)*(n+2)) by XCMPLX_1:76;
then A5: s.(n+1)/s.n >= 1 by XCMPLX_1:6,60;
 s.n>0 by A1,A2;
    hence s.(n+1)>=s.n by A5,XREAL_1:191;
  end;
then A6: s is non-decreasing by SEQM_3:def 8;
 now
    let n;
A7: 2*(n+1)>0 by XREAL_1:129;
A8: 2*(n+1)<>0;
A9: s.(n+(n+1)) = (1 + 1/(2*n+(1+1))) to_power (2*n+1+1) by A1
      .= ((1 + 1/(2*(n+1))) to_power (n+1)) to_power 2 by Th33;
 2*(n+1)+1>0+1 by A7,XREAL_1:6;
then  1/(2*(n+1)+1)<1 by XREAL_1:212;
then A10: - 1/(2*(n+1)+1)> -1 by XREAL_1:24;
then A11: - 1/(2*(n+1)+1) + 1 > -1 + 1 by XREAL_1:6;
A12: (1 + 1/(2*(n+1))) to_power (n+1)
    = (1/(1/(1 + 1/(2*(n+1))))) to_power (n+1)
      .= (1/(1 + 1/(2*(n+1)))) to_power (-(n+1)) by Th32
      .= (1/((1*(2*(n+1)) + 1)/(2*(n+1)))) to_power (-(n+1)) by A8,XCMPLX_1:113
      .= ((2*(n+1)+1-1)/(2*(n+1)+1)) to_power (-(n+1)) by XCMPLX_1:77
      .= ((2*(n+1)+1)/(2*(n+1)+1) - 1/(2*(n+1)+1)) to_power (-(n+1))
      .= (1 - 1/(2*(n+1)+1)) to_power (-(n+1)) by XCMPLX_1:60
      .= 1 / (1 - 1/(2*(n+1)+1)) to_power (n+1) by A11,Th28;
     (
1 + - 1/(2*(n+1)+1)) to_power (n+1) >= 1 + (n+1)*(- 1/(2*(n+1)+1)) by A10,
PREPOWER:16;
then  (1 - 1/(2*(n+1)+1)) to_power (n+1) >= 1-(n+1)/(2*(n+1)+1);
    then A13: (
1 - 1/(2*(n+1)+1)) to_power (n+1) >= (1*(2*(n+1)+1)-(n+1))/(2*(n +1 )+1)
    by XCMPLX_1:127;
 now
      assume (2*(n+1)-n)/(2*(n+1)+1) < 1/2;
then   (2*(n+1)-n)*2 < (2*(n+1)+1)*1 by XREAL_1:102;
then   2*(n+1)+(-n + (2*(n+1)-n)) < 2*(n+1)+1;
      hence contradiction by XREAL_1:6;
    end;
then  (1 - 1/(2*(n+1)+1)) to_power (n+1) >= 1/2 by A13,XXREAL_0:2;
then A14: (1 + 1/(2*(n+1))) to_power (n+1) <= 1/(1/2) by A12,XREAL_1:85;
 (1 + 1/(2*(n+1))) to_power (n+1) > 0 by Th34;
then  ((1 + 1/(2*(n+1))) to_power (n+1))^2 <= 2*2 by A14,XREAL_1:66;
then A15: s.(n+(n+1)) <= 2*2 by A9,Th46;
 s.n<=s.(n+(n+1)) by A6,SEQM_3:5;
then  s.n <= 2*2 by A15,XXREAL_0:2;
    hence s.n < 2*2 + 1 by XXREAL_0:2;
  end;
then  s is bounded_above by SEQ_2:def 3;
  hence thesis by A6;
end;

definition
  func number_e -> real number means
  for s being Real_Sequence st for n holds s.n = (1 + 1/(n+1)) to_power (n+1)
  holds it = lim s;
  existence
  proof
    deffunc F(Element of NAT) = (1 + 1/($1+1)) to_power ($1+1);
    consider s1 being Real_Sequence such that
A1: for n holds s1.n = F(n) from SEQ_1:sch 1;
    take lim s1;
    let s be Real_Sequence such that
A2: for n holds s.n = (1 + 1/(n+1)) to_power (n+1);
 now
      let n be Element of NAT;
      thus s1.n = (1 + 1/(n+1)) to_power (n+1) by A1
        .= s.n by A2;
    end;
    hence thesis by FUNCT_2:63;
  end;
  uniqueness
  proof
    let a,b;
    assume that
A3: for s being Real_Sequence st for n holds s.n = (1 + 1/(n+1)) to_power (n+1)
    holds a = lim s and
A4: for s being Real_Sequence st for n holds s.n = (1 + 1/(n+1)) to_power (n+1)
    holds b = lim s;
    deffunc F(Element of NAT) = (1 + 1/($1+1)) to_power ($1+1);
    consider s1 being Real_Sequence such that
A5: for n holds s1.n = F(n) from SEQ_1:sch 1;
 lim s1 = a by A3,A5;
    hence thesis by A4,A5;
  end;
end;

definition
  redefine func number_e -> Real;
  coherence by XREAL_0:def 1;
end;

theorem Th60:
  2 to_power 2 = 4
proof
  thus 2 to_power 2 = 2^2 by Th46
    .= 4;
end;

theorem Th61:
  2 to_power 3 = 8
proof
  thus 2 to_power 3 = 2 to_power (2+1) .= (2 to_power 2)*(2 to_power 1) by Th27
    .= 4*2 by Th25,Th60
    .= 8;
end;

theorem
  2 to_power 4 = 16
proof
  thus 2 to_power 4 = 2 to_power (2+2) .= (2 to_power 2)*(2 to_power 2) by Th27
    .= 16 by Th60;
end;

theorem
  2 to_power 5 = 32
proof
  thus 2 to_power 5 = 2 to_power (3+2) .= (2 to_power 3)*(2 to_power 2) by Th27
    .= 32 by Th60,Th61;
end;

theorem
  2 to_power 6 = 64
proof
  thus 2 to_power 6 = 2 to_power (3+3) .= 2 to_power 3 * 2 to_power 3 by Th27
    .= 64 by Th61;
end;