theorem Th15:
for
f,
k,
m,
r,
s,
t,
u being
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 ! ) )