ngtmnft

Description: An extended real is not greater than minus infinity iff they are equal. (Contributed by NM, 2-Feb-2006)

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

Step	Hyp	Ref	Expression
1		mnfxr	$⊢ −∞ \in ℝ^{*}$
2		xrltnr	$⊢ −∞ \in ℝ^{*} \to \neg −∞ < −∞$
3	1 2	ax-mp	$⊢ \neg −∞ < −∞$
4		breq2	$⊢ A = −∞ \to (−∞ < A \leftrightarrow −∞ < −∞)$
5	3 4	mtbiri	$⊢ A = −∞ \to \neg −∞ < A$
6		mnfle	$⊢ A \in ℝ^{*} \to −∞ \leq A$
7		xrleloe	$⊢ (−∞ \in ℝ^{} \land A \in ℝ^{}) \to (−∞ \leq A \leftrightarrow (−∞ < A \lor −∞ = A))$
8	1 7	mpan	$⊢ A \in ℝ^{*} \to (−∞ \leq A \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		eqcom	$⊢ −∞ = A \leftrightarrow A = −∞$
12	10 11	imbitrdi	$⊢ A \in ℝ^{*} \to (\neg −∞ < A \to A = −∞)$
13	5 12	impbid2	$⊢ A \in ℝ^{*} \to (A = −∞ \leftrightarrow \neg −∞ < A)$

Metamath Proof Explorer