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