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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgz	⊢ ℤ[i]
1		vx	⊢ 𝑥
2		cc	⊢ ℂ
3		cre	⊢ ℜ
4	1	cv	⊢ 𝑥
5	4 3	cfv	⊢ ( ℜ ‘ 𝑥 )
6		cz	⊢ ℤ
7	5 6	wcel	⊢ ( ℜ ‘ 𝑥 ) ∈ ℤ
8		cim	⊢ ℑ
9	4 8	cfv	⊢ ( ℑ ‘ 𝑥 )
10	9 6	wcel	⊢ ( ℑ ‘ 𝑥 ) ∈ ℤ
11	7 10	wa	⊢ ( ( ℜ ‘ 𝑥 ) ∈ ℤ ∧ ( ℑ ‘ 𝑥 ) ∈ ℤ )
12	11 1 2	crab	⊢ { 𝑥 ∈ ℂ ∣ ( ( ℜ ‘ 𝑥 ) ∈ ℤ ∧ ( ℑ ‘ 𝑥 ) ∈ ℤ ) }
13	0 12	wceq	⊢ ℤ[i] = { 𝑥 ∈ ℂ ∣ ( ( ℜ ‘ 𝑥 ) ∈ ℤ ∧ ( ℑ ‘ 𝑥 ) ∈ ℤ ) }