Description: There is no smallest positive real number. (Contributed by NM, 28-Oct-2004)
Ref | Expression | ||
---|---|---|---|
Assertion | nominpos | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rehalfcl | |
|
2 | 2re | |
|
3 | 2pos | |
|
4 | divgt0 | |
|
5 | 2 3 4 | mpanr12 | |
6 | 5 | ex | |
7 | halfpos | |
|
8 | 7 | biimpd | |
9 | 6 8 | jcad | |
10 | breq2 | |
|
11 | breq1 | |
|
12 | 10 11 | anbi12d | |
13 | 12 | rspcev | |
14 | 1 9 13 | syl6an | |
15 | iman | |
|
16 | 14 15 | sylib | |
17 | 16 | nrex | |