Theorem nn0mnfxrd

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

	Ref	Expression
Hypothesis	nn0mnfxrd.1	⊢ ( 𝜑 → 𝐴 ∈ ( ℕ0 ∪ { -∞ } ) )
Assertion	nn0mnfxrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )

Proof

Step	Hyp	Ref	Expression
1		nn0mnfxrd.1	⊢ ( 𝜑 → 𝐴 ∈ ( ℕ0 ∪ { -∞ } ) )
2		nn0re	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ )
3	2	rexrd	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ* )
4	3	adantl	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ0 ) → 𝐴 ∈ ℝ* )
5		mnfxr	⊢ -∞ ∈ ℝ*
6		eleq1	⊢ ( 𝐴 = -∞ → ( 𝐴 ∈ ℝ* ↔ -∞ ∈ ℝ* ) )
7	5 6	mpbiri	⊢ ( 𝐴 = -∞ → 𝐴 ∈ ℝ* )
8	7	adantl	⊢ ( ( 𝜑 ∧ 𝐴 = -∞ ) → 𝐴 ∈ ℝ* )
9		elunsn	⊢ ( 𝐴 ∈ ( ℕ0 ∪ { -∞ } ) → ( 𝐴 ∈ ( ℕ0 ∪ { -∞ } ) ↔ ( 𝐴 ∈ ℕ0 ∨ 𝐴 = -∞ ) ) )
10	9	ibi	⊢ ( 𝐴 ∈ ( ℕ0 ∪ { -∞ } ) → ( 𝐴 ∈ ℕ0 ∨ 𝐴 = -∞ ) )
11	1 10	syl	⊢ ( 𝜑 → ( 𝐴 ∈ ℕ0 ∨ 𝐴 = -∞ ) )
12	4 8 11	mpjaodan	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )