now :: thesis: ( a > 0 implies ex d being object st
( a = d |^ n & d > 0 ) )
set X = { b where b is Real : ( 0 < b & b |^ n <= a ) } ;
for x being object st x in { b where b is Real : ( 0 < b & b |^ n <= a ) } holds
x in REAL
proof
let x be object ; :: thesis: ( x in { b where b is Real : ( 0 < b & b |^ n <= a ) } implies x in REAL )
assume x in { b where b is Real : ( 0 < b & b |^ n <= a ) } ; :: thesis: x in REAL
then ex b being Real st
( x = b & 0 < b & b |^ n <= a ) ;
hence x in REAL by XREAL_0:def 1; :: thesis: verum
end;
then reconsider X = { b where b is Real : ( 0 < b & b |^ n <= a ) } as Subset of REAL by TARSKI:def 3;
reconsider a1 = a as Real ;
reconsider j = 1 as Element of REAL by NUMBERS:19;
A2: ( j <= a implies ex c being Real st c in X )
proof
assume A3: j <= a ; :: thesis: ex c being Real st c in X
take j ; :: thesis: j in X
j |^ n <= a by A3, NEWTON:10;
hence j in X ; :: thesis: verum
end;
A4: ( a < 1 implies ex c being Real st c is UpperBound of X )
proof
consider c being Real such that
A5: c = 1 ;
assume A6: a < 1 ; :: thesis: ex c being Real st c is UpperBound of X
take c ; :: thesis: c is UpperBound of X
let b be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not b in X or b <= c )
assume b in X ; :: thesis: b <= c
then consider d being Real such that
A7: ( d = b & 0 < d & d |^ n <= a ) ;
assume not b <= c ; :: thesis: contradiction
then 1 |^ n < d |^ n by A1, A5, Lm1, A7;
then 1 < d |^ n by NEWTON:10;
hence contradiction by A6, A7, XXREAL_0:2; :: thesis: verum
end;
assume A8: a > 0 ; :: thesis: ex d being object st
( a = d |^ n & d > 0 )
( 1 <= a implies ex c being Real st c is UpperBound of X )
proof
assume A9: 1 <= a ; :: thesis: ex c being Real st c is UpperBound of X
take a ; :: thesis: a is UpperBound of X
let b be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not b in X or b <= a )
assume b in X ; :: thesis: b <= a
then consider d being Real such that
A10: ( b = d & 0 < d & d |^ n <= a ) ;
assume a < b ; :: thesis: contradiction
then a |^ n < d |^ n by A1, A8, Lm1, A10;
then a |^ n < a by A10, XXREAL_0:2;
hence contradiction by A1, A9, Th12; :: thesis: verum
end;
then A11: X is bounded_above by A4;
take d = upper_bound X; :: thesis: ( a = d |^ n & d > 0 )
A12: ( a < 1 implies ex c being Real st c in X )
proof
assume A13: a < 1 ; :: thesis: ex c being Real st c in X
reconsider a = a as Real ;
take a ; :: thesis: a in X
a |^ n <= a by A1, A8, A13, Th14;
hence a in X by A8; :: thesis: verum
end;
A14: 0 < d
proof
consider c being Real such that
A15: c in X by A2, A12;
ex e being Real st
( e = c & 0 < e & e |^ n <= a ) by A15;
hence 0 < d by A11, A15, SEQ_4:def 1; :: thesis: verum
end;
A16: not a < d |^ n
proof
set b = (d * (1 - (a / (d |^ n)))) / (n + 1);
assume A17: a < d |^ n ; :: thesis: contradiction
then A18: (1 / (n + 1)) * (d |^ n) > (1 / (n + 1)) * a by XREAL_1:68;
a * ((d |^ n) ") > 0 * a by A8, A17;
then - (- (a / (d |^ n))) > 0 ;
then - (a / (d |^ n)) < 0 ;
then 1 + (- (a / (d |^ n))) < 1 + 0 by XREAL_1:6;
then A19: (1 - (a / (d |^ n))) * ((n + 1) ") < 1 * ((n + 1) ") by XREAL_1:68;
1 < n + 1 by A1, NAT_1:13;
then (n + 1) " < 1 by XREAL_1:212;
then (1 - (a / (d |^ n))) / (n + 1) < 1 by A19, XXREAL_0:2;
then A20: d * ((1 - (a / (d |^ n))) / (n + 1)) < d * 1 by A14, XREAL_1:68;
then ((d * (1 - (a / (d |^ n)))) / (n + 1)) / d < d / d by A14, XREAL_1:74;
then ((d * (1 - (a / (d |^ n)))) / (n + 1)) / d < 1 by A14, XCMPLX_1:60;
then - 1 < - (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d) by XREAL_1:24;
then A21: (1 + (- (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d))) |^ n >= 1 + (n * (- (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d))) by Th16;
a / (d |^ n) < (d |^ n) / (d |^ n) by A8, A17, XREAL_1:74;
then 0 + (a / (d |^ n)) < 1 by A8, A17, XCMPLX_1:60;
then 0 < 1 - (a / (d |^ n)) by XREAL_1:20;
then d * 0 < d * (1 - (a / (d |^ n))) by A14;
then 0 / (n + 1) < (d * (1 - (a / (d |^ n)))) / (n + 1) ;
then consider c being Real such that
A22: c in X and
A23: d - ((d * (1 - (a / (d |^ n)))) / (n + 1)) < c by A2, A12, A11, SEQ_4:def 1;
0 < d - ((d * (1 - (a / (d |^ n)))) / (n + 1)) by A20, XREAL_1:50;
then A24: (d - ((d * (1 - (a / (d |^ n)))) / (n + 1))) |^ n < c |^ n by A1, A23, Lm1;
(1 + (n * (- (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d)))) * (d |^ n) = (1 - (n * (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d))) * (d |^ n)
.= (1 - (n * ((d * ((1 - (a / (d |^ n))) / (n + 1))) / d))) * (d |^ n)
.= (1 - (n * ((((1 - (a / (d |^ n))) / (n + 1)) / d) * d))) * (d |^ n)
.= (1 - (n * ((1 - (a / (d |^ n))) / (n + 1)))) * (d |^ n) by A14, XCMPLX_1:87
.= (1 - (((1 - (a / (d |^ n))) * n) / (n + 1))) * (d |^ n)
.= (1 - ((1 - (a / (d |^ n))) * (n / (n + 1)))) * (d |^ n)
.= ((1 - (n / (n + 1))) + ((a / (d |^ n)) * (n / (n + 1)))) * (d |^ n)
.= ((((n + 1) / (n + 1)) - (n / (n + 1))) + ((a / (d |^ n)) * (n / (n + 1)))) * (d |^ n) by XCMPLX_1:60
.= ((((n + 1) - n) / (n + 1)) + ((a / (d |^ n)) * (n / (n + 1)))) * (d |^ n)
.= ((1 / (n + 1)) + (((n / (n + 1)) * a) / (d |^ n))) * (d |^ n)
.= ((1 / (n + 1)) * (d |^ n)) + ((((n / (n + 1)) * a) / (d |^ n)) * (d |^ n))
.= ((1 / (n + 1)) * (d |^ n)) + ((n / (n + 1)) * a) by A8, A17, XCMPLX_1:87 ;
then A25: (1 + (n * (- (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d)))) * (d |^ n) > ((1 / (n + 1)) * a) + ((n / (n + 1)) * a) by A18, XREAL_1:6;
(d - ((d * (1 - (a / (d |^ n)))) / (n + 1))) |^ n = ((d - ((d * (1 - (a / (d |^ n)))) / (n + 1))) * 1) |^ n
.= ((d - ((d * (1 - (a / (d |^ n)))) / (n + 1))) * ((d ") * d)) |^ n by A14, XCMPLX_0:def 7
.= (((d - ((d * (1 - (a / (d |^ n)))) / (n + 1))) * (d ")) * d) |^ n
.= (((d - ((d * (1 - (a / (d |^ n)))) / (n + 1))) / d) * d) |^ n
.= (((d / d) - (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d)) * d) |^ n
.= ((1 - (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d)) * d) |^ n by A14, XCMPLX_1:60
.= ((1 + (- (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d))) |^ n) * (d |^ n) by NEWTON:7 ;
then (d - ((d * (1 - (a / (d |^ n)))) / (n + 1))) |^ n >= (1 + (n * (- (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d)))) * (d |^ n) by A8, A17, A21, XREAL_1:64;
then (d - ((d * (1 - (a / (d |^ n)))) / (n + 1))) |^ n > ((n + 1) / (n + 1)) * a by A25, XXREAL_0:2;
then A26: (d - ((d * (1 - (a / (d |^ n)))) / (n + 1))) |^ n > 1 * a by XCMPLX_1:60;
ex e being Real st
( e = c & 0 < e & e |^ n <= a ) by A22;
hence contradiction by A24, A26, XXREAL_0:2; :: thesis: verum
end;
not d |^ n < a
proof
set b = min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n)));
set c = (1 + (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))))) * d;
A27: ((1 + (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))))) * d) |^ n = ((1 + (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))))) |^ n) * (d |^ n) by NEWTON:7;
A28: 0 < 3 |^ n by Th6;
(3 |^ n) * (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n)))) <= (((a / (d |^ n)) - 1) / (3 |^ n)) * (3 |^ n) by XREAL_1:64, XXREAL_0:17;
then (3 |^ n) * (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n)))) <= (a / (d |^ n)) - 1 by A28, XCMPLX_1:87;
then A29: 1 + ((3 |^ n) * (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))))) <= a / (d |^ n) by XREAL_1:19;
A30: d |^ n > 0 by A14, Th6;
A31: d |^ n <> 0 by A14, Th6;
assume d |^ n < a ; :: thesis: contradiction
then (d |^ n) / (d |^ n) < a / (d |^ n) by A30, XREAL_1:74;
then 1 < a / (d |^ n) by A31, XCMPLX_1:60;
then 1 - 1 < (a / (d |^ n)) - 1 by XREAL_1:9;
then ((a / (d |^ n)) - 1) / (3 |^ n) > 0 / (3 |^ n) by A28;
then A32: min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))) > 0 by XXREAL_0:15;
then 1 + (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n)))) > 1 + 0 by XREAL_1:6;
then A33: (1 + (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))))) * d > 1 * d by A14, XREAL_1:68;
min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))) <= 1 / 2 by XXREAL_0:17;
then min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))) < 1 by XXREAL_0:2;
then (1 + (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))))) |^ n <= 1 + ((3 |^ n) * (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))))) by A32, Th17;
then (1 + (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))))) |^ n <= a / (d |^ n) by A29, XXREAL_0:2;
then ((1 + (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))))) * d) |^ n <= (a / (d |^ n)) * (d |^ n) by A30, A27, XREAL_1:64;
then A34: ((1 + (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))))) * d) |^ n <= a by A31, XCMPLX_1:87;
(1 + (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))))) * d > 0 * d by A14, A32;
then (1 + (min ((1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))))) * d in X by A34;
hence contradiction by A11, A33, SEQ_4:def 1; :: thesis: verum
end;
hence ( a = d |^ n & d > 0 ) by A14, A16, XXREAL_0:1; :: thesis: verum
end;
hence ( ( a > 0 implies ex b1 being Real st
( b1 |^ n = a & b1 > 0 ) ) & ( a = 0 implies ex b1 being Real st b1 = 0 ) ) ; :: thesis: verum