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

Metamath Proof Explorer

Theorem xnn0xrge0

Description: An extended nonnegative integer is an extended nonnegative real. (Contributed by AV, 10-Dec-2020)

Ref Expression
Assertion xnn0xrge0 ( 𝐴 ∈ ℕ0* → 𝐴 ∈ ( 0 [,] +∞ ) )

Proof

Step Hyp Ref Expression
1 elxnn0 ⊢ ( 𝐴 ∈ ℕ0* ↔ ( 𝐴 ∈ ℕ0 ∨ 𝐴 = +∞ ) )
2 nn0re ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ )
3 2 rexrd ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ* )
4 nn0ge0 ⊢ ( 𝐴 ∈ ℕ0 → 0 ≤ 𝐴 )
5 elxrge0 ⊢ ( 𝐴 ∈ ( 0 [,] +∞ ) ↔ ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) )
6 3 4 5 sylanbrc ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ( 0 [,] +∞ ) )
7 0xr ⊢ 0 ∈ ℝ*
8 pnfxr ⊢ +∞ ∈ ℝ*
9 0lepnf ⊢ 0 ≤ +∞
10 ubicc2 ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 ≤ +∞ ) → +∞ ∈ ( 0 [,] +∞ ) )
11 7 8 9 10 mp3an ⊢ +∞ ∈ ( 0 [,] +∞ )
12 eleq1 ⊢ ( 𝐴 = +∞ → ( 𝐴 ∈ ( 0 [,] +∞ ) ↔ +∞ ∈ ( 0 [,] +∞ ) ) )
13 11 12 mpbiri ⊢ ( 𝐴 = +∞ → 𝐴 ∈ ( 0 [,] +∞ ) )
14 6 13 jaoi ⊢ ( ( 𝐴 ∈ ℕ0 ∨ 𝐴 = +∞ ) → 𝐴 ∈ ( 0 [,] +∞ ) )
15 1 14 sylbi ⊢ ( 𝐴 ∈ ℕ0* → 𝐴 ∈ ( 0 [,] +∞ ) )