Theorem xnn0xr

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

	Ref	Expression
Assertion	xnn0xr	$$⊢A\in {\mathbb{N}}_0^{*}\to A\in {ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		elxnn0	$$⊢A\in {\mathbb{N}}_0^{*}\leftrightarrow \left(A\in {\mathbb{N}}_0\vee A=\mathrm{+\infty }\right)$$
2		nn0re	$$⊢A\in {\mathbb{N}}_0\to A\in ℝ$$
3	2	rexrd	$$⊢A\in {\mathbb{N}}_0\to A\in {ℝ}^{*}$$
4		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
5		eleq1	$$⊢A=\mathrm{+\infty }\to \left(A\in {ℝ}^{*}\leftrightarrow \mathrm{+\infty }\in {ℝ}^{*}\right)$$
6	4 5	mpbiri	$$⊢A=\mathrm{+\infty }\to A\in {ℝ}^{*}$$
7	3 6	jaoi	$$⊢\left(A\in {\mathbb{N}}_0\vee A=\mathrm{+\infty }\right)\to A\in {ℝ}^{*}$$
8	1 7	sylbi	$$⊢A\in {\mathbb{N}}_0^{*}\to A\in {ℝ}^{*}$$