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	$⊢ A \in ℝ^{*} \to A \leq +∞$

Step	Hyp	Ref	Expression
1		pnfnlt	$⊢ A \in ℝ^{*} \to \neg +∞ < A$
2		pnfxr	$⊢ +∞ \in ℝ^{*}$
3		xrlenlt	$⊢ (A \in ℝ^{} \land +∞ \in ℝ^{}) \to (A \leq +∞ \leftrightarrow \neg +∞ < A)$
4	2 3	mpan2	$⊢ A \in ℝ^{*} \to (A \leq +∞ \leftrightarrow \neg +∞ < A)$
5	1 4	mpbird	$⊢ A \in ℝ^{*} \to A \leq +∞$