let n be Nat; :: thesis: for t, z being Integer holds t * z divides ((t - z) |^ ((2 * n) + 1)) - ((t |^ ((2 * n) + 1)) - (z |^ ((2 * n) + 1)))
let t, z be Integer; :: thesis: t * z divides ((t - z) |^ ((2 * n) + 1)) - ((t |^ ((2 * n) + 1)) - (z |^ ((2 * n) + 1)))
A1: (- z) |^ ((2 * n) + 1) = - (z |^ ((2 * n) + 1)) by POWER:2;
t * z divides ((t - z) |^ ((2 * n) + 1)) - ((t |^ ((2 * n) + 1)) + ((- z) |^ ((2 * n) + 1))) by Th19;
hence t * z divides ((t - z) |^ ((2 * n) + 1)) - ((t |^ ((2 * n) + 1)) - (z |^ ((2 * n) + 1))) by A1; :: thesis: verum