let n, a, b be Nat; :: thesis: ( a,b are_coprime & a + b > 2 implies ( a + b divides (a |^ n) + (b |^ n) iff not a + b divides (a |^ n) - (b |^ n) ) )
assume A1: ( a,b are_coprime & a + b > 2 ) ; :: thesis: ( a + b divides (a |^ n) + (b |^ n) iff not a + b divides (a |^ n) - (b |^ n) )
A2: b > 0
proof
assume not b > 0 ; :: thesis: contradiction
then b = 0 ;
hence contradiction by A1; :: thesis: verum
end;
A3: not a + b divides 2 * (a |^ n) by A1, A2, Lm1;
( a + b divides (a |^ n) - (b |^ n) implies not a + b divides (a |^ n) + (b |^ n) )
proof
assume ( a + b divides (a |^ n) - (b |^ n) & a + b divides (a |^ n) + (b |^ n) ) ; :: thesis: contradiction
then a + b divides ((a |^ n) + (b |^ n)) + ((a |^ n) - (b |^ n)) by WSIERP_1:4;
hence contradiction by A3; :: thesis: verum
end;
hence ( a + b divides (a |^ n) + (b |^ n) iff not a + b divides (a |^ n) - (b |^ n) ) by NEWTON01:38; :: thesis: verum