orng0le1

Description: In an ordered ring, the ring unity is positive. (Contributed by Thierry Arnoux, 21-Jan-2018)

	Ref	Expression
Hypotheses	orng0le1.1	$⊢ \underset{˙}{0} = 0_{F}$
	orng0le1.2	$⊢ \underset{˙}{1} = 1_{F}$
	orng0le1.3	$⊢ \underset{˙}{\leq} = \leq_{F}$
Assertion	orng0le1	$⊢ F \in oRing \to \underset{˙}{0} \underset{˙}{\leq} \underset{˙}{1}$

Step	Hyp	Ref	Expression
1		orng0le1.1	$⊢ \underset{˙}{0} = 0_{F}$
2		orng0le1.2	$⊢ \underset{˙}{1} = 1_{F}$
3		orng0le1.3	$⊢ \underset{˙}{\leq} = \leq_{F}$
4		orngring	$⊢ F \in oRing \to F \in Ring$
5		eqid	$⊢ {Base}_{F} = {Base}_{F}$
6	5 2	ringidcl	$⊢ F \in Ring \to \underset{˙}{1} \in {Base}_{F}$
7	4 6	syl	$⊢ F \in oRing \to \underset{˙}{1} \in {Base}_{F}$
8		eqid	$⊢ \cdot_{F} = \cdot_{F}$
9	5 3 1 8	orngsqr	$⊢ (F \in oRing \land \underset{˙}{1} \in {Base}_{F}) \to \underset{˙}{0} \underset{˙}{\leq} (\underset{˙}{1} \cdot_{F} \underset{˙}{1})$
10	7 9	mpdan	$⊢ F \in oRing \to \underset{˙}{0} \underset{˙}{\leq} (\underset{˙}{1} \cdot_{F} \underset{˙}{1})$
11	5 8 2	ringlidm	$⊢ (F \in Ring \land \underset{˙}{1} \in {Base}_{F}) \to \underset{˙}{1} \cdot_{F} \underset{˙}{1} = \underset{˙}{1}$
12	4 6 11	syl2anc2	$⊢ F \in oRing \to \underset{˙}{1} \cdot_{F} \underset{˙}{1} = \underset{˙}{1}$
13	10 12	breqtrd	$⊢ F \in oRing \to \underset{˙}{0} \underset{˙}{\leq} \underset{˙}{1}$

Metamath Proof Explorer