let n be Nat; ( n > 0 implies (2 to_power n) mod 2 = 0 )
assume
n > 0
; (2 to_power n) mod 2 = 0
then A1:
n >= 0 + 1
by NAT_1:13;
2 to_power n =
2 to_power ((n - 1) + 1)
.=
2 to_power ((n -' 1) + 1)
by A1, XREAL_1:233
.=
(2 to_power (n -' 1)) * (2 to_power 1)
by POWER:27
.=
(2 to_power (n -' 1)) * 2
by POWER:25
;
hence
(2 to_power n) mod 2 = 0
by NAT_D:13; verum