let n be Nat; :: thesis: for t, z being Integer holds t * z divides (((t + z) |^ n) - ((t - z) |^ n)) + (((- z) |^ n) - (z |^ n))
let t, z be Integer; :: thesis: t * z divides (((t + z) |^ n) - ((t - z) |^ n)) + (((- z) |^ n) - (z |^ n))
A1: ((t + z) |^ n) - ((t |^ n) + (z |^ n)) = (((t + (- z)) |^ n) - ((t |^ n) + ((- z) |^ n))) + ((((t + z) |^ n) - ((t - z) |^ n)) + (((- z) |^ n) - (z |^ n))) ;
per cases ( n = 0 or n > 0 ) ;
suppose n = 0 ; :: thesis: t * z divides (((t + z) |^ n) - ((t - z) |^ n)) + (((- z) |^ n) - (z |^ n))
then ((1 * ((t + z) |^ n)) - (1 * ((t - z) |^ n))) + ((1 * ((- z) |^ n)) - (1 * (z |^ n))) = 0 ;
hence t * z divides (((t + z) |^ n) - ((t - z) |^ n)) + (((- z) |^ n) - (z |^ n)) by INT_2:12; :: thesis: verum
end;
suppose n > 0 ; :: thesis: t * z divides (((t + z) |^ n) - ((t - z) |^ n)) + (((- z) |^ n) - (z |^ n))
then ( t * z divides ((t - z) |^ n) - ((t |^ n) + ((- z) |^ n)) & t * z divides ((t + z) |^ n) - ((t |^ n) + (z |^ n)) ) by Th17, Th19;
hence t * z divides (((t + z) |^ n) - ((t - z) |^ n)) + (((- z) |^ n) - (z |^ n)) by A1, INT_2:1; :: thesis: verum
end;
end;