Theorem pnfge

Description: Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006)

	Ref	Expression
Assertion	pnfge	⊢ ( 𝐴 ∈ ℝ* → 𝐴 ≤ +∞ )

Proof

Step	Hyp	Ref	Expression
1		pnfnlt	⊢ ( 𝐴 ∈ ℝ* → ¬ +∞ < 𝐴 )
2		pnfxr	⊢ +∞ ∈ ℝ*
3		xrlenlt	⊢ ( ( 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴 ) )
4	2 3	mpan2	⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴 ) )
5	1 4	mpbird	⊢ ( 𝐴 ∈ ℝ* → 𝐴 ≤ +∞ )