Metamath Proof Explorer


Theorem oddm1even

Description: An integer is odd iff its predecessor is even. (Contributed by Mario Carneiro, 5-Sep-2016)

Ref Expression
Assertion oddm1even N¬2N2N1

Proof

Step Hyp Ref Expression
1 simpl NnN
2 1 zcnd NnN
3 1cnd Nn1
4 2cnd Nn2
5 simpr Nnn
6 5 zcnd Nnn
7 4 6 mulcld Nn2n
8 2 3 7 subadd2d NnN1=2n2n+1=N
9 eqcom N1=2n2n=N1
10 4 6 mulcomd Nn2n=n2
11 10 eqeq1d Nn2n=N1n2=N1
12 9 11 syl5bb NnN1=2nn2=N1
13 8 12 bitr3d Nn2n+1=Nn2=N1
14 13 rexbidva Nn2n+1=Nnn2=N1
15 odd2np1 N¬2Nn2n+1=N
16 2z 2
17 peano2zm NN1
18 divides 2N12N1nn2=N1
19 16 17 18 sylancr N2N1nn2=N1
20 14 15 19 3bitr4d N¬2N2N1