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