Metamath Proof Explorer


Theorem oddp1d2

Description: An integer is odd iff its successor divided by 2 is an integer. This is a representation of odd numbers without using the divides relation, see zeo and zeo2 . (Contributed by AV, 22-Jun-2021)

Ref Expression
Assertion oddp1d2 N¬2NN+12

Proof

Step Hyp Ref Expression
1 oddp1even N¬2N2N+1
2 2z 2
3 2ne0 20
4 peano2z NN+1
5 dvdsval2 220N+12N+1N+12
6 2 3 4 5 mp3an12i N2N+1N+12
7 1 6 bitrd N¬2NN+12