theorem
for
k being
positive Nat holds
(
k + 1 is
prime iff ex
a,
b,
c,
d,
e,
f,
g,
h,
i,
j,
l,
m,
n,
o,
p,
q,
r,
s,
t,
u,
w,
v,
x,
y,
z being
Nat st
0 = (((((((((((((((((w * z) + h) + j) - q) ^2) + (((((((g * k) + g) + k) * (h + j)) + h) - z) ^2)) + (((((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1) - (f ^2)) ^2)) + (((((p + q) + z) + (2 * n)) - e) ^2)) + ((((((e |^ 3) * (e + 2)) * ((a + 1) |^ 2)) + 1) - (o ^2)) ^2)) + ((((x ^2) - (((a ^2) -' 1) * (y ^2))) - 1) ^2)) + (((((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1) - (u ^2)) ^2)) + (((((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1) - ((x + (c * u)) ^2)) ^2)) + ((((m ^2) - (((a ^2) -' 1) * (l ^2))) - 1) ^2)) + (((k + (i * (a - 1))) - l) ^2)) + ((((n + l) + v) - y) ^2)) + ((((p + (l * ((a - n) - 1))) + (b * ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1))) - m) ^2)) + ((((q + (y * ((a - p) - 1))) + (s * ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1))) - x) ^2)) + ((((z + ((p * l) * (a - p))) + (t * ((((2 * a) * p) - (p ^2)) - 1))) - (p * m)) ^2) )