Theorem xnn0gt0

Description: Nonzero extended nonnegative integers are strictly greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023)

	Ref	Expression
Assertion	xnn0gt0	⊢ ( ( 𝑁 ∈ ℕ0* ∧ 𝑁 ≠ 0 ) → 0 < 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		elxnn0	⊢ ( 𝑁 ∈ ℕ0* ↔ ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) )
2		elnnne0	⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ) )
3		nngt0	⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 )
4	2 3	sylbir	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ) → 0 < 𝑁 )
5	4	ancoms	⊢ ( ( 𝑁 ≠ 0 ∧ 𝑁 ∈ ℕ0 ) → 0 < 𝑁 )
6	5	adantll	⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) ∧ 𝑁 ≠ 0 ) ∧ 𝑁 ∈ ℕ0 ) → 0 < 𝑁 )
7		0ltpnf	⊢ 0 < +∞
8		breq2	⊢ ( 𝑁 = +∞ → ( 0 < 𝑁 ↔ 0 < +∞ ) )
9	7 8	mpbiri	⊢ ( 𝑁 = +∞ → 0 < 𝑁 )
10	9	adantl	⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) ∧ 𝑁 ≠ 0 ) ∧ 𝑁 = +∞ ) → 0 < 𝑁 )
11		simpl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) ∧ 𝑁 ≠ 0 ) → ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) )
12	6 10 11	mpjaodan	⊢ ( ( ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) ∧ 𝑁 ≠ 0 ) → 0 < 𝑁 )
13	1 12	sylanb	⊢ ( ( 𝑁 ∈ ℕ0* ∧ 𝑁 ≠ 0 ) → 0 < 𝑁 )