theorem Th16: :: HILB10_8:16

for f, k being Nat st f = k ! & k > 0 holds
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 )