Metamath Proof Explorer

Theorem nn0onn

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

Ref Expression
Assertion nn0onn 
|- ( ( N e. NN0 /\ -. 2 || N ) -> N e. NN )

Proof

Step Hyp Ref Expression
1 z0even 
 |-  2 || 0
2 breq2 
 |-  ( N = 0 -> ( 2 || N <-> 2 || 0 ) )
3 1 2 mpbiri 
 |-  ( N = 0 -> 2 || N )
4 3 necon3bi 
 |-  ( -. 2 || N -> N =/= 0 )
5 4 anim2i 
 |-  ( ( N e. NN0 /\ -. 2 || N ) -> ( N e. NN0 /\ N =/= 0 ) )
6 elnnne0 
 |-  ( N e. NN <-> ( N e. NN0 /\ N =/= 0 ) )
7 5 6 sylibr 
 |-  ( ( N e. NN0 /\ -. 2 || N ) -> N e. NN )