:: deftheorem Def6 defines |-count NEWTON03:def 7 :
for a being Integer st |.a.| <> 1 holds
for b being non zero Integer
for b₃ being Nat holds
( b₃ = a |-count b iff ( a |^ b₃ divides b & not a |^ (b₃ + 1) divides b ) );