Metamath Proof Explorer


Theorem ofldlt1

Description: In an ordered field, the ring unity is strictly positive. (Contributed by Thierry Arnoux, 21-Jan-2018)

Ref Expression
Hypotheses orng0le1.1 0˙=0F
orng0le1.2 1˙=1F
ofld0lt1.3 <˙=<F
Assertion ofldlt1 FoField0˙<˙1˙

Proof

Step Hyp Ref Expression
1 orng0le1.1 0˙=0F
2 orng0le1.2 1˙=1F
3 ofld0lt1.3 <˙=<F
4 isofld FoFieldFFieldFoRing
5 4 simprbi FoFieldFoRing
6 eqid F=F
7 1 2 6 orng0le1 FoRing0˙F1˙
8 5 7 syl FoField0˙F1˙
9 ofldfld FoFieldFField
10 isfld FFieldFDivRingFCRing
11 10 simplbi FFieldFDivRing
12 1 2 drngunz FDivRing1˙0˙
13 9 11 12 3syl FoField1˙0˙
14 13 necomd FoField0˙1˙
15 1 fvexi 0˙V
16 2 fvexi 1˙V
17 6 3 pltval FoField0˙V1˙V0˙<˙1˙0˙F1˙0˙1˙
18 15 16 17 mp3an23 FoField0˙<˙1˙0˙F1˙0˙1˙
19 8 14 18 mpbir2and FoField0˙<˙1˙