let m be Nat; :: thesis: for p being Prime holds
( m divides p |^ 4 iff m in {1,p,(p |^ 2),(p |^ 3),(p |^ 4)} )
let p be Prime; :: thesis: ( m divides p |^ 4 iff m in {1,p,(p |^ 2),(p |^ 3),(p |^ 4)} )
thus ( m divides p |^ 4 implies m in {1,p,(p |^ 2),(p |^ 3),(p |^ 4)} ) :: thesis: ( m in {1,p,(p |^ 2),(p |^ 3),(p |^ 4)} implies m divides p |^ 4 )

proof

assume m divides p |^ 4 ; :: thesis: m in {1,p,(p |^ 2),(p |^ 3),(p |^ 4)}
then consider r being Nat such that
A1: m = p |^ r and
A2: r <= 4 by GROUPP_1:2;
not not r = 0 & ... & not r = 4 by A2;
then ( m = 1 or m = p or m = p |^ 2 or m = p |^ 3 or m = p |^ 4 ) by A1, NEWTON:4;
hence m in {1,p,(p |^ 2),(p |^ 3),(p |^ 4)} by ENUMSET1:def 3; :: thesis: verum

end;

assume m in {1,p,(p |^ 2),(p |^ 3),(p |^ 4)} ; :: thesis: m divides p |^ 4
then ( m = 1 or m = p |^ 1 or m = p |^ 2 or m = p |^ 3 or m = p |^ 4 ) by ENUMSET1:def 3;
hence m divides p |^ 4 by INT_2:12, NEWTON:89; :: thesis: verum