let n be Nat; :: thesis: for t, z being Integer holds
( t divides ((t + z) |^ n) - (z |^ n) & z divides ((t + z) |^ n) - (t |^ n) )
let t, z be Integer; :: thesis: ( t divides ((t + z) |^ n) - (z |^ n) & z divides ((t + z) |^ n) - (t |^ n) )
defpred S₁[ Nat] means ( t divides ((t + z) |^ $1) - (z |^ $1) & z divides ((t + z) |^ $1) - (t |^ $1) );
A1: S₁[ 0 ]

proof

( (t + z) |^ 0 = 1 & z |^ 0 = 1 & t |^ 0 = 1 ) by NEWTON:4;
hence S₁[ 0 ] by INT_1:def 4, INT_1:11; :: thesis: verum

end;

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 A2a: S₁[x] ; :: thesis: S₁[x + 1]
then A4: t divides (((t + z) |^ x) * z) - (z |^ (x + 1)) by Lm2;
A5: z divides (((t + z) |^ x) * t) - (t |^ (x + 1)) by Lm2, A2a;
A6: ( t divides ((t + z) |^ x) * t & z divides ((t + z) |^ x) * z ) ;
then A7: t divides (((t + z) |^ x) * t) + ((((t + z) |^ x) * z) - (z |^ (x + 1))) by WSIERP_1:4, A4;
A3: (t + z) |^ (x + 1) = ((t + z) |^ x) * ((t + z) |^ 1) by NEWTON:8
.= (((t + z) |^ x) * t) + (((t + z) |^ x) * z) ;
z divides (((t + z) |^ x) * z) + ((((t + z) |^ x) * t) - (t |^ (x + 1))) by WSIERP_1:4, A5, A6;
hence S₁[x + 1] by A3, A7; :: thesis: verum

end;

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