now :: thesis: ( a > 0 implies ex d being object st

( a = d |^ n & d > 0 ) )

hence
( ( a > 0 implies ex b( 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

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 )

( a = d |^ n & d > 0 )

( 1 <= a implies ex c being Real st c is UpperBound of X )

take d = upper_bound X; :: thesis: ( a = d |^ n & d > 0 )

A12: ( a < 1 implies ex c being Real st c in X )

end;for x being object st x in { b where b is Real : ( 0 < b & b |^ n <= a ) } holds

x in REAL

proof

then reconsider X = { b where b is Real : ( 0 < b & b |^ n <= a ) } as Subset of REAL by TARSKI:def 3;
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;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

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

A4:
( a < 1 implies ex c being Real st c is UpperBound of X )
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;take j ; :: thesis: j in X

j |^ n <= a by A3, NEWTON:10;

hence j in X ; :: thesis: verum

proof

assume A8:
a > 0
; :: thesis: ex d being object st
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;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

( a = d |^ n & d > 0 )

( 1 <= a implies ex c being Real st c is UpperBound of X )

proof

then A11:
X is bounded_above
by A4;
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;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

take d = upper_bound X; :: thesis: ( a = d |^ n & d > 0 )

A12: ( a < 1 implies ex c being Real st c in X )

proof

A14:
0 < d
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;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

proof

A16:
not a < d |^ n
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;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

proof

not d |^ n < a
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;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

proof

hence
( a = d |^ n & d > 0 )
by A14, A16, XXREAL_0:1; :: thesis: verum
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;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

( b