let a be Integer; :: thesis: for b being non zero Integer holds
( b divides a iff a mod b = 0 )
let b be non zero Integer; :: thesis: ( b divides a iff a mod b = 0 )
( a, 0 are_congruent_mod b iff a mod b = 0 mod b ) by NAT_D:64;
hence ( b divides a iff a mod b = 0 ) ; :: thesis: verum