let a be non zero Nat; :: thesis: for p being non trivial Nat holds
( p |^ (p |-count a) divides a & not p * (p |^ (p |-count a)) divides a )
let p be non trivial Nat; :: thesis: ( p |^ (p |-count a) divides a & not p * (p |^ (p |-count a)) divides a )
( a <> 0 & p <> 1 ) by NAT_2:def 1;
then ( p |^ (p |-count a) divides a & not p |^ ((p |-count a) + 1) divides a ) by NAT_3:def 7;
hence ( p |^ (p |-count a) divides a & not p * (p |^ (p |-count a)) divides a ) by NEWTON:6; :: thesis: verum