Step | Hyp | Ref
| Expression |
1 | | nnnn0 9237 |
. . . . . . 7
   |
2 | | znchr.y |
. . . . . . . 8
ℤ/nℤ   |
3 | | eqid 2193 |
. . . . . . . 8
         |
4 | | eqid 2193 |
. . . . . . . 8
 RHom   RHom   |
5 | 2, 3, 4 | znzrhfo 14113 |
. . . . . . 7

 RHom            |
6 | 1, 5 | syl 14 |
. . . . . 6
  RHom            |
7 | | znrrg.e |
. . . . . . . 8
RLReg   |
8 | 7, 3 | rrgss 13746 |
. . . . . . 7
     |
9 | 8 | sseli 3175 |
. . . . . 6
       |
10 | | foelrn 5787 |
. . . . . 6
   RHom         
     
  RHom       |
11 | 6, 9, 10 | syl2an 289 |
. . . . 5
 
 
  RHom       |
12 | 11 | ex 115 |
. . . 4
  
  RHom        |
13 | | nncn 8980 |
. . . . . . . . . . . . . . . 16
   |
14 | 13 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
      RHom        |
15 | | simplr 528 |
. . . . . . . . . . . . . . . . 17
      RHom        |
16 | | nnz 9326 |
. . . . . . . . . . . . . . . . . 18
   |
17 | 16 | ad2antrr 488 |
. . . . . . . . . . . . . . . . 17
      RHom        |
18 | | nnne0 9000 |
. . . . . . . . . . . . . . . . . . 19
   |
19 | 18 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
      RHom        |
20 | | simpr 110 |
. . . . . . . . . . . . . . . . . . 19
     |
21 | 20 | necon3ai 2413 |
. . . . . . . . . . . . . . . . . 18
 
   |
22 | 19, 21 | syl 14 |
. . . . . . . . . . . . . . . . 17
      RHom     
    |
23 | | gcdn0cl 12089 |
. . . . . . . . . . . . . . . . 17
           |
24 | 15, 17, 22, 23 | syl21anc 1248 |
. . . . . . . . . . . . . . . 16
      RHom          |
25 | 24 | nncnd 8986 |
. . . . . . . . . . . . . . 15
      RHom          |
26 | 24 | nnap0d 9018 |
. . . . . . . . . . . . . . 15
      RHom        #   |
27 | 14, 25, 26 | divcanap2d 8801 |
. . . . . . . . . . . . . 14
      RHom          
     |
28 | | gcddvds 12090 |
. . . . . . . . . . . . . . . . 17
 
    
    |
29 | 15, 17, 28 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
      RHom              |
30 | 29 | simpld 112 |
. . . . . . . . . . . . . . 15
      RHom          |
31 | 24 | nnzd 9428 |
. . . . . . . . . . . . . . . 16
      RHom          |
32 | 29 | simprd 114 |
. . . . . . . . . . . . . . . . . 18
      RHom          |
33 | | simpll 527 |
. . . . . . . . . . . . . . . . . . 19
      RHom        |
34 | | nndivdvds 11929 |
. . . . . . . . . . . . . . . . . . 19
  
    
       |
35 | 33, 24, 34 | syl2anc 411 |
. . . . . . . . . . . . . . . . . 18
      RHom          
     |
36 | 32, 35 | mpbid 147 |
. . . . . . . . . . . . . . . . 17
      RHom            |
37 | 36 | nnzd 9428 |
. . . . . . . . . . . . . . . 16
      RHom            |
38 | | dvdsmulc 11952 |
. . . . . . . . . . . . . . . 16
   
            
            |
39 | 31, 15, 37, 38 | syl3anc 1249 |
. . . . . . . . . . . . . . 15
      RHom             
            |
40 | 30, 39 | mpd 13 |
. . . . . . . . . . . . . 14
      RHom          
           |
41 | 27, 40 | eqbrtrrd 4053 |
. . . . . . . . . . . . 13
      RHom              |
42 | | simpr 110 |
. . . . . . . . . . . . . . 15
      RHom        RHom       |
43 | 1 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
      RHom        |
44 | 43, 5 | syl 14 |
. . . . . . . . . . . . . . . . 17
      RHom       RHom            |
45 | | fof 5468 |
. . . . . . . . . . . . . . . . 17
  RHom         
 RHom            |
46 | 44, 45 | syl 14 |
. . . . . . . . . . . . . . . 16
      RHom       RHom            |
47 | 46, 37 | ffvelcdmd 5686 |
. . . . . . . . . . . . . . 15
      RHom        RHom               |
48 | | eqid 2193 |
. . . . . . . . . . . . . . . 16
         |
49 | | eqid 2193 |
. . . . . . . . . . . . . . . 16
         |
50 | 7, 3, 48, 49 | rrgeq0i 13744 |
. . . . . . . . . . . . . . 15
    RHom       RHom                  RHom             RHom     
       
  RHom    

          |
51 | 42, 47, 50 | syl2anc 411 |
. . . . . . . . . . . . . 14
      RHom          RHom             RHom                RHom                |
52 | 2 | zncrng 14110 |
. . . . . . . . . . . . . . . . . . . . 21

  |
53 | 1, 52 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
   |
54 | 53 | crngringd 13489 |
. . . . . . . . . . . . . . . . . . 19
   |
55 | 54 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
      RHom        |
56 | 4 | zrhrhm 14088 |
. . . . . . . . . . . . . . . . . 18

 RHom  ℤring RingHom    |
57 | 55, 56 | syl 14 |
. . . . . . . . . . . . . . . . 17
      RHom       RHom  ℤring RingHom    |
58 | | zringbas 14062 |
. . . . . . . . . . . . . . . . . 18
  ℤring |
59 | | zringmulr 14065 |
. . . . . . . . . . . . . . . . . 18
  ℤring |
60 | 58, 59, 48 | rhmmul 13644 |
. . . . . . . . . . . . . . . . 17
   RHom  ℤring
RingHom 
       RHom              RHom             RHom            |
61 | 57, 15, 37, 60 | syl3anc 1249 |
. . . . . . . . . . . . . . . 16
      RHom        RHom              RHom             RHom            |
62 | 61 | eqeq1d 2202 |
. . . . . . . . . . . . . . 15
      RHom         RHom              
   RHom             RHom                 |
63 | 15, 37 | zmulcld 9435 |
. . . . . . . . . . . . . . . 16
      RHom        
     |
64 | 2, 4, 49 | zndvds0 14115 |
. . . . . . . . . . . . . . . 16
  
         RHom              
         |
65 | 43, 63, 64 | syl2anc 411 |
. . . . . . . . . . . . . . 15
      RHom         RHom              
         |
66 | 62, 65 | bitr3d 190 |
. . . . . . . . . . . . . 14
      RHom          RHom             RHom             
         |
67 | 2, 4, 49 | zndvds0 14115 |
. . . . . . . . . . . . . . 15
  

      RHom     
      
       |
68 | 43, 37, 67 | syl2anc 411 |
. . . . . . . . . . . . . 14
      RHom         RHom     
      
       |
69 | 51, 66, 68 | 3imtr3d 202 |
. . . . . . . . . . . . 13
      RHom       
            |
70 | 41, 69 | mpd 13 |
. . . . . . . . . . . 12
      RHom            |
71 | 14, 25, 26 | divcanap1d 8800 |
. . . . . . . . . . . 12
      RHom           
    |
72 | 36 | nncnd 8986 |
. . . . . . . . . . . . 13
      RHom            |
73 | 72 | mulridd 8026 |
. . . . . . . . . . . 12
      RHom                  |
74 | 70, 71, 73 | 3brtr4d 4061 |
. . . . . . . . . . 11
      RHom           
 
        |
75 | | 1zzd 9334 |
. . . . . . . . . . . 12
      RHom        |
76 | 36 | nnne0d 9017 |
. . . . . . . . . . . 12
      RHom            |
77 | | dvdscmulr 11953 |
. . . . . . . . . . . 12
   
  
  

   
   
                |
78 | 31, 75, 37, 76, 77 | syl112anc 1253 |
. . . . . . . . . . 11
      RHom                 
    
   |
79 | 74, 78 | mpbid 147 |
. . . . . . . . . 10
      RHom          |
80 | 15, 17 | gcdcld 12095 |
. . . . . . . . . . 11
      RHom          |
81 | | dvds1 11985 |
. . . . . . . . . . 11
  
  
     |
82 | 80, 81 | syl 14 |
. . . . . . . . . 10
      RHom              |
83 | 79, 82 | mpbid 147 |
. . . . . . . . 9
      RHom          |
84 | | znunit.u |
. . . . . . . . . . 11
Unit   |
85 | 2, 84, 4 | znunit 14124 |
. . . . . . . . . 10
 
    RHom    
     |
86 | 43, 15, 85 | syl2anc 411 |
. . . . . . . . 9
      RHom         RHom          |
87 | 83, 86 | mpbird 167 |
. . . . . . . 8
      RHom        RHom       |
88 | 87 | ex 115 |
. . . . . . 7
 
    RHom       RHom        |
89 | | eleq1 2256 |
. . . . . . . 8
   RHom    

  RHom        |
90 | | eleq1 2256 |
. . . . . . . 8
   RHom    

  RHom        |
91 | 89, 90 | imbi12d 234 |
. . . . . . 7
   RHom    
 
    RHom       RHom         |
92 | 88, 91 | syl5ibrcom 157 |
. . . . . 6
 
    RHom          |
93 | 92 | rexlimdva 2611 |
. . . . 5
  
  RHom     
    |
94 | 93 | com23 78 |
. . . 4
      RHom         |
95 | 12, 94 | mpdd 41 |
. . 3
 
   |
96 | 95 | ssrdv 3185 |
. 2
   |
97 | 7, 84 | unitrrg 13747 |
. . 3

  |
98 | 54, 97 | syl 14 |
. 2
   |
99 | 96, 98 | eqssd 3196 |
1
   |