theorem
for
k being
Nat for
L being
positive Nat st
k > 0 holds
(
k + 1 is
prime iff ex
f,
i,
j,
m,
u being
positive Nat ex
r,
s,
t being
Nat ex
A,
B,
C,
D,
E,
F,
G,
H,
I,
W,
U,
M,
S,
T,
Q being
Integer st
(
(D * F) * I is
square &
F divides H - C &
(((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)) &
k + 1
divides f + 1 &
A = M * (U + 1) &
B = W + 1 &
C = (r + W) + 1 &
D = (((A ^2) - 1) * (C ^2)) + 1 &
E = (((2 * i) * (C ^2)) * L) * D &
F = (((A ^2) - 1) * (E ^2)) + 1 &
G = A + (F * (F - A)) &
H = B + ((2 * (j - 1)) * C) &
I = (((G ^2) - 1) * (H ^2)) + 1 &
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 ) )