let a, b, m be Nat; a + b divides (a |^ ((2 * m) + 1)) + (b |^ ((2 * m) + 1))
A2:
(a |^ ((2 * m) + 2)) - (b |^ ((2 * m) + 2)) = (((a |^ ((2 * m) + 1)) + (b |^ ((2 * m) + 1))) * (a - b)) + ((a * b) * ((a |^ (2 * m)) - (b |^ (2 * m))))
by Th21;
set n = m + 1;
consider t being Integer such that
A4:
(a |^ (2 * m)) - (b |^ (2 * m)) = ((a |^ 2) - (b |^ 2)) * t
by Th33, INT_1:def 3;
consider z being Integer such that
A4a:
(a |^ (2 * (m + 1))) - (b |^ (2 * (m + 1))) = ((a |^ 2) - (b |^ 2)) * z
by Th33, INT_1:def 3;
A5: (a - b) * ((a |^ ((2 * m) + 1)) + (b |^ ((2 * m) + 1))) =
((a |^ ((2 * m) + 2)) - (b |^ ((2 * m) + 2))) - ((a * b) * ((a |^ (2 * m)) - (b |^ (2 * m))))
by A2
.=
((a |^ (2 * (m + 1))) - (b |^ (2 * (m + 1)))) - ((a * b) * (((a |^ 2) - (b |^ 2)) * t))
by A4
.=
((a |^ 2) - (b |^ 2)) * (z - ((a * b) * t))
by A4a
.=
((a - b) * (a + b)) * (z - ((a * b) * t))
by Th1
.=
(a - b) * ((a + b) * (z - ((a * b) * t)))
;
X:
2 * a = a + a
;
( (a |^ ((2 * m) + 1)) + (b |^ ((2 * m) + 1)) = (a + b) * (z - ((a * b) * t)) or a - b = 0 )
by A5, XCMPLX_1:5;
hence
a + b divides (a |^ ((2 * m) + 1)) + (b |^ ((2 * m) + 1))
by Lm46, X; verum