Metamath Proof Explorer


Theorem ofldlt1

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

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

Proof

Step Hyp Ref Expression
1 orng0le1.1 0 ˙ = 0 F
2 orng0le1.2 1 ˙ = 1 F
3 ofld0lt1.3 < ˙ = < F
4 isofld F oField F Field F oRing
5 4 simprbi F oField F oRing
6 eqid F = F
7 1 2 6 orng0le1 F oRing 0 ˙ F 1 ˙
8 5 7 syl F oField 0 ˙ F 1 ˙
9 ofldfld F oField F Field
10 isfld F Field F DivRing F CRing
11 10 simplbi F Field F DivRing
12 1 2 drngunz F DivRing 1 ˙ 0 ˙
13 9 11 12 3syl F oField 1 ˙ 0 ˙
14 13 necomd F oField 0 ˙ 1 ˙
15 1 fvexi 0 ˙ V
16 2 fvexi 1 ˙ V
17 6 3 pltval F oField 0 ˙ V 1 ˙ V 0 ˙ < ˙ 1 ˙ 0 ˙ F 1 ˙ 0 ˙ 1 ˙
18 15 16 17 mp3an23 F oField 0 ˙ < ˙ 1 ˙ 0 ˙ F 1 ˙ 0 ˙ 1 ˙
19 8 14 18 mpbir2and F oField 0 ˙ < ˙ 1 ˙