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=fld𝑠
Assertion qdrng QDivRing

Proof

Step Hyp Ref Expression
1 qrng.q Q=fld𝑠
2 qsubdrg SubRingfldfld𝑠DivRing
3 2 simpri fld𝑠DivRing
4 1 3 eqeltri QDivRing