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	$⊢ ℤ [i] = \{x \in ℂ \| (ℜ (x) \in ℤ \land ℑ (x) \in ℤ)\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgz	$class ℤ [i]$
1		vx	$setvar x$
2		cc	$class ℂ$
3		cre	$class ℜ$
4	1	cv	$setvar x$
5	4 3	cfv	$class ℜ (x)$
6		cz	$class ℤ$
7	5 6	wcel	$wff ℜ (x) \in ℤ$
8		cim	$class ℑ$
9	4 8	cfv	$class ℑ (x)$
10	9 6	wcel	$wff ℑ (x) \in ℤ$
11	7 10	wa	$wff (ℜ (x) \in ℤ \land ℑ (x) \in ℤ)$
12	11 1 2	crab	$class \{x \in ℂ \| (ℜ (x) \in ℤ \land ℑ (x) \in ℤ)\}$
13	0 12	wceq	$wff ℤ [i] = \{x \in ℂ \| (ℜ (x) \in ℤ \land ℑ (x) \in ℤ)\}$

Metamath Proof Explorer

Definition df-gz

Detailed syntax breakdown