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	⊢ ( ℚ ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s ℚ ) ∈ DivRing )

Proof

Step	Hyp	Ref	Expression
1		qcn	⊢ ( 𝑥 ∈ ℚ → 𝑥 ∈ ℂ )
2		qaddcl	⊢ ( ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) → ( 𝑥 + 𝑦 ) ∈ ℚ )
3		qnegcl	⊢ ( 𝑥 ∈ ℚ → - 𝑥 ∈ ℚ )
4		zssq	⊢ ℤ ⊆ ℚ
5		1z	⊢ 1 ∈ ℤ
6	4 5	sselii	⊢ 1 ∈ ℚ
7		qmulcl	⊢ ( ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) → ( 𝑥 · 𝑦 ) ∈ ℚ )
8		qreccl	⊢ ( ( 𝑥 ∈ ℚ ∧ 𝑥 ≠ 0 ) → ( 1 / 𝑥 ) ∈ ℚ )
9	1 2 3 6 7 8	cnsubdrglem	⊢ ( ℚ ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s ℚ ) ∈ DivRing )