Metamath Proof Explorer

Theorem qdrng

Description: The rationals form a division ring. (Contributed by Mario Carneiro, 8-Sep-2014)

Ref Expression
Hypothesis qrng.q 
|- Q = ( CCfld |`s QQ )
Assertion qdrng 
|- Q e. DivRing

Proof

Step Hyp Ref Expression
1 qrng.q 
 |-  Q = ( CCfld |`s QQ )
2 qsubdrg 
 |-  ( QQ e. ( SubRing ` CCfld ) /\ ( CCfld |`s QQ ) e. DivRing )
3 2 simpri 
 |-  ( CCfld |`s QQ ) e. DivRing
4 1 3 eqeltri 
 |-  Q e. DivRing