This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nn0onn

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

		Ref	Expression
	Assertion	nn0onn	$⊢ (N \in ℕ_{0} \land \neg 2 ∥ N) \to N \in ℕ$

Step	Hyp	Ref	Expression
1		z0even	$⊢ 2 ∥ 0$
2		breq2	$⊢ N = 0 \to (2 ∥ N \leftrightarrow 2 ∥ 0)$
3	1 2	mpbiri	$⊢ N = 0 \to 2 ∥ N$
4	3	necon3bi	$⊢ \neg 2 ∥ N \to N \neq 0$
5	4	anim2i	$⊢ (N \in ℕ_{0} \land \neg 2 ∥ N) \to (N \in ℕ_{0} \land N \neq 0)$
6		elnnne0	$⊢ N \in ℕ \leftrightarrow (N \in ℕ_{0} \land N \neq 0)$
7	5 6	sylibr	$⊢ (N \in ℕ_{0} \land \neg 2 ∥ N) \to N \in ℕ$