let k be positive Nat; :: thesis: ( 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)) ) )
thus ( k + 1 is prime implies 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)) ) ) :: thesis: ( 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)) ) implies k + 1 is prime )

proof

A1: (k + 1) -' 1 = (k + 1) - 1 by NAT_1:11, XREAL_1:233;
assume k + 1 is prime ; :: thesis: 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)) )
then ((k !) + 1) mod (k + 1) = 0 by A1, NAT_5:22;
then k + 1 divides (k !) + 1 by INT_1:62;
then consider g1 being Nat such that
A2: (k !) + 1 = (k + 1) * g1 by NAT_D:def 3;
g1 <> 0 by A2;
then reconsider g = g1 - 1 as Nat ;
(k !) + 1 = (k + 1) * (g + 1) by A2;
then consider j, h, w being Nat, n, p, q, z being positive Nat such that
A3: q = ((w * z) + h) + j and
A4: z = ((((g * k) + g) + k) * (h + j)) + h and
A5: ((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 is square and
A6: ( p = (n + 1) |^ k & q = (p + 1) |^ n & z = p |^ (k + 1) ) by Th29;
consider f being Nat such that
A7: ((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 = f ^2 by A5, PYTHTRIP:def 3;
set e = ((p + q) + z) + (2 * n);
( p >= 1 & q >= 1 ) by NAT_1:14;
then p + q >= 1 + 1 by XREAL_1:7;
then (p + q) + z >= 2 + 0 by XREAL_1:7;
then A8: ((p + q) + z) + (2 * n) >= 2 + 0 by XREAL_1:7;
then consider a, o being Nat such that
A9: ( 10 divides a + 1 & ((((((p + q) + z) + (2 * n)) ^2) * ((((p + q) + z) + (2 * n)) * ((((p + q) + z) + (2 * n)) + 2))) * ((a + 1) ^2)) + 1 = o ^2 ) by Th6;
( 9 + 1 = 10 & 10 <= a + 1 ) by A9, INT_2:27;
then A10: 9 <= a by XREAL_1:6;
then A11: a >= 1 + 1 by XXREAL_0:2;
a > 1 by A10, XXREAL_0:2;
then reconsider a = a as non trivial Nat by NEWTON03:def 1;
A12: ((((p + q) + z) + (2 * n)) - 1) + ((((p + q) + z) + (2 * n)) |^ ((((p + q) + z) + (2 * n)) -' 2)) > (((p + q) + z) + (2 * n)) - 1 by XREAL_1:29;
((((p + q) + z) + (2 * n)) - 1) + ((((p + q) + z) + (2 * n)) |^ ((((p + q) + z) + (2 * n)) -' 2)) <= a by A9, A8, Th5;
then (((p + q) + z) + (2 * n)) - 1 < a by A12, XXREAL_0:2;
then A13: ((((p + q) + z) + (2 * n)) - 1) + 1 <= a by INT_1:7;
( (((p + q) + z) + (2 * n)) ^2 = (((p + q) + z) + (2 * n)) |^ 2 & (a + 1) |^ 2 = (a + 1) ^2 ) by NEWTON:81;
then A14: ((((p + q) + z) + (2 * n)) ^2) * (((p + q) + z) + (2 * n)) = (((p + q) + z) + (2 * n)) |^ (2 + 1) by NEWTON:6;
set y = Py (a,n);
1 <= n by NAT_1:14;
then consider c, d, r, u, x being Nat such that
A15: [x,(Py (a,n))] is Pell's_solution of (a ^2) -' 1 and
A16: u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * ((Py (a,n)) ^2)) * ((Py (a,n)) ^2)) + 1 and
A17: (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * (Py (a,n)))) ^2)) + 1 and
n <= Py (a,n) by Th28;
set m = Px (a,k);
set l = Py (a,k);
A18: ((Px (a,k)) ^2) - (((a ^2) -' 1) * ((Py (a,k)) ^2)) = 1 by HILB10_1:7;
consider i being Integer such that
A19: (a - 1) * i = (Py (a,k)) - k by INT_1:def 5, HILB10_1:24;
i >= 0 by A19, NAT_1:21, HILB10_1:13;
then reconsider i = i as Element of NAT by INT_1:3;
reconsider n1 = n - 1 as Element of NAT by NAT_1:14, NAT_1:21;
A20: ( n -' 1 = n - 1 & n - 1 = n1 ) by NAT_1:14, XREAL_1:233;
A21: Px (a,n1) >= 1 by NAT_1:14;
A22: (Py (a,n1)) + (Py (a,n1)) >= (Py (a,n1)) + n1 by HILB10_1:13, XREAL_1:6;
(Py (a,n1)) * a >= (Py (a,n1)) * 2 by A11, XREAL_1:64;
then (Py (a,n1)) * a >= (Py (a,n1)) + n1 by A22, XXREAL_0:2;
then (Px (a,n1)) + ((Py (a,n1)) * a) >= 1 + ((Py (a,n1)) + n1) by A21, XREAL_1:7;
then A23: Py (a,(n1 + 1)) >= 1 + ((Py (a,n1)) + n1) by HILB10_1:6;
A24: k >= 1 by NAT_1:14;
A25: 2 * k >= 2 * 1 by NAT_1:14, XREAL_1:64;
( (2 * k) ^2 = (2 * k) |^ 2 & (n + 1) |^ 2 = (n + 1) ^2 ) by NEWTON:81;
then ((2 * k) ^2) * (2 * k) = (2 * k) |^ (2 + 1) by NEWTON:6;
then ((((2 * k) ^2) * ((2 * k) * ((2 * k) + 2))) * ((n + 1) ^2)) + 1 = f ^2 by NEWTON:81, A7;
then A26: ((2 * k) - 1) + ((2 * k) |^ ((2 * k) -' 2)) <= n by A25, Th5;
((2 * k) - 1) + ((2 * k) |^ ((2 * k) -' 2)) > (2 * k) - 1 by XREAL_1:29;
then (2 * k) - 1 < n by A26, XXREAL_0:2;
then ((2 * k) - 1) + 1 <= n by INT_1:7;
then ( 1 + k <= k + k & k + k <= n ) by A24, XREAL_1:7;
then 1 + k <= n by XXREAL_0:2;
then k <= n -' 1 by A20, XREAL_1:19;
then ( k = n -' 1 or k < n -' 1 ) by XXREAL_0:1;
then ( Py (a,k) = Py (a,(n -' 1)) or Py (a,k) < Py (a,(n -' 1)) ) by HILB10_1:11;
then (Py (a,k)) + n <= (Py (a,(n -' 1))) + n by XREAL_1:6;
then (Py (a,n)) - (n + (Py (a,k))) is Element of NAT by NAT_1:21, A23, A20, XXREAL_0:2;
then consider v being Nat such that
A27: v = (Py (a,n)) - (n + (Py (a,k))) ;
A28: ( 2 * n = n + n & n + n >= n + 1 & n + 1 >= 1 + 1 ) by XREAL_1:6, NAT_1:14;
then 2 * n >= 1 + 1 by XXREAL_0:2;
then 2 * n > 1 by NAT_1:13;
then ( ((p + q) + z) + (2 * n) > ((p + q) + z) + 1 & (p + q) + (z + 1) > z + 1 & (z + q) + (p + 1) > p + 1 & (p + z) + (q + 1) > q + 1 & ((p + q) + z) + (2 * n) > 2 * n ) by XREAL_1:29, XREAL_1:6;
then ( ((p + q) + z) + (2 * n) > z + 1 & ((p + q) + z) + (2 * n) > p + 1 & ((p + q) + z) + (2 * n) > q + 1 & ((p + q) + z) + (2 * n) > n + 1 ) by A28, XXREAL_0:2;
then A29: ( a > z + 1 & a > p + 1 & a > q + 1 & a > n + 1 ) by A13, XXREAL_0:2;
then A30: ( a > z & a > p & a > q & a > n + 1 ) by NAT_1:13;
A31: ( (n + 1) |^ k < a & (p + 1) |^ n < a & p |^ (k + 1) < a ) by A29, NAT_1:13, A6;
consider b being Integer such that
A32: ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1) * b = (Px (a,k)) - (p + ((Py (a,k)) * (a - (n + 1)))) by INT_1:def 5, A6, Th13;
A33: ( a * (n + 1) > (n + 1) * (n + 1) & (n + 1) * (n + 1) = (n + 1) ^2 ) by A29, XREAL_1:68, SQUARE_1:def 1;
(a * (n + 1)) + (a * (n + 1)) > ((n + 1) ^2) + 1 by NAT_1:14, A33, XREAL_1:8;
then A34: ((2 * a) * (n + 1)) - (((n + 1) ^2) + 1) > 0 by XREAL_1:50;
p + ((Py (a,k)) * (a - (n + 1))) <= Px (a,k) by A31, Th14, A6;
then b >= 0 by A32, A34, XREAL_1:48;
then reconsider b = b as Element of NAT by INT_1:3;
consider s being Integer such that
A35: ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1) * s = (Px (a,n)) - (q + ((Py (a,n)) * (a - (p + 1)))) by INT_1:def 5, A6, Th13;
( a * (p + 1) > (p + 1) * (p + 1) & (p + 1) * (p + 1) = (p + 1) ^2 ) by SQUARE_1:def 1, A29, XREAL_1:68;
then (a * (p + 1)) + (a * (p + 1)) > ((p + 1) ^2) + 1 by XREAL_1:8, NAT_1:14;
then A36: ((2 * a) * (p + 1)) - (((p + 1) ^2) + 1) > 0 by XREAL_1:50;
consider n2 being Nat such that
A37: ( x = Px (a,n2) & Py (a,n) = Py (a,n2) ) by A15, HILB10_1:4;
q + ((Py (a,n)) * (a - (p + 1))) <= Px (a,n) by Th14, A31, A6;
then s >= 0 by A35, A36, XREAL_1:48;
then reconsider s = s as Element of NAT by INT_1:3;
consider t1 being Integer such that
A38: ((((2 * a) * p) - (p ^2)) - 1) * t1 = (Px (a,k)) - ((p |^ k) + ((Py (a,k)) * (a - p))) by Th13, INT_1:def 5;
a > p by A29, NAT_1:13;
then ( a * p > p * p & p * p = p ^2 ) by SQUARE_1:def 1, XREAL_1:68;
then (a * p) + (a * p) > (p ^2) + 1 by XREAL_1:8, NAT_1:14;
then A39: ((2 * a) * p) - ((p ^2) + 1) > 0 by XREAL_1:50;
A40: ( z = (p |^ k) * p & p >= 1 ) by NAT_1:14, NEWTON:6, A6;
( a > (p |^ k) * p & (p |^ k) * p >= (p |^ k) * 1 ) by A30, XREAL_1:64, NAT_1:14, NEWTON:6, A6;
then ( a > p |^ k & p |^ k > 0 ) by XXREAL_0:2;
then Px (a,k) >= (p |^ k) + ((Py (a,k)) * (a - p)) by Th14;
then t1 >= 0 by A39, A38, XREAL_1:48;
then reconsider t1 = t1 as Element of NAT by INT_1:3;
set t = t1 * p;
A41: (((((2 * a) * p) - (p ^2)) - 1) * t1) * p = ((Px (a,k)) - ((p |^ k) + ((Py (a,k)) * (a - p)))) * p by A38;
take a ; :: thesis: ex 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)) )
take b ; :: thesis: ex 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)) )
take c ; :: thesis: ex 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)) )
take d ; :: thesis: ex 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)) )
take ((p + q) + z) + (2 * n) ; :: thesis: ex 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 & ((p + q) + z) + (2 * n) = ((p + q) + z) + (2 * n) & ((((((p + q) + z) + (2 * n)) |^ 3) * ((((p + q) + z) + (2 * n)) + 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)) )
take f ; :: thesis: ex 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 & ((p + q) + z) + (2 * n) = ((p + q) + z) + (2 * n) & ((((((p + q) + z) + (2 * n)) |^ 3) * ((((p + q) + z) + (2 * n)) + 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)) )
take g ; :: thesis: ex 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 & ((p + q) + z) + (2 * n) = ((p + q) + z) + (2 * n) & ((((((p + q) + z) + (2 * n)) |^ 3) * ((((p + q) + z) + (2 * n)) + 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)) )
take h ; :: thesis: ex 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 & ((p + q) + z) + (2 * n) = ((p + q) + z) + (2 * n) & ((((((p + q) + z) + (2 * n)) |^ 3) * ((((p + q) + z) + (2 * n)) + 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)) )
take i ; :: thesis: ex 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 & ((p + q) + z) + (2 * n) = ((p + q) + z) + (2 * n) & ((((((p + q) + z) + (2 * n)) |^ 3) * ((((p + q) + z) + (2 * n)) + 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)) )
take j ; :: thesis: ex 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 & ((p + q) + z) + (2 * n) = ((p + q) + z) + (2 * n) & ((((((p + q) + z) + (2 * n)) |^ 3) * ((((p + q) + z) + (2 * n)) + 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)) )
take Py (a,k) ; :: thesis: ex 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 & ((p + q) + z) + (2 * n) = ((p + q) + z) + (2 * n) & ((((((p + q) + z) + (2 * n)) |^ 3) * ((((p + q) + z) + (2 * n)) + 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,(Py (a,k))] is Pell's_solution of (a ^2) -' 1 & Py (a,k) = k + (i * (a - 1)) & (n + (Py (a,k))) + v = y & m = (p + ((Py (a,k)) * ((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 * (Py (a,k))) * (a - p))) + (t * ((((2 * a) * p) - (p ^2)) - 1)) )
take Px (a,k) ; :: thesis: ex 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 & ((p + q) + z) + (2 * n) = ((p + q) + z) + (2 * n) & ((((((p + q) + z) + (2 * n)) |^ 3) * ((((p + q) + z) + (2 * n)) + 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 & [(Px (a,k)),(Py (a,k))] is Pell's_solution of (a ^2) -' 1 & Py (a,k) = k + (i * (a - 1)) & (n + (Py (a,k))) + v = y & Px (a,k) = (p + ((Py (a,k)) * ((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 * (Px (a,k)) = (z + ((p * (Py (a,k))) * (a - p))) + (t * ((((2 * a) * p) - (p ^2)) - 1)) )
take n ; :: thesis: ex 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 & ((p + q) + z) + (2 * n) = ((p + q) + z) + (2 * n) & ((((((p + q) + z) + (2 * n)) |^ 3) * ((((p + q) + z) + (2 * n)) + 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 & [(Px (a,k)),(Py (a,k))] is Pell's_solution of (a ^2) -' 1 & Py (a,k) = k + (i * (a - 1)) & (n + (Py (a,k))) + v = y & Px (a,k) = (p + ((Py (a,k)) * ((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 * (Px (a,k)) = (z + ((p * (Py (a,k))) * (a - p))) + (t * ((((2 * a) * p) - (p ^2)) - 1)) )
take o ; :: thesis: ex 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 & ((p + q) + z) + (2 * n) = ((p + q) + z) + (2 * n) & ((((((p + q) + z) + (2 * n)) |^ 3) * ((((p + q) + z) + (2 * n)) + 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 & [(Px (a,k)),(Py (a,k))] is Pell's_solution of (a ^2) -' 1 & Py (a,k) = k + (i * (a - 1)) & (n + (Py (a,k))) + v = y & Px (a,k) = (p + ((Py (a,k)) * ((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 * (Px (a,k)) = (z + ((p * (Py (a,k))) * (a - p))) + (t * ((((2 * a) * p) - (p ^2)) - 1)) )
take p ; :: thesis: ex 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 & ((p + q) + z) + (2 * n) = ((p + q) + z) + (2 * n) & ((((((p + q) + z) + (2 * n)) |^ 3) * ((((p + q) + z) + (2 * n)) + 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 & [(Px (a,k)),(Py (a,k))] is Pell's_solution of (a ^2) -' 1 & Py (a,k) = k + (i * (a - 1)) & (n + (Py (a,k))) + v = y & Px (a,k) = (p + ((Py (a,k)) * ((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 * (Px (a,k)) = (z + ((p * (Py (a,k))) * (a - p))) + (t * ((((2 * a) * p) - (p ^2)) - 1)) )
take q ; :: thesis: ex 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 & ((p + q) + z) + (2 * n) = ((p + q) + z) + (2 * n) & ((((((p + q) + z) + (2 * n)) |^ 3) * ((((p + q) + z) + (2 * n)) + 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 & [(Px (a,k)),(Py (a,k))] is Pell's_solution of (a ^2) -' 1 & Py (a,k) = k + (i * (a - 1)) & (n + (Py (a,k))) + v = y & Px (a,k) = (p + ((Py (a,k)) * ((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 * (Px (a,k)) = (z + ((p * (Py (a,k))) * (a - p))) + (t * ((((2 * a) * p) - (p ^2)) - 1)) )
take r ; :: thesis: ex 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 & ((p + q) + z) + (2 * n) = ((p + q) + z) + (2 * n) & ((((((p + q) + z) + (2 * n)) |^ 3) * ((((p + q) + z) + (2 * n)) + 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 & [(Px (a,k)),(Py (a,k))] is Pell's_solution of (a ^2) -' 1 & Py (a,k) = k + (i * (a - 1)) & (n + (Py (a,k))) + v = y & Px (a,k) = (p + ((Py (a,k)) * ((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 * (Px (a,k)) = (z + ((p * (Py (a,k))) * (a - p))) + (t * ((((2 * a) * p) - (p ^2)) - 1)) )
take s ; :: thesis: ex 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 & ((p + q) + z) + (2 * n) = ((p + q) + z) + (2 * n) & ((((((p + q) + z) + (2 * n)) |^ 3) * ((((p + q) + z) + (2 * n)) + 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 & [(Px (a,k)),(Py (a,k))] is Pell's_solution of (a ^2) -' 1 & Py (a,k) = k + (i * (a - 1)) & (n + (Py (a,k))) + v = y & Px (a,k) = (p + ((Py (a,k)) * ((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 * (Px (a,k)) = (z + ((p * (Py (a,k))) * (a - p))) + (t * ((((2 * a) * p) - (p ^2)) - 1)) )
take t1 * p ; :: thesis: ex 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 & ((p + q) + z) + (2 * n) = ((p + q) + z) + (2 * n) & ((((((p + q) + z) + (2 * n)) |^ 3) * ((((p + q) + z) + (2 * n)) + 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 & [(Px (a,k)),(Py (a,k))] is Pell's_solution of (a ^2) -' 1 & Py (a,k) = k + (i * (a - 1)) & (n + (Py (a,k))) + v = y & Px (a,k) = (p + ((Py (a,k)) * ((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 * (Px (a,k)) = (z + ((p * (Py (a,k))) * (a - p))) + ((t1 * p) * ((((2 * a) * p) - (p ^2)) - 1)) )
take u ; :: thesis: ex 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 & ((p + q) + z) + (2 * n) = ((p + q) + z) + (2 * n) & ((((((p + q) + z) + (2 * n)) |^ 3) * ((((p + q) + z) + (2 * n)) + 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 & [(Px (a,k)),(Py (a,k))] is Pell's_solution of (a ^2) -' 1 & Py (a,k) = k + (i * (a - 1)) & (n + (Py (a,k))) + v = y & Px (a,k) = (p + ((Py (a,k)) * ((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 * (Px (a,k)) = (z + ((p * (Py (a,k))) * (a - p))) + ((t1 * p) * ((((2 * a) * p) - (p ^2)) - 1)) )
take w ; :: thesis: ex 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 & ((p + q) + z) + (2 * n) = ((p + q) + z) + (2 * n) & ((((((p + q) + z) + (2 * n)) |^ 3) * ((((p + q) + z) + (2 * n)) + 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 & [(Px (a,k)),(Py (a,k))] is Pell's_solution of (a ^2) -' 1 & Py (a,k) = k + (i * (a - 1)) & (n + (Py (a,k))) + v = y & Px (a,k) = (p + ((Py (a,k)) * ((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 * (Px (a,k)) = (z + ((p * (Py (a,k))) * (a - p))) + ((t1 * p) * ((((2 * a) * p) - (p ^2)) - 1)) )
take v ; :: thesis: ex 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 & ((p + q) + z) + (2 * n) = ((p + q) + z) + (2 * n) & ((((((p + q) + z) + (2 * n)) |^ 3) * ((((p + q) + z) + (2 * n)) + 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 & [(Px (a,k)),(Py (a,k))] is Pell's_solution of (a ^2) -' 1 & Py (a,k) = k + (i * (a - 1)) & (n + (Py (a,k))) + v = y & Px (a,k) = (p + ((Py (a,k)) * ((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 * (Px (a,k)) = (z + ((p * (Py (a,k))) * (a - p))) + ((t1 * p) * ((((2 * a) * p) - (p ^2)) - 1)) )
take x ; :: thesis: ex 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 & ((p + q) + z) + (2 * n) = ((p + q) + z) + (2 * n) & ((((((p + q) + z) + (2 * n)) |^ 3) * ((((p + q) + z) + (2 * n)) + 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 & [(Px (a,k)),(Py (a,k))] is Pell's_solution of (a ^2) -' 1 & Py (a,k) = k + (i * (a - 1)) & (n + (Py (a,k))) + v = y & Px (a,k) = (p + ((Py (a,k)) * ((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 * (Px (a,k)) = (z + ((p * (Py (a,k))) * (a - p))) + ((t1 * p) * ((((2 * a) * p) - (p ^2)) - 1)) )
take Py (a,n) ; :: thesis: ex 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 & ((p + q) + z) + (2 * n) = ((p + q) + z) + (2 * n) & ((((((p + q) + z) + (2 * n)) |^ 3) * ((((p + q) + z) + (2 * n)) + 2)) * ((a + 1) |^ 2)) + 1 = o ^2 & [x,(Py (a,n))] is Pell's_solution of (a ^2) -' 1 & u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * ((Py (a,n)) ^2)) * ((Py (a,n)) ^2)) + 1 & (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * (Py (a,n)))) ^2)) + 1 & [(Px (a,k)),(Py (a,k))] is Pell's_solution of (a ^2) -' 1 & Py (a,k) = k + (i * (a - 1)) & (n + (Py (a,k))) + v = Py (a,n) & Px (a,k) = (p + ((Py (a,k)) * ((a - n) - 1))) + (b * ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1)) & x = (q + ((Py (a,n)) * ((a - p) - 1))) + (s * ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1)) & p * (Px (a,k)) = (z + ((p * (Py (a,k))) * (a - p))) + ((t1 * p) * ((((2 * a) * p) - (p ^2)) - 1)) )
take z ; :: thesis: ( 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 & ((p + q) + z) + (2 * n) = ((p + q) + z) + (2 * n) & ((((((p + q) + z) + (2 * n)) |^ 3) * ((((p + q) + z) + (2 * n)) + 2)) * ((a + 1) |^ 2)) + 1 = o ^2 & [x,(Py (a,n))] is Pell's_solution of (a ^2) -' 1 & u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * ((Py (a,n)) ^2)) * ((Py (a,n)) ^2)) + 1 & (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * (Py (a,n)))) ^2)) + 1 & [(Px (a,k)),(Py (a,k))] is Pell's_solution of (a ^2) -' 1 & Py (a,k) = k + (i * (a - 1)) & (n + (Py (a,k))) + v = Py (a,n) & Px (a,k) = (p + ((Py (a,k)) * ((a - n) - 1))) + (b * ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1)) & x = (q + ((Py (a,n)) * ((a - p) - 1))) + (s * ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1)) & p * (Px (a,k)) = (z + ((p * (Py (a,k))) * (a - p))) + ((t1 * p) * ((((2 * a) * p) - (p ^2)) - 1)) )
thus ( 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 ) by A3, A4, A7; :: thesis: ( ((p + q) + z) + (2 * n) = ((p + q) + z) + (2 * n) & ((((((p + q) + z) + (2 * n)) |^ 3) * ((((p + q) + z) + (2 * n)) + 2)) * ((a + 1) |^ 2)) + 1 = o ^2 & [x,(Py (a,n))] is Pell's_solution of (a ^2) -' 1 & u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * ((Py (a,n)) ^2)) * ((Py (a,n)) ^2)) + 1 & (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * (Py (a,n)))) ^2)) + 1 & [(Px (a,k)),(Py (a,k))] is Pell's_solution of (a ^2) -' 1 & Py (a,k) = k + (i * (a - 1)) & (n + (Py (a,k))) + v = Py (a,n) & Px (a,k) = (p + ((Py (a,k)) * ((a - n) - 1))) + (b * ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1)) & x = (q + ((Py (a,n)) * ((a - p) - 1))) + (s * ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1)) & p * (Px (a,k)) = (z + ((p * (Py (a,k))) * (a - p))) + ((t1 * p) * ((((2 * a) * p) - (p ^2)) - 1)) )
thus ( ((p + q) + z) + (2 * n) = ((p + q) + z) + (2 * n) & ((((((p + q) + z) + (2 * n)) |^ 3) * ((((p + q) + z) + (2 * n)) + 2)) * ((a + 1) |^ 2)) + 1 = o ^2 ) by A14, A9, NEWTON:81; :: thesis: ( [x,(Py (a,n))] is Pell's_solution of (a ^2) -' 1 & u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * ((Py (a,n)) ^2)) * ((Py (a,n)) ^2)) + 1 & (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * (Py (a,n)))) ^2)) + 1 & [(Px (a,k)),(Py (a,k))] is Pell's_solution of (a ^2) -' 1 & Py (a,k) = k + (i * (a - 1)) & (n + (Py (a,k))) + v = Py (a,n) & Px (a,k) = (p + ((Py (a,k)) * ((a - n) - 1))) + (b * ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1)) & x = (q + ((Py (a,n)) * ((a - p) - 1))) + (s * ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1)) & p * (Px (a,k)) = (z + ((p * (Py (a,k))) * (a - p))) + ((t1 * p) * ((((2 * a) * p) - (p ^2)) - 1)) )
thus ( [x,(Py (a,n))] is Pell's_solution of (a ^2) -' 1 & u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * ((Py (a,n)) ^2)) * ((Py (a,n)) ^2)) + 1 & (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * (Py (a,n)))) ^2)) + 1 ) by A15, A16, A17; :: thesis: ( [(Px (a,k)),(Py (a,k))] is Pell's_solution of (a ^2) -' 1 & Py (a,k) = k + (i * (a - 1)) & (n + (Py (a,k))) + v = Py (a,n) & Px (a,k) = (p + ((Py (a,k)) * ((a - n) - 1))) + (b * ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1)) & x = (q + ((Py (a,n)) * ((a - p) - 1))) + (s * ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1)) & p * (Px (a,k)) = (z + ((p * (Py (a,k))) * (a - p))) + ((t1 * p) * ((((2 * a) * p) - (p ^2)) - 1)) )
thus ( [(Px (a,k)),(Py (a,k))] is Pell's_solution of (a ^2) -' 1 & Py (a,k) = k + (i * (a - 1)) & (n + (Py (a,k))) + v = Py (a,n) ) by A27, A19, A18, Lm1; :: thesis: ( Px (a,k) = (p + ((Py (a,k)) * ((a - n) - 1))) + (b * ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1)) & x = (q + ((Py (a,n)) * ((a - p) - 1))) + (s * ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1)) & p * (Px (a,k)) = (z + ((p * (Py (a,k))) * (a - p))) + ((t1 * p) * ((((2 * a) * p) - (p ^2)) - 1)) )
thus ( Px (a,k) = (p + ((Py (a,k)) * ((a - n) - 1))) + (b * ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1)) & x = (q + ((Py (a,n)) * ((a - p) - 1))) + (s * ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1)) & p * (Px (a,k)) = (z + ((p * (Py (a,k))) * (a - p))) + ((t1 * p) * ((((2 * a) * p) - (p ^2)) - 1)) ) by A35, HILB10_1:12, A37, A41, A40, A32; :: thesis: verum

end;

given 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 such that A42: q = ((w * z) + h) + j and
A43: z = ((((g * k) + g) + k) * (h + j)) + h and
A44: ((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 = f ^2 and
A45: e = ((p + q) + z) + (2 * n) and
A46: (((e |^ 3) * (e + 2)) * ((a + 1) |^ 2)) + 1 = o ^2 and
A47: [x,y] is Pell's_solution of (a ^2) -' 1 and
A48: u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1 and
A49: (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1 and
A50: [m,l] is Pell's_solution of (a ^2) -' 1 and
A51: l = k + (i * (a - 1)) and
A52: (n + l) + v = y and
A53: m = (p + (l * ((a - n) - 1))) + (b * ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1)) and
A54: x = (q + (y * ((a - p) - 1))) + (s * ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1)) and
A55: p * m = (z + ((p * l) * (a - p))) + (t * ((((2 * a) * p) - (p ^2)) - 1)) ; :: thesis: k + 1 is prime
A56: k >= 1 by NAT_1:14;
A57: 2 * k >= 2 * 1 by NAT_1:14, XREAL_1:64;
( (2 * k) ^2 = (2 * k) |^ 2 & (n + 1) |^ 2 = (n + 1) ^2 ) by NEWTON:81;
then ((2 * k) ^2) * (2 * k) = (2 * k) |^ (2 + 1) by NEWTON:6;
then ((((2 * k) ^2) * ((2 * k) * ((2 * k) + 2))) * ((n + 1) ^2)) + 1 = f ^2 by NEWTON:81, A44;
then A58: ((2 * k) - 1) + ((2 * k) |^ ((2 * k) -' 2)) <= n by A57, Th5;
((2 * k) - 1) + ((2 * k) |^ ((2 * k) -' 2)) > (2 * k) - 1 by XREAL_1:29;
then (2 * k) - 1 < n by A58, XXREAL_0:2;
then ((2 * k) - 1) + 1 <= n by INT_1:7;
then ( 1 + k <= k + k & k + k <= n ) by A56, XREAL_1:7;
then A59: 1 + k <= n by XXREAL_0:2;
then A60: k < n by NAT_1:13;
A61: 1 + 1 <= 1 + k by NAT_1:14, XREAL_1:6;
then A62: 2 <= n by A59, XXREAL_0:2;
then A63: ( e >= 2 * n & 2 * n = n + n & n + n >= 2 + 0 & n + n >= n + 2 ) by A45, XREAL_1:7, XREAL_1:31;
then A64: ( e >= 2 & e >= (n + 1) + 1 ) by XXREAL_0:2;
then A65: e > n + 1 by NAT_1:13;
( e ^2 = e |^ 2 & (a + 1) |^ 2 = (a + 1) ^2 ) by NEWTON:81;
then (e ^2) * e = e |^ (2 + 1) by NEWTON:6;
then A66: (((e ^2) * (e * (e + 2))) * ((a + 1) ^2)) + 1 = o ^2 by NEWTON:81, A46;
then A67: (e - 1) + (e |^ (e -' 2)) <= a by A64, Th5;
A68: (e - 1) + (e |^ (e -' 2)) > e - 1 by A45, XREAL_1:29, A58;
(e - 1) + (e |^ (e -' 2)) <= a by A66, A64, Th5;
then e - 1 < a by A68, XXREAL_0:2;
then A69: (e - 1) + 1 <= a by INT_1:7;
( n >= 1 & ((p + q) + z) + n >= n ) by NAT_1:14, A58, XREAL_1:31;
then (((p + q) + z) + n) + n >= n + 1 by XREAL_1:7;
then e > n by A45, NAT_1:13;
then A70: ( n < a & 1 <= n ) by A69, XXREAL_0:2, A62;
then A71: a > 1 by XXREAL_0:2;
then reconsider a = a as non trivial Nat by NEWTON03:def 1;
reconsider a1 = a - 1 as Nat ;
n <= n + (l + v) by XREAL_1:31;
then A72: y = Py (a,n) by A52, A70, A47, A48, A49, Th28;
consider n2 being Nat such that
A73: ( x = Px (a,n2) & y = Py (a,n2) ) by A47, HILB10_1:4;
A74: n = n2 by A73, A72, HILB10_1:12;
consider k1 being Nat such that
A75: ( m = Px (a,k1) & l = Py (a,k1) ) by A50, HILB10_1:4;
n + v >= 1 + 0 by A70, XREAL_1:7;
then l + 1 <= l + (n + v) by XREAL_1:6;
then Py (a,k1) < Py (a,n) by A52, A72, A75, NAT_1:13;
then ( k1 <> n & k1 <= n ) by HILB10_1:11;
then k1 < n by XXREAL_0:1;
then k1 + 1 <= n by NAT_1:13;
then k1 + 1 < a by A70, XXREAL_0:2;
then A76: (k1 + 1) - 1 < a - 1 by XREAL_1:9;
k + 1 < a by A70, XXREAL_0:2, A59;
then A77: (k + 1) - 1 < a - 1 by XREAL_1:9;
(Py (a,k1)) - k = i * (a - 1) by A51, A75;
then A78: k, Py (a,k1) are_congruent_mod a - 1 by INT_1:14, INT_1:def 5;
Py (a,k1),k1 are_congruent_mod a - 1 by HILB10_1:24;
then ( (0 + k) mod a1 = (0 + k1) mod a1 & 0 mod a1 = 0 ) by NAT_D:64, A78, INT_1:15;
then A79: ( k = k mod a1 & k mod a1 = k1 mod a1 & k1 mod a1 = k1 ) by A76, A77, NAT_D:16;
2 * n >= 1 + 1 by A63;
then A80: 2 * n > 1 by NAT_1:13;
p + ((q + z) + (2 * n)) >= 1 + p by XREAL_1:6, A58, NAT_1:14;
then e > p by A45, NAT_1:13;
then A81: a > p by A69, XXREAL_0:2;
e >= 1 + 1 by A63, XXREAL_0:2;
then e > 1 by NAT_1:13;
then e - 1 > 1 - 1 by XREAL_1:9;
then 0 + (e |^ (e -' 2)) < (e - 1) + (e |^ (e -' 2)) by XREAL_1:6;
then A82: e to_power (e -' 2) < a by A67, XXREAL_0:2;
A83: ( e - 2 >= (n + 2) - 2 & e - 2 > (n + 1) - 2 & e -' 2 = e - 2 & n - 1 >= 2 - 1 ) by A62, A64, A65, XREAL_1:233, XREAL_1:9;
then A84: ( e -' 2 > k & e -' 2 > 1 ) by A60, XXREAL_0:2;
A85: (n + 1) |^ k < a

proof

A86: n + 1 > 0 + 1 by A58, XREAL_1:6;
( (n + 1) to_power k < (n + 1) to_power (e -' 2) & (n + 1) to_power (e -' 2) < e to_power (e -' 2) ) by A65, A84, A86, POWER:37, POWER:39;
then (n + 1) to_power k < e to_power (e -' 2) by XXREAL_0:2;
hence (n + 1) |^ k < a by A82, XXREAL_0:2; :: thesis: verum

end;

A87: 2 * 1 <= n * a by A71, A62, XREAL_1:66;
A88: n + 1 <= a by A70, NAT_1:13;
then (n + 1) * n <= a * n by XREAL_1:64;
then ( ((n + 1) * n) + (n + 1) <= (a * n) + a & (n + 1) ^2 = (n + 1) * (n + 1) ) by A88, XREAL_1:7, SQUARE_1:def 1;
then ((n + 1) ^2) + 2 <= ((a * n) + a) + (n * a) by A87, XREAL_1:7;
then (((n + 1) ^2) + 1) + 1 <= ((2 * a) * n) + a ;
then ((n + 1) ^2) + 1 < ((2 * a) * n) + a by NAT_1:13;
then 0 < (((2 * a) * n) + a) - (((n + 1) ^2) + 1) by XREAL_1:50;
then 0 + a < (((((2 * a) * n) + a) - ((n + 1) ^2)) - 1) + a by XREAL_1:6;
then A89: ( p < (((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1 & (n + 1) |^ k < (((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1 ) by A81, A85, XXREAL_0:2;
m - (p + (l * ((a - n) - 1))) = b * ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1) by A53;
then A90: Px (a,k),p + ((Py (a,k)) * ((a - n) - 1)) are_congruent_mod (((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1 by INT_1:def 5, A79, A75;
A91: (Py (a,k)) * (a - (n + 1)),(Py (a,k)) * (a - (n + 1)) are_congruent_mod (((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1 by INT_1:11;
((n + 1) |^ k) + ((Py (a,k)) * (a - (n + 1))), Px (a,k) are_congruent_mod (((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1 by Th13, INT_1:14;
then ((n + 1) |^ k) + ((Py (a,k)) * (a - (n + 1))),p + ((Py (a,k)) * ((a - n) - 1)) are_congruent_mod (((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1 by A90, INT_1:15;
then (((n + 1) |^ k) + ((Py (a,k)) * (a - (n + 1)))) - ((Py (a,k)) * (a - (n + 1))),(p + ((Py (a,k)) * ((a - n) - 1))) - ((Py (a,k)) * (a - (n + 1))) are_congruent_mod (((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1 by A91, INT_1:17;
then ( (0 + ((n + 1) |^ k)) mod ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1) = (0 + p) mod ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1) & 0 mod ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1) = 0 ) by NAT_D:64;
then A92: ( (n + 1) |^ k = ((n + 1) |^ k) mod ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1) & ((n + 1) |^ k) mod ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1) = p mod ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1) & p mod ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1) = p ) by A89, NAT_D:16;
n + 1 >= 1 + 1 by A70, XREAL_1:6;
then p >= k + 1 by A92, NEWTON:85;
then p > k by NAT_1:13;
then A93: p > 1 by A56, XXREAL_0:2;
q + ((p + z) + (2 * n)) >= 1 + q by XREAL_1:6, A58, NAT_1:14;
then e > q by A45, NAT_1:13;
then A94: a > q by A69, XXREAL_0:2;
( n >= 2 & p >= 1 ) by A92, NAT_1:14, A61, A59, XXREAL_0:2;
then ( n + p >= 2 + 1 & n + (q + z) >= n + 0 ) by XREAL_1:7;
then ((n + q) + z) + (n + p) >= n + (2 + 1) by XREAL_1:7;
then e - 2 >= ((n + 2) + 1) - 2 by A45, XREAL_1:9;
then A95: e -' 2 > n by A83, NAT_1:13;
A96: (p + 1) |^ n < a

proof

A97: p + 1 > 0 + 1 by A92, XREAL_1:6;
p + 1 < p + (2 * n) by A80, XREAL_1:6;
then A98: (p + 1) + 0 < (p + (2 * n)) + (q + z) by XREAL_1:8;
( (p + 1) to_power n < (p + 1) to_power (e -' 2) & (p + 1) to_power (e -' 2) < e to_power (e -' 2) ) by A45, A98, A95, A97, POWER:37, POWER:39;
then (p + 1) to_power n < e to_power (e -' 2) by XXREAL_0:2;
hence (p + 1) |^ n < a by A82, XXREAL_0:2; :: thesis: verum

end;

( a >= 1 + 1 & p >= 1 ) by A71, A92, NAT_1:13, NAT_1:14;
then A99: 2 * 1 <= p * a by XREAL_1:66;
A100: p + 1 <= a by A81, NAT_1:13;
then (p + 1) * p <= a * p by XREAL_1:64;
then ( ((p + 1) * p) + (p + 1) <= (a * p) + a & (p + 1) ^2 = (p + 1) * (p + 1) ) by SQUARE_1:def 1, A100, XREAL_1:7;
then ((p + 1) ^2) + 2 <= ((a * p) + a) + (p * a) by A99, XREAL_1:7;
then (((p + 1) ^2) + 1) + 1 <= ((2 * a) * p) + a ;
then ((p + 1) ^2) + 1 < ((2 * a) * p) + a by NAT_1:13;
then 0 < (((2 * a) * p) + a) - (((p + 1) ^2) + 1) by XREAL_1:50;
then 0 + a < (((((2 * a) * p) + a) - ((p + 1) ^2)) - 1) + a by XREAL_1:6;
then A101: ( (p + 1) |^ n < (((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1 & q < (((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1 ) by A94, A96, XXREAL_0:2;
(Px (a,n)) - (q + ((Py (a,n)) * ((a - p) - 1))) = s * ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1) by A54, A74, A73;
then A102: Px (a,n),q + ((Py (a,n)) * ((a - p) - 1)) are_congruent_mod (((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1 by INT_1:def 5;
A103: (Py (a,n)) * ((a - p) - 1),(Py (a,n)) * ((a - p) - 1) are_congruent_mod (((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1 by INT_1:11;
((p + 1) |^ n) + ((Py (a,n)) * (a - (p + 1))), Px (a,n) are_congruent_mod (((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1 by Th13, INT_1:14;
then ((p + 1) |^ n) + ((Py (a,n)) * (a - (p + 1))),q + ((Py (a,n)) * ((a - p) - 1)) are_congruent_mod (((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1 by A102, INT_1:15;
then (((p + 1) |^ n) + ((Py (a,n)) * (a - (p + 1)))) - ((Py (a,n)) * ((a - p) - 1)),(q + ((Py (a,n)) * ((a - p) - 1))) - ((Py (a,n)) * ((a - p) - 1)) are_congruent_mod (((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1 by A103, INT_1:17;
then ( (0 + ((p + 1) |^ n)) mod ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1) = (0 + q) mod ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1) & 0 mod ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1) = 0 ) by NAT_D:64;
then A104: ( (p + 1) |^ n = ((p + 1) |^ n) mod ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1) & ((p + 1) |^ n) mod ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1) = q mod ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1) & q mod ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1) = q ) by A101, NAT_D:16;
(p + q) + (2 * n) >= 0 + 1 by A58, NAT_1:13;
then z + ((p + q) + (2 * n)) >= 1 + z by XREAL_1:6;
then e > z by A45, NAT_1:13;
then A105: a > z by A69, XXREAL_0:2;
A106: p |^ (k + 1) < a

proof

A107: e -' 2 > k + 1 by A59, A95, XXREAL_0:2;
p + 1 < p + (2 * n) by A80, XREAL_1:6;
then (p + 1) + 0 < (p + (2 * n)) + (q + z) by XREAL_1:8;
then A108: p < e by A45, NAT_1:13;
( p to_power (k + 1) < p to_power (e -' 2) & p to_power (e -' 2) < e to_power (e -' 2) ) by A93, A108, A107, POWER:37, POWER:39;
then p to_power (k + 1) < e to_power (e -' 2) by XXREAL_0:2;
hence p |^ (k + 1) < a by A82, XXREAL_0:2; :: thesis: verum

end;

p + 1 <= a by A81, NAT_1:13;
then A109: (p + 1) * p <= a * p by XREAL_1:64;
A110: a * 1 <= a * p by A92, NAT_1:14, XREAL_1:64;
( (p ^2) + 1 <= (p ^2) + p & p ^2 = p * p ) by A92, NAT_1:14, XREAL_1:6, SQUARE_1:def 1;
then (p ^2) + 1 <= a * p by A109, XXREAL_0:2;
then ((p ^2) + 1) + a <= (a * p) + (a * p) by A110, XREAL_1:7;
then (a + ((p ^2) + 1)) - ((p ^2) + 1) <= ((2 * a) * p) - ((p ^2) + 1) by XREAL_1:9;
then A111: ( p |^ (k + 1) < (((2 * a) * p) - (p ^2)) - 1 & z < (((2 * a) * p) - (p ^2)) - 1 ) by A105, A106, XXREAL_0:2;
(p * m) - (z + ((p * l) * (a - p))) = t * ((((2 * a) * p) - (p ^2)) - 1) by A55;
then A112: p * (Px (a,k)),z + ((p * (Py (a,k))) * (a - p)) are_congruent_mod (((2 * a) * p) - (p ^2)) - 1 by INT_1:def 5, A79, A75;
A113: (p * (Py (a,k))) * (a - p),(p * (Py (a,k))) * (a - p) are_congruent_mod (((2 * a) * p) - (p ^2)) - 1 by INT_1:11;
A114: p,p are_congruent_mod (((2 * a) * p) - (p ^2)) - 1 by INT_1:11;
(p |^ k) + ((Py (a,k)) * (a - p)), Px (a,k) are_congruent_mod (((2 * a) * p) - (p ^2)) - 1 by Th13, INT_1:14;
then p * ((p |^ k) + ((Py (a,k)) * (a - p))),p * (Px (a,k)) are_congruent_mod (((2 * a) * p) - (p ^2)) - 1 by INT_1:18, A114;
then p * ((p |^ k) + ((Py (a,k)) * (a - p))),z + ((p * (Py (a,k))) * (a - p)) are_congruent_mod (((2 * a) * p) - (p ^2)) - 1 by A112, INT_1:15;
then ((p * (p |^ k)) + ((p * (Py (a,k))) * (a - p))) - ((p * (Py (a,k))) * (a - p)),(z + ((p * (Py (a,k))) * (a - p))) - ((p * (Py (a,k))) * (a - p)) are_congruent_mod (((2 * a) * p) - (p ^2)) - 1 by A113, INT_1:17;
then p |^ (k + 1),z are_congruent_mod (((2 * a) * p) - (p ^2)) - 1 by NEWTON:6;
then ( (0 + (p |^ (k + 1))) mod ((((2 * a) * p) - (p ^2)) - 1) = (0 + z) mod ((((2 * a) * p) - (p ^2)) - 1) & 0 mod ((((2 * a) * p) - (p ^2)) - 1) = 0 ) by NAT_D:64;
then A115: ( p |^ (k + 1) = (p |^ (k + 1)) mod ((((2 * a) * p) - (p ^2)) - 1) & (p |^ (k + 1)) mod ((((2 * a) * p) - (p ^2)) - 1) = z mod ((((2 * a) * p) - (p ^2)) - 1) & z mod ((((2 * a) * p) - (p ^2)) - 1) = z ) by A111, NAT_D:16;
A116: k + 1 > 1 by NAT_1:13, NAT_1:14;
A117: (k + 1) -' 1 = (k + 1) - 1 by XREAL_1:233, NAT_1:14;
((g * k) + g) + k = k ! by A44, Th29, A42, A43, A115, A104, A92, A58;
then (k !) + 1 = (g + 1) * (k + 1) ;
then k + 1 divides (k !) + 1 by INT_1:def 3;
then ((k !) + 1) mod (k + 1) = 0 by INT_1:62;
hence k + 1 is prime by A116, A117, NAT_5:22; :: thesis: verum