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 20547 | . 2 class ℤring | |
2 | ccnfld 20475 | . . 3 class ℂfld | |
3 | cz 11970 | . . 3 class ℤ | |
4 | cress 16474 | . . 3 class ↾s | |
5 | 2, 3, 4 | co 7145 | . 2 class (ℂfld ↾s ℤ) |
6 | 1, 5 | wceq 1528 | 1 wff ℤring = (ℂfld ↾s ℤ) |
Colors of variables: wff setvar class |
This definition is referenced by: zringcrng 20549 zringbas 20553 zringplusg 20554 zringmulg 20555 zringmulr 20556 zring0 20557 zring1 20558 zringlpirlem1 20561 zringunit 20565 zringcyg 20568 zringmpg 20569 prmirred 20572 zndvds 20626 zringnrg 23325 zlmclm 23645 zclmncvs 23681 lgseisenlem4 25882 zringnm 31101 zringsubgval 44347 |
Copyright terms: Public domain | W3C validator |