Theorem zsubrg

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

	Ref	Expression
Assertion	zsubrg	$$⊢\mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		zcn	$$⊢x\in \mathbb{Z}\to x\in ℂ$$
2		zaddcl	$$⊢\left(x\in \mathbb{Z}\wedge y\in \mathbb{Z}\right)\to x+y\in \mathbb{Z}$$
3		znegcl	$$⊢x\in \mathbb{Z}\to -x\in \mathbb{Z}$$
4		1z	$$⊢1\in \mathbb{Z}$$
5		zmulcl	$$⊢\left(x\in \mathbb{Z}\wedge y\in \mathbb{Z}\right)\to xy\in \mathbb{Z}$$
6	1 2 3 4 5	cnsubrglem	$$⊢\mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$