Metamath Proof Explorer


Theorem recrng

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

Ref Expression
Assertion recrng fld*-Ring

Proof

Step Hyp Ref Expression
1 rebase =Basefld
2 refldcj *=*fld
3 refld fldField
4 isfld fldFieldfldDivRingfldCRing
5 3 4 mpbi fldDivRingfldCRing
6 5 simpri fldCRing
7 6 a1i fldCRing
8 cjre xx=x
9 8 adantl xx=x
10 1 2 7 9 idsrngd fld*-Ring
11 10 mptru fld*-Ring