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

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 ⊢ A ∈ 0 +∞ → A ≠ −∞

Proof

Step Hyp Ref Expression
1 eliccxr ⊢ A ∈ 0 +∞ → A ∈ ℝ *
2 0xr ⊢ 0 ∈ ℝ *
3 pnfxr ⊢ +∞ ∈ ℝ *
4 iccgelb ⊢ 0 ∈ ℝ * ∧ +∞ ∈ ℝ * ∧ A ∈ 0 +∞ → 0 ≤ A
5 2 3 4 mp3an12 ⊢ A ∈ 0 +∞ → 0 ≤ A
6 ge0nemnf ⊢ A ∈ ℝ * ∧ 0 ≤ A → A ≠ −∞
7 1 5 6 syl2anc ⊢ A ∈ 0 +∞ → A ≠ −∞