Step | Hyp | Ref
| Expression |
1 | | fzfid 12224 |
. . . 4
       |
2 | | pire 23492 |
. . . . . . . 8
 |
3 | | basellem8.n |
. . . . . . . . 9
     |
4 | | 2nn 10790 |
. . . . . . . . . . 11
 |
5 | | nnmulcl 10654 |
. . . . . . . . . . 11
 
     |
6 | 4, 5 | mpan 684 |
. . . . . . . . . 10
     |
7 | 6 | peano2nnd 10648 |
. . . . . . . . 9
       |
8 | 3, 7 | syl5eqel 2553 |
. . . . . . . 8
   |
9 | | nndivre 10667 |
. . . . . . . 8
 
     |
10 | 2, 8, 9 | sylancr 676 |
. . . . . . 7
 
   |
11 | 10 | resqcld 12480 |
. . . . . 6
         |
12 | 11 | adantr 472 |
. . . . 5
 
             |
13 | 3 | basellem1 24086 |
. . . . . . . 8
 
                 |
14 | | tanrpcl 23538 |
. . . . . . . 8
        
 
          |
15 | 13, 14 | syl 17 |
. . . . . . 7
 
               |
16 | 15 | rpred 11364 |
. . . . . 6
 
               |
17 | 15 | rpne0d 11369 |
. . . . . 6
 
               |
18 | | 2z 10993 |
. . . . . . . 8
 |
19 | | znegcl 10996 |
. . . . . . . 8
    |
20 | 18, 19 | ax-mp 5 |
. . . . . . 7
  |
21 | 20 | a1i 11 |
. . . . . 6
 
        |
22 | 16, 17, 21 | reexpclzd 12479 |
. . . . 5
 
                    |
23 | 12, 22 | remulcld 9689 |
. . . 4
 
                            |
24 | | elfznn 11854 |
. . . . . . 7
       |
25 | 24 | adantl 473 |
. . . . . 6
 
       |
26 | 25 | nnred 10646 |
. . . . 5
 
       |
27 | 25 | nnne0d 10676 |
. . . . 5
 
       |
28 | 26, 27, 21 | reexpclzd 12479 |
. . . 4
 
            |
29 | 16 | recnd 9687 |
. . . . . . . 8
 
               |
30 | | 2nn0 10910 |
. . . . . . . 8
 |
31 | | expneg 12318 |
. . . . . . . 8
                                        |
32 | 29, 30, 31 | sylancl 675 |
. . . . . . 7
 
                                  |
33 | 32 | oveq2d 6324 |
. . . . . 6
 
                                                  |
34 | 10 | recnd 9687 |
. . . . . . . . 9
 
   |
35 | 34 | sqcld 12452 |
. . . . . . . 8
         |
36 | 35 | adantr 472 |
. . . . . . 7
 
             |
37 | | rpexpcl 12329 |
. . . . . . . . . 10
         
               |
38 | 15, 18, 37 | sylancl 675 |
. . . . . . . . 9
 
                   |
39 | 38 | rpred 11364 |
. . . . . . . 8
 
                   |
40 | 39 | recnd 9687 |
. . . . . . 7
 
                   |
41 | 38 | rpne0d 11369 |
. . . . . . 7
 
                   |
42 | 36, 40, 41 | divrecd 10408 |
. . . . . 6
 
                                                 |
43 | 33, 42 | eqtr4d 2508 |
. . . . 5
 
                                                |
44 | 25 | nnrpd 11362 |
. . . . . . 7
 
       |
45 | | rpexpcl 12329 |
. . . . . . 7
           |
46 | 44, 20, 45 | sylancl 675 |
. . . . . 6
 
            |
47 | | 2cn 10702 |
. . . . . . . . . . . 12
 |
48 | 47 | negnegi 9964 |
. . . . . . . . . . 11
   |
49 | 48 | oveq2i 6319 |
. . . . . . . . . 10
           |
50 | 25 | nncnd 10647 |
. . . . . . . . . . 11
 
       |
51 | 50, 27, 21 | expnegd 12461 |
. . . . . . . . . 10
 
                    |
52 | 49, 51 | syl5reqr 2520 |
. . . . . . . . 9
 
                  |
53 | 52 | oveq1d 6323 |
. . . . . . . 8
 
                                  |
54 | | nncn 10639 |
. . . . . . . . . . 11
   |
55 | | nnne0 10664 |
. . . . . . . . . . 11
   |
56 | 20 | a1i 11 |
. . . . . . . . . . 11
    |
57 | 54, 55, 56 | expclzd 12459 |
. . . . . . . . . 10
        |
58 | 25, 57 | syl 17 |
. . . . . . . . 9
 
            |
59 | 50, 27, 21 | expne0d 12460 |
. . . . . . . . 9
 
            |
60 | 36, 58, 59 | divrec2d 10409 |
. . . . . . . 8
 
                                   |
61 | 2 | recni 9673 |
. . . . . . . . . . . 12
 |
62 | 61 | a1i 11 |
. . . . . . . . . . 11
 
       |
63 | 8 | nncnd 10647 |
. . . . . . . . . . . . 13
   |
64 | 8 | nnne0d 10676 |
. . . . . . . . . . . . 13
   |
65 | 63, 64 | jca 541 |
. . . . . . . . . . . 12
 
   |
66 | 65 | adantr 472 |
. . . . . . . . . . 11
 
         |
67 | | divass 10310 |
. . . . . . . . . . 11
  
            |
68 | 50, 62, 66, 67 | syl3anc 1292 |
. . . . . . . . . 10
 
               |
69 | 68 | oveq1d 6323 |
. . . . . . . . 9
 
               
       |
70 | 34 | adantr 472 |
. . . . . . . . . 10
 
         |
71 | 50, 70 | sqmuld 12466 |
. . . . . . . . 9
 
                           |
72 | 69, 71 | eqtrd 2505 |
. . . . . . . 8
 
                           |
73 | 53, 60, 72 | 3eqtr4d 2515 |
. . . . . . 7
 
                            |
74 | | elioore 11691 |
. . . . . . . . . 10
        
 
      |
75 | 13, 74 | syl 17 |
. . . . . . . . 9
 
           |
76 | 75 | resqcld 12480 |
. . . . . . . 8
 
               |
77 | | tangtx 23539 |
. . . . . . . . . 10
        
 
              |
78 | 13, 77 | syl 17 |
. . . . . . . . 9
 
                   |
79 | | eliooord 11719 |
. . . . . . . . . . . . . 14
        
 
              |
80 | 13, 79 | syl 17 |
. . . . . . . . . . . . 13
 
         
         |
81 | 80 | simpld 466 |
. . . . . . . . . . . 12
 
           |
82 | 75, 81 | elrpd 11361 |
. . . . . . . . . . 11
 
           |
83 | 82 | rpge0d 11368 |
. . . . . . . . . 10
 
           |
84 | 15 | rpge0d 11368 |
. . . . . . . . . 10
 
               |
85 | 75, 16, 83, 84 | lt2sqd 12488 |
. . . . . . . . 9
 
                                         |
86 | 78, 85 | mpbid 215 |
. . . . . . . 8
 
                           |
87 | 76, 39, 86 | ltled 9800 |
. . . . . . 7
 
                           |
88 | 73, 87 | eqbrtrd 4416 |
. . . . . 6
 
                                |
89 | 12, 46, 38, 88 | lediv23d 11427 |
. . . . 5
 
                                |
90 | 43, 89 | eqbrtrd 4416 |
. . . 4
 
                         
       |
91 | 1, 23, 28, 90 | fsumle 13936 |
. . 3
                           
             |
92 | | oveq2 6316 |
. . . . . . . . . . 11
       |
93 | 92 | oveq1d 6323 |
. . . . . . . . . 10
           |
94 | 93, 3 | syl6eqr 2523 |
. . . . . . . . 9
       |
95 | 94 | oveq2d 6324 |
. . . . . . . 8
           |
96 | 95 | oveq2d 6324 |
. . . . . . 7
               |
97 | 96 | oveq2d 6324 |
. . . . . 6
                               |
98 | 95 | oveq2d 6324 |
. . . . . . 7
                 |
99 | 98 | oveq2d 6324 |
. . . . . 6
                     |
100 | 97, 99 | oveq12d 6326 |
. . . . 5
                                                     |
101 | | basel.j |
. . . . . 6
                   |
102 | | nnex 10637 |
. . . . . . . . 9
 |
103 | 102 | a1i 11 |
. . . . . . . 8
  |
104 | | ovex 6336 |
. . . . . . . . 9
                 |
105 | 104 | a1i 11 |
. . . . . . . 8
                    |
106 | | ovex 6336 |
. . . . . . . . 9
            |
107 | 106 | a1i 11 |
. . . . . . . 8
               |
108 | | basel.h |
. . . . . . . . 9
                     |
109 | 2 | resqcli 12398 |
. . . . . . . . . . . 12
     |
110 | | 6re 10712 |
. . . . . . . . . . . 12
 |
111 | | 6nn 10794 |
. . . . . . . . . . . . 13
 |
112 | 111 | nnne0i 10666 |
. . . . . . . . . . . 12
 |
113 | 109, 110,
112 | redivcli 10396 |
. . . . . . . . . . 11
       |
114 | 113 | a1i 11 |
. . . . . . . . . 10
          |
115 | | ovex 6336 |
. . . . . . . . . . 11
         |
116 | 115 | a1i 11 |
. . . . . . . . . 10
            |
117 | | fconstmpt 4883 |
. . . . . . . . . . 11
                   |
118 | 117 | a1i 11 |
. . . . . . . . . 10
                    |
119 | | 1zzd 10992 |
. . . . . . . . . . 11
    |
120 | | ovex 6336 |
. . . . . . . . . . . 12
       |
121 | 120 | a1i 11 |
. . . . . . . . . . 11
          |
122 | | fconstmpt 4883 |
. . . . . . . . . . . 12
       |
123 | 122 | a1i 11 |
. . . . . . . . . . 11
        |
124 | | basel.g |
. . . . . . . . . . . 12
         |
125 | 124 | a1i 11 |
. . . . . . . . . . 11
          |
126 | 103, 119,
121, 123, 125 | offval2 6567 |
. . . . . . . . . 10
                   |
127 | 103, 114,
116, 118, 126 | offval2 6567 |
. . . . . . . . 9
                                        |
128 | 108, 127 | syl5eq 2517 |
. . . . . . . 8
                    |
129 | | ovex 6336 |
. . . . . . . . . 10
          |
130 | 129 | a1i 11 |
. . . . . . . . 9
             |
131 | 47 | negcli 9962 |
. . . . . . . . . . 11
  |
132 | 131 | a1i 11 |
. . . . . . . . . 10
     |
133 | | fconstmpt 4883 |
. . . . . . . . . . 11
         |
134 | 133 | a1i 11 |
. . . . . . . . . 10
          |
135 | 103, 132,
121, 134, 125 | offval2 6567 |
. . . . . . . . 9
                     |
136 | 103, 119,
130, 123, 135 | offval2 6567 |
. . . . . . . 8
                              |
137 | 103, 105,
107, 128, 136 | offval2 6567 |
. . . . . . 7
                                                   |
138 | 137 | trud 1461 |
. . . . . 6
                                                  |
139 | 101, 138 | eqtri 2493 |
. . . . 5
                                |
140 | | ovex 6336 |
. . . . 5
                      |
141 | 100, 139,
140 | fvmpt 5963 |
. . . 4
                            |
142 | 113 | recni 9673 |
. . . . . . . 8
       |
143 | 142 | a1i 11 |
. . . . . . 7
         |
144 | 6 | nncnd 10647 |
. . . . . . . 8
     |
145 | 144, 63, 64 | divcld 10405 |
. . . . . . 7
       |
146 | | ax-1cn 9615 |
. . . . . . . . 9
 |
147 | | subcl 9894 |
. . . . . . . . 9
   
       |
148 | 144, 146,
147 | sylancl 675 |
. . . . . . . 8
       |
149 | 148, 63, 64 | divcld 10405 |
. . . . . . 7
         |
150 | 143, 145,
149 | mulassd 9684 |
. . . . . 6
                                           |
151 | | 1cnd 9677 |
. . . . . . . . . 10
   |
152 | 63, 151, 63, 64 | divsubdird 10444 |
. . . . . . . . 9
             |
153 | 3 | oveq1i 6318 |
. . . . . . . . . . 11
         |
154 | | pncan 9901 |
. . . . . . . . . . . 12
   
           |
155 | 144, 146,
154 | sylancl 675 |
. . . . . . . . . . 11
           |
156 | 153, 155 | syl5eq 2517 |
. . . . . . . . . 10
 
     |
157 | 156 | oveq1d 6323 |
. . . . . . . . 9
           |
158 | 63, 64 | dividd 10403 |
. . . . . . . . . 10
     |
159 | 158 | oveq1d 6323 |
. . . . . . . . 9
             |
160 | 152, 157,
159 | 3eqtr3rd 2514 |
. . . . . . . 8
           |
161 | 160 | oveq2d 6324 |
. . . . . . 7
                           |
162 | 131 | a1i 11 |
. . . . . . . . 9
    |
163 | 63, 162, 63, 64 | divdird 10443 |
. . . . . . . 8
               |
164 | | negsub 9942 |
. . . . . . . . . . 11
 
        |
165 | 63, 47, 164 | sylancl 675 |
. . . . . . . . . 10
 
      |
166 | | df-2 10690 |
. . . . . . . . . . . 12
   |
167 | 3, 166 | oveq12i 6320 |
. . . . . . . . . . 11
           |
168 | 144, 151,
151 | pnpcan2d 10043 |
. . . . . . . . . . 11
               |
169 | 167, 168 | syl5eq 2517 |
. . . . . . . . . 10
 
       |
170 | 165, 169 | eqtrd 2505 |
. . . . . . . . 9
 
        |
171 | 170 | oveq1d 6323 |
. . . . . . . 8
              |
172 | 162, 63, 64 | divrecd 10408 |
. . . . . . . . 9
           |
173 | 158, 172 | oveq12d 6326 |
. . . . . . . 8
                 |
174 | 163, 171,
173 | 3eqtr3rd 2514 |
. . . . . . 7
                |
175 | 161, 174 | oveq12d 6326 |
. . . . . 6
                                            |
176 | 8 | nnsqcld 12474 |
. . . . . . . . . . 11
       |
177 | 176 | nncnd 10647 |
. . . . . . . . . 10
       |
178 | | 6cn 10713 |
. . . . . . . . . 10
 |
179 | | mulcom 9643 |
. . . . . . . . . 10
     
               |
180 | 177, 178,
179 | sylancl 675 |
. . . . . . . . 9
               |
181 | 180 | oveq2d 6324 |
. . . . . . . 8
                                               |
182 | 109 | recni 9673 |
. . . . . . . . . 10
     |
183 | 182 | a1i 11 |
. . . . . . . . 9
       |
184 | 144, 148 | mulcld 9681 |
. . . . . . . . 9
           |
185 | 176 | nnne0d 10676 |
. . . . . . . . . 10
       |
186 | 177, 185 | jca 541 |
. . . . . . . . 9
             |
187 | 178, 112 | pm3.2i 462 |
. . . . . . . . . 10
   |
188 | 187 | a1i 11 |
. . . . . . . . 9
     |
189 | | divmuldiv 10329 |
. . . . . . . . 9
                              
                                              |
190 | 183, 184,
186, 188, 189 | syl22anc 1293 |
. . . . . . . 8
                                               |
191 | | divmuldiv 10329 |
. . . . . . . . 9
                              
                                              |
192 | 183, 184,
188, 186, 191 | syl22anc 1293 |
. . . . . . . 8
                                               |
193 | 181, 190,
192 | 3eqtr4d 2515 |
. . . . . . 7
                                               |
194 | 61 | a1i 11 |
. . . . . . . . 9
   |
195 | 194, 63, 64 | sqdivd 12467 |
. . . . . . . 8
                   |
196 | 195 | oveq1d 6323 |
. . . . . . 7
                                           |
197 | 144, 63, 148, 63, 64, 64 | divmuldivd 10446 |
. . . . . . . . 9
                           |
198 | 63 | sqvald 12451 |
. . . . . . . . . 10
         |
199 | 198 | oveq2d 6324 |
. . . . . . . . 9
                             |
200 | 197, 199 | eqtr4d 2508 |
. . . . . . . 8
                             |
201 | 200 | oveq2d 6324 |
. . . . . . 7
                                             |
202 | 193, 196,
201 | 3eqtr4d 2515 |
. . . . . 6
                                         |
203 | 150, 175,
202 | 3eqtr4d 2515 |
. . . . 5
                                          |
204 | | eqid 2471 |
. . . . . . 7
                                                       |
205 | | eqid 2471 |
. . . . . . 7
                                       |
206 | 3, 204, 205 | basellem5 24090 |
. . . . . 6
                                |
207 | 206 | oveq2d 6324 |
. . . . 5
                                                |
208 | 203, 207 | eqtr4d 2508 |
. . . 4
                                                   |
209 | 22 | recnd 9687 |
. . . . 5
 
                    |
210 | 1, 35, 209 | fsummulc2 13922 |
. . . 4
                            
                            |
211 | 141, 208,
210 | 3eqtrd 2509 |
. . 3
                                  |
212 | | oveq1 6315 |
. . . . . . 7
             |
213 | | eqid 2471 |
. . . . . . 7
               |
214 | | ovex 6336 |
. . . . . . 7
      |
215 | 212, 213,
214 | fvmpt 5963 |
. . . . . 6
                   |
216 | 25, 215 | syl 17 |
. . . . 5
 
                       |
217 | | id 22 |
. . . . . 6
   |
218 | | nnuz 11218 |
. . . . . 6
     |
219 | 217, 218 | syl6eleq 2559 |
. . . . 5
       |
220 | 216, 219,
58 | fsumser 13873 |
. . . 4
                           |
221 | | basel.f |
. . . . 5
           |
222 | 221 | fveq1i 5880 |
. . . 4
                  |
223 | 220, 222 | syl6reqr 2524 |
. . 3
                  |
224 | 91, 211, 223 | 3brtr4d 4426 |
. 2
           |
225 | 75 | resincld 14274 |
. . . . . 6
 
               |
226 | | sincosq1sgn 23532 |
. . . . . . . . 9
        
 
                    |
227 | 13, 226 | syl 17 |
. . . . . . . 8
 
                         |
228 | 227 | simpld 466 |
. . . . . . 7
 
               |
229 | 228 | gt0ne0d 10199 |
. . . . . 6
 
               |
230 | 225, 229,
21 | reexpclzd 12479 |
. . . . 5
 
                    |
231 | 12, 230 | remulcld 9689 |
. . . 4
 
                            |
232 | | sinltx 14320 |
. . . . . . . . . 10
                   |
233 | 82, 232 | syl 17 |
. . . . . . . . 9
 
                   |
234 | 225, 75, 233 | ltled 9800 |
. . . . . . . 8
 
                   |
235 | | 0re 9661 |
. . . . . . . . . . 11
 |
236 | | ltle 9740 |
. . . . . . . . . . 11
                   
           |
237 | 235, 225,
236 | sylancr 676 |
. . . . . . . . . 10
 
                         |
238 | 228, 237 | mpd 15 |
. . . . . . . . 9
 
               |
239 | 225, 75, 238, 83 | le2sqd 12489 |
. . . . . . . 8
 
                 
                       |
240 | 234, 239 | mpbid 215 |
. . . . . . 7
 
                
          |
241 | 240, 73 | breqtrrd 4422 |
. . . . . 6
 
                
               |
242 | 225 | resqcld 12480 |
. . . . . . . 8
 
                   |
243 | 242, 12, 46 | lemuldiv2d 11411 |
. . . . . . 7
 
                              
                            |
244 | 225, 228 | elrpd 11361 |
. . . . . . . . 9
 
               |
245 | | rpexpcl 12329 |
. . . . . . . . 9
         
               |
246 | 244, 18, 245 | sylancl 675 |
. . . . . . . 8
 
                   |
247 | 28, 12, 246 | lemuldivd 11410 |
. . . . . . 7
 
                              
                            |
248 | 243, 247 | bitr3d 263 |
. . . . . 6
 
                              
                            |
249 | 241, 248 | mpbid 215 |
. . . . 5
 
                                |
250 | 225 | recnd 9687 |
. . . . . . . 8
 
               |
251 | | expneg 12318 |
. . . . . . . 8
                                        |
252 | 250, 30, 251 | sylancl 675 |
. . . . . . 7
 
                                  |
253 | 252 | oveq2d 6324 |
. . . . . 6
 
                                                  |
254 | 242 | recnd 9687 |
. . . . . . 7
 
                   |
255 | 246 | rpne0d 11369 |
. . . . . . 7
 
                   |
256 | 36, 254, 255 | divrecd 10408 |
. . . . . 6
 
                                                 |
257 | 253, 256 | eqtr4d 2508 |
. . . . 5
 
                                                |
258 | 249, 257 | breqtrrd 4422 |
. . . 4
 
                                 |
259 | 1, 28, 231, 258 | fsumle 13936 |
. . 3
                                         |
260 | 95 | oveq2d 6324 |
. . . . . 6
               |
261 | 97, 260 | oveq12d 6326 |
. . . . 5
                                               |
262 | | basel.k |
. . . . . 6
           |
263 | | ovex 6336 |
. . . . . . . . 9
         |
264 | 263 | a1i 11 |
. . . . . . . 8
            |
265 | 103, 119,
121, 123, 125 | offval2 6567 |
. . . . . . . 8
                   |
266 | 103, 105,
264, 128, 265 | offval2 6567 |
. . . . . . 7
                                        |
267 | 266 | trud 1461 |
. . . . . 6
                                       |
268 | 262, 267 | eqtri 2493 |
. . . . 5
                             |
269 | | ovex 6336 |
. . . . 5
                   |
270 | 261, 268,
269 | fvmpt 5963 |
. . . 4
                         |
271 | | peano2cn 9823 |
. . . . . . . 8
 
   |
272 | 63, 271 | syl 17 |
. . . . . . 7
 
   |
273 | 272, 63, 64 | divcld 10405 |
. . . . . 6
       |
274 | 143, 145,
273 | mulassd 9684 |
. . . . 5
                                       |
275 | 63, 151, 63, 64 | divdird 10443 |
. . . . . . 7
             |
276 | 158 | oveq1d 6323 |
. . . . . . 7
             |
277 | 275, 276 | eqtr2d 2506 |
. . . . . 6
           |
278 | 161, 277 | oveq12d 6326 |
. . . . 5
                                       |
279 | 180 | oveq2d 6324 |
. . . . . . 7
                                           |
280 | 144, 272 | mulcld 9681 |
. . . . . . . 8
         |
281 | | divmuldiv 10329 |
. . . . . . . 8
          
                 
                             
            |
282 | 183, 280,
186, 188, 281 | syl22anc 1293 |
. . . . . . 7
                              
            |
283 | | divmuldiv 10329 |
. . . . . . . 8
          
                 
                             
            |
284 | 183, 280,
188, 186, 283 | syl22anc 1293 |
. . . . . . 7
                                           |
285 | 279, 282,
284 | 3eqtr4d 2515 |
. . . . . 6
                                
          |
286 | 75 | recoscld 14275 |
. . . . . . . . . . . . . . 15
 
               |
287 | 286 | recnd 9687 |
. . . . . . . . . . . . . 14
 
               |
288 | 287 | sqcld 12452 |
. . . . . . . . . . . . 13
 
                   |
289 | 254, 288,
254, 255 | divdird 10443 |
. . . . . . . . . . . 12
 
                                                                                                     |
290 | 75 | recnd 9687 |
. . . . . . . . . . . . . 14
 
           |
291 | | sincossq 14307 |
. . . . . . . . . . . . . 14
    
                            |
292 | 290, 291 | syl 17 |
. . . . . . . . . . . . 13
 
                                 |
293 | 292 | oveq1d 6323 |
. . . . . . . . . . . 12
 
                                                             |
294 | 254, 255 | dividd 10403 |
. . . . . . . . . . . . 13
 
                                 |
295 | 227 | simprd 470 |
. . . . . . . . . . . . . . . . . . 19
 
               |
296 | 295 | gt0ne0d 10199 |
. . . . . . . . . . . . . . . . . 18
 
               |
297 | | tanval 14259 |
. . . . . . . . . . . . . . . . . 18
                                           |
298 | 290, 296,
297 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
 
                                 |
299 | 298 | oveq1d 6323 |
. . . . . . . . . . . . . . . 16
 
                                         |
300 | 250, 287,
296 | sqdivd 12467 |
. . . . . . . . . . . . . . . 16
 
                                                       |
301 | 299, 300 | eqtrd 2505 |
. . . . . . . . . . . . . . 15
 
                                             |
302 | 301 | oveq2d 6324 |
. . . . . . . . . . . . . 14
 
                                                 |
303 | | sqne0 12379 |
. . . . . . . . . . . . . . . . 17
                                 |
304 | 287, 303 | syl 17 |
. . . . . . . . . . . . . . . 16
 
                             |
305 | 296, 304 | mpbird 240 |
. . . . . . . . . . . . . . 15
 
                   |
306 | 254, 288,
255, 305 | recdivd 10422 |
. . . . . . . . . . . . . 14
 
                                                             |
307 | 32, 302, 306 | 3eqtrrd 2510 |
. . . . . . . . . . . . 13
 
                                              |
308 | 294, 307 | oveq12d 6326 |
. . . . . . . . . . . 12
 
                                                                            |
309 | 289, 293,
308 | 3eqtr3d 2513 |
. . . . . . . . . . 11
 
                                    |
310 | | addcom 9837 |
. . . . . . . . . . . 12
                                                |
311 | 146, 209,
310 | sylancr 676 |
. . . . . . . . . . 11
 
                                     |
312 | 252, 309,
311 | 3eqtrd 2509 |
. . . . . . . . . 10
 
                                   |
313 | 312 | sumeq2dv 13846 |
. . . . . . . . 9
                                           |
314 | | 1cnd 9677 |
. . . . . . . . . 10
 
       |
315 | 1, 209, 314 | fsumadd 13882 |
. . . . . . . . 9
                                                   |
316 | | fsumconst 13928 |
. . . . . . . . . . . 12
     
                   |
317 | 1, 146, 316 | sylancl 675 |
. . . . . . . . . . 11
                   |
318 | | nnnn0 10900 |
. . . . . . . . . . . . 13
   |
319 | | hashfz1 12567 |
. . . . . . . . . . . . 13

          |
320 | 318, 319 | syl 17 |
. . . . . . . . . . . 12
           |
321 | 320 | oveq1d 6323 |
. . . . . . . . . . 11
               |
322 | | nncn 10639 |
. . . . . . . . . . . 12
   |
323 | 322 | mulid1d 9678 |
. . . . . . . . . . 11
 
   |
324 | 317, 321,
323 | 3eqtrd 2509 |
. . . . . . . . . 10
         |
325 | 206, 324 | oveq12d 6326 |
. . . . . . . . 9
                                          |
326 | 313, 315,
325 | 3eqtrd 2509 |
. . . . . . . 8
                                  |
327 | | 3cn 10706 |
. . . . . . . . . . . . 13
 |
328 | 327 | a1i 11 |
. . . . . . . . . . . 12
   |
329 | 144, 148,
328 | adddid 9685 |
. . . . . . . . . . 11
                           |
330 | | df-3 10691 |
. . . . . . . . . . . . . . . . 17
   |
331 | 330 | oveq1i 6318 |
. . . . . . . . . . . . . . . 16
       |
332 | 47, 146 | pncan3oi 9911 |
. . . . . . . . . . . . . . . 16
     |
333 | 331, 332,
166 | 3eqtri 2497 |
. . . . . . . . . . . . . . 15
     |
334 | 333 | oveq2i 6319 |
. . . . . . . . . . . . . 14
             |
335 | 144, 151,
328 | subadd23d 10027 |
. . . . . . . . . . . . . 14
               |
336 | 144, 151,
151 | addassd 9683 |
. . . . . . . . . . . . . 14
               |
337 | 334, 335,
336 | 3eqtr4a 2531 |
. . . . . . . . . . . . 13
               |
338 | 3 | oveq1i 6318 |
. . . . . . . . . . . . 13
         |
339 | 337, 338 | syl6eqr 2523 |
. . . . . . . . . . . 12
           |
340 | 339 | oveq2d 6324 |
. . . . . . . . . . 11
                   |
341 | | 2cnd 10704 |
. . . . . . . . . . . . . 14
   |
342 | 341, 322,
328 | mul32d 9861 |
. . . . . . . . . . . . 13
           |
343 | | 3t2e6 10784 |
. . . . . . . . . . . . . . 15
   |
344 | 327, 47 | mulcomi 9667 |
. . . . . . . . . . . . . . 15
     |
345 | 343, 344 | eqtr3i 2495 |
. . . . . . . . . . . . . 14
   |
346 | 345 | oveq1i 6318 |
. . . . . . . . . . . . 13
       |
347 | 342, 346 | syl6eqr 2523 |
. . . . . . . . . . . 12
         |
348 | 347 | oveq2d 6324 |
. . . . . . . . . . 11
                             |
349 | 329, 340,
348 | 3eqtr3d 2513 |
. . . . . . . . . 10
                     |
350 | 349 | oveq1d 6323 |
. . . . . . . . 9
     
                   |
351 | | mulcl 9641 |
. . . . . . . . . . 11
 
     |
352 | 178, 322,
351 | sylancr 676 |
. . . . . . . . . 10
     |
353 | 178 | a1i 11 |
. . . . . . . . . 10
   |
354 | 112 | a1i 11 |
. . . . . . . . . 10
   |
355 | 184, 352,
353, 354 | divdird 10443 |
. . . . . . . . 9
                                 |
356 | 322, 353,
354 | divcan3d 10410 |
. . . . . . . . . 10
       |
357 | 356 | oveq2d 6324 |
. . . . . . . . 9
                               |
358 | 350, 355,
357 | 3eqtrd 2509 |
. . . . . . . 8
     
                 |
359 | 326, 358 | eqtr4d 2508 |
. . . . . . 7
                              |
360 | 195, 359 | oveq12d 6326 |
. . . . . 6
                                                  |
361 | 144, 63, 272, 63, 64, 64 | divmuldivd 10446 |
. . . . . . . 8
                       |
362 | 198 | oveq2d 6324 |
. . . . . . . 8
     
                   |
363 | 361, 362 | eqtr4d 2508 |
. . . . . . 7
                         |
364 | 363 | oveq2d 6324 |
. . . . . 6
                                         |
365 | 285, 360,
364 | 3eqtr4d 2515 |
. . . . 5
                                                |
366 | 274, 278,
365 | 3eqtr4d 2515 |
. . . 4
                                                |
367 | 230 | recnd 9687 |
. . . . 5
 
                    |
368 | 1, 35, 367 | fsummulc2 13922 |
. . . 4
                            
                            |
369 | 270, 366,
368 | 3eqtrd 2509 |
. . 3
                                  |
370 | 259, 223,
369 | 3brtr4d 4426 |
. 2
           |
371 | 224, 370 | jca 541 |
1
     
               |