let x, y, z be Nat; :: thesis: ( x,y are_coprime & (x |^ 2) + (y |^ 2) = z |^ 4 implies 7 divides x * y )
assume A1: x,y are_coprime ; :: thesis: ( not (x |^ 2) + (y |^ 2) = z |^ 4 or 7 divides x * y )
then ( x is odd or y is odd ) by NEWTON05:35;
hence ( not (x |^ 2) + (y |^ 2) = z |^ 4 or 7 divides x * y ) by A1, Lm1; :: thesis: verum