let a be non zero Integer; :: thesis: for b being non trivial Nat holds
( b |-count a = 0 iff not b divides a )
let b be non trivial Nat; :: thesis: ( b |-count a = 0 iff not b divides a )
reconsider c = |.a.| as non zero Nat ;
b > 1 by Def0;
then ( not b divides |.a.| iff b |-count |.a.| = 0 ) by NAT_3:27;
hence ( b |-count a = 0 iff not b divides a ) by INT_2:16; :: thesis: verum