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 )

( a is odd & b is odd & c is even implies (a |^ 2) + (b |^ 2) <> c |^ 2 )

proof

hence
( a is odd & b is odd implies (a |^ 2) + (b |^ 2) <> c |^ 2 )
; :: thesis: verum
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;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