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

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;

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

L1: 3 divides a * b

proof

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

then
( 3 divides a + b or 3 divides a - b )
by INT_5:7, PEPIN:41;
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 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;