mnfltpnf

Description: Minus infinity is less than plus infinity. (Contributed by NM, 14-Oct-2005)

		Ref	Expression
	Assertion	mnfltpnf	$⊢ −∞ < +∞$

Step	Hyp	Ref	Expression
1		eqid	$⊢ −∞ = −∞$
2		eqid	$⊢ +∞ = +∞$
3		olc	$⊢ (−∞ = −∞ \land +∞ = +∞) \to (((−∞ \in ℝ \land +∞ \in ℝ) \land −∞ <_{ℝ} +∞) \lor (−∞ = −∞ \land +∞ = +∞))$
4	1 2 3	mp2an	$⊢ (((−∞ \in ℝ \land +∞ \in ℝ) \land −∞ <_{ℝ} +∞) \lor (−∞ = −∞ \land +∞ = +∞))$
5	4	orci	$⊢ ((((−∞ \in ℝ \land +∞ \in ℝ) \land −∞ <_{ℝ} +∞) \lor (−∞ = −∞ \land +∞ = +∞)) \lor ((−∞ \in ℝ \land +∞ = +∞) \lor (−∞ = −∞ \land +∞ \in ℝ)))$
6		mnfxr	$⊢ −∞ \in ℝ^{*}$
7		pnfxr	$⊢ +∞ \in ℝ^{*}$
8		ltxr	$⊢ (−∞ \in ℝ^{} \land +∞ \in ℝ^{}) \to (−∞ < +∞ \leftrightarrow ((((−∞ \in ℝ \land +∞ \in ℝ) \land −∞ <_{ℝ} +∞) \lor (−∞ = −∞ \land +∞ = +∞)) \lor ((−∞ \in ℝ \land +∞ = +∞) \lor (−∞ = −∞ \land +∞ \in ℝ))))$
9	6 7 8	mp2an	$⊢ −∞ < +∞ \leftrightarrow ((((−∞ \in ℝ \land +∞ \in ℝ) \land −∞ <_{ℝ} +∞) \lor (−∞ = −∞ \land +∞ = +∞)) \lor ((−∞ \in ℝ \land +∞ = +∞) \lor (−∞ = −∞ \land +∞ \in ℝ)))$
10	5 9	mpbir	$⊢ −∞ < +∞$

Metamath Proof Explorer