let n be Nat; :: thesis: for t, z being Integer st n > 0 holds
t * z divides ((t - z) |^ n) - ((t |^ n) + ((- z) |^ n))
let t, z be Integer; :: thesis: ( n > 0 implies t * z divides ((t - z) |^ n) - ((t |^ n) + ((- z) |^ n)) )
( n > 0 implies t * (- z) divides ((t + (- z)) |^ n) - ((t |^ n) + ((- z) |^ n)) ) by Th17;
then ( n > 0 implies - (t * z) divides ((t + (- z)) |^ n) - ((t |^ n) + ((- z) |^ n)) ) ;
hence ( n > 0 implies t * z divides ((t - z) |^ n) - ((t |^ n) + ((- z) |^ n)) ) by INT_2:10; :: thesis: verum