let p be Prime; :: thesis: for a being non zero Nat st p divides a holds
(pfexp a) . p <> 0
let a be non zero Nat; :: thesis: ( p divides a implies (pfexp a) . p <> 0 )
assume p divides a ; :: thesis: (pfexp a) . p <> 0
then A1: p |^ (0 + 1) divides a ;
( (pfexp a) . p = p |-count a & p <> 1 ) by Def8, INT_2:def 4;
hence (pfexp a) . p <> 0 by A1, Def7; :: thesis: verum