Definition df-zring 21554

Description: The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.)

Assertion

Ref	Expression
df-zring	⊢ ℤring = (ℂfld ↾s ℤ)

Detailed syntax breakdown of Definition df-zring

Step	Hyp	Ref	Expression
1		czring 21553	. 2 class ℤring
2		ccnfld 21479	. . 3 class ℂfld
3		cz 12579	. . 3 class ℤ
4		cress 17278	. . 3 class ↾s
5	2, 3, 4	co 7400	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1563	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  21555  zringbas  21560  zringplusg  21561  zringsub  21562  zringmulg  21563  zringmulr  21564  zring0  21565  zring1  21566  zringlpirlem1  21569  zringunit  21573  zringcyg  21576  zringsubgval  21577  zringmpg  21578  prmirred  21581  zndvds  21656  zringnrg  24902  zlmclm  25228  zclmncvs  25264  lgseisenlem4  27496  gsumzrsum  33293  zringnm  34260