nltmnf

Description: No extended real is less than minus infinity. (Contributed by NM, 15-Oct-2005)

		Ref	Expression
	Assertion	nltmnf	$⊢ A \in ℝ^{*} \to \neg A < −∞$

Step	Hyp	Ref	Expression
1		mnfnre	$⊢ −∞ \notin ℝ$
2	1	neli	$⊢ \neg −∞ \in ℝ$
3	2	intnan	$⊢ \neg (A \in ℝ \land −∞ \in ℝ)$
4	3	intnanr	$⊢ \neg ((A \in ℝ \land −∞ \in ℝ) \land A <_{ℝ} −∞)$
5		pnfnemnf	$⊢ +∞ \neq −∞$
6	5	nesymi	$⊢ \neg −∞ = +∞$
7	6	intnan	$⊢ \neg (A = −∞ \land −∞ = +∞)$
8	4 7	pm3.2ni	$⊢ \neg (((A \in ℝ \land −∞ \in ℝ) \land A <_{ℝ} −∞) \lor (A = −∞ \land −∞ = +∞))$
9	6	intnan	$⊢ \neg (A \in ℝ \land −∞ = +∞)$
10	2	intnan	$⊢ \neg (A = −∞ \land −∞ \in ℝ)$
11	9 10	pm3.2ni	$⊢ \neg ((A \in ℝ \land −∞ = +∞) \lor (A = −∞ \land −∞ \in ℝ))$
12	8 11	pm3.2ni	$⊢ \neg ((((A \in ℝ \land −∞ \in ℝ) \land A <_{ℝ} −∞) \lor (A = −∞ \land −∞ = +∞)) \lor ((A \in ℝ \land −∞ = +∞) \lor (A = −∞ \land −∞ \in ℝ)))$
13		mnfxr	$⊢ −∞ \in ℝ^{*}$
14		ltxr	$⊢ (A \in ℝ^{} \land −∞ \in ℝ^{}) \to (A < −∞ \leftrightarrow ((((A \in ℝ \land −∞ \in ℝ) \land A <_{ℝ} −∞) \lor (A = −∞ \land −∞ = +∞)) \lor ((A \in ℝ \land −∞ = +∞) \lor (A = −∞ \land −∞ \in ℝ))))$
15	13 14	mpan2	$⊢ A \in ℝ^{*} \to (A < −∞ \leftrightarrow ((((A \in ℝ \land −∞ \in ℝ) \land A <_{ℝ} −∞) \lor (A = −∞ \land −∞ = +∞)) \lor ((A \in ℝ \land −∞ = +∞) \lor (A = −∞ \land −∞ \in ℝ))))$
16	12 15	mtbiri	$⊢ A \in ℝ^{*} \to \neg A < −∞$

Metamath Proof Explorer