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

Definition df-zn 16740
 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 16736 . 2 ℤ/n
2 vn . . 3
3 cn0 10177 . . 3
4 vz . . . 4
5 ccnfld 16658 . . . . 5 fld
6 cz 10238 . . . . 5
7 cress 13425 . . . . 5 s
85, 6, 7co 6040 . . . 4 flds
9 vs . . . . 5
104cv 1648 . . . . . 6
112cv 1648 . . . . . . . . 9
1211csn 3774 . . . . . . . 8
13 crsp 16198 . . . . . . . . 9 RSpan
1410, 13cfv 5413 . . . . . . . 8 RSpan
1512, 14cfv 5413 . . . . . . 7 RSpan
16 cqg 14895 . . . . . . 7 ~QG
1710, 15, 16co 6040 . . . . . 6 ~QG RSpan
18 cqus 13686 . . . . . 6 s
1910, 17, 18co 6040 . . . . 5 s ~QG RSpan
209cv 1648 . . . . . 6
21 cnx 13421 . . . . . . . 8
22 cple 13491 . . . . . . . 8
2321, 22cfv 5413 . . . . . . 7
24 vf . . . . . . . 8
25 czrh 16733 . . . . . . . . . 10 RHom
2620, 25cfv 5413 . . . . . . . . 9 RHom
27 cc0 8946 . . . . . . . . . . 11
2811, 27wceq 1649 . . . . . . . . . 10
29 cfzo 11090 . . . . . . . . . . 11 ..^
3027, 11, 29co 6040 . . . . . . . . . 10 ..^
3128, 6, 30cif 3699 . . . . . . . . 9 ..^
3226, 31cres 4839 . . . . . . . 8 RHom ..^
3324cv 1648 . . . . . . . . . 10
34 cle 9077 . . . . . . . . . 10
3533, 34ccom 4841 . . . . . . . . 9
3633ccnv 4836 . . . . . . . . 9
3735, 36ccom 4841 . . . . . . . 8
3824, 32, 37csb 3211 . . . . . . 7 RHom ..^
3923, 38cop 3777 . . . . . 6 RHom ..^
40 csts 13422 . . . . . 6 sSet
4120, 39, 40co 6040 . . . . 5 sSet RHom ..^
429, 19, 41csb 3211 . . . 4 s ~QG RSpan sSet RHom ..^
434, 8, 42csb 3211 . . 3 flds s ~QG RSpan sSet RHom ..^
442, 3, 43cmpt 4226 . 2 flds s ~QG RSpan sSet RHom ..^
451, 44wceq 1649 1 ℤ/n flds s ~QG RSpan sSet RHom ..^
 Colors of variables: wff set class This definition is referenced by:  znval  16771
 Copyright terms: Public domain W3C validator