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

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

Metamath Proof Explorer