let a, b, n be Nat; :: thesis: ( a,b are_coprime & a + b > 2 & n is even implies not a + b divides (a |^ n) + (b |^ n) )
assume A1: ( a,b are_coprime & a + b > 2 & n is even ) ; :: thesis: not a + b divides (a |^ n) + (b |^ n)
then a + b divides (a |^ n) - (b |^ n) by NEWTON01:36;
hence not a + b divides (a |^ n) + (b |^ n) by A1, Th31; :: thesis: verum