let a, b, n be Nat; :: thesis: ( a divides b implies (n |^ a) - 1 divides (n |^ b) - 1 )
given m being Nat such that A1: b = a * m ; :: according to NAT_D:def 3 :: thesis: (n |^ a) - 1 divides (n |^ b) - 1
(n |^ a) - 1 divides ((n |^ a) |^ m) - (1 |^ m) by NEWTON01:33;
hence (n |^ a) - 1 divides (n |^ b) - 1 by A1, NEWTON:9; :: thesis: verum