let a, b, n be Nat; :: thesis: ( a + b divides (a |^ n) + (b |^ n) or a + b divides (a |^ n) - (b |^ n) )

per cases ( n is odd or n is even ) ;

suppose n is odd ; :: thesis: ( a + b divides (a |^ n) + (b |^ n) or a + b divides (a |^ n) - (b |^ n) )

then ex k being Nat st n = (2 * k) + 1 by ABIAN:9;
hence ( a + b divides (a |^ n) + (b |^ n) or a + b divides (a |^ n) - (b |^ n) ) by Th34; :: thesis: verum

end;

suppose n is even ; :: thesis: ( a + b divides (a |^ n) + (b |^ n) or a + b divides (a |^ n) - (b |^ n) )

then consider m being Nat such that
A2: n = 2 * m ;
A3: a + b divides (a |^ 2) - (b |^ 2) by Lm44;
(a |^ 2) - (b |^ 2) divides (a |^ (2 * m)) - (b |^ (2 * m)) by Th33;
hence ( a + b divides (a |^ n) + (b |^ n) or a + b divides (a |^ n) - (b |^ n) ) by A2, A3, INT_2:9; :: thesis: verum

end;

end;