let f, k be Nat; :: thesis: ( f = k ! & k > 0 implies ex m, r, s, t, u, W, U, S, T, Q being Nat ex M being non trivial Nat st
( m > 0 & u > 0 & (r + W) + 1 = Py ((M * (U + 1)),(W + 1)) & (((M ^2) - 1) * (S ^2)) + 1 is square & ((((M * U) ^2) - 1) * (T ^2)) + 1 is square & (((W ^2) * (u ^2)) - ((((W ^2) - 1) * S) * u)) - 1, 0 are_congruent_mod Q & (((4 * (f ^2)) - 1) * ((r - (((m * S) * T) * U)) ^2)) + (((4 * (u ^2)) * (S ^2)) * (T ^2)) < ((((8 * f) * u) * S) * T) * (r - (((m * S) * T) * U)) & W = ((100 * f) * k) * (k + 1) & U = ((100 * (u |^ 3)) * (W |^ 3)) + 1 & M = (((100 * m) * U) * W) + 1 & S = (((M - 1) * s) + k) + 1 & T = (((((M * U) - 1) * t) + W) - k) + 1 & Q = (((2 * M) * W) - (W ^2)) - 1 ) )
assume A1: ( f = k ! & k > 0 ) ; :: thesis: ex m, r, s, t, u, W, U, S, T, Q being Nat ex M being non trivial Nat st
( m > 0 & u > 0 & (r + W) + 1 = Py ((M * (U + 1)),(W + 1)) & (((M ^2) - 1) * (S ^2)) + 1 is square & ((((M * U) ^2) - 1) * (T ^2)) + 1 is square & (((W ^2) * (u ^2)) - ((((W ^2) - 1) * S) * u)) - 1, 0 are_congruent_mod Q & (((4 * (f ^2)) - 1) * ((r - (((m * S) * T) * U)) ^2)) + (((4 * (u ^2)) * (S ^2)) * (T ^2)) < ((((8 * f) * u) * S) * T) * (r - (((m * S) * T) * U)) & W = ((100 * f) * k) * (k + 1) & U = ((100 * (u |^ 3)) * (W |^ 3)) + 1 & M = (((100 * m) * U) * W) + 1 & S = (((M - 1) * s) + k) + 1 & T = (((((M * U) - 1) * t) + W) - k) + 1 & Q = (((2 * M) * W) - (W ^2)) - 1 )
set W = ((100 * f) * k) * (k + 1);
set u = (((100 * f) * k) * (k + 1)) |^ k;
set U = ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1;
set IW = ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1));
set IWk = (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k;
A2: len (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) = (((100 * f) * k) * (k + 1)) + 1 by NEWTON:def 4;
( ((f * k) * 100) * (k + 1) >= ((f * k) * 100) * 1 & f >= 1 ) by XREAL_1:64, A1, NAT_1:14;
then ( ((100 * f) * k) * (k + 1) >= f * (100 * k) & f * (100 * k) >= 1 * (100 * k) ) by XREAL_1:64;
then A3: ( ((100 * f) * k) * (k + 1) >= 100 * k & 100 * k >= 5 * k & 100 * k >= 1 * k & 100 * k >= 3 * k ) by XXREAL_0:2, XREAL_1:64;
then A4: ( ((100 * f) * k) * (k + 1) >= 5 * k & ((100 * f) * k) * (k + 1) >= k & ((100 * f) * k) * (k + 1) >= 3 * k ) by XXREAL_0:2;
A5: k <= ((100 * f) * k) * (k + 1) by A3, XXREAL_0:2;
k >= 1 by A1, NAT_1:14;
then 1 + 0 < k + k by XREAL_1:8;
then A6: (1 + 0) + k < (k + k) + k by XREAL_1:6;
then A7: k + 1 < ((100 * f) * k) * (k + 1) by A4, XXREAL_0:2;
( (((100 * f) * k) * (k + 1)) |^ (1 + 1) = (((100 * f) * k) * (k + 1)) * ((((100 * f) * k) * (k + 1)) |^ 1) & (((100 * f) * k) * (k + 1)) |^ 1 = ((100 * f) * k) * (k + 1) ) by NEWTON:6;
then A8: (((100 * f) * k) * (k + 1)) |^ (2 + 1) = ((((100 * f) * k) * (k + 1)) * (((100 * f) * k) * (k + 1))) * (((100 * f) * k) * (k + 1)) by NEWTON:6;
( ((((100 * f) * k) * (k + 1)) |^ k) |^ (1 + 1) = ((((100 * f) * k) * (k + 1)) |^ k) * (((((100 * f) * k) * (k + 1)) |^ k) |^ 1) & ((((100 * f) * k) * (k + 1)) |^ k) |^ 1 = (((100 * f) * k) * (k + 1)) |^ k ) by NEWTON:6;
then A9: ((((100 * f) * k) * (k + 1)) |^ k) |^ (2 + 1) = (((((100 * f) * k) * (k + 1)) |^ k) * ((((100 * f) * k) * (k + 1)) |^ k)) * ((((100 * f) * k) * (k + 1)) |^ k) by NEWTON:6;
( ((((100 * f) * k) * (k + 1)) |^ k) |^ (2 + 1) >= ((((100 * f) * k) * (k + 1)) |^ k) * 1 & (((100 * f) * k) * (k + 1)) |^ 3 >= 1 & ((((100 * f) * k) * (k + 1)) |^ k) |^ 3 >= 1 & (((100 * f) * k) * (k + 1)) |^ 3 >= (((100 * f) * k) * (k + 1)) * 1 ) by A1, NAT_1:14, A8, A9, XREAL_1:64;
then ( (((((100 * f) * k) * (k + 1)) |^ k) |^ 3) * ((((100 * f) * k) * (k + 1)) |^ 3) >= 1 * ((((100 * f) * k) * (k + 1)) |^ k) & (((((100 * f) * k) * (k + 1)) |^ k) |^ 3) * ((((100 * f) * k) * (k + 1)) |^ 3) >= 1 * (((100 * f) * k) * (k + 1)) ) by XREAL_1:66;
then A10: ( ((((((100 * f) * k) * (k + 1)) |^ k) |^ 3) * ((((100 * f) * k) * (k + 1)) |^ 3)) * 100 >= (1 * ((((100 * f) * k) * (k + 1)) |^ k)) * 12 & ((((((100 * f) * k) * (k + 1)) |^ k) |^ 3) * ((((100 * f) * k) * (k + 1)) |^ 3)) * 100 >= (1 * (((100 * f) * k) * (k + 1))) * 2 ) by XREAL_1:66;
A11: 2 * (((100 * f) * k) * (k + 1)) <= ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 by A10, NAT_1:13;
reconsider Wk = (((100 * f) * k) * (k + 1)) - k as Nat by A3, XXREAL_0:2, NAT_1:21;
A12: k < (((100 * f) * k) * (k + 1)) + 1 by A5, NAT_1:13;
then A13: len ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k) = k by A2, FINSEQ_1:59;
consider IWW being FinSequence such that
A14: ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1)) = ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k) ^ IWW by FINSEQ_1:80;
reconsider IWW = IWW as FinSequence of REAL by A14, FINSEQ_1:36;
reconsider k1 = k - 1 as Nat by A1;
A15: len (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k) ^ IWW) = k + (len IWW) by A13, FINSEQ_1:22;
then A16: len IWW = Wk + 1 by A2, A14;
A17: len ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k) = (k1 - 0) + 1 by A12, A2, FINSEQ_1:59;
A18: for i being Nat st i + 1 in dom ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k) holds
((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k) . (i + 1) = ((((100 * f) * k) * (k + 1)) choose (0 + i)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' (0 + i)))

proof

let i be Nat; :: thesis: ( i + 1 in dom ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k) implies ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k) . (i + 1) = ((((100 * f) * k) * (k + 1)) choose (0 + i)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' (0 + i))) )
assume A19: i + 1 in dom ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k) ; :: thesis: ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k) . (i + 1) = ((((100 * f) * k) * (k + 1)) choose (0 + i)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' (0 + i)))
A20: i + 1 in dom (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) by A19, RELAT_1:57;
i + 1 <= k by A19, FINSEQ_3:25, A13;
then i + 1 <= ((100 * f) * k) * (k + 1) by A5, XXREAL_0:2;
then i < ((100 * f) * k) * (k + 1) by NAT_1:13;
then A21: (((100 * f) * k) * (k + 1)) -' i = (((100 * f) * k) * (k + 1)) - i by XREAL_1:233;
A22: (i + 1) - 1 = i ;
((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k) . (i + 1) = (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) . (i + 1) by A19, FUNCT_1:47
.= (((((100 * f) * k) * (k + 1)) choose i) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' i))) * (1 |^ i) by A20, A22, A21, NEWTON:def 4 ;
hence ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k) . (i + 1) = ((((100 * f) * k) * (k + 1)) choose (0 + i)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' (0 + i))) ; :: thesis: verum

end;

A23: ( (((100 * f) * k) * (k + 1)) |^ 0 = 1 & (((100 * f) * k) * (k + 1)) -' 0 = (((100 * f) * k) * (k + 1)) - 0 ) by XREAL_1:233, NEWTON:4;
k1 < k1 + 1 by NAT_1:13;
then k1 < ((100 * f) * k) * (k + 1) by A5, XXREAL_0:2;
then A24: ( 0 < Sum ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k) & Sum ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k) < (2 * ((((100 * f) * k) * (k + 1)) |^ 0)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' 0)) ) by Th14, A11, A17, A18;
set UIWk = (1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k);
A25: (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) = 1 by XCMPLX_1:87;
(((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1) = ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) by NEWTON:6;
then 1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1)) = (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk)) by XCMPLX_1:102;
then A26: (1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk) = (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * ((1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk))
.= (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * 1 by XCMPLX_1:87 ;
rng ((1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k)) c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k)) or y in NAT )
assume A27: y in rng ((1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k)) ; :: thesis: y in NAT
consider i being object such that
A28: ( i in dom ((1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k)) & ((1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k)) . i = y ) by A27, FUNCT_1:def 3;
reconsider i = i as Nat by A28;
A29: dom ((1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k)) = dom ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k) by VALUED_1:def 5;
then A30: ( 1 <= i & i <= k ) by A28, FINSEQ_3:25, A13;
then reconsider i1 = i - 1 as Nat ;
i = i1 + 1 ;
then i1 < k by A30, NAT_1:13;
then A31: ( k -' i1 = k - i1 & (((100 * f) * k) * (k + 1)) -' i1 = (((100 * f) * k) * (k + 1)) - i1 & k -' i = k - i ) by A5, XXREAL_0:2, A30, XREAL_1:233;
then A32: (((100 * f) * k) * (k + 1)) -' i1 = Wk + (k -' i1) ;
k -' i1 = (k -' i) + 1 by A31;
then A33: ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (k -' i1)) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) = (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (k -' i)) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) by NEWTON:6
.= ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (k -' i)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))
.= (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (k -' i) by A25 ;
((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k) . (i1 + 1) = ((((100 * f) * k) * (k + 1)) choose (0 + i1)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' (0 + i1))) by A29, A28, A18;
then ((1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k)) . i = (1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * (((((100 * f) * k) * (k + 1)) choose i1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' i1))) by VALUED_1:6
.= (1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * (((((100 * f) * k) * (k + 1)) choose i1) * (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (k -' i1)))) by A32, NEWTON:8
.= ((((100 * f) * k) * (k + 1)) choose i1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (k -' i)) by A33, A26 ;
hence y in NAT by A28; :: thesis: verum

end;

then reconsider UIWk = (1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k) as FinSequence of NAT by FINSEQ_1:def 4;
reconsider Z = Sum UIWk as Element of NAT by ORDINAL1:def 12;
A34: (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + k) = ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) by NEWTON:8;
A35: ( Z = (1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * (Sum ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k)) & (1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * (Sum ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k)) < (1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * ((2 * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k)) ) by A34, XREAL_1:68, A24, A23, RVSUM_1:87;
set m = Z;
set M = (((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1;
set mu = ((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1);
reconsider M = (((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1 as non trivial Nat by A35, A24, A1;
reconsider MU = M * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) as non trivial Nat ;
set S = Py (M,(k + 1));
set T = Py (MU,(Wk + 1));
reconsider r = (Py ((((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1)),((((100 * f) * k) * (k + 1)) + 1))) - ((((100 * f) * k) * (k + 1)) + 1) as Nat by NAT_1:21, HILB10_1:13;
consider s being Integer such that
A36: (M - 1) * s = (Py (M,(k + 1))) - (k + 1) by INT_1:def 5, HILB10_1:24;
(Py (M,(k + 1))) - (k + 1) >= (k + 1) - (k + 1) by XREAL_1:9, HILB10_1:13;
then s >= 0 by A36;
then reconsider s = s as Element of NAT by INT_1:3;
consider t being Integer such that
A37: (MU - 1) * t = (Py (MU,(Wk + 1))) - (Wk + 1) by INT_1:def 5, HILB10_1:24;
(Py (MU,(Wk + 1))) - (Wk + 1) >= (Wk + 1) - (Wk + 1) by XREAL_1:9, HILB10_1:13;
then t >= 0 by A37;
then reconsider t = t as Element of NAT by INT_1:3;
A38: (((MU - 1) * t) + Wk) + 1 = Py (MU,(Wk + 1)) by A37;
set Q = (((2 * M) * (((100 * f) * k) * (k + 1))) - ((((100 * f) * k) * (k + 1)) ^2)) - 1;
A39: (M * (((100 * f) * k) * (k + 1))) - 1 >= 0 by A1;
((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1)) >= 1 * (((100 * f) * k) * (k + 1)) by XREAL_1:64, A35, A24, NAT_1:14;
then M > 1 * (((100 * f) * k) * (k + 1)) by NAT_1:13;
then ( M * (((100 * f) * k) * (k + 1)) >= (((100 * f) * k) * (k + 1)) * (((100 * f) * k) * (k + 1)) & (((100 * f) * k) * (k + 1)) * (((100 * f) * k) * (k + 1)) = (((100 * f) * k) * (k + 1)) ^2 ) by XREAL_1:64, SQUARE_1:def 1;
then (M * (((100 * f) * k) * (k + 1))) + (M * (((100 * f) * k) * (k + 1))) >= (M * (((100 * f) * k) * (k + 1))) + ((((100 * f) * k) * (k + 1)) ^2) by XREAL_1:7;
then ((M * (((100 * f) * k) * (k + 1))) + (M * (((100 * f) * k) * (k + 1)))) - (((((100 * f) * k) * (k + 1)) ^2) + 1) >= ((M * (((100 * f) * k) * (k + 1))) + ((((100 * f) * k) * (k + 1)) ^2)) - (((((100 * f) * k) * (k + 1)) ^2) + 1) by XREAL_1:9;
then reconsider Q = (((2 * M) * (((100 * f) * k) * (k + 1))) - ((((100 * f) * k) * (k + 1)) ^2)) - 1 as Element of NAT by A39, INT_1:3;
M ^2 = M * M by SQUARE_1:def 1;
then A40: (M ^2) -' 1 = (M ^2) - 1 by NAT_1:14, XREAL_1:233;
A41: ((Px (M,(k + 1))) ^2) - (((M ^2) - 1) * ((Py (M,(k + 1))) ^2)) = 1 by A40, HILB10_1:7;
MU ^2 = MU * MU by SQUARE_1:def 1;
then A42: (MU ^2) -' 1 = (MU ^2) - 1 by XREAL_1:233, NAT_1:14;
((Px (MU,(Wk + 1))) ^2) - (((MU ^2) - 1) * ((Py (MU,(Wk + 1))) ^2)) = 1 by A42, HILB10_1:7;
then A43: (((MU ^2) - 1) * ((Py (MU,(Wk + 1))) ^2)) + 1 is square ;
A44: for i being Nat st i + 1 in dom IWW holds
IWW . (i + 1) = ((((100 * f) * k) * (k + 1)) choose (k + i)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' (k + i)))

proof

let i be Nat; :: thesis: ( i + 1 in dom IWW implies IWW . (i + 1) = ((((100 * f) * k) * (k + 1)) choose (k + i)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' (k + i))) )
assume A45: i + 1 in dom IWW ; :: thesis: IWW . (i + 1) = ((((100 * f) * k) * (k + 1)) choose (k + i)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' (k + i)))
A46: k + (i + 1) in dom (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) by A45, A13, A14, FINSEQ_1:28;
then (k + i) + 1 <= (((100 * f) * k) * (k + 1)) + 1 by A2, FINSEQ_3:25;
then A47: (((100 * f) * k) * (k + 1)) -' (k + i) = (((100 * f) * k) * (k + 1)) - (k + i) by XREAL_1:6, XREAL_1:233;
A48: (k + (i + 1)) - 1 = k + i ;
IWW . (i + 1) = (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) . (k + (i + 1)) by FINSEQ_1:def 7, A13, A14, A45
.= (((((100 * f) * k) * (k + 1)) choose (k + i)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' (k + i)))) * (1 |^ (k + i)) by A46, A48, A47, NEWTON:def 4 ;
hence IWW . (i + 1) = ((((100 * f) * k) * (k + 1)) choose (k + i)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' (k + i))) ; :: thesis: verum

end;

A49: ( 0 < Sum IWW & Sum IWW < (2 * ((((100 * f) * k) * (k + 1)) |^ k)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' k)) ) by A16, Th14, A11, A5, A1, A44;
set UIWW = (1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * IWW;
set D = Sum ((1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * IWW);
A50: (((100 * f) * k) * (k + 1)) -' k = Wk by A3, XXREAL_0:2, XREAL_1:233;
A51: ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 >= 1 by NAT_1:14;
((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1)) >= 1 * (((100 * f) * k) * (k + 1)) by A35, A24, NAT_1:14, XREAL_1:64;
then (((100 * f) * k) * (k + 1)) + 1 <= (M - 1) + 1 by XREAL_1:6;
then A52: ((((100 * f) * k) * (k + 1)) + 1) * 1 <= M * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) by A51, XREAL_1:66;
((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 < (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1 by NAT_1:13;
then M * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) <= M * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1) by XREAL_1:64;
then (((100 * f) * k) * (k + 1)) + 1 <= M * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1) by A52, XXREAL_0:2;
then ((100 * f) * k) * (k + 1) < M * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1) by NAT_1:13;
then consider t1 being _Theta such that
A53: Py ((((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1)),((((100 * f) * k) * (k + 1)) + 1)) = ((2 * (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) |^ (((100 * f) * k) * (k + 1))) * (1 + (t1 * ((((100 * f) * k) * (k + 1)) / (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))))) by Th10;
reconsider I = 1 as _Theta by Def1;
set E = (t1 * ((((100 * f) * k) * (k + 1)) / (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1)))) - (((((100 * f) * k) * (k + 1)) + 1) / ((2 * (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) |^ (((100 * f) * k) * (k + 1))));
( (((100 * f) * k) * (k + 1)) |^ (1 + 1) = (((100 * f) * k) * (k + 1)) * ((((100 * f) * k) * (k + 1)) |^ 1) & (((100 * f) * k) * (k + 1)) |^ 1 = ((100 * f) * k) * (k + 1) ) by NEWTON:6;
then A54: (((100 * f) * k) * (k + 1)) |^ (2 + 1) = ((((100 * f) * k) * (k + 1)) * (((100 * f) * k) * (k + 1))) * (((100 * f) * k) * (k + 1)) by NEWTON:6;
A55: ((100 * f) * k) * (k + 1) >= 1 by A1, NAT_1:14;
A56: 2 * (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1)) >= 1 by NAT_1:14;
( ((f * k) * 100) * (k + 1) >= ((f * k) * 100) * 1 & f >= 1 ) by XREAL_1:64, A1, NAT_1:14;
then ( ((100 * f) * k) * (k + 1) >= f * (100 * k) & f * (100 * k) >= 1 * (100 * k) ) by XREAL_1:64;
then ( ((100 * f) * k) * (k + 1) >= 100 * k & 100 * k >= 5 * k & 100 * k >= 1 * k ) by XXREAL_0:2, XREAL_1:64;
then A57: k <= ((100 * f) * k) * (k + 1) by XXREAL_0:2;
(((100 * f) * k) * (k + 1)) |^ k >= 1 by NAT_1:14, A1;
then A58: ( ((((100 * f) * k) * (k + 1)) |^ k) |^ 3 >= (((100 * f) * k) * (k + 1)) |^ k & (((100 * f) * k) * (k + 1)) |^ 3 >= 1 & (((100 * f) * k) * (k + 1)) |^ 3 >= ((100 * f) * k) * (k + 1) & ((((100 * f) * k) * (k + 1)) |^ k) |^ 3 >= 1 ) by A55, PREPOWER:12, NAT_1:14;
then ( (((((100 * f) * k) * (k + 1)) |^ k) |^ 3) * ((((100 * f) * k) * (k + 1)) |^ 3) >= ((((100 * f) * k) * (k + 1)) |^ k) * 1 & (((((100 * f) * k) * (k + 1)) |^ k) |^ 3) * ((((100 * f) * k) * (k + 1)) |^ 3) >= (((100 * f) * k) * (k + 1)) * 1 ) by XREAL_1:66;
then ( ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 > 100 * ((((((100 * f) * k) * (k + 1)) |^ k) |^ 3) * ((((100 * f) * k) * (k + 1)) |^ 3)) & 100 * ((((((100 * f) * k) * (k + 1)) |^ k) |^ 3) * ((((100 * f) * k) * (k + 1)) |^ 3)) >= 100 * ((((100 * f) * k) * (k + 1)) |^ k) & 100 * ((((((100 * f) * k) * (k + 1)) |^ k) |^ 3) * ((((100 * f) * k) * (k + 1)) |^ 3)) >= 100 * (((100 * f) * k) * (k + 1)) ) by XREAL_1:64, NAT_1:13;
then A59: ( ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 >= 100 * ((((100 * f) * k) * (k + 1)) |^ k) & 100 * ((((100 * f) * k) * (k + 1)) |^ k) >= 12 * ((((100 * f) * k) * (k + 1)) |^ k) & ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 >= 100 * (((100 * f) * k) * (k + 1)) & 100 * ((((100 * f) * k) * (k + 1)) |^ k) >= 16 * ((((100 * f) * k) * (k + 1)) |^ k) ) by XXREAL_0:2, XREAL_1:64;
Z * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) >= 1 by NAT_1:14, A35, A24;
then ( (100 * (((100 * f) * k) * (k + 1))) * (Z * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) >= (100 * (((100 * f) * k) * (k + 1))) * 1 & (100 * (((100 * f) * k) * (k + 1))) * 1 >= 5 * k ) by A57, XREAL_1:66;
then (100 * (((100 * f) * k) * (k + 1))) * (Z * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) >= 5 * k by XXREAL_0:2;
then A60: 5 * k <= M by NAT_1:13;
then A61: (5 * k) / M <= 1 by XREAL_1:183;
A62: 2 * k <= 5 * k by XREAL_1:64;
then A63: M >= 2 * k by A60, XXREAL_0:2;
then (2 * k) / M <= 1 by XREAL_1:183;
then A64: 2 * (k / M) <= 1 by XCMPLX_1:74;
A65: ( 4 * (((100 * f) * k) * (k + 1)) <= 100 * (((100 * f) * k) * (k + 1)) & 2 * (((100 * f) * k) * (k + 1)) <= 100 * (((100 * f) * k) * (k + 1)) ) by XREAL_1:64;
then A66: ( 4 * (((100 * f) * k) * (k + 1)) <= ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 & 2 * (((100 * f) * k) * (k + 1)) <= ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 ) by A59, XXREAL_0:2;
then A67: 2 * (((100 * f) * k) * (k + 1)) <= (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1 by NAT_1:13;
((100 * f) * k) * (k + 1) <= (((100 * f) * k) * (k + 1)) + (((100 * f) * k) * (k + 1)) by NAT_1:11;
then A68: ((100 * f) * k) * (k + 1) <= ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 by A66, XXREAL_0:2;
Wk <= (((100 * f) * k) * (k + 1)) - 0 by XREAL_1:10;
then ( 4 * Wk <= 4 * (((100 * f) * k) * (k + 1)) & 2 * Wk <= 2 * (((100 * f) * k) * (k + 1)) ) by XREAL_1:64;
then A69: ( 4 * Wk <= ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 & 2 * Wk <= ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 ) by A66, XXREAL_0:2;
then (4 * Wk) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) <= 1 by XREAL_1:183;
then A70: ((4 * Wk) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (1 / M) <= 1 * (1 / M) by XREAL_1:64;
2 * (2 * (Wk / MU)) = 4 * (Wk / MU)
.= (4 * Wk) / MU by XCMPLX_1:74
.= ((4 * Wk) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (1 / M) by XCMPLX_1:103 ;
then A71: ( (2 * (1 / M)) + (2 * (2 * (Wk / MU))) <= (2 * (1 / M)) + (1 * (1 / M)) & (2 * (1 / M)) + (1 * (1 / M)) = 3 * (1 / M) & 3 * (1 / M) = (3 * 1) / M ) by A70, XREAL_1:6, XCMPLX_1:74;
3 * 1 <= 3 * k by XREAL_1:64, A1, NAT_1:14;
then (3 * 1) / M <= (3 * k) / M by XREAL_1:72;
then (2 * (1 / M)) + (2 * (2 * (Wk / MU))) <= (3 * k) / M by A71, XXREAL_0:2;
then A72: (2 * (k / M)) + ((2 * (1 / M)) + (2 * (2 * (Wk / MU)))) <= (2 * (k / M)) + ((3 * k) / M) by XREAL_1:6;
2 * (k / M) = (2 * k) / M by XCMPLX_1:74;
then A73: (2 * (k / M)) + ((3 * k) / M) = ((2 * k) + (3 * k)) / M by XCMPLX_1:62;
then ( ((2 * (k / M)) + (2 * (1 / M))) + 0 <= ((2 * (k / M)) + (2 * (1 / M))) + (2 * (2 * (Wk / MU))) & ((2 * (k / M)) + (2 * (1 / M))) + (2 * (2 * (Wk / MU))) <= 1 ) by A72, A61, XXREAL_0:2, XREAL_1:6;
then A74: (2 * (k / M)) + (2 * (1 / M)) <= 1 by XXREAL_0:2;
A75: 2 * (((100 * f) * k) * (k + 1)) <= ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 by A65, A59, XXREAL_0:2;
M >= 1 by NAT_1:14;
then A76: MU >= 1 * (2 * Wk) by A69, XREAL_1:66;
2 * k >= 1 * k by XREAL_1:64;
then consider t3 being _Theta such that
A77: Py (M,(k + 1)) = ((2 * M) |^ k) * (1 + (t3 * (k / M))) by Th10, A63, XXREAL_0:2;
2 * Wk >= 1 * Wk by XREAL_1:64;
then consider t4 being _Theta such that
A78: Py (MU,(Wk + 1)) = ((2 * MU) |^ Wk) * (1 + (t4 * (Wk / MU))) by Th10, A76, XXREAL_0:2;
1 * M >= 2 * k by A62, A60, XXREAL_0:2;
then k / M <= 1 / 2 by XREAL_1:102;
then consider T3 being _Theta such that
A79: 1 / (1 + (t3 * (k / M))) = 1 + ((T3 * 2) * (k / M)) by Th7;
1 * MU >= 2 * Wk by A76;
then Wk / MU <= 1 / 2 by XREAL_1:102;
then consider T4 being _Theta such that
A80: 1 / (1 + (t4 * (Wk / MU))) = 1 + ((T4 * 2) * (Wk / MU)) by Th7;
1 * (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1)) >= M * (2 * (((100 * f) * k) * (k + 1))) by A67, XREAL_1:64;
then ((((100 * f) * k) * (k + 1)) * (2 * M)) / (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1)) <= 1 by XREAL_1:79;
then (2 * M) * ((((100 * f) * k) * (k + 1)) / (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) <= 1 by XCMPLX_1:74;
then A81: (((100 * f) * k) * (k + 1)) / (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1)) <= 1 / (2 * M) by XREAL_1:77;
then A82: - ((((100 * f) * k) * (k + 1)) / (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) >= - (1 / (2 * M)) by XREAL_1:24;
( - 1 <= t1 & t1 <= 1 ) by Def1;
then ( (- 1) * ((((100 * f) * k) * (k + 1)) / (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) <= t1 * ((((100 * f) * k) * (k + 1)) / (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) & t1 * ((((100 * f) * k) * (k + 1)) / (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) <= 1 * ((((100 * f) * k) * (k + 1)) / (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) ) by XREAL_1:64;
then A83: ( - (1 / (2 * M)) <= t1 * ((((100 * f) * k) * (k + 1)) / (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) & t1 * ((((100 * f) * k) * (k + 1)) / (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) <= 1 / (2 * M) ) by A81, A82, XXREAL_0:2;
(((100 * f) * k) * (k + 1)) + 1 <= (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1 by A68, XREAL_1:6;
then A84: ((((100 * f) * k) * (k + 1)) + 1) * (2 * M) <= ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1) * (2 * M) by XREAL_1:64;
2 * (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1)) <= (2 * (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) |^ (((100 * f) * k) * (k + 1)) by A56, A55, PREPOWER:12;
then ((((100 * f) * k) * (k + 1)) + 1) * (2 * M) <= 1 * ((2 * (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) |^ (((100 * f) * k) * (k + 1))) by A84, XXREAL_0:2;
then ((((100 * f) * k) * (k + 1)) + 1) / ((2 * (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) |^ (((100 * f) * k) * (k + 1))) <= 1 / (2 * M) by XREAL_1:102;
then ( 1 / (2 * M) >= - (((((100 * f) * k) * (k + 1)) + 1) / ((2 * (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) |^ (((100 * f) * k) * (k + 1)))) & - (((((100 * f) * k) * (k + 1)) + 1) / ((2 * (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) |^ (((100 * f) * k) * (k + 1)))) >= - (1 / (2 * M)) ) by XREAL_1:24;
then A85: ( (- (1 / (2 * M))) + (- (1 / (2 * M))) <= (t1 * ((((100 * f) * k) * (k + 1)) / (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1)))) + (- (((((100 * f) * k) * (k + 1)) + 1) / ((2 * (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) |^ (((100 * f) * k) * (k + 1))))) & (t1 * ((((100 * f) * k) * (k + 1)) / (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1)))) + (- (((((100 * f) * k) * (k + 1)) + 1) / ((2 * (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) |^ (((100 * f) * k) * (k + 1))))) <= (1 / (2 * M)) + (1 / (2 * M)) ) by A83, XREAL_1:7;
A86: (1 * 1) / (2 * M) = (1 / 2) * (1 / M) by XCMPLX_1:76;
A87: (t1 * ((((100 * f) * k) * (k + 1)) / (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1)))) - (((((100 * f) * k) * (k + 1)) + 1) / ((2 * (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) |^ (((100 * f) * k) * (k + 1)))) <= I * (1 / M) by A85, A86;
A88: (- I) * (1 / M) <= (t1 * ((((100 * f) * k) * (k + 1)) / (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1)))) - (((((100 * f) * k) * (k + 1)) + 1) / ((2 * (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) |^ (((100 * f) * k) * (k + 1)))) by A85, A86;
consider t2 being _Theta such that
A89: (t1 * ((((100 * f) * k) * (k + 1)) / (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1)))) - (((((100 * f) * k) * (k + 1)) + 1) / ((2 * (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) |^ (((100 * f) * k) * (k + 1)))) = t2 * (1 / M) by A87, A88, Th4;
consider T5 being _Theta such that
A90: (1 + (T3 * (2 * (k / M)))) * (1 + (t2 * (1 / M))) = 1 + (T5 * ((2 * (k / M)) + (2 * (1 / M)))) by A64, Th3;
consider T6 being _Theta such that
A91: (1 + (T5 * ((2 * (k / M)) + (2 * (1 / M))))) * (1 + (T4 * (2 * (Wk / MU)))) = 1 + (T6 * (((2 * (k / M)) + (2 * (1 / M))) + (2 * (2 * (Wk / MU))))) by A74, Th3;
A92: |.(((2 * (k / M)) + (2 * (1 / M))) + (2 * (2 * (Wk / MU)))).| = ((2 * (k / M)) + (2 * (1 / M))) + (2 * (2 * (Wk / MU))) ;
A93: |.((5 * k) / M).| = (5 * k) / M ;
consider T7 being _Theta such that
A94: T6 * (((2 * (k / M)) + (2 * (1 / M))) + (2 * (2 * (Wk / MU)))) = T7 * ((5 * k) / M) by A73, A72, A92, A93, Th2;
A95: 1 / (Py (M,(k + 1))) = (1 / ((2 * M) |^ k)) * (1 + ((T3 * 2) * (k / M))) by A79, A77, XCMPLX_1:102;
A96: 1 / (Py (MU,(Wk + 1))) = (1 / ((2 * MU) |^ Wk)) * (1 + ((T4 * 2) * (Wk / MU))) by A80, A78, XCMPLX_1:102;
A97: (2 * (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) |^ (((100 * f) * k) * (k + 1)) = ((2 * M) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1)) |^ (((100 * f) * k) * (k + 1))
.= ((2 * M) |^ (((100 * f) * k) * (k + 1))) * (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1) |^ (((100 * f) * k) * (k + 1))) by NEWTON:7 ;
((2 * M) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) |^ Wk = ((2 * M) |^ Wk) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk) by NEWTON:7;
then A98: ((2 * M) |^ k) * ((2 * MU) |^ Wk) = (((2 * M) |^ k) * ((2 * M) |^ Wk)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk)
.= ((2 * M) |^ (k + Wk)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk) by NEWTON:8 ;
(1 / ((2 * M) |^ k)) * (1 / ((2 * MU) |^ Wk)) = 1 / (((2 * M) |^ (((100 * f) * k) * (k + 1))) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk)) by A98, XCMPLX_1:102;
then A99: (((2 * (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) |^ (((100 * f) * k) * (k + 1))) * (1 / ((2 * M) |^ k))) * (1 / ((2 * MU) |^ Wk)) = (((2 * M) |^ (((100 * f) * k) * (k + 1))) * (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1) |^ (((100 * f) * k) * (k + 1)))) * (1 / (((2 * M) |^ (((100 * f) * k) * (k + 1))) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk))) by A97
.= (((2 * M) |^ (((100 * f) * k) * (k + 1))) * (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1) |^ (((100 * f) * k) * (k + 1)))) / (((2 * M) |^ (((100 * f) * k) * (k + 1))) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk)) by XCMPLX_1:99
.= (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1) |^ (((100 * f) * k) * (k + 1))) / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk) by XCMPLX_1:91 ;
r = (((2 * (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) |^ (((100 * f) * k) * (k + 1))) * (1 + (t1 * ((((100 * f) * k) * (k + 1)) / (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1)))))) - ((((((100 * f) * k) * (k + 1)) + 1) / ((2 * (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) |^ (((100 * f) * k) * (k + 1)))) * ((2 * (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) |^ (((100 * f) * k) * (k + 1)))) by A53, XCMPLX_1:87;
then r = ((2 * (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) |^ (((100 * f) * k) * (k + 1))) * ((1 + (t1 * ((((100 * f) * k) * (k + 1)) / (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))))) - (((((100 * f) * k) * (k + 1)) + 1) / ((2 * (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) |^ (((100 * f) * k) * (k + 1))))) ;
then A100: r = ((2 * (((((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1))) |^ (((100 * f) * k) * (k + 1))) * (1 + (t2 * (1 / M))) by A89;
A101: r / ((Py (M,(k + 1))) * (Py (MU,(Wk + 1)))) = r * (1 / ((Py (M,(k + 1))) * (Py (MU,(Wk + 1))))) by XCMPLX_1:99
.= r * ((1 / (Py (M,(k + 1)))) * (1 / (Py (MU,(Wk + 1))))) by XCMPLX_1:102
.= ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1) |^ (((100 * f) * k) * (k + 1))) / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk)) * (((1 + (t2 * (1 / M))) * (1 + ((T3 * 2) * (k / M)))) * (1 + ((T4 * 2) * (Wk / MU)))) by A96, A95, A99, A100
.= ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1) |^ (((100 * f) * k) * (k + 1))) / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk)) * (1 + (T7 * ((5 * k) / M))) by A90, A91, A94 ;
A102: ( Sum ((1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * IWW) = (1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * (Sum IWW) & (1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * (Sum IWW) < (1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * ((2 * ((((100 * f) * k) * (k + 1)) |^ k)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk)) ) by A50, XREAL_1:68, A49, RVSUM_1:87;
( ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1) |^ (((100 * f) * k) * (k + 1)) = Sum (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) & Sum (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) = (Sum ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k)) + (Sum IWW) ) by A14, RVSUM_1:75, NEWTON:30;
then A103: Z + (Sum ((1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * IWW)) = (1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1) |^ (((100 * f) * k) * (k + 1))) by A102, A35
.= (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1) |^ (((100 * f) * k) * (k + 1))) / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1)) by XCMPLX_1:99 ;
A104: ((100 * f) * k) * (k + 1) >= k + 1 by A6, A4, XXREAL_0:2;
A105: ((100 * f) * k) * (k + 1) > k by NAT_1:13, A7;
A106: k >= 1 by A1, NAT_1:14;
A107: ( k -' 0 = k - 0 & (((100 * f) * k) * (k + 1)) -' 0 = (((100 * f) * k) * (k + 1)) - 0 & k -' 1 = k - 1 ) by A1, NAT_1:14, XREAL_1:233;
then (((100 * f) * k) * (k + 1)) -' 0 = Wk + (k -' 0) ;
then A108: (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' 0) = ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (k -' 0)) by NEWTON:8;
k -' 0 = (k -' 1) + 1 by A107;
then A109: ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (k -' 0)) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) = (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (k -' 1)) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) by NEWTON:6
.= ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (k -' 1)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))
.= (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (k -' 1) by A25 ;
((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1),1) In_Power (((100 * f) * k) * (k + 1))) | k) . (0 + 1) = ((((100 * f) * k) * (k + 1)) choose (0 + 0)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' (0 + 0))) by A13, FINSEQ_3:25, A106, A18;
then A110: UIWk . 1 = (1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * (((((100 * f) * k) * (k + 1)) choose 0) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' 0))) by VALUED_1:6
.= ((((100 * f) * k) * (k + 1)) choose 0) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k1) by A107, A109, A26, A108
.= 1 * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k1) by NEWTON:19 ;
reconsider Z = Sum UIWk as Element of NAT by ORDINAL1:def 12;
consider uiwk being FinSequence of NAT , y being Element of NAT such that
A111: UIWk = <*y*> ^ uiwk by A17, FINSEQ_2:130;
Sum UIWk = y + (Sum uiwk) by A111, RVSUM_1:76;
then A112: Sum UIWk >= y + 0 by XREAL_1:6;
A113: (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k1) = (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (k1 + 1) by NEWTON:6;
((100 * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) * Z >= ((100 * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k1) by A112, A110, A111, XREAL_1:64;
then A114: M > (100 * (((100 * f) * k) * (k + 1))) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) by A113, NAT_1:13;
(k + 1) * (f * k) >= 1 * (f * k) by NAT_1:11, XREAL_1:64;
then ((k + 1) * (f * k)) * 100 >= (1 * (f * k)) * 3 by XREAL_1:66;
then (100 * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k)) * (((100 * f) * k) * (k + 1)) >= (100 * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k)) * ((3 * f) * k) by XREAL_1:64;
then A115: M > 300 * (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * (f * k)) by A114, XXREAL_0:2;
A116: 300 * (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * (f * k)) >= 240 * (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * (f * k)) by XREAL_1:64;
then A117: ((240 * f) * k) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) < M by XXREAL_0:2, A115;
(f * k) * k <= (f * k) * (k + 1) by NAT_1:11, XREAL_1:64;
then ((f * k) * k) * 96 <= ((f * k) * (k + 1)) * 100 by XREAL_1:66;
then A118: ( (96 * f) * (k * k) <= ((100 * f) * k) * (k + 1) & k ^2 = k * k ) by SQUARE_1:def 1;
then 12 * ((8 * f) * (k ^2)) <= 1 * (((100 * f) * k) * (k + 1)) ;
then A119: ((8 * f) * (k ^2)) / (((100 * f) * k) * (k + 1)) <= 1 / 12 by XREAL_1:102, A1;
1 <= f by A1, NAT_1:14;
then 24 * 1 <= 96 * f by XREAL_1:66;
then (24 * 1) * (k ^2) <= (96 * f) * (k ^2) by XREAL_1:64;
then A120: (24 * 1) * (k ^2) <= ((100 * f) * k) * (k + 1) by A118, XXREAL_0:2;
A121: 1 * (k ^2) <= 24 * (k ^2) by XREAL_1:64;
2 * (k ^2) <= 24 * (k ^2) by XREAL_1:64;
then 2 * (k ^2) <= (((100 * f) * k) * (k + 1)) * 1 by A120, XXREAL_0:2;
then A122: (k ^2) / (((100 * f) * k) * (k + 1)) <= 1 / 2 by XREAL_1:102, A1;
(k * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k)) * 1 <= (k * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k)) * f by A1, NAT_1:14, XREAL_1:64;
then ((k * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k)) * 1) * 120 <= ((k * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k)) * f) * 240 by XREAL_1:66;
then 12 * ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) <= 1 * M by A117, XXREAL_0:2;
then A123: ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M <= 1 / 12 by XREAL_1:102;
A124: 1 * ((((((100 * f) * k) * (k + 1)) |^ k) |^ 3) * ((((100 * f) * k) * (k + 1)) |^ 3)) <= 100 * ((((((100 * f) * k) * (k + 1)) |^ k) |^ 3) * ((((100 * f) * k) * (k + 1)) |^ 3)) by XREAL_1:64;
((((100 * f) * k) * (k + 1)) * (((100 * f) * k) * (k + 1))) * 1 <= (((100 * f) * k) * (k + 1)) |^ 3 by A54, A1, NAT_1:14, XREAL_1:64;
then ( ((((100 * f) * k) * (k + 1)) * (((100 * f) * k) * (k + 1))) * ((((100 * f) * k) * (k + 1)) |^ k) <= ((((100 * f) * k) * (k + 1)) |^ 3) * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3) & ((((100 * f) * k) * (k + 1)) |^ 3) * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3) < ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 ) by A58, XREAL_1:66, NAT_1:13, A124;
then (((100 * f) * k) * (k + 1)) * ((((100 * f) * k) * (k + 1)) * ((((100 * f) * k) * (k + 1)) |^ k)) <= ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 by XXREAL_0:2;
then A125: (((100 * f) * k) * (k + 1)) * ((((100 * f) * k) * (k + 1)) |^ (k + 1)) <= ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 by NEWTON:6;
1 <= k * (k + 1) by A1, NAT_1:14;
then 96 * 1 <= (k * (k + 1)) * 100 by XREAL_1:66;
then (96 * 1) * f <= ((k * (k + 1)) * 100) * f by XREAL_1:64;
then (96 * f) * ((((100 * f) * k) * (k + 1)) |^ (k + 1)) <= (((100 * f) * k) * (k + 1)) * ((((100 * f) * k) * (k + 1)) |^ (k + 1)) by XREAL_1:64;
then 12 * ((8 * f) * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) <= 1 * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) by A125, XXREAL_0:2;
then A126: ((8 * f) * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) <= 1 / 12 by XREAL_1:102;
1 <= (f * k) * (k + 1) by A1, NAT_1:14;
then 1 * 24 <= 100 * ((f * k) * (k + 1)) by XREAL_1:66;
then 24 * ((((100 * f) * k) * (k + 1)) |^ (k + 1)) <= (((100 * f) * k) * (k + 1)) * ((((100 * f) * k) * (k + 1)) |^ (k + 1)) by XREAL_1:64;
then 12 * (2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) <= (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) * 1 by A125, XXREAL_0:2;
then (2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) <= 1 / 12 by XREAL_1:102;
then 2 * (((((100 * f) * k) * (k + 1)) |^ (k + 1)) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) <= 1 / 12 by XCMPLX_1:74;
then A127: 2 * (((((100 * f) * k) * (k + 1)) |^ (k + 1)) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) <= 1 / 12 by XCMPLX_1:99;
A128: ( ((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) + (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M) <= (1 / 12) + (1 / 12) & (1 / 12) + (1 / 12) = 1 / 6 & 1 / 6 <= 1 / 2 ) by A127, A123, XREAL_1:7;
then A129: ((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) + (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M) <= 1 / 2 by XXREAL_0:2;
A130: ( 2 * (((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) + (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M)) <= 2 * (1 / 6) & 2 * (1 / 6) <= 1 ) by A128, XREAL_1:64;
A131: 2 * (((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) + (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M)) <= 1 by A130, XXREAL_0:2;
A132: ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) = ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) + (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) by XCMPLX_1:62
.= 1 + (I * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) by XCMPLX_1:60 ;
1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) <= 1 / (2 * (((100 * f) * k) * (k + 1))) by A66, XREAL_1:118, A1;
then consider T8 being _Theta such that
A133: (1 + (I * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) |^ (((100 * f) * k) * (k + 1)) = 1 + (((T8 * 2) * (((100 * f) * k) * (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) by Th9;
A134: (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1) |^ (((100 * f) * k) * (k + 1))) / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk) = ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1) |^ (((100 * f) * k) * (k + 1))) / (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k))) by XCMPLX_1:92
.= ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1) |^ (((100 * f) * k) * (k + 1))) / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + k))) by NEWTON:8
.= ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * (1 + (((T8 * 2) * (((100 * f) * k) * (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) by A133, A132, PREPOWER:8 ;
A135: |.2.| = 2 ;
A136: (2 * (((100 * f) * k) * (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) <= 1 by XREAL_1:183, A66;
then A137: - ((2 * (((100 * f) * k) * (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) >= - 1 by XREAL_1:24;
( - 1 <= T8 & T8 <= 1 ) by Def1;
then ( (- 1) * ((2 * (((100 * f) * k) * (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) <= T8 * ((2 * (((100 * f) * k) * (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) & T8 * ((2 * (((100 * f) * k) * (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) <= 1 * ((2 * (((100 * f) * k) * (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) ) by XREAL_1:64;
then ( - 1 <= T8 * ((2 * (((100 * f) * k) * (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) & T8 * ((2 * (((100 * f) * k) * (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) <= 1 ) by A136, A137, XXREAL_0:2;
then A138: ( (- 1) + 1 <= (T8 * ((2 * (((100 * f) * k) * (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) + 1 & (T8 * ((2 * (((100 * f) * k) * (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) + 1 <= 1 + 1 ) by XREAL_1:6;
A139: (2 * (((100 * f) * k) * (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) = (2 * (((100 * f) * k) * (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) by XCMPLX_1:99;
then |.(1 + (((T8 * 2) * (((100 * f) * k) * (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))).| = 1 + (((T8 * 2) * (((100 * f) * k) * (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) by A138, ABSVALUE:def 1;
then consider T9 being _Theta such that
A140: T7 * (1 + (((T8 * 2) * (((100 * f) * k) * (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) = T9 * 2 by Th2, A135, A138, A139;
A141: (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * (1 + (((T8 * 2) * (((100 * f) * k) * (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))))) * (T7 * ((5 * k) / M)) = (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * ((1 + (((T8 * 2) * (((100 * f) * k) * (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) * T7)) * ((5 * k) / M)
.= (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * (2 * T9)) * ((5 * k) / M) by A140
.= T9 * ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 2) * ((5 * k) / M))
.= T9 * (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 2) * (5 * k)) / M) by XCMPLX_1:74 ;
A142: (1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) = (1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) by NEWTON:6
.= 1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk) by XCMPLX_1:92 ;
A143: (Sum ((1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * IWW)) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) = (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) * ((1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * (Sum IWW)) by RVSUM_1:87;
IWW <> {} by A16;
then consider iww being FinSequence of REAL , x being Element of REAL such that
A144: IWW = <*x*> ^ iww by FINSEQ_2:130;
1 <= Wk + 1 by NAT_1:11;
then ((((100 * f) * k) * (k + 1)) choose (k + 0)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' (k + 0))) = IWW . (0 + 1) by A44, A15, A2, A14, FINSEQ_3:25
.= x by A144 ;
then A145: x = ((((100 * f) * k) * (k + 1)) choose k) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk) by A3, XXREAL_0:2, XREAL_1:233;
Wk > 0 by A105, XREAL_1:50;
then reconsider Wk1 = Wk - 1 as Nat ;
A146: len <*x*> = 1 by FINSEQ_1:40;
then Wk + 1 = 1 + (len iww) by A144, A15, A2, A14, FINSEQ_1:22;
then A147: len iww = ((((100 * f) * k) * (k + 1)) - (k + 1)) + 1 ;
for i being Nat st i + 1 in dom iww holds
iww . (i + 1) = ((((100 * f) * k) * (k + 1)) choose ((k + 1) + i)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' ((k + 1) + i)))

proof

let i be Nat; :: thesis: ( i + 1 in dom iww implies iww . (i + 1) = ((((100 * f) * k) * (k + 1)) choose ((k + 1) + i)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' ((k + 1) + i))) )
assume A148: i + 1 in dom iww ; :: thesis: iww . (i + 1) = ((((100 * f) * k) * (k + 1)) choose ((k + 1) + i)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' ((k + 1) + i)))
iww . (i + 1) = IWW . (1 + (i + 1)) by A144, A146, A148, FINSEQ_1:def 7
.= ((((100 * f) * k) * (k + 1)) choose (k + (i + 1))) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' (k + (i + 1)))) by A44, FINSEQ_1:28, A148, A144, A146 ;
hence iww . (i + 1) = ((((100 * f) * k) * (k + 1)) choose ((k + 1) + i)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' ((k + 1) + i))) ; :: thesis: verum

end;

then A149: ( 0 < Sum iww & Sum iww < (2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' (k + 1))) ) by Th14, A104, A75, A147;
A150: (1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk)) * x = ((1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk)) * ((((100 * f) * k) * (k + 1)) choose k) by A145
.= 1 * ((((100 * f) * k) * (k + 1)) choose k) by XCMPLX_1:87 ;
Sum IWW = x + (Sum iww) by A144, RVSUM_1:76;
then A151: (Sum ((1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * IWW)) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) = ((((100 * f) * k) * (k + 1)) choose k) + ((1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk)) * (Sum iww)) by A143, A142, A150;
A152: ( (((100 * f) * k) * (k + 1)) -' (k + 1) = (((100 * f) * k) * (k + 1)) - (k + 1) & (((100 * f) * k) * (k + 1)) - (k + 1) = Wk1 ) by A6, A4, XXREAL_0:2, XREAL_1:233;
Wk = Wk1 + 1 ;
then A153: (1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk)) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' (k + 1))) = (1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk1))) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk1) by A152, NEWTON:6
.= 1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) by XCMPLX_1:92 ;
(1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk)) * (Sum iww) < (1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk)) * ((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ ((((100 * f) * k) * (k + 1)) -' (k + 1)))) by A149, XREAL_1:68;
then consider T10 being _Theta such that
A154: I * ((1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk)) * (Sum iww)) = T10 * ((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) by A153, A149, Th5;
A155: ( (Wk + k) choose k >= Wk + 1 & Wk + 1 > Wk ) by NAT_1:13, NAT_1:14, A1, RAMSEY_1:11;
then (((100 * f) * k) * (k + 1)) choose k >= 1 by NAT_1:14;
then reconsider T12 = 1 / ((((100 * f) * k) * (k + 1)) choose k) as _Theta by Def1, XREAL_1:183;
A156: ((((100 * f) * k) * (k + 1)) choose k) * T12 = 1 by XCMPLX_1:87, A155;
consider T11 being _Theta such that
A157: (T10 * ((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) + (T9 * (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M)) = T11 * (((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) + (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M)) by Th6;
(Z + (Sum ((1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * IWW))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) = ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1) |^ (((100 * f) * k) * (k + 1))) / (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) by A103, NEWTON:6
.= (((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1) |^ (((100 * f) * k) * (k + 1))) / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk) by XCMPLX_1:92 ;
then A158: (r / ((Py (M,(k + 1))) * (Py (MU,(Wk + 1))))) - (Z * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) = ((Sum ((1 / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ (Wk + 1))) * IWW)) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) + (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1) |^ (((100 * f) * k) * (k + 1))) / ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ Wk)) * (T7 * ((5 * k) / M))) by A101
.= (((((100 * f) * k) * (k + 1)) choose k) + (T10 * ((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))))) + (T9 * (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M)) by A151, A154, A141, A134
.= ((((100 * f) * k) * (k + 1)) choose k) + (T11 * (((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) + (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M))) by A157
.= ((((100 * f) * k) * (k + 1)) choose k) + (((((((100 * f) * k) * (k + 1)) choose k) * T12) * T11) * (((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) + (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M))) by A156
.= ((((100 * f) * k) * (k + 1)) choose k) * (1 + ((T12 * T11) * (((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) + (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M)))) ;
consider T131 being _Theta such that
A159: (((100 * f) * k) * (k + 1)) choose k = (((((100 * f) * k) * (k + 1)) |^ k) / (k !)) * (1 + (T131 * ((k ^2) / (((100 * f) * k) * (k + 1))))) by A121, A120, XXREAL_0:2, Th8;
consider T13 being _Theta such that
A160: 1 / (1 + (T131 * ((k ^2) / (((100 * f) * k) * (k + 1))))) = 1 + ((T13 * 2) * ((k ^2) / (((100 * f) * k) * (k + 1)))) by Th7, A122;
A161: 1 / ((((((100 * f) * k) * (k + 1)) |^ k) / (k !)) * (1 + (T131 * ((k ^2) / (((100 * f) * k) * (k + 1)))))) = (1 / (((((100 * f) * k) * (k + 1)) |^ k) / (k !))) * (1 / (1 + (T131 * ((k ^2) / (((100 * f) * k) * (k + 1)))))) by XCMPLX_1:102
.= ((k !) / ((((100 * f) * k) * (k + 1)) |^ k)) * (1 / (1 + (T131 * ((k ^2) / (((100 * f) * k) * (k + 1)))))) by XCMPLX_1:57 ;
consider T14 being _Theta such that
A162: 1 / (1 + ((T12 * T11) * (((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) + (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M)))) = 1 + ((T14 * 2) * (((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) + (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M))) by Th7, A129;
A163: ((k !) / ((((100 * f) * k) * (k + 1)) |^ k)) * ((((100 * f) * k) * (k + 1)) |^ k) = k ! by XCMPLX_1:87, A1;
consider T15 being _Theta such that
A164: (1 + (T14 * (2 * (((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) + (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M))))) * (1 + (T13 * (2 * ((k ^2) / (((100 * f) * k) * (k + 1)))))) = 1 + (T15 * ((2 * (((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) + (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M))) + (2 * (2 * ((k ^2) / (((100 * f) * k) * (k + 1))))))) by A131, Th3;
A165: 1 * (((((100 * f) * k) * (k + 1)) |^ k) / ((r / ((Py (M,(k + 1))) * (Py (MU,(Wk + 1))))) - (Z * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) = ((1 / ((r / ((Py (M,(k + 1))) * (Py (MU,(Wk + 1))))) - (Z * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) * 1) * ((((100 * f) * k) * (k + 1)) |^ k) by XCMPLX_1:101
.= ((1 / ((((100 * f) * k) * (k + 1)) choose k)) * (1 + ((T14 * 2) * (((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) + (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M))))) * ((((100 * f) * k) * (k + 1)) |^ k) by A162, A158, XCMPLX_1:102
.= (k !) * ((1 + (T13 * (2 * ((k ^2) / (((100 * f) * k) * (k + 1)))))) * (1 + (T14 * (2 * (((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) + (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M)))))) by A160, A163, A159, A161
.= (k !) * (1 + (T15 * ((2 * (((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) + (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M))) + (2 * (2 * ((k ^2) / (((100 * f) * k) * (k + 1)))))))) by A164 ;
- f <= 0 ;
then ((k !) - (f * 2)) + (2 * f) <= 0 + (2 * f) by A1, XREAL_1:6;
then reconsider T16 = (k !) / (2 * f) as _Theta by Def1, XREAL_1:183;
A166: (2 * f) * ((2 * (((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) + (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M))) + (2 * (2 * ((k ^2) / (((100 * f) * k) * (k + 1)))))) = ((((8 * f) * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) + ((2 * f) * (2 * (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M)))) + ((2 * f) * (2 * (2 * ((k ^2) / (((100 * f) * k) * (k + 1))))))
.= ((((8 * f) * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) + ((4 * f) * (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M))) + ((8 * f) * ((k ^2) / (((100 * f) * k) * (k + 1)))) by XCMPLX_1:99
.= ((((8 * f) * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) + (((4 * f) * ((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k)) / M)) + ((8 * f) * ((k ^2) / (((100 * f) * k) * (k + 1)))) by XCMPLX_1:74
.= ((((8 * f) * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) + ((((40 * f) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k)) * k) / M)) + (((8 * f) * (k ^2)) / (((100 * f) * k) * (k + 1))) by XCMPLX_1:74 ;
k ! = T16 * (2 * f) by XCMPLX_1:87, A1;
then A167: ((((100 * f) * k) * (k + 1)) |^ k) / ((r / ((Py (M,(k + 1))) * (Py (MU,(Wk + 1))))) - (Z * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) = (k !) + ((T15 * T16) * ((2 * f) * ((2 * (((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) + (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M))) + (2 * (2 * ((k ^2) / (((100 * f) * k) * (k + 1)))))))) by A165
.= (k !) + ((T15 * T16) * (((((8 * f) * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) + ((((40 * f) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k)) * k) / M)) + (((8 * f) * (k ^2)) / (((100 * f) * k) * (k + 1))))) by A166 ;
6 * (((40 * f) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k)) * k) < 1 * M by A116, XXREAL_0:2, A115;
then A168: (((40 * f) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k)) * k) / M < 1 / 6 by XREAL_1:106;
(((8 * f) * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) + (((8 * f) * (k ^2)) / (((100 * f) * k) * (k + 1))) <= (1 / 12) + (1 / 12) by A119, A126, XREAL_1:7;
then A169: ((((8 * f) * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) + (((8 * f) * (k ^2)) / (((100 * f) * k) * (k + 1)))) + ((((40 * f) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k)) * k) / M) < ((1 / 12) + (1 / 12)) + (1 / 6) by A168, XREAL_1:8;
( - 1 <= T15 * T16 & T15 * T16 <= 1 ) by Def1;
then ( (1 / 3) * (- 1) < (- 1) * (((((8 * f) * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) + ((((40 * f) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k)) * k) / M)) + (((8 * f) * (k ^2)) / (((100 * f) * k) * (k + 1)))) & (- 1) * (((((8 * f) * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) + ((((40 * f) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k)) * k) / M)) + (((8 * f) * (k ^2)) / (((100 * f) * k) * (k + 1)))) <= (T15 * T16) * (((((8 * f) * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) + ((((40 * f) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k)) * k) / M)) + (((8 * f) * (k ^2)) / (((100 * f) * k) * (k + 1)))) & (T15 * T16) * (((((8 * f) * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) + ((((40 * f) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k)) * k) / M)) + (((8 * f) * (k ^2)) / (((100 * f) * k) * (k + 1)))) <= 1 * (((((8 * f) * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) + ((((40 * f) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k)) * k) / M)) + (((8 * f) * (k ^2)) / (((100 * f) * k) * (k + 1)))) & 1 * (((((8 * f) * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) + ((((40 * f) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k)) * k) / M)) + (((8 * f) * (k ^2)) / (((100 * f) * k) * (k + 1)))) < 1 / 3 ) by A169, XREAL_1:64, XREAL_1:69;
then ( (1 / 3) * (- 1) < (T15 * T16) * (((((8 * f) * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) + ((((40 * f) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k)) * k) / M)) + (((8 * f) * (k ^2)) / (((100 * f) * k) * (k + 1)))) & (T15 * T16) * (((((8 * f) * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) + ((((40 * f) * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k)) * k) / M)) + (((8 * f) * (k ^2)) / (((100 * f) * k) * (k + 1)))) < 1 / 3 ) by XXREAL_0:2;
then ( - (1 / 2) < (((((100 * f) * k) * (k + 1)) |^ k) / ((r / ((Py (M,(k + 1))) * (Py (MU,(Wk + 1))))) - (Z * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) - f & (((((100 * f) * k) * (k + 1)) |^ k) / ((r / ((Py (M,(k + 1))) * (Py (MU,(Wk + 1))))) - (Z * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) - f < 1 / 2 ) by A1, A167, XXREAL_0:2;
then ( ((((((100 * f) * k) * (k + 1)) |^ k) / ((r / ((Py (M,(k + 1))) * (Py (MU,(Wk + 1))))) - (Z * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) - f) ^2 < (1 / 2) ^2 & (1 / 2) ^2 = (1 / 2) * (1 / 2) ) by SQUARE_1:def 1, SQUARE_1:50;
then A170: ((((((100 * f) * k) * (k + 1)) |^ k) / ((r / ((Py (M,(k + 1))) * (Py (MU,(Wk + 1))))) - (Z * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) - f) * ((((((100 * f) * k) * (k + 1)) |^ k) / ((r / ((Py (M,(k + 1))) * (Py (MU,(Wk + 1))))) - (Z * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) - f) < 1 / 4 by SQUARE_1:def 1;
set R = r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1));
A171: r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) <> 0

proof

assume r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) = 0 ; :: thesis: contradiction
then A172: r / ((Py (M,(k + 1))) * (Py (MU,(Wk + 1)))) = ((Z * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * ((Py (M,(k + 1))) * (Py (MU,(Wk + 1))))) / ((Py (M,(k + 1))) * (Py (MU,(Wk + 1))))
.= (Z * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((Py (M,(k + 1))) * (Py (MU,(Wk + 1)))) / ((Py (M,(k + 1))) * (Py (MU,(Wk + 1))))) by XCMPLX_1:74
.= (Z * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * 1 by XCMPLX_1:60 ;
A173: - (((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) + (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M)) >= - (1 / 2) by A129, XREAL_1:24;
- 1 <= T12 * T11 by Def1;
then (- 1) * (((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) + (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M)) <= (T12 * T11) * (((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) + (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M)) by XREAL_1:64;
then - (1 / 2) <= (T12 * T11) * (((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) + (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M)) by A173, XXREAL_0:2;
then (- (1 / 2)) + 1 <= ((T12 * T11) * (((2 * ((((100 * f) * k) * (k + 1)) |^ (k + 1))) * (1 / (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) + (((((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) |^ k) * 10) * k) / M))) + 1 by XREAL_1:6;
hence contradiction by A158, XCMPLX_1:87, A155, A172; :: thesis: verum

end;

A174: ( ((((100 * f) * k) * (k + 1)) |^ k) ^2 = ((((100 * f) * k) * (k + 1)) |^ k) * ((((100 * f) * k) * (k + 1)) |^ k) & (Py (M,(k + 1))) ^2 = (Py (M,(k + 1))) * (Py (M,(k + 1))) & (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) ^2 = (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) & (Py (MU,(Wk + 1))) ^2 = (Py (MU,(Wk + 1))) * (Py (MU,(Wk + 1))) & f ^2 = f * f ) by SQUARE_1:def 1;
A175: (((((((100 * f) * k) * (k + 1)) |^ k) * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) - (f * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))))) / (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) = (((((((100 * f) * k) * (k + 1)) |^ k) * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) / (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) - ((f * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) / (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) by XCMPLX_1:120
.= ((((((100 * f) * k) * (k + 1)) |^ k) * ((Py (M,(k + 1))) * (Py (MU,(Wk + 1))))) / (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) - f by A171, XCMPLX_1:89
.= (((((100 * f) * k) * (k + 1)) |^ k) / ((r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) / ((Py (M,(k + 1))) * (Py (MU,(Wk + 1)))))) - f by XCMPLX_1:77
.= (((((100 * f) * k) * (k + 1)) |^ k) / ((r / ((Py (M,(k + 1))) * (Py (MU,(Wk + 1))))) - (((Z * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * ((Py (M,(k + 1))) * (Py (MU,(Wk + 1))))) / ((Py (M,(k + 1))) * (Py (MU,(Wk + 1))))))) - f by XCMPLX_1:120
.= (((((100 * f) * k) * (k + 1)) |^ k) / ((r / ((Py (M,(k + 1))) * (Py (MU,(Wk + 1))))) - (Z * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) - f by XCMPLX_1:89 ;
(((((((((100 * f) * k) * (k + 1)) |^ k) * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) - (f * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))))) / (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) * ((((((((100 * f) * k) * (k + 1)) |^ k) * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) - (f * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))))) / (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))))) * 4 < (1 / 4) * 4 by XREAL_1:68, A170, A175;
then ((((((((((100 * f) * k) * (k + 1)) |^ k) * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) - (f * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))))) / (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) * ((((((((100 * f) * k) * (k + 1)) |^ k) * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) - (f * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))))) / (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))))) * 4) * ((r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) < 1 * ((r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) by A171, XREAL_1:68;
then ((((((((((100 * f) * k) * (k + 1)) |^ k) * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) - (f * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))))) / (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) * (((((((((100 * f) * k) * (k + 1)) |^ k) * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) - (f * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))))) / (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))))) * 4 < 1 * ((r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) ;
then ((((((((((100 * f) * k) * (k + 1)) |^ k) * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) - (f * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))))) / (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))) * (((((((100 * f) * k) * (k + 1)) |^ k) * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) - (f * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))))) * 4 < (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) by A171, XCMPLX_1:87;
then ((((((((100 * f) * k) * (k + 1)) |^ k) * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) - (f * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))))) * (((((((100 * f) * k) * (k + 1)) |^ k) * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) - (f * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))))) * 4 < (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) by A171, XCMPLX_1:87;
then ((((((((((100 * f) * k) * (k + 1)) |^ k) ^2) * ((Py (M,(k + 1))) ^2)) * ((Py (MU,(Wk + 1))) ^2)) * 4) - ((8 * ((((((100 * f) * k) * (k + 1)) |^ k) * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1))))) * (f * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))))) + ((4 * (f ^2)) * ((r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) ^2))) + ((8 * ((((((100 * f) * k) * (k + 1)) |^ k) * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1))))) * (f * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))))) < ((r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) ^2) + ((8 * ((((((100 * f) * k) * (k + 1)) |^ k) * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1))))) * (f * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))))) by A174, XREAL_1:6;
then A176: (((((((((((100 * f) * k) * (k + 1)) |^ k) ^2) * ((Py (M,(k + 1))) ^2)) * ((Py (MU,(Wk + 1))) ^2)) * 4) - ((8 * ((((((100 * f) * k) * (k + 1)) |^ k) * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1))))) * (f * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))))) + ((4 * (f ^2)) * ((r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) ^2))) + ((8 * ((((((100 * f) * k) * (k + 1)) |^ k) * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1))))) * (f * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))))) - ((r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) ^2) < (((r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) ^2) + ((8 * ((((((100 * f) * k) * (k + 1)) |^ k) * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1))))) * (f * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)))))) - ((r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) ^2) by XREAL_1:14;
take Z ; :: thesis: ex r, s, t, u, W, U, S, T, Q being Nat ex M being non trivial Nat st
( Z > 0 & u > 0 & (r + W) + 1 = Py ((M * (U + 1)),(W + 1)) & (((M ^2) - 1) * (S ^2)) + 1 is square & ((((M * U) ^2) - 1) * (T ^2)) + 1 is square & (((W ^2) * (u ^2)) - ((((W ^2) - 1) * S) * u)) - 1, 0 are_congruent_mod Q & (((4 * (f ^2)) - 1) * ((r - (((Z * S) * T) * U)) ^2)) + (((4 * (u ^2)) * (S ^2)) * (T ^2)) < ((((8 * f) * u) * S) * T) * (r - (((Z * S) * T) * U)) & W = ((100 * f) * k) * (k + 1) & U = ((100 * (u |^ 3)) * (W |^ 3)) + 1 & M = (((100 * Z) * U) * W) + 1 & S = (((M - 1) * s) + k) + 1 & T = (((((M * U) - 1) * t) + W) - k) + 1 & Q = (((2 * M) * W) - (W ^2)) - 1 )
take r ; :: thesis: ex s, t, u, W, U, S, T, Q being Nat ex M being non trivial Nat st
( Z > 0 & u > 0 & (r + W) + 1 = Py ((M * (U + 1)),(W + 1)) & (((M ^2) - 1) * (S ^2)) + 1 is square & ((((M * U) ^2) - 1) * (T ^2)) + 1 is square & (((W ^2) * (u ^2)) - ((((W ^2) - 1) * S) * u)) - 1, 0 are_congruent_mod Q & (((4 * (f ^2)) - 1) * ((r - (((Z * S) * T) * U)) ^2)) + (((4 * (u ^2)) * (S ^2)) * (T ^2)) < ((((8 * f) * u) * S) * T) * (r - (((Z * S) * T) * U)) & W = ((100 * f) * k) * (k + 1) & U = ((100 * (u |^ 3)) * (W |^ 3)) + 1 & M = (((100 * Z) * U) * W) + 1 & S = (((M - 1) * s) + k) + 1 & T = (((((M * U) - 1) * t) + W) - k) + 1 & Q = (((2 * M) * W) - (W ^2)) - 1 )
take s ; :: thesis: ex t, u, W, U, S, T, Q being Nat ex M being non trivial Nat st
( Z > 0 & u > 0 & (r + W) + 1 = Py ((M * (U + 1)),(W + 1)) & (((M ^2) - 1) * (S ^2)) + 1 is square & ((((M * U) ^2) - 1) * (T ^2)) + 1 is square & (((W ^2) * (u ^2)) - ((((W ^2) - 1) * S) * u)) - 1, 0 are_congruent_mod Q & (((4 * (f ^2)) - 1) * ((r - (((Z * S) * T) * U)) ^2)) + (((4 * (u ^2)) * (S ^2)) * (T ^2)) < ((((8 * f) * u) * S) * T) * (r - (((Z * S) * T) * U)) & W = ((100 * f) * k) * (k + 1) & U = ((100 * (u |^ 3)) * (W |^ 3)) + 1 & M = (((100 * Z) * U) * W) + 1 & S = (((M - 1) * s) + k) + 1 & T = (((((M * U) - 1) * t) + W) - k) + 1 & Q = (((2 * M) * W) - (W ^2)) - 1 )
take t ; :: thesis: ex u, W, U, S, T, Q being Nat ex M being non trivial Nat st
( Z > 0 & u > 0 & (r + W) + 1 = Py ((M * (U + 1)),(W + 1)) & (((M ^2) - 1) * (S ^2)) + 1 is square & ((((M * U) ^2) - 1) * (T ^2)) + 1 is square & (((W ^2) * (u ^2)) - ((((W ^2) - 1) * S) * u)) - 1, 0 are_congruent_mod Q & (((4 * (f ^2)) - 1) * ((r - (((Z * S) * T) * U)) ^2)) + (((4 * (u ^2)) * (S ^2)) * (T ^2)) < ((((8 * f) * u) * S) * T) * (r - (((Z * S) * T) * U)) & W = ((100 * f) * k) * (k + 1) & U = ((100 * (u |^ 3)) * (W |^ 3)) + 1 & M = (((100 * Z) * U) * W) + 1 & S = (((M - 1) * s) + k) + 1 & T = (((((M * U) - 1) * t) + W) - k) + 1 & Q = (((2 * M) * W) - (W ^2)) - 1 )
take (((100 * f) * k) * (k + 1)) |^ k ; :: thesis: ex W, U, S, T, Q being Nat ex M being non trivial Nat st
( Z > 0 & (((100 * f) * k) * (k + 1)) |^ k > 0 & (r + W) + 1 = Py ((M * (U + 1)),(W + 1)) & (((M ^2) - 1) * (S ^2)) + 1 is square & ((((M * U) ^2) - 1) * (T ^2)) + 1 is square & (((W ^2) * (((((100 * f) * k) * (k + 1)) |^ k) ^2)) - ((((W ^2) - 1) * S) * ((((100 * f) * k) * (k + 1)) |^ k))) - 1, 0 are_congruent_mod Q & (((4 * (f ^2)) - 1) * ((r - (((Z * S) * T) * U)) ^2)) + (((4 * (((((100 * f) * k) * (k + 1)) |^ k) ^2)) * (S ^2)) * (T ^2)) < ((((8 * f) * ((((100 * f) * k) * (k + 1)) |^ k)) * S) * T) * (r - (((Z * S) * T) * U)) & W = ((100 * f) * k) * (k + 1) & U = ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * (W |^ 3)) + 1 & M = (((100 * Z) * U) * W) + 1 & S = (((M - 1) * s) + k) + 1 & T = (((((M * U) - 1) * t) + W) - k) + 1 & Q = (((2 * M) * W) - (W ^2)) - 1 )
take ((100 * f) * k) * (k + 1) ; :: thesis: ex U, S, T, Q being Nat ex M being non trivial Nat st
( Z > 0 & (((100 * f) * k) * (k + 1)) |^ k > 0 & (r + (((100 * f) * k) * (k + 1))) + 1 = Py ((M * (U + 1)),((((100 * f) * k) * (k + 1)) + 1)) & (((M ^2) - 1) * (S ^2)) + 1 is square & ((((M * U) ^2) - 1) * (T ^2)) + 1 is square & ((((((100 * f) * k) * (k + 1)) ^2) * (((((100 * f) * k) * (k + 1)) |^ k) ^2)) - (((((((100 * f) * k) * (k + 1)) ^2) - 1) * S) * ((((100 * f) * k) * (k + 1)) |^ k))) - 1, 0 are_congruent_mod Q & (((4 * (f ^2)) - 1) * ((r - (((Z * S) * T) * U)) ^2)) + (((4 * (((((100 * f) * k) * (k + 1)) |^ k) ^2)) * (S ^2)) * (T ^2)) < ((((8 * f) * ((((100 * f) * k) * (k + 1)) |^ k)) * S) * T) * (r - (((Z * S) * T) * U)) & ((100 * f) * k) * (k + 1) = ((100 * f) * k) * (k + 1) & U = ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 & M = (((100 * Z) * U) * (((100 * f) * k) * (k + 1))) + 1 & S = (((M - 1) * s) + k) + 1 & T = (((((M * U) - 1) * t) + (((100 * f) * k) * (k + 1))) - k) + 1 & Q = (((2 * M) * (((100 * f) * k) * (k + 1))) - ((((100 * f) * k) * (k + 1)) ^2)) - 1 )
take ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 ; :: thesis: ex S, T, Q being Nat ex M being non trivial Nat st
( Z > 0 & (((100 * f) * k) * (k + 1)) |^ k > 0 & (r + (((100 * f) * k) * (k + 1))) + 1 = Py ((M * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1)),((((100 * f) * k) * (k + 1)) + 1)) & (((M ^2) - 1) * (S ^2)) + 1 is square & ((((M * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) ^2) - 1) * (T ^2)) + 1 is square & ((((((100 * f) * k) * (k + 1)) ^2) * (((((100 * f) * k) * (k + 1)) |^ k) ^2)) - (((((((100 * f) * k) * (k + 1)) ^2) - 1) * S) * ((((100 * f) * k) * (k + 1)) |^ k))) - 1, 0 are_congruent_mod Q & (((4 * (f ^2)) - 1) * ((r - (((Z * S) * T) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) ^2)) + (((4 * (((((100 * f) * k) * (k + 1)) |^ k) ^2)) * (S ^2)) * (T ^2)) < ((((8 * f) * ((((100 * f) * k) * (k + 1)) |^ k)) * S) * T) * (r - (((Z * S) * T) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) & ((100 * f) * k) * (k + 1) = ((100 * f) * k) * (k + 1) & ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 = ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 & M = (((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1 & S = (((M - 1) * s) + k) + 1 & T = (((((M * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) - 1) * t) + (((100 * f) * k) * (k + 1))) - k) + 1 & Q = (((2 * M) * (((100 * f) * k) * (k + 1))) - ((((100 * f) * k) * (k + 1)) ^2)) - 1 )
take Py (M,(k + 1)) ; :: thesis: ex T, Q being Nat ex M being non trivial Nat st
( Z > 0 & (((100 * f) * k) * (k + 1)) |^ k > 0 & (r + (((100 * f) * k) * (k + 1))) + 1 = Py ((M * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1)),((((100 * f) * k) * (k + 1)) + 1)) & (((M ^2) - 1) * ((Py (M,(k + 1))) ^2)) + 1 is square & ((((M * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) ^2) - 1) * (T ^2)) + 1 is square & ((((((100 * f) * k) * (k + 1)) ^2) * (((((100 * f) * k) * (k + 1)) |^ k) ^2)) - (((((((100 * f) * k) * (k + 1)) ^2) - 1) * (Py (M,(k + 1)))) * ((((100 * f) * k) * (k + 1)) |^ k))) - 1, 0 are_congruent_mod Q & (((4 * (f ^2)) - 1) * ((r - (((Z * (Py (M,(k + 1)))) * T) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) ^2)) + (((4 * (((((100 * f) * k) * (k + 1)) |^ k) ^2)) * ((Py (M,(k + 1))) ^2)) * (T ^2)) < ((((8 * f) * ((((100 * f) * k) * (k + 1)) |^ k)) * (Py (M,(k + 1)))) * T) * (r - (((Z * (Py (M,(k + 1)))) * T) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) & ((100 * f) * k) * (k + 1) = ((100 * f) * k) * (k + 1) & ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 = ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 & M = (((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1 & Py (M,(k + 1)) = (((M - 1) * s) + k) + 1 & T = (((((M * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) - 1) * t) + (((100 * f) * k) * (k + 1))) - k) + 1 & Q = (((2 * M) * (((100 * f) * k) * (k + 1))) - ((((100 * f) * k) * (k + 1)) ^2)) - 1 )
take Py (MU,(Wk + 1)) ; :: thesis: ex Q being Nat ex M being non trivial Nat st
( Z > 0 & (((100 * f) * k) * (k + 1)) |^ k > 0 & (r + (((100 * f) * k) * (k + 1))) + 1 = Py ((M * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1)),((((100 * f) * k) * (k + 1)) + 1)) & (((M ^2) - 1) * ((Py (M,(k + 1))) ^2)) + 1 is square & ((((M * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) ^2) - 1) * ((Py (MU,(Wk + 1))) ^2)) + 1 is square & ((((((100 * f) * k) * (k + 1)) ^2) * (((((100 * f) * k) * (k + 1)) |^ k) ^2)) - (((((((100 * f) * k) * (k + 1)) ^2) - 1) * (Py (M,(k + 1)))) * ((((100 * f) * k) * (k + 1)) |^ k))) - 1, 0 are_congruent_mod Q & (((4 * (f ^2)) - 1) * ((r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) ^2)) + (((4 * (((((100 * f) * k) * (k + 1)) |^ k) ^2)) * ((Py (M,(k + 1))) ^2)) * ((Py (MU,(Wk + 1))) ^2)) < ((((8 * f) * ((((100 * f) * k) * (k + 1)) |^ k)) * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) & ((100 * f) * k) * (k + 1) = ((100 * f) * k) * (k + 1) & ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 = ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 & M = (((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1 & Py (M,(k + 1)) = (((M - 1) * s) + k) + 1 & Py (MU,(Wk + 1)) = (((((M * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) - 1) * t) + (((100 * f) * k) * (k + 1))) - k) + 1 & Q = (((2 * M) * (((100 * f) * k) * (k + 1))) - ((((100 * f) * k) * (k + 1)) ^2)) - 1 )
take Q ; :: thesis: ex M being non trivial Nat st
( Z > 0 & (((100 * f) * k) * (k + 1)) |^ k > 0 & (r + (((100 * f) * k) * (k + 1))) + 1 = Py ((M * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1)),((((100 * f) * k) * (k + 1)) + 1)) & (((M ^2) - 1) * ((Py (M,(k + 1))) ^2)) + 1 is square & ((((M * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) ^2) - 1) * ((Py (MU,(Wk + 1))) ^2)) + 1 is square & ((((((100 * f) * k) * (k + 1)) ^2) * (((((100 * f) * k) * (k + 1)) |^ k) ^2)) - (((((((100 * f) * k) * (k + 1)) ^2) - 1) * (Py (M,(k + 1)))) * ((((100 * f) * k) * (k + 1)) |^ k))) - 1, 0 are_congruent_mod Q & (((4 * (f ^2)) - 1) * ((r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) ^2)) + (((4 * (((((100 * f) * k) * (k + 1)) |^ k) ^2)) * ((Py (M,(k + 1))) ^2)) * ((Py (MU,(Wk + 1))) ^2)) < ((((8 * f) * ((((100 * f) * k) * (k + 1)) |^ k)) * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) & ((100 * f) * k) * (k + 1) = ((100 * f) * k) * (k + 1) & ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 = ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 & M = (((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1 & Py (M,(k + 1)) = (((M - 1) * s) + k) + 1 & Py (MU,(Wk + 1)) = (((((M * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) - 1) * t) + (((100 * f) * k) * (k + 1))) - k) + 1 & Q = (((2 * M) * (((100 * f) * k) * (k + 1))) - ((((100 * f) * k) * (k + 1)) ^2)) - 1 )
take M ; :: thesis: ( Z > 0 & (((100 * f) * k) * (k + 1)) |^ k > 0 & (r + (((100 * f) * k) * (k + 1))) + 1 = Py ((M * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1)),((((100 * f) * k) * (k + 1)) + 1)) & (((M ^2) - 1) * ((Py (M,(k + 1))) ^2)) + 1 is square & ((((M * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) ^2) - 1) * ((Py (MU,(Wk + 1))) ^2)) + 1 is square & ((((((100 * f) * k) * (k + 1)) ^2) * (((((100 * f) * k) * (k + 1)) |^ k) ^2)) - (((((((100 * f) * k) * (k + 1)) ^2) - 1) * (Py (M,(k + 1)))) * ((((100 * f) * k) * (k + 1)) |^ k))) - 1, 0 are_congruent_mod Q & (((4 * (f ^2)) - 1) * ((r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) ^2)) + (((4 * (((((100 * f) * k) * (k + 1)) |^ k) ^2)) * ((Py (M,(k + 1))) ^2)) * ((Py (MU,(Wk + 1))) ^2)) < ((((8 * f) * ((((100 * f) * k) * (k + 1)) |^ k)) * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) & ((100 * f) * k) * (k + 1) = ((100 * f) * k) * (k + 1) & ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 = ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 & M = (((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1 & Py (M,(k + 1)) = (((M - 1) * s) + k) + 1 & Py (MU,(Wk + 1)) = (((((M * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) - 1) * t) + (((100 * f) * k) * (k + 1))) - k) + 1 & Q = (((2 * M) * (((100 * f) * k) * (k + 1))) - ((((100 * f) * k) * (k + 1)) ^2)) - 1 )
thus ( Z > 0 & (((100 * f) * k) * (k + 1)) |^ k > 0 & (r + (((100 * f) * k) * (k + 1))) + 1 = Py ((M * ((((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1) + 1)),((((100 * f) * k) * (k + 1)) + 1)) & (((M ^2) - 1) * ((Py (M,(k + 1))) ^2)) + 1 is square & ((((M * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) ^2) - 1) * ((Py (MU,(Wk + 1))) ^2)) + 1 is square & ((((((100 * f) * k) * (k + 1)) ^2) * (((((100 * f) * k) * (k + 1)) |^ k) ^2)) - (((((((100 * f) * k) * (k + 1)) ^2) - 1) * (Py (M,(k + 1)))) * ((((100 * f) * k) * (k + 1)) |^ k))) - 1, 0 are_congruent_mod Q & (((4 * (f ^2)) - 1) * ((r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) ^2)) + (((4 * (((((100 * f) * k) * (k + 1)) |^ k) ^2)) * ((Py (M,(k + 1))) ^2)) * ((Py (MU,(Wk + 1))) ^2)) < ((((8 * f) * ((((100 * f) * k) * (k + 1)) |^ k)) * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (r - (((Z * (Py (M,(k + 1)))) * (Py (MU,(Wk + 1)))) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1))) & ((100 * f) * k) * (k + 1) = ((100 * f) * k) * (k + 1) & ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 = ((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1 & M = (((100 * Z) * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) * (((100 * f) * k) * (k + 1))) + 1 & Py (M,(k + 1)) = (((M - 1) * s) + k) + 1 & Py (MU,(Wk + 1)) = (((((M * (((100 * (((((100 * f) * k) * (k + 1)) |^ k) |^ 3)) * ((((100 * f) * k) * (k + 1)) |^ 3)) + 1)) - 1) * t) + (((100 * f) * k) * (k + 1))) - k) + 1 & Q = (((2 * M) * (((100 * f) * k) * (k + 1))) - ((((100 * f) * k) * (k + 1)) ^2)) - 1 ) by A1, A176, Th12, A36, A38, A41, A43; :: thesis: verum