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 
|- ZZ e. ( SubRing ` CCfld )

Proof

Step Hyp Ref Expression
1 zcn 
 |-  ( x e. ZZ -> x e. CC )
2 zaddcl 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( x + y ) e. ZZ )
3 znegcl 
 |-  ( x e. ZZ -> -u x e. ZZ )
4 1z 
 |-  1 e. ZZ
5 zmulcl 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( x x. y ) e. ZZ )
6 1 2 3 4 5 cnsubrglem 
 |-  ZZ e. ( SubRing ` CCfld )