let a, b be Nat; :: thesis: ( not 3 divides a * b implies 3 divides (a + b) * (a - b) )
assume not 3 divides a * b ; :: thesis: 3 divides (a + b) * (a - b)
then ( not 3 gcd a = |.3.| & not 3 gcd b = |.3.| ) by INT_2:2, Th3;
then A3: ( 3,a |^ 2 are_coprime & 3,b |^ 2 are_coprime ) by PEPIN:2, PEPIN:41, WSIERP_1:10;
then 3 gcd (a |^ 2) <> |.3.| ;
then not (a |^ 2) - 0, 0 are_congruent_mod 3 by Th3;
then A4: a |^ 2,1 are_congruent_mod 3 by NAT_6:15;
3 gcd (b |^ 2) <> |.3.| by A3;
then not (b |^ 2) - 0, 0 are_congruent_mod 3 by Th3;
then b |^ 2,1 are_congruent_mod 3 by NAT_6:15;
then (a |^ 2) - (b |^ 2),1 - 1 are_congruent_mod 3 by A4, INT_1:17;
hence 3 divides (a + b) * (a - b) by NEWTON01:1; :: thesis: verum