reconsider a1 = a, b1 = b as Real by XREAL_0:def 1;
set X = { c where c is Real : a to_power c <= b } ;
A4:
for x being set st x in { c where c is Real : a to_power c <= b } holds
x in REAL
reconsider X = { c where c is Real : a to_power c <= b } as Subset of REAL by A4, 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;
A12:
a1 - 1
> 0 - 1
by A9, XREAL_1:11;
A13:
(1 + (a1 - 1)) to_power n >= 1
+ (n * (a1 - 1))
by A12, PREPOWER:24;
A14:
1
+ (n * (a1 - 1)) >= 0 + (n * (a1 - 1))
by XREAL_1:8;
A15:
(1 + (a1 - 1)) to_power n >= n * (a1 - 1)
by A13, A14, XXREAL_0:2;
A16:
a1 - 1
> 1
- 1
by A9, XREAL_1:11;
A17:
n * (a1 - 1) > (1 / (b * (a1 - 1))) * (a1 - 1)
by A11, A16, XREAL_1:70;
A18:
n * (a1 - 1) >= 1
/ b
by A16, A17, XCMPLX_1:93;
A19:
a to_power n >= 1
/ b
by A15, A18, XXREAL_0:2;
A20:
1
/ (a to_power n) <= 1
/ (1 / b)
by A10, A19, XREAL_1:87;
A21:
a1 to_power (- n) <= b1
by A9, A20, Th33;
thus
ex
d being
real number st
a to_power d <= b
by A21;
verum end;
consider d being
real number such that A28:
a to_power d <= b
by A22;
take
d
;
d in X
A29:
d is
Real
by XREAL_0:def 1;
thus
d in X
by A28, A29;
verum
end;
A30:
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 A45:
a to_power d > b
;
contradiction
consider e being
real number such that A46:
b < e
and A47:
e < a to_power d
by A45, 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;
A49:
n <= m
by XXREAL_0:25;
A50:
(a - 1) / ((e / b) - 1) < m
by A48, A49, XXREAL_0:2;
A51:
e / b > 1
by A3, A46, XREAL_1:189;
A52:
(e / b) - 1
> 1
- 1
by A51, XREAL_1:11;
A53:
a - 1
< m * ((e / b) - 1)
by A50, A52, XREAL_1:79;
A54:
1
<= m
by XXREAL_0:25;
A55:
(a - 1) / m < (e / b) - 1
by A53, A54, XREAL_1:85;
A56:
((a - 1) / m) + 1
< ((e / b) - 1) + 1
by A55, XREAL_1:8;
A57:
(m -root a1) - 1
<= (a1 - 1) / m
by A1, Th23, XXREAL_0:25;
A58:
((m -root a) - 1) + 1
<= ((a - 1) / m) + 1
by A57, XREAL_1:8;
A59:
m -root a <= e / b
by A56, A58, XXREAL_0:2;
A60:
a1 to_power (1 / m) <= e / b1
by A1, A59, Th52, XXREAL_0:25;
A61:
(a to_power (1 / m)) * b <= e
by A3, A60, 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;
A65:
a1 to_power (1 / m) >= 0
by A1, Th39;
A66:
(a to_power c) * (a to_power (1 / m)) <= (a to_power (1 / m)) * b
by A64, A65, XREAL_1:66;
A67:
(a to_power c) * (a to_power (1 / m)) <= e
by A61, A66, XXREAL_0:2;
A68:
a1 to_power (c + (1 / m)) <= e
by A1, A67, Th32;
A69:
d < c + (1 / m)
by A63, XREAL_1:21;
A70:
a1 to_power d <= a1 to_power (c + (1 / m))
by A31, A69, Th44;
thus
contradiction
by A47, A68, A70, XXREAL_0:2;
verum
end; A71:
not
a to_power d < b
proof
assume A72:
a to_power d < b
;
contradiction
consider e being
real number such that A73:
a to_power d < e
and A74:
e < b
by A72, XREAL_1:7;
reconsider e =
e as
Real by XREAL_0:def 1;
A75:
a1 to_power d > 0
by A1, Th39;
A76:
b / e > 1
by A73, A74, A75, XREAL_1:189;
A77:
(b / e) - 1
> 1
- 1
by A76, 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();
A79:
for
n being
Element of
NAT st
n >= 1 holds
s . n = n -root a1
by A78;
A80:
(
s is
convergent &
lim s = 1 )
by A1, A79, Th24;
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, A80, SEQ_2:def 7;
reconsider m =
max 1,
n as
Element of
NAT by XXREAL_0:16;
A82:
abs ((s . m) - 1) < (b / e) - 1
by A81, XXREAL_0:25;
A83:
abs ((m -root a) - 1) < (b / e) - 1
by A78, A82;
A84:
(m -root a) - 1
<= abs ((m -root a) - 1)
by ABSVALUE:11;
A85:
(m -root a) - 1
< (b / e) - 1
by A83, A84, XXREAL_0:2;
A86:
m -root a < b / e
by A85, XREAL_1:11;
A87:
a1 to_power (1 / m) < b1 / e
by A1, A86, Th52, XXREAL_0:25;
A88:
(a to_power d) * (a to_power (1 / m)) < (b / e) * (a to_power d)
by A75, A87, XREAL_1:70;
A89:
a to_power (d + (1 / m)) < (b * (a to_power d)) / e
by A1, A88, Th32;
A90:
(a to_power d) / e < 1
by A73, A75, XREAL_1:191;
A91:
((a to_power d) / e) * b < 1
* b
by A3, A90, XREAL_1:70;
A92:
a to_power (d + (1 / m)) <= b
by A89, A91, XXREAL_0:2;
A93:
d + (1 / m) in X
by A92;
A94:
(
m >= 1 &
d + (1 / m) <= d )
by A32, A93, SEQ_4:def 4, XXREAL_0:25;
thus
contradiction
by A94, XREAL_1:31;
verum
end; thus
b = a to_power d
by A44, A71, 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;
A98:
1
/ a > 1
/ 1
by A1, A95, XREAL_1:90;
A99:
(1 / a) - 1
> 1
- 1
by A98, XREAL_1:11;
A100:
n * ((1 / a) - 1) > b - 1
by A97, A99, XREAL_1:79;
A101:
1
+ (n * ((1 / a) - 1)) > 1
+ (b - 1)
by A100, XREAL_1:8;
A102:
(1 / a) - 1
> 0 - 1
by A1, XREAL_1:11;
A103:
(1 + ((1 / a1) - 1)) to_power n >= 1
+ (n * ((1 / a1) - 1))
by A102, PREPOWER:24;
A104:
(1 / a) to_power n > b
by A101, A103, XXREAL_0:2;
A105:
a1 to_power (- n) > b1
by A1, A104, Th37;
thus
X is
bounded_below
by A106, SEQ_4:def 2;
verum
end; take d =
lower_bound X;
b = a to_power dA110:
not
b < a to_power d
proof
assume A111:
a to_power d > b
;
contradiction
consider e being
real number such that A112:
b < e
and A113:
e < a to_power d
by A111, 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;
A115:
n <= m
by XXREAL_0:25;
A116:
((1 / a) - 1) / ((e / b) - 1) < m
by A114, A115, XXREAL_0:2;
A117:
e / b > 1
by A3, A112, XREAL_1:189;
A118:
(e / b) - 1
> 1
- 1
by A117, XREAL_1:11;
A119:
(1 / a) - 1
< m * ((e / b) - 1)
by A116, A118, XREAL_1:79;
A120:
1
<= m
by XXREAL_0:25;
A121:
((1 / a) - 1) / m < (e / b) - 1
by A119, A120, XREAL_1:85;
A122:
(((1 / a) - 1) / m) + 1
< ((e / b) - 1) + 1
by A121, XREAL_1:8;
A123:
(m -root (1 / a1)) - 1
<= ((1 / a1) - 1) / m
by A1, Th23, XXREAL_0:25;
A124:
((m -root (1 / a)) - 1) + 1
<= (((1 / a) - 1) / m) + 1
by A123, XREAL_1:8;
A125:
m -root (1 / a) <= e / b
by A122, A124, XXREAL_0:2;
A126:
(1 / a1) to_power (1 / m) <= e / b1
by A1, A125, Th52, XXREAL_0:25;
A127:
((1 / a) to_power (1 / m)) * b <= e
by A3, A126, XREAL_1:85;
A128:
(a1 to_power (- (1 / m))) * b1 <= e
by A1, A127, 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;
A132:
a1 to_power (- (1 / m)) >= 0
by A1, Th39;
A133:
(a to_power c) * (a to_power (- (1 / m))) <= (a to_power (- (1 / m))) * b
by A131, A132, XREAL_1:66;
A134:
(a to_power c) * (a to_power (- (1 / m))) <= e
by A128, A133, XXREAL_0:2;
A135:
a1 to_power (c + (- (1 / m))) <= e
by A1, A134, Th32;
A136:
d > c - (1 / m)
by A130, XREAL_1:21;
A137:
a1 to_power d <= a1 to_power (c - (1 / m))
by A1, A95, A136, Th45;
thus
contradiction
by A113, A135, A137, XXREAL_0:2;
verum
end; A138:
not
a to_power d < b
proof
assume A139:
a to_power d < b
;
contradiction
consider e being
real number such that A140:
a to_power d < e
and A141:
e < b
by A139, XREAL_1:7;
reconsider e =
e as
Real by XREAL_0:def 1;
A142:
a1 to_power d > 0
by A1, Th39;
A143:
b / e > 1
by A140, A141, A142, XREAL_1:189;
A144:
(b / e) - 1
> 1
- 1
by A143, 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();
A146:
for
n being
Element of
NAT st
n >= 1 holds
s . n = n -root (1 / a1)
by A145;
A147:
(
s is
convergent &
lim s = 1 )
by A1, A146, Th24;
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, A147, SEQ_2:def 7;
reconsider m =
max 1,
n as
Element of
NAT by XXREAL_0:16;
A149:
abs ((s . m) - 1) < (b / e) - 1
by A148, XXREAL_0:25;
A150:
abs ((m -root (1 / a)) - 1) < (b / e) - 1
by A145, A149;
A151:
(m -root (1 / a)) - 1
<= abs ((m -root (1 / a)) - 1)
by ABSVALUE:11;
A152:
(m -root (1 / a)) - 1
< (b / e) - 1
by A150, A151, XXREAL_0:2;
A153:
m -root (1 / a) < b / e
by A152, XREAL_1:11;
A154:
(1 / a1) to_power (1 / m) < b1 / e
by A1, A153, Th52, XXREAL_0:25;
A155:
(a to_power d) * ((1 / a) to_power (1 / m)) < (b / e) * (a to_power d)
by A142, A154, XREAL_1:70;
A156:
(a1 to_power d) * (a1 to_power (- (1 / m))) < (b1 / e) * (a1 to_power d)
by A1, A155, Th37;
A157:
a to_power (d - (1 / m)) < (b * (a to_power d)) / e
by A1, A156, Th32;
A158:
(a to_power d) / e < 1
by A140, A142, XREAL_1:191;
A159:
((a to_power d) / e) * b < 1
* b
by A3, A158, XREAL_1:70;
A160:
a to_power (d - (1 / m)) < b
by A157, A159, XXREAL_0:2;
A161:
d - (1 / m) in X
by A160;
A162:
(
m >= 1 &
d - (1 / m) >= d )
by A96, A161, SEQ_4:def 5, XXREAL_0:25;
thus
contradiction
by A162, XREAL_1:46;
verum
end; thus
b = a to_power d
by A110, A138, XXREAL_0:1;
verum end;
thus
ex b1 being real number st a to_power b1 = b
by A30; verum