Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-zn Structured version   Unicode version

Definition df-zn 16785
 Description: Define the ring of integers . This is literally the quotient ring of by the ideal , but we augment it with a total order. (Contributed by Mario Carneiro, 14-Jun-2015.)
Assertion
Ref Expression
df-zn ℤ/n flds s ~QG RSpan sSet RHom ..^
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-zn
StepHypRef Expression
1 czn 16781 . 2 ℤ/n
2 vn . . 3
3 cn0 10221 . . 3
4 vz . . . 4
5 ccnfld 16703 . . . . 5 fld
6 cz 10282 . . . . 5
7 cress 13470 . . . . 5 s
85, 6, 7co 6081 . . . 4 flds
9 vs . . . . 5
104cv 1651 . . . . . 6
112cv 1651 . . . . . . . . 9
1211csn 3814 . . . . . . . 8
13 crsp 16243 . . . . . . . . 9 RSpan
1410, 13cfv 5454 . . . . . . . 8 RSpan
1512, 14cfv 5454 . . . . . . 7 RSpan
16 cqg 14940 . . . . . . 7 ~QG
1710, 15, 16co 6081 . . . . . 6 ~QG RSpan
18 cqus 13731 . . . . . 6 s
1910, 17, 18co 6081 . . . . 5 s ~QG RSpan
209cv 1651 . . . . . 6
21 cnx 13466 . . . . . . . 8
22 cple 13536 . . . . . . . 8
2321, 22cfv 5454 . . . . . . 7
24 vf . . . . . . . 8
25 czrh 16778 . . . . . . . . . 10 RHom
2620, 25cfv 5454 . . . . . . . . 9 RHom
27 cc0 8990 . . . . . . . . . . 11
2811, 27wceq 1652 . . . . . . . . . 10
29 cfzo 11135 . . . . . . . . . . 11 ..^
3027, 11, 29co 6081 . . . . . . . . . 10 ..^
3128, 6, 30cif 3739 . . . . . . . . 9 ..^
3226, 31cres 4880 . . . . . . . 8 RHom ..^
3324cv 1651 . . . . . . . . . 10
34 cle 9121 . . . . . . . . . 10
3533, 34ccom 4882 . . . . . . . . 9
3633ccnv 4877 . . . . . . . . 9
3735, 36ccom 4882 . . . . . . . 8
3824, 32, 37csb 3251 . . . . . . 7 RHom ..^
3923, 38cop 3817 . . . . . 6 RHom ..^
40 csts 13467 . . . . . 6 sSet
4120, 39, 40co 6081 . . . . 5 sSet RHom ..^
429, 19, 41csb 3251 . . . 4 s ~QG RSpan sSet RHom ..^
434, 8, 42csb 3251 . . 3 flds s ~QG RSpan sSet RHom ..^
442, 3, 43cmpt 4266 . 2 flds s ~QG RSpan sSet RHom ..^
451, 44wceq 1652 1 ℤ/n flds s ~QG RSpan sSet RHom ..^
 Colors of variables: wff set class This definition is referenced by:  znval  16816
 Copyright terms: Public domain W3C validator