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

Metamath Proof Explorer

Theorem xrge0nre

Description: An extended real which is not a real is plus infinity. (Contributed by Thierry Arnoux, 16-Oct-2017)

Ref Expression
Assertion xrge0nre ⊢ A ∈ 0 +∞ ∧ ¬ A ∈ ℝ → A = +∞

Proof

Step Hyp Ref Expression
1 eliccxr ⊢ A ∈ 0 +∞ → A ∈ ℝ *
2 xrge0neqmnf ⊢ A ∈ 0 +∞ → A ≠ −∞
3 xrnemnf ⊢ A ∈ ℝ * ∧ A ≠ −∞ ↔ A ∈ ℝ ∨ A = +∞
4 3 biimpi ⊢ A ∈ ℝ * ∧ A ≠ −∞ → A ∈ ℝ ∨ A = +∞
5 1 2 4 syl2anc ⊢ A ∈ 0 +∞ → A ∈ ℝ ∨ A = +∞
6 5 orcanai ⊢ A ∈ 0 +∞ ∧ ¬ A ∈ ℝ → A = +∞