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 [,] +∞ ) )