let k, n be Nat; :: thesis: for a, p being Integer st p |^ ((2 * n) + k) divides a |^ 2 holds
p |^ n divides a
let a, p be Integer; :: thesis: ( p |^ ((2 * n) + k) divides a |^ 2 implies p |^ n divides a )
assume A1: p |^ ((2 * n) + k) divides a |^ 2 ; :: thesis: p |^ n divides a
p |^ (2 * n) divides p |^ ((2 * n) + k) by NAT_1:11, NEWTON89;
then p |^ (2 * n) divides a |^ 2 by A1, INT_2:9;
then A2: (p |^ n) |^ 2 divides a |^ 2 by NEWTON:9;
|.(p |^ n).| |^ 2 = |.((p |^ n) |^ 2).| by TAYLOR_2:1
.= ((p |^ n) |^ 2) gcd (a |^ 2) by A2, NEWTON02:3
.= ((p |^ n) gcd a) |^ 2 by NEWTON027 ;
hence p |^ n divides a by POW1, NEWTON02:3; :: thesis: verum