Theorem nn0onn

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

	Ref	Expression
Assertion	nn0onn	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑁 ) → 𝑁 ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		z0even	⊢ 2 ∥ 0
2		breq2	⊢ ( 𝑁 = 0 → ( 2 ∥ 𝑁 ↔ 2 ∥ 0 ) )
3	1 2	mpbiri	⊢ ( 𝑁 = 0 → 2 ∥ 𝑁 )
4	3	necon3bi	⊢ ( ¬ 2 ∥ 𝑁 → 𝑁 ≠ 0 )
5	4	anim2i	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑁 ) → ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ) )
6		elnnne0	⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ) )
7	5 6	sylibr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑁 ) → 𝑁 ∈ ℕ )