# Metamath Proof Explorer

## Theorem nominpos

Description: There is no smallest positive real number. (Contributed by NM, 28-Oct-2004)

Ref Expression
Assertion nominpos ${⊢}¬\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left(0<{x}\wedge ¬\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left(0<{y}\wedge {y}<{x}\right)\right)$

### Proof

Step Hyp Ref Expression
1 rehalfcl ${⊢}{x}\in ℝ\to \frac{{x}}{2}\in ℝ$
2 2re ${⊢}2\in ℝ$
3 2pos ${⊢}0<2$
4 divgt0 ${⊢}\left(\left({x}\in ℝ\wedge 0<{x}\right)\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to 0<\frac{{x}}{2}$
5 2 3 4 mpanr12 ${⊢}\left({x}\in ℝ\wedge 0<{x}\right)\to 0<\frac{{x}}{2}$
6 5 ex ${⊢}{x}\in ℝ\to \left(0<{x}\to 0<\frac{{x}}{2}\right)$
7 halfpos ${⊢}{x}\in ℝ\to \left(0<{x}↔\frac{{x}}{2}<{x}\right)$
8 7 biimpd ${⊢}{x}\in ℝ\to \left(0<{x}\to \frac{{x}}{2}<{x}\right)$
9 6 8 jcad ${⊢}{x}\in ℝ\to \left(0<{x}\to \left(0<\frac{{x}}{2}\wedge \frac{{x}}{2}<{x}\right)\right)$
10 breq2 ${⊢}{y}=\frac{{x}}{2}\to \left(0<{y}↔0<\frac{{x}}{2}\right)$
11 breq1 ${⊢}{y}=\frac{{x}}{2}\to \left({y}<{x}↔\frac{{x}}{2}<{x}\right)$
12 10 11 anbi12d ${⊢}{y}=\frac{{x}}{2}\to \left(\left(0<{y}\wedge {y}<{x}\right)↔\left(0<\frac{{x}}{2}\wedge \frac{{x}}{2}<{x}\right)\right)$
13 12 rspcev ${⊢}\left(\frac{{x}}{2}\in ℝ\wedge \left(0<\frac{{x}}{2}\wedge \frac{{x}}{2}<{x}\right)\right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left(0<{y}\wedge {y}<{x}\right)$
14 1 9 13 syl6an ${⊢}{x}\in ℝ\to \left(0<{x}\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left(0<{y}\wedge {y}<{x}\right)\right)$
15 iman ${⊢}\left(0<{x}\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left(0<{y}\wedge {y}<{x}\right)\right)↔¬\left(0<{x}\wedge ¬\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left(0<{y}\wedge {y}<{x}\right)\right)$
16 14 15 sylib ${⊢}{x}\in ℝ\to ¬\left(0<{x}\wedge ¬\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left(0<{y}\wedge {y}<{x}\right)\right)$
17 16 nrex ${⊢}¬\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left(0<{x}\wedge ¬\exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\left(0<{y}\wedge {y}<{x}\right)\right)$