Theorem xnn0xrnemnf

Description: The extended nonnegative integers are extended reals without negative infinity. (Contributed by AV, 10-Dec-2020)

	Ref	Expression
Assertion	xnn0xrnemnf	$$⊢A\in {\mathbb{N}}_0^{*}\to \left(A\in {ℝ}^{*}\wedge A\ne \mathrm{-\infty }\right)$$

Proof

Step	Hyp	Ref	Expression
1		xnn0xr	$$⊢A\in {\mathbb{N}}_0^{*}\to A\in {ℝ}^{*}$$
2		xnn0nemnf	$$⊢A\in {\mathbb{N}}_0^{*}\to A\ne \mathrm{-\infty }$$
3	1 2	jca	$$⊢A\in {\mathbb{N}}_0^{*}\to \left(A\in {ℝ}^{*}\wedge A\ne \mathrm{-\infty }\right)$$