let n be Nat; 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; (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
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; verum