Description: _i is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | igz | |- _i e. Z[i] |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-icn | |- _i e. CC |
|
| 2 | rei | |- ( Re ` _i ) = 0 |
|
| 3 | 0z | |- 0 e. ZZ |
|
| 4 | 2 3 | eqeltri | |- ( Re ` _i ) e. ZZ |
| 5 | imi | |- ( Im ` _i ) = 1 |
|
| 6 | 1z | |- 1 e. ZZ |
|
| 7 | 5 6 | eqeltri | |- ( Im ` _i ) e. ZZ |
| 8 | elgz | |- ( _i e. Z[i] <-> ( _i e. CC /\ ( Re ` _i ) e. ZZ /\ ( Im ` _i ) e. ZZ ) ) |
|
| 9 | 1 4 7 8 | mpbir3an | |- _i e. Z[i] |