let x, y, z, t be Nat; :: thesis: ( not x,y are_coprime or (x ^2) + (5 * (y ^2)) <> z ^2 or (5 * (x ^2)) + (y ^2) <> t ^2 )
assume A1: x,y are_coprime ; :: thesis: ( (x ^2) + (5 * (y ^2)) <> z ^2 or (5 * (x ^2)) + (y ^2) <> t ^2 )
assume A2: ( (x ^2) + (5 * (y ^2)) = z ^2 & (5 * (x ^2)) + (y ^2) = t ^2 ) ; :: thesis: contradiction
A3: ( z |^ 2 = z ^2 & t |^ 2 = t ^2 ) by WSIERP_1:1;
A4: ( x |^ 2 = x ^2 & y |^ 2 = y ^2 ) by WSIERP_1:1;
3 divides 3 * (2 * ((x ^2) + (y ^2))) ;
then 3 divides (z ^2) + (t ^2) by A2;
then ( 3 divides z & 3 divides t ) by A3, NEWTON02:189;
then ( 3 * 3 divides z ^2 & 3 * 3 divides t ^2 ) by NAT_3:1;
then 9 divides (z ^2) + (t ^2) by NAT_D:8;
then consider a being Nat such that
A5: 6 * ((x ^2) + (y ^2)) = 9 * a by A2;
(x ^2) + (y ^2) = (3 / 2) * a by A5;
then consider b being Nat such that
A6: a = 2 * b by Th5, XPRIMES1:2, XPRIMES1:3, INT_2:30;
2 * ((x ^2) + (y ^2)) = 2 * (3 * b) by A5, A6;
then 3 divides (x ^2) + (y ^2) ;
then ( 3 divides x & 3 divides y ) by A4, NEWTON02:189;
hence contradiction by A1, PYTHTRIP:def 1; :: thesis: verum