let a, b, n be Nat; :: thesis: ( a,b are_coprime & a + b > 2 & n is odd implies not a + b divides (a |^ n) - (b |^ n) )
assume A1: ( a,b are_coprime & a + b > 2 & n is odd ) ; :: thesis: not a + b divides (a |^ n) - (b |^ n)
then consider k being Nat such that
A2: n = (2 * k) + 1 by ABIAN:9;
a + b divides (a |^ n) + (b |^ n) by A2, NEWTON01:35;
hence not a + b divides (a |^ n) - (b |^ n) by A1, Th31; :: thesis: verum