let n be Nat; for u, z being Integer holds
( u divides (u + z) |^ n iff u divides z |^ n )
let u, z be Integer; ( u divides (u + z) |^ n iff u divides z |^ n )
A0:
u divides ((u + z) |^ n) - (z |^ n)
by Th10;
consider t being Integer such that
A1:
t = - (z |^ n)
;
A2:
u divides ((u + z) |^ n) + t
by A0, A1;
then A3:
( u divides t implies u divides (u + z) |^ n )
by INT_2:1;
( u divides (u + z) |^ n implies u divides t )
by INT_2:1, A2;
hence
( u divides (u + z) |^ n iff u divides z |^ n )
by A1, A3, INT_2:10; verum