theorem :: NUMBER18:43

for a, n being Nat st n > 1 holds
( (a |^ n) + 1 is odd iff a is even )