let a, b, c be Nat; :: thesis: ( (a |^ 2) + (b |^ 2) = c |^ 2 implies 3 divides (a * b) * c )
A0: ((a |^ 2) * (b |^ 2)) * (c |^ 2) = ((a * b) |^ 2) * (c |^ 2) by NEWTON:7
.= ((a * b) * c) |^ 2 by NEWTON:7 ;
assume A1: (a |^ 2) + (b |^ 2) = c |^ 2 ; :: thesis: 3 divides (a * b) * c
per cases then ( 3 divides ((a |^ 2) * (b |^ 2)) * (c |^ 2) or ( 3 divides (a |^ 2) - (b |^ 2) & not 3 divides ((a |^ 2) * (b |^ 2)) * (c |^ 2) ) ) by LmAB3;
suppose 3 divides ((a |^ 2) * (b |^ 2)) * (c |^ 2) ; :: thesis: 3 divides (a * b) * c
hence 3 divides (a * b) * c by A0, NAT_3:5, PEPIN:41; :: thesis: verum
end;
suppose ( 3 divides (a |^ 2) - (b |^ 2) & not 3 divides ((a |^ 2) * (b |^ 2)) * (c |^ 2) ) ; :: thesis: 3 divides (a * b) * c
then B2: ( not 3 divides (a |^ 2) * ((b |^ 2) * (c |^ 2)) & not 3 divides (b |^ 2) * ((a |^ 2) * (c |^ 2)) & not 3 divides (c |^ 2) * ((b |^ 2) * (a |^ 2)) ) ;
then ( not 3 divides a |^ 2 & not 3 divides b |^ 2 & not 3 divides c |^ 2 ) by INT_2:2;
then ( not 3 divides a & not 3 divides b & not 3 divides c ) by Th14;
then not 3 divides c * a by INT_5:7, PEPIN:41;
then 3 divides (c + a) * (c - a) by Th50;
then 3 divides (c |^ 2) - (a |^ 2) by NEWTON01:1;
hence 3 divides (a * b) * c by A1, B2, INT_2:2; :: thesis: verum
end;
end;