# Metamath Proof Explorer

## Theorem nltmnf

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

Ref Expression
Assertion nltmnf ${⊢}{A}\in {ℝ}^{*}\to ¬{A}<\mathrm{-\infty }$

### Proof

Step Hyp Ref Expression
1 mnfnre ${⊢}\mathrm{-\infty }\notin ℝ$
2 1 neli ${⊢}¬\mathrm{-\infty }\in ℝ$
3 2 intnan ${⊢}¬\left({A}\in ℝ\wedge \mathrm{-\infty }\in ℝ\right)$
4 3 intnanr ${⊢}¬\left(\left({A}\in ℝ\wedge \mathrm{-\infty }\in ℝ\right)\wedge {A}{<}_{ℝ}\mathrm{-\infty }\right)$
5 pnfnemnf ${⊢}\mathrm{+\infty }\ne \mathrm{-\infty }$
6 5 nesymi ${⊢}¬\mathrm{-\infty }=\mathrm{+\infty }$
7 6 intnan ${⊢}¬\left({A}=\mathrm{-\infty }\wedge \mathrm{-\infty }=\mathrm{+\infty }\right)$
8 4 7 pm3.2ni ${⊢}¬\left(\left(\left({A}\in ℝ\wedge \mathrm{-\infty }\in ℝ\right)\wedge {A}{<}_{ℝ}\mathrm{-\infty }\right)\vee \left({A}=\mathrm{-\infty }\wedge \mathrm{-\infty }=\mathrm{+\infty }\right)\right)$
9 6 intnan ${⊢}¬\left({A}\in ℝ\wedge \mathrm{-\infty }=\mathrm{+\infty }\right)$
10 2 intnan ${⊢}¬\left({A}=\mathrm{-\infty }\wedge \mathrm{-\infty }\in ℝ\right)$
11 9 10 pm3.2ni ${⊢}¬\left(\left({A}\in ℝ\wedge \mathrm{-\infty }=\mathrm{+\infty }\right)\vee \left({A}=\mathrm{-\infty }\wedge \mathrm{-\infty }\in ℝ\right)\right)$
12 8 11 pm3.2ni ${⊢}¬\left(\left(\left(\left({A}\in ℝ\wedge \mathrm{-\infty }\in ℝ\right)\wedge {A}{<}_{ℝ}\mathrm{-\infty }\right)\vee \left({A}=\mathrm{-\infty }\wedge \mathrm{-\infty }=\mathrm{+\infty }\right)\right)\vee \left(\left({A}\in ℝ\wedge \mathrm{-\infty }=\mathrm{+\infty }\right)\vee \left({A}=\mathrm{-\infty }\wedge \mathrm{-\infty }\in ℝ\right)\right)\right)$
13 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
14 ltxr ${⊢}\left({A}\in {ℝ}^{*}\wedge \mathrm{-\infty }\in {ℝ}^{*}\right)\to \left({A}<\mathrm{-\infty }↔\left(\left(\left(\left({A}\in ℝ\wedge \mathrm{-\infty }\in ℝ\right)\wedge {A}{<}_{ℝ}\mathrm{-\infty }\right)\vee \left({A}=\mathrm{-\infty }\wedge \mathrm{-\infty }=\mathrm{+\infty }\right)\right)\vee \left(\left({A}\in ℝ\wedge \mathrm{-\infty }=\mathrm{+\infty }\right)\vee \left({A}=\mathrm{-\infty }\wedge \mathrm{-\infty }\in ℝ\right)\right)\right)\right)$
15 13 14 mpan2 ${⊢}{A}\in {ℝ}^{*}\to \left({A}<\mathrm{-\infty }↔\left(\left(\left(\left({A}\in ℝ\wedge \mathrm{-\infty }\in ℝ\right)\wedge {A}{<}_{ℝ}\mathrm{-\infty }\right)\vee \left({A}=\mathrm{-\infty }\wedge \mathrm{-\infty }=\mathrm{+\infty }\right)\right)\vee \left(\left({A}\in ℝ\wedge \mathrm{-\infty }=\mathrm{+\infty }\right)\vee \left({A}=\mathrm{-\infty }\wedge \mathrm{-\infty }\in ℝ\right)\right)\right)\right)$
16 12 15 mtbiri ${⊢}{A}\in {ℝ}^{*}\to ¬{A}<\mathrm{-\infty }$