let x, y be Integer; :: thesis: for c being odd Nat holds (x |^ 2) - (y |^ 3) <> ((2 * c) |^ 3) - 1
A1: x |^ 2 = x ^2 by WSIERP_1:1;
let c be odd Nat; :: thesis: (x |^ 2) - (y |^ 3) <> ((2 * c) |^ 3) - 1
assume A2: (x |^ 2) - (y |^ 3) = ((2 * c) |^ 3) - 1 ; :: thesis: contradiction
A3: (2 * c) |^ 3 = ((2 * c) * (2 * c)) * (2 * c) by POLYEQ_5:2;

per cases ( y is odd or y is even ) ;

suppose y is odd ; :: thesis: contradiction

then consider s being Integer such that
A4: y - c = 2 * s by ABIAN:11;
A5: 3 mod 8 = 3 by NAT_D:24;
(c ^2) mod 8 = 1 by Th60;
then 3 = ((3 mod 8) * ((c ^2) mod 8)) mod 8 by NAT_D:24
.= (3 * (c ^2)) mod 8 by NAT_D:67 ;
then consider j being Integer such that
A6: 3 * (c ^2) = (j * 8) + 3 by A5, NAT_D:64, NAT_6:9;
((j * 8) + 3) - 3 >= 3 - 3 by A6, XREAL_1:66;
then j >= 0 ;
then reconsider j = j as Element of NAT by INT_1:3;
((y - c) ^2) + (3 * (c ^2)) = ((2 * s) ^2) + ((8 * j) + 3) by A4, A6
.= (4 * ((s ^2) + (2 * j))) + 3 ;
then consider p, q being Nat such that
A7: p = (4 * q) + 3 and
A8: p is prime and
A9: p divides ((y - c) ^2) + (3 * (c ^2)) by NUMBER05:3;
y |^ 3 = (y * y) * y by POLYEQ_5:2;
then (y + (2 * c)) * (((y - c) ^2) + (3 * (c ^2))) = ((2 * c) |^ 3) + (y |^ 3) by A3
.= (x |^ 2) + 1 by A2 ;
then ((y - c) ^2) + (3 * (c ^2)) divides (x ^2) + 1 by A1;
hence contradiction by A7, A8, A9, Lm18, INT_2:9; :: thesis: verum

end;

suppose y is even ; :: thesis: contradiction

then consider i being Integer such that
A10: y = 2 * i by ABIAN:11;
( ((2 * i) |^ 3) mod 8 = 0 & ((2 * c) |^ 3) mod 8 = 0 ) by Lm19;
then ((y |^ 3) + ((2 * c) |^ 3)) mod 8 = (0 + 0) mod 8 by A10, NAT_D:66;
then (((y |^ 3) + ((2 * c) |^ 3)) - 1) mod 8 = ((0 mod 8) - (1 mod 8)) mod 8 by INT_6:7
.= (7 + ((- 1) * 8)) mod 8 by NAT_D:24
.= 7 mod 8 by NAT_D:61 ;
then (x ^2) mod 8 = 7 by A1, A2, NAT_D:24;
hence contradiction by Th59, Th60; :: thesis: verum

end;

end;