let a, n be Nat; :: thesis: ( n > 1 implies ( (a |^ n) + 1 is odd iff a is even ) )
assume A1: n > 1 ; :: thesis: ( (a |^ n) + 1 is odd iff a is even )
thus ( (a |^ n) + 1 is odd implies a is even ) ; :: thesis: ( a is even implies (a |^ n) + 1 is odd )
assume a is even ; :: thesis: (a |^ n) + 1 is odd
hence (a |^ n) + 1 is odd by A1; :: thesis: verum