given x, y, z, t being Nat such that A1: (x ^2) + (2 * (y ^2)) = z ^2 and
A2: (2 * (x ^2)) + (y ^2) = t ^2 and
A3: x,y are_coprime ; :: thesis: contradiction
A4: (2 * (x ^2)) mod 4 = ((2 mod 4) * ((x ^2) mod 4)) mod 4 by NAT_D:67;
A5: (2 * (y ^2)) mod 4 = ((2 mod 4) * ((y ^2) mod 4)) mod 4 by NAT_D:67;
A6: 2 mod 4 = 2 by NAT_D:24;

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

suppose ( x is even & y is even ) ; :: thesis: contradiction

hence contradiction by A3, NEWTON05:35; :: thesis: verum

end;

suppose ( x is odd & y is odd ) ; :: thesis: contradiction

then ( (x ^2) mod 4 = 1 & (y ^2) mod 4 = 1 ) by PYTHTRIP:4;
then ((x ^2) + (2 * (y ^2))) mod 4 = (1 + (2 * 1)) mod 4 by A5, A6, NAT_D:66
.= 3 by NAT_D:24 ;
hence contradiction by A1, PYTHTRIP:3, PYTHTRIP:4; :: thesis: verum

end;

suppose ( x is even & y is odd ) ; :: thesis: contradiction

then ( (x ^2) mod 4 = 0 & (y ^2) mod 4 = 1 ) by PYTHTRIP:3, PYTHTRIP:4;
then ((x ^2) + (2 * (y ^2))) mod 4 = (0 + (2 * 1)) mod 4 by A5, A6, NAT_D:66
.= 2 by NAT_D:24 ;
hence contradiction by A1, PYTHTRIP:3, PYTHTRIP:4; :: thesis: verum

end;

suppose ( x is odd & y is even ) ; :: thesis: contradiction

then ( (x ^2) mod 4 = 1 & (y ^2) mod 4 = 0 ) by PYTHTRIP:3, PYTHTRIP:4;
then ((2 * (x ^2)) + (y ^2)) mod 4 = ((2 * 1) + 0) mod 4 by A4, A6, NAT_D:66
.= 2 by NAT_D:24 ;
hence contradiction by A2, PYTHTRIP:3, PYTHTRIP:4; :: thesis: verum

end;

end;