Metamath Proof Explorer


Theorem oddp1even

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

Ref Expression
Assertion oddp1even N¬2N2N+1

Proof

Step Hyp Ref Expression
1 oddm1even N¬2N2N1
2 2z 2
3 peano2zm NN1
4 dvdsadd 2N12N122+N-1
5 2 3 4 sylancr N2N122+N-1
6 2cnd N2
7 zcn NN
8 1cnd N1
9 6 7 8 addsub12d N2+N-1=N+2-1
10 2m1e1 21=1
11 10 oveq2i N+2-1=N+1
12 9 11 eqtrdi N2+N-1=N+1
13 12 breq2d N22+N-12N+1
14 1 5 13 3bitrd N¬2N2N+1