let k be Nat; :: thesis:
let L be positive Nat; :: thesis:
assume A1: k > 0 ; :: thesis:
A2: (k + 1) -' 1 = (k + 1) - 1 by XREAL_1:233, NAT_1:11;
thus ( k + 1 is prime implies 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 ) ) :: thesis:

assume k + 1 is prime ; :: thesis:
then A3: ( ((((k + 1) -' 1) !) + 1) mod (k + 1) = 0 & k + 1 > 1 ) by NAT_5:22;
set f = k ! ;
consider m, r, s, t, u, W, U, S, T, Q being Nat, M being non trivial Nat such that
A4: ( m > 0 & u > 0 ) and
A5: (r + W) + 1 = Py ((M * (U + 1)),(W + 1)) and
A6: ( (((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 * ((k !) ^2)) - 1) * ((r - (((m * S) * T) * U)) ^2)) + (((4 * (u ^2)) * (S ^2)) * (T ^2)) < ((((8 * (k !)) * u) * S) * T) * (r - (((m * S) * T) * U)) ) and
A7: ( W = ((100 * (k !)) * 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 ) by Th16, A1;
set C = (r + W) + 1;
set B = W + 1;
set A = M * (U + 1);
consider i, j being positive Nat, D, E, F, G, H, I being Integer such that
A8: ( (D * F) * I is square & F divides H - ((r + W) + 1) & W + 1 <= (r + W) + 1 ) and
A9: ( D = ((((M * (U + 1)) ^2) - 1) * (((r + W) + 1) ^2)) + 1 & E = (((2 * i) * (((r + W) + 1) ^2)) * L) * D & F = ((((M * (U + 1)) ^2) - 1) * (E ^2)) + 1 & G = (M * (U + 1)) + (F * (F - (M * (U + 1)))) & H = (W + 1) + ((2 * (j - 1)) * ((r + W) + 1)) & I = (((G ^2) - 1) * (H ^2)) + 1 ) by A5, Th20;
reconsider m = m, u = u as positive Nat by A4;
take k ! ; :: thesis:
take i ; :: thesis:
take j ; :: thesis:
take m ; :: thesis:
take u ; :: thesis:
take r ; :: thesis:
take s ; :: thesis:
take t ; :: thesis:
take M * (U + 1) ; :: thesis:
take W + 1 ; :: thesis:
take (r + W) + 1 ; :: thesis:
take D ; :: thesis:
take E ; :: thesis:
take F ; :: thesis:
take G ; :: thesis:
take H ; :: thesis:
take I ; :: thesis:
take W ; :: thesis:
take U ; :: thesis:
take M ; :: thesis:
take S ; :: thesis:
take T ; :: thesis:
take Q ; :: thesis:
thus ( (D * F) * I is square & F divides H - ((r + W) + 1) ) by A8; :: thesis:
thus ( (((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 * ((k !) ^2)) - 1) * ((r - (((m * S) * T) * U)) ^2)) + (((4 * (u ^2)) * (S ^2)) * (T ^2)) < ((((8 * (k !)) * u) * S) * T) * (r - (((m * S) * T) * U)) & k + 1 divides (k !) + 1 ) by A3, A6, INT_1:62, A2; :: thesis:
thus ( M * (U + 1) = M * (U + 1) & W + 1 = W + 1 & (r + W) + 1 = (r + W) + 1 & D = ((((M * (U + 1)) ^2) - 1) * (((r + W) + 1) ^2)) + 1 & E = (((2 * i) * (((r + W) + 1) ^2)) * L) * D & F = ((((M * (U + 1)) ^2) - 1) * (E ^2)) + 1 & G = (M * (U + 1)) + (F * (F - (M * (U + 1)))) & H = (W + 1) + ((2 * (j - 1)) * ((r + W) + 1)) & I = (((G ^2) - 1) * (H ^2)) + 1 & W = ((100 * (k !)) * 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 ) by A9, A7; :: thesis:

end;

given f, i, j, m, u being positive Nat, r, s, t being Nat, A, B, C, D, E, F, G, H, I, W, U, M, S, T, Q being Integer such that A10: (D * F) * I is square and
A11: F divides H - C and
A12: (((M ^2) - 1) * (S ^2)) + 1 is square and
A13: ((((M * U) ^2) - 1) * (T ^2)) + 1 is square and
A14: (((W ^2) * (u ^2)) - ((((W ^2) - 1) * S) * u)) - 1, 0 are_congruent_mod Q and
A15: (((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)) and
A16: k + 1 divides f + 1 and
A17: A = M * (U + 1) and
A18: B = W + 1 and
A19: C = (r + W) + 1 and
A20: D = (((A ^2) - 1) * (C ^2)) + 1 and
A21: ( 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 ) and
A22: W = ((100 * f) * k) * (k + 1) and
A23: U = ((100 * (u |^ 3)) * (W |^ 3)) + 1 and
A24: M = (((100 * m) * U) * W) + 1 and
A25: S = (((M - 1) * s) + k) + 1 and
A26: T = (((((M * U) - 1) * t) + W) - k) + 1 and
A27: Q = (((2 * M) * W) - (W ^2)) - 1 ; :: thesis:
A28: r + (W + 1) >= (W + 1) + 0 by XREAL_1:6;
reconsider W = W, U = U, M = M, S = S as Element of NAT by A22, A23, A24, A25, INT_1:3;
A29: ((100 * f) * k) * (k + 1) >= 1 * (k + 1) by A1, NAT_1:14, XREAL_1:64;
A30: W > k by A29, A22, NAT_1:13;
then W - k > 0 by XREAL_1:50;
then (((M * U) - 1) * t) + (W - k) >= 0 + 0 by A23, A24;
then reconsider T = T as Element of NAT by A26, INT_1:3;
reconsider Wk = W - k as Nat by A30, NAT_1:21;
A31: (M * W) - 1 >= 0 by A1, A22, A23, A24;
((100 * m) * U) * W >= 1 * W by XREAL_1:64, A23, NAT_1:14;
then A32: M > W by A24, NAT_1:13;
then ( M * W >= W * W & W * W = W ^2 ) by XREAL_1:64, SQUARE_1:def 1;
then (M * W) + (M * W) >= (M * W) + (W ^2) by XREAL_1:7;
then ((M * W) + (M * W)) - ((W ^2) + 1) >= ((M * W) + (W ^2)) - ((W ^2) + 1) by XREAL_1:9;
then reconsider Q = Q as Element of NAT by A31, A27, INT_1:3;
( M >= 1 & U + 1 > 1 ) by A22, A23, A24, NAT_1:14, NAT_1:13;
then M * (U + 1) > 1 * 1 by XREAL_1:97;
then reconsider mu1 = M * (U + 1) as non trivial Nat by NEWTON03:def 1;
W >= 1 by A1, A22, NAT_1:14;
then M > 1 by A32, XXREAL_0:2;
then reconsider M = M as non trivial Nat by NEWTON03:def 1;
M * (U + 1) is non trivial Nat ;
then reconsider A = A as non trivial Nat by A17;
W + 1 > 0 ;
then reconsider B = B as positive Nat by A18;
(r + W) + 1 is Nat ;
then reconsider C = C as Nat by A19;
A33: k + 1 > 0 + 1 by A1, XREAL_1:6;
C = Py (A,B) by A28, A18, A19, A10, A11, A20, A21, Th20;
then f = k ! by A1, A12, A13, A14, A15, A22, A23, A24, A25, A26, A27, Th15, A17, A18, A19;
then ((((k + 1) -' 1) !) + 1) mod (k + 1) = 0 by A16, INT_1:62, A2;
hence k + 1 is prime by A33, NAT_5:22; :: thesis: