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

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

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