let a, b, c, n be Nat; :: thesis: ( 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 ) ; :: thesis: ( 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 ) ; :: thesis: verum

assume A1: ( a,b are_coprime & c is even & (a |^ n) + (b |^ n) = c |^ n ) ; :: thesis: ( 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 ) ; :: thesis: verum