Theorem qfld

Description: The field of rational numbers is a field. (Contributed by Thierry Arnoux, 19-Oct-2025)

	Ref	Expression
Hypothesis	qfld.1	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
Assertion	qfld	$$⊢Q\in \mathrm{Field}$$

Proof

Step	Hyp	Ref	Expression
1		qfld.1	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
2	1	qdrng	$$⊢Q\in \mathrm{DivRing}$$
3		cncrng	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CRing}$$
4		qsubdrg	$$⊢\left(\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{DivRing}\right)$$
5	4	simpli	$$⊢\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
6	1	subrgcrng	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{CRing}\wedge \mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)\to Q\in \mathrm{CRing}$$
7	3 5 6	mp2an	$$⊢Q\in \mathrm{CRing}$$
8		isfld	$$⊢Q\in \mathrm{Field}\leftrightarrow \left(Q\in \mathrm{DivRing}\wedge Q\in \mathrm{CRing}\right)$$
9	2 7 8	mpbir2an	$$⊢Q\in \mathrm{Field}$$