Metamath Proof Explorer

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 = x ∈ ℂ | ℜ ⁡ x ∈ ℤ ∧ ℑ ⁡ x ∈ ℤ

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 ∈ ℤ
8 cim class ℑ
9 4 8 cfv class ℑ ⁡ x
10 9 6 wcel wff ℑ ⁡ x ∈ ℤ
11 7 10 wa wff ℜ ⁡ x ∈ ℤ ∧ ℑ ⁡ x ∈ ℤ
12 11 1 2 crab class x ∈ ℂ | ℜ ⁡ x ∈ ℤ ∧ ℑ ⁡ x ∈ ℤ
13 0 12 wceq wff ℤ i = x ∈ ℂ | ℜ ⁡ x ∈ ℤ ∧ ℑ ⁡ x ∈ ℤ