![]() |
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 21474 | . 2 class ℤring | |
2 | ccnfld 21381 | . . 3 class ℂfld | |
3 | cz 12610 | . . 3 class ℤ | |
4 | cress 17273 | . . 3 class ↾s | |
5 | 2, 3, 4 | co 7430 | . 2 class (ℂfld ↾s ℤ) |
6 | 1, 5 | wceq 1536 | 1 wff ℤring = (ℂfld ↾s ℤ) |
Colors of variables: wff setvar class |
This definition is referenced by: zringcrng 21476 zringbas 21481 zringplusg 21482 zringsub 21483 zringmulg 21484 zringmulr 21485 zring0 21486 zring1 21487 zringlpirlem1 21490 zringunit 21494 zringcyg 21497 zringsubgval 21498 zringmpg 21499 prmirred 21502 zndvds 21585 zringnrg 24823 zlmclm 25158 zclmncvs 25195 lgseisenlem4 27436 gsumzrsum 33044 zringnm 33918 |
Copyright terms: Public domain | W3C validator |