Step | Hyp | Ref
| Expression |
1 | | 2z 9335 |
. . . . . 6
 |
2 | 1 | a1i 9 |
. . . . 5
 
IDomn   |
3 | | nnz 9326 |
. . . . . 6
   |
4 | 3 | adantr 276 |
. . . . 5
 
IDomn   |
5 | | hash2 10870 |
. . . . . . 7
♯ 
 |
6 | | isidom 13750 |
. . . . . . . . . . . 12
 IDomn  Domn  |
7 | 6 | simprbi 275 |
. . . . . . . . . . 11
 IDomn Domn |
8 | | domnnzr 13744 |
. . . . . . . . . . 11
 Domn NzRing |
9 | 7, 8 | syl 14 |
. . . . . . . . . 10
 IDomn NzRing |
10 | | eqid 2193 |
. . . . . . . . . . . 12
         |
11 | 10 | isnzr2 13658 |
. . . . . . . . . . 11
 NzRing         |
12 | 11 | simprbi 275 |
. . . . . . . . . 10
 NzRing       |
13 | 9, 12 | syl 14 |
. . . . . . . . 9
 IDomn       |
14 | 13 | adantl 277 |
. . . . . . . 8
 
IDomn       |
15 | | 2onn 6565 |
. . . . . . . . . 10
 |
16 | | nnfi 6919 |
. . . . . . . . . 10
   |
17 | 15, 16 | ax-mp 5 |
. . . . . . . . 9
 |
18 | | zntos.y |
. . . . . . . . . . 11
ℤ/nℤ   |
19 | 18, 10 | znfi 14114 |
. . . . . . . . . 10
       |
20 | 19 | adantr 276 |
. . . . . . . . 9
 
IDomn       |
21 | | fihashdom 10861 |
. . . . . . . . 9
        ♯  ♯     
       |
22 | 17, 20, 21 | sylancr 414 |
. . . . . . . 8
 
IDomn  ♯  ♯     
       |
23 | 14, 22 | mpbird 167 |
. . . . . . 7
 
IDomn ♯  ♯        |
24 | 5, 23 | eqbrtrrid 4065 |
. . . . . 6
 
IDomn ♯        |
25 | 18, 10 | znhash 14115 |
. . . . . . 7
 ♯        |
26 | 25 | adantr 276 |
. . . . . 6
 
IDomn ♯        |
27 | 24, 26 | breqtrd 4055 |
. . . . 5
 
IDomn   |
28 | | eluz2 9588 |
. . . . 5
         |
29 | 2, 4, 27, 28 | syl3anbrc 1183 |
. . . 4
 
IDomn       |
30 | | nncn 8980 |
. . . . . . . . . . . 12
   |
31 | 30 | ad2antrr 488 |
. . . . . . . . . . 11
   IDomn 
 
  |
32 | | nncn 8980 |
. . . . . . . . . . . 12
   |
33 | 32 | ad2antrl 490 |
. . . . . . . . . . 11
   IDomn 
 
  |
34 | | nnap0 9001 |
. . . . . . . . . . . 12
 #   |
35 | 34 | ad2antrl 490 |
. . . . . . . . . . 11
   IDomn 
 
#   |
36 | 31, 33, 35 | divcanap1d 8800 |
. . . . . . . . . 10
   IDomn 
 
      |
37 | 36 | fveq2d 5550 |
. . . . . . . . 9
   IDomn 
 
  RHom           RHom       |
38 | 7 | ad2antlr 489 |
. . . . . . . . . . . 12
   IDomn 
 
Domn |
39 | | domnring 13745 |
. . . . . . . . . . . 12
 Domn   |
40 | 38, 39 | syl 14 |
. . . . . . . . . . 11
   IDomn 
 
  |
41 | | eqid 2193 |
. . . . . . . . . . . 12
 RHom   RHom   |
42 | 41 | zrhrhm 14082 |
. . . . . . . . . . 11

 RHom  ℤring RingHom    |
43 | 40, 42 | syl 14 |
. . . . . . . . . 10
   IDomn 
 
 RHom  ℤring RingHom    |
44 | | simprr 531 |
. . . . . . . . . . 11
   IDomn 
 
  |
45 | | nnz 9326 |
. . . . . . . . . . . . 13
   |
46 | 45 | ad2antrl 490 |
. . . . . . . . . . . 12
   IDomn 
 
  |
47 | | nnne0 9000 |
. . . . . . . . . . . . 13
   |
48 | 47 | ad2antrl 490 |
. . . . . . . . . . . 12
   IDomn 
 
  |
49 | 3 | ad2antrr 488 |
. . . . . . . . . . . 12
   IDomn 
 
  |
50 | | dvdsval2 11920 |
. . . . . . . . . . . 12
   
     |
51 | 46, 48, 49, 50 | syl3anc 1249 |
. . . . . . . . . . 11
   IDomn 
 
      |
52 | 44, 51 | mpbid 147 |
. . . . . . . . . 10
   IDomn 
 
    |
53 | | zringbas 14056 |
. . . . . . . . . . 11
  ℤring |
54 | | zringmulr 14059 |
. . . . . . . . . . 11
  ℤring |
55 | | eqid 2193 |
. . . . . . . . . . 11
         |
56 | 53, 54, 55 | rhmmul 13638 |
. . . . . . . . . 10
   RHom  ℤring
RingHom  

   RHom            RHom               RHom        |
57 | 43, 52, 46, 56 | syl3anc 1249 |
. . . . . . . . 9
   IDomn 
 
  RHom            RHom               RHom        |
58 | | iddvds 11934 |
. . . . . . . . . . 11
   |
59 | 49, 58 | syl 14 |
. . . . . . . . . 10
   IDomn 
 
  |
60 | | nnnn0 9237 |
. . . . . . . . . . . 12
   |
61 | 60 | ad2antrr 488 |
. . . . . . . . . . 11
   IDomn 
 
  |
62 | | eqid 2193 |
. . . . . . . . . . . 12
         |
63 | 18, 41, 62 | zndvds0 14109 |
. . . . . . . . . . 11
 
    RHom        
   |
64 | 61, 49, 63 | syl2anc 411 |
. . . . . . . . . 10
   IDomn 
 
   RHom        
   |
65 | 59, 64 | mpbird 167 |
. . . . . . . . 9
   IDomn 
 
  RHom           |
66 | 37, 57, 65 | 3eqtr3d 2234 |
. . . . . . . 8
   IDomn 
 
   RHom               RHom            |
67 | 53, 10 | rhmf 13637 |
. . . . . . . . . . 11
  RHom  ℤring RingHom   RHom            |
68 | 43, 67 | syl 14 |
. . . . . . . . . 10
   IDomn 
 
 RHom            |
69 | 68, 52 | ffvelcdmd 5686 |
. . . . . . . . 9
   IDomn 
 
  RHom    
        |
70 | 68, 46 | ffvelcdmd 5686 |
. . . . . . . . 9
   IDomn 
 
  RHom           |
71 | 10, 55, 62 | domneq0 13746 |
. . . . . . . . 9
  Domn   RHom          
  RHom         
    RHom               RHom             RHom             RHom             |
72 | 38, 69, 70, 71 | syl3anc 1249 |
. . . . . . . 8
   IDomn 
 
    RHom               RHom             RHom             RHom             |
73 | 66, 72 | mpbid 147 |
. . . . . . 7
   IDomn 
 
   RHom             RHom            |
74 | 18, 41, 62 | zndvds0 14109 |
. . . . . . . . . 10
  
     RHom          
     |
75 | 61, 52, 74 | syl2anc 411 |
. . . . . . . . 9
   IDomn 
 
   RHom          
     |
76 | | nnre 8979 |
. . . . . . . . . . . . . 14
   |
77 | 76 | ad2antrr 488 |
. . . . . . . . . . . . 13
   IDomn 
 
  |
78 | | nnre 8979 |
. . . . . . . . . . . . . 14
   |
79 | 78 | ad2antrl 490 |
. . . . . . . . . . . . 13
   IDomn 
 
  |
80 | | nngt0 8997 |
. . . . . . . . . . . . . 14
   |
81 | 80 | ad2antrr 488 |
. . . . . . . . . . . . 13
   IDomn 
 
  |
82 | | nngt0 8997 |
. . . . . . . . . . . . . 14
   |
83 | 82 | ad2antrl 490 |
. . . . . . . . . . . . 13
   IDomn 
 
  |
84 | 77, 79, 81, 83 | divgt0d 8944 |
. . . . . . . . . . . 12
   IDomn 
 
    |
85 | | elnnz 9317 |
. . . . . . . . . . . 12
  
        |
86 | 52, 84, 85 | sylanbrc 417 |
. . . . . . . . . . 11
   IDomn 
 
    |
87 | | dvdsle 11973 |
. . . . . . . . . . 11
  
   

     |
88 | 49, 86, 87 | syl2anc 411 |
. . . . . . . . . 10
   IDomn 
 
  
     |
89 | | 1red 8024 |
. . . . . . . . . . . 12
   IDomn 
 
  |
90 | | 0lt1 8136 |
. . . . . . . . . . . . 13
 |
91 | 90 | a1i 9 |
. . . . . . . . . . . 12
   IDomn 
 
  |
92 | | lediv2 8900 |
. . . . . . . . . . . 12
      
          |
93 | 79, 83, 89, 91, 77, 81, 92 | syl222anc 1265 |
. . . . . . . . . . 11
   IDomn 
 
        |
94 | | nnle1eq1 8996 |
. . . . . . . . . . . 12
 
   |
95 | 94 | ad2antrl 490 |
. . . . . . . . . . 11
   IDomn 
 

   |
96 | 31 | div1d 8789 |
. . . . . . . . . . . 12
   IDomn 
 
    |
97 | 96 | breq1d 4039 |
. . . . . . . . . . 11
   IDomn 
 
    
     |
98 | 93, 95, 97 | 3bitr3rd 219 |
. . . . . . . . . 10
   IDomn 
 
  
   |
99 | 88, 98 | sylibd 149 |
. . . . . . . . 9
   IDomn 
 
  
   |
100 | 75, 99 | sylbid 150 |
. . . . . . . 8
   IDomn 
 
   RHom          
   |
101 | 18, 41, 62 | zndvds0 14109 |
. . . . . . . . . 10
 
    RHom        
   |
102 | 61, 46, 101 | syl2anc 411 |
. . . . . . . . 9
   IDomn 
 
   RHom        
   |
103 | | nnnn0 9237 |
. . . . . . . . . . 11
   |
104 | 103 | ad2antrl 490 |
. . . . . . . . . 10
   IDomn 
 
  |
105 | | dvdseq 11977 |
. . . . . . . . . . 11
    
 
  |
106 | 105 | expr 375 |
. . . . . . . . . 10
   
     |
107 | 104, 61, 44, 106 | syl21anc 1248 |
. . . . . . . . 9
   IDomn 
 

   |
108 | 102, 107 | sylbid 150 |
. . . . . . . 8
   IDomn 
 
   RHom            |
109 | 100, 108 | orim12d 787 |
. . . . . . 7
   IDomn 
 
    RHom             RHom               |
110 | 73, 109 | mpd 13 |
. . . . . 6
   IDomn 
 
    |
111 | 110 | expr 375 |
. . . . 5
   IDomn
       |
112 | 111 | ralrimiva 2567 |
. . . 4
 
IDomn  
     |
113 | | isprm2 12242 |
. . . 4

      
      |
114 | 29, 112, 113 | sylanbrc 417 |
. . 3
 
IDomn   |
115 | 114 | ex 115 |
. 2
 
IDomn    |
116 | 18 | znidom 14116 |
. 2

IDomn |
117 | 115, 116 | impbid1 142 |
1
 
IDomn
   |