![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-gz | GIF version |
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 |
---|---|
df-gz | ⊢ ℤ[i] = {𝑥 ∈ ℂ ∣ ((ℜ‘𝑥) ∈ ℤ ∧ (ℑ‘𝑥) ∈ ℤ)} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cgz 12350 | . 2 class ℤ[i] | |
2 | vx | . . . . . . 7 setvar 𝑥 | |
3 | 2 | cv 1352 | . . . . . 6 class 𝑥 |
4 | cre 10833 | . . . . . 6 class ℜ | |
5 | 3, 4 | cfv 5212 | . . . . 5 class (ℜ‘𝑥) |
6 | cz 9242 | . . . . 5 class ℤ | |
7 | 5, 6 | wcel 2148 | . . . 4 wff (ℜ‘𝑥) ∈ ℤ |
8 | cim 10834 | . . . . . 6 class ℑ | |
9 | 3, 8 | cfv 5212 | . . . . 5 class (ℑ‘𝑥) |
10 | 9, 6 | wcel 2148 | . . . 4 wff (ℑ‘𝑥) ∈ ℤ |
11 | 7, 10 | wa 104 | . . 3 wff ((ℜ‘𝑥) ∈ ℤ ∧ (ℑ‘𝑥) ∈ ℤ) |
12 | cc 7800 | . . 3 class ℂ | |
13 | 11, 2, 12 | crab 2459 | . 2 class {𝑥 ∈ ℂ ∣ ((ℜ‘𝑥) ∈ ℤ ∧ (ℑ‘𝑥) ∈ ℤ)} |
14 | 1, 13 | wceq 1353 | 1 wff ℤ[i] = {𝑥 ∈ ℂ ∣ ((ℜ‘𝑥) ∈ ℤ ∧ (ℑ‘𝑥) ∈ ℤ)} |
Colors of variables: wff set class |
This definition is referenced by: elgz 12352 |
Copyright terms: Public domain | W3C validator |