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 ` F )
	orng0le1.2	|- .1. = ( 1r ` F )
	ofld0lt1.3	|- .< = ( lt ` F )
Assertion	ofldlt1	|- ( F e. oField -> .0. .< .1. )

Proof

Step	Hyp	Ref	Expression
1		orng0le1.1	|- .0. = ( 0g ` F )
2		orng0le1.2	|- .1. = ( 1r ` F )
3		ofld0lt1.3	|- .< = ( lt ` F )
4		isofld	|- ( F e. oField <-> ( F e. Field /\ F e. oRing ) )
5	4	simprbi	|- ( F e. oField -> F e. oRing )
6		eqid	|- ( le ` F ) = ( le ` F )
7	1 2 6	orng0le1	|- ( F e. oRing -> .0. ( le ` F ) .1. )
8	5 7	syl	|- ( F e. oField -> .0. ( le ` F ) .1. )
9		ofldfld	|- ( F e. oField -> F e. Field )
10		isfld	|- ( F e. Field <-> ( F e. DivRing /\ F e. CRing ) )
11	10	simplbi	|- ( F e. Field -> F e. DivRing )
12	1 2	drngunz	|- ( F e. DivRing -> .1. =/= .0. )
13	9 11 12	3syl	|- ( F e. oField -> .1. =/= .0. )
14	13	necomd	|- ( F e. oField -> .0. =/= .1. )
15	1	fvexi	|- .0. e. _V
16	2	fvexi	|- .1. e. _V
17	6 3	pltval	|- ( ( F e. oField /\ .0. e. _V /\ .1. e. _V ) -> ( .0. .< .1. <-> ( .0. ( le ` F ) .1. /\ .0. =/= .1. ) ) )
18	15 16 17	mp3an23	|- ( F e. oField -> ( .0. .< .1. <-> ( .0. ( le ` F ) .1. /\ .0. =/= .1. ) ) )
19	8 14 18	mpbir2and	|- ( F e. oField -> .0. .< .1. )