let n be Nat; :: thesis: for a, b being Integer holds (a * b) * (a - b) divides ((a - b) * ((a + b) |^ n)) - ((a |^ (n + 1)) - (b |^ (n + 1)))
let a, b be Integer; :: thesis: (a * b) * (a - b) divides ((a - b) * ((a + b) |^ n)) - ((a |^ (n + 1)) - (b |^ (n + 1)))
A0: ( len ((a,b) In_Power ((n + 1) - 1)) = n + 1 & len ((a,b) Subnomial ((n + 1) - 1)) = n + 1 ) ;
reconsider R1 = (a,b) In_Power n as Element of (n + 1) -tuples_on REAL by A0, FINSEQ_2:92;
reconsider R2 = (a,b) Subnomial n as Element of (n + 1) -tuples_on REAL by A0, FINSEQ_2:92;
A1: Sum (((a,b) In_Power n) - ((a,b) Subnomial n)) = Sum (R1 - R2)
.= (Sum ((a,b) In_Power n)) - (Sum ((a,b) Subnomial n)) by RVSUM_1:90 ;
reconsider f = ((a,b) In_Power n) - ((a,b) Subnomial n) as INT -valued FinSequence ;
for i being Nat st i in dom f holds
a * b divides (((a,b) In_Power n) - ((a,b) Subnomial n)) . i
proof
let i be Nat; :: thesis: ( i in dom f implies a * b divides (((a,b) In_Power n) - ((a,b) Subnomial n)) . i )
assume B1: i in dom f ; :: thesis: a * b divides (((a,b) In_Power n) - ((a,b) Subnomial n)) . i
a * b divides (((a,b) In_Power n) . i) - (((a,b) Subnomial n) . i) by DIS;
hence a * b divides (((a,b) In_Power n) - ((a,b) Subnomial n)) . i by B1, VALUED_1:13; :: thesis: verum
end;
then A2: a * b divides Sum (((a,b) In_Power n) - ((a,b) Subnomial n)) by INT436;
((a - b) * ((a + b) |^ n)) - ((a |^ (n + 1)) - (b |^ (n + 1))) = ((a - b) * ((a + b) |^ n)) - ((a - b) * (Sum ((a,b) Subnomial n))) by SumS
.= ((a - b) * (Sum ((a,b) In_Power n))) - ((a - b) * (Sum ((a,b) Subnomial n))) by NEWTON:30
.= (a - b) * ((Sum ((a,b) In_Power n)) - (Sum ((a,b) Subnomial n))) ;
hence (a * b) * (a - b) divides ((a - b) * ((a + b) |^ n)) - ((a |^ (n + 1)) - (b |^ (n + 1))) by A1, A2, NEWTON02:2; :: thesis: verum