Metamath Proof Explorer

Theorem mnflt

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

Ref Expression
Assertion mnflt ${⊢}{A}\in ℝ\to \mathrm{-\infty }<{A}$

Proof

Step Hyp Ref Expression
1 eqid ${⊢}\mathrm{-\infty }=\mathrm{-\infty }$
2 olc ${⊢}\left(\mathrm{-\infty }=\mathrm{-\infty }\wedge {A}\in ℝ\right)\to \left(\left(\mathrm{-\infty }\in ℝ\wedge {A}=\mathrm{+\infty }\right)\vee \left(\mathrm{-\infty }=\mathrm{-\infty }\wedge {A}\in ℝ\right)\right)$
3 1 2 mpan ${⊢}{A}\in ℝ\to \left(\left(\mathrm{-\infty }\in ℝ\wedge {A}=\mathrm{+\infty }\right)\vee \left(\mathrm{-\infty }=\mathrm{-\infty }\wedge {A}\in ℝ\right)\right)$
4 3 olcd ${⊢}{A}\in ℝ\to \left(\left(\left(\left(\mathrm{-\infty }\in ℝ\wedge {A}\in ℝ\right)\wedge \mathrm{-\infty }{<}_{ℝ}{A}\right)\vee \left(\mathrm{-\infty }=\mathrm{-\infty }\wedge {A}=\mathrm{+\infty }\right)\right)\vee \left(\left(\mathrm{-\infty }\in ℝ\wedge {A}=\mathrm{+\infty }\right)\vee \left(\mathrm{-\infty }=\mathrm{-\infty }\wedge {A}\in ℝ\right)\right)\right)$
5 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
6 rexr ${⊢}{A}\in ℝ\to {A}\in {ℝ}^{*}$
7 ltxr ${⊢}\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge {A}\in {ℝ}^{*}\right)\to \left(\mathrm{-\infty }<{A}↔\left(\left(\left(\left(\mathrm{-\infty }\in ℝ\wedge {A}\in ℝ\right)\wedge \mathrm{-\infty }{<}_{ℝ}{A}\right)\vee \left(\mathrm{-\infty }=\mathrm{-\infty }\wedge {A}=\mathrm{+\infty }\right)\right)\vee \left(\left(\mathrm{-\infty }\in ℝ\wedge {A}=\mathrm{+\infty }\right)\vee \left(\mathrm{-\infty }=\mathrm{-\infty }\wedge {A}\in ℝ\right)\right)\right)\right)$
8 5 6 7 sylancr ${⊢}{A}\in ℝ\to \left(\mathrm{-\infty }<{A}↔\left(\left(\left(\left(\mathrm{-\infty }\in ℝ\wedge {A}\in ℝ\right)\wedge \mathrm{-\infty }{<}_{ℝ}{A}\right)\vee \left(\mathrm{-\infty }=\mathrm{-\infty }\wedge {A}=\mathrm{+\infty }\right)\right)\vee \left(\left(\mathrm{-\infty }\in ℝ\wedge {A}=\mathrm{+\infty }\right)\vee \left(\mathrm{-\infty }=\mathrm{-\infty }\wedge {A}\in ℝ\right)\right)\right)\right)$
9 4 8 mpbird ${⊢}{A}\in ℝ\to \mathrm{-\infty }<{A}$