let p be Prime; :: thesis: for a being non empty natural number st p divides a holds
(pfexp a) . p <> 0
let a be non empty natural number ; :: 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 by NEWTON:10;
( (pfexp a) . p = p |-count a & p <> 1 ) by Def8, INT_2:def 5;
hence (pfexp a) . p <> 0 by A1, Def7; :: thesis: verum