let n be Nat; :: thesis: for a being non trivial Nat
for p being prime Nat st a divides p |^ n holds
p divides a
let a be non trivial Nat; :: thesis: for p being prime Nat st a divides p |^ n holds
p divides a
let p be prime Nat; :: thesis: ( a divides p |^ n implies p divides a )
assume a divides p |^ n ; :: thesis: p divides a
then A1: a gcd (p |^ n) = |.a.| by NEWTON02:3;
per cases ( a gcd p = 1 or a gcd p = p ) by GCDP;
suppose a gcd p = 1 ; :: thesis: p divides a
then a gcd (p |^ n) = 1 by WSIERP_1:12;
hence p divides a by A1, Def0; :: thesis: verum
end;
suppose a gcd p = p ; :: thesis: p divides a
hence p divides a by INT_2:def 2; :: thesis: verum
end;
end;