Metamath Proof Explorer

Theorem resubdrg

Description: The real numbers form a division subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014) (Revised by Thierry Arnoux, 30-Jun-2019)

Ref Expression
Assertion resubdrg 
|- ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing )

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( x e. RR -> x e. CC )
2 readdcl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + y ) e. RR )
3 renegcl 
 |-  ( x e. RR -> -u x e. RR )
4 1re 
 |-  1 e. RR
5 remulcl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x x. y ) e. RR )
6 rereccl 
 |-  ( ( x e. RR /\ x =/= 0 ) -> ( 1 / x ) e. RR )
7 1 2 3 4 5 6 cnsubdrglem 
 |-  ( RR e. ( SubRing ` CCfld ) /\ ( CCfld |`s RR ) e. DivRing )
8 df-refld 
 |-  RRfld = ( CCfld |`s RR )
9 8 eleq1i 
 |-  ( RRfld e. DivRing <-> ( CCfld |`s RR ) e. DivRing )
10 9 anbi2i 
 |-  ( ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing ) <-> ( RR e. ( SubRing ` CCfld ) /\ ( CCfld |`s RR ) e. DivRing ) )
11 7 10 mpbir 
 |-  ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing )