let n, m be natural number ; :: thesis: for p being Prime st n <> 0 & m <= p |-count n holds
p |^ m divides n
let p be Prime; :: thesis: ( n <> 0 & m <= p |-count n implies p |^ m divides n )
assume that
A1: n <> 0 and
A2: m <= p |-count n ; :: thesis: p |^ m divides n
A3: p |^ m divides p |^ (p |-count n) by A2, RADIX_1:7;
p > 1 by INT_2:def 5;
then p |^ (p |-count n) divides n by A1, NAT_3:def 7;
hence p |^ m divides n by A3, NAT_D:4; :: thesis: verum