nn0mnfxrd

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

		Ref	Expression
	Hypothesis	nn0mnfxrd.1	$⊢ φ \to A \in (ℕ_{0} \cup \{−∞\})$
	Assertion	nn0mnfxrd	$⊢ φ \to A \in ℝ^{*}$

Step	Hyp	Ref	Expression
1		nn0mnfxrd.1	$⊢ φ \to A \in (ℕ_{0} \cup \{−∞\})$
2		nn0re	$⊢ A \in ℕ_{0} \to A \in ℝ$
3	2	rexrd	$⊢ A \in ℕ_{0} \to A \in ℝ^{*}$
4	3	adantl	$⊢ (φ \land A \in ℕ_{0}) \to A \in ℝ^{*}$
5		mnfxr	$⊢ −∞ \in ℝ^{*}$
6		eleq1	$⊢ A = −∞ \to (A \in ℝ^{} \leftrightarrow −∞ \in ℝ^{})$
7	5 6	mpbiri	$⊢ A = −∞ \to A \in ℝ^{*}$
8	7	adantl	$⊢ (φ \land A = −∞) \to A \in ℝ^{*}$
9		elunsn	$⊢ A \in (ℕ_{0} \cup \{−∞\}) \to (A \in (ℕ_{0} \cup \{−∞\}) \leftrightarrow (A \in ℕ_{0} \lor A = −∞))$
10	9	ibi	$⊢ A \in (ℕ_{0} \cup \{−∞\}) \to (A \in ℕ_{0} \lor A = −∞)$
11	1 10	syl	$⊢ φ \to (A \in ℕ_{0} \lor A = −∞)$
12	4 8 11	mpjaodan	$⊢ φ \to A \in ℝ^{*}$

Metamath Proof Explorer