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	$$⊢\left(\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{DivRing}\right)$$

Proof

Step	Hyp	Ref	Expression
1		qcn	$$⊢x\in \mathbb{Q}\to x\in ℂ$$
2		qaddcl	$$⊢\left(x\in \mathbb{Q}\wedge y\in \mathbb{Q}\right)\to x+y\in \mathbb{Q}$$
3		qnegcl	$$⊢x\in \mathbb{Q}\to -x\in \mathbb{Q}$$
4		zssq	$$⊢\mathbb{Z}\subseteq \mathbb{Q}$$
5		1z	$$⊢1\in \mathbb{Z}$$
6	4 5	sselii	$$⊢1\in \mathbb{Q}$$
7		qmulcl	$$⊢\left(x\in \mathbb{Q}\wedge y\in \mathbb{Q}\right)\to xy\in \mathbb{Q}$$
8		qreccl	$$⊢\left(x\in \mathbb{Q}\wedge x\ne 0\right)\to \frac{1}{x}\in \mathbb{Q}$$
9	1 2 3 6 7 8	cnsubdrglem	$$⊢\left(\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{DivRing}\right)$$