let a, b be Nat; ( not 3 divides a * b implies 3 divides (a + b) * (a - b) )
assume
not 3 divides a * b
; 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; verum