let a, b be Nat; :: thesis: ( b <> 1 implies ( ( a <> 0 & b |-count a = 0 ) iff not b divides a ) )
1 divides a by NAT_D:6;
then A1: b |^ 0 divides a by NEWTON:4;
assume A2: 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
A3: ( a <> 0 & b |-count a = 0 ) and
A4: b divides a ; :: thesis: contradiction
not b |^ (0 + 1) divides a by A2, A3, Def7;
hence contradiction by A4; :: thesis: verum

end;

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