Metamath Proof Explorer


Theorem orng0le1

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

Ref Expression
Hypotheses orng0le1.1 0 ˙ = 0 F
orng0le1.2 1 ˙ = 1 F
orng0le1.3 ˙ = F
Assertion orng0le1 F oRing 0 ˙ ˙ 1 ˙

Proof

Step Hyp Ref Expression
1 orng0le1.1 0 ˙ = 0 F
2 orng0le1.2 1 ˙ = 1 F
3 orng0le1.3 ˙ = F
4 orngring F oRing F Ring
5 eqid Base F = Base F
6 5 2 ringidcl F Ring 1 ˙ Base F
7 4 6 syl F oRing 1 ˙ Base F
8 eqid F = F
9 5 3 1 8 orngsqr F oRing 1 ˙ Base F 0 ˙ ˙ 1 ˙ F 1 ˙
10 7 9 mpdan F oRing 0 ˙ ˙ 1 ˙ F 1 ˙
11 5 8 2 ringlidm F Ring 1 ˙ Base F 1 ˙ F 1 ˙ = 1 ˙
12 4 6 11 syl2anc2 F oRing 1 ˙ F 1 ˙ = 1 ˙
13 10 12 breqtrd F oRing 0 ˙ ˙ 1 ˙