let k be 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, L, W, U, M, S, T, Q being Integer st
( (D * F) * I is square & (((M ^2) - 1) * (S ^2)) + 1 is square & ((((M * U) ^2) - 1) * (T ^2)) + 1 is square & (((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)) & F * L divides (((H - C) * L) + ((F * (f + 1)) * Q)) + ((F * (k + 1)) * ((((((W ^2) - 1) * S) * u) - ((W ^2) * (u ^2))) + 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 & L = (k + 1) * Q & 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 ( ((((k + 1) -' 1) !) + 1) mod (k + 1) = 0 & k + 1 > 1 ) by NAT_5:22;
then A3: k + 1 divides (k !) + 1 by INT_1:62, A2;
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 and
A7: ((((M * U) ^2) - 1) * (T ^2)) + 1 is square and
A8: (((W ^2) * (u ^2)) - ((((W ^2) - 1) * S) * u)) - 1, 0 are_congruent_mod Q and
A9: (((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
A10: W = ((100 * (k !)) * k) * (k + 1) and
A11: U = ((100 * (u |^ 3)) * (W |^ 3)) + 1 and
A12: M = (((100 * m) * U) * W) + 1 and
A13: S = (((M - 1) * s) + k) + 1 and
A14: T = (((((M * U) - 1) * t) + W) - k) + 1 and
A15: Q = (((2 * M) * W) - (W ^2)) - 1 by Th16, A1;
A16: ((100 * (k !)) * k) * (k + 1) >= 1 * (k + 1) by A1, NAT_1:14, XREAL_1:64;
A17: W > k by A16, A10, NAT_1:13;
reconsider Wk = W - k as Nat by A17, NAT_1:21;
A18: (M * W) - 1 >= 0 + 1 by INT_1:7, A1, A10;
((100 * m) * U) * W >= 1 * W by XREAL_1:64, A4, A11, NAT_1:14;
then M > W by A12, NAT_1:13;
then ( M * W > W * W & W * W = W ^2 ) by A10, A1, XREAL_1:68, SQUARE_1:def 1;
then (M * W) + (M * W) > (M * W) + (W ^2) by XREAL_1:8;
then ((M * W) + (M * W)) - ((W ^2) + 1) > ((M * W) + (W ^2)) - ((W ^2) + 1) by XREAL_1:9;
then reconsider Q = Q as positive Nat by A15, A18;
set L = (k + 1) * Q;
reconsider L = (k + 1) * Q as positive Nat ;
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
A19: ( (D * F) * I is square & F divides H - ((r + W) + 1) & W + 1 <= (r + W) + 1 ) and
A20: ( 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;
A21: 1,1 are_congruent_mod k + 1 by INT_1:11;
A22: 2 * M,2 * M are_congruent_mod k + 1 by INT_1:11;
W - 0 = ((100 * (k !)) * k) * (k + 1) by A10;
then W, 0 are_congruent_mod k + 1 by INT_1:def 3, INT_1:def 4;
then ( W * W,0 * 0 are_congruent_mod k + 1 & W * (2 * M),0 * (2 * M) are_congruent_mod k + 1 ) by A22, INT_1:18;
then ((2 * M) * W) - (W * W),0 - 0 are_congruent_mod k + 1 by INT_1:17;
then (((2 * M) * W) - (W * W)) - 1,(0 - 0) - 1 are_congruent_mod k + 1 by A21, INT_1:17;
then Q, - 1 are_congruent_mod k + 1 by A15, SQUARE_1:def 1;
then Q gcd (k + 1) = (- 1) gcd (k + 1) by WSIERP_1:43;
then ( Q gcd (k + 1) = 1 gcd (k + 1) & 1 gcd (k + 1) = 1 ) by NEWTON02:1, WSIERP_1:8;
then A23: Q,k + 1 are_coprime by INT_2:def 3;
Q divides - (((((W ^2) * (u ^2)) - ((((W ^2) - 1) * S) * u)) - 1) - 0) by INT_2:10, A8, INT_1:def 4;
then A24: L divides (Q * ((k !) + 1)) + ((k + 1) * ((((((W ^2) - 1) * S) * u) - ((W ^2) * (u ^2))) + 1)) by Th22, A3, A23;
A25: (((M * (U + 1)) ^2) - 1) * E,(((M * (U + 1)) ^2) - 1) * E are_congruent_mod L by INT_1:11;
A26: 1,1 are_congruent_mod L by INT_1:11;
E - 0 = (((2 * i) * (((r + W) + 1) ^2)) * D) * L by A20;
then E, 0 are_congruent_mod L by INT_1:def 3, INT_1:def 4;
then ((((M * (U + 1)) ^2) - 1) * E) * E,((((M * (U + 1)) ^2) - 1) * E) * 0 are_congruent_mod L by A25, INT_1:18;
then ((((M * (U + 1)) ^2) - 1) * (E * E)) + 1,0 + 1 are_congruent_mod L by A26, INT_1:16;
then ((((M * (U + 1)) ^2) - 1) * (E ^2)) + 1,0 + 1 are_congruent_mod L by SQUARE_1:def 1;
then ( F gcd L = 1 gcd L & 1 gcd L = 1 ) by A20, WSIERP_1:8, WSIERP_1:43;
then F,L are_coprime by INT_2:def 3;
then A27: F * L divides (((Q * ((k !) + 1)) + ((k + 1) * ((((((W ^2) - 1) * S) * u) - ((W ^2) * (u ^2))) + 1))) * F) + ((H - ((r + W) + 1)) * L) by Th22, A19, A24;
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 L ; :: 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 & (((M ^2) - 1) * (S ^2)) + 1 is square & ((((M * U) ^2) - 1) * (T ^2)) + 1 is square ) by A19, A6, A7; :: thesis:
thus ( (((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)) & F * L divides (((H - ((r + W) + 1)) * L) + ((F * ((k !) + 1)) * Q)) + ((F * (k + 1)) * ((((((W ^2) - 1) * S) * u) - ((W ^2) * (u ^2))) + 1)) ) by A9, A27; :: 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 ) by A20; :: thesis:
thus ( L = (k + 1) * Q & 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 A10, A11, A12, A13, A14, A15; :: 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, L, W, U, M, S, T, Q being Integer such that A28: (D * F) * I is square and
A29: (((M ^2) - 1) * (S ^2)) + 1 is square and
A30: ((((M * U) ^2) - 1) * (T ^2)) + 1 is square and
A31: (((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
A32: F * L divides (((H - C) * L) + ((F * (f + 1)) * Q)) + ((F * (k + 1)) * ((((((W ^2) - 1) * S) * u) - ((W ^2) * (u ^2))) + 1)) and
A33: A = M * (U + 1) and
A34: B = W + 1 and
A35: C = (r + W) + 1 and
A36: D = (((A ^2) - 1) * (C ^2)) + 1 and
A37: ( 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
A38: L = (k + 1) * Q and
A39: W = ((100 * f) * k) * (k + 1) and
A40: U = ((100 * (u |^ 3)) * (W |^ 3)) + 1 and
A41: M = (((100 * m) * U) * W) + 1 and
A42: S = (((M - 1) * s) + k) + 1 and
A43: T = (((((M * U) - 1) * t) + W) - k) + 1 and
A44: Q = (((2 * M) * W) - (W ^2)) - 1 ; :: thesis:
A45: r + (W + 1) >= (W + 1) + 0 by XREAL_1:6;
reconsider W = W, U = U, M = M, S = S as Element of NAT by A39, A40, A41, A42, INT_1:3;
A46: ((100 * f) * k) * (k + 1) >= 1 * (k + 1) by A1, NAT_1:14, XREAL_1:64;
A47: W > k by A46, A39, NAT_1:13;
then W - k > 0 by XREAL_1:50;
then (((M * U) - 1) * t) + (W - k) >= 0 + 0 by A40, A41;
then reconsider T = T as Element of NAT by A43, INT_1:3;
reconsider Wk = W - k as Nat by A47, NAT_1:21;
A48: (M * W) - 1 >= 0 + 1 by INT_1:7, A1, A39, A40, A41;
((100 * m) * U) * W >= 1 * W by XREAL_1:64, A40, NAT_1:14;
then A49: M > W by A41, NAT_1:13;
then ( M * W > W * W & W * W = W ^2 ) by A1, A39, XREAL_1:68, SQUARE_1:def 1;
then (M * W) + (M * W) > (M * W) + (W ^2) by XREAL_1:8;
then ((M * W) + (M * W)) - ((W ^2) + 1) > ((M * W) + (W ^2)) - ((W ^2) + 1) by XREAL_1:9;
then reconsider Q = Q as positive Nat by A44, A48;
( M >= 1 & U + 1 > 1 ) by A39, A40, A41, 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, A39, NAT_1:14;
then M > 1 by A49, 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 A33;
W + 1 > 0 ;
then reconsider B = B as positive Nat by A34;
(r + W) + 1 is Nat ;
then reconsider C = C as Nat by A35;
A50: 1,1 are_congruent_mod k + 1 by INT_1:11;
A51: 2 * M,2 * M are_congruent_mod k + 1 by INT_1:11;
W - 0 = ((100 * f) * k) * (k + 1) by A39;
then W, 0 are_congruent_mod k + 1 by INT_1:def 3, INT_1:def 4;
then ( W * W,0 * 0 are_congruent_mod k + 1 & W * (2 * M),0 * (2 * M) are_congruent_mod k + 1 ) by A51, INT_1:18;
then ((2 * M) * W) - (W * W),0 - 0 are_congruent_mod k + 1 by INT_1:17;
then (((2 * M) * W) - (W * W)) - 1,(0 - 0) - 1 are_congruent_mod k + 1 by A50, INT_1:17;
then Q, - 1 are_congruent_mod k + 1 by A44, SQUARE_1:def 1;
then Q gcd (k + 1) = (- 1) gcd (k + 1) by WSIERP_1:43;
then ( Q gcd (k + 1) = 1 gcd (k + 1) & 1 gcd (k + 1) = 1 ) by NEWTON02:1, WSIERP_1:8;
then A52: Q,k + 1 are_coprime by INT_2:def 3;
A53: ((A ^2) - 1) * E,((A ^2) - 1) * E are_congruent_mod L by INT_1:11;
A54: 1,1 are_congruent_mod L by INT_1:11;
E - 0 = (((2 * i) * (C ^2)) * D) * L by A37;
then E, 0 are_congruent_mod L by INT_1:def 3, INT_1:def 4;
then (((A ^2) - 1) * E) * E,(((A ^2) - 1) * E) * 0 are_congruent_mod L by A53, INT_1:18;
then (((A ^2) - 1) * (E * E)) + 1,0 + 1 are_congruent_mod L by A54, INT_1:16;
then (((A ^2) - 1) * (E ^2)) + 1,0 + 1 are_congruent_mod L by SQUARE_1:def 1;
then ( F gcd L = 1 gcd L & 1 gcd L = 1 ) by A37, WSIERP_1:8, WSIERP_1:43;
then A55: F,L are_coprime by INT_2:def 3;
F * L divides ((H - C) * L) + (F * (((f + 1) * Q) + ((k + 1) * ((((((W ^2) - 1) * S) * u) - ((W ^2) * (u ^2))) + 1)))) by A32;
then A56: ( F divides H - C & Q * (k + 1) divides ((f + 1) * Q) + ((k + 1) * ((((((W ^2) - 1) * S) * u) - ((W ^2) * (u ^2))) + 1)) ) by A38, A55, Th22;
then A57: ( Q divides (((((W ^2) - 1) * S) * u) - ((W ^2) * (u ^2))) + 1 & k + 1 divides f + 1 ) by A52, Th22;
then Q divides - ((((((W ^2) - 1) * S) * u) - ((W ^2) * (u ^2))) + 1) by INT_2:10;
then Q divides ((((W ^2) * (u ^2)) - ((((W ^2) - 1) * S) * u)) - 1) - 0 ;
then A58: (((W ^2) * (u ^2)) - ((((W ^2) - 1) * S) * u)) - 1, 0 are_congruent_mod Q by INT_1:def 4;
A59: k + 1 > 0 + 1 by A1, XREAL_1:6;
C = Py (A,B) by A38, A45, A34, A35, A28, A56, A36, A37, Th20;
then f = k ! by A1, A29, A30, A58, A31, A39, A40, A41, A42, A43, A44, Th15, A33, A34, A35;
then ((((k + 1) -' 1) !) + 1) mod (k + 1) = 0 by A57, INT_1:62, A2;
hence k + 1 is prime by A59, NAT_5:22; :: thesis: