Metamath Proof Explorer

Theorem refld

Description: The real numbers form a field. (Contributed by Thierry Arnoux, 1-Nov-2017)

Ref Expression
Assertion refld 
|- RRfld e. Field

Proof

Step Hyp Ref Expression
1 resubdrg 
 |-  ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing )
2 1 simpri 
 |-  RRfld e. DivRing
3 df-refld 
 |-  RRfld = ( CCfld |`s RR )
4 cncrng 
 |-  CCfld e. CRing
5 1 simpli 
 |-  RR e. ( SubRing ` CCfld )
6 eqid 
 |-  ( CCfld |`s RR ) = ( CCfld |`s RR )
7 6 subrgcrng 
 |-  ( ( CCfld e. CRing /\ RR e. ( SubRing ` CCfld ) ) -> ( CCfld |`s RR ) e. CRing )
8 4 5 7 mp2an 
 |-  ( CCfld |`s RR ) e. CRing
9 3 8 eqeltri 
 |-  RRfld e. CRing
10 isfld 
 |-  ( RRfld e. Field <-> ( RRfld e. DivRing /\ RRfld e. CRing ) )
11 2 9 10 mpbir2an 
 |-  RRfld e. Field