Metamath Proof Explorer


Theorem resrng

Description: The real numbers form a star ring. (Contributed by Thierry Arnoux, 19-Apr-2019) (Proof shortened by Thierry Arnoux, 11-Jan-2025)

Ref Expression
Assertion resrng fld *-Ring

Proof

Step Hyp Ref Expression
1 rebase = Base fld
2 refldcj * = * fld
3 refld fld Field
4 3 a1i fld Field
5 4 fldcrngd fld CRing
6 cjre x x = x
7 6 adantl x x = x
8 1 2 5 7 idsrngd fld *-Ring
9 8 mptru fld *-Ring