let x, y, z, t be Nat; :: thesis: ( not x,y are_coprime or (x ^2) + (6 * (y ^2)) <> z ^2 or (6 * (x ^2)) + (y ^2) <> t ^2 )
assume A1: x,y are_coprime ; :: thesis: ( (x ^2) + (6 * (y ^2)) <> z ^2 or (6 * (x ^2)) + (y ^2) <> t ^2 )
assume A2: ( (x ^2) + (6 * (y ^2)) = z ^2 & (6 * (x ^2)) + (y ^2) = t ^2 ) ; :: thesis: contradiction
then 7 * ((x ^2) + (y ^2)) = (z ^2) + (t ^2) ;
then 7 divides (z ^2) + (t ^2) ;
then A3: ( 7 divides z & 7 divides t ) by NUMBER02:52;
then 7 divides z + t by NAT_D:8;
then A4: 7 * 7 divides (z + t) * (z + t) by NAT_3:1;
A5: 7 * 7 divides z * t by A3, NAT_3:1;
z * t divides 2 * (z * t) ;
then 7 * 7 divides 2 * (z * t) by A5, INT_2:9;
then 7 * 7 divides ((7 * ((x ^2) + (y ^2))) + ((2 * z) * t)) - (2 * (z * t)) by A2, A4, INT_5:1;
then 7 divides (x ^2) + (y ^2) by INT_4:7;
then ( 7 divides x & 7 divides y ) by NUMBER02:52;
hence contradiction by A1, PYTHTRIP:def 1; :: thesis: verum