Metamath Proof Explorer


Theorem qsubdrg

Description: The rational numbers form a division subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Assertion qsubdrg SubRingfldfld𝑠DivRing

Proof

Step Hyp Ref Expression
1 qcn xx
2 qaddcl xyx+y
3 qnegcl xx
4 zssq
5 1z 1
6 4 5 sselii 1
7 qmulcl xyxy
8 qreccl xx01x
9 1 2 3 6 7 8 cnsubdrglem SubRingfldfld𝑠DivRing