let n be Nat; :: thesis: ( n > 0 implies 2 to_power n is even )
assume n > 0 ; :: thesis: 2 to_power n is even
then (2 to_power n) mod 2 = 0 by NAT_2:17;
hence 2 to_power n is even by NAT_2:21; :: thesis: verum