:: deftheorem Def7 defines |-count NAT_3:def 7 :
for n, d being Nat st d <> 1 & n <> 0 holds
for b₃ being Nat holds
( b₃ = d |-count n iff ( d |^ b₃ divides n & not d |^ (b₃ + 1) divides n ) );