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 ⊢ A ∈ ℕ 0 * → A ∈ 0 +∞

Proof

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