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	⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ ¬ 𝐴 ∈ ℝ ) → 𝐴 = +∞ )

Proof

Step	Hyp	Ref	Expression
1		eliccxr	⊢ ( 𝐴 ∈ ( 0 [,] +∞ ) → 𝐴 ∈ ℝ* )
2		xrge0neqmnf	⊢ ( 𝐴 ∈ ( 0 [,] +∞ ) → 𝐴 ≠ -∞ )
3		xrnemnf	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) )
4	3	biimpi	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) → ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) )
5	1 2 4	syl2anc	⊢ ( 𝐴 ∈ ( 0 [,] +∞ ) → ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) )
6	5	orcanai	⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ ¬ 𝐴 ∈ ℝ ) → 𝐴 = +∞ )