let m be Nat; :: thesis: for t, z being Integer st m > 0 holds
t * z divides ((t + z) |^ m) - ((t |^ m) + (z |^ m))
let t, z be Integer; :: thesis: ( m > 0 implies t * z divides ((t + z) |^ m) - ((t |^ m) + (z |^ m)) )
assume m > 0 ; :: thesis: t * z divides ((t + z) |^ m) - ((t |^ m) + (z |^ m))
then consider n being Nat such that
A0: m = 1 + n by NAT_1:14, NAT_1:10;
t * z divides ((t + z) |^ (n + 1)) - ((t |^ (n + 1)) + (z |^ (n + 1)))

proof

defpred S₁[ Nat] means t * z divides ((t + z) |^ ($1 + 1)) - ((t |^ ($1 + 1)) + (z |^ ($1 + 1)));
A1: S₁[ 0 ] by INT_2:12;
A2: for x being Nat st S₁[x] holds
S₁[x + 1]

proof

let x be Nat; :: thesis: ( S₁[x] implies S₁[x + 1] )
assume S₁[x] ; :: thesis: S₁[x + 1]
then B2: t * z divides (((t + z) |^ (x + 1)) - ((t |^ (x + 1)) + (z |^ (x + 1)))) * (t + z) by INT_2:2;
B3: (((t + z) |^ (x + 1)) - ((t |^ (x + 1)) + (z |^ (x + 1)))) * (t + z) = ((((((t + z) |^ (x + 1)) * (t + z)) - ((t |^ (x + 1)) * t)) - (z * (t |^ (x + 1)))) - (t * (z |^ (x + 1)))) - ((z |^ (x + 1)) * z)
.= (((((t + z) |^ ((x + 1) + 1)) - ((t |^ (x + 1)) * t)) - (z * (t |^ (x + 1)))) - (t * (z |^ (x + 1)))) - ((z |^ (x + 1)) * z) by NEWTON:6
.= (((((t + z) |^ ((x + 1) + 1)) - (t |^ ((x + 1) + 1))) - (z * (t |^ (x + 1)))) - (t * (z |^ (x + 1)))) - ((z |^ (x + 1)) * z) by NEWTON:6
.= (((((t + z) |^ ((x + 1) + 1)) - (t |^ ((x + 1) + 1))) - (z * ((t |^ x) * t))) - (t * (z |^ (x + 1)))) - ((z |^ (x + 1)) * z) by NEWTON:6
.= (((((t + z) |^ ((x + 1) + 1)) - (t |^ ((x + 1) + 1))) - ((z * (t |^ x)) * t)) - (t * ((z |^ x) * z))) - ((z |^ (x + 1)) * z) by NEWTON:6
.= (((((t + z) |^ ((x + 1) + 1)) - (t |^ ((x + 1) + 1))) - (z * ((t |^ x) * t))) - (t * ((z |^ x) * z))) - (z |^ ((x + 1) + 1)) by NEWTON:6
.= ((((t + z) |^ ((x + 1) + 1)) - (t |^ ((x + 1) + 1))) - (z |^ ((x + 1) + 1))) + ((t * z) * ((- (t |^ x)) - (z |^ x))) ;
t * z divides (t * z) * ((- (t |^ x)) - (z |^ x)) ;
hence S₁[x + 1] by B2, B3, INT_2:1; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A1, A2);
hence t * z divides ((t + z) |^ (n + 1)) - ((t |^ (n + 1)) + (z |^ (n + 1))) ; :: thesis: verum

end;

hence t * z divides ((t + z) |^ m) - ((t |^ m) + (z |^ m)) by A0; :: thesis: verum