Metamath Proof Explorer


Theorem nominpos

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

Ref Expression
Assertion nominpos ¬x0<x¬y0<yy<x

Proof

Step Hyp Ref Expression
1 rehalfcl xx2
2 2re 2
3 2pos 0<2
4 divgt0 x0<x20<20<x2
5 2 3 4 mpanr12 x0<x0<x2
6 5 ex x0<x0<x2
7 halfpos x0<xx2<x
8 7 biimpd x0<xx2<x
9 6 8 jcad x0<x0<x2x2<x
10 breq2 y=x20<y0<x2
11 breq1 y=x2y<xx2<x
12 10 11 anbi12d y=x20<yy<x0<x2x2<x
13 12 rspcev x20<x2x2<xy0<yy<x
14 1 9 13 syl6an x0<xy0<yy<x
15 iman 0<xy0<yy<x¬0<x¬y0<yy<x
16 14 15 sylib x¬0<x¬y0<yy<x
17 16 nrex ¬x0<x¬y0<yy<x