now
assume A2: a > 0 ; :: thesis: ex d being Element of REAL st
( a = d |^ n & d > 0 )
set X = { b where b is Real : ( 0 < b & b |^ n <= a ) } ;
{ b where b is Real : ( 0 < b & b |^ n <= a ) } is Subset of REAL
proof
for x being set st x in { b where b is Real : ( 0 < b & b |^ n <= a ) } holds
x in REAL
proof
let x be set ; :: 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 ; :: thesis: verum
end;
hence { b where b is Real : ( 0 < b & b |^ n <= a ) } is Subset of REAL by TARSKI:def 3; :: thesis: verum
end;
then reconsider X = { b where b is Real : ( 0 < b & b |^ n <= a ) } as Subset of REAL ;
reconsider a1 = a as Real by XREAL_0:def 1;
A3: ex c being real number st c in X
proof
A4: ( 1 <= a implies ex c being real number st c in X )
proof
assume A5: 1 <= a ; :: thesis: ex c being real number st c in X
consider c being real number such that
A6: c = 1 ;
take c ; :: thesis: c in X
c |^ n <= a by A5, A6, NEWTON:15;
hence c in X by A6; :: thesis: verum
end;
( a < 1 implies ex c being real number st c in X )
proof
assume A7: a < 1 ; :: thesis: ex c being real number st c in X
reconsider a = a as Real by XREAL_0:def 1;
take a ; :: thesis: a in X
a |^ n <= a by A1, A2, A7, Th22;
hence a in X by A2; :: thesis: verum
end;
hence ex c being real number st c in X by A4; :: thesis: verum
end;
A8: X is bounded_above
proof
A9: ( 1 <= a implies ex c being real number st
for b being real number st b in X holds
b <= c )
proof
assume A10: 1 <= a ; :: thesis: ex c being real number st
for b being real number st b in X holds
b <= c
take a1 ; :: thesis: for b being real number st b in X holds
b <= a1
thus for b being real number st b in X holds
b <= a1 :: thesis: verum
proof
let b be real number ; :: thesis: ( b in X implies b <= a1 )
assume b in X ; :: thesis: b <= a1
then A11: ex d being Real st
( b = d & 0 < d & d |^ n <= a ) ;
assume a1 < b ; :: thesis: contradiction
then a |^ n < b |^ n by A1, A2, Lm1;
then a1 |^ n < a1 by A11, XXREAL_0:2;
hence contradiction by A1, A10, Th20; :: thesis: verum
end;
end;
( a < 1 implies ex c being real number st
for b being real number st b in X holds
b <= c )
proof
assume A12: a < 1 ; :: thesis: ex c being real number st
for b being real number st b in X holds
b <= c
consider c being real number such that
A13: c = 1 ;
take c ; :: thesis: for b being real number st b in X holds
b <= c
thus for b being real number st b in X holds
b <= c :: thesis: verum
proof
let b be real number ; :: thesis: ( b in X implies b <= c )
assume b in X ; :: thesis: b <= c
then A14: ex d being Real st
( d = b & 0 < d & d |^ n <= a ) ;
assume not b <= c ; :: thesis: contradiction
then 1 |^ n < b |^ n by A1, A13, Lm1;
then 1 < b |^ n by NEWTON:15;
hence contradiction by A12, A14, XXREAL_0:2; :: thesis: verum
end;
end;
hence X is bounded_above by A9, SEQ_4:def 1; :: thesis: verum
end;
take d = upper_bound X; :: thesis: ( a = d |^ n & d > 0 )
A15: 0 < d
proof
consider c being real number such that
A16: c in X by A3;
ex e being Real st
( e = c & 0 < e & e |^ n <= a ) by A16;
hence 0 < d by A8, A16, SEQ_4:def 4; :: thesis: verum
end;
A17: not a < d |^ n
proof
assume A18: a < d |^ n ; :: thesis: contradiction
set b = (d * (1 - (a / (d |^ n)))) / (n + 1);
a / (d |^ n) < (d |^ n) / (d |^ n) by A2, A18, XREAL_1:76;
then 0 + (a / (d |^ n)) < 1 by A2, A18, XCMPLX_1:60;
then A21: 0 < 1 - (a / (d |^ n)) by XREAL_1:22;
then d * 0 < d * (1 - (a / (d |^ n))) by A15, XREAL_1:70;
then A22: 0 / (n + 1) < (d * (1 - (a / (d |^ n)))) / (n + 1) by XREAL_1:76;
1 < n + 1 by A1, NAT_1:13;
then 1 / (n + 1) < 1 by XREAL_1:214;
then A23: (n + 1) " < 1 ;
(d |^ n) " > 0 by A2, A18;
then a * ((d |^ n) " ) > 0 * a by A2, XREAL_1:70;
then - (- (a / (d |^ n))) > 0 ;
then - (a / (d |^ n)) < 0 ;
then 1 + (- (a / (d |^ n))) < 1 + 0 by XREAL_1:8;
then (1 - (a / (d |^ n))) * ((n + 1) " ) < 1 * ((n + 1) " ) by XREAL_1:70;
then (1 - (a / (d |^ n))) / (n + 1) < (n + 1) " ;
then A24: (1 - (a / (d |^ n))) / (n + 1) < 1 by A23, XXREAL_0:2;
(1 - (a / (d |^ n))) * ((n + 1) " ) > 0 * ((n + 1) " ) by A21, XREAL_1:70;
then (1 - (a / (d |^ n))) / (n + 1) > 0 ;
then d * ((1 - (a / (d |^ n))) / (n + 1)) < d * 1 by A15, A24, XREAL_1:99;
then A25: (d * (1 - (a / (d |^ n)))) / (n + 1) < d ;
consider c being real number such that
A26: ( c in X & d - ((d * (1 - (a / (d |^ n)))) / (n + 1)) < c ) by A3, A8, A22, SEQ_4:def 4;
0 < d - ((d * (1 - (a / (d |^ n)))) / (n + 1)) by A25, XREAL_1:52;
then A27: (d - ((d * (1 - (a / (d |^ n)))) / (n + 1))) |^ n < c |^ n by A1, A26, Lm1;
A28: ex e being Real st
( e = c & 0 < e & e |^ n <= a ) by A26;
((d * (1 - (a / (d |^ n)))) / (n + 1)) / d < d / d by A15, A25, XREAL_1:76;
then ((d * (1 - (a / (d |^ n)))) / (n + 1)) / d < 1 by A15, XCMPLX_1:60;
then A29: - 1 < - (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d) by XREAL_1:26;
A30: (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 A15, 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 A15, XCMPLX_1:60
.= ((1 + (- (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d))) |^ n) * (d |^ n) by NEWTON:12 ;
(1 + (- (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d))) |^ n >= 1 + (n * (- (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d))) by A29, Th24;
then A31: (d - ((d * (1 - (a / (d |^ n)))) / (n + 1))) |^ n >= (1 + (n * (- (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d)))) * (d |^ n) by A2, A18, A30, XREAL_1:66;
A32: (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 A15, XCMPLX_1:88
.= (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 A2, A18, XCMPLX_1:88 ;
(1 / (n + 1)) * (d |^ n) > (1 / (n + 1)) * a by A18, XREAL_1:70;
then (1 + (n * (- (((d * (1 - (a / (d |^ n)))) / (n + 1)) / d)))) * (d |^ n) > ((1 / (n + 1)) * a) + ((n / (n + 1)) * a) by A32, XREAL_1:8;
then (d - ((d * (1 - (a / (d |^ n)))) / (n + 1))) |^ n > ((1 / (n + 1)) + (n / (n + 1))) * a by A31, XXREAL_0:2;
then (d - ((d * (1 - (a / (d |^ n)))) / (n + 1))) |^ n > ((n + 1) / (n + 1)) * a ;
then (d - ((d * (1 - (a / (d |^ n)))) / (n + 1))) |^ n > 1 * a by XCMPLX_1:60;
hence contradiction by A27, A28, XXREAL_0:2; :: thesis: verum
end;
not d |^ n < a
proof
assume A33: d |^ n < a ; :: thesis: contradiction
A34: d |^ n > 0 by A15, Th13;
A35: d |^ n <> 0 by A15, Th13;
(d |^ n) / (d |^ n) < a / (d |^ n) by A33, A34, XREAL_1:76;
then 1 < a / (d |^ n) by A35, XCMPLX_1:60;
then A36: 1 - 1 < (a / (d |^ n)) - 1 by XREAL_1:11;
A37: 0 < 3 |^ n by Th13;
then A38: ((a / (d |^ n)) - 1) / (3 |^ n) > 0 / (3 |^ n) by A36, XREAL_1:76;
set b = min (1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n));
min (1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n)) <= 1 / 2 by XXREAL_0:17;
then A39: min (1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n)) < 1 by XXREAL_0:2;
(3 |^ n) * (min (1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))) <= (((a / (d |^ n)) - 1) / (3 |^ n)) * (3 |^ n) by XREAL_1:66, XXREAL_0:17;
then (3 |^ n) * (min (1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))) <= (a / (d |^ n)) - 1 by A37, XCMPLX_1:88;
then A40: 1 + ((3 |^ n) * (min (1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n)))) <= a / (d |^ n) by XREAL_1:21;
A41: min (1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n)) > 0 by A38, XXREAL_0:15;
then 1 + (min (1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))) > 1 + 0 by XREAL_1:8;
then A42: (1 + (min (1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n)))) * d > 1 * d by A15, XREAL_1:70;
A43: 1 + (min (1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n))) > 0 + 0 by A41;
(1 + (min (1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n)))) |^ n <= 1 + ((3 |^ n) * (min (1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n)))) by A39, A41, Th25;
then A44: (1 + (min (1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n)))) |^ n <= a / (d |^ n) by A40, XXREAL_0:2;
set c = (1 + (min (1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n)))) * d;
A45: (1 + (min (1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n)))) * d > 0 * d by A15, A43, XREAL_1:70;
((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:12;
then ((1 + (min (1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n)))) * d) |^ n <= (a / (d |^ n)) * (d |^ n) by A34, A44, XREAL_1:66;
then ((1 + (min (1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n)))) * d) |^ n <= a by A35, XCMPLX_1:88;
then (1 + (min (1 / 2),(((a1 / (d |^ n)) - 1) / (3 |^ n)))) * d in X by A45;
hence contradiction by A8, A42, SEQ_4:def 4; :: thesis: verum
end;
hence ( a = d |^ n & d > 0 ) by A15, A17, XXREAL_0:1; :: thesis: verum
end;
hence ( ( a > 0 implies ex b1 being real number st
( b1 |^ n = a & b1 > 0 ) ) & ( a = 0 implies ex b1 being real number st b1 = 0 ) ) ; :: thesis: verum