theorem Th38: :: NAT_3:38

for p being Prime
for a being non zero Nat st p divides a holds
(pfexp a) . p <> 0