# Metamath Proof Explorer

## Theorem reltxrnmnf

Description: For all extended real numbers not being minus infinity there is a smaller real number. (Contributed by AV, 5-Sep-2020)

Ref Expression
Assertion reltxrnmnf ${⊢}\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\mathrm{-\infty }<{x}\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{y}<{x}\right)$

### Proof

Step Hyp Ref Expression
1 elxr ${⊢}{x}\in {ℝ}^{*}↔\left({x}\in ℝ\vee {x}=\mathrm{+\infty }\vee {x}=\mathrm{-\infty }\right)$
2 reltre ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{y}<{x}$
3 2 rspec ${⊢}{x}\in ℝ\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{y}<{x}$
4 3 a1d ${⊢}{x}\in ℝ\to \left(\mathrm{-\infty }<{x}\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{y}<{x}\right)$
5 0red ${⊢}{x}=\mathrm{+\infty }\to 0\in ℝ$
6 breq1 ${⊢}{y}=0\to \left({y}<{x}↔0<{x}\right)$
7 6 adantl ${⊢}\left({x}=\mathrm{+\infty }\wedge {y}=0\right)\to \left({y}<{x}↔0<{x}\right)$
8 0ltpnf ${⊢}0<\mathrm{+\infty }$
9 breq2 ${⊢}{x}=\mathrm{+\infty }\to \left(0<{x}↔0<\mathrm{+\infty }\right)$
10 8 9 mpbiri ${⊢}{x}=\mathrm{+\infty }\to 0<{x}$
11 5 7 10 rspcedvd ${⊢}{x}=\mathrm{+\infty }\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{y}<{x}$
12 11 a1d ${⊢}{x}=\mathrm{+\infty }\to \left(\mathrm{-\infty }<{x}\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{y}<{x}\right)$
13 breq2 ${⊢}{x}=\mathrm{-\infty }\to \left(\mathrm{-\infty }<{x}↔\mathrm{-\infty }<\mathrm{-\infty }\right)$
14 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
15 nltmnf ${⊢}\mathrm{-\infty }\in {ℝ}^{*}\to ¬\mathrm{-\infty }<\mathrm{-\infty }$
16 15 pm2.21d ${⊢}\mathrm{-\infty }\in {ℝ}^{*}\to \left(\mathrm{-\infty }<\mathrm{-\infty }\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{y}<{x}\right)$
17 14 16 ax-mp ${⊢}\mathrm{-\infty }<\mathrm{-\infty }\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{y}<{x}$
18 13 17 syl6bi ${⊢}{x}=\mathrm{-\infty }\to \left(\mathrm{-\infty }<{x}\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{y}<{x}\right)$
19 4 12 18 3jaoi ${⊢}\left({x}\in ℝ\vee {x}=\mathrm{+\infty }\vee {x}=\mathrm{-\infty }\right)\to \left(\mathrm{-\infty }<{x}\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{y}<{x}\right)$
20 1 19 sylbi ${⊢}{x}\in {ℝ}^{*}\to \left(\mathrm{-\infty }<{x}\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{y}<{x}\right)$
21 20 rgen ${⊢}\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\mathrm{-\infty }<{x}\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}{y}<{x}\right)$