reconsider a1 = a, b1 = b as Real ;
set X = { c where c is Real : a to_power c <= b } ;
for x being object 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;
A4:
ex d being Real st d in X
proof
A5:
now for a, b being Real st a > 1 & b > 0 holds
ex d being Real st a to_power d <= blet a,
b be
Real;
( a > 1 & b > 0 implies ex d being Real st a to_power d <= b )assume that A6:
a > 1
and A7:
b > 0
;
ex d being Real st a to_power d <= breconsider a1 =
a,
b1 =
b as
Real ;
set e =
a1 - 1;
consider n being
Nat such that A8:
n > 1
/ (b * (a1 - 1))
by SEQ_4:3;
a1 - 1
> 0 - 1
by A6, XREAL_1:9;
then A9:
(1 + (a1 - 1)) to_power n >= 1
+ (n * (a1 - 1))
by PREPOWER:16;
1
+ (n * (a1 - 1)) >= 0 + (n * (a1 - 1))
by XREAL_1:6;
then A10:
(1 + (a1 - 1)) to_power n >= n * (a1 - 1)
by A9, XXREAL_0:2;
A11:
a1 - 1
> 1
- 1
by A6, XREAL_1:9;
then
n * (a1 - 1) > (1 / (b * (a1 - 1))) * (a1 - 1)
by A8, XREAL_1:68;
then
n * (a1 - 1) >= 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 being
Real st
a to_power d <= b
;
verum end;
then consider d being
Real such that A13:
a to_power d <= b
;
take
d
;
d in X
thus
d in X
by A13;
verum
end;
now ex d being object st b = a to_power dper cases
( a > 1 or a < 1 )
by A2, XXREAL_0:1;
suppose A14:
a > 1
;
ex d being object st b = a to_power dA15:
X is
bounded_above
take d =
upper_bound X;
b = a to_power dA20:
not
b < a to_power d
proof
assume
a to_power d > b
;
contradiction
then consider e being
Real such that A21:
b < e
and A22:
e < a to_power d
by XREAL_1:5;
reconsider e =
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 being
Real such that A29:
c in X
and A30:
d - (1 / m) < c
by A4, A15, A26, SEQ_4:def 1;
reconsider c =
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;
verum
end;
not
a to_power d < b
proof
assume
a to_power d < b
;
contradiction
then consider e being
Real such that A33:
a to_power d < e
and A34:
e < b
by XREAL_1:5;
reconsider e =
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 H1(
Nat)
-> Real = $1
-root a;
consider s being
Real_Sequence such that A37:
for
n being
Nat holds
s . n = H1(
n)
from SEQ_1:sch 1();
for
n being
Nat 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;
verum
end; hence
b = a to_power d
by A20, XXREAL_0:1;
verum end; suppose A41:
a < 1
;
ex d being object st b = a to_power dA42:
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
;
XXREAL_2:def 9 - n is LowerBound of X
let c be
ExtReal;
XXREAL_2:def 2 ( not c in X or - n <= c )
assume
c in X
;
- n <= c
then consider d being
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;
verum
end; take d =
lower_bound X;
b = a to_power dA47:
not
b < a to_power d
proof
assume
a to_power d > b
;
contradiction
then consider e being
Real such that A48:
b < e
and A49:
e < a to_power d
by XREAL_1:5;
reconsider e =
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 being
Real such that A56:
c in X
and A57:
c < d + (1 / m)
by A4, A42, A53, SEQ_4:def 2;
reconsider c =
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;
verum
end;
not
a to_power d < b
proof
assume
a to_power d < b
;
contradiction
then consider e being
Real such that A60:
a to_power d < e
and A61:
e < b
by XREAL_1:5;
reconsider e =
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 H1(
Nat)
-> Real = $1
-root (1 / a);
consider s being
Real_Sequence such that A64:
for
n being
Nat holds
s . n = H1(
n)
from SEQ_1:sch 1();
for
n being
Nat 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;
verum
end; hence
b = a to_power d
by A47, XXREAL_0:1;
verum end; end; end;
hence
ex b1 being Real st a to_power b1 = b
; verum