Theorem nn0onn

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

	Ref	Expression
Assertion	nn0onn	$$⊢\left(N\in {\mathbb{N}}_0\wedge \neg 2\parallel N\right)\to N\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		z0even	$$⊢2\parallel 0$$
2		breq2	$$⊢N=0\to \left(2\parallel N\leftrightarrow 2\parallel 0\right)$$
3	1 2	mpbiri	$$⊢N=0\to 2\parallel N$$
4	3	necon3bi	$$⊢\neg 2\parallel N\to N\ne 0$$
5	4	anim2i	$$⊢\left(N\in {\mathbb{N}}_0\wedge \neg 2\parallel N\right)\to \left(N\in {\mathbb{N}}_0\wedge N\ne 0\right)$$
6		elnnne0	$$⊢N\in \mathbb{N}\leftrightarrow \left(N\in {\mathbb{N}}_0\wedge N\ne 0\right)$$
7	5 6	sylibr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \neg 2\parallel N\right)\to N\in \mathbb{N}$$