let a, b, n be Nat; :: thesis: ( n > 0 & a - b divides (a |^ n) - (b |^ n) implies a - b divides (a |^ (n + 1)) - (b |^ (n + 1)) )
assume A1: ( n > 0 & a - b divides (a |^ n) - (b |^ n) ) ; :: thesis: a - b divides (a |^ (n + 1)) - (b |^ (n + 1))
consider q being Integer such that
A3: (a |^ n) - (b |^ n) = (a - b) * q by A1;
per cases ( a - b is even or a - b is odd ) ;
suppose a - b is even ; :: thesis: a - b divides (a |^ (n + 1)) - (b |^ (n + 1))
then A5: ( a + b is even & (a |^ n) + (b |^ n) is even & (a |^ n) - (b |^ n) is even ) by Lm18e;
then consider l being Integer such that
A6: a + b = 2 * l ;
consider k being Integer such that
A7: (a |^ n) + (b |^ n) = 2 * k by A5;
(a |^ (n + 1)) - (b |^ (n + 1)) = (((2 * k) * (a - b)) + ((2 * l) * ((a |^ n) - (b |^ n)))) / 2 by Th13, A6, A7
.= (k * (a - b)) + (l * ((a |^ n) - (b |^ n)))
.= (k * (a - b)) + (l * ((a - b) * q)) by A3
.= (a - b) * (k + (l * q)) ;
hence a - b divides (a |^ (n + 1)) - (b |^ (n + 1)) ; :: thesis: verum
end;
suppose A12: a - b is odd ; :: thesis: a - b divides (a |^ (n + 1)) - (b |^ (n + 1))
then A13: ( a + b is odd & (a |^ n) + (b |^ n) is odd & (a |^ n) - (b |^ n) is odd & (a |^ (n + 1)) - (b |^ (n + 1)) is odd ) by A1, Lm18d;
q is odd by A3, A1, A12, Lm18d;
then consider m being Integer such that
A18: 2 * m = ((a |^ n) + (b |^ n)) + ((a + b) * q) by A13, ABIAN:11;
(a |^ (n + 1)) - (b |^ (n + 1)) = ((((a |^ n) + (b |^ n)) * (a - b)) + ((a + b) * ((a - b) * q))) / 2 by Th13, A3
.= ((a - b) * (((a |^ n) + (b |^ n)) + ((a + b) * q))) / 2
.= ((a - b) * (2 * m)) / 2 by A18
.= (a - b) * m ;
hence a - b divides (a |^ (n + 1)) - (b |^ (n + 1)) ; :: thesis: verum
end;
end;