let n be Nat; :: thesis: ( n > 0 implies ( n mod 2 = 0 iff (n -' 1) mod 2 = 1 ) )
assume A1: n > 0 ; :: thesis: ( n mod 2 = 0 iff (n -' 1) mod 2 = 1 )
thus ( n mod 2 = 0 implies (n -' 1) mod 2 = 1 ) :: thesis: ( (n -' 1) mod 2 = 1 implies n mod 2 = 0 )
proof
consider t being Nat such that
A2: n = (2 * t) + (n mod 2) and
n mod 2 < 2 by NAT_D:def 2;
assume A3: n mod 2 = 0 ; :: thesis: (n -' 1) mod 2 = 1
then t > 0 by A1, A2;
then A4: t >= 0 + 1 by NAT_1:13;
n >= 0 + 1 by A1, NAT_1:13;
then n -' 1 = (2 * ((t - 1) + 1)) - 1 by A3, A2, XREAL_1:233
.= (2 * (t - 1)) + ((1 + 1) - 1)
.= (2 * (t -' 1)) + 1 by A4, XREAL_1:233 ;
hence (n -' 1) mod 2 = 1 by NAT_D:def 2; :: thesis: verum
end;
assume (n -' 1) mod 2 = 1 ; :: thesis: n mod 2 = 0
then consider t being Nat such that
A5: n -' 1 = (2 * t) + 1 and
1 < 2 by NAT_D:def 2;
n >= 0 + 1 by A1, NAT_1:13;
then n = ((2 * t) + 1) + 1 by A5, XREAL_1:235
.= (2 * (t + 1)) + 0 ;
hence n mod 2 = 0 by NAT_D:def 2; :: thesis: verum