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

Metamath Proof Explorer

Theorem xrgepnfd

Description: An extended real greater than or equal to +oo is +oo (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses xrgepnfd.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
xrgepnfd.2 ⊢ ( 𝜑 → +∞ ≤ 𝐴 )
Assertion xrgepnfd ( 𝜑 → 𝐴 = +∞ )

Proof

Step Hyp Ref Expression
1 xrgepnfd.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2 xrgepnfd.2 ⊢ ( 𝜑 → +∞ ≤ 𝐴 )
3 pnfxr ⊢ +∞ ∈ ℝ*
4 3 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
5 pnfge ⊢ ( 𝐴 ∈ ℝ* → 𝐴 ≤ +∞ )
6 1 5 syl ⊢ ( 𝜑 → 𝐴 ≤ +∞ )
7 1 4 6 2 xrletrid ⊢ ( 𝜑 → 𝐴 = +∞ )