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

Metamath Proof Explorer

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