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 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) )
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 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) ) :: 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 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) implies k + 1 is prime )

proof

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 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)
then consider 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
A1: q = ((w * z) + h) + j and
A2: z = ((((g * k) + g) + k) * (h + j)) + h and
A3: ((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 = f ^2 and
A4: e = ((p + q) + z) + (2 * n) and
A5: (((e |^ 3) * (e + 2)) * ((a + 1) |^ 2)) + 1 = o ^2 and
A6: [x,y] is Pell's_solution of (a ^2) -' 1 and
A7: u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1 and
A8: (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1 and
A9: [m,l] is Pell's_solution of (a ^2) -' 1 and
A10: l = k + (i * (a - 1)) and
A11: (n + l) + v = y and
A12: m = (p + (l * ((a - n) - 1))) + (b * ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1)) and
A13: x = (q + (y * ((a - p) - 1))) + (s * ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1)) and
A14: p * m = (z + ((p * l) * (a - p))) + (t * ((((2 * a) * p) - (p ^2)) - 1)) by Th30;
reconsider x1 = (((w * z) + h) + j) - q, x2 = (((((g * k) + g) + k) * (h + j)) + h) - z, x3 = (((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1) - (f ^2), x4 = (((p + q) + z) + (2 * n)) - e, x5 = ((((e |^ 3) * (e + 2)) * ((a + 1) |^ 2)) + 1) - (o ^2) as Integer ;
reconsider x6 = ((x ^2) - (((a ^2) -' 1) * (y ^2))) - 1, x7 = (((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1) - (u ^2), x8 = (((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1) - ((x + (c * u)) ^2), x9 = ((m ^2) - (((a ^2) -' 1) * (l ^2))) - 1, x10 = (k + (i * (a - 1))) - l as Integer ;
reconsider x11 = ((n + l) + v) - y, x12 = ((p + (l * ((a - n) - 1))) + (b * ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1))) - m, x13 = ((q + (y * ((a - p) - 1))) + (s * ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1))) - x, x14 = ((z + ((p * l) * (a - p))) + (t * ((((2 * a) * p) - (p ^2)) - 1))) - (p * m) as Integer ;
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 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)
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 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)
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 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)
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 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)
take e ; :: 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 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)
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 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)
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 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)
take h ; :: thesis: ex 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)
take i ; :: thesis: ex 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)
take j ; :: thesis: ex 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)
take l ; :: thesis: ex 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)
take m ; :: thesis: ex 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)
take n ; :: thesis: ex 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)
take o ; :: thesis: ex 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)
take p ; :: thesis: ex 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)
take q ; :: thesis: ex 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)
take r ; :: thesis: ex 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)
take s ; :: thesis: ex 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)
take t ; :: thesis: ex 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)
take u ; :: thesis: ex 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)
take w ; :: thesis: ex 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)
take v ; :: thesis: ex 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)
take x ; :: thesis: ex 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)
take y ; :: thesis: ex 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)
take z ; :: thesis: 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)
A15: ( x1 ^2 = x1 * x1 & x2 ^2 = x2 * x2 & x3 ^2 = x3 * x3 & x4 ^2 = x4 * x4 & x5 ^2 = x5 * x5 & x6 ^2 = x6 * x6 & x7 ^2 = x7 * x7 & x8 ^2 = x8 * x8 & x9 ^2 = x9 * x9 & x10 ^2 = x10 * x10 & x11 ^2 = x11 * x11 & x12 ^2 = x12 * x12 & x13 ^2 = x13 * x13 & x14 ^2 = x14 * x14 ) by SQUARE_1:def 1;
(m ^2) - (((a ^2) -' 1) * (l ^2)) = 1 by A9, Lm1;
hence 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) by A1, A2, A3, A4, A15, A5, A6, Lm1, A7, A8, A10, A11, A12, A13, A14; :: 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 A16: 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) ; :: thesis: k + 1 is prime
reconsider x1 = (((w * z) + h) + j) - q, x2 = (((((g * k) + g) + k) * (h + j)) + h) - z, x3 = (((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1) - (f ^2), x4 = (((p + q) + z) + (2 * n)) - e, x5 = ((((e |^ 3) * (e + 2)) * ((a + 1) |^ 2)) + 1) - (o ^2) as Integer ;
reconsider x6 = ((x ^2) - (((a ^2) -' 1) * (y ^2))) - 1, x7 = (((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1) - (u ^2), x8 = (((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1) - ((x + (c * u)) ^2), x9 = ((m ^2) - (((a ^2) -' 1) * (l ^2))) - 1, x10 = (k + (i * (a - 1))) - l as Integer ;
reconsider x11 = ((n + l) + v) - y, x12 = ((p + (l * ((a - n) - 1))) + (b * ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1))) - m, x13 = ((q + (y * ((a - p) - 1))) + (s * ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1))) - x, x14 = ((z + ((p * l) * (a - p))) + (t * ((((2 * a) * p) - (p ^2)) - 1))) - (p * m) as Integer ;
A17: ( x1 ^2 = x1 * x1 & x2 ^2 = x2 * x2 & x3 ^2 = x3 * x3 & x4 ^2 = x4 * x4 & x5 ^2 = x5 * x5 & x6 ^2 = x6 * x6 & x7 ^2 = x7 * x7 & x8 ^2 = x8 * x8 & x9 ^2 = x9 * x9 & x10 ^2 = x10 * x10 & x11 ^2 = x11 * x11 & x12 ^2 = x12 * x12 & x13 ^2 = x13 * x13 & x14 ^2 = x14 * x14 ) by SQUARE_1:def 1;
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)) )

proof

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 e ; :: 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 & 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 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 & 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 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 & 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 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 & 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 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 & 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 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 & 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 l ; :: 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 & 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 m ; :: 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 & 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 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 & 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 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 & 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 ; :: 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 & 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 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 & 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 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 & 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 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 & 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 t ; :: 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 & 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 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 & 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 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 & 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 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 & 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 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 & 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 y ; :: 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 & 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 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 & 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)) )
x1 = 0 by A16, A17;
hence q = ((w * z) + h) + j ; :: thesis: ( 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)) )
x2 = 0 by A16, A17;
hence z = ((((g * k) + g) + k) * (h + j)) + h ; :: thesis: ( ((((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)) )
x3 = 0 by A16, A17;
hence ((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 = f ^2 ; :: thesis: ( 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)) )
x4 = 0 by A16, A17;
hence e = ((p + q) + z) + (2 * n) ; :: thesis: ( (((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)) )
x5 = 0 by A16, A17;
hence (((e |^ 3) * (e + 2)) * ((a + 1) |^ 2)) + 1 = o ^2 ; :: thesis: ( [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)) )
x6 = 0 by A16, A17;
hence [x,y] is Pell's_solution of (a ^2) -' 1 by Lm1; :: thesis: ( 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)) )
x7 = 0 by A16, A17;
hence u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1 ; :: thesis: ( (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)) )
x8 = 0 by A16, A17;
hence (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1 ; :: thesis: ( [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)) )
x9 = 0 by A16, A17;
hence [m,l] is Pell's_solution of (a ^2) -' 1 by Lm1; :: thesis: ( 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)) )
x10 = 0 by A16, A17;
hence l = k + (i * (a - 1)) ; :: thesis: ( (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)) )
x11 = 0 by A16, A17;
hence (n + l) + v = y ; :: thesis: ( 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)) )
x12 = 0 by A16, A17;
hence m = (p + (l * ((a - n) - 1))) + (b * ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1)) ; :: thesis: ( 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)) )
x13 = 0 by A16, A17;
hence x = (q + (y * ((a - p) - 1))) + (s * ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1)) ; :: thesis: p * m = (z + ((p * l) * (a - p))) + (t * ((((2 * a) * p) - (p ^2)) - 1))
x14 = 0 by A16, A17;
hence p * m = (z + ((p * l) * (a - p))) + (t * ((((2 * a) * p) - (p ^2)) - 1)) ; :: thesis: verum

end;

hence k + 1 is prime by Th30; :: thesis: verum