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 being set st x in { c where c is Real : a to_power c <= b } holds
x in REAL
then reconsider X = { c where c is Real : a to_power c <= b } as Subset of REAL by TARSKI:def 3;
A7:
ex d being real number st d in X
proof
A8:
now let a,
b be
real number ;
( a > 1 & b > 0 implies ex d being real number st a to_power d <= b )assume that A9:
a > 1
and A10:
b > 0
;
ex d being real number st a to_power d <= breconsider a1 =
a,
b1 =
b as
Real by XREAL_0:def 1;
set e =
a1 - 1;
consider n being
Element of
NAT such that A11:
n > 1
/ (b * (a1 - 1))
by SEQ_4:10;
a1 - 1
> 0 - 1
by A9, XREAL_1:11;
then A13:
(1 + (a1 - 1)) to_power n >= 1
+ (n * (a1 - 1))
by PREPOWER:24;
1
+ (n * (a1 - 1)) >= 0 + (n * (a1 - 1))
by XREAL_1:8;
then A15:
(1 + (a1 - 1)) to_power n >= n * (a1 - 1)
by A13, XXREAL_0:2;
A16:
a1 - 1
> 1
- 1
by A9, XREAL_1:11;
then
n * (a1 - 1) > (1 / (b * (a1 - 1))) * (a1 - 1)
by A11, XREAL_1:70;
then
n * (a1 - 1) >= 1
/ b
by A16, XCMPLX_1:93;
then
a to_power n >= 1
/ b
by A15, XXREAL_0:2;
then
1
/ (a to_power n) <= 1
/ (1 / b)
by A10, XREAL_1:87;
then
a1 to_power (- n) <= b1
by A9, Th33;
hence
ex
d being
real number st
a to_power d <= b
;
verum end;
then consider d being
real number such that A28:
a to_power d <= b
;
take
d
;
d in X
d is
Real
by XREAL_0:def 1;
hence
d in X
by A28;
verum
end;
now per cases
( a > 1 or a < 1 )
by A2, XXREAL_0:1;
suppose A31:
a > 1
;
ex d being Element of REAL st b = a to_power dA32:
X is
bounded_above
take d =
upper_bound X;
b = a to_power dA44:
not
b < a to_power d
proof
assume
a to_power d > b
;
contradiction
then consider e being
real number such that A46:
b < e
and A47:
e < a to_power d
by XREAL_1:7;
reconsider e =
e as
Real by XREAL_0:def 1;
consider n being
Element of
NAT such that A48:
n > (a1 - 1) / ((e / b1) - 1)
by SEQ_4:10;
reconsider m =
max 1,
n as
Element of
NAT by XXREAL_0:16;
n <= m
by XXREAL_0:25;
then A50:
(a - 1) / ((e / b) - 1) < m
by A48, XXREAL_0:2;
e / b > 1
by A3, A46, XREAL_1:189;
then
(e / b) - 1
> 1
- 1
by XREAL_1:11;
then A53:
a - 1
< m * ((e / b) - 1)
by A50, XREAL_1:79;
A54:
1
<= m
by XXREAL_0:25;
then
(a - 1) / m < (e / b) - 1
by A53, XREAL_1:85;
then A56:
((a - 1) / m) + 1
< ((e / b) - 1) + 1
by XREAL_1:8;
(m -root a1) - 1
<= (a1 - 1) / m
by A1, Th23, XXREAL_0:25;
then
((m -root a) - 1) + 1
<= ((a - 1) / m) + 1
by XREAL_1:8;
then
m -root a <= e / b
by A56, XXREAL_0:2;
then
a1 to_power (1 / m) <= e / b1
by A1, Th52, XXREAL_0:25;
then A61:
(a to_power (1 / m)) * b <= e
by A3, XREAL_1:85;
consider c being
real number such that A62:
c in X
and A63:
d - (1 / m) < c
by A7, A32, A54, SEQ_4:def 4;
reconsider c =
c as
Real by XREAL_0:def 1;
A64:
ex
g being
Real st
(
g = c &
a to_power g <= b )
by A62;
a1 to_power (1 / m) >= 0
by A1, Th39;
then
(a to_power c) * (a to_power (1 / m)) <= (a to_power (1 / m)) * b
by A64, XREAL_1:66;
then
(a to_power c) * (a to_power (1 / m)) <= e
by A61, XXREAL_0:2;
then A68:
a1 to_power (c + (1 / m)) <= e
by A1, Th32;
d < c + (1 / m)
by A63, XREAL_1:21;
then
a1 to_power d <= a1 to_power (c + (1 / m))
by A31, Th44;
hence
contradiction
by A47, A68, XXREAL_0:2;
verum
end;
not
a to_power d < b
proof
assume
a to_power d < b
;
contradiction
then consider e being
real number such that A73:
a to_power d < e
and A74:
e < b
by XREAL_1:7;
reconsider e =
e as
Real by XREAL_0:def 1;
A75:
a1 to_power d > 0
by A1, Th39;
then
b / e > 1
by A73, A74, XREAL_1:189;
then A77:
(b / e) - 1
> 1
- 1
by XREAL_1:11;
deffunc H1(
Element of
NAT )
-> real number = $1
-root a;
consider s being
Real_Sequence such that A78:
for
n being
Element of
NAT holds
s . n = H1(
n)
from SEQ_1:sch 1();
for
n being
Element of
NAT st
n >= 1 holds
s . n = n -root a1
by A78;
then
(
s is
convergent &
lim s = 1 )
by A1, Th24;
then consider n being
Element of
NAT such that A81:
for
m being
Element of
NAT st
m >= n holds
abs ((s . m) - 1) < (b / e) - 1
by A77, SEQ_2:def 7;
reconsider m =
max 1,
n as
Element of
NAT by XXREAL_0:16;
abs ((s . m) - 1) < (b / e) - 1
by A81, XXREAL_0:25;
then A83:
abs ((m -root a) - 1) < (b / e) - 1
by A78;
(m -root a) - 1
<= abs ((m -root a) - 1)
by ABSVALUE:11;
then
(m -root a) - 1
< (b / e) - 1
by A83, XXREAL_0:2;
then
m -root a < b / e
by XREAL_1:11;
then
a1 to_power (1 / m) < b1 / e
by A1, Th52, XXREAL_0:25;
then
(a to_power d) * (a to_power (1 / m)) < (b / e) * (a to_power d)
by A75, XREAL_1:70;
then A89:
a to_power (d + (1 / m)) < (b * (a to_power d)) / e
by A1, Th32;
(a to_power d) / e < 1
by A73, A75, XREAL_1:191;
then
((a to_power d) / e) * b < 1
* b
by A3, XREAL_1:70;
then
a to_power (d + (1 / m)) <= b
by A89, XXREAL_0:2;
then
d + (1 / m) in X
;
then
(
m >= 1 &
d + (1 / m) <= d )
by A32, SEQ_4:def 4, XXREAL_0:25;
hence
contradiction
by XREAL_1:31;
verum
end; hence
b = a to_power d
by A44, XXREAL_0:1;
verum end; suppose A95:
a < 1
;
ex d being Element of REAL st b = a to_power dA96:
X is
bounded_below
proof
consider n being
Element of
NAT such that A97:
n > (b1 - 1) / ((1 / a1) - 1)
by SEQ_4:10;
1
/ a > 1
/ 1
by A1, A95, XREAL_1:90;
then
(1 / a) - 1
> 1
- 1
by XREAL_1:11;
then
n * ((1 / a) - 1) > b - 1
by A97, XREAL_1:79;
then A101:
1
+ (n * ((1 / a) - 1)) > 1
+ (b - 1)
by XREAL_1:8;
(1 / a) - 1
> 0 - 1
by A1, XREAL_1:11;
then
(1 + ((1 / a1) - 1)) to_power n >= 1
+ (n * ((1 / a1) - 1))
by PREPOWER:24;
then
(1 / a) to_power n > b
by A101, XXREAL_0:2;
then A105:
a1 to_power (- n) > b1
by A1, Th37;
take
- n
;
XXREAL_2:def 9 - n is LowerBound of X
let c be
ext-real number ;
XXREAL_2:def 2 ( not c in X or - n <= c )
assume
c in X
;
- n <= c
then consider d being
Real such that A108:
(
d = c &
a to_power d <= b )
;
a1 to_power d <= a1 to_power (- n)
by A105, A108, XXREAL_0:2;
hence
c >= - n
by A1, A95, Th45, A108;
verum
end; take d =
lower_bound X;
b = a to_power dA110:
not
b < a to_power d
proof
assume
a to_power d > b
;
contradiction
then consider e being
real number such that A112:
b < e
and A113:
e < a to_power d
by XREAL_1:7;
reconsider e =
e as
Real by XREAL_0:def 1;
consider n being
Element of
NAT such that A114:
n > ((1 / a1) - 1) / ((e / b1) - 1)
by SEQ_4:10;
reconsider m =
max 1,
n as
Element of
NAT by XXREAL_0:16;
n <= m
by XXREAL_0:25;
then A116:
((1 / a) - 1) / ((e / b) - 1) < m
by A114, XXREAL_0:2;
e / b > 1
by A3, A112, XREAL_1:189;
then
(e / b) - 1
> 1
- 1
by XREAL_1:11;
then A119:
(1 / a) - 1
< m * ((e / b) - 1)
by A116, XREAL_1:79;
A120:
1
<= m
by XXREAL_0:25;
then
((1 / a) - 1) / m < (e / b) - 1
by A119, XREAL_1:85;
then A122:
(((1 / a) - 1) / m) + 1
< ((e / b) - 1) + 1
by XREAL_1:8;
(m -root (1 / a1)) - 1
<= ((1 / a1) - 1) / m
by A1, Th23, XXREAL_0:25;
then
((m -root (1 / a)) - 1) + 1
<= (((1 / a) - 1) / m) + 1
by XREAL_1:8;
then
m -root (1 / a) <= e / b
by A122, XXREAL_0:2;
then
(1 / a1) to_power (1 / m) <= e / b1
by A1, Th52, XXREAL_0:25;
then
((1 / a) to_power (1 / m)) * b <= e
by A3, XREAL_1:85;
then A128:
(a1 to_power (- (1 / m))) * b1 <= e
by A1, Th37;
consider c being
real number such that A129:
c in X
and A130:
c < d + (1 / m)
by A7, A96, A120, SEQ_4:def 5;
reconsider c =
c as
Real by XREAL_0:def 1;
A131:
ex
g being
Real st
(
g = c &
a to_power g <= b )
by A129;
a1 to_power (- (1 / m)) >= 0
by A1, Th39;
then
(a to_power c) * (a to_power (- (1 / m))) <= (a to_power (- (1 / m))) * b
by A131, XREAL_1:66;
then
(a to_power c) * (a to_power (- (1 / m))) <= e
by A128, XXREAL_0:2;
then A135:
a1 to_power (c + (- (1 / m))) <= e
by A1, Th32;
d > c - (1 / m)
by A130, XREAL_1:21;
then
a1 to_power d <= a1 to_power (c - (1 / m))
by A1, A95, Th45;
hence
contradiction
by A113, A135, XXREAL_0:2;
verum
end;
not
a to_power d < b
proof
assume
a to_power d < b
;
contradiction
then consider e being
real number such that A140:
a to_power d < e
and A141:
e < b
by XREAL_1:7;
reconsider e =
e as
Real by XREAL_0:def 1;
A142:
a1 to_power d > 0
by A1, Th39;
then
b / e > 1
by A140, A141, XREAL_1:189;
then A144:
(b / e) - 1
> 1
- 1
by XREAL_1:11;
deffunc H1(
Element of
NAT )
-> Real = $1
-root (1 / a);
consider s being
Real_Sequence such that A145:
for
n being
Element of
NAT holds
s . n = H1(
n)
from SEQ_1:sch 1();
for
n being
Element of
NAT st
n >= 1 holds
s . n = n -root (1 / a1)
by A145;
then
(
s is
convergent &
lim s = 1 )
by A1, Th24;
then consider n being
Element of
NAT such that A148:
for
m being
Element of
NAT st
m >= n holds
abs ((s . m) - 1) < (b / e) - 1
by A144, SEQ_2:def 7;
reconsider m =
max 1,
n as
Element of
NAT by XXREAL_0:16;
abs ((s . m) - 1) < (b / e) - 1
by A148, XXREAL_0:25;
then A150:
abs ((m -root (1 / a)) - 1) < (b / e) - 1
by A145;
(m -root (1 / a)) - 1
<= abs ((m -root (1 / a)) - 1)
by ABSVALUE:11;
then
(m -root (1 / a)) - 1
< (b / e) - 1
by A150, XXREAL_0:2;
then
m -root (1 / a) < b / e
by XREAL_1:11;
then
(1 / a1) to_power (1 / m) < b1 / e
by A1, Th52, XXREAL_0:25;
then
(a to_power d) * ((1 / a) to_power (1 / m)) < (b / e) * (a to_power d)
by A142, XREAL_1:70;
then
(a1 to_power d) * (a1 to_power (- (1 / m))) < (b1 / e) * (a1 to_power d)
by A1, Th37;
then A157:
a to_power (d - (1 / m)) < (b * (a to_power d)) / e
by A1, Th32;
(a to_power d) / e < 1
by A140, A142, XREAL_1:191;
then
((a to_power d) / e) * b < 1
* b
by A3, XREAL_1:70;
then
a to_power (d - (1 / m)) < b
by A157, XXREAL_0:2;
then
d - (1 / m) in X
;
then
(
m >= 1 &
d - (1 / m) >= d )
by A96, SEQ_4:def 5, XXREAL_0:25;
hence
contradiction
by XREAL_1:46;
verum
end; hence
b = a to_power d
by A110, XXREAL_0:1;
verum end;
hence
ex b1 being real number st a to_power b1 = b
; verum