Proof of Theorem dchrisum0lem1
Step | Hyp | Ref
| Expression |
1 | | fzfid 12186 |
. . . 4
 

          |
2 | | fzfid 12186 |
. . . 4
 

                    |
3 | | fzfid 12186 |
. . . 4
            
                      |
4 | | elfznn 11828 |
. . . . . . 7
           |
5 | | elfzuz 11796 |
. . . . . . 7
                                 |
6 | 4, 5 | anim12i 570 |
. . . . . 6
         
                                   |
7 | 6 | a1i 11 |
. . . . 5
 

         
                                    |
8 | | elfzuz 11796 |
. . . . . . 7
                               |
9 | | elfznn 11828 |
. . . . . . 7
                 |
10 | 8, 9 | anim12ci 571 |
. . . . . 6
                   
                             |
11 | 10 | a1i 11 |
. . . . 5
 

                   
                              |
12 | | eluzelz 11168 |
. . . . . . . . . . . 12
          
  |
13 | 12 | ad2antll 735 |
. . . . . . . . . . 11
    
              |
14 | 13 | zred 11040 |
. . . . . . . . . 10
    
              |
15 | | simpr 463 |
. . . . . . . . . . . . 13
 

  |
16 | | 2z 10969 |
. . . . . . . . . . . . 13
 |
17 | | rpexpcl 12291 |
. . . . . . . . . . . . 13
         |
18 | 15, 16, 17 | sylancl 668 |
. . . . . . . . . . . 12
 

      |
19 | 18 | rpred 11341 |
. . . . . . . . . . 11
 

      |
20 | 19 | adantr 467 |
. . . . . . . . . 10
    
                  |
21 | | simprl 764 |
. . . . . . . . . . 11
    
              |
22 | 21 | nnrpd 11339 |
. . . . . . . . . 10
    
              |
23 | 14, 20, 22 | lemuldivd 11387 |
. . . . . . . . 9
    
                  
         |
24 | 21 | nnred 10624 |
. . . . . . . . . 10
    
              |
25 | 15 | rprege0d 11348 |
. . . . . . . . . . . . . 14
 

    |
26 | | flge0nn0 12054 |
. . . . . . . . . . . . . 14
         |
27 | | nn0p1nn 10909 |
. . . . . . . . . . . . . 14
    
        |
28 | 25, 26, 27 | 3syl 18 |
. . . . . . . . . . . . 13
 

        |
29 | 28 | adantr 467 |
. . . . . . . . . . . 12
    
                    |
30 | | simprr 766 |
. . . . . . . . . . . 12
    
                        |
31 | | eluznn 11229 |
. . . . . . . . . . . 12
       
          
  |
32 | 29, 30, 31 | syl2anc 667 |
. . . . . . . . . . 11
    
              |
33 | 32 | nnrpd 11339 |
. . . . . . . . . 10
    
              |
34 | 24, 20, 33 | lemuldiv2d 11388 |
. . . . . . . . 9
    
                            |
35 | 23, 34 | bitr3d 259 |
. . . . . . . 8
    
                            |
36 | | rpcn 11310 |
. . . . . . . . . . . . . . . 16

  |
37 | 36 | adantl 468 |
. . . . . . . . . . . . . . 15
 

  |
38 | 37 | sqvald 12413 |
. . . . . . . . . . . . . 14
 

        |
39 | 38 | adantr 467 |
. . . . . . . . . . . . 13
    
                    |
40 | | simplr 762 |
. . . . . . . . . . . . . . . 16
    
              |
41 | 40 | rpred 11341 |
. . . . . . . . . . . . . . 15
    
              |
42 | | reflcl 12032 |
. . . . . . . . . . . . . . . 16
       |
43 | | peano2re 9806 |
. . . . . . . . . . . . . . . 16
             |
44 | 41, 42, 43 | 3syl 18 |
. . . . . . . . . . . . . . 15
    
                    |
45 | | fllep1 12037 |
. . . . . . . . . . . . . . . 16
         |
46 | 41, 45 | syl 17 |
. . . . . . . . . . . . . . 15
    
                    |
47 | | eluzle 11171 |
. . . . . . . . . . . . . . . 16
          
        |
48 | 47 | ad2antll 735 |
. . . . . . . . . . . . . . 15
    
                    |
49 | 41, 44, 14, 46, 48 | letrd 9792 |
. . . . . . . . . . . . . 14
    
              |
50 | 41, 14, 40 | lemul1d 11381 |
. . . . . . . . . . . . . 14
    
              
     |
51 | 49, 50 | mpbid 214 |
. . . . . . . . . . . . 13
    
                  |
52 | 39, 51 | eqbrtrd 4423 |
. . . . . . . . . . . 12
    
                    |
53 | 20, 41, 33 | ledivmuld 11391 |
. . . . . . . . . . . 12
    
                      
     |
54 | 52, 53 | mpbird 236 |
. . . . . . . . . . 11
    
                    |
55 | | nnre 10616 |
. . . . . . . . . . . . 13
   |
56 | 55 | ad2antrl 734 |
. . . . . . . . . . . 12
    
              |
57 | 20, 32 | nndivred 10658 |
. . . . . . . . . . . 12
    
                    |
58 | | letr 9727 |
. . . . . . . . . . . 12
       
        
          |
59 | 56, 57, 41, 58 | syl3anc 1268 |
. . . . . . . . . . 11
    
                          
   |
60 | 54, 59 | mpan2d 680 |
. . . . . . . . . 10
    
                  
   |
61 | 35, 60 | sylbid 219 |
. . . . . . . . 9
    
                  
   |
62 | 61 | pm4.71rd 641 |
. . . . . . . 8
    
                              |
63 | | nnge1 10635 |
. . . . . . . . . . . . . 14
   |
64 | 63 | ad2antrl 734 |
. . . . . . . . . . . . 13
    
              |
65 | | 1re 9642 |
. . . . . . . . . . . . . . . 16
 |
66 | | 0lt1 10136 |
. . . . . . . . . . . . . . . 16
 |
67 | 65, 66 | pm3.2i 457 |
. . . . . . . . . . . . . . 15
   |
68 | 67 | a1i 11 |
. . . . . . . . . . . . . 14
    
                |
69 | 22 | rpregt0d 11347 |
. . . . . . . . . . . . . 14
    
                |
70 | 18 | adantr 467 |
. . . . . . . . . . . . . . 15
    
                  |
71 | 70 | rpregt0d 11347 |
. . . . . . . . . . . . . 14
    
                        |
72 | | lediv2 10496 |
. . . . . . . . . . . . . 14
                                 |
73 | 68, 69, 71, 72 | syl3anc 1268 |
. . . . . . . . . . . . 13
    
                            |
74 | 64, 73 | mpbid 214 |
. . . . . . . . . . . 12
    
                          |
75 | 20 | recnd 9669 |
. . . . . . . . . . . . 13
    
                  |
76 | 75 | div1d 10375 |
. . . . . . . . . . . 12
    
                        |
77 | 74, 76 | breqtrd 4427 |
. . . . . . . . . . 11
    
                        |
78 | | simpl 459 |
. . . . . . . . . . . . 13
 
             |
79 | | nndivre 10645 |
. . . . . . . . . . . . 13
     
         |
80 | 19, 78, 79 | syl2an 480 |
. . . . . . . . . . . 12
    
                    |
81 | | letr 9727 |
. . . . . . . . . . . 12
                                       |
82 | 14, 80, 20, 81 | syl3anc 1268 |
. . . . . . . . . . 11
    
                                      |
83 | 77, 82 | mpan2d 680 |
. . . . . . . . . 10
    
                  
       |
84 | 35, 83 | sylbird 239 |
. . . . . . . . 9
    
                  
       |
85 | 84 | pm4.71rd 641 |
. . . . . . . 8
    
                                  |
86 | 35, 62, 85 | 3bitr3d 287 |
. . . . . . 7
    
                    
               |
87 | | fznnfl 12089 |
. . . . . . . . . 10
         
     |
88 | 87 | baibd 920 |
. . . . . . . . 9
 
         
   |
89 | 41, 21, 88 | syl2anc 667 |
. . . . . . . 8
    
                    
   |
90 | 80 | flcld 12034 |
. . . . . . . . . 10
    
                        |
91 | | elfz5 11792 |
. . . . . . . . . 10
                                           
             |
92 | 30, 90, 91 | syl2anc 667 |
. . . . . . . . 9
    
                                
             |
93 | | flge 12041 |
. . . . . . . . . 10
       
       
             |
94 | 80, 13, 93 | syl2anc 667 |
. . . . . . . . 9
    
                  
             |
95 | 92, 94 | bitr4d 260 |
. . . . . . . 8
    
                                
         |
96 | 89, 95 | anbi12d 717 |
. . . . . . 7
    
                                                      |
97 | 20 | flcld 12034 |
. . . . . . . . . 10
    
                      |
98 | | elfz5 11792 |
. . . . . . . . . 10
                                       
           |
99 | 30, 97, 98 | syl2anc 667 |
. . . . . . . . 9
    
                              
           |
100 | | flge 12041 |
. . . . . . . . . 10
     
     
           |
101 | 20, 13, 100 | syl2anc 667 |
. . . . . . . . 9
    
                
           |
102 | 99, 101 | bitr4d 260 |
. . . . . . . 8
    
                              
       |
103 | | fznnfl 12089 |
. . . . . . . . . 10
                     
           |
104 | 103 | baibd 920 |
. . . . . . . . 9
       
               
         |
105 | 57, 21, 104 | syl2anc 667 |
. . . . . . . 8
    
                          
         |
106 | 102, 105 | anbi12d 717 |
. . . . . . 7
    
                                                              |
107 | 86, 96, 106 | 3bitr4d 289 |
. . . . . 6
    
                                                                                |
108 | 107 | ex 436 |
. . . . 5
 

 
                                                                                |
109 | 7, 11, 108 | pm5.21ndd 356 |
. . . 4
 

         
                                                          |
110 | | ssun2 3598 |
. . . . . . . 8
                                                   |
111 | 28 | adantr 467 |
. . . . . . . . . 10
            
        |
112 | | nnuz 11194 |
. . . . . . . . . 10
     |
113 | 111, 112 | syl6eleq 2539 |
. . . . . . . . 9
            
            |
114 | | dchrisum0lem1a 24324 |
. . . . . . . . . 10
            
      
                     |
115 | 114 | simprd 465 |
. . . . . . . . 9
            
                    |
116 | | fzsplit2 11824 |
. . . . . . . . 9
                                                                             |
117 | 113, 115,
116 | syl2anc 667 |
. . . . . . . 8
            
                                              |
118 | 110, 117 | syl5sseqr 3481 |
. . . . . . 7
            
                                    |
119 | 118 | sselda 3432 |
. . . . . 6
   

                             
                |
120 | | rpvmasum2.g |
. . . . . . . . 9
DChr   |
121 | | rpvmasum.z |
. . . . . . . . 9
ℤ/nℤ   |
122 | | rpvmasum2.d |
. . . . . . . . 9
     |
123 | | rpvmasum.l |
. . . . . . . . 9
 RHom   |
124 | | rpvmasum2.w |
. . . . . . . . . . . . 13
                |
125 | | ssrab2 3514 |
. . . . . . . . . . . . 13
   
           
  |
126 | 124, 125 | eqsstri 3462 |
. . . . . . . . . . . 12

  |
127 | | dchrisum0.b |
. . . . . . . . . . . 12
   |
128 | 126, 127 | sseldi 3430 |
. . . . . . . . . . 11
     |
129 | 128 | eldifad 3416 |
. . . . . . . . . 10
   |
130 | 129 | ad3antrrr 736 |
. . . . . . . . 9
   

                       
  |
131 | | elfzelz 11800 |
. . . . . . . . . 10
                 |
132 | 131 | adantl 468 |
. . . . . . . . 9
   

                       
  |
133 | 120, 121,
122, 123, 130, 132 | dchrzrhcl 24173 |
. . . . . . . 8
   

                       
          |
134 | | elfznn 11828 |
. . . . . . . . . . . 12
                 |
135 | 134 | adantl 468 |
. . . . . . . . . . 11
   

                       
  |
136 | 135 | nnrpd 11339 |
. . . . . . . . . 10
   

                       
  |
137 | 136 | rpsqrtcld 13473 |
. . . . . . . . 9
   

                       
      |
138 | 137 | rpcnd 11343 |
. . . . . . . 8
   

                       
      |
139 | 137 | rpne0d 11346 |
. . . . . . . 8
   

                       
      |
140 | 133, 138,
139 | divcld 10383 |
. . . . . . 7
   

                       
                |
141 | 4 | adantl 468 |
. . . . . . . . . . . 12
            
  |
142 | 141 | nnrpd 11339 |
. . . . . . . . . . 11
            
  |
143 | 142 | rpsqrtcld 13473 |
. . . . . . . . . 10
            
      |
144 | 143 | rpcnne0d 11350 |
. . . . . . . . 9
            
            |
145 | 144 | adantr 467 |
. . . . . . . 8
   

                       
            |
146 | 145 | simpld 461 |
. . . . . . 7
   

                       
      |
147 | 145 | simprd 465 |
. . . . . . 7
   

                       
      |
148 | 140, 146,
147 | divcld 10383 |
. . . . . 6
   

                       
                      |
149 | 119, 148 | syldan 473 |
. . . . 5
   

                             
                      |
150 | 149 | anasss 653 |
. . . 4
            
                     
                      |
151 | 1, 2, 3, 109, 150 | fsumcom2 13835 |
. . 3
 

          
                                                                                                   |
152 | 151 | mpteq2dva 4489 |
. 2
                                                                            
                                      |
153 | 65 | a1i 11 |
. . 3
   |
154 | | 2cn 10680 |
. . . . . . . 8
 |
155 | 15 | rpsqrtcld 13473 |
. . . . . . . . 9
 

      |
156 | 155 | rpcnd 11343 |
. . . . . . . 8
 

      |
157 | | mulcl 9623 |
. . . . . . . 8
               |
158 | 154, 156,
157 | sylancr 669 |
. . . . . . 7
 

        |
159 | 143 | rprecred 11352 |
. . . . . . . . . 10
            
        |
160 | 1, 159 | fsumrecl 13800 |
. . . . . . . . 9
 

                  |
161 | 160 | recnd 9669 |
. . . . . . . 8
 

                  |
162 | 161, 158 | subcld 9986 |
. . . . . . 7
 

 
                        |
163 | | 2re 10679 |
. . . . . . . . . . 11
 |
164 | | dchrisum0.c |
. . . . . . . . . . . . 13
      |
165 | | elrege0 11738 |
. . . . . . . . . . . . 13
   
    |
166 | 164, 165 | sylib 200 |
. . . . . . . . . . . 12
 
   |
167 | 166 | simpld 461 |
. . . . . . . . . . 11
   |
168 | | remulcl 9624 |
. . . . . . . . . . 11
 
     |
169 | 163, 167,
168 | sylancr 669 |
. . . . . . . . . 10
     |
170 | 169 | adantr 467 |
. . . . . . . . 9
 

    |
171 | 170, 155 | rerpdivcld 11369 |
. . . . . . . 8
 

          |
172 | 171 | recnd 9669 |
. . . . . . 7
 

          |
173 | 158, 162,
172 | adddird 9668 |
. . . . . 6
 

                                                             
                                  |
174 | 158, 161 | pncan3d 9989 |
. . . . . . 7
 

                                                  |
175 | 174 | oveq1d 6305 |
. . . . . 6
 

                                                                      |
176 | | 2cnd 10682 |
. . . . . . . . 9
 

  |
177 | 176, 156,
172 | mulassd 9666 |
. . . . . . . 8
 

                                  |
178 | 170 | recnd 9669 |
. . . . . . . . . 10
 

    |
179 | 155 | rpne0d 11346 |
. . . . . . . . . 10
 

      |
180 | 178, 156,
179 | divcan2d 10385 |
. . . . . . . . 9
 

                  |
181 | 180 | oveq2d 6306 |
. . . . . . . 8
 

                      |
182 | 177, 181 | eqtrd 2485 |
. . . . . . 7
 

                      |
183 | 182 | oveq1d 6305 |
. . . . . 6
 

                                                                                              |
184 | 173, 175,
183 | 3eqtr3d 2493 |
. . . . 5
 

 
                               
                                  |
185 | 184 | mpteq2dva 4489 |
. . . 4
                                                                         |
186 | | remulcl 9624 |
. . . . . . . 8
           |
187 | 163, 169,
186 | sylancr 669 |
. . . . . . 7
       |
188 | 187 | recnd 9669 |
. . . . . 6
       |
189 | 188 | adantr 467 |
. . . . 5
 

      |
190 | 162, 172 | mulcld 9663 |
. . . . 5
 

                                    |
191 | | rpssre 11312 |
. . . . . 6
 |
192 | | o1const 13683 |
. . . . . 6
                  |
193 | 191, 188,
192 | sylancr 669 |
. . . . 5
            |
194 | | eqid 2451 |
. . . . . . . 8

 
                         
                        |
195 | 194 | divsqrsum 23907 |
. . . . . . 7

 
                         |
196 | | rlimdmo1 13681 |
. . . . . . 7
   
                                                       |
197 | 195, 196 | mp1i 13 |
. . . . . 6
                                |
198 | 178, 156,
179 | divrecd 10386 |
. . . . . . . . 9
 

                    |
199 | 198 | mpteq2dva 4489 |
. . . . . . . 8
           
             |
200 | 155 | rprecred 11352 |
. . . . . . . . 9
 

        |
201 | 169 | recnd 9669 |
. . . . . . . . . 10
     |
202 | | rlimconst 13608 |
. . . . . . . . . 10
              |
203 | 191, 201,
202 | sylancr 669 |
. . . . . . . . 9
          |
204 | | sqrtlim 23898 |
. . . . . . . . . 10

         |
205 | 204 | a1i 11 |
. . . . . . . . 9
            |
206 | 170, 200,
203, 205 | rlimmul 13708 |
. . . . . . . 8
                    |
207 | 199, 206 | eqbrtrd 4423 |
. . . . . . 7
                  |
208 | | rlimo1 13680 |
. . . . . . 7
                               |
209 | 207, 208 | syl 17 |
. . . . . 6
                |
210 | 162, 172,
197, 209 | o1mul2 13688 |
. . . . 5
                                          |
211 | 189, 190,
193, 210 | o1add2 13687 |
. . . 4
                                                |
212 | 185, 211 | eqeltrd 2529 |
. . 3
                                  |
213 | 160, 171 | remulcld 9671 |
. . 3
 

 
                          |
214 | 3, 149 | fsumcl 13799 |
. . . 4
            
                                            |
215 | 1, 214 | fsumcl 13799 |
. . 3
 

          
                                           |
216 | 215 | abscld 13498 |
. . . . 5
 

             
                                            |
217 | 213 | recnd 9669 |
. . . . . 6
 

 
                          |
218 | 217 | abscld 13498 |
. . . . 5
 

                                |
219 | 214 | abscld 13498 |
. . . . . . 7
            
   
                                            |
220 | 1, 219 | fsumrecl 13800 |
. . . . . 6
 

                                                          |
221 | 1, 214 | fsumabs 13861 |
. . . . . 6
 

             
                                         
                                                          |
222 | 171 | adantr 467 |
. . . . . . . . 9
            
          |
223 | 159, 222 | remulcld 9671 |
. . . . . . . 8
            
                  |
224 | 119, 140 | syldan 473 |
. . . . . . . . . . . 12
   

                             
                |
225 | 3, 224 | fsumcl 13799 |
. . . . . . . . . . 11
            
                                      |
226 | 225 | abscld 13498 |
. . . . . . . . . 10
            
   
                                      |
227 | | rpvmasum.a |
. . . . . . . . . . 11
   |
228 | | rpvmasum2.1 |
. . . . . . . . . . 11
     |
229 | | dchrisum0lem1.f |
. . . . . . . . . . 11
                 |
230 | | dchrisum0.s |
. . . . . . . . . . 11
      |
231 | | dchrisum0.1 |
. . . . . . . . . . 11
                     
        |
232 | 121, 123,
227, 120, 122, 228, 124, 127, 229, 164, 230, 231 | dchrisum0lem1b 24353 |
. . . . . . . . . 10
            
   
                                              |
233 | 226, 222,
143, 232 | lediv1dd 11396 |
. . . . . . . . 9
            
                                                              |
234 | 143 | rpcnd 11343 |
. . . . . . . . . . 11
            
      |
235 | 143 | rpne0d 11346 |
. . . . . . . . . . 11
            
      |
236 | 225, 234,
235 | absdivd 13517 |
. . . . . . . . . 10
            
                                                                                                  |
237 | 3, 234, 224, 235 | fsumdivc 13847 |
. . . . . . . . . . 11
            
                                                                                      |
238 | 237 | fveq2d 5869 |
. . . . . . . . . 10
            
                                                                                              |
239 | 143 | rprege0d 11348 |
. . . . . . . . . . . 12
            
            |
240 | | absid 13359 |
. . . . . . . . . . . 12
                         |
241 | 239, 240 | syl 17 |
. . . . . . . . . . 11
            
              |
242 | 241 | oveq2d 6306 |
. . . . . . . . . 10
            
                                                                                                  |
243 | 236, 238,
242 | 3eqtr3rd 2494 |
. . . . . . . . 9
            
                                                                                              |
244 | 172 | adantr 467 |
. . . . . . . . . 10
            
          |
245 | 244, 234,
235 | divrec2d 10387 |
. . . . . . . . 9
            
                                |
246 | 233, 243,
245 | 3brtr3d 4432 |
. . . . . . . 8
            
   
                                         
                  |
247 | 1, 219, 223, 246 | fsumle 13859 |
. . . . . . 7
 

                                                                                    |
248 | 159 | recnd 9669 |
. . . . . . . 8
            
        |
249 | 1, 172, 248 | fsummulc1 13846 |
. . . . . . 7
 

 
                                                    |
250 | 247, 249 | breqtrrd 4429 |
. . . . . 6
 

                                                                                    |
251 | 216, 220,
213, 221, 250 | letrd 9792 |
. . . . 5
 

             
                                         
 
                          |
252 | 213 | leabsd 13476 |
. . . . 5
 

 
                       
                                |
253 | 216, 213,
218, 251, 252 | letrd 9792 |
. . . 4
 

             
                                         
                                |
254 | 253 | adantrr 723 |
. . 3
 
      
                                                                                    |
255 | 153, 212,
213, 215, 254 | o1le 13716 |
. 2
                                                            |
256 | 152, 255 | eqeltrrd 2530 |
1
                      
                                         |