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

Metamath Proof Explorer

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 < 𝑁 )