Theorem mnfltxr

Description: Minus infinity is less than an extended real that is either real or plus infinity. (Contributed by NM, 2-Feb-2006)

	Ref	Expression
Assertion	mnfltxr	$$⊢\left(A\in ℝ\vee A=\mathrm{+\infty }\right)\to \mathrm{-\infty }<A$$

Proof

Step	Hyp	Ref	Expression
1		mnflt	$$⊢A\in ℝ\to \mathrm{-\infty }<A$$
2		mnfltpnf	$$⊢\mathrm{-\infty }<\mathrm{+\infty }$$
3		breq2	$$⊢A=\mathrm{+\infty }\to \left(\mathrm{-\infty }<A\leftrightarrow \mathrm{-\infty }<\mathrm{+\infty }\right)$$
4	2 3	mpbiri	$$⊢A=\mathrm{+\infty }\to \mathrm{-\infty }<A$$
5	1 4	jaoi	$$⊢\left(A\in ℝ\vee A=\mathrm{+\infty }\right)\to \mathrm{-\infty }<A$$