let a, b, c be Nat; :: thesis: ( a is odd & b is odd implies (a |^ 2) + (b |^ 2) <> c |^ 2 )
( a is odd & b is odd & c is even implies (a |^ 2) + (b |^ 2) <> c |^ 2 )
proof
assume A1: ( a is odd & b is odd & c is even ) ; :: thesis: (a |^ 2) + (b |^ 2) <> c |^ 2
then ( 4 divides (a |^ 1) - (b |^ 1) or 4 divides (a |^ 1) + (b |^ 1) ) by Th58;
then 4 divides ((a |^ 1) - (b |^ 1)) * ((a |^ 1) + (b |^ 1)) by INT_2:2;
then 4 divides (a |^ 2) - (b |^ 2) by NEWTON01:1;
then A2: not 4 divides (a |^ 2) + (b |^ 2) by A1, Th58;
2 * 2 divides c * c by A1, LmGCD;
hence (a |^ 2) + (b |^ 2) <> c |^ 2 by A2, NEWTON:81; :: thesis: verum
end;
hence ( a is odd & b is odd implies (a |^ 2) + (b |^ 2) <> c |^ 2 ) ; :: thesis: verum