Theorem gzcrng

Description: The gaussian integers form a commutative ring. (Contributed by Thierry Arnoux, 18-Mar-2018)

	Ref	Expression
Assertion	gzcrng	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\left[i\right]\in \mathrm{CRing}$$

Proof

Step	Hyp	Ref	Expression
1		cncrng	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CRing}$$
2		gzsubrg	$$⊢\mathbb{Z}\left[i\right]\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
3		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\left[i\right]={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\left[i\right]$$
4	3	subrgcrng	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{CRing}\wedge \mathbb{Z}\left[i\right]\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)\to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\left[i\right]\in \mathrm{CRing}$$
5	1 2 4	mp2an	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\left[i\right]\in \mathrm{CRing}$$