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	⊢ ( 𝐴 ∈ ℝ* → ( +∞ ≤ 𝐴 ↔ 𝐴 = +∞ ) )