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

then C2: 3 divides b by L1, NAT_6:7, PEPIN:41;

then C3: 3 divides - b by INT_2:10;

assume A1: 3 divides ((a + b) * (a - b)) + (a * b) ; :: thesis: 3 divides a

L1: 3 divides a * b

proof

L2:
3 divides (a + b) * (a - b)
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;then 3 divides (a + b) * (a - b) by Th50;

hence contradiction by A1, A2, INT_2:1; :: thesis: verum

proof

assume C1:
not 3 divides a
; :: thesis: contradiction
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 by Th50;

hence contradiction by A1, A2, INT_2:1; :: thesis: verum

then C2: 3 divides b by L1, NAT_6:7, PEPIN:41;

then C3: 3 divides - b by INT_2:10;