let p be Prime; :: thesis: for a being Element of NAT st a <> 0 holds
( 1 <= p |^ (p |-count a) & p |^ (p |-count a) <= a )
let a be Element of NAT ; :: thesis: ( a <> 0 implies ( 1 <= p |^ (p |-count a) & p |^ (p |-count a) <= a ) )
assume A1: a <> 0 ; :: thesis: ( 1 <= p |^ (p |-count a) & p |^ (p |-count a) <= a )
set x = p |^ (p |-count a);
p >= 1 by INT_2:def 4;
hence 1 <= p |^ (p |-count a) by PREPOWER:11; :: thesis: p |^ (p |-count a) <= a
p <> 1 by INT_2:def 4;
then p |^ (p |-count a) divides a by A1, NAT_3:def 7;
hence p |^ (p |-count a) <= a by A1, NAT_D:7; :: thesis: verum