nemnftgtmnft

Description: An extended real that is not minus infinity, is larger than minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020)

		Ref	Expression
	Assertion	nemnftgtmnft	$⊢ (A \in ℝ^{*} \land A \neq −∞) \to −∞ < A$

Step	Hyp	Ref	Expression
1		simpr	$⊢ (A \in ℝ^{*} \land A \neq −∞) \to A \neq −∞$
2	1	neneqd	$⊢ (A \in ℝ^{*} \land A \neq −∞) \to \neg A = −∞$
3		ngtmnft	$⊢ A \in ℝ^{*} \to (A = −∞ \leftrightarrow \neg −∞ < A)$
4	3	adantr	$⊢ (A \in ℝ^{*} \land A \neq −∞) \to (A = −∞ \leftrightarrow \neg −∞ < A)$
5	2 4	mtbid	$⊢ (A \in ℝ^{*} \land A \neq −∞) \to \neg \neg −∞ < A$
6		notnotb	$⊢ −∞ < A \leftrightarrow \neg \neg −∞ < A$
7	5 6	sylibr	$⊢ (A \in ℝ^{*} \land A \neq −∞) \to −∞ < A$

Metamath Proof Explorer