Metamath Proof Explorer

Theorem zsubrg

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

		Ref	Expression
	Assertion	zsubrg	$⊢ ℤ \in SubRing (ℂ_{fld})$

Step	Hyp	Ref	Expression
1		zcn	$⊢ x \in ℤ \to x \in ℂ$
2		zaddcl	$⊢ (x \in ℤ \land y \in ℤ) \to x + y \in ℤ$
3		znegcl	$⊢ x \in ℤ \to - x \in ℤ$
4		1z	$⊢ 1 \in ℤ$
5		zmulcl	$⊢ (x \in ℤ \land y \in ℤ) \to x y \in ℤ$
6	1 2 3 4 5	cnsubrglem	$⊢ ℤ \in SubRing (ℂ_{fld})$