Definition df-gz

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgz	|- Z[i]
1		vx	|- x
2		cc	|- CC
3		cre	|- Re
4	1	cv	|- x
5	4 3	cfv	|- ( Re ` x )
6		cz	|- ZZ
7	5 6	wcel	|- ( Re ` x ) e. ZZ
8		cim	|- Im
9	4 8	cfv	|- ( Im ` x )
10	9 6	wcel	|- ( Im ` x ) e. ZZ
11	7 10	wa	|- ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ )
12	11 1 2	crab	|- { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }
13	0 12	wceq	|- Z[i] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }