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	$$⊢\underset{\dot{}}{0}=0_F$$
	orng0le1.2	$$⊢\underset{\dot{}}{1}=1_F$$
	ofld0lt1.3	$$⊢\underset{\dot{}}{<}={<}_F$$
Assertion	ofldlt1	$$⊢F\in \mathrm{oField}\to \underset{\dot{}}{0}\underset{\dot{}}{<}\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		orng0le1.1	$$⊢\underset{\dot{}}{0}=0_F$$
2		orng0le1.2	$$⊢\underset{\dot{}}{1}=1_F$$
3		ofld0lt1.3	$$⊢\underset{\dot{}}{<}={<}_F$$
4		isofld	$$⊢F\in \mathrm{oField}\leftrightarrow \left(F\in \mathrm{Field}\wedge F\in \mathrm{oRing}\right)$$
5	4	simprbi	$$⊢F\in \mathrm{oField}\to F\in \mathrm{oRing}$$
6		eqid	$$⊢{\le }_F={\le }_F$$
7	1 2 6	orng0le1	$$⊢F\in \mathrm{oRing}\to \underset{\dot{}}{0}{\le }_F\underset{\dot{}}{1}$$
8	5 7	syl	$$⊢F\in \mathrm{oField}\to \underset{\dot{}}{0}{\le }_F\underset{\dot{}}{1}$$
9		ofldfld	$$⊢F\in \mathrm{oField}\to F\in \mathrm{Field}$$
10		isfld	$$⊢F\in \mathrm{Field}\leftrightarrow \left(F\in \mathrm{DivRing}\wedge F\in \mathrm{CRing}\right)$$
11	10	simplbi	$$⊢F\in \mathrm{Field}\to F\in \mathrm{DivRing}$$
12	1 2	drngunz	$$⊢F\in \mathrm{DivRing}\to \underset{\dot{}}{1}\ne \underset{\dot{}}{0}$$
13	9 11 12	3syl	$$⊢F\in \mathrm{oField}\to \underset{\dot{}}{1}\ne \underset{\dot{}}{0}$$
14	13	necomd	$$⊢F\in \mathrm{oField}\to \underset{\dot{}}{0}\ne \underset{\dot{}}{1}$$
15	1	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
16	2	fvexi	$$⊢\underset{\dot{}}{1}\in \mathrm{V}$$
17	6 3	pltval	$$⊢\left(F\in \mathrm{oField}\wedge \underset{\dot{}}{0}\in \mathrm{V}\wedge \underset{\dot{}}{1}\in \mathrm{V}\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}\underset{\dot{}}{1}\leftrightarrow \left(\underset{\dot{}}{0}{\le }_F\underset{\dot{}}{1}\wedge \underset{\dot{}}{0}\ne \underset{\dot{}}{1}\right)\right)$$
18	15 16 17	mp3an23	$$⊢F\in \mathrm{oField}\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}\underset{\dot{}}{1}\leftrightarrow \left(\underset{\dot{}}{0}{\le }_F\underset{\dot{}}{1}\wedge \underset{\dot{}}{0}\ne \underset{\dot{}}{1}\right)\right)$$
19	8 14 18	mpbir2and	$$⊢F\in \mathrm{oField}\to \underset{\dot{}}{0}\underset{\dot{}}{<}\underset{\dot{}}{1}$$