Metamath Proof Explorer


Theorem nominpos

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

Ref Expression
Assertion nominpos ¬ x 0 < x ¬ y 0 < y y < x

Proof

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