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