This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )