let a, b, c, n be Nat; ( a,b are_coprime & c is even & (a |^ n) + (b |^ n) = c |^ n implies ( a + b is even & a - b is even ) )
assume A1:
( a,b are_coprime & c is even & (a |^ n) + (b |^ n) = c |^ n )
; ( a + b is even & a - b is even )
( n = 0 implies (1 * (a |^ n)) + (1 * (b |^ n)) > 1 * (c |^ n) )
;
then
( ( a is even & b is even ) or ( a is odd & b is odd ) )
by A1;
hence
( a + b is even & a - b is even )
; verum