:: Real Exponents and Logarithms
:: by Konrad Raczkowski and Andrzej N\c{e}dzusiak
::
:: Received October 1, 1990
:: Copyright (c) 1990-2026 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, XCMPLX_0;
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, CARD_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions INT_1, ABIAN, XXREAL_2;
equalities SQUARE_1, XCMPLX_0;
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, ORDINAL1;
schemes SEQ_1;
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 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 natural Number;
let a be Real;
func n-root a -> Real equals
:Def1:
n -Root a if a>=0 & n>=1,
-n -Root (-a) if a<0 & n is odd;
consistency;
coherence;
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 Th6:
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 Th17:
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 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;
func a to_power b -> Real 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;
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;
theorem Th24:
a to_power 0 = 1
proof
thus a to_power 0 = a #Z 0 by Def2
.= 1 by PREPOWER:34;
end;
theorem
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, 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
.= a^2;
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
.= (-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)
.= 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;
assume that
A1: a>0 and
A2: a<>1 and
A3: b>0;
func log(a,b) -> Real means
:Def3:
a to_power it = b;
existence
proof
reconsider a1=a, b1=b as Real;
set X = {c where c is Real: a to_power c <= b};
for x being object holds x in X implies x in REAL
proof
let x be object;
assume x in X;
then ex c be Real st x = c & a to_power c <= b;
hence thesis by XREAL_0:def 1;
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 such that
A6: a>1 and
A7: b>0;
reconsider a1=a, b1=b as Real;
set e = a1-1;
consider n being Nat 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;
thus thesis by A13;
end;
now per cases by A2,XXREAL_0:1;
suppose
A14: a>1;
A15: X is bounded_above
proof consider n being Nat 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 ExtReal;
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 such that
A21: b<e and
A22: e<a to_power d by XREAL_1:5;
reconsider e as Real;
consider n being Nat such that
A23: n > (a1-1)/(e/b1-1) by SEQ_4:3;
reconsider m = max(1,n) as Element of NAT by ORDINAL1:def 12;
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 such that
A29: c in X and
A30: d-1/m < c by A4,A15,A26,SEQ_4:def 1;
reconsider c as Real;
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 such that
A33: a to_power d<e and
A34: e<b by XREAL_1:5;
reconsider e as Real;
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(Nat) = $1-root a;
consider s being Real_Sequence such that
A37: for n being Nat 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 being Nat such that
A38: for m being Nat st m>=n holds |.s.m - 1.|<b/e-1
by A36,SEQ_2:def 7;
reconsider m = max(1,n) as Element of NAT by ORDINAL1:def 12;
|.s.m - 1.|<b/e-1 by A38,XXREAL_0:25;
then A39: |.m-root a - 1.|<b/e-1 by A37;
m-root a - 1<=|.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 being Nat 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 ExtReal;
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 such that
A48: b<e and
A49: e<a to_power d by XREAL_1:5;
reconsider e as Real;
consider n being Nat such that
A50: n > (1/a1-1)/(e/b1-1) by SEQ_4:3;
reconsider m = max(1,n) as Element of NAT by ORDINAL1:def 12;
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 such that
A56: c in X and
A57: c <d+1/m by A4,A42,A53,SEQ_4:def 2;
reconsider c as Real;
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 such that
A60: a to_power d<e and
A61: e<b by XREAL_1:5;
reconsider e as Real;
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(Nat) = $1-root (1/a);
consider s being Real_Sequence such that
A64: for n being Nat 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 being Nat such that
A65: for m being Nat st m>=n holds |.s.m - 1.|<b/e-1
by A63,SEQ_2:def 7;
reconsider m = max(1,n) as Element of NAT by ORDINAL1:def 12;
|.s.m - 1.|<b/e-1 by A65,XXREAL_0:25;
then A66: |.m-root (1/a) - 1.|<b/e-1 by A64;
m-root (1/a) - 1<=|.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;
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;
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 being Nat 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 being Nat holds s.n = (1 + 1/(n+1)) to_power (n+1);
now
let n be 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)
.=(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 be Nat;
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 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(Nat) = (1 + 1/($1+1)) to_power ($1+1);
consider s1 being Real_Sequence such that
A1: for n being Nat 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(Nat) = (1 + 1/($1+1)) to_power ($1+1);
consider s1 being Real_Sequence such that
A5: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
A6: for n holds s1.n = F(n) by A5;
lim s1 = a by A3,A6;
hence thesis by A4,A6;
end;
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 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;
registration
let n be non zero Nat;
reduce n-root 1 to 1;
reducibility by Th6,NAT_1:14;
reduce n-root 0 to 0;
reducibility by Th5,NAT_1:14;
end;
registration
let a be positive Real, n be non zero Nat;
cluster n-root a -> positive;
coherence
proof
n >= 1 by NAT_1:14; then
n-root a > n-root 0 by Th17;
hence thesis;
end;
end;
registration
let a be non negative Real;
cluster 2-root a -> non negative;
coherence by Th7;
end;