let a be Integer; :: thesis: for m, n being Nat st m >= n holds
a |^ n divides a |^ m
let m, n be Nat; :: thesis: ( m >= n implies a |^ n divides a |^ m )
A1: ( |.(a |^ n).| = |.a.| |^ n & |.(a |^ m).| = |.a.| |^ m ) by TAYLOR_2:1;
assume m >= n ; :: thesis: a |^ n divides a |^ m
hence a |^ n divides a |^ m by INT_2:16, A1, NEWTON:89; :: thesis: verum