let n be non zero Nat; :: thesis: for a, b being Integer holds
( b |^ n divides a |^ n iff b divides a )
let a, b be Integer; :: thesis: ( b |^ n divides a |^ n iff b divides a )
thus ( b |^ n divides a |^ n implies b divides a ) :: thesis: ( b divides a implies b |^ n divides a |^ n )

proof

assume A1: b |^ n divides a |^ n ; :: thesis: b divides a
|.b.| |^ n = |.(b |^ n).| by TAYLOR_2:1
.= (b |^ n) gcd (a |^ n) by A1, NEWTON02:3
.= (b gcd a) |^ n by NEWTON027 ;
hence b divides a by NEWTON02:3, WSIERP_1:3; :: thesis: verum

end;

thus ( b divides a implies b |^ n divides a |^ n ) by NEWTON02:15; :: thesis: verum