nltpnft

Description: An extended real is not less than plus infinity iff they are equal. (Contributed by NM, 30-Jan-2006)

		Ref	Expression
	Assertion	nltpnft	$⊢ A \in ℝ^{*} \to (A = +∞ \leftrightarrow \neg A < +∞)$

Step	Hyp	Ref	Expression
1		pnfxr	$⊢ +∞ \in ℝ^{*}$
2		xrltnr	$⊢ +∞ \in ℝ^{*} \to \neg +∞ < +∞$
3	1 2	ax-mp	$⊢ \neg +∞ < +∞$
4		breq1	$⊢ A = +∞ \to (A < +∞ \leftrightarrow +∞ < +∞)$
5	3 4	mtbiri	$⊢ A = +∞ \to \neg A < +∞$
6		pnfge	$⊢ A \in ℝ^{*} \to A \leq +∞$
7		xrleloe	$⊢ (A \in ℝ^{} \land +∞ \in ℝ^{}) \to (A \leq +∞ \leftrightarrow (A < +∞ \lor A = +∞))$
8	1 7	mpan2	$⊢ A \in ℝ^{*} \to (A \leq +∞ \leftrightarrow (A < +∞ \lor A = +∞))$
9	6 8	mpbid	$⊢ A \in ℝ^{*} \to (A < +∞ \lor A = +∞)$
10	9	ord	$⊢ A \in ℝ^{*} \to (\neg A < +∞ \to A = +∞)$
11	5 10	impbid2	$⊢ A \in ℝ^{*} \to (A = +∞ \leftrightarrow \neg A < +∞)$

Metamath Proof Explorer