let b, a be natural number ; :: thesis: ( b <> 1 implies ( ( a <> 0 & b |-count a = 0 ) iff not b divides a ) )
assume A1: b <> 1 ; :: thesis: ( ( a <> 0 & b |-count a = 0 ) iff not b divides a )
thus ( a <> 0 & b |-count a = 0 implies not b divides a ) :: thesis: ( not b divides a implies ( a <> 0 & b |-count a = 0 ) )

proof

assume that
A2: a <> 0 and
A3: b |-count a = 0 and
A4: b divides a ; :: thesis: contradiction
not b |^ (0 + 1) divides a by A1, A2, A3, Def7;
hence contradiction by A4, NEWTON:10; :: thesis: verum

end;

assume A5: not b divides a ; :: thesis: ( a <> 0 & b |-count a = 0 )
then A6: not b |^ (0 + 1) divides a by NEWTON:10;
A7: a <> 0 by A5, NAT_D:6;
1 divides a by NAT_D:6;
then b |^ 0 divides a by NEWTON:9;
hence ( a <> 0 & b |-count a = 0 ) by A1, A6, A7, Def7; :: thesis: verum