Step | Hyp | Ref
| Expression |
1 | | 2z 11409 |
. . . . . 6
|
2 | 1 | a1i 11 |
. . . . 5
IDomn |
3 | | nnz 11399 |
. . . . . 6
|
4 | 3 | adantr 481 |
. . . . 5
IDomn |
5 | | hash2 13193 |
. . . . . . 7
|
6 | | isidom 19304 |
. . . . . . . . . . . 12
IDomn Domn |
7 | 6 | simprbi 480 |
. . . . . . . . . . 11
IDomn Domn |
8 | | domnnzr 19295 |
. . . . . . . . . . 11
Domn NzRing |
9 | 7, 8 | syl 17 |
. . . . . . . . . 10
IDomn NzRing |
10 | | eqid 2622 |
. . . . . . . . . . . 12
|
11 | 10 | isnzr2 19263 |
. . . . . . . . . . 11
NzRing |
12 | 11 | simprbi 480 |
. . . . . . . . . 10
NzRing |
13 | 9, 12 | syl 17 |
. . . . . . . . 9
IDomn |
14 | 13 | adantl 482 |
. . . . . . . 8
IDomn |
15 | | df2o2 7574 |
. . . . . . . . . 10
|
16 | | prfi 8235 |
. . . . . . . . . 10
|
17 | 15, 16 | eqeltri 2697 |
. . . . . . . . 9
|
18 | | fvex 6201 |
. . . . . . . . 9
|
19 | | hashdom 13168 |
. . . . . . . . 9
|
20 | 17, 18, 19 | mp2an 708 |
. . . . . . . 8
|
21 | 14, 20 | sylibr 224 |
. . . . . . 7
IDomn |
22 | 5, 21 | syl5eqbrr 4689 |
. . . . . 6
IDomn |
23 | | zntos.y |
. . . . . . . 8
ℤ/nℤ |
24 | 23, 10 | znhash 19907 |
. . . . . . 7
|
25 | 24 | adantr 481 |
. . . . . 6
IDomn |
26 | 22, 25 | breqtrd 4679 |
. . . . 5
IDomn |
27 | | eluz2 11693 |
. . . . 5
|
28 | 2, 4, 26, 27 | syl3anbrc 1246 |
. . . 4
IDomn |
29 | | nncn 11028 |
. . . . . . . . . . . 12
|
30 | 29 | ad2antrr 762 |
. . . . . . . . . . 11
IDomn
|
31 | | nncn 11028 |
. . . . . . . . . . . 12
|
32 | 31 | ad2antrl 764 |
. . . . . . . . . . 11
IDomn
|
33 | | nnne0 11053 |
. . . . . . . . . . . 12
|
34 | 33 | ad2antrl 764 |
. . . . . . . . . . 11
IDomn
|
35 | 30, 32, 34 | divcan1d 10802 |
. . . . . . . . . 10
IDomn
|
36 | 35 | fveq2d 6195 |
. . . . . . . . 9
IDomn
RHom RHom |
37 | 7 | ad2antlr 763 |
. . . . . . . . . . . 12
IDomn
Domn |
38 | | domnring 19296 |
. . . . . . . . . . . 12
Domn |
39 | 37, 38 | syl 17 |
. . . . . . . . . . 11
IDomn
|
40 | | eqid 2622 |
. . . . . . . . . . . 12
RHom RHom |
41 | 40 | zrhrhm 19860 |
. . . . . . . . . . 11
RHom ℤring RingHom |
42 | 39, 41 | syl 17 |
. . . . . . . . . 10
IDomn
RHom ℤring RingHom |
43 | | simprr 796 |
. . . . . . . . . . 11
IDomn
|
44 | | nnz 11399 |
. . . . . . . . . . . . 13
|
45 | 44 | ad2antrl 764 |
. . . . . . . . . . . 12
IDomn
|
46 | 3 | ad2antrr 762 |
. . . . . . . . . . . 12
IDomn
|
47 | | dvdsval2 14986 |
. . . . . . . . . . . 12
|
48 | 45, 34, 46, 47 | syl3anc 1326 |
. . . . . . . . . . 11
IDomn
|
49 | 43, 48 | mpbid 222 |
. . . . . . . . . 10
IDomn
|
50 | | zringbas 19824 |
. . . . . . . . . . 11
ℤring |
51 | | zringmulr 19827 |
. . . . . . . . . . 11
ℤring |
52 | | eqid 2622 |
. . . . . . . . . . 11
|
53 | 50, 51, 52 | rhmmul 18727 |
. . . . . . . . . 10
RHom ℤring
RingHom
RHom RHom RHom |
54 | 42, 49, 45, 53 | syl3anc 1326 |
. . . . . . . . 9
IDomn
RHom RHom RHom |
55 | | iddvds 14995 |
. . . . . . . . . . 11
|
56 | 46, 55 | syl 17 |
. . . . . . . . . 10
IDomn
|
57 | | nnnn0 11299 |
. . . . . . . . . . . 12
|
58 | 57 | ad2antrr 762 |
. . . . . . . . . . 11
IDomn
|
59 | | eqid 2622 |
. . . . . . . . . . . 12
|
60 | 23, 40, 59 | zndvds0 19899 |
. . . . . . . . . . 11
RHom
|
61 | 58, 46, 60 | syl2anc 693 |
. . . . . . . . . 10
IDomn
RHom
|
62 | 56, 61 | mpbird 247 |
. . . . . . . . 9
IDomn
RHom |
63 | 36, 54, 62 | 3eqtr3d 2664 |
. . . . . . . 8
IDomn
RHom RHom |
64 | 50, 10 | rhmf 18726 |
. . . . . . . . . . 11
RHom ℤring RingHom RHom |
65 | 42, 64 | syl 17 |
. . . . . . . . . 10
IDomn
RHom |
66 | 65, 49 | ffvelrnd 6360 |
. . . . . . . . 9
IDomn
RHom
|
67 | 65, 45 | ffvelrnd 6360 |
. . . . . . . . 9
IDomn
RHom |
68 | 10, 52, 59 | domneq0 19297 |
. . . . . . . . 9
Domn RHom
RHom
RHom RHom RHom RHom |
69 | 37, 66, 67, 68 | syl3anc 1326 |
. . . . . . . 8
IDomn
RHom RHom RHom RHom |
70 | 63, 69 | mpbid 222 |
. . . . . . 7
IDomn
RHom RHom |
71 | 23, 40, 59 | zndvds0 19899 |
. . . . . . . . . 10
RHom
|
72 | 58, 49, 71 | syl2anc 693 |
. . . . . . . . 9
IDomn
RHom
|
73 | | nnre 11027 |
. . . . . . . . . . . . . 14
|
74 | 73 | ad2antrr 762 |
. . . . . . . . . . . . 13
IDomn
|
75 | | nnre 11027 |
. . . . . . . . . . . . . 14
|
76 | 75 | ad2antrl 764 |
. . . . . . . . . . . . 13
IDomn
|
77 | | nngt0 11049 |
. . . . . . . . . . . . . 14
|
78 | 77 | ad2antrr 762 |
. . . . . . . . . . . . 13
IDomn
|
79 | | nngt0 11049 |
. . . . . . . . . . . . . 14
|
80 | 79 | ad2antrl 764 |
. . . . . . . . . . . . 13
IDomn
|
81 | 74, 76, 78, 80 | divgt0d 10959 |
. . . . . . . . . . . 12
IDomn
|
82 | | elnnz 11387 |
. . . . . . . . . . . 12
|
83 | 49, 81, 82 | sylanbrc 698 |
. . . . . . . . . . 11
IDomn
|
84 | | dvdsle 15032 |
. . . . . . . . . . 11
|
85 | 46, 83, 84 | syl2anc 693 |
. . . . . . . . . 10
IDomn
|
86 | | 1red 10055 |
. . . . . . . . . . . 12
IDomn
|
87 | | 0lt1 10550 |
. . . . . . . . . . . . 13
|
88 | 87 | a1i 11 |
. . . . . . . . . . . 12
IDomn
|
89 | | lediv2 10913 |
. . . . . . . . . . . 12
|
90 | 76, 80, 86, 88, 74, 78, 89 | syl222anc 1342 |
. . . . . . . . . . 11
IDomn
|
91 | | nnle1eq1 11048 |
. . . . . . . . . . . 12
|
92 | 91 | ad2antrl 764 |
. . . . . . . . . . 11
IDomn
|
93 | 30 | div1d 10793 |
. . . . . . . . . . . 12
IDomn
|
94 | 93 | breq1d 4663 |
. . . . . . . . . . 11
IDomn
|
95 | 90, 92, 94 | 3bitr3rd 299 |
. . . . . . . . . 10
IDomn
|
96 | 85, 95 | sylibd 229 |
. . . . . . . . 9
IDomn
|
97 | 72, 96 | sylbid 230 |
. . . . . . . 8
IDomn
RHom
|
98 | 23, 40, 59 | zndvds0 19899 |
. . . . . . . . . 10
RHom
|
99 | 58, 45, 98 | syl2anc 693 |
. . . . . . . . 9
IDomn
RHom
|
100 | | nnnn0 11299 |
. . . . . . . . . . 11
|
101 | 100 | ad2antrl 764 |
. . . . . . . . . 10
IDomn
|
102 | | dvdseq 15036 |
. . . . . . . . . . 11
|
103 | 102 | expr 643 |
. . . . . . . . . 10
|
104 | 101, 58, 43, 103 | syl21anc 1325 |
. . . . . . . . 9
IDomn
|
105 | 99, 104 | sylbid 230 |
. . . . . . . 8
IDomn
RHom |
106 | 97, 105 | orim12d 883 |
. . . . . . 7
IDomn
RHom RHom |
107 | 70, 106 | mpd 15 |
. . . . . 6
IDomn
|
108 | 107 | expr 643 |
. . . . 5
IDomn
|
109 | 108 | ralrimiva 2966 |
. . . 4
IDomn
|
110 | | isprm2 15395 |
. . . 4
|
111 | 28, 109, 110 | sylanbrc 698 |
. . 3
IDomn |
112 | 111 | ex 450 |
. 2
IDomn |
113 | 23 | znfld 19909 |
. . 3
Field |
114 | | fldidom 19305 |
. . 3
Field IDomn |
115 | 113, 114 | syl 17 |
. 2
IDomn |
116 | 112, 115 | impbid1 215 |
1
IDomn
|