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 ;
t * z divides ((t + z) |^ (n + 1)) - ((t |^ (n + 1)) + (z |^ (n + 1)))
proof
defpred S1[ Nat] means t * z divides ((t + z) |^ (\$1 + 1)) - ((t |^ (\$1 + 1)) + (z |^ (\$1 + 1)));
A1: S1[ 0 ] by INT_2:12;
A2: for x being Nat st S1[x] holds
S1[x + 1]
proof
let x be Nat; :: thesis: ( S1[x] implies S1[x + 1] )
assume S1[x] ; :: thesis: S1[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 S1[x + 1] by ; :: thesis: verum
end;
for m being Nat holds S1[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