let f, k, m, r, s, t, u be Nat; for W, M, U, S, T, Q being Integer st f > 0 & k > 0 & m > 0 & u > 0 & (((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 holds
( M * (U + 1) is non trivial Nat & W is Nat & ( for mu being non trivial Nat
for w being Nat st mu = M * (U + 1) & w = W & (r + W) + 1 = Py (mu,(w + 1)) holds
f = k ! ) )
let W, M, U, S, T, Q be Integer; ( f > 0 & k > 0 & m > 0 & u > 0 & (((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 implies ( M * (U + 1) is non trivial Nat & W is Nat & ( for mu being non trivial Nat
for w being Nat st mu = M * (U + 1) & w = W & (r + W) + 1 = Py (mu,(w + 1)) holds
f = k ! ) ) )
assume that
A1:
( f > 0 & k > 0 & m > 0 & u > 0 )
and
A2:
(((M ^2) - 1) * (S ^2)) + 1 is square
and
A3:
((((M * U) ^2) - 1) * (T ^2)) + 1 is square
and
A4:
(((W ^2) * (u ^2)) - ((((W ^2) - 1) * S) * u)) - 1, 0 are_congruent_mod Q
and
A5:
(((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))
and
A6:
W = ((100 * f) * k) * (k + 1)
and
A7:
U = ((100 * (u |^ 3)) * (W |^ 3)) + 1
and
A8:
M = (((100 * m) * U) * W) + 1
and
A9:
S = (((M - 1) * s) + k) + 1
and
A10:
T = (((((M * U) - 1) * t) + W) - k) + 1
and
A11:
Q = (((2 * M) * W) - (W ^2)) - 1
; ( M * (U + 1) is non trivial Nat & W is Nat & ( for mu being non trivial Nat
for w being Nat st mu = M * (U + 1) & w = W & (r + W) + 1 = Py (mu,(w + 1)) holds
f = k ! ) )
set MM = M;
set UU = U;
set WW = W;
reconsider W = W, U = U, M = M, S = S as Element of NAT by A6, A7, A8, A9, INT_1:3;
A12:
((100 * f) * k) * (k + 1) >= 1 * (k + 1)
by A1, NAT_1:14, XREAL_1:64;
A13:
W > k
by A12, A6, NAT_1:13;
then A14:
W - k > 0
by XREAL_1:50;
then A15:
(((M * U) - 1) * t) + (W - k) >= 0 + 0
by A7, A8;
then reconsider T = T as Element of NAT by A10, INT_1:3;
reconsider Wk = W - k as Nat by A13, NAT_1:21;
A16:
(M * W) - 1 >= 0
by A1, A6, A7, A8;
((100 * m) * U) * W >= 1 * W
by XREAL_1:64, A1, A7, NAT_1:14;
then A17:
M > W
by A8, NAT_1:13;
then
( M * W >= W * W & W * W = W ^2 )
by XREAL_1:64, SQUARE_1:def 1;
then
(M * W) + (M * W) >= (M * W) + (W ^2)
by XREAL_1:7;
then
((M * W) + (M * W)) - ((W ^2) + 1) >= ((M * W) + (W ^2)) - ((W ^2) + 1)
by XREAL_1:9;
then reconsider Q = Q as Element of NAT by A16, A11, INT_1:3;
A18:
U > 1
by A7, NAT_1:13, A1, A6, NAT_1:14;
A19:
( M >= 1 & U + 1 > 1 )
by A6, A7, A8, NAT_1:14, NAT_1:13;
then
( M * (U + 1) > 1 * 1 & W = W )
by XREAL_1:97;
hence
( M * (U + 1) is non trivial Nat & W is Nat )
by NEWTON03:def 1; for mu being non trivial Nat
for w being Nat st mu = M * (U + 1) & w = W & (r + W) + 1 = Py (mu,(w + 1)) holds
f = k !
M * U > 1 * 1
by A19, A18, XREAL_1:97;
then reconsider MU = M * U as non trivial Nat by NEWTON03:def 1;
W >= 1
by A1, A6, NAT_1:14;
then
M > 1
by A17, XXREAL_0:2;
then reconsider M = M as non trivial Nat by NEWTON03:def 1;
reconsider M1 = M - 1 as Nat ;
let mu be non trivial Nat; for w being Nat st mu = M * (U + 1) & w = W & (r + W) + 1 = Py (mu,(w + 1)) holds
f = k !
let w be Nat; ( mu = M * (U + 1) & w = W & (r + W) + 1 = Py (mu,(w + 1)) implies f = k ! )
assume A20:
( mu = M * (U + 1) & w = W & (r + W) + 1 = Py (mu,(w + 1)) )
; f = k !
set R = r - (((m * S) * T) * U);
A21:
( u ^2 = u * u & S ^2 = S * S & (r - (((m * S) * T) * U)) ^2 = (r - (((m * S) * T) * U)) * (r - (((m * S) * T) * U)) & T ^2 = T * T & f ^2 = f * f )
by SQUARE_1:def 1;
0 < ((((8 * f) * u) * S) * T) * (r - (((m * S) * T) * U))
by A1, A21, A5;
then A22:
r - (((m * S) * T) * U) > 0
;
((m * T) * U) * S >= S * 1
by XREAL_1:64, A1, A7, A15, A10, NAT_1:14;
then
0 < r - S
by A22, XREAL_1:10;
then A23:
S < r
by XREAL_1:47;
((m * S) * U) * T >= T * 1
by XREAL_1:64, NAT_1:14, A1, A6, A7, A8, A9;
then
0 < r - T
by A22, XREAL_1:10;
then A24:
T < r
by XREAL_1:47;
A25:
((u / ((r / (S * T)) - (m * U))) - f) * ((u / ((r / (S * T)) - (m * U))) - f) < 1 / 4
A27:
( r < Py (M,M1) & r < Py (M,(MU - 1)) )
proof
A28:
r + 0 < r + (W + 1)
by XREAL_1:8;
A29:
Py (
mu,
(w + 1))
<= (2 * (M * (U + 1))) |^ W
by A20, HILB10_1:17;
U >= 1
+ 1
by NAT_1:13, A18;
then reconsider u2 =
U - 2 as
Nat by NAT_1:21;
A30:
(
(M |^ 2) * 1
<= (M |^ 2) * (M |^ u2) &
(M |^ 2) * (M |^ u2) = M |^ (2 + u2) )
by NAT_1:14, NEWTON:8, XREAL_1:64;
A31:
(
M |^ (1 + 1) = M * (M |^ 1) &
M |^ 1
= M )
by NEWTON:6;
((100 * m) * W) * U >= 1
* U
by XREAL_1:64, A1, A6, NAT_1:14;
then
M > U
by A8, NAT_1:13;
then
M >= U + 1
by NAT_1:13;
then
M * (U + 1) <= M * M
by XREAL_1:64;
then
(
0 < M * (U + 1) &
M * (U + 1) <= M |^ U )
by A30, A31, XXREAL_0:2;
then A32:
2
* (M * (U + 1)) <= 2
* (M |^ U)
by XREAL_1:64;
U >= 1
by A6, A7, NAT_1:14;
then
2
* (M |^ U) <= (2 |^ U) * (M |^ U)
by PREPOWER:12, XREAL_1:64;
then
2
* (M |^ U) <= (2 * M) |^ U
by NEWTON:7;
then
2
* (M * (U + 1)) <= (2 * M) |^ U
by A32, XXREAL_0:2;
then
(2 * (M * (U + 1))) |^ W <= ((2 * M) |^ U) |^ W
by PREPOWER:9;
then A33:
(2 * (M * (U + 1))) |^ W <= (2 * M) |^ (U * W)
by NEWTON:9;
((2 * M) |^ (U * W)) |^ 1
= (2 * M) |^ (U * W)
;
then A34:
((2 * M) |^ (U * W)) * ((2 * M) |^ (U * W)) =
((2 * M) |^ (U * W)) |^ (1 + 1)
by NEWTON:6
.=
(2 * M) |^ ((U * W) * 2)
by NEWTON:9
;
(
U * W >= 1 & 2
* M >= 1 &
M >= 1 )
by A1, A6, A7, NAT_1:14;
then
(
(2 * M) |^ (U * W) >= 2
* M & 2
* M >= 2
* 1 )
by PREPOWER:12, XREAL_1:64;
then
1
* 2
<= (2 * M) |^ (U * W)
by XXREAL_0:2;
then
1
<= ((2 * M) |^ (U * W)) / 2
by XREAL_1:77;
then
((2 * M) |^ (U * W)) * 1
<= ((2 * M) |^ (U * W)) * (((2 * M) |^ (U * W)) * (1 / 2))
by XREAL_1:64;
then A35:
(2 * (M * (U + 1))) |^ W <= ((2 * M) |^ ((U * W) * 2)) * (1 / 2)
by A34, A33, XXREAL_0:2;
((100 * U) * W) * m >= ((100 * U) * W) * 1
by A1, NAT_1:14, XREAL_1:64;
then A36:
M > (100 * U) * W
by A8, NAT_1:13;
A37:
( 4
* (U * W) <= 100
* (U * W) & 2
* (U * W) <= 100
* (U * W) )
by XREAL_1:64;
then A38:
(
(4 * U) * W < M &
(2 * U) * W < M )
by A36, XXREAL_0:2;
consider t being
_Theta such that A39:
Py (
M,
(((2 * U) * W) + 1))
= ((2 * M) |^ ((U * W) * 2)) * (1 + (t * (((2 * U) * W) / M)))
by A37, A36, XXREAL_0:2, Th10;
- 1
<= t
by Def1;
then A40:
(- 1) * ((4 * U) * W) <= t * ((4 * U) * W)
by XREAL_1:64;
(- 1) * M <= (- 1) * ((4 * U) * W)
by A38, XREAL_1:65;
then
- M <= (t * ((2 * U) * W)) * 2
by A40, XXREAL_0:2;
then
(
M * (- (1 / 2)) = (M * (- 1)) / 2 &
(M * (- 1)) / 2
<= t * ((2 * U) * W) )
by XREAL_1:79;
then
- (1 / 2) <= (t * ((2 * U) * W)) / M
by XREAL_1:77;
then
- (1 / 2) <= t * (((2 * U) * W) / M)
by XCMPLX_1:74;
then
( 1
/ 2
= 1
+ (- (1 / 2)) & 1
+ (- (1 / 2)) <= 1
+ (t * (((2 * U) * W) / M)) )
by XREAL_1:7;
then
((2 * M) |^ ((U * W) * 2)) * (1 / 2) <= ((2 * M) |^ ((U * W) * 2)) * (1 + (t * (((2 * U) * W) / M)))
by XREAL_1:64;
then A41:
(2 * (M * (U + 1))) |^ W <= Py (
M,
(((2 * U) * W) + 1))
by A35, A39, XXREAL_0:2;
A42:
2
* U >= 2
* 1
by A7, A6, NAT_1:14, XREAL_1:64;
(
m * U >= 1 &
W >= 1 )
by A1, A6, A7, NAT_1:14;
then
100
* (m * U) >= 3
* 1
by XREAL_1:66;
then
(100 * (m * U)) * W >= 3
* W
by XREAL_1:64;
then
(
M >= ((2 * W) + W) + 1 &
((2 * W) + W) + 1
= ((2 * W) + 1) + W &
((2 * W) + 1) + W >= ((2 * W) + 1) + 1 )
by A1, A6, NAT_1:14, XREAL_1:6, A8;
then
(2 * W) + 2
<= M
by XXREAL_0:2;
then
((2 * W) + 2) * U <= MU
by XREAL_1:64;
then
(
((2 * W) * U) + 2
<= ((2 * W) * U) + (2 * U) &
((2 * W) * U) + (2 * U) <= MU )
by A42, XREAL_1:6;
then
(((2 * W) * U) + 1) + 1
<= MU
by XXREAL_0:2;
then
((2 * W) * U) + 1
<= MU - 1
by XREAL_1:19;
then
(
(2 * (U * W)) + 1
< MU - 1 or
(2 * (U * W)) + 1
= MU - 1 )
by XXREAL_0:1;
then A43:
Py (
M,
(((2 * U) * W) + 1))
<= Py (
M,
(MU - 1))
by HILB10_1:11;
(2 * (U * W)) + 1
<= 100
* (U * W)
by NAT_1:13, A1, A6, A7, XREAL_1:68;
then
(
(2 * (U * W)) + 1
< M &
M = M1 + 1 )
by A36, XXREAL_0:2;
then
(2 * (U * W)) + 1
<= M1
by NAT_1:13;
then
(
(2 * (U * W)) + 1
< M1 or
(2 * (U * W)) + 1
= M1 )
by XXREAL_0:1;
then A44:
Py (
M,
(((2 * U) * W) + 1))
<= Py (
M,
M1)
by HILB10_1:11;
r < (2 * (M * (U + 1))) |^ W
by A28, A20, A29, XXREAL_0:2;
then
r < Py (
M,
(((2 * U) * W) + 1))
by A41, XXREAL_0:2;
hence
(
r < Py (
M,
M1) &
r < Py (
M,
(MU - 1)) )
by A43, A44, XXREAL_0:2;
verum
end;
A45:
U >= 1
by A6, A7, NAT_1:14;
A46:
((100 * m) * U) * W >= 1 * W
by XREAL_1:64, A1, A7, NAT_1:14;
then
W + 1 <= (M - 1) + 1
by A8, XREAL_1:6;
then A47:
(W + 1) * 1 <= M * U
by A45, XREAL_1:66;
A48:
S = Py (M,(k + 1))
proof
A49:
S < Py (
M,
M1)
by A27, A23, XXREAL_0:2;
A50:
M - 1
>= k + 1
by A46, A8, A6, A12, XXREAL_0:2;
S - (k + 1) = s * (M - 1)
by A9;
then
S,
k + 1
are_congruent_mod M - 1
by INT_1:def 3, INT_1:def 4;
hence
S = Py (
M,
(k + 1))
by A2, A49, A50, Th11, A9;
verum
end;
A51:
T = Py (MU,(Wk + 1))
proof
M * 1
<= MU
by XREAL_1:64, A6, A7, NAT_1:14;
then
Py (
M,
(MU - 1))
<= Py (
MU,
(MU - 1))
by HILB10_6:15;
then
r < Py (
MU,
(MU - 1))
by A27, XXREAL_0:2;
then A52:
T < Py (
MU,
(MU - 1))
by A24, XXREAL_0:2;
A53:
( 1
- k <= 1
- 1 & 1
- 1
= 0 )
by XREAL_1:10, A1, NAT_1:14;
(
(1 - k) + (W + 1) <= 0 + (W + 1) &
0 + (W + 1) <= MU )
by A47, A53, XREAL_1:6;
then
(Wk + 1) + 1
<= MU
by XXREAL_0:2;
then A54:
Wk + 1
<= MU - 1
by XREAL_1:19;
T - (Wk + 1) = (MU - 1) * t
by A10;
hence
T = Py (
MU,
(Wk + 1))
by A54, A52, A10, A15, A3, Th11, INT_1:def 5;
verum
end;
A55:
r - (((m * S) * T) * U) < ((3 * u) * S) * T
A58:
(m * U) + (3 * u) > r / (S * T)
U < U + 1
by NAT_1:13;
then
M * U <= M * (U + 1)
by XREAL_1:64;
then
W + 1 <= M * (U + 1)
by A47, XXREAL_0:2;
then
W < M * (U + 1)
by NAT_1:13;
then consider t1 being _Theta such that
A59:
Py (mu,(w + 1)) = ((2 * mu) |^ w) * (1 + (t1 * (w / mu)))
by A20, Th10;
reconsider I = 1 as _Theta by Def1;
set E = (t1 * (w / mu)) - ((W + 1) / ((2 * mu) |^ w));
( W |^ (1 + 1) = W * (W |^ 1) & W |^ 1 = W )
by NEWTON:6;
then A60:
W |^ (2 + 1) = (W * W) * W
by NEWTON:6;
( u |^ (1 + 1) = u * (u |^ 1) & u |^ 1 = u )
by NEWTON:6;
then A61:
u |^ (2 + 1) = (u * u) * u
by NEWTON:6;
A62:
W >= 1
by A1, A6, NAT_1:14;
A63:
m >= 1
by A1, NAT_1:14;
A64:
2 * mu >= 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
( W >= f * (100 * k) & f * (100 * k) >= 1 * (100 * k) )
by A6, XREAL_1:64;
then A65:
( W >= 100 * k & 100 * k >= 5 * k & 100 * k >= 1 * k )
by XXREAL_0:2, XREAL_1:64;
then A66:
k <= W
by XXREAL_0:2;
( U > 100 * ((u |^ 3) * (W |^ 3)) & 100 * ((u |^ 3) * (W |^ 3)) >= 1 * ((u |^ 3) * (W |^ 3)) )
by A7, NAT_1:13, XREAL_1:64;
then
U > (u |^ 3) * (W |^ 3)
by A7, NAT_1:13;
then A67:
U |^ k >= ((u |^ 3) * (W |^ 3)) |^ k
by A1, A6, PREPOWER:9;
A68:
u >= 1
by NAT_1:14, A1;
then A69:
( u |^ 3 >= u & W |^ 3 >= 1 & W |^ 3 >= W & u |^ 3 >= 1 )
by A62, PREPOWER:12, NAT_1:14;
then
( (u |^ 3) * (W |^ 3) >= u * 1 & (u |^ 3) * (W |^ 3) >= W * 1 )
by XREAL_1:66;
then
( U > 100 * ((u |^ 3) * (W |^ 3)) & 100 * ((u |^ 3) * (W |^ 3)) >= 100 * u & 100 * ((u |^ 3) * (W |^ 3)) >= 100 * W )
by XREAL_1:64, NAT_1:13, A7;
then A70:
( U >= 100 * u & 100 * u >= 12 * u & U >= 100 * W & 100 * u >= 16 * u )
by XXREAL_0:2, XREAL_1:64;
then A71:
U >= 12 * u
by XXREAL_0:2;
( (W |^ k) |^ (1 + 1) = ((W |^ k) |^ 1) * (W |^ k) & (W |^ k) |^ 1 = W |^ k )
by NEWTON:6;
then
(W |^ k) |^ (2 + 1) = ((W |^ k) * (W |^ k)) * (W |^ k)
by NEWTON:6;
then A72:
((W |^ k) ^2) * (W |^ k) = (W |^ k) |^ 3
by SQUARE_1:def 1;
k >= 1
by A1, NAT_1:14;
then
u |^ k >= u
by A68, PREPOWER:12;
then
(u |^ k) |^ 3 >= u |^ 3
by A1, PREPOWER:9;
then A73:
(u |^ k) |^ 3 >= (u ^2) * u
by A61, SQUARE_1:def 1;
m * U >= 1
by NAT_1:14, A1, A20, A7;
then
( (100 * W) * (m * U) >= (100 * W) * 1 & (100 * W) * 1 >= 5 * k )
by A66, XREAL_1:66;
then
(100 * W) * (m * U) >= 5 * k
by XXREAL_0:2;
then A74:
5 * k <= M
by NAT_1:13, A8;
then A75:
(5 * k) / M <= 1
by XREAL_1:183;
A76:
2 * k <= 5 * k
by XREAL_1:64;
then A77:
M >= 2 * k
by A74, XXREAL_0:2;
then
(2 * k) / M <= 1
by XREAL_1:183;
then A78:
2 * (k / M) <= 1
by XCMPLX_1:74;
A79:
( 4 * W <= 100 * W & 2 * W <= 100 * W )
by XREAL_1:64;
then A80:
( 4 * W <= U & 2 * W <= U )
by A70, XXREAL_0:2;
then A81:
2 * W <= U + 1
by NAT_1:13;
W <= W + W
by NAT_1:11;
then A82:
W <= U
by A80, XXREAL_0:2;
Wk <= W - 0
by XREAL_1:10;
then
( 4 * Wk <= 4 * W & 2 * Wk <= 2 * W )
by XREAL_1:64;
then A83:
( 4 * Wk <= U & 2 * Wk <= U )
by A80, XXREAL_0:2;
then
(4 * Wk) / U <= 1
by XREAL_1:183;
then A84:
((4 * Wk) / U) * (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) / U) * (1 / M)
by XCMPLX_1:103
;
then A85:
( (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 A84, 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 A85, XXREAL_0:2;
then A86:
(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 A87:
(2 * (k / M)) + ((3 * k) / M) = ((2 * k) + (3 * k)) / M
by XCMPLX_1:62;
( ((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 A86, A87, A75, XXREAL_0:2, XREAL_1:6;
then A88:
(2 * (k / M)) + (2 * (1 / M)) <= 1
by XXREAL_0:2;
A89:
2 * W <= U
by A79, A70, XXREAL_0:2;
M >= 1
by NAT_1:14;
then A90:
MU >= 1 * (2 * Wk)
by A83, XREAL_1:66;
(3 * 2) * u <= 12 * u
by XREAL_1:64;
then
(3 * u) * 2 <= 1 * U
by A71, XXREAL_0:2;
then A91:
(3 * u) / U <= 1 / 2
by XREAL_1:102, A20, A7;
(4 * u) * 4 <= 1 * U
by A70, XXREAL_0:2;
then A92:
(4 * u) / U <= 1 / 4
by XREAL_1:102, A20, A7;
1 * mu >= M * (2 * W)
by A81, A20, XREAL_1:64;
then
(W * (2 * M)) / mu <= 1
by XREAL_1:79;
then
(2 * M) * (W / mu) <= 1
by XCMPLX_1:74;
then A93:
W / mu <= 1 / (2 * M)
by XREAL_1:77;
then A94:
- (W / mu) >= - (1 / (2 * M))
by XREAL_1:24;
( - 1 <= t1 & t1 <= 1 )
by Def1;
then
( (- 1) * (w / mu) <= t1 * (w / mu) & t1 * (w / mu) <= 1 * (w / mu) )
by XREAL_1:64;
then A95:
( - (1 / (2 * M)) <= t1 * (w / mu) & t1 * (w / mu) <= 1 / (2 * M) )
by A20, A93, A94, XXREAL_0:2;
W + 1 <= U + 1
by A82, XREAL_1:6;
then A96:
(W + 1) * (2 * M) <= (U + 1) * (2 * M)
by XREAL_1:64;
2 * mu <= (2 * mu) |^ w
by A64, A20, A62, PREPOWER:12;
then
(W + 1) * (2 * M) <= 1 * ((2 * mu) |^ w)
by A20, A96, XXREAL_0:2;
then
(W + 1) / ((2 * mu) |^ w) <= 1 / (2 * M)
by XREAL_1:102;
then
( 1 / (2 * M) >= - ((W + 1) / ((2 * mu) |^ w)) & - ((W + 1) / ((2 * mu) |^ w)) >= - (1 / (2 * M)) )
by XREAL_1:24;
then A97:
( (- (1 / (2 * M))) + (- (1 / (2 * M))) <= (t1 * (w / mu)) + (- ((W + 1) / ((2 * mu) |^ w))) & (t1 * (w / mu)) + (- ((W + 1) / ((2 * mu) |^ w))) <= (1 / (2 * M)) + (1 / (2 * M)) )
by A95, XREAL_1:7;
A98:
(1 * 1) / (2 * M) = (1 / 2) * (1 / M)
by XCMPLX_1:76;
A99:
(t1 * (w / mu)) - ((W + 1) / ((2 * mu) |^ w)) <= I * (1 / M)
by A97, A98;
A100:
(- I) * (1 / M) <= (t1 * (w / mu)) - ((W + 1) / ((2 * mu) |^ w))
by A97, A98;
consider t2 being _Theta such that
A101:
(t1 * (w / mu)) - ((W + 1) / ((2 * mu) |^ W)) = t2 * (1 / M)
by A20, A99, A100, Th4;
A102:
r = (((2 * mu) |^ w) * (1 + (t1 * (w / mu)))) - (W + 1)
by A59, A20;
r = (((2 * mu) |^ w) * (1 + (t1 * (w / mu)))) - (((W + 1) / ((2 * mu) |^ W)) * ((2 * mu) |^ W))
by A102, XCMPLX_1:87;
then
r = ((2 * mu) |^ w) * ((1 + (t1 * (w / mu))) - ((W + 1) / ((2 * mu) |^ W)))
by A20;
then A103:
r = ((2 * mu) |^ w) * (1 + (t2 * (1 / M)))
by A101;
( S <= (2 * M) |^ k & T <= (2 * MU) |^ Wk )
by A48, A51, HILB10_1:17;
then
S * T <= ((2 * M) |^ k) * ((2 * MU) |^ Wk)
by XREAL_1:66;
then A104:
r / (S * T) >= r / (((2 * M) |^ k) * ((2 * MU) |^ Wk))
by XREAL_1:118, A9, A10, A15;
((2 * M) * U) |^ Wk = ((2 * M) |^ Wk) * (U |^ Wk)
by NEWTON:7;
then A105: ((2 * M) |^ k) * ((2 * MU) |^ Wk) =
(((2 * M) |^ k) * ((2 * M) |^ Wk)) * (U |^ Wk)
.=
((2 * M) |^ (k + Wk)) * (U |^ Wk)
by NEWTON:8
;
(2 * mu) |^ w =
((2 * M) * (U + 1)) |^ W
by A20
.=
((2 * M) |^ W) * ((U + 1) |^ W)
by NEWTON:7
;
then A106: r / (((2 * M) |^ k) * ((2 * MU) |^ Wk)) =
(((2 * M) |^ W) * (((U + 1) |^ W) * (1 + (t2 * (1 / M))))) / (((2 * M) |^ W) * (U |^ Wk))
by A103, A105
.=
(((U + 1) |^ W) * (1 + (t2 * (1 / M)))) / ((U |^ Wk) * 1)
by XCMPLX_1:91
.=
(((U + 1) |^ W) / (U |^ Wk)) * ((1 + (t2 * (1 / M))) / 1)
by XCMPLX_1:76
.=
(((U + 1) |^ W) / (U |^ Wk)) * (1 + (t2 * (1 / M)))
;
1 / M <= 1 / 2
by NAT_2:29, XREAL_1:118;
then A107:
- (1 / M) >= - (1 / 2)
by XREAL_1:24;
( - 1 <= t2 & t2 <= 1 )
by Def1;
then
(- 1) * (1 / M) <= t2 * (1 / M)
by XREAL_1:64;
then
- (1 / 2) <= t2 * (1 / M)
by A107, XXREAL_0:2;
then
1 + (- (1 / 2)) <= 1 + (t2 * (1 / M))
by XREAL_1:6;
then
(((U + 1) |^ W) / (U |^ Wk)) * (1 + (t2 * (1 / M))) >= (1 / 2) * (((U + 1) |^ W) / (U |^ Wk))
by XREAL_1:66;
then A108:
r / (S * T) >= (1 / 2) * (((U + 1) |^ W) / (U |^ Wk))
by A104, A106, XXREAL_0:2;
U < U + 1
by NAT_1:13;
then
U |^ W < (U + 1) |^ W
by PREPOWER:10, A1, A6, NAT_1:14;
then A109:
(U |^ W) / (U |^ Wk) < ((U + 1) |^ W) / (U |^ Wk)
by A7, XREAL_1:74;
A110:
U |^ (Wk + k) = (U |^ Wk) * (U |^ k)
by NEWTON:8;
then
(U |^ W) / ((U |^ Wk) * 1) = (U |^ k) / 1
by A7, XCMPLX_1:91;
then
(1 / 2) * (U |^ k) < (1 / 2) * (((U + 1) |^ W) / (U |^ Wk))
by XREAL_1:68, A109;
then A111:
r / (S * T) > (1 / 2) * (U |^ k)
by A108, XXREAL_0:2;
m * U >= 1 * (12 * u)
by A71, A63, XREAL_1:66;
then
20 * (m * U) >= 20 * (12 * u)
by XREAL_1:66;
then
((20 * m) * U) * W >= (240 * u) * W
by XREAL_1:66;
then A112:
(80 * ((m * U) * W)) + (20 * ((m * U) * W)) >= (80 * ((m * U) * W)) + (((80 * 3) * u) * W)
by XREAL_1:6;
( (m * U) + (3 * u) > (1 / 2) * (U |^ k) & (1 / 2) * (U |^ k) >= (1 / 2) * (((u |^ 3) * (W |^ 3)) |^ k) )
by A58, A67, A111, XXREAL_0:2, XREAL_1:66;
then
(m * U) + (3 * u) > (1 / 2) * (((u |^ 3) * (W |^ 3)) |^ k)
by XXREAL_0:2;
then A113:
((m * U) + (3 * u)) * (80 * W) >= ((1 / 2) * (((u |^ 3) * (W |^ 3)) |^ k)) * (80 * W)
by XREAL_1:66;
A114:
M > (80 * ((m * U) + (3 * u))) * W
by NAT_1:13, A8, A112;
(((u |^ 3) * (W |^ 3)) |^ k) * W =
(((u |^ 3) |^ k) * ((W |^ 3) |^ k)) * W
by NEWTON:7
.=
((u |^ (k * 3)) * ((W |^ 3) |^ k)) * W
by NEWTON:9
.=
((u |^ (k * 3)) * (W |^ (3 * k))) * W
by NEWTON:9
.=
(((u |^ k) |^ 3) * (W |^ (3 * k))) * W
by NEWTON:9
.=
(((u |^ k) |^ 3) * ((W |^ k) |^ 3)) * W
by NEWTON:9
;
then A115:
M > ((40 * ((u |^ k) |^ 3)) * ((W |^ k) |^ 3)) * W
by A113, A114, XXREAL_0:2;
(40 * ((u |^ k) |^ 3)) * (((W |^ k) |^ 3) * W) >= 1 * (((W |^ k) |^ 3) * W)
by A1, NAT_1:14, XREAL_1:64;
then A116:
M > W * (((W |^ k) ^2) * (W |^ k))
by A72, A115, XXREAL_0:2;
40 * ((W |^ k) |^ 3) >= 1
by NAT_1:14, A6, A1;
then
(40 * ((W |^ k) |^ 3)) * ((u |^ k) |^ 3) >= 1 * ((u ^2) * u)
by A73, XREAL_1:66;
then
((40 * ((W |^ k) |^ 3)) * ((u |^ k) |^ 3)) * W >= (1 * ((u ^2) * u)) * W
by XREAL_1:66;
then
W * ((u ^2) * u) < M
by A115, XXREAL_0:2;
then A117:
u = W |^ k
by A116, Th13, A6, A1, A4, A48, A11;
A118: (r - (((m * S) * T) * U)) / ((S * T) * U) =
(r / ((S * T) * U)) - ((m * ((S * T) * U)) / (1 * ((S * T) * U)))
by XCMPLX_1:120
.=
(r / ((S * T) * U)) - (m / 1)
by A15, A10, A7, A8, A9, XCMPLX_1:91
;
(r - (((m * S) * T) * U)) / ((S * T) * U) < ((3 * u) * (S * T)) / ((S * T) * U)
by A55, A8, A9, A15, A10, A7, XREAL_1:74;
then
(r / ((S * T) * U)) - (m / 1) < (3 * u) / U
by A118, A8, A9, A15, A10, XCMPLX_1:91;
then A119:
(r / ((S * T) * U)) - (m / 1) < 1 / 2
by A91, XXREAL_0:2;
2 * k >= 1 * k
by XREAL_1:64;
then consider t3 being _Theta such that
A120:
Py (M,(k + 1)) = ((2 * M) |^ k) * (1 + (t3 * (k / M)))
by Th10, A77, XXREAL_0:2;
2 * Wk >= 1 * Wk
by XREAL_1:64;
then consider t4 being _Theta such that
A121:
Py (MU,(Wk + 1)) = ((2 * MU) |^ Wk) * (1 + (t4 * (Wk / MU)))
by Th10, A90, XXREAL_0:2;
1 * M >= 2 * k
by A76, A74, XXREAL_0:2;
then
k / M <= 1 / 2
by XREAL_1:102;
then consider T3 being _Theta such that
A122:
1 / (1 + (t3 * (k / M))) = 1 + ((T3 * 2) * (k / M))
by Th7;
1 * MU >= 2 * Wk
by A90;
then
Wk / MU <= 1 / 2
by XREAL_1:102;
then consider T4 being _Theta such that
A123:
1 / (1 + (t4 * (Wk / MU))) = 1 + ((T4 * 2) * (Wk / MU))
by Th7;
consider T5 being _Theta such that
A124:
(1 + (T3 * (2 * (k / M)))) * (1 + (t2 * (1 / M))) = 1 + (T5 * ((2 * (k / M)) + (2 * (1 / M))))
by A78, Th3;
consider T6 being _Theta such that
A125:
(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 A88, Th3;
A126:
|.(((2 * (k / M)) + (2 * (1 / M))) + (2 * (2 * (Wk / MU)))).| = ((2 * (k / M)) + (2 * (1 / M))) + (2 * (2 * (Wk / MU)))
;
|.((5 * k) / M).| = (5 * k) / M
;
then consider T7 being _Theta such that
A127:
T6 * (((2 * (k / M)) + (2 * (1 / M))) + (2 * (2 * (Wk / MU)))) = T7 * ((5 * k) / M)
by A87, A126, Th2, A86;
A128:
1 / S = (1 / ((2 * M) |^ k)) * (1 + ((T3 * 2) * (k / M)))
by A120, A48, XCMPLX_1:102, A122;
A129:
1 / T = (1 / ((2 * MU) |^ Wk)) * (1 + ((T4 * 2) * (Wk / MU)))
by A123, A121, A51, XCMPLX_1:102;
A130: (2 * mu) |^ w =
((2 * M) * (U + 1)) |^ W
by A20
.=
((2 * M) |^ W) * ((U + 1) |^ W)
by NEWTON:7
;
(1 / ((2 * M) |^ k)) * (1 / ((2 * MU) |^ Wk)) = 1 / (((2 * M) |^ W) * (U |^ Wk))
by A105, XCMPLX_1:102;
then A131: (((2 * mu) |^ w) * (1 / ((2 * M) |^ k))) * (1 / ((2 * MU) |^ Wk)) =
(((2 * M) |^ W) * ((U + 1) |^ W)) * (1 / (((2 * M) |^ W) * (U |^ Wk)))
by A130
.=
(((2 * M) |^ W) * ((U + 1) |^ W)) / (((2 * M) |^ W) * (U |^ Wk))
by XCMPLX_1:99
.=
((U + 1) |^ W) / (U |^ Wk)
by XCMPLX_1:91
;
A132: r / (S * T) =
r * (1 / (S * T))
by XCMPLX_1:99
.=
r * ((1 / S) * (1 / T))
by XCMPLX_1:102
.=
(((U + 1) |^ W) / (U |^ Wk)) * (((1 + (t2 * (1 / M))) * (1 + ((T3 * 2) * (k / M)))) * (1 + ((T4 * 2) * (Wk / MU))))
by A131, A103, A129, A128
.=
(((U + 1) |^ W) / (U |^ Wk)) * (1 + (T7 * ((5 * k) / M)))
by A124, A125, A127
;
then A133: r / ((S * T) * U) =
((((U + 1) |^ W) / (U |^ Wk)) * (1 + (T7 * ((5 * k) / M)))) * (1 / U)
by XCMPLX_1:103
.=
((((U + 1) |^ W) / (U |^ Wk)) * (1 / U)) * (1 + (T7 * ((5 * k) / M)))
.=
(((U + 1) |^ W) / ((U |^ Wk) * U)) * (1 + (T7 * ((5 * k) / M)))
by XCMPLX_1:103
.=
(((U + 1) |^ W) / (U |^ (Wk + 1))) * (1 + (T7 * ((5 * k) / M)))
by NEWTON:6
;
set IW = (U,1) In_Power W;
set IWk = ((U,1) In_Power W) | k;
A134:
len ((U,1) In_Power W) = W + 1
by NEWTON:def 4;
A135:
k < W + 1
by A66, NAT_1:13;
then A136:
len (((U,1) In_Power W) | k) = k
by A134, FINSEQ_1:59;
consider IWW being FinSequence such that
A137:
(U,1) In_Power W = (((U,1) In_Power W) | k) ^ IWW
by FINSEQ_1:80;
reconsider IWW = IWW as FinSequence of REAL by A137, FINSEQ_1:36;
reconsider k1 = k - 1 as Nat by A1;
A138:
len ((((U,1) In_Power W) | k) ^ IWW) = k + (len IWW)
by A136, FINSEQ_1:22;
then A139:
len IWW = Wk + 1
by A134, A137;
A140:
len (((U,1) In_Power W) | k) = (k1 - 0) + 1
by A135, A134, FINSEQ_1:59;
A141:
for i being Nat st i + 1 in dom (((U,1) In_Power W) | k) holds
(((U,1) In_Power W) | k) . (i + 1) = (W choose (0 + i)) * (U |^ (W -' (0 + i)))
proof
let i be
Nat;
( i + 1 in dom (((U,1) In_Power W) | k) implies (((U,1) In_Power W) | k) . (i + 1) = (W choose (0 + i)) * (U |^ (W -' (0 + i))) )
assume A142:
i + 1
in dom (((U,1) In_Power W) | k)
;
(((U,1) In_Power W) | k) . (i + 1) = (W choose (0 + i)) * (U |^ (W -' (0 + i)))
A143:
i + 1
in dom ((U,1) In_Power W)
by A142, RELAT_1:57;
i + 1
<= k
by A142, FINSEQ_3:25, A136;
then
i + 1
<= W
by A66, XXREAL_0:2;
then
i < W
by NAT_1:13;
then A144:
W -' i = W - i
by XREAL_1:233;
A145:
(i + 1) - 1
= i
;
(((U,1) In_Power W) | k) . (i + 1) =
((U,1) In_Power W) . (i + 1)
by A142, FUNCT_1:47
.=
((W choose i) * (U |^ (W -' i))) * (1 |^ i)
by A143, A145, A144, NEWTON:def 4
;
hence
(((U,1) In_Power W) | k) . (i + 1) = (W choose (0 + i)) * (U |^ (W -' (0 + i)))
;
verum
end;
A146:
( W |^ 0 = 1 & W -' 0 = W - 0 )
by XREAL_1:233, NEWTON:4;
k1 < k1 + 1
by NAT_1:13;
then
k1 < W
by A66, XXREAL_0:2;
then A147:
( 0 < Sum (((U,1) In_Power W) | k) & Sum (((U,1) In_Power W) | k) < (2 * (W |^ 0)) * (U |^ (W -' 0)) )
by Th14, A89, A140, A141;
set UIWk = (1 / (U |^ (Wk + 1))) * (((U,1) In_Power W) | k);
A148:
(1 / U) * U = 1
by A7, A6, XCMPLX_1:87;
U |^ (Wk + 1) = (U |^ Wk) * U
by NEWTON:6;
then
1 / (U |^ (Wk + 1)) = (1 / U) * (1 / (U |^ Wk))
by XCMPLX_1:102;
then A149: (1 / (U |^ (Wk + 1))) * (U |^ Wk) =
(1 / U) * ((1 / (U |^ Wk)) * (U |^ Wk))
.=
(1 / U) * 1
by XCMPLX_1:87, A7
;
rng ((1 / (U |^ (Wk + 1))) * (((U,1) In_Power W) | k)) c= NAT
proof
let y be
object ;
TARSKI:def 3 ( not y in rng ((1 / (U |^ (Wk + 1))) * (((U,1) In_Power W) | k)) or y in NAT )
assume A150:
y in rng ((1 / (U |^ (Wk + 1))) * (((U,1) In_Power W) | k))
;
y in NAT
consider i being
object such that A151:
(
i in dom ((1 / (U |^ (Wk + 1))) * (((U,1) In_Power W) | k)) &
((1 / (U |^ (Wk + 1))) * (((U,1) In_Power W) | k)) . i = y )
by A150, FUNCT_1:def 3;
reconsider i =
i as
Nat by A151;
A152:
dom ((1 / (U |^ (Wk + 1))) * (((U,1) In_Power W) | k)) = dom (((U,1) In_Power W) | k)
by VALUED_1:def 5;
then A153:
( 1
<= i &
i <= k )
by A151, FINSEQ_3:25, A136;
then reconsider i1 =
i - 1 as
Nat ;
i = i1 + 1
;
then
i1 < k
by A153, NAT_1:13;
then A154:
(
k -' i1 = k - i1 &
W -' i1 = W - i1 &
k -' i = k - i )
by A66, XXREAL_0:2, A153, XREAL_1:233;
then A155:
W -' i1 = Wk + (k -' i1)
;
k -' i1 = (k -' i) + 1
by A154;
then A156:
(U |^ (k -' i1)) * (1 / U) =
((U |^ (k -' i)) * U) * (1 / U)
by NEWTON:6
.=
(U |^ (k -' i)) * (U * (1 / U))
.=
U |^ (k -' i)
by A148
;
(((U,1) In_Power W) | k) . (i1 + 1) = (W choose (0 + i1)) * (U |^ (W -' (0 + i1)))
by A152, A151, A141;
then ((1 / (U |^ (Wk + 1))) * (((U,1) In_Power W) | k)) . i =
(1 / (U |^ (Wk + 1))) * ((W choose i1) * (U |^ (W -' i1)))
by VALUED_1:6
.=
(1 / (U |^ (Wk + 1))) * ((W choose i1) * ((U |^ Wk) * (U |^ (k -' i1))))
by A155, NEWTON:8
.=
(W choose i1) * (U |^ (k -' i))
by A156, A149
;
hence
y in NAT
by A151;
verum
end;
then reconsider UIWk = (1 / (U |^ (Wk + 1))) * (((U,1) In_Power W) | k) as FinSequence of NAT by FINSEQ_1:def 4;
reconsider Z = Sum UIWk as Element of NAT by ORDINAL1:def 12;
A157: (1 / (U |^ (Wk + 1))) * ((2 * (U |^ Wk)) * (U |^ k)) =
2 * ((1 / U) * (U |^ (k1 + 1)))
by A149
.=
2 * ((1 / U) * ((U |^ k1) * U))
by NEWTON:6
.=
(2 * ((1 / U) * U)) * (U |^ k1)
.=
(2 * 1) * (U |^ k1)
by A6, A7, XCMPLX_1:87
;
A158:
( Z = (1 / (U |^ (Wk + 1))) * (Sum (((U,1) In_Power W) | k)) & (1 / (U |^ (Wk + 1))) * (Sum (((U,1) In_Power W) | k)) < (1 / (U |^ (Wk + 1))) * ((2 * (U |^ Wk)) * (U |^ k)) )
by A7, A110, XREAL_1:68, A147, A146, RVSUM_1:87;
A159:
for i being Nat st i + 1 in dom IWW holds
IWW . (i + 1) = (W choose (k + i)) * (U |^ (W -' (k + i)))
proof
let i be
Nat;
( i + 1 in dom IWW implies IWW . (i + 1) = (W choose (k + i)) * (U |^ (W -' (k + i))) )
assume A160:
i + 1
in dom IWW
;
IWW . (i + 1) = (W choose (k + i)) * (U |^ (W -' (k + i)))
A161:
k + (i + 1) in dom ((U,1) In_Power W)
by A160, A136, A137, FINSEQ_1:28;
then
(k + i) + 1
<= W + 1
by A134, FINSEQ_3:25;
then A162:
W -' (k + i) = W - (k + i)
by XREAL_1:6, XREAL_1:233;
A163:
(k + (i + 1)) - 1
= k + i
;
IWW . (i + 1) =
((U,1) In_Power W) . (k + (i + 1))
by FINSEQ_1:def 7, A136, A137, A160
.=
((W choose (k + i)) * (U |^ (W -' (k + i)))) * (1 |^ (k + i))
by A161, A163, A162, NEWTON:def 4
;
hence
IWW . (i + 1) = (W choose (k + i)) * (U |^ (W -' (k + i)))
;
verum
end;
A164:
( 0 < Sum IWW & Sum IWW < (2 * (W |^ k)) * (U |^ (W -' k)) )
by A139, Th14, A89, A66, A1, A159;
set UIWW = (1 / (U |^ (Wk + 1))) * IWW;
set D = Sum ((1 / (U |^ (Wk + 1))) * IWW);
A165:
W -' k = Wk
by A65, XXREAL_0:2, XREAL_1:233;
A166:
( Sum ((1 / (U |^ (Wk + 1))) * IWW) = (1 / (U |^ (Wk + 1))) * (Sum IWW) & (1 / (U |^ (Wk + 1))) * (Sum IWW) < (1 / (U |^ (Wk + 1))) * ((2 * (W |^ k)) * (U |^ Wk)) )
by A7, A165, XREAL_1:68, A164, RVSUM_1:87;
( (U + 1) |^ W = Sum ((U,1) In_Power W) & Sum ((U,1) In_Power W) = (Sum (((U,1) In_Power W) | k)) + (Sum IWW) )
by A137, RVSUM_1:75, NEWTON:30;
then A167: Z + (Sum ((1 / (U |^ (Wk + 1))) * IWW)) =
(1 / (U |^ (Wk + 1))) * ((U + 1) |^ W)
by A166, A158
.=
((U + 1) |^ W) / (U |^ (Wk + 1))
by XCMPLX_1:99
;
A168:
|.(Sum ((1 / (U |^ (Wk + 1))) * IWW)).| = Sum ((1 / (U |^ (Wk + 1))) * IWW)
by A166, A164, ABSVALUE:def 1;
A169:
( |.T7.| <= 1 & |.((5 * k) / M).| <= 1 )
by Th1, A74, XREAL_1:183;
|.(((Sum ((1 / (U |^ (Wk + 1))) * IWW)) * T7) * ((5 * k) / M)).| =
|.((Sum ((1 / (U |^ (Wk + 1))) * IWW)) * T7).| * |.((5 * k) / M).|
by COMPLEX1:65
.=
(|.(Sum ((1 / (U |^ (Wk + 1))) * IWW)).| * |.T7.|) * |.((5 * k) / M).|
by COMPLEX1:65
.=
(|.((5 * k) / M).| * |.T7.|) * (Sum ((1 / (U |^ (Wk + 1))) * IWW))
by A168
;
then
|.(((Sum ((1 / (U |^ (Wk + 1))) * IWW)) * T7) * ((5 * k) / M)).| <= 1 * (Sum ((1 / (U |^ (Wk + 1))) * IWW))
by A166, A164, A169, XREAL_1:160, XREAL_1:64;
then A170:
|.(Sum ((1 / (U |^ (Wk + 1))) * IWW)).| + |.(((Sum ((1 / (U |^ (Wk + 1))) * IWW)) * T7) * ((5 * k) / M)).| <= (Sum ((1 / (U |^ (Wk + 1))) * IWW)) + (1 * (Sum ((1 / (U |^ (Wk + 1))) * IWW)))
by A168, XREAL_1:6;
|.(T7 * (Z * ((5 * k) / M))).| = |.T7.| * |.(Z * ((5 * k) / M)).|
by COMPLEX1:65;
then A171:
|.(T7 * (Z * ((5 * k) / M))).| <= 1 * |.(Z * ((5 * k) / M)).|
by Th1, XREAL_1:64;
(Sum ((1 / (U |^ (Wk + 1))) * IWW)) * (1 + (T7 * ((5 * k) / M))) = (Sum ((1 / (U |^ (Wk + 1))) * IWW)) + (((Sum ((1 / (U |^ (Wk + 1))) * IWW)) * T7) * ((5 * k) / M))
;
then
|.((Sum ((1 / (U |^ (Wk + 1))) * IWW)) * (1 + (T7 * ((5 * k) / M)))).| <= |.(Sum ((1 / (U |^ (Wk + 1))) * IWW)).| + |.(((Sum ((1 / (U |^ (Wk + 1))) * IWW)) * T7) * ((5 * k) / M)).|
by COMPLEX1:56;
then
|.((Sum ((1 / (U |^ (Wk + 1))) * IWW)) * (1 + (T7 * ((5 * k) / M)))).| <= (Sum ((1 / (U |^ (Wk + 1))) * IWW)) + (Sum ((1 / (U |^ (Wk + 1))) * IWW))
by A170, XXREAL_0:2;
then A172:
|.((Sum ((1 / (U |^ (Wk + 1))) * IWW)) * (1 + (T7 * ((5 * k) / M)))).| + |.((Z * T7) * ((5 * k) / M)).| <= ((Sum ((1 / (U |^ (Wk + 1))) * IWW)) + (Sum ((1 / (U |^ (Wk + 1))) * IWW))) + (Z * ((5 * k) / M))
by A171, XREAL_1:7;
|.(((Sum ((1 / (U |^ (Wk + 1))) * IWW)) * (1 + (T7 * ((5 * k) / M)))) + ((Z * T7) * ((5 * k) / M))).| <= |.((Sum ((1 / (U |^ (Wk + 1))) * IWW)) * (1 + (T7 * ((5 * k) / M)))).| + |.((Z * T7) * ((5 * k) / M)).|
by COMPLEX1:56;
then A173:
|.(((Sum ((1 / (U |^ (Wk + 1))) * IWW)) * (1 + (T7 * ((5 * k) / M)))) + ((Z * T7) * ((5 * k) / M))).| <= ((Sum ((1 / (U |^ (Wk + 1))) * IWW)) + (Sum ((1 / (U |^ (Wk + 1))) * IWW))) + (Z * ((5 * k) / M))
by A172, XXREAL_0:2;
A174: 2 * ((2 * (1 / U)) * u) =
(4 * u) * (1 / U)
.=
((4 * u) * 1) / U
by XCMPLX_1:74
;
2 * (Sum ((1 / (U |^ (Wk + 1))) * IWW)) < 2 * ((2 * (1 / U)) * u)
by A166, A149, A117, XREAL_1:68;
then A175:
2 * (Sum ((1 / (U |^ (Wk + 1))) * IWW)) < 1 / 4
by A174, A92, XXREAL_0:2;
A176:
U |^ (k1 + 1) = (U |^ k1) * U
by NEWTON:6;
( 1 / 2 < 1 & 1 <= m )
by A1, NAT_1:14;
then
1 / 2 <= m
by XXREAL_0:2;
then A177:
(1 / 2) + m <= m + m
by XREAL_1:6;
A178:
r / ((S * T) * U) < (1 / 2) + (m / 1)
by A119, XREAL_1:19;
then A179:
r / ((S * T) * U) <= 2 * m
by A177, XXREAL_0:2;
A180: (((1 / 2) * (U |^ k)) * (1 / U)) * (50 * U) =
(25 * (U |^ k)) * (U * (1 / U))
.=
(25 * (U |^ k)) * 1
by XCMPLX_1:87, A7, A6
;
r / ((S * T) * U) = (r / (S * T)) * (1 / U)
by XCMPLX_1:103;
then
r / ((S * T) * U) >= ((1 / 2) * (U |^ k)) * (1 / U)
by A111, XREAL_1:64;
then
2 * m >= ((1 / 2) * (U |^ k)) * (1 / U)
by A179, XXREAL_0:2;
then
(2 * m) * (50 * U) >= 25 * (U |^ k)
by XREAL_1:64, A180;
then
( M > ((100 * m) * U) * W & ((100 * m) * U) * W >= (25 * (U |^ k)) * W )
by XREAL_1:64, NAT_1:13, A8;
then
( M > 25 * ((U |^ k) * W) & 25 * ((U |^ k) * W) >= 24 * ((U |^ k) * W) )
by XXREAL_0:2, XREAL_1:64;
then A181:
M > 24 * ((U |^ k) * W)
by XXREAL_0:2;
((10 * f) * k) * (10 * (k + 1)) >= ((10 * f) * k) * 1
by NAT_1:14, XREAL_1:64;
then A182:
(24 * (U |^ k)) * W >= (24 * (U |^ k)) * ((10 * f) * k)
by A6, XREAL_1:64;
then A183:
((240 * f) * k) * (U |^ k) < M
by A181, XXREAL_0:2;
(f * k) * k <= (f * k) * (k + 1)
by XREAL_1:64, NAT_1:11;
then
((f * k) * k) * 96 <= ((f * k) * (k + 1)) * 100
by XREAL_1:66;
then A184:
( (96 * f) * (k * k) <= W & k ^2 = k * k )
by A6, SQUARE_1:def 1;
then
12 * ((8 * f) * (k ^2)) <= 1 * W
;
then A185:
((8 * f) * (k ^2)) / W <= 1 / 12
by XREAL_1:102, A1, A6;
1 <= f
by A1, NAT_1:14;
then
24 * 1 <= 96 * f
by XREAL_1:66;
then A186:
(24 * 1) * (k ^2) <= (96 * f) * (k ^2)
by XREAL_1:64;
then A187:
(24 * 1) * (k ^2) <= W
by A184, XXREAL_0:2;
A188:
1 * (k ^2) <= 24 * (k ^2)
by XREAL_1:64;
2 * (k ^2) <= 24 * (k ^2)
by XREAL_1:64;
then
2 * (k ^2) <= W * 1
by A187, XXREAL_0:2;
then A189:
(k ^2) / W <= 1 / 2
by XREAL_1:102, A1, A6;
6 * (4 * (k ^2)) <= 1 * W
by A186, A184, XXREAL_0:2;
then
(4 * (k ^2)) / W <= 1 / 6
by XREAL_1:102, A1, A6;
then A190:
4 * ((k ^2) / W) <= 1 / 6
by XCMPLX_1:74;
(k * (U |^ k)) * 1 <= (k * (U |^ k)) * f
by A1, NAT_1:14, XREAL_1:64;
then
((k * (U |^ k)) * 1) * 120 <= ((k * (U |^ k)) * f) * 240
by XREAL_1:66;
then
12 * (((U |^ k) * 10) * k) <= 1 * M
by A183, XXREAL_0:2;
then A191:
(((U |^ k) * 10) * k) / M <= 1 / 12
by XREAL_1:102;
A192:
1 * ((u |^ 3) * (W |^ 3)) <= 100 * ((u |^ 3) * (W |^ 3))
by XREAL_1:64;
(W * W) * 1 <= W |^ 3
by A60, A1, A6, NAT_1:14, XREAL_1:64;
then
( (W * W) * u <= (W |^ 3) * (u |^ 3) & (W |^ 3) * (u |^ 3) < U )
by A69, XREAL_1:66, A7, NAT_1:13, A192;
then
W * (W * (W |^ k)) <= U
by XXREAL_0:2, A117;
then A193:
W * (W |^ (k + 1)) <= U
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) * (W |^ (k + 1)) <= W * (W |^ (k + 1))
by A6, XREAL_1:64;
then
12 * ((8 * f) * (W |^ (k + 1))) <= 1 * U
by A193, XXREAL_0:2;
then A194:
((8 * f) * (W |^ (k + 1))) / U <= 1 / 12
by XREAL_1:102, A7;
1 <= (f * k) * (k + 1)
by A1, NAT_1:14;
then
1 * 24 <= 100 * ((f * k) * (k + 1))
by XREAL_1:66;
then
24 * (W |^ (k + 1)) <= W * (W |^ (k + 1))
by A6, XREAL_1:64;
then
12 * (2 * (W |^ (k + 1))) <= U * 1
by A193, XXREAL_0:2;
then
(2 * (W |^ (k + 1))) / U <= 1 / 12
by XREAL_1:102, A7;
then
2 * ((W |^ (k + 1)) / U) <= 1 / 12
by XCMPLX_1:74;
then A195:
2 * ((W |^ (k + 1)) * (1 / U)) <= 1 / 12
by XCMPLX_1:99;
A196:
( ((2 * (W |^ (k + 1))) * (1 / U)) + ((((U |^ k) * 10) * k) / M) <= (1 / 12) + (1 / 12) & (1 / 12) + (1 / 12) = 1 / 6 & 1 / 6 <= 1 / 2 )
by A195, A191, XREAL_1:7;
then A197:
((2 * (W |^ (k + 1))) * (1 / U)) + ((((U |^ k) * 10) * k) / M) <= 1 / 2
by XXREAL_0:2;
A198:
( 2 * (((2 * (W |^ (k + 1))) * (1 / U)) + ((((U |^ k) * 10) * k) / M)) <= 2 * (1 / 6) & 2 * (1 / 6) <= 1 )
by A196, XREAL_1:64;
then A199:
(2 * (((2 * (W |^ (k + 1))) * (1 / U)) + ((((U |^ k) * 10) * k) / M))) + (2 * (2 * ((k ^2) / W))) <= ((2 * 1) / 6) + (1 / 6)
by A190, XREAL_1:7;
A200:
2 * (((2 * (W |^ (k + 1))) * (1 / U)) + ((((U |^ k) * 10) * k) / M)) <= 1
by A198, XXREAL_0:2;
((6 * f) * U) * ((40 * k) * (U |^ k1)) >= 1 * ((40 * k) * (U |^ k1))
by XREAL_1:64, NAT_1:14, A1, A20, A7;
then A201:
(2 * (U |^ k1)) * (20 * k) <= M
by A176, A183, XXREAL_0:2;
Z * (20 * k) <= (2 * (U |^ k1)) * (20 * k)
by A158, A157, XREAL_1:64;
then
4 * (Z * (5 * k)) <= 1 * M
by A201, XXREAL_0:2;
then
(Z * (5 * k)) / M <= 1 / 4
by XREAL_1:102;
then
Z * ((5 * k) / M) <= 1 / 4
by XCMPLX_1:74;
then
( (2 * (Sum ((1 / (U |^ (Wk + 1))) * IWW))) + (Z * ((5 * k) / M)) < (1 / 4) + (1 / 4) & (1 / 4) + (1 / 4) = 1 / 2 )
by A175, XREAL_1:8;
then
|.(((Sum ((1 / (U |^ (Wk + 1))) * IWW)) * (1 + (T7 * ((5 * k) / M)))) + ((Z * T7) * ((5 * k) / M))).| < 1 / 2
by A173, XXREAL_0:2;
then A202:
( - (1 / 2) <= ((Sum ((1 / (U |^ (Wk + 1))) * IWW)) * (1 + (T7 * ((5 * k) / M)))) + ((Z * T7) * ((5 * k) / M)) & ((Sum ((1 / (U |^ (Wk + 1))) * IWW)) * (1 + (T7 * ((5 * k) / M)))) + ((Z * T7) * ((5 * k) / M)) <= 1 / 2 )
by ABSVALUE:5;
m - Z > ((r / ((S * T) * U)) - (1 / 2)) - Z
by XREAL_1:9, A178, XREAL_1:19;
then
( m - Z > (((Sum ((1 / (U |^ (Wk + 1))) * IWW)) * (1 + (T7 * ((5 * k) / M)))) + ((Z * T7) * ((5 * k) / M))) - (1 / 2) & (((Sum ((1 / (U |^ (Wk + 1))) * IWW)) * (1 + (T7 * ((5 * k) / M)))) + ((Z * T7) * ((5 * k) / M))) - (1 / 2) >= (- (1 / 2)) - (1 / 2) )
by A167, A133, A202, XREAL_1:9;
then
m - Z > - 1
by XXREAL_0:2;
then A203:
m - Z >= (- 1) + 1
by INT_1:7;
m - Z < (r / ((S * T) * U)) - Z
by XREAL_1:9, XREAL_1:47, A118, A22, A15, A10, A7, A8, A9;
then
m - Z <= 1 / 2
by A202, XXREAL_0:2, A167, A133;
then
m - Z < 1 + 0
by XXREAL_0:2;
then A204:
m - Z = 0
by A203, INT_1:7;
A205: (U + 1) / U =
(U / U) + (1 / U)
by XCMPLX_1:62
.=
1 + (I * (1 / U))
by XCMPLX_1:60, A6, A7
;
1 / U <= 1 / (2 * W)
by A80, XREAL_1:118, A1, A6;
then consider T8 being _Theta such that
A206:
(1 + (I * (1 / U))) |^ W = 1 + (((T8 * 2) * W) * (1 / U))
by Th9;
A207: ((U + 1) |^ W) / (U |^ Wk) =
(U |^ k) * (((U + 1) |^ W) / ((U |^ Wk) * (U |^ k)))
by A7, XCMPLX_1:92
.=
(U |^ k) * (((U + 1) |^ W) / (U |^ (Wk + k)))
by NEWTON:8
.=
(U |^ k) * (1 + (((T8 * 2) * W) * (1 / U)))
by A206, A205, PREPOWER:8
;
A208:
|.2.| = 2
;
A209:
(2 * W) / U <= 1
by XREAL_1:183, A80;
then A210:
- ((2 * W) / U) >= - 1
by XREAL_1:24;
( - 1 <= T8 & T8 <= 1 )
by Def1;
then
( (- 1) * ((2 * W) / U) <= T8 * ((2 * W) / U) & T8 * ((2 * W) / U) <= 1 * ((2 * W) / U) )
by XREAL_1:64;
then
( - 1 <= T8 * ((2 * W) / U) & T8 * ((2 * W) / U) <= 1 )
by A209, A210, XXREAL_0:2;
then A211:
( (- 1) + 1 <= (T8 * ((2 * W) / U)) + 1 & (T8 * ((2 * W) / U)) + 1 <= 1 + 1 )
by XREAL_1:6;
A212:
(2 * W) * (1 / U) = (2 * W) / U
by XCMPLX_1:99;
then
|.(1 + (((T8 * 2) * W) * (1 / U))).| = 1 + (((T8 * 2) * W) * (1 / U))
by A211, ABSVALUE:def 1;
then consider T9 being _Theta such that
A213:
T7 * (1 + (((T8 * 2) * W) * (1 / U))) = T9 * 2
by Th2, A208, A211, A212;
A214: ((U |^ k) * (1 + (((T8 * 2) * W) * (1 / U)))) * (T7 * ((5 * k) / M)) =
((U |^ k) * ((1 + (((T8 * 2) * W) * (1 / U))) * T7)) * ((5 * k) / M)
.=
((U |^ k) * (2 * T9)) * ((5 * k) / M)
by A213
.=
T9 * (((U |^ k) * 2) * ((5 * k) / M))
.=
T9 * ((((U |^ k) * 2) * (5 * k)) / M)
by XCMPLX_1:74
;
A215: (1 / (U |^ (Wk + 1))) * U =
(1 / (U * (U |^ Wk))) * U
by NEWTON:6
.=
1 / (U |^ Wk)
by XCMPLX_1:92, A7
;
A216:
(Sum ((1 / (U |^ (Wk + 1))) * IWW)) * U = U * ((1 / (U |^ (Wk + 1))) * (Sum IWW))
by RVSUM_1:87;
IWW <> {}
by A139;
then consider iww being FinSequence of REAL , x being Element of REAL such that
A217:
IWW = <*x*> ^ iww
by FINSEQ_2:130;
1 <= Wk + 1
by NAT_1:11;
then A218: (W choose (k + 0)) * (U |^ (W -' (k + 0))) =
IWW . (0 + 1)
by A159, A138, A134, A137, FINSEQ_3:25
.=
x
by A217
;
reconsider Wk1 = Wk - 1 as Nat by A14;
A219:
len <*x*> = 1
by FINSEQ_1:40;
then
Wk + 1 = 1 + (len iww)
by A217, A138, A134, A137, FINSEQ_1:22;
then A220:
len iww = (W - (k + 1)) + 1
;
for i being Nat st i + 1 in dom iww holds
iww . (i + 1) = (W choose ((k + 1) + i)) * (U |^ (W -' ((k + 1) + i)))
then A222:
( 0 < Sum iww & Sum iww < (2 * (W |^ (k + 1))) * (U |^ (W -' (k + 1))) )
by Th14, A12, A6, A89, A220;
A223: (1 / (U |^ Wk)) * x =
((1 / (U |^ Wk)) * (U |^ Wk)) * (W choose k)
by A218, A165
.=
1 * (W choose k)
by A7, XCMPLX_1:87
;
Sum IWW = x + (Sum iww)
by A217, RVSUM_1:76;
then A224:
(Sum ((1 / (U |^ (Wk + 1))) * IWW)) * U = (W choose k) + ((1 / (U |^ Wk)) * (Sum iww))
by A216, A215, A223;
A225:
( W -' (k + 1) = W - (k + 1) & W - (k + 1) = Wk1 )
by A6, A12, XREAL_1:233;
Wk = Wk1 + 1
;
then A226: (1 / (U |^ Wk)) * (U |^ (W -' (k + 1))) =
(1 / (U * (U |^ Wk1))) * (U |^ Wk1)
by A225, NEWTON:6
.=
1 / U
by XCMPLX_1:92, A7
;
(1 / (U |^ Wk)) * (Sum iww) < (1 / (U |^ Wk)) * ((2 * (W |^ (k + 1))) * (U |^ (W -' (k + 1))))
by A222, XREAL_1:68, A7;
then consider T10 being _Theta such that
A227:
I * ((1 / (U |^ Wk)) * (Sum iww)) = T10 * ((2 * (W |^ (k + 1))) * (1 / U))
by A226, A222, Th5;
A228:
( (Wk + k) choose k >= Wk + 1 & Wk + 1 > Wk )
by NAT_1:14, A1, NAT_1:13, RAMSEY_1:11;
then
W choose k >= 1
by NAT_1:14;
then reconsider T12 = 1 / (W choose k) as _Theta by Def1, XREAL_1:183;
A229:
(W choose k) * T12 = 1
by XCMPLX_1:87, A228;
consider T11 being _Theta such that
A230:
(T10 * ((2 * (W |^ (k + 1))) * (1 / U))) + (T9 * ((((U |^ k) * 10) * k) / M)) = T11 * (((2 * (W |^ (k + 1))) * (1 / U)) + ((((U |^ k) * 10) * k) / M))
by Th6;
(Z + (Sum ((1 / (U |^ (Wk + 1))) * IWW))) * U =
(((U + 1) |^ W) / ((U |^ Wk) * U)) * U
by A167, NEWTON:6
.=
((U + 1) |^ W) / (U |^ Wk)
by XCMPLX_1:92, A7
;
then A231: (r / (S * T)) - (m * U) =
((Sum ((1 / (U |^ (Wk + 1))) * IWW)) * U) + ((((U + 1) |^ W) / (U |^ Wk)) * (T7 * ((5 * k) / M)))
by A204, A132
.=
((W choose k) + (T10 * ((2 * (W |^ (k + 1))) * (1 / U)))) + (T9 * ((((U |^ k) * 10) * k) / M))
by A214, A207, A227, A224
.=
(W choose k) + (T11 * (((2 * (W |^ (k + 1))) * (1 / U)) + ((((U |^ k) * 10) * k) / M)))
by A230
.=
(W choose k) + ((((W choose k) * T12) * T11) * (((2 * (W |^ (k + 1))) * (1 / U)) + ((((U |^ k) * 10) * k) / M)))
by A229
.=
(W choose k) * (1 + ((T12 * T11) * (((2 * (W |^ (k + 1))) * (1 / U)) + ((((U |^ k) * 10) * k) / M))))
;
consider T131 being _Theta such that
A232:
W choose k = ((W |^ k) / (k !)) * (1 + (T131 * ((k ^2) / W)))
by A188, A187, XXREAL_0:2, Th8;
consider T13 being _Theta such that
A233:
1 / (1 + (T131 * ((k ^2) / W))) = 1 + ((T13 * 2) * ((k ^2) / W))
by Th7, A189;
A234: 1 / (((W |^ k) / (k !)) * (1 + (T131 * ((k ^2) / W)))) =
(1 / ((W |^ k) / (k !))) * (1 / (1 + (T131 * ((k ^2) / W))))
by XCMPLX_1:102
.=
((k !) / (W |^ k)) * (1 / (1 + (T131 * ((k ^2) / W))))
by XCMPLX_1:57
;
consider T14 being _Theta such that
A235:
1 / (1 + ((T12 * T11) * (((2 * (W |^ (k + 1))) * (1 / U)) + ((((U |^ k) * 10) * k) / M)))) = 1 + ((T14 * 2) * (((2 * (W |^ (k + 1))) * (1 / U)) + ((((U |^ k) * 10) * k) / M)))
by Th7, A197;
A236:
((k !) / (W |^ k)) * (W |^ k) = k !
by XCMPLX_1:87, A1, A6;
consider T15 being _Theta such that
A237:
(1 + (T14 * (2 * (((2 * (W |^ (k + 1))) * (1 / U)) + ((((U |^ k) * 10) * k) / M))))) * (1 + (T13 * (2 * ((k ^2) / W)))) = 1 + (T15 * ((2 * (((2 * (W |^ (k + 1))) * (1 / U)) + ((((U |^ k) * 10) * k) / M))) + (2 * (2 * ((k ^2) / W)))))
by A200, Th3;
T15 >= - 1
by Def1;
then
( T15 * ((2 * (((2 * (W |^ (k + 1))) * (1 / U)) + ((((U |^ k) * 10) * k) / M))) + (2 * (2 * ((k ^2) / W)))) >= (- 1) * ((2 * (((2 * (W |^ (k + 1))) * (1 / U)) + ((((U |^ k) * 10) * k) / M))) + (2 * (2 * ((k ^2) / W)))) & (- 1) * ((2 * (((2 * (W |^ (k + 1))) * (1 / U)) + ((((U |^ k) * 10) * k) / M))) + (2 * (2 * ((k ^2) / W)))) >= (- 1) * (1 / 2) )
by A199, XREAL_1:64, XREAL_1:65;
then
T15 * ((2 * (((2 * (W |^ (k + 1))) * (1 / U)) + ((((U |^ k) * 10) * k) / M))) + (2 * (2 * ((k ^2) / W)))) >= - (1 / 2)
by XXREAL_0:2;
then
( 1 + (T15 * ((2 * (((2 * (W |^ (k + 1))) * (1 / U)) + ((((U |^ k) * 10) * k) / M))) + (2 * (2 * ((k ^2) / W))))) >= 1 + (- (1 / 2)) & 1 + (- (1 / 2)) = 1 / 2 )
by XREAL_1:6;
then A238:
(k !) * (1 + (T15 * ((2 * (((2 * (W |^ (k + 1))) * (1 / U)) + ((((U |^ k) * 10) * k) / M))) + (2 * (2 * ((k ^2) / W)))))) >= (k !) * (1 / 2)
by XREAL_1:64;
A239: 1 * (u / ((r / (S * T)) - (m * U))) =
((1 / ((r / (S * T)) - (m * U))) * 1) * u
by XCMPLX_1:101
.=
((((k !) / (W |^ k)) * (1 / (1 + (T131 * ((k ^2) / W))))) * (1 + ((T14 * 2) * (((2 * (W |^ (k + 1))) * (1 / U)) + ((((U |^ k) * 10) * k) / M))))) * (W |^ k)
by A117, A232, A234, A235, A231, XCMPLX_1:102
.=
(k !) * ((1 + (T13 * (2 * ((k ^2) / W)))) * (1 + (T14 * (2 * (((2 * (W |^ (k + 1))) * (1 / U)) + ((((U |^ k) * 10) * k) / M))))))
by A236, A233
.=
(k !) * (1 + (T15 * ((2 * (((2 * (W |^ (k + 1))) * (1 / U)) + ((((U |^ k) * 10) * k) / M))) + (2 * (2 * ((k ^2) / W))))))
by A237
;
then A240:
(u / ((r / (S * T)) - (m * U))) - f >= ((k !) * (1 / 2)) - f
by A238, XREAL_1:9;
(1 / 2) ^2 = (1 / 2) * (1 / 2)
by SQUARE_1:def 1;
then
((u / ((r / (S * T)) - (m * U))) - f) ^2 < (1 / 2) ^2
by A25, SQUARE_1:def 1;
then A241:
( - (1 / 2) < (u / ((r / (S * T)) - (m * U))) - f & (u / ((r / (S * T)) - (m * U))) - f < 1 / 2 )
by SQUARE_1:48;
then
((k !) * (1 / 2)) - f < 1 / 2
by A240, XXREAL_0:2;
then
( (((k !) * (1 / 2)) - f) * 2 < (1 / 2) * 2 & (1 / 2) * 2 = 1 )
by XREAL_1:68;
then
( (k !) - (f * 2) = (((k !) * (1 / 2)) * 2) - (f * 2) & (((k !) * (1 / 2)) * 2) - (f * 2) < (1 / 2) * 2 & (1 / 2) * 2 = 1 + 0 )
;
then
(k !) - (f * 2) <= 0
by INT_1:7;
then
((k !) - (f * 2)) + (2 * f) <= 0 + (2 * f)
by XREAL_1:6;
then reconsider T16 = (k !) / (2 * f) as _Theta by Def1, XREAL_1:183;
A242: (2 * f) * ((2 * (((2 * (W |^ (k + 1))) * (1 / U)) + ((((U |^ k) * 10) * k) / M))) + (2 * (2 * ((k ^2) / W)))) =
((((8 * f) * (W |^ (k + 1))) * (1 / U)) + ((4 * f) * ((((U |^ k) * 10) * k) / M))) + ((2 * f) * (2 * (2 * ((k ^2) / W))))
.=
((((8 * f) * (W |^ (k + 1))) / U) + ((4 * f) * ((((U |^ k) * 10) * k) / M))) + ((8 * f) * ((k ^2) / W))
by XCMPLX_1:99
.=
((((8 * f) * (W |^ (k + 1))) / U) + (((4 * f) * (((U |^ k) * 10) * k)) / M)) + ((8 * f) * ((k ^2) / W))
by XCMPLX_1:74
.=
((((8 * f) * (W |^ (k + 1))) / U) + ((((40 * f) * (U |^ k)) * k) / M)) + (((8 * f) * (k ^2)) / W)
by XCMPLX_1:74
;
k ! = T16 * (2 * f)
by XCMPLX_1:87, A1;
then A243: u / ((r / (S * T)) - (m * U)) =
(k !) + ((T15 * T16) * ((2 * f) * ((2 * (((2 * (W |^ (k + 1))) * (1 / U)) + ((((U |^ k) * 10) * k) / M))) + (2 * (2 * ((k ^2) / W))))))
by A239
.=
(k !) + ((T15 * T16) * (((((8 * f) * (W |^ (k + 1))) / U) + ((((40 * f) * (U |^ k)) * k) / M)) + (((8 * f) * (k ^2)) / W)))
by A242
;
6 * (((40 * f) * (U |^ k)) * k) < 1 * M
by A182, A181, XXREAL_0:2;
then A244:
(((40 * f) * (U |^ k)) * k) / M < 1 / 6
by XREAL_1:106;
(((8 * f) * (W |^ (k + 1))) / U) + (((8 * f) * (k ^2)) / W) <= (1 / 12) + (1 / 12)
by A185, A194, XREAL_1:7;
then A245:
((((8 * f) * (W |^ (k + 1))) / U) + (((8 * f) * (k ^2)) / W)) + ((((40 * f) * (U |^ k)) * k) / M) < ((1 / 12) + (1 / 12)) + (1 / 6)
by A244, XREAL_1:8;
( - 1 <= T15 * T16 & T15 * T16 <= 1 )
by Def1;
then
( (1 / 3) * (- 1) < (- 1) * (((((8 * f) * (W |^ (k + 1))) / U) + ((((40 * f) * (U |^ k)) * k) / M)) + (((8 * f) * (k ^2)) / W)) & (- 1) * (((((8 * f) * (W |^ (k + 1))) / U) + ((((40 * f) * (U |^ k)) * k) / M)) + (((8 * f) * (k ^2)) / W)) <= (T15 * T16) * (((((8 * f) * (W |^ (k + 1))) / U) + ((((40 * f) * (U |^ k)) * k) / M)) + (((8 * f) * (k ^2)) / W)) & (T15 * T16) * (((((8 * f) * (W |^ (k + 1))) / U) + ((((40 * f) * (U |^ k)) * k) / M)) + (((8 * f) * (k ^2)) / W)) <= 1 * (((((8 * f) * (W |^ (k + 1))) / U) + ((((40 * f) * (U |^ k)) * k) / M)) + (((8 * f) * (k ^2)) / W)) & 1 * (((((8 * f) * (W |^ (k + 1))) / U) + ((((40 * f) * (U |^ k)) * k) / M)) + (((8 * f) * (k ^2)) / W)) < 1 / 3 )
by A245, XREAL_1:64, XREAL_1:69;
then
( (1 / 3) * (- 1) < (T15 * T16) * (((((8 * f) * (W |^ (k + 1))) / U) + ((((40 * f) * (U |^ k)) * k) / M)) + (((8 * f) * (k ^2)) / W)) & (T15 * T16) * (((((8 * f) * (W |^ (k + 1))) / U) + ((((40 * f) * (U |^ k)) * k) / M)) + (((8 * f) * (k ^2)) / W)) < 1 / 3 )
by XXREAL_0:2;
then
( (- (1 / 3)) + (k !) < u / ((r / (S * T)) - (m * U)) & u / ((r / (S * T)) - (m * U)) < (1 / 3) + (k !) )
by A243, XREAL_1:6;
then
( ((- (1 / 3)) + (k !)) - (1 / 2) < (u / ((r / (S * T)) - (m * U))) - ((u / ((r / (S * T)) - (m * U))) - f) & (u / ((r / (S * T)) - (m * U))) - ((u / ((r / (S * T)) - (m * U))) - f) < ((1 / 3) + (k !)) - (- (1 / 2)) )
by A241, XREAL_1:15;
then
( ((- (5 / 6)) + (k !)) - (k !) < f - (k !) & f - (k !) < ((k !) + (5 / 6)) - (k !) )
by XREAL_1:9;
then
( (- 1) + 0 < f - (k !) & f - (k !) < 1 + 0 )
by XXREAL_0:2;
then
( (- 1) + 1 <= f - (k !) & f - (k !) <= 0 )
by INT_1:7;
then
f - (k !) = 0
;
hence
f = k !
; verum