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
proof
let x be object ; :: thesis: ( x in { c where c is Real : a to_power c <= b } implies x in REAL )
assume x in { c where c is Real : a to_power c <= b } ; :: thesis: x in REAL
then ex c being Real st
( x = c & a to_power c <= b ) ;
hence x in REAL by XREAL_0:def 1; :: thesis: verum
end;
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 :: thesis: for a, b being Real st a > 1 & b > 0 holds
ex d being Real st a to_power d <= b
let a, b be Real; :: thesis: ( a > 1 & b > 0 implies ex d being Real st a to_power d <= b )
assume that
A6: a > 1 and
A7: b > 0 ; :: thesis: ex d being Real st a to_power d <= b
reconsider 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 ; :: thesis: verum
end;
now :: thesis: ex d being Real st a to_power d <= b
per cases ( a > 1 or a < 1 ) by A2, XXREAL_0:1;
suppose a > 1 ; :: thesis: ex d being Real st a to_power d <= b
hence ex d being Real st a to_power d <= b by A3, A5; :: thesis: verum
end;
suppose a < 1 ; :: thesis: ex e being Real st a to_power e <= b
then 1 / a > 1 / 1 by A1, XREAL_1:88;
then consider d being Real such that
A12: (1 / a) to_power d <= b by A3, A5;
a1 to_power (- d) <= b1 by A1, A12, Th32;
hence ex e being Real st a to_power e <= b ; :: thesis: verum
end;
end;
end;
then consider d being Real such that
A13: a to_power d <= b ;
take d ; :: thesis: d in X
thus d in X by A13; :: thesis: verum
end;
now :: thesis: ex d being object st b = a to_power d
per cases ( a > 1 or a < 1 ) by A2, XXREAL_0:1;
suppose A14: a > 1 ; :: thesis: ex d being object st b = a to_power d
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 ; :: according to XXREAL_2:def 10 :: thesis: n is UpperBound of X
let c be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not c in X or c <= n )
assume c in X ; :: thesis: c <= n
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; :: thesis: verum
end;
take d = upper_bound X; :: thesis: b = a to_power d
A20: not b < a to_power d
proof
assume a to_power d > b ; :: thesis: 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; :: thesis: verum
end;
not a to_power d < b
proof
assume a to_power d < b ; :: thesis: 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; :: thesis: verum
end;
hence b = a to_power d by A20, XXREAL_0:1; :: thesis: verum
end;
suppose A41: a < 1 ; :: thesis: ex d being object st b = a to_power d
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 ; :: according to XXREAL_2:def 9 :: thesis: - n is LowerBound of X
let c be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not c in X or - n <= c )
assume c in X ; :: thesis: - 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; :: thesis: verum
end;
take d = lower_bound X; :: thesis: b = a to_power d
A47: not b < a to_power d
proof
assume a to_power d > b ; :: thesis: 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; :: thesis: verum
end;
not a to_power d < b
proof
assume a to_power d < b ; :: thesis: 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; :: thesis: verum
end;
hence b = a to_power d by A47, XXREAL_0:1; :: thesis: verum
end;
end;
end;
hence ex b1 being Real st a to_power b1 = b ; :: thesis: verum