Metamath Proof Explorer

Theorem gzcrng

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

Ref Expression
Assertion gzcrng 
|- ( CCfld |`s Z[i] ) e. CRing

Proof

Step Hyp Ref Expression
1 cncrng 
 |-  CCfld e. CRing
2 gzsubrg 
 |-  Z[i] e. ( SubRing ` CCfld )
3 eqid 
 |-  ( CCfld |`s Z[i] ) = ( CCfld |`s Z[i] )
4 3 subrgcrng 
 |-  ( ( CCfld e. CRing /\ Z[i] e. ( SubRing ` CCfld ) ) -> ( CCfld |`s Z[i] ) e. CRing )
5 1 2 4 mp2an 
 |-  ( CCfld |`s Z[i] ) e. CRing