Theorem orng0le1

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

	Ref	Expression
Hypotheses	orng0le1.1	⊢ 0 = ( 0g ‘ 𝐹 )
	orng0le1.2	⊢ 1 = ( 1r ‘ 𝐹 )
	orng0le1.3	⊢ ≤ = ( le ‘ 𝐹 )
Assertion	orng0le1	⊢ ( 𝐹 ∈ oRing → 0 ≤ 1 )

Proof

Step	Hyp	Ref	Expression
1		orng0le1.1	⊢ 0 = ( 0g ‘ 𝐹 )
2		orng0le1.2	⊢ 1 = ( 1r ‘ 𝐹 )
3		orng0le1.3	⊢ ≤ = ( le ‘ 𝐹 )
4		orngring	⊢ ( 𝐹 ∈ oRing → 𝐹 ∈ Ring )
5		eqid	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
6	5 2	ringidcl	⊢ ( 𝐹 ∈ Ring → 1 ∈ ( Base ‘ 𝐹 ) )
7	4 6	syl	⊢ ( 𝐹 ∈ oRing → 1 ∈ ( Base ‘ 𝐹 ) )
8		eqid	⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
9	5 3 1 8	orngsqr	⊢ ( ( 𝐹 ∈ oRing ∧ 1 ∈ ( Base ‘ 𝐹 ) ) → 0 ≤ ( 1 ( .r ‘ 𝐹 ) 1 ) )
10	7 9	mpdan	⊢ ( 𝐹 ∈ oRing → 0 ≤ ( 1 ( .r ‘ 𝐹 ) 1 ) )
11	5 8 2	ringlidm	⊢ ( ( 𝐹 ∈ Ring ∧ 1 ∈ ( Base ‘ 𝐹 ) ) → ( 1 ( .r ‘ 𝐹 ) 1 ) = 1 )
12	4 6 11	syl2anc2	⊢ ( 𝐹 ∈ oRing → ( 1 ( .r ‘ 𝐹 ) 1 ) = 1 )
13	10 12	breqtrd	⊢ ( 𝐹 ∈ oRing → 0 ≤ 1 )