given q, s, t being Prime such that A1: q ^2 = (s ^2) + (t ^2) ; :: thesis: contradiction

per cases ( ( s is even & t is odd ) or ( s is odd & t is even ) ) by A1, Th38;

suppose that A2: s is even and
t is odd ; :: thesis: contradiction

s = 2 by A2, LAGRA4SQ:13;
then (q ^2) - (t ^2) = 4 by A1;
hence contradiction by Th35; :: thesis: verum

end;

suppose that s is odd and
A3: t is even ; :: thesis: contradiction

t = 2 by A3, LAGRA4SQ:13;
then (q ^2) - (s ^2) = 4 by A1;
hence contradiction by Th35; :: thesis: verum

end;

end;