Metamath Proof Explorer


Theorem xgepnf

Description: An extended real which is greater than plus infinity is plus infinity. (Contributed by Thierry Arnoux, 18-Dec-2016)

Ref Expression
Assertion xgepnf ( 𝐴 ∈ ℝ* → ( +∞ ≤ 𝐴𝐴 = +∞ ) )

Proof

Step Hyp Ref Expression
1 pnfxr +∞ ∈ ℝ*
2 xrlenlt ( ( +∞ ∈ ℝ*𝐴 ∈ ℝ* ) → ( +∞ ≤ 𝐴 ↔ ¬ 𝐴 < +∞ ) )
3 1 2 mpan ( 𝐴 ∈ ℝ* → ( +∞ ≤ 𝐴 ↔ ¬ 𝐴 < +∞ ) )
4 nltpnft ( 𝐴 ∈ ℝ* → ( 𝐴 = +∞ ↔ ¬ 𝐴 < +∞ ) )
5 3 4 bitr4d ( 𝐴 ∈ ℝ* → ( +∞ ≤ 𝐴𝐴 = +∞ ) )