Description: In an ordered field, the ring unity is strictly positive. (Contributed by Thierry Arnoux, 21-Jan-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | orng0le1.1 | |
|
orng0le1.2 | |
||
ofld0lt1.3 | |
||
Assertion | ofldlt1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orng0le1.1 | |
|
2 | orng0le1.2 | |
|
3 | ofld0lt1.3 | |
|
4 | isofld | |
|
5 | 4 | simprbi | |
6 | eqid | |
|
7 | 1 2 6 | orng0le1 | |
8 | 5 7 | syl | |
9 | ofldfld | |
|
10 | isfld | |
|
11 | 10 | simplbi | |
12 | 1 2 | drngunz | |
13 | 9 11 12 | 3syl | |
14 | 13 | necomd | |
15 | 1 | fvexi | |
16 | 2 | fvexi | |
17 | 6 3 | pltval | |
18 | 15 16 17 | mp3an23 | |
19 | 8 14 18 | mpbir2and | |