Metamath Proof Explorer


Theorem nn0onn

Description: An odd nonnegative integer is positive. (Contributed by Steven Nguyen, 25-Mar-2023)

Ref Expression
Assertion nn0onn N0¬2NN

Proof

Step Hyp Ref Expression
1 z0even 20
2 breq2 N=02N20
3 1 2 mpbiri N=02N
4 3 necon3bi ¬2NN0
5 4 anim2i N0¬2NN0N0
6 elnnne0 NN0N0
7 5 6 sylibr N0¬2NN