Theorem nn0mnfxrd

Description: Nonnegative integers or minus infinity are extended real numbers. (Contributed by Thierry Arnoux, 15-Feb-2026)

	Ref	Expression
Hypothesis	nn0mnfxrd.1	$$⊢\phi \to A\in \left({\mathbb{N}}_0\cup \left\{\mathrm{-\infty }\right\}\right)$$
Assertion	nn0mnfxrd	$$⊢\phi \to A\in {ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		nn0mnfxrd.1	$$⊢\phi \to A\in \left({\mathbb{N}}_0\cup \left\{\mathrm{-\infty }\right\}\right)$$
2		nn0re	$$⊢A\in {\mathbb{N}}_0\to A\in ℝ$$
3	2	rexrd	$$⊢A\in {\mathbb{N}}_0\to A\in {ℝ}^{*}$$
4	3	adantl	$$⊢\left(\phi \wedge A\in {\mathbb{N}}_0\right)\to A\in {ℝ}^{*}$$
5		mnfxr	$$⊢\mathrm{-\infty }\in {ℝ}^{*}$$
6		eleq1	$$⊢A=\mathrm{-\infty }\to \left(A\in {ℝ}^{*}\leftrightarrow \mathrm{-\infty }\in {ℝ}^{*}\right)$$
7	5 6	mpbiri	$$⊢A=\mathrm{-\infty }\to A\in {ℝ}^{*}$$
8	7	adantl	$$⊢\left(\phi \wedge A=\mathrm{-\infty }\right)\to A\in {ℝ}^{*}$$
9		elunsn	$$⊢A\in \left({\mathbb{N}}_0\cup \left\{\mathrm{-\infty }\right\}\right)\to \left(A\in \left({\mathbb{N}}_0\cup \left\{\mathrm{-\infty }\right\}\right)\leftrightarrow \left(A\in {\mathbb{N}}_0\vee A=\mathrm{-\infty }\right)\right)$$
10	9	ibi	$$⊢A\in \left({\mathbb{N}}_0\cup \left\{\mathrm{-\infty }\right\}\right)\to \left(A\in {\mathbb{N}}_0\vee A=\mathrm{-\infty }\right)$$
11	1 10	syl	$$⊢\phi \to \left(A\in {\mathbb{N}}_0\vee A=\mathrm{-\infty }\right)$$
12	4 8 11	mpjaodan	$$⊢\phi \to A\in {ℝ}^{*}$$