set A = { [x,y] where x, y is Integer : y |^ 2 = (x |^ 3) + ((x + 4) |^ 2) } ;
thus { [x,y] where x, y is Integer : y |^ 2 = (x |^ 3) + ((x + 4) |^ 2) } c= {[0,4],[0,(- 4)]} :: according to XBOOLE_0:def 10 :: thesis: {[0,4],[0,(- 4)]} c= { [x,y] where x, y is Integer : y |^ 2 = (x |^ 3) + ((x + 4) |^ 2) }
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { [x,y] where x, y is Integer : y |^ 2 = (x |^ 3) + ((x + 4) |^ 2) } or e in {[0,4],[0,(- 4)]} )
assume e in { [x,y] where x, y is Integer : y |^ 2 = (x |^ 3) + ((x + 4) |^ 2) } ; :: thesis: e in {[0,4],[0,(- 4)]}
then consider x, y being Integer such that
A1: e = [x,y] and
A2: y |^ 2 = (x |^ 3) + ((x + 4) |^ 2) ;
A3: y |^ 2 = y ^2 by WSIERP_1:1;
A4: 4 |^ 2 = 4 ^2 by WSIERP_1:1;
per cases ( x = 0 or x <> 0 ) ;
suppose A5: x = 0 ; :: thesis: e in {[0,4],[0,(- 4)]}
then ( y = 4 or y = - 4 ) by A2, A3, A4, SQUARE_1:40;
hence e in {[0,4],[0,(- 4)]} by A1, A5, TARSKI:def 2; :: thesis: verum
end;
suppose A6: x <> 0 ; :: thesis: e in {[0,4],[0,(- 4)]}
set d = ((y - x) - 4) gcd ((y + x) + 4);
A7: (x + 4) |^ 2 = (x + 4) ^2 by WSIERP_1:1;
then A8: x |^ 3 = ((y - x) - 4) * ((y + x) + 4) by A2, A3;
then A9: ( (y - x) - 4 <> 0 & (y + x) + 4 <> 0 ) by A6;
A10: ((y - x) - 4) gcd ((y + x) + 4) divides (y - x) - 4 by INT_2:def 2;
A11: ((y - x) - 4) gcd ((y + x) + 4) divides (y + x) + 4 by INT_2:def 2;
A12: ((y - x) - 4) gcd ((y + x) + 4) divides ((y - x) - 4) * ((y + x) + 4) by A11, INT_2:2;
A13: ((y - x) - 4) gcd ((y + x) + 4) divides ((y + x) + 4) - ((y - x) - 4) by A10, A11, INT_5:1;
A14: x |^ 3 = (x * x) * x by POLYEQ_5:2;
A15: for p being odd Prime holds not p divides ((y - x) - 4) gcd ((y + x) + 4)
proof
given p being odd Prime such that A16: p divides ((y - x) - 4) gcd ((y + x) + 4) ; :: thesis: contradiction
A17: p divides 2 * (x + 4) by A13, A16, INT_2:2;
p divides ((y - x) - 4) * ((y + x) + 4) by A12, A16, INT_2:2;
then A18: p divides x by A2, A3, A7, Th6;
A19: p divides (x + y) + 4 by A11, A16, INT_2:2;
A20: ( p divides x + 4 or ex z being Integer st
( p = z * 2 & z divides x + 4 ) ) by A17, Th8, XPRIMES1:2;
p divides (y - x) - 4 by A10, A16, INT_2:2;
then p divides ((y - x) - 4) + (x + 4) by A20, WSIERP_1:4;
then p divides x + y by A18, WSIERP_1:4;
then p divides ((y + x) + 4) - (x + y) by A19, INT_5:1;
then ( p = 1 or p = 2 * 1 or p = 2 * 2 ) by NUMBER05:21;
hence contradiction by INT_2:def 4; :: thesis: verum
end;
consider E being Nat, b being odd Nat such that
A21: ((y - x) - 4) gcd ((y + x) + 4) = b * (2 |^ E) by A9, NAT_6:3;
A22: now :: thesis: not b <> 1
assume b <> 1 ; :: thesis: contradiction
then consider p being Element of NAT such that
A23: p is prime and
A24: p divides b by INT_2:31, NAT_1:23;
p is odd by A24;
hence contradiction by A15, A21, A23, A24, INT_2:2; :: thesis: verum
end;
consider m, n being Integer such that
A25: (y - x) - 4 = (((y - x) - 4) gcd ((y + x) + 4)) * m and
A26: (y + x) + 4 = (((y - x) - 4) gcd ((y + x) + 4)) * n and
A27: m,n are_coprime by A9, INT_2:23;
A28: 3 = (2 * 1) + 1 ;
per cases ( 16 divides ((y - x) - 4) gcd ((y + x) + 4) or not ((2 * 2) * 2) * 2 divides ((y - x) - 4) gcd ((y + x) + 4) ) ;
suppose A29: 16 divides ((y - x) - 4) gcd ((y + x) + 4) ; :: thesis: e in {[0,4],[0,(- 4)]}
then A30: 16 * 16 divides (((y - x) - 4) gcd ((y + x) + 4)) * (((y - x) - 4) gcd ((y + x) + 4)) by NAT_3:1;
(((y - x) - 4) gcd ((y + x) + 4)) * (((y - x) - 4) gcd ((y + x) + 4)) divides ((y - x) - 4) * ((y + x) + 4) by A10, A11, NAT_3:1;
then 2 |^ 8 divides x |^ 3 by A2, A3, A7, A30, Lm4, INT_2:9;
then 2 |^ 3 divides x by Lm2, Th101;
then A31: ((2 * 2) * 2) * 2 divides 2 * x by Lm2, NAT_3:1;
16 divides (2 * x) + 8 by A13, A29, INT_2:9;
then 16 divides ((2 * x) + 8) - (2 * x) by A31, INT_5:1;
hence e in {[0,4],[0,(- 4)]} by NAT_D:7; :: thesis: verum
end;
suppose not ((2 * 2) * 2) * 2 divides ((y - x) - 4) gcd ((y + x) + 4) ; :: thesis: e in {[0,4],[0,(- 4)]}
then not 2 |^ 4 divides 2 |^ E by A21, A22, POLYEQ_5:3;
then 3 + 1 > E by NEWTON:89;
then E <= 3 by NAT_1:13;
then not not E = 0 & ... & not E = 3 ;
per cases then ( E = 0 or E = 1 or E = 2 or E = 3 ) ;
suppose E = 0 ; :: thesis: e in {[0,4],[0,(- 4)]}
then A32: (y - x) - 4,(y + x) + 4 are_coprime by A21, A22;
then consider a being Integer such that
A33: (y - x) - 4 = a |^ 3 by A8, A28, Th103;
consider b being Integer such that
A34: (y + x) + 4 = b |^ 3 by A8, A28, A32, Th103;
x |^ 3 = (a * b) |^ 3 by A8, A33, A34, NEWTON:7;
then A35: x = a * b by A28, NEWTON03:13;
A36: (2 * x) + 8 = (b |^ 3) - (a |^ 3) by A33, A34;
A37: a |^ 3 = (a * a) * a by POLYEQ_5:2;
A38: b |^ 3 = (b * b) * b by POLYEQ_5:2;
per cases ( a = b or a <> b ) ;
suppose a = b ; :: thesis: e in {[0,4],[0,(- 4)]}
then (2 * x) + 8 = 0 by A36;
then y |^ 2 = (((- 4) * (- 4)) * (- 4)) + 0 by A2, POLYEQ_5:2;
hence e in {[0,4],[0,(- 4)]} ; :: thesis: verum
end;
suppose A39: a <> b ; :: thesis: e in {[0,4],[0,(- 4)]}
per cases ( a * b = 0 or a * b > 0 or a * b < 0 ) ;
suppose a * b = 0 ; :: thesis: e in {[0,4],[0,(- 4)]}
hence e in {[0,4],[0,(- 4)]} by A6, A35; :: thesis: verum
end;
suppose A40: a * b > 0 ; :: thesis: e in {[0,4],[0,(- 4)]}
A41: ((2 * a) * b) + 8 = (b |^ 3) - (a |^ 3) by A33, A34, A35
.= (b - a) * (((b - a) ^2) + ((3 * a) * b)) by A37, A38 ;
A42: b - a <> 1
proof
assume b - a = 1 ; :: thesis: contradiction
then ((2 * a) * b) + 8 = 1 + ((3 * a) * b) by A41;
then y ^2 = (7 |^ 3) + ((7 + 4) ^2) by A2, A3, A35, WSIERP_1:1
.= ((7 * 7) * 7) + 121 by POLYEQ_5:2
.= 464 ;
hence contradiction by Lm13; :: thesis: verum
end;
A43: 3 * (a * b) > 0 by A40;
then A44: ((b - a) ^2) + ((3 * a) * b) >= 0 ;
2 * (a * b) > 0 by A40;
then b - a > 0 by A41, A44;
then b - a >= 0 + 1 by NAT_1:13;
then b - a > 1 by A42, XXREAL_0:1;
then A45: b - a >= 1 + 1 by NAT_1:13;
then A46: (b - a) * (((b - a) ^2) + ((3 * a) * b)) >= 2 * (((b - a) ^2) + ((3 * a) * b)) by A43, XREAL_1:64;
(2 * ((b - a) ^2)) + ((6 * a) * b) > 0 + ((6 * a) * b) by A45, XREAL_1:6;
then (b - a) * (((b - a) ^2) + ((3 * a) * b)) > (6 * a) * b by A46, XXREAL_0:2;
then ((6 * a) * b) - ((2 * a) * b) < (((2 * a) * b) + 8) - ((2 * a) * b) by A41, XREAL_1:8;
then 4 * (a * b) < 4 * 2 ;
then a * b = 1 by A40, NAT_1:23, XREAL_1:64;
then ( ( a = 1 & b = 1 ) or ( a = - 1 & b = - 1 ) ) by INT_1:9;
hence e in {[0,4],[0,(- 4)]} by A39; :: thesis: verum
end;
suppose a * b < 0 ; :: thesis: e in {[0,4],[0,(- 4)]}
per cases then ( ( a > 0 & b < 0 ) or ( a < 0 & b > 0 ) ) by XREAL_1:133;
suppose that A47: a > 0 and
A48: b < 0 ; :: thesis: e in {[0,4],[0,(- 4)]}
A49: (- b) |^ 3 = - (b |^ 3) by A28, POWER:2;
A50: (- b) |^ 3 = ((- b) * (- b)) * (- b) by POLYEQ_5:2;
0 + 1 <= a by A47, NAT_1:13;
then A51: (a * a) * a >= (a * a) * 1 by XREAL_1:64;
- b >= 0 + 1 by A48, NAT_1:13;
then (b ^2) * (- b) >= (b ^2) * 1 by XREAL_1:64;
then A52: (a |^ 3) + ((- b) |^ 3) >= (a ^2) + ((- b) ^2) by A37, A50, A51, XREAL_1:7;
((a ^2) + ((- b) ^2)) + ((2 * a) * b) = (a + b) ^2 ;
then (((a ^2) + ((- b) ^2)) + ((2 * a) * b)) - ((2 * a) * b) >= 0 - ((2 * a) * b) by XREAL_1:9;
then A53: (a |^ 3) - (b |^ 3) >= - ((2 * a) * b) by A49, A52, XXREAL_0:2;
A54: (a |^ 3) - (b |^ 3) = (- ((2 * a) * b)) - 8 by A33, A34, A35;
(- ((2 * a) * b)) - 8 < (- ((2 * a) * b)) - 0 by XREAL_1:8;
hence e in {[0,4],[0,(- 4)]} by A53, A54; :: thesis: verum
end;
suppose that A55: a < 0 and
A56: b > 0 ; :: thesis: e in {[0,4],[0,(- 4)]}
b |^ 3 = ((a |^ 3) + ((2 * a) * b)) + 8 by A33, A34, A35;
then (b |^ 3) - 8 < 0 by A37, A55, A56;
then b |^ 3 < 0 + 8 by XREAL_1:19;
then b = 1 by A56, Lm2, NAT_1:23, PREPOWER:9;
then A57: 1 |^ 3 = ((a |^ 3) + ((2 * a) * 1)) + 8 by A33, A34, A35;
a <= 0 - 1 by A55, INT_1:52;
per cases then ( a = - 1 or a < - 1 ) by XXREAL_0:1;
suppose a = - 1 ; :: thesis: e in {[0,4],[0,(- 4)]}
hence e in {[0,4],[0,(- 4)]} by A37, A57; :: thesis: verum
end;
suppose a < - 1 ; :: thesis: e in {[0,4],[0,(- 4)]}
then A58: a <= (- 1) - 1 by INT_1:52;
then a |^ 3 <= (- 2) |^ 3 by A28, Th104;
then A59: a |^ 3 <= ((- 2) * (- 2)) * (- 2) by POLYEQ_5:2;
2 * a <= 2 * (- 2) by A58, XREAL_1:64;
then (a |^ 3) + (2 * a) <= (- 8) + (- 4) by A59, XREAL_1:7;
then ((a |^ 3) + (2 * a)) + 7 <= (- 12) + 7 by XREAL_1:6;
hence e in {[0,4],[0,(- 4)]} by A57; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;
end;
suppose A60: E = 1 ; :: thesis: e in {[0,4],[0,(- 4)]}
then A61: ((y - x) - 4) gcd ((y + x) + 4) = 2 by A21, A22;
A62: 2 divides x by A2, A3, A7, A12, A21, A22, A60, Th6, XPRIMES1:2;
A63: 2 divides (y - x) - 4 by A21, A22, A25, A60;
2 divides 2 * 2 ;
then 2 divides ((y - x) - 4) + 4 by A63, WSIERP_1:4;
then 2 divides (y - x) + x by A62, WSIERP_1:4;
then A64: 2 divides m + n by A25, A26, A61;
A65: now :: thesis: ( ( m is odd & n is odd & m is odd & n is odd ) or ( m is even & n is odd & contradiction ) or ( m is odd & n is even & contradiction ) or ( m is even & n is even & contradiction ) )
per cases ( ( m is odd & n is odd ) or ( m is even & n is odd ) or ( m is odd & n is even ) or ( m is even & n is even ) ) ;
case ( m is odd & n is odd ) ; :: thesis: ( m is odd & n is odd )
hence ( m is odd & n is odd ) ; :: thesis: verum
end;
end;
end;
then consider m1 being Integer such that
A66: m = (2 * m1) + 1 by ABIAN:1;
consider n1 being Integer such that
A67: n = (2 * n1) + 1 by A65, ABIAN:1;
set u = 8 * ((m1 * ((2 * n1) + 1)) + n1);
A68: x |^ 3 = (2 * m) * (2 * n) by A8, A21, A22, A25, A26, A60
.= (8 * ((m1 * ((2 * n1) + 1)) + n1)) + 4 by A66, A67 ;
((8 * ((m1 * ((2 * n1) + 1)) + n1)) + 4) mod 8 = (((8 * ((m1 * ((2 * n1) + 1)) + n1)) mod 8) + (4 mod 8)) mod 8 by NAT_D:66
.= (0 + (4 mod 8)) mod 8 by NAT_D:71
.= 4 by NAT_D:24 ;
then not 8 divides x |^ 3 by A68, INT_1:62;
hence e in {[0,4],[0,(- 4)]} by A62, Lm2, NEWTON02:15; :: thesis: verum
end;
suppose E = 2 ; :: thesis: e in {[0,4],[0,(- 4)]}
then A69: ((y - x) - 4) gcd ((y + x) + 4) = 2 ^2 by A21, A22, WSIERP_1:1;
then A70: x |^ 3 = (4 * m) * (4 * n) by A8, A25, A26
.= 16 * (m * n) ;
then 2 |^ 4 divides x |^ 3 by Lm3;
then A71: 4 divides x by Lm1, Th100;
then consider w being Integer such that
A72: x = 4 * w ;
(x * x) * x = (((16 * 4) * w) * w) * w by A72;
then m * n = 4 * ((w * w) * w) by A70, A14;
then A73: 4 divides m * n ;
A74: 4 divides y + x by A11, A69, INT_2:1;
A75: 2 divides 2 * 2 ;
( ( 4 divides m & n is odd ) or ( 4 divides n & m is odd ) )
proof
assume ( not 4 divides m or n is even ) ; :: thesis: ( 4 divides n & m is odd )
end;
per cases then ( ( 4 divides m & n is odd ) or ( 4 divides n & m is odd ) ) ;
suppose that A82: 4 divides m and
A83: n is odd ; :: thesis: e in {[0,4],[0,(- 4)]}
consider n1 being Integer such that
A84: n = (2 * n1) + 1 by A83, ABIAN:1;
A85: 4 divides 4 * n1 ;
4 divides (2 * (2 * n1)) + (2 * (m + 1)) by A74, A84, A25, A26, A69, A71, INT_2:1;
then A86: 4 divides (2 * m) + (2 * 1) by A85, INT_2:1;
4 divides 2 * m by A82, INT_2:2;
hence e in {[0,4],[0,(- 4)]} by A86, INT_2:1, NAT_D:7; :: thesis: verum
end;
suppose that A87: 4 divides n and
A88: m is odd ; :: thesis: e in {[0,4],[0,(- 4)]}
consider m1 being Integer such that
A89: m = (2 * m1) + 1 by A88, ABIAN:1;
A90: 4 divides 4 * m1 ;
4 divides (2 * (2 * m1)) + (2 * (n + 1)) by A74, A89, A25, A26, A69, A71, INT_2:1;
then A91: 4 divides (2 * n) + (2 * 1) by A90, INT_2:1;
4 divides 2 * n by A87, INT_2:2;
hence e in {[0,4],[0,(- 4)]} by A91, INT_2:1, NAT_D:7; :: thesis: verum
end;
end;
end;
suppose E = 3 ; :: thesis: e in {[0,4],[0,(- 4)]}
then A92: ((y - x) - 4) gcd ((y + x) + 4) = (2 * 2) * 2 by A21, A22, POLYEQ_5:2;
then A93: x |^ 3 = (8 * m) * (8 * n) by A8, A25, A26
.= 64 * (m * n) ;
A94: m * n = ((x / 4) * (x / 4)) * (x / 4) by A14, A93
.= (x / 4) |^ 3 by POLYEQ_5:2 ;
16 divides 16 * 4 ;
then 2 |^ 4 divides x |^ 3 by A93, Lm3, INT_2:2;
then A95: 4 divides x by Lm1, Th100;
then consider a being Integer such that
A96: m = a |^ 3 by A27, A94, A28, Th103;
consider b being Integer such that
A97: n = b |^ 3 by A27, A94, A28, A95, Th103;
A98: a <> 0 by A6, A93, A96;
A99: b <> 0 by A6, A93, A97;
(x / 4) |^ 3 = (a * b) |^ 3 by A94, A96, A97, NEWTON:7;
then x / 4 = a * b by A28, NEWTON03:13;
then A100: (a * b) + 1 = (b |^ 3) - (a |^ 3) by A25, A26, A92, A96, A97;
then A101: a <> b by NEWTON:11;
A102: ( b |^ 3 = (b * b) * b & a |^ 3 = (a * a) * a ) by POLYEQ_5:2;
A103: now :: thesis: not |.(b - a).| < 1
assume |.(b - a).| < 1 ; :: thesis: contradiction
then b - a = 0 by NAT_1:14;
hence contradiction by A101; :: thesis: verum
end;
per cases ( a * b = 0 or a * b > 0 or a * b < 0 ) ;
suppose a * b = 0 ; :: thesis: e in {[0,4],[0,(- 4)]}
hence e in {[0,4],[0,(- 4)]} by A98, A99; :: thesis: verum
end;
suppose A104: a * b > 0 ; :: thesis: e in {[0,4],[0,(- 4)]}
then (a * b) + 1 > 0 + 1 by XREAL_1:8;
then A105: (b - a) * (((b - a) ^2) + ((3 * a) * b)) > 1 by A100, A102;
A106: (a * b) * 3 > 3 * 0 by A104;
then b - a > a - a by XREAL_1:8;
then A107: b - a >= 0 + 1 by NAT_1:13;
then ((b - a) ^2) + ((3 * a) * b) > 0 + ((3 * a) * b) by XREAL_1:6;
then (b - a) * (((b - a) ^2) + ((3 * a) * b)) > 1 * ((3 * a) * b) by A106, A107, XREAL_1:97;
then ((3 * a) * b) - (a * b) < ((a * b) + 1) - (a * b) by A100, A102, XREAL_1:9;
then A108: ((2 * a) * b) / 2 < 1 / 2 by XREAL_1:74;
a * b >= 0 + 1 by A104, NAT_1:13;
hence e in {[0,4],[0,(- 4)]} by A108, XXREAL_0:2; :: thesis: verum
end;
suppose A109: a * b < 0 ; :: thesis: e in {[0,4],[0,(- 4)]}
then A110: |.(a * b).| = - (a * b) by ABSVALUE:def 1;
A111: |.((b |^ 3) - (a |^ 3)).| = |.((b - a) * (((b + a) ^2) - (a * b))).| by A102
.= |.(b - a).| * |.(((b + a) ^2) - (a * b)).| by COMPLEX1:65 ;
A112: 1 * |.(((b + a) ^2) - (a * b)).| <= |.(b - a).| * |.(((b + a) ^2) - (a * b)).| by A103, XREAL_1:64;
0 - (a * b) <= ((b + a) ^2) - (a * b) by XREAL_1:9;
then |.(- (a * b)).| <= |.(((b + a) ^2) - (a * b)).| by A109, TOPREAL6:2;
then A113: - (a * b) <= |.(b - a).| * |.(((b + a) ^2) - (a * b)).| by A110, A112, XXREAL_0:2;
A114: (a * b) + 1 <= 0 by A109, INT_1:7;
(a * b) + 0 < (a * b) + 1 by XREAL_1:8;
hence e in {[0,4],[0,(- 4)]} by A100, A111, A110, A113, A114, Th2; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;
end;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in {[0,4],[0,(- 4)]} or e in { [x,y] where x, y is Integer : y |^ 2 = (x |^ 3) + ((x + 4) |^ 2) } )
assume e in {[0,4],[0,(- 4)]} ; :: thesis: e in { [x,y] where x, y is Integer : y |^ 2 = (x |^ 3) + ((x + 4) |^ 2) }
then A115: ( e = [0,4] or e = [0,(- 4)] ) by TARSKI:def 2;
(- 4) |^ 2 = (0 |^ 3) + ((0 + 4) |^ 2) by WSIERP_1:1;
hence e in { [x,y] where x, y is Integer : y |^ 2 = (x |^ 3) + ((x + 4) |^ 2) } by A115; :: thesis: verum