let a, b be non zero Nat; for n being odd Nat holds ((a |^ (n + 2)) + (b |^ (n + 2))) / (a + b) = ((a |^ (n + 1)) + (b |^ (n + 1))) - ((a * b) * (((a |^ n) + (b |^ n)) / (a + b)))
let n be odd Nat; ((a |^ (n + 2)) + (b |^ (n + 2))) / (a + b) = ((a |^ (n + 1)) + (b |^ (n + 1))) - ((a * b) * (((a |^ n) + (b |^ n)) / (a + b)))
reconsider m = (n - 1) / 2 as Nat ;
(a |^ (((2 * m) + 1) + 2)) + (b |^ (((2 * m) + 1) + 2)) = ((a + b) * ((a |^ (((2 * m) + 1) + 1)) + (b |^ (((2 * m) + 1) + 1)))) - ((a * b) * ((a |^ ((2 * m) + 1)) + (b |^ ((2 * m) + 1))))
by RI3;
then ((a |^ (((2 * m) + 1) + 2)) + (b |^ (((2 * m) + 1) + 2))) / (a + b) =
(((a + b) * ((a |^ (((2 * m) + 1) + 1)) + (b |^ (((2 * m) + 1) + 1)))) / (a + b)) - (((a * b) * ((a |^ ((2 * m) + 1)) + (b |^ ((2 * m) + 1)))) / (a + b))
by XCMPLX_1:120
.=
((a |^ (((2 * m) + 1) + 1)) + (b |^ (((2 * m) + 1) + 1))) - (((a * b) * ((a |^ ((2 * m) + 1)) + (b |^ ((2 * m) + 1)))) / (a + b))
by XCMPLX_1:89
.=
((a |^ (((2 * m) + 1) + 1)) + (b |^ (((2 * m) + 1) + 1))) - ((a * b) * (((a |^ ((2 * m) + 1)) + (b |^ ((2 * m) + 1))) / (a + b)))
by XCMPLX_1:74
;
hence
((a |^ (n + 2)) + (b |^ (n + 2))) / (a + b) = ((a |^ (n + 1)) + (b |^ (n + 1))) - ((a * b) * (((a |^ n) + (b |^ n)) / (a + b)))
; verum