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 S1[ Nat] means ( t divides ((t + z) |^ $1) - (z |^ $1) & z divides ((t + z) |^ $1) - (t |^ $1) );
A1: S1[ 0 ]
proof
( (t + z) |^ 0 = 1 & z |^ 0 = 1 & t |^ 0 = 1 ) by NEWTON:4;
hence S1[ 0 ] by INT_1:def 4, INT_1:11; :: thesis: verum
end;
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 A2a: S1[x] ; :: thesis: S1[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 S1[x + 1] by A3, A7; :: thesis: verum
end;
for m being Nat holds S1[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