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 = ( 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 )