Metamath Proof Explorer

Theorem xrge0neqmnf

Description: A nonnegative extended real is not equal to minus infinity. (Contributed by Thierry Arnoux, 9-Jun-2017) (Proof shortened by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion xrge0neqmnf ( 𝐴 ∈ ( 0 [,] +∞ ) → 𝐴 ≠ -∞ )

Proof

Step Hyp Ref Expression
1 eliccxr ⊢ ( 𝐴 ∈ ( 0 [,] +∞ ) → 𝐴 ∈ ℝ* )
2 0xr ⊢ 0 ∈ ℝ*
3 pnfxr ⊢ +∞ ∈ ℝ*
4 iccgelb ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐴 ∈ ( 0 [,] +∞ ) ) → 0 ≤ 𝐴 )
5 2 3 4 mp3an12 ⊢ ( 𝐴 ∈ ( 0 [,] +∞ ) → 0 ≤ 𝐴 )
6 ge0nemnf ⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) → 𝐴 ≠ -∞ )
7 1 5 6 syl2anc ⊢ ( 𝐴 ∈ ( 0 [,] +∞ ) → 𝐴 ≠ -∞ )