let b, a be natural number ; :: thesis: ( b <> 1 & a <> 0 & b divides b |^ (b |-count a) implies b divides a )
assume that
A1: b <> 1 and
A2: a <> 0 and
A3: b divides b |^ (b |-count a) ; :: thesis: b divides a
b |^ (b |-count a) divides a by A1, A2, Def7;
hence b divides a by A3, NAT_D:4; :: thesis: verum