let n, i be Nat; :: thesis: for p being Prime st n <> 0 & p |^ i divides n holds
i <= p |-count n
let p be Prime; :: thesis: ( n <> 0 & p |^ i divides n implies i <= p |-count n )
assume A0: n <> 0 ; :: thesis: ( not p |^ i divides n or i <= p |-count n )
assume A1: p |^ i divides n ; :: thesis: i <= p |-count n
reconsider b = p |^ i as non zero Nat ;
reconsider a = n as non zero Nat by A0;
p |-count b <= p |-count a by A1, NAT_3:30;
hence i <= p |-count n by NAT_3:25, INT_2:def 4; :: thesis: verum