let c, m be Nat; :: thesis: for a, b being Integer st a divides b & b |^ m divides c holds
a |^ m divides c
let a, b be Integer; :: thesis: ( a divides b & b |^ m divides c implies a |^ m divides c )
assume A1: ( a divides b & b |^ m divides c ) ; :: thesis: a |^ m divides c
then a gcd b = |.a.| by NEWTON02:3;
then (a |^ m) gcd (b |^ m) = |.a.| |^ m by NEWTON027
.= |.(a |^ m).| by TAYLOR_2:1 ;
then a |^ m divides b |^ m by NEWTON02:3;
hence a |^ m divides c by A1, INT_2:9; :: thesis: verum