Definition df-gz 12358

Description: Define the set of gaussian integers, which are complex numbers whose real and imaginary parts are integers. (Note that the [ _i ] is actually part of the symbol token and has no independent meaning.) (Contributed by Mario Carneiro, 14-Jul-2014.)

Assertion

Ref	Expression
df-gz	|- ZZ[_i] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }

Detailed syntax breakdown of Definition df-gz

Step	Hyp	Ref	Expression
1		cgz 12357	. 2 class ZZ[_i]
2		vx	. . . . . . 7 setvar x
3	2	cv 1352	. . . . . 6 class x
4		cre 10840	. . . . . 6 class Re
5	3, 4	cfv 5213	. . . . 5 class ( Re ` x )
6		cz 9247	. . . . 5 class ZZ
7	5, 6	wcel 2148	. . . 4 wff ( Re ` x ) e. ZZ
8		cim 10841	. . . . . 6 class Im
9	3, 8	cfv 5213	. . . . 5 class ( Im ` x )
10	9, 6	wcel 2148	. . . 4 wff ( Im ` x ) e. ZZ
11	7, 10	wa 104	. . 3 wff ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ )
12		cc 7804	. . 3 class CC
13	11, 2, 12	crab 2459	. 2 class { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }
14	1, 13	wceq 1353	1 wff ZZ[_i] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }

This definition is referenced by:  elgz  12359