Theorem gzcrng

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

	Ref	Expression
Assertion	gzcrng	⊢ ( ℂfld ↾s ℤ[i] ) ∈ CRing

Proof

Step	Hyp	Ref	Expression
1		cncrng	⊢ ℂfld ∈ CRing
2		gzsubrg	⊢ ℤ[i] ∈ ( SubRing ‘ ℂfld )
3		eqid	⊢ ( ℂfld ↾s ℤ[i] ) = ( ℂfld ↾s ℤ[i] )
4	3	subrgcrng	⊢ ( ( ℂfld ∈ CRing ∧ ℤ[i] ∈ ( SubRing ‘ ℂfld ) ) → ( ℂfld ↾s ℤ[i] ) ∈ CRing )
5	1 2 4	mp2an	⊢ ( ℂfld ↾s ℤ[i] ) ∈ CRing