let x be Nat; :: thesis: for t, z being Integer st t divides ((t + z) |^ x) - (z |^ x) holds
t divides (((t + z) |^ x) * z) - (z |^ (x + 1))
let t, z be Integer; :: thesis: ( t divides ((t + z) |^ x) - (z |^ x) implies t divides (((t + z) |^ x) * z) - (z |^ (x + 1)) )
assume t divides ((t + z) |^ x) - (z |^ x) ; :: thesis: t divides (((t + z) |^ x) * z) - (z |^ (x + 1))
then t divides (((t + z) |^ x) - (z |^ x)) * z by INT_2:2;
then t divides (((t + z) |^ x) * z) - ((z |^ x) * z) ;
hence t divides (((t + z) |^ x) * z) - (z |^ (x + 1)) by NEWTON:6; :: thesis: verum