let k be non zero Nat; :: thesis:
given x, y being positive Nat such that A1: ((x |^ 2) + (2 |^ (2 * k))) + 1 = y |^ 3 ; :: thesis:
A2: x |^ 2 = x ^2 by WSIERP_1:1;
A3: y |^ 3 = (y * y) * y by POLYEQ_5:2;

assume x is odd ; :: thesis:
then reconsider x = x as odd Nat ;
A4: (x ^2) mod 8 = 1 by NUMBER10:60;
((x |^ 2) + (2 |^ (2 * k))) + 1 is even ;
then y is even by A1;
then A5: (y |^ 3) mod 8 = 0 by Th82;
A6: (((x |^ 2) + (2 |^ (2 * k))) + 1) mod 8 = ((((x |^ 2) mod 8) + ((2 |^ (2 * k)) mod 8)) + (1 mod 8)) mod 8 by NUMBER05:8
.= (2 + ((2 |^ (2 * k)) mod 8)) mod 8 by A2, A4 ;
2 |^ (k * 2) = (2 |^ k) |^ 2 by NEWTON:9
.= (2 |^ k) ^2 by WSIERP_1:1 ;
then ( (2 |^ (2 * k)) mod 8 = 0 or (2 |^ (2 * k)) mod 8 = 4 ) by NUMBER10:59;
hence contradiction by A1, A5, A6, NAT_D:24; :: thesis:

end;

then consider a, z being Nat such that
z is odd and
A7: a > 0 and
A8: x = (2 |^ a) * z by NAT_5:2;
A9: (y |^ 3) - 1 = (y - 1) * (((y ^2) + y) + 1) by A3;
reconsider a = a as positive Nat by A7;
A10: (2 |^ a) |^ 2 = 2 |^ (2 * a) by NEWTON:9;
A11: (2 |^ a) |^ 2 = (2 |^ a) ^2 by WSIERP_1:1;
A12: 2 |^ (2 * a) = (2 |^ 2) |^ a by NEWTON:9;
A13: 2 |^ (2 * k) = (2 |^ 2) |^ k by NEWTON:9;

A14: now :: thesis:

assume that
A15: (y |^ 3) - 1, 0 are_congruent_mod 4 and
A16: y,3 are_congruent_mod 4 ; :: thesis:
A17: y - 1,3 - 1 are_congruent_mod 4 by A16;
A18: y ^2 ,3 ^2 are_congruent_mod 4 by A16, INT_1:18;
A19: (4 * 1) + 0, 0 are_congruent_mod 4 ;
(4 * 2) + 1,1 are_congruent_mod 4 ;
then y ^2 ,1 are_congruent_mod 4 by A18, INT_1:15;
then (y ^2) + y,1 + 3 are_congruent_mod 4 by A16, INT_1:16;
then (y ^2) + y, 0 are_congruent_mod 4 by A19, INT_1:15;
then ((y ^2) + y) + 1,0 + 1 are_congruent_mod 4 ;
then (y - 1) * (((y ^2) + y) + 1),2 * 1 are_congruent_mod 4 by A17, INT_1:18;
then 2,(y |^ 3) - 1 are_congruent_mod 4 by A3, INT_1:14;
then 2, 0 are_congruent_mod 4 by A15, INT_1:15;
then 2 mod 4 = 0 mod 4 ;
hence contradiction by NAT_D:24; :: thesis:

end;

A20: now :: thesis:

assume A21: y,1 are_congruent_mod 4 ; :: thesis:
then y * y,1 * 1 are_congruent_mod 4 by INT_1:18;
then (y ^2) + y,1 + 1 are_congruent_mod 4 by A21, INT_1:16;
then ((y ^2) + y) + 1,2 + 1 are_congruent_mod 4 ;
then ex A being Integer st ((y ^2) + y) + 1 = (A * 4) + 3 by NAT_6:9;
then consider p, q being Nat such that
A22: p = (4 * q) + 3 and
A23: p is prime and
A24: p divides ((y ^2) + y) + 1 by NUMBER05:3;
take p = p; :: thesis:
take q = q; :: thesis:
thus p = (4 * q) + 3 by A22; :: thesis:
thus p is prime by A23; :: thesis:
thus p divides ((y ^2) + y) + 1 by A24; :: thesis:

assume p divides 2 ; :: thesis:
then ( p = 1 or p = 2 ) by NUMBER07:9;
hence ( (4 * q) + 2 = 0 or (4 * q) + 1 = 0 ) by A22; :: thesis:
hence contradiction ; :: thesis:

end;

hence not p divides 2 ; :: thesis:

end;

per cases by XXREAL_0:1;

suppose A25: a = k ; :: thesis:

then A26: (2 |^ (2 * k)) * ((z ^2) + 1) = (((2 |^ a) * z) ^2) + (2 |^ (2 * k)) by A10, A11
.= (y |^ 3) - 1 by A1, A8, WSIERP_1:1 ;
y is odd by A26;

per cases by Th81;

suppose y,1 are_congruent_mod 4 ; :: thesis:

then consider p, q being Nat such that
A27: p = (4 * q) + 3 and
A28: p is prime and
A29: p divides ((y ^2) + y) + 1 and
A30: not p divides 2 by A20;
p divides (2 |^ (2 * k)) * ((z ^2) + 1) by A9, A26, A29, INT_2:2;
then ( p divides 2 |^ (2 * k) or p divides (z ^2) + 1 ) by A28, INT_5:7;
then p divides (z ^2) + (1 ^2) by A30, A28, NAT_3:5;
then p divides 1 by A27, A28, NUMBER10:62;
hence contradiction by A28, INT_2:27; :: thesis:

end;

suppose y,3 are_congruent_mod 4 ; :: thesis:

hence contradiction by A14, A26, A12, A25, Lm1, INT_2:2, NAT_3:3; :: thesis:

end;

end;

end;

suppose a < k ; :: thesis:

then reconsider ka = k - a as Element of NAT by INT_1:5;
A31: (2 |^ (2 * a)) * ((2 |^ ka) ^2) = ((2 |^ (2 * a)) * (2 |^ ka)) * (2 |^ ka)
.= (2 |^ ((2 * a) + ka)) * (2 |^ ka) by NEWTON:8
.= 2 |^ (((2 * a) + ka) + ka) by NEWTON:8
.= 2 |^ (2 * k) ;
then A32: (y |^ 3) - 1 = (2 |^ (2 * a)) * (((2 |^ ka) ^2) + (z ^2)) by A1, A2, A8, A10, A11;
y is odd by A1, A8, A31;

per cases by Th81;

suppose y,1 are_congruent_mod 4 ; :: thesis:

then consider p, q being Nat such that
A33: p = (4 * q) + 3 and
A34: p is prime and
A35: p divides ((y ^2) + y) + 1 and
A36: not p divides 2 by A20;
p divides (2 |^ (2 * a)) * (((2 |^ ka) ^2) + (z ^2)) by A9, A31, A1, A2, A8, A10, A11, A35, INT_2:2;
then ( p divides 2 |^ (2 * a) or p divides ((2 |^ ka) ^2) + (z ^2) ) by A34, INT_5:7;
then p divides 2 |^ ka by A33, A34, A36, NAT_3:5, NUMBER10:62;
hence contradiction by A34, A36, NAT_3:5; :: thesis:

end;

suppose y,3 are_congruent_mod 4 ; :: thesis:

hence contradiction by A14, A12, A32, Lm1, INT_2:2, NAT_3:3; :: thesis:

end;

end;

end;

suppose a > k ; :: thesis:

then reconsider ak = a - k as Element of NAT by INT_1:5;
A37: ((2 |^ (2 * k)) * (2 |^ ak)) * (2 |^ ak) = (2 |^ ((2 * k) + ak)) * (2 |^ ak) by NEWTON:8
.= 2 |^ (((2 * k) + ak) + ak) by NEWTON:8
.= 2 |^ (a + a)
.= (2 |^ a) * (2 |^ a) by NEWTON:8 ;
(2 |^ (2 * k)) * (((2 |^ ak) * z) ^2) = (((2 |^ (2 * k)) * (2 |^ ak)) * (2 |^ ak)) * (z * z)
.= ((2 |^ a) * (2 |^ a)) * (z * z) by A37
.= ((2 |^ a) * z) * ((2 |^ a) * z) ;
then A38: (y |^ 3) - 1 = ((2 |^ (2 * k)) * (((2 |^ ak) * z) ^2)) + ((2 |^ (2 * k)) * 1) by A1, A8, WSIERP_1:1
.= (2 |^ (2 * k)) * ((((2 |^ ak) * z) ^2) + 1) ;
then y is odd ;

per cases by Th81;

suppose y,1 are_congruent_mod 4 ; :: thesis:

then consider p, q being Nat such that
A39: p = (4 * q) + 3 and
A40: p is prime and
A41: p divides ((y ^2) + y) + 1 and
A42: not p divides 2 by A20;
p divides (2 |^ (2 * k)) * ((((2 |^ ak) * z) ^2) + 1) by A9, A38, A41, INT_2:2;
then ( p divides 2 |^ (2 * k) or p divides (((2 |^ ak) * z) ^2) + (1 ^2) ) by A40, INT_5:7;
then p divides 1 by A39, A40, A42, NAT_3:5, NUMBER10:62;
hence contradiction by A40, INT_2:27; :: thesis:

end;

suppose y,3 are_congruent_mod 4 ; :: thesis:

hence contradiction by A14, A38, A13, Lm1, INT_2:2, NAT_3:3; :: thesis:

end;

end;

end;

end;