Step | Hyp | Ref
| Expression |
1 | | fzfid 12218 |
. . . 4
 

          |
2 | | simpl 463 |
. . . . 5
 

  |
3 | | elfznn 11857 |
. . . . 5
           |
4 | | rpvmasum2.g |
. . . . . . 7
DChr   |
5 | | rpvmasum.z |
. . . . . . 7
ℤ/nℤ   |
6 | | rpvmasum2.d |
. . . . . . 7
     |
7 | | rpvmasum.l |
. . . . . . 7
 RHom   |
8 | | rpvmasum2.w |
. . . . . . . . . . 11
                |
9 | | ssrab2 3526 |
. . . . . . . . . . 11
   
           
  |
10 | 8, 9 | eqsstri 3474 |
. . . . . . . . . 10

  |
11 | | dchrisum0.b |
. . . . . . . . . 10
   |
12 | 10, 11 | sseldi 3442 |
. . . . . . . . 9
     |
13 | 12 | eldifad 3428 |
. . . . . . . 8
   |
14 | 13 | adantr 471 |
. . . . . . 7
 

  |
15 | | nnz 10988 |
. . . . . . . 8
   |
16 | 15 | adantl 472 |
. . . . . . 7
 

  |
17 | 4, 5, 6, 7, 14, 16 | dchrzrhcl 24222 |
. . . . . 6
 

          |
18 | | nnrp 11340 |
. . . . . . . . 9
   |
19 | 18 | adantl 472 |
. . . . . . . 8
 

  |
20 | 19 | rpsqrtcld 13522 |
. . . . . . 7
 

      |
21 | 20 | rpcnd 11372 |
. . . . . 6
 

      |
22 | 20 | rpne0d 11375 |
. . . . . 6
 

      |
23 | 17, 21, 22 | divcld 10411 |
. . . . 5
 

                |
24 | 2, 3, 23 | syl2an 484 |
. . . 4
            
                |
25 | 1, 24 | fsumcl 13848 |
. . 3
 

                          |
26 | | dchrisum0lem2.u |
. . . . 5
    |
27 | | rlimcl 13616 |
. . . . 5
    |
28 | 26, 27 | syl 17 |
. . . 4
   |
29 | 28 | adantr 471 |
. . 3
 

  |
30 | | 0xr 9713 |
. . . . . . . . 9
 |
31 | | 0lt1 10164 |
. . . . . . . . 9
 |
32 | | df-ioo 11668 |
. . . . . . . . . 10




    |
33 | | df-ico 11670 |
. . . . . . . . . 10




    |
34 | | xrltletr 11483 |
. . . . . . . . . 10
    
    |
35 | 32, 33, 34 | ixxss1 11682 |
. . . . . . . . 9
    
      |
36 | 30, 31, 35 | mp2an 683 |
. . . . . . . 8
       |
37 | | ioorp 11741 |
. . . . . . . 8
    |
38 | 36, 37 | sseqtri 3476 |
. . . . . . 7
    |
39 | | resmpt 5173 |
. . . . . . 7
     
                                                            |
40 | 38, 39 | ax-mp 5 |
. . . . . 6
                                                             |
41 | 38 | sseli 3440 |
. . . . . . . . 9
   
  |
42 | 3 | adantl 472 |
. . . . . . . . . 10
            
  |
43 | | fveq2 5888 |
. . . . . . . . . . . . 13
           |
44 | 43 | fveq2d 5892 |
. . . . . . . . . . . 12
                   |
45 | | fveq2 5888 |
. . . . . . . . . . . 12
           |
46 | 44, 45 | oveq12d 6333 |
. . . . . . . . . . 11
                               |
47 | | dchrisum0lem1.f |
. . . . . . . . . . 11
                 |
48 | | ovex 6343 |
. . . . . . . . . . 11
               |
49 | 46, 47, 48 | fvmpt3i 5976 |
. . . . . . . . . 10
                     |
50 | 42, 49 | syl 17 |
. . . . . . . . 9
            
                    |
51 | 41, 50 | sylanl2 661 |
. . . . . . . 8
               
                    |
52 | | 1re 9668 |
. . . . . . . . . . . 12
 |
53 | | elicopnf 11759 |
. . . . . . . . . . . 12
    
     |
54 | 52, 53 | ax-mp 5 |
. . . . . . . . . . 11
   
    |
55 | | flge1nn 12087 |
. . . . . . . . . . 11
         |
56 | 54, 55 | sylbi 200 |
. . . . . . . . . 10
   
      |
57 | 56 | adantl 472 |
. . . . . . . . 9
 
          |
58 | | nnuz 11223 |
. . . . . . . . 9
     |
59 | 57, 58 | syl6eleq 2550 |
. . . . . . . 8
 
              |
60 | 41, 24 | sylanl2 661 |
. . . . . . . 8
               
                |
61 | 51, 59, 60 | fsumser 13845 |
. . . . . . 7
 
                                        |
62 | 61 | mpteq2dva 4503 |
. . . . . 6
     
                                         |
63 | 40, 62 | syl5eq 2508 |
. . . . 5
                                                 |
64 | | fveq2 5888 |
. . . . . . 7
                       |
65 | | rpssre 11341 |
. . . . . . . . 9
 |
66 | 65 | a1i 11 |
. . . . . . . 8
   |
67 | 38, 66 | syl5ss 3455 |
. . . . . . 7
      |
68 | | 1zzd 10997 |
. . . . . . 7
   |
69 | 46 | cbvmptv 4509 |
. . . . . . . . . . . . 13
                                 |
70 | 47, 69 | eqtri 2484 |
. . . . . . . . . . . 12
                 |
71 | 23, 70 | fmptd 6069 |
. . . . . . . . . . 11
       |
72 | 71 | ffvelrnda 6045 |
. . . . . . . . . 10
 

      |
73 | 58, 68, 72 | serf 12273 |
. . . . . . . . 9
          |
74 | 73 | feqmptd 5941 |
. . . . . . . 8
              |
75 | | dchrisum0.s |
. . . . . . . 8
      |
76 | 74, 75 | eqbrtrrd 4439 |
. . . . . . 7
           |
77 | 73 | ffvelrnda 6045 |
. . . . . . 7
 

        |
78 | 54 | simprbi 470 |
. . . . . . . 8
   
  |
79 | 78 | adantl 472 |
. . . . . . 7
 
      |
80 | 58, 64, 67, 68, 76, 77, 79 | climrlim2 13660 |
. . . . . 6
                   |
81 | | rlimo1 13729 |
. . . . . 6
                                     |
82 | 80, 81 | syl 17 |
. . . . 5
                     |
83 | 63, 82 | eqeltrd 2540 |
. . . 4
                                     |
84 | | eqid 2462 |
. . . . . 6

                                                    |
85 | 25, 84 | fmptd 6069 |
. . . . 5
                                 |
86 | | 1red 9684 |
. . . . 5
   |
87 | 85, 66, 86 | o1resb 13679 |
. . . 4
                                
                                   |
88 | 83, 87 | mpbird 240 |
. . 3
                                |
89 | | o1const 13732 |
. . . 4
          |
90 | 65, 28, 89 | sylancr 674 |
. . 3
        |
91 | 25, 29, 88, 90 | o1mul2 13737 |
. 2
                                  |
92 | | simpr 467 |
. . . . . . . . 9
 

  |
93 | | 2z 10998 |
. . . . . . . . 9
 |
94 | | rpexpcl 12323 |
. . . . . . . . 9
         |
95 | 92, 93, 94 | sylancl 673 |
. . . . . . . 8
 

      |
96 | 3 | nnrpd 11368 |
. . . . . . . 8
           |
97 | | rpdivcl 11354 |
. . . . . . . 8
               |
98 | 95, 96, 97 | syl2an 484 |
. . . . . . 7
            
        |
99 | | dchrisum0lem2.h |
. . . . . . . . 9
                           |
100 | 99 | divsqrsumf 23955 |
. . . . . . . 8
     |
101 | 100 | ffvelrni 6044 |
. . . . . . 7
      
            |
102 | 98, 101 | syl 17 |
. . . . . 6
            
            |
103 | 102 | recnd 9695 |
. . . . 5
            
            |
104 | 24, 103 | mulcld 9689 |
. . . 4
            
                            |
105 | 1, 104 | fsumcl 13848 |
. . 3
 

                                      |
106 | 25, 29 | mulcld 9689 |
. . 3
 

                            |
107 | 26 | ad2antrr 737 |
. . . . . . . . 9
            
   |
108 | 107, 27 | syl 17 |
. . . . . . . 8
            
  |
109 | 24, 108 | mulcld 9689 |
. . . . . . 7
            
                  |
110 | 1, 104, 109 | fsumsub 13898 |
. . . . . 6
 

                                                                                                                        |
111 | 24, 103, 108 | subdid 10102 |
. . . . . . 7
            
                                                                          |
112 | 111 | sumeq2dv 13818 |
. . . . . 6
 

                                                                                              |
113 | 1, 29, 24 | fsummulc1 13895 |
. . . . . . 7
 

                                                      |
114 | 113 | oveq2d 6331 |
. . . . . 6
 

                                                                                                                                  |
115 | 110, 112,
114 | 3eqtr4d 2506 |
. . . . 5
 

                                                                                                        |
116 | 115 | mpteq2dva 4503 |
. . . 4
                                                                                                             |
117 | 103, 108 | subcld 10012 |
. . . . . . 7
            
              |
118 | 24, 117 | mulcld 9689 |
. . . . . 6
            
                              |
119 | 1, 118 | fsumcl 13848 |
. . . . 5
 

                                        |
120 | 119 | abscld 13547 |
. . . . . . 7
 

   
                                        |
121 | 118 | abscld 13547 |
. . . . . . . 8
            
                                  |
122 | 1, 121 | fsumrecl 13849 |
. . . . . . 7
 

                                            |
123 | | 1red 9684 |
. . . . . . 7
 

  |
124 | 1, 118 | fsumabs 13910 |
. . . . . . 7
 

   
                                                                                  |
125 | | rprege0 11345 |
. . . . . . . . . . . 12

    |
126 | 125 | adantl 472 |
. . . . . . . . . . 11
 

    |
127 | 126 | simpld 465 |
. . . . . . . . . 10
 

  |
128 | | reflcl 12064 |
. . . . . . . . . 10
       |
129 | 127, 128 | syl 17 |
. . . . . . . . 9
 

      |
130 | 129, 92 | rerpdivcld 11398 |
. . . . . . . 8
 

        |
131 | | simplr 767 |
. . . . . . . . . . 11
            
  |
132 | 131 | rprecred 11381 |
. . . . . . . . . 10
            
    |
133 | 24 | abscld 13547 |
. . . . . . . . . . . 12
            
                    |
134 | 96 | rpsqrtcld 13522 |
. . . . . . . . . . . . . 14
               |
135 | 134 | adantl 472 |
. . . . . . . . . . . . 13
            
      |
136 | 135 | rprecred 11381 |
. . . . . . . . . . . 12
            
        |
137 | 117 | abscld 13547 |
. . . . . . . . . . . 12
            
                  |
138 | 135, 131 | rpdivcld 11387 |
. . . . . . . . . . . . 13
            
        |
139 | 65, 138 | sseldi 3442 |
. . . . . . . . . . . 12
            
        |
140 | 24 | absge0d 13555 |
. . . . . . . . . . . 12
            
                    |
141 | 117 | absge0d 13555 |
. . . . . . . . . . . 12
            
                  |
142 | 2, 3, 17 | syl2an 484 |
. . . . . . . . . . . . . . 15
            
          |
143 | 135 | rpcnd 11372 |
. . . . . . . . . . . . . . 15
            
      |
144 | 135 | rpne0d 11375 |
. . . . . . . . . . . . . . 15
            
      |
145 | 142, 143,
144 | absdivd 13566 |
. . . . . . . . . . . . . 14
            
                                          |
146 | 135 | rprege0d 11377 |
. . . . . . . . . . . . . . . 16
            
            |
147 | | absid 13408 |
. . . . . . . . . . . . . . . 16
                         |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . . 15
            
              |
149 | 148 | oveq2d 6331 |
. . . . . . . . . . . . . 14
            
                                          |
150 | 145, 149 | eqtrd 2496 |
. . . . . . . . . . . . 13
            
                                      |
151 | 142 | abscld 13547 |
. . . . . . . . . . . . . 14
            
              |
152 | | 1red 9684 |
. . . . . . . . . . . . . 14
            
  |
153 | | eqid 2462 |
. . . . . . . . . . . . . . 15
         |
154 | 13 | ad2antrr 737 |
. . . . . . . . . . . . . . 15
            
  |
155 | | rpvmasum.a |
. . . . . . . . . . . . . . . . . . 19
   |
156 | 155 | nnnn0d 10954 |
. . . . . . . . . . . . . . . . . 18
   |
157 | 5, 153, 7 | znzrhfo 19167 |
. . . . . . . . . . . . . . . . . 18

          |
158 | | fof 5816 |
. . . . . . . . . . . . . . . . . 18
                   |
159 | 156, 157,
158 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
           |
160 | 159 | adantr 471 |
. . . . . . . . . . . . . . . 16
 

          |
161 | | elfzelz 11829 |
. . . . . . . . . . . . . . . 16
           |
162 | | ffvelrn 6043 |
. . . . . . . . . . . . . . . 16
                     |
163 | 160, 161,
162 | syl2an 484 |
. . . . . . . . . . . . . . 15
            
          |
164 | 4, 6, 5, 153, 154, 163 | dchrabs2 24239 |
. . . . . . . . . . . . . 14
            
              |
165 | 151, 152,
135, 164 | lediv1dd 11425 |
. . . . . . . . . . . . 13
            
                          |
166 | 150, 165 | eqbrtrd 4437 |
. . . . . . . . . . . 12
            
                          |
167 | 99, 107 | divsqrtsum2 23957 |
. . . . . . . . . . . . . 14
   

                               
              |
168 | 98, 167 | mpdan 679 |
. . . . . . . . . . . . 13
            
                              |
169 | 95 | rprege0d 11377 |
. . . . . . . . . . . . . . . . 17
 

            |
170 | | sqrtdiv 13378 |
. . . . . . . . . . . . . . . . 17
      
                                |
171 | 169, 96, 170 | syl2an 484 |
. . . . . . . . . . . . . . . 16
            
                          |
172 | 125 | ad2antlr 738 |
. . . . . . . . . . . . . . . . . 18
            
    |
173 | | sqrtsq 13382 |
. . . . . . . . . . . . . . . . . 18
             |
174 | 172, 173 | syl 17 |
. . . . . . . . . . . . . . . . 17
            
          |
175 | 174 | oveq1d 6330 |
. . . . . . . . . . . . . . . 16
            
                      |
176 | 171, 175 | eqtrd 2496 |
. . . . . . . . . . . . . . 15
            
                  |
177 | 176 | oveq2d 6331 |
. . . . . . . . . . . . . 14
            
                      |
178 | | rpcnne0 11348 |
. . . . . . . . . . . . . . . 16

    |
179 | 178 | ad2antlr 738 |
. . . . . . . . . . . . . . 15
            
    |
180 | 135 | rpcnne0d 11379 |
. . . . . . . . . . . . . . 15
            
            |
181 | | recdiv 10341 |
. . . . . . . . . . . . . . 15
              
                |
182 | 179, 180,
181 | syl2anc 671 |
. . . . . . . . . . . . . 14
            
                |
183 | 177, 182 | eqtrd 2496 |
. . . . . . . . . . . . 13
            
                    |
184 | 168, 183 | breqtrd 4441 |
. . . . . . . . . . . 12
            
                        |
185 | 133, 136,
137, 139, 140, 141, 166, 184 | lemul12ad 10577 |
. . . . . . . . . . 11
            
                                                    |
186 | 24, 117 | absmuld 13565 |
. . . . . . . . . . 11
            
                                                                      |
187 | | 1cnd 9685 |
. . . . . . . . . . . . 13
            
  |
188 | | dmdcan 10345 |
. . . . . . . . . . . . 13
            
                    |
189 | 180, 179,
187, 188 | syl3anc 1276 |
. . . . . . . . . . . 12
            
                  |
190 | 138 | rpcnd 11372 |
. . . . . . . . . . . . 13
            
        |
191 | | reccl 10305 |
. . . . . . . . . . . . . 14
                   |
192 | 180, 191 | syl 17 |
. . . . . . . . . . . . 13
            
        |
193 | 190, 192 | mulcomd 9690 |
. . . . . . . . . . . 12
            
                              |
194 | 189, 193 | eqtr3d 2498 |
. . . . . . . . . . 11
            
                  |
195 | 185, 186,
194 | 3brtr4d 4447 |
. . . . . . . . . 10
            
                                    |
196 | 1, 121, 132, 195 | fsumle 13908 |
. . . . . . . . 9
 

                                                        |
197 | | flge0nn0 12086 |
. . . . . . . . . . . 12
         |
198 | | hashfz1 12561 |
. . . . . . . . . . . 12
    
                  |
199 | 126, 197,
198 | 3syl 18 |
. . . . . . . . . . 11
 

                  |
200 | 199 | oveq1d 6330 |
. . . . . . . . . 10
 

                          |
201 | 92 | rpreccld 11380 |
. . . . . . . . . . . 12
 

    |
202 | 201 | rpcnd 11372 |
. . . . . . . . . . 11
 

    |
203 | | fsumconst 13900 |
. . . . . . . . . . 11
                                           |
204 | 1, 202, 203 | syl2anc 671 |
. . . . . . . . . 10
 

                              |
205 | 129 | recnd 9695 |
. . . . . . . . . . 11
 

      |
206 | 178 | adantl 472 |
. . . . . . . . . . . 12
 

    |
207 | 206 | simpld 465 |
. . . . . . . . . . 11
 

  |
208 | 206 | simprd 469 |
. . . . . . . . . . 11
 

  |
209 | 205, 207,
208 | divrecd 10414 |
. . . . . . . . . 10
 

                |
210 | 200, 204,
209 | 3eqtr4d 2506 |
. . . . . . . . 9
 

                    |
211 | 196, 210 | breqtrd 4441 |
. . . . . . . 8
 

                                                  |
212 | | flle 12067 |
. . . . . . . . . . 11
       |
213 | 127, 212 | syl 17 |
. . . . . . . . . 10
 

      |
214 | 127 | recnd 9695 |
. . . . . . . . . . 11
 

  |
215 | 214 | mulid1d 9686 |
. . . . . . . . . 10
 

    |
216 | 213, 215 | breqtrrd 4443 |
. . . . . . . . 9
 

        |
217 | | rpregt0 11344 |
. . . . . . . . . . 11

    |
218 | 217 | adantl 472 |
. . . . . . . . . 10
 

    |
219 | | ledivmul 10509 |
. . . . . . . . . 10
     
                   |
220 | 129, 123,
218, 219 | syl3anc 1276 |
. . . . . . . . 9
 

      
         |
221 | 216, 220 | mpbird 240 |
. . . . . . . 8
 

        |
222 | 122, 130,
123, 211, 221 | letrd 9818 |
. . . . . . 7
 

                                            |
223 | 120, 122,
123, 124, 222 | letrd 9818 |
. . . . . 6
 

   
                                        |
224 | 223 | adantrr 728 |
. . . . 5
 
                                               |
225 | 66, 119, 86, 86, 224 | elo1d 13649 |
. . . 4
                                              |
226 | 116, 225 | eqeltrrd 2541 |
. . 3
                                                                        |
227 | 105, 106,
226 | o1dif 13742 |
. 2
                                                                             |
228 | 91, 227 | mpbird 240 |
1
                                            |