Definition df-gz 16968

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	⊢ ℤ[i] = {𝑥 ∈ ℂ ∣ ((ℜ‘𝑥) ∈ ℤ ∧ (ℑ‘𝑥) ∈ ℤ)}

Detailed syntax breakdown of Definition df-gz

Step	Hyp	Ref	Expression
1		cgz 16967	. 2 class ℤ[i]
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1539	. . . . . 6 class 𝑥
4		cre 15136	. . . . . 6 class ℜ
5	3, 4	cfv 6561	. . . . 5 class (ℜ‘𝑥)
6		cz 12613	. . . . 5 class ℤ
7	5, 6	wcel 2108	. . . 4 wff (ℜ‘𝑥) ∈ ℤ
8		cim 15137	. . . . . 6 class ℑ
9	3, 8	cfv 6561	. . . . 5 class (ℑ‘𝑥)
10	9, 6	wcel 2108	. . . 4 wff (ℑ‘𝑥) ∈ ℤ
11	7, 10	wa 395	. . 3 wff ((ℜ‘𝑥) ∈ ℤ ∧ (ℑ‘𝑥) ∈ ℤ)
12		cc 11153	. . 3 class ℂ
13	11, 2, 12	crab 3436	. 2 class {𝑥 ∈ ℂ ∣ ((ℜ‘𝑥) ∈ ℤ ∧ (ℑ‘𝑥) ∈ ℤ)}
14	1, 13	wceq 1540	1 wff ℤ[i] = {𝑥 ∈ ℂ ∣ ((ℜ‘𝑥) ∈ ℤ ∧ (ℑ‘𝑥) ∈ ℤ)}

This definition is referenced by:  elgz  16969