| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-zring | Structured version Visualization version GIF version | ||
| Description: The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.) |
| Ref | Expression |
|---|---|
| df-zring | ⊢ ℤring = (ℂfld ↾s ℤ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | czring 21457 | . 2 class ℤring | |
| 2 | ccnfld 21364 | . . 3 class ℂfld | |
| 3 | cz 12613 | . . 3 class ℤ | |
| 4 | cress 17274 | . . 3 class ↾s | |
| 5 | 2, 3, 4 | co 7431 | . 2 class (ℂfld ↾s ℤ) |
| 6 | 1, 5 | wceq 1540 | 1 wff ℤring = (ℂfld ↾s ℤ) |
| Colors of variables: wff setvar class |
| This definition is referenced by: zringcrng 21459 zringbas 21464 zringplusg 21465 zringsub 21466 zringmulg 21467 zringmulr 21468 zring0 21469 zring1 21470 zringlpirlem1 21473 zringunit 21477 zringcyg 21480 zringsubgval 21481 zringmpg 21482 prmirred 21485 zndvds 21568 zringnrg 24809 zlmclm 25145 zclmncvs 25182 lgseisenlem4 27422 gsumzrsum 33062 zringnm 33957 |
| Copyright terms: Public domain | W3C validator |