reconsider a1 = a, b1 = b as Real by XREAL_0:def 1;
set X = { c where c is Real : a to_power c <= b } ;
{ c where c is Real : a to_power c <= b } is Subset of REAL
proof
for x being set st x in { c where c is Real : a to_power c <= b } holds
x in REAL
proof
let x be set ; :: 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 ; :: thesis: verum
end;
hence { c where c is Real : a to_power c <= b } is Subset of REAL by TARSKI:def 3; :: thesis: verum
end;
then reconsider X = { c where c is Real : a to_power c <= b } as Subset of REAL ;
A3: ex d being real number st d in X
proof
A4: now
let a, b be real number ; :: thesis: ( a > 1 & b > 0 implies ex d being real number st a to_power d <= b )
assume A5: ( a > 1 & b > 0 ) ; :: thesis: ex d being real number st a to_power d <= b
reconsider a1 = a, b1 = b as Real by XREAL_0:def 1;
set e = a1 - 1;
consider n being Element of NAT such that
A6: n > 1 / (b * (a1 - 1)) by SEQ_4:10;
a1 - 1 > 0 - 1 by A5, XREAL_1:11;
then A7: (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 A8: (1 + (a1 - 1)) to_power n >= n * (a1 - 1) by A7, XXREAL_0:2;
A9: a1 - 1 > 1 - 1 by A5, XREAL_1:11;
then n * (a1 - 1) > (1 / (b * (a1 - 1))) * (a1 - 1) by A6, XREAL_1:70;
then n * (a1 - 1) >= 1 / b by A9, XCMPLX_1:93;
then A10: a to_power n >= 1 / b by A8, XXREAL_0:2;
1 / b > 0 by A5;
then 1 / (a to_power n) <= 1 / (1 / b) by A10, XREAL_1:87;
then 1 / (a to_power n) <= b ;
then a1 to_power (- n) <= b1 by A5, Th33;
hence ex d being real number st a to_power d <= b ; :: thesis: verum
end;
now
per cases ( a > 1 or a < 1 ) by A1, XXREAL_0:1;
suppose a > 1 ; :: thesis: ex d being real number st a to_power d <= b
hence ex d being real number st a to_power d <= b by A2, A4; :: thesis: verum
end;
suppose a < 1 ; :: thesis: ex e being real number st a to_power e <= b
then 1 / a > 1 / 1 by A1, XREAL_1:90;
then consider d being real number such that
A11: (1 / a) to_power d <= b by A2, A4;
a1 to_power (- d) <= b1 by A1, A11, Th37;
hence ex e being real number st a to_power e <= b ; :: thesis: verum
end;
end;
end;
then consider d being real number such that
A12: a to_power d <= b ;
take d ; :: thesis: d in X
d is Real by XREAL_0:def 1;
hence d in X by A12; :: thesis: verum
end;
now
per cases ( a > 1 or a < 1 ) by A1, XXREAL_0:1;
suppose A13: a > 1 ; :: thesis: ex d being Element of REAL st b = a to_power d
A14: X is bounded_above
proof
consider n being Element of NAT such that
A15: n > (b1 - 1) / (a1 - 1) by SEQ_4:10;
a - 1 > 1 - 1 by A13, XREAL_1:11;
then n * (a - 1) > b - 1 by A15, XREAL_1:79;
then A16: 1 + (n * (a - 1)) > 1 + (b - 1) by XREAL_1:8;
a - 1 > 0 - 1 by A1, XREAL_1:11;
then (1 + (a1 - 1)) to_power n >= 1 + (n * (a1 - 1)) by PREPOWER:24;
then A17: a to_power n > b by A16, XXREAL_0:2;
now
let c be real number ; :: thesis: ( c in X implies c <= n )
assume c in X ; :: thesis: c <= n
then ex d being Real st
( d = c & a to_power d <= b ) ;
then a1 to_power c <= a1 to_power n by A17, XXREAL_0:2;
hence c <= n by A13, Th44; :: thesis: verum
end;
hence X is bounded_above by SEQ_4:def 1; :: thesis: verum
end;
take d = upper_bound X; :: thesis: b = a to_power d
A18: not b < a to_power d
proof
assume a to_power d > b ; :: thesis: contradiction
then consider e being real number such that
A19: ( b < e & 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
A20: 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 A21: (a - 1) / ((e / b) - 1) < m by A20, XXREAL_0:2;
e / b > 1 by A2, A19, XREAL_1:189;
then (e / b) - 1 > 1 - 1 by XREAL_1:11;
then A22: a - 1 < m * ((e / b) - 1) by A21, XREAL_1:79;
A23: 1 <= m by XXREAL_0:25;
then (a - 1) / m < (e / b) - 1 by A22, XREAL_1:85;
then A24: ((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 A24, XXREAL_0:2;
then a1 to_power (1 / m) <= e / b1 by A1, Th52, XXREAL_0:25;
then A25: (a to_power (1 / m)) * b <= e by A2, XREAL_1:85;
1 / m > 0 by A23;
then consider c being real number such that
A26: ( c in X & d - (1 / m) < c ) by A3, A14, SEQ_4:def 4;
reconsider c = c as Real by XREAL_0:def 1;
A27: ex g being Real st
( g = c & a to_power g <= b ) by A26;
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 A27, XREAL_1:66;
then (a to_power c) * (a to_power (1 / m)) <= e by A25, XXREAL_0:2;
then A28: a1 to_power (c + (1 / m)) <= e by A1, Th32;
d < c + (1 / m) by A26, XREAL_1:21;
then a1 to_power d <= a1 to_power (c + (1 / m)) by A13, Th44;
hence contradiction by A19, A28, 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 number such that
A29: ( a to_power d < e & e < b ) by XREAL_1:7;
reconsider e = e as Real by XREAL_0:def 1;
A30: a1 to_power d > 0 by A1, Th39;
then b / e > 1 by A29, XREAL_1:189;
then A31: (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
A32: 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 A32;
then ( s is convergent & lim s = 1 ) by A1, Th24;
then consider n being Element of NAT such that
A33: for m being Element of NAT st m >= n holds
abs ((s . m) - 1) < (b / e) - 1 by A31, SEQ_2:def 7;
reconsider m = max 1,n as Element of NAT by XXREAL_0:16;
A34: ( m >= n & m >= 1 ) by XXREAL_0:25;
abs ((s . m) - 1) < (b / e) - 1 by A33, XXREAL_0:25;
then A35: abs ((m -root a) - 1) < (b / e) - 1 by A32;
(m -root a) - 1 <= abs ((m -root a) - 1) by ABSVALUE:11;
then (m -root a) - 1 < (b / e) - 1 by A35, 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 A30, XREAL_1:70;
then a1 to_power (d + (1 / m)) < (b1 / e) * (a1 to_power d) by A1, Th32;
then a to_power (d + (1 / m)) < (b * (a to_power d)) / e ;
then A36: a to_power (d + (1 / m)) < ((a to_power d) / e) * b ;
(a to_power d) / e < 1 by A29, A30, XREAL_1:191;
then ((a to_power d) / e) * b < 1 * b by A2, XREAL_1:70;
then a to_power (d + (1 / m)) <= b by A36, XXREAL_0:2;
then d + (1 / m) in X ;
then d + (1 / m) <= d by A14, SEQ_4:def 4;
then 1 / m <= 0 by XREAL_1:31;
hence contradiction by A34; :: thesis: verum
end;
hence b = a to_power d by A18, XXREAL_0:1; :: thesis: verum
end;
suppose A37: a < 1 ; :: thesis: ex d being Element of REAL st b = a to_power d
A38: X is bounded_below
proof
consider n being Element of NAT such that
A39: n > (b1 - 1) / ((1 / a1) - 1) by SEQ_4:10;
1 / a > 1 / 1 by A1, A37, XREAL_1:90;
then (1 / a) - 1 > 1 - 1 by XREAL_1:11;
then n * ((1 / a) - 1) > b - 1 by A39, XREAL_1:79;
then A40: 1 + (n * ((1 / a) - 1)) > 1 + (b - 1) by XREAL_1:8;
1 / a > 0 by A1;
then (1 / a) - 1 > 0 - 1 by 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 A40, XXREAL_0:2;
then A41: a1 to_power (- n) > b1 by A1, Th37;
now
let c be real number ; :: thesis: ( c in X implies c >= - n )
assume c in X ; :: thesis: c >= - n
then ex d being Real st
( d = c & a to_power d <= b ) ;
then a1 to_power c <= a1 to_power (- n) by A41, XXREAL_0:2;
hence c >= - n by A1, A37, Th45; :: thesis: verum
end;
hence X is bounded_below by SEQ_4:def 2; :: thesis: verum
end;
take d = lower_bound X; :: thesis: b = a to_power d
A42: not b < a to_power d
proof
assume a to_power d > b ; :: thesis: contradiction
then consider e being real number such that
A43: ( b < e & 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
A44: 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 A45: ((1 / a) - 1) / ((e / b) - 1) < m by A44, XXREAL_0:2;
e / b > 1 by A2, A43, XREAL_1:189;
then (e / b) - 1 > 1 - 1 by XREAL_1:11;
then A46: (1 / a) - 1 < m * ((e / b) - 1) by A45, XREAL_1:79;
A47: 1 <= m by XXREAL_0:25;
then ((1 / a) - 1) / m < (e / b) - 1 by A46, XREAL_1:85;
then A48: (((1 / a) - 1) / m) + 1 < ((e / b) - 1) + 1 by XREAL_1:8;
A49: 1 / a > 0 by A1;
then (m -root (1 / a1)) - 1 <= ((1 / a1) - 1) / m by 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 A48, XXREAL_0:2;
then (1 / a1) to_power (1 / m) <= e / b1 by A49, Th52, XXREAL_0:25;
then ((1 / a) to_power (1 / m)) * b <= e by A2, XREAL_1:85;
then A50: (a1 to_power (- (1 / m))) * b1 <= e by A1, Th37;
1 / m > 0 by A47;
then consider c being real number such that
A51: ( c in X & c < d + (1 / m) ) by A3, A38, SEQ_4:def 5;
reconsider c = c as Real by XREAL_0:def 1;
A52: ex g being Real st
( g = c & a to_power g <= b ) by A51;
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 A52, XREAL_1:66;
then (a to_power c) * (a to_power (- (1 / m))) <= e by A50, XXREAL_0:2;
then A53: a1 to_power (c + (- (1 / m))) <= e by A1, Th32;
d > c - (1 / m) by A51, XREAL_1:21;
then a1 to_power d <= a1 to_power (c - (1 / m)) by A1, A37, Th45;
hence contradiction by A43, A53, 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 number such that
A54: ( a to_power d < e & e < b ) by XREAL_1:7;
reconsider e = e as Real by XREAL_0:def 1;
A55: a1 to_power d > 0 by A1, Th39;
then b / e > 1 by A54, XREAL_1:189;
then A56: (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
A57: for n being Element of NAT holds s . n = H1(n) from SEQ_1:sch 1();
 A58: 1 / a > 0 by A1;
for n being Element of NAT st n >= 1 holds
s . n = n -root (1 / a1) by A57;
then ( s is convergent & lim s = 1 ) by A58, Th24;
then consider n being Element of NAT such that
A59: for m being Element of NAT st m >= n holds
abs ((s . m) - 1) < (b / e) - 1 by A56, SEQ_2:def 7;
reconsider m = max 1,n as Element of NAT by XXREAL_0:16;
A60: ( m >= n & m >= 1 ) by XXREAL_0:25;
abs ((s . m) - 1) < (b / e) - 1 by A59, XXREAL_0:25;
then A61: abs ((m -root (1 / a)) - 1) < (b / e) - 1 by A57;
(m -root (1 / a)) - 1 <= abs ((m -root (1 / a)) - 1) by ABSVALUE:11;
then (m -root (1 / a)) - 1 < (b / e) - 1 by A61, XXREAL_0:2;
then m -root (1 / a) < b / e by XREAL_1:11;
then (1 / a1) to_power (1 / m) < b1 / e by A58, Th52, XXREAL_0:25;
then (a to_power d) * ((1 / a) to_power (1 / m)) < (b / e) * (a to_power d) by A55, XREAL_1:70;
then (a1 to_power d) * (a1 to_power (- (1 / m))) < (b1 / e) * (a1 to_power d) by A1, Th37;
then a1 to_power (d + (- (1 / m))) < (b1 / e) * (a1 to_power d) by A1, Th32;
then a to_power (d - (1 / m)) < (b * (a to_power d)) / e ;
then A62: a to_power (d - (1 / m)) < ((a to_power d) / e) * b ;
(a to_power d) / e < 1 by A54, A55, XREAL_1:191;
then ((a to_power d) / e) * b < 1 * b by A2, XREAL_1:70;
then a to_power (d - (1 / m)) < b by A62, XXREAL_0:2;
then d - (1 / m) in X ;
then d - (1 / m) >= d by A38, SEQ_4:def 5;
then 1 / m <= 0 by XREAL_1:46;
hence contradiction by A60; :: thesis: verum
end;
hence b = a to_power d by A42, XXREAL_0:1; :: thesis: verum
end;
end;
end;
hence ex b1 being real number st a to_power b1 = b ; :: thesis: verum