let a, b be Nat; :: thesis: ( 3 divides ((a + b) * (a - b)) + (a * b) implies 3 divides a )
assume A1: 3 divides ((a + b) * (a - b)) + (a * b) ; :: thesis: 3 divides a
L1: 3 divides a * b

proof

assume A2: not 3 divides a * b ; :: thesis: contradiction
then 3 divides (a + b) * (a - b) by Th50;
hence contradiction by A1, A2, INT_2:1; :: thesis: verum

end;

L2: 3 divides (a + b) * (a - b)

proof

assume A2: not 3 divides (a + b) * (a - b) ; :: thesis: contradiction
then 3 divides a * b by Th50;
hence contradiction by A1, A2, INT_2:1; :: thesis: verum

end;

assume C1: not 3 divides a ; :: thesis: contradiction
then C2: 3 divides b by L1, NAT_6:7, PEPIN:41;
then C3: 3 divides - b by INT_2:10;

per cases ( 3 divides a + b or 3 divides a + (- b) ) by L2, INT_5:7, PEPIN:41;

suppose 3 divides a + b ; :: thesis: contradiction

hence contradiction by C1, C2, INT_2:1; :: thesis: verum

end;

suppose 3 divides a + (- b) ; :: thesis: contradiction

hence contradiction by C1, C3, INT_2:1; :: thesis: verum

end;

end;