Metamath Proof Explorer


Theorem qdrng

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

Ref Expression
Hypothesis qrng.q 𝑄 = ( ℂflds ℚ )
Assertion qdrng 𝑄 ∈ DivRing

Proof

Step Hyp Ref Expression
1 qrng.q 𝑄 = ( ℂflds ℚ )
2 qsubdrg ( ℚ ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂflds ℚ ) ∈ DivRing )
3 2 simpri ( ℂflds ℚ ) ∈ DivRing
4 1 3 eqeltri 𝑄 ∈ DivRing