theorem Th30:
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
(
q = ((w * z) + h) + j &
z = ((((g * k) + g) + k) * (h + j)) + h &
((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1
= f ^2 &
e = ((p + q) + z) + (2 * n) &
(((e |^ 3) * (e + 2)) * ((a + 1) |^ 2)) + 1
= o ^2 &
[x,y] is
Pell's_solution of
(a ^2) -' 1 &
u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1 &
(x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1 &
[m,l] is
Pell's_solution of
(a ^2) -' 1 &
l = k + (i * (a - 1)) &
(n + l) + v = y &
m = (p + (l * ((a - n) - 1))) + (b * ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1)) &
x = (q + (y * ((a - p) - 1))) + (s * ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1)) &
p * m = (z + ((p * l) * (a - p))) + (t * ((((2 * a) * p) - (p ^2)) - 1)) ) )