let a be Integer; :: thesis: for b being non zero Integer holds
( not b divides a iff (a mod b) + ((- a) mod b) = b )
let b be non zero Integer; :: thesis: ( not b divides a iff (a mod b) + ((- a) mod b) = b )
A2: ( a mod b = a - ((a div b) * b) & (- a) mod b = (- a) - (((- a) div b) * b) ) by INT_1:def 10;
thus ( not b divides a implies (a mod b) + ((- a) mod b) = b ) :: thesis: ( (a mod b) + ((- a) mod b) = b implies not b divides a )

proof

assume not b divides a ; :: thesis: (a mod b) + ((- a) mod b) = b
then (- b) * (- 1) = (- b) * ((a div b) + ((- a) div b)) by DIV
.= (a - ((a div b) * b)) + ((- a) - (((- a) div b) * b)) ;
hence (a mod b) + ((- a) mod b) = b by A2; :: thesis: verum

end;

( b divides a implies (a mod b) + ((- a) mod b) = 0 )

proof

assume b divides a ; :: thesis: (a mod b) + ((- a) mod b) = 0
then ( a mod b = 0 & (- a) mod b = 0 ) by INT162, INT_2:10;
hence (a mod b) + ((- a) mod b) = 0 ; :: thesis: verum

end;

hence ( (a mod b) + ((- a) mod b) = b implies not b divides a ) ; :: thesis: verum