Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-gz | Structured version Visualization version Unicode version |
Description: Define the set of gaussian integers, which are complex numbers whose real and imaginary parts are integers. (Note that the is actually part of the symbol token and has no independent meaning.) (Contributed by Mario Carneiro, 14-Jul-2014.) |
Ref | Expression |
---|---|
df-gz |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cgz 15633 | . 2 | |
2 | vx | . . . . . . 7 | |
3 | 2 | cv 1482 | . . . . . 6 |
4 | cre 13837 | . . . . . 6 | |
5 | 3, 4 | cfv 5888 | . . . . 5 |
6 | cz 11377 | . . . . 5 | |
7 | 5, 6 | wcel 1990 | . . . 4 |
8 | cim 13838 | . . . . . 6 | |
9 | 3, 8 | cfv 5888 | . . . . 5 |
10 | 9, 6 | wcel 1990 | . . . 4 |
11 | 7, 10 | wa 384 | . . 3 |
12 | cc 9934 | . . 3 | |
13 | 11, 2, 12 | crab 2916 | . 2 |
14 | 1, 13 | wceq 1483 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: elgz 15635 |
Copyright terms: Public domain | W3C validator |