Step | Hyp | Ref
| Expression |
1 | | oveq2 5918 |
. . . . . . . . 9
       |
2 | 1 | fveq2d 5550 |
. . . . . . . 8
               |
3 | 2 | cbvmptv 4125 |
. . . . . . 7
                                 |
4 | 3 | oveq2i 5921 |
. . . . . 6
 g                   g                   |
5 | | eqid 2193 |
. . . . . . 7
         |
6 | | eqid 2193 |
. . . . . . 7
         |
7 | | lgseisen.1 |
. . . . . . . . . . 11
       |
8 | 7 | eldifad 3164 |
. . . . . . . . . 10
   |
9 | | lgseisen.7 |
. . . . . . . . . . 11
ℤ/nℤ   |
10 | 9 | znidom 14122 |
. . . . . . . . . 10

IDomn |
11 | 8, 10 | syl 14 |
. . . . . . . . 9
 IDomn |
12 | 11 | idomcringd 13758 |
. . . . . . . 8
   |
13 | | lgseisen.8 |
. . . . . . . . 9
mulGrp   |
14 | 13 | crngmgp 13484 |
. . . . . . . 8

CMnd |
15 | 12, 14 | syl 14 |
. . . . . . 7
 CMnd |
16 | | 1zzd 9334 |
. . . . . . 7
   |
17 | | oddn2prm 12389 |
. . . . . . . . 9
    
  |
18 | 7, 17 | syl 14 |
. . . . . . . 8
   |
19 | | prmz 12239 |
. . . . . . . . 9

  |
20 | | oddm1d2 12023 |
. . . . . . . . 9
 
 
     |
21 | 8, 19, 20 | 3syl 17 |
. . . . . . . 8
         |
22 | 18, 21 | mpbid 147 |
. . . . . . 7
       |
23 | 11 | idomringd 13759 |
. . . . . . . . . . 11
   |
24 | | lgseisen.9 |
. . . . . . . . . . . 12
 RHom   |
25 | 24 | zrhrhm 14088 |
. . . . . . . . . . 11

ℤring RingHom    |
26 | | zringbas 14062 |
. . . . . . . . . . . 12
  ℤring |
27 | | eqid 2193 |
. . . . . . . . . . . 12
         |
28 | 26, 27 | rhmf 13643 |
. . . . . . . . . . 11
 ℤring RingHom            |
29 | 23, 25, 28 | 3syl 17 |
. . . . . . . . . 10
           |
30 | | 2z 9335 |
. . . . . . . . . . 11
 |
31 | | elfzelz 10081 |
. . . . . . . . . . 11
           |
32 | | zmulcl 9360 |
. . . . . . . . . . 11
 
     |
33 | 30, 31, 32 | sylancr 414 |
. . . . . . . . . 10
             |
34 | | ffvelcdm 5683 |
. . . . . . . . . 10
                         |
35 | 29, 33, 34 | syl2an 289 |
. . . . . . . . 9
 
                     |
36 | 35 | fmpttd 5705 |
. . . . . . . 8
                                   |
37 | 13, 27 | mgpbasg 13406 |
. . . . . . . . . 10

          |
38 | 12, 37 | syl 14 |
. . . . . . . . 9
           |
39 | 38 | feq3d 5384 |
. . . . . . . 8
                                                                     |
40 | 36, 39 | mpbid 147 |
. . . . . . 7
                                   |
41 | | lgseisen.2 |
. . . . . . . 8
       |
42 | | lgseisen.3 |
. . . . . . . 8
   |
43 | | lgseisen.4 |
. . . . . . . 8
       |
44 | | lgseisen.5 |
. . . . . . . 8
                      |
45 | | lgseisen.6 |
. . . . . . . 8
       |
46 | 7, 41, 42, 43, 44, 45 | lgseisenlem2 15135 |
. . . . . . 7
                       |
47 | 5, 6, 15, 16, 22, 40, 46 | gsumfzreidx 13396 |
. . . . . 6
  g                   g                      |
48 | 4, 47 | eqtr3id 2240 |
. . . . 5
  g                   g                      |
49 | 7, 41, 42, 43, 44 | lgseisenlem1 15134 |
. . . . . . . 8
                       |
50 | 44 | fmpt 5700 |
. . . . . . . 8
 
                           
                      |
51 | 49, 50 | sylibr 134 |
. . . . . . 7
                                |
52 | 44 | a1i 9 |
. . . . . . 7
                  
     |
53 | | eqidd 2194 |
. . . . . . 7
                                   |
54 | | oveq2 5918 |
. . . . . . . 8
         
             
     |
55 | 54 | fveq2d 5550 |
. . . . . . 7
         
                           |
56 | 51, 52, 53, 55 | fmptcof 5717 |
. . . . . 6
                                        
       |
57 | 56 | oveq2d 5926 |
. . . . 5
  g                     g                      
        |
58 | 41 | eldifad 3164 |
. . . . . . . . . . . . . . . . . . . . 21
   |
59 | 58 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
 
           |
60 | | prmz 12239 |
. . . . . . . . . . . . . . . . . . . 20

  |
61 | 59, 60 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
 
           |
62 | | 2nn 9133 |
. . . . . . . . . . . . . . . . . . . . 21
 |
63 | | elfznn 10110 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
64 | 63 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . 21
 
           |
65 | | nnmulcl 8993 |
. . . . . . . . . . . . . . . . . . . . 21
 
     |
66 | 62, 64, 65 | sylancr 414 |
. . . . . . . . . . . . . . . . . . . 20
 
             |
67 | 66 | nnzd 9428 |
. . . . . . . . . . . . . . . . . . 19
 
             |
68 | 61, 67 | zmulcld 9435 |
. . . . . . . . . . . . . . . . . 18
 
         
     |
69 | 8 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
 
           |
70 | | prmnn 12238 |
. . . . . . . . . . . . . . . . . . 19

  |
71 | 69, 70 | syl 14 |
. . . . . . . . . . . . . . . . . 18
 
           |
72 | 68, 71 | zmodcld 10406 |
. . . . . . . . . . . . . . . . 17
 
                 |
73 | 43, 72 | eqeltrid 2280 |
. . . . . . . . . . . . . . . 16
 
           |
74 | 73 | nn0zd 9427 |
. . . . . . . . . . . . . . 15
 
           |
75 | | m1expcl 10623 |
. . . . . . . . . . . . . . 15
        |
76 | 74, 75 | syl 14 |
. . . . . . . . . . . . . 14
 
                |
77 | 76, 74 | zmulcld 9435 |
. . . . . . . . . . . . 13
 
                  |
78 | 77, 71 | zmodcld 10406 |
. . . . . . . . . . . 12
 
                
   |
79 | 78 | nn0cnd 9285 |
. . . . . . . . . . 11
 
                
   |
80 | | 2cnd 9045 |
. . . . . . . . . . 11
 
           |
81 | | 2ap0 9065 |
. . . . . . . . . . . 12
#  |
82 | 81 | a1i 9 |
. . . . . . . . . . 11
 
         #   |
83 | 79, 80, 82 | divcanap2d 8801 |
. . . . . . . . . 10
 
                  
              |
84 | 83 | fveq2d 5550 |
. . . . . . . . 9
 
                                         |
85 | | zq 9681 |
. . . . . . . . . . . . . . 15
   |
86 | 8, 19, 85 | 3syl 17 |
. . . . . . . . . . . . . 14
   |
87 | 86 | adantr 276 |
. . . . . . . . . . . . 13
 
           |
88 | 71 | nngt0d 9016 |
. . . . . . . . . . . . 13
 
           |
89 | | eqidd 2194 |
. . . . . . . . . . . . 13
 
              
          |
90 | 43 | oveq1i 5920 |
. . . . . . . . . . . . . 14
           |
91 | | zq 9681 |
. . . . . . . . . . . . . . . 16
     
     |
92 | 68, 91 | syl 14 |
. . . . . . . . . . . . . . 15
 
         
     |
93 | | modqabs2 10419 |
. . . . . . . . . . . . . . 15
     
       
         |
94 | 92, 87, 88, 93 | syl3anc 1249 |
. . . . . . . . . . . . . 14
 
               
         |
95 | 90, 94 | eqtrid 2238 |
. . . . . . . . . . . . 13
 
                   |
96 | 76, 76, 74, 68, 87, 88, 89, 95 | modqmul12d 10439 |
. . . . . . . . . . . 12
 
                
                |
97 | | zq 9681 |
. . . . . . . . . . . . . 14
                 |
98 | 77, 97 | syl 14 |
. . . . . . . . . . . . 13
 
                  |
99 | | modqabs2 10419 |
. . . . . . . . . . . . 13
        
                   
   |
100 | 98, 87, 88, 99 | syl3anc 1249 |
. . . . . . . . . . . 12
 
                           
   |
101 | 76 | zcnd 9430 |
. . . . . . . . . . . . . 14
 
                |
102 | 61 | zcnd 9430 |
. . . . . . . . . . . . . 14
 
           |
103 | 67 | zcnd 9430 |
. . . . . . . . . . . . . 14
 
             |
104 | 101, 102,
103 | mulassd 8033 |
. . . . . . . . . . . . 13
 
                                 |
105 | 104 | oveq1d 5925 |
. . . . . . . . . . . 12
 
                             
       |
106 | 96, 100, 105 | 3eqtr4d 2236 |
. . . . . . . . . . 11
 
                                   |
107 | 8, 70 | syl 14 |
. . . . . . . . . . . . 13
   |
108 | 107 | adantr 276 |
. . . . . . . . . . . 12
 
           |
109 | 78 | nn0zd 9427 |
. . . . . . . . . . . 12
 
                
   |
110 | 76, 61 | zmulcld 9435 |
. . . . . . . . . . . . 13
 
                  |
111 | 110, 67 | zmulcld 9435 |
. . . . . . . . . . . 12
 
                      |
112 | | moddvds 11932 |
. . . . . . . . . . . 12
                                
              
        
                |
113 | 108, 109,
111, 112 | syl3anc 1249 |
. . . . . . . . . . 11
 
                                 
        
                |
114 | 106, 113 | mpbid 147 |
. . . . . . . . . 10
 
                                 |
115 | 71 | nnnn0d 9283 |
. . . . . . . . . . 11
 
           |
116 | 9, 24 | zndvds 14114 |
. . . . . . . . . . 11
                                                   
                         |
117 | 115, 109,
111, 116 | syl3anc 1249 |
. . . . . . . . . 10
 
                    
                
        
                |
118 | 114, 117 | mpbird 167 |
. . . . . . . . 9
 
                                       |
119 | 23, 25 | syl 14 |
. . . . . . . . . . 11
 ℤring
RingHom    |
120 | 119 | adantr 276 |
. . . . . . . . . 10
 
         ℤring RingHom    |
121 | | zringmulr 14065 |
. . . . . . . . . . 11
  ℤring |
122 | | eqid 2193 |
. . . . . . . . . . 11
         |
123 | 26, 121, 122 | rhmmul 13644 |
. . . . . . . . . 10
  ℤring
RingHom                                                      |
124 | 120, 110,
67, 123 | syl3anc 1249 |
. . . . . . . . 9
 
                                                   |
125 | 84, 118, 124 | 3eqtrd 2230 |
. . . . . . . 8
 
                                                     |
126 | 125 | mpteq2dva 4119 |
. . . . . . 7
                      
                                          |
127 | 16, 22 | fzfigd 10492 |
. . . . . . . 8
           |
128 | 29 | adantr 276 |
. . . . . . . . 9
 
                   |
129 | 128, 110 | ffvelcdmd 5686 |
. . . . . . . 8
 
                          |
130 | 128, 67 | ffvelcdmd 5686 |
. . . . . . . 8
 
                     |
131 | | eqidd 2194 |
. . . . . . . 8
                                             |
132 | | eqidd 2194 |
. . . . . . . 8
                                   |
133 | 127, 129,
130, 131, 132 | offval2 6138 |
. . . . . . 7
                                                                                    |
134 | 126, 133 | eqtr4d 2229 |
. . . . . 6
                      
                                                     |
135 | 134 | oveq2d 5926 |
. . . . 5
  g                      
       g                                                  |
136 | 48, 57, 135 | 3eqtrd 2230 |
. . . 4
  g                   g                                                  |
137 | | eqid 2193 |
. . . . . 6
       |
138 | 38 | eleq2d 2263 |
. . . . . . . 8
                                   |
139 | 138 | adantr 276 |
. . . . . . 7
 
                        
                  |
140 | 129, 139 | mpbid 147 |
. . . . . 6
 
                          |
141 | 38 | eleq2d 2263 |
. . . . . . . 8
                         |
142 | 141 | adantr 276 |
. . . . . . 7
 
                   
             |
143 | 130, 142 | mpbid 147 |
. . . . . 6
 
                     |
144 | | eqid 2193 |
. . . . . 6
                                           |
145 | | eqid 2193 |
. . . . . 6
                                 |
146 | 5, 137, 15, 16, 22, 140, 143, 144, 145 | gsumfzmptfidmadd2 13399 |
. . . . 5
  g                                                 g                             g                     |
147 | 13, 122 | mgpplusgg 13404 |
. . . . . . . . 9

         |
148 | 12, 147 | syl 14 |
. . . . . . . 8
          |
149 | 148 | ofeqd 6124 |
. . . . . . 7
              |
150 | 149 | oveqd 5927 |
. . . . . 6
                                                                                              |
151 | 150 | oveq2d 5926 |
. . . . 5
  g                                                 g                                                 |
152 | 148 | oveqd 5927 |
. . . . 5
   g                              g                     g 
                           g                     |
153 | 146, 151,
152 | 3eqtr4d 2236 |
. . . 4
  g                                                  g                              g                     |
154 | 136, 153 | eqtrd 2226 |
. . 3
  g                    g                              g                     |
155 | 154 | oveq1d 5925 |
. 2
   g                   /r    g                      g                              g                    /r    g                     |
156 | 15 | cmnmndd 13367 |
. . . 4
   |
157 | | eqid 2193 |
. . . . . 6
Unit  Unit   |
158 | 157, 13 | unitsubm 13599 |
. . . . 5

Unit  SubMnd    |
159 | 23, 158 | syl 14 |
. . . 4
 Unit  SubMnd    |
160 | | elfzle2 10084 |
. . . . . . . . . 10
               |
161 | 160 | adantl 277 |
. . . . . . . . 9
 
               |
162 | 64 | nnred 8985 |
. . . . . . . . . 10
 
           |
163 | | prmuz2 12259 |
. . . . . . . . . . . 12

      |
164 | | uz2m1nn 9660 |
. . . . . . . . . . . 12
    
    |
165 | 69, 163, 164 | 3syl 17 |
. . . . . . . . . . 11
 
         
   |
166 | 165 | nnred 8985 |
. . . . . . . . . 10
 
         
   |
167 | | 2re 9042 |
. . . . . . . . . . 11
 |
168 | 167 | a1i 9 |
. . . . . . . . . 10
 
           |
169 | | 2pos 9063 |
. . . . . . . . . . 11
 |
170 | 169 | a1i 9 |
. . . . . . . . . 10
 
           |
171 | | lemuldiv2 8891 |
. . . . . . . . . 10
  
   
    
       |
172 | 162, 166,
168, 170, 171 | syl112anc 1253 |
. . . . . . . . 9
 
           
 
       |
173 | 161, 172 | mpbird 167 |
. . . . . . . 8
 
               |
174 | 69, 19 | syl 14 |
. . . . . . . . 9
 
           |
175 | | peano2zm 9345 |
. . . . . . . . 9
 
   |
176 | | fznn 10145 |
. . . . . . . . 9
           
           |
177 | 174, 175,
176 | 3syl 17 |
. . . . . . . 8
 
                 
           |
178 | 66, 173, 177 | mpbir2and 946 |
. . . . . . 7
 
                   |
179 | | fzm1ndvds 11988 |
. . . . . . 7
          
    |
180 | 71, 178, 179 | syl2anc 411 |
. . . . . 6
 
             |
181 | 9, 157, 24 | znunit 14124 |
. . . . . . . 8
            Unit    
    |
182 | 115, 67, 181 | syl2anc 411 |
. . . . . . 7
 
                Unit 
       |
183 | | coprm 12272 |
. . . . . . . . 9
               |
184 | 19 | adantr 276 |
. . . . . . . . . . 11
    
  |
185 | | simpr 110 |
. . . . . . . . . . 11
         |
186 | 184, 185 | gcdcomd 12101 |
. . . . . . . . . 10
               |
187 | 186 | eqeq1d 2202 |
. . . . . . . . 9
                 |
188 | 183, 187 | bitrd 188 |
. . . . . . . 8
               |
189 | 69, 67, 188 | syl2anc 411 |
. . . . . . 7
 
         
 
       |
190 | 182, 189 | bitr4d 191 |
. . . . . 6
 
                Unit 
     |
191 | 180, 190 | mpbird 167 |
. . . . 5
 
               Unit    |
192 | 191 | fmpttd 5705 |
. . . 4
                             Unit    |
193 | 156, 16, 22, 159, 192 | gsumfzsubmcl 13397 |
. . 3
  g                  Unit    |
194 | | eqid 2193 |
. . . 4
/r  /r   |
195 | | eqid 2193 |
. . . 4
         |
196 | 157, 194,
195 | dvrid 13617 |
. . 3
   g                  Unit  
  g                   /r    g 
                       |
197 | 23, 193, 196 | syl2anc 411 |
. 2
   g                   /r    g                         |
198 | 129 | fmpttd 5705 |
. . . . . 6
                                        |
199 | 38 | feq3d 5384 |
. . . . . 6
                                                                               |
200 | 198, 199 | mpbid 147 |
. . . . 5
                                        |
201 | 5, 6, 156, 16, 22, 200 | gsumfzcl 13061 |
. . . 4
  g                             |
202 | 201, 38 | eleqtrrd 2273 |
. . 3
  g                             |
203 | 27, 157, 194, 122 | dvrcan3 13621 |
. . 3
   g                          
 g                  Unit      g 
                            g                    /r    g                    g                         |
204 | 23, 202, 193, 203 | syl3anc 1249 |
. 2
    g 
                            g                    /r    g                    g                         |
205 | 155, 197,
204 | 3eqtr3rd 2235 |
1
  g                             |