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