let a be Nat; :: thesis: for p being Prime st a <> 1 & a <> p holds
a |-count p = 0
let p be Prime; :: thesis: ( a <> 1 & a <> p implies a |-count p = 0 )
assume that
A1: a <> 1 and
A2: a <> p ; :: thesis: a |-count p = 0
a |^ 0 = 1 by NEWTON:4;
then A3: a |^ 0 divides p by NAT_D:6;
not a |^ (0 + 1) divides p by A1, A2, INT_2:def 4;
hence a |-count p = 0 by A1, A3, Def7; :: thesis: verum