![]() |
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 | zring 20334 | . 2 class ℤring | |
2 | ccnfld 20262 | . . 3 class ℂfld | |
3 | cz 11799 | . . 3 class ℤ | |
4 | cress 16346 | . . 3 class ↾s | |
5 | 2, 3, 4 | co 6982 | . 2 class (ℂfld ↾s ℤ) |
6 | 1, 5 | wceq 1508 | 1 wff ℤring = (ℂfld ↾s ℤ) |
Colors of variables: wff setvar class |
This definition is referenced by: zringcrng 20336 zringbas 20340 zringplusg 20341 zringmulg 20342 zringmulr 20343 zring0 20344 zring1 20345 zringlpirlem1 20348 zringunit 20352 zringcyg 20355 zringmpg 20356 prmirred 20359 zndvds 20413 zringnrg 23114 zlmclm 23434 zclmncvs 23470 lgseisenlem4 25671 zringnm 30877 zringsubgval 43851 |
Copyright terms: Public domain | W3C validator |