This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

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