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

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;

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

per cases ( 3 divides a + b or 3 divides b + (- a) ) by L3;

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

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

end;

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

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

end;

end;