Theorem xnn0xr

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

	Ref	Expression
Assertion	xnn0xr	⊢ ( 𝐴 ∈ ℕ0* → 𝐴 ∈ ℝ* )

Proof

Step	Hyp	Ref	Expression
1		elxnn0	⊢ ( 𝐴 ∈ ℕ0* ↔ ( 𝐴 ∈ ℕ0 ∨ 𝐴 = +∞ ) )
2		nn0re	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ )
3	2	rexrd	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ* )
4		pnfxr	⊢ +∞ ∈ ℝ*
5		eleq1	⊢ ( 𝐴 = +∞ → ( 𝐴 ∈ ℝ* ↔ +∞ ∈ ℝ* ) )
6	4 5	mpbiri	⊢ ( 𝐴 = +∞ → 𝐴 ∈ ℝ* )
7	3 6	jaoi	⊢ ( ( 𝐴 ∈ ℕ0 ∨ 𝐴 = +∞ ) → 𝐴 ∈ ℝ* )
8	1 7	sylbi	⊢ ( 𝐴 ∈ ℕ0* → 𝐴 ∈ ℝ* )