Metamath Proof Explorer

Theorem gzsubrg

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

Ref Expression
Assertion gzsubrg 
|- Z[i] e. ( SubRing ` CCfld )

Proof

Step Hyp Ref Expression
1 gzcn 
 |-  ( x e. Z[i] -> x e. CC )
2 gzaddcl 
 |-  ( ( x e. Z[i] /\ y e. Z[i] ) -> ( x + y ) e. Z[i] )
3 gznegcl 
 |-  ( x e. Z[i] -> -u x e. Z[i] )
4 1z 
 |-  1 e. ZZ
5 zgz 
 |-  ( 1 e. ZZ -> 1 e. Z[i] )
6 4 5 ax-mp 
 |-  1 e. Z[i]
7 gzmulcl 
 |-  ( ( x e. Z[i] /\ y e. Z[i] ) -> ( x x. y ) e. Z[i] )
8 1 2 3 6 7 cnsubrglem 
 |-  Z[i] e. ( SubRing ` CCfld )