This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( 0g ‘ 𝐹 )
orng0le1.2 ⊢ 1 = ( 1r ‘ 𝐹 )
ofld0lt1.3 ⊢ < = ( lt ‘ 𝐹 )
Assertion ofldlt1 ( 𝐹 ∈ oField → 0 < 1 )

Proof

Step Hyp Ref Expression
1 orng0le1.1 ⊢ 0 = ( 0g ‘ 𝐹 )
2 orng0le1.2 ⊢ 1 = ( 1r ‘ 𝐹 )
3 ofld0lt1.3 ⊢ < = ( lt ‘ 𝐹 )
4 isofld ⊢ ( 𝐹 ∈ oField ↔ ( 𝐹 ∈ Field ∧ 𝐹 ∈ oRing ) )
5 4 simprbi ⊢ ( 𝐹 ∈ oField → 𝐹 ∈ oRing )
6 eqid ⊢ ( le ‘ 𝐹 ) = ( le ‘ 𝐹 )
7 1 2 6 orng0le1 ⊢ ( 𝐹 ∈ oRing → 0 ( le ‘ 𝐹 ) 1 )
8 5 7 syl ⊢ ( 𝐹 ∈ oField → 0 ( le ‘ 𝐹 ) 1 )
9 ofldfld ⊢ ( 𝐹 ∈ oField → 𝐹 ∈ Field )
10 isfld ⊢ ( 𝐹 ∈ Field ↔ ( 𝐹 ∈ DivRing ∧ 𝐹 ∈ CRing ) )
11 10 simplbi ⊢ ( 𝐹 ∈ Field → 𝐹 ∈ DivRing )
12 1 2 drngunz ⊢ ( 𝐹 ∈ DivRing → 1 ≠ 0 )
13 9 11 12 3syl ⊢ ( 𝐹 ∈ oField → 1 ≠ 0 )
14 13 necomd ⊢ ( 𝐹 ∈ oField → 0 ≠ 1 )
15 1 fvexi ⊢ 0 ∈ V
16 2 fvexi ⊢ 1 ∈ V
17 6 3 pltval ⊢ ( ( 𝐹 ∈ oField ∧ 0 ∈ V ∧ 1 ∈ V ) → ( 0 < 1 ↔ ( 0 ( le ‘ 𝐹 ) 1 ∧ 0 ≠ 1 ) ) )
18 15 16 17 mp3an23 ⊢ ( 𝐹 ∈ oField → ( 0 < 1 ↔ ( 0 ( le ‘ 𝐹 ) 1 ∧ 0 ≠ 1 ) ) )
19 8 14 18 mpbir2and ⊢ ( 𝐹 ∈ oField → 0 < 1 )