Step | Hyp | Ref
| Expression |
1 | | fzfid 11911 |
. . . . . 6
 
           |
2 | | simpr 461 |
. . . . . . . . 9
 

  |
3 | | elfznn 11594 |
. . . . . . . . . 10
           |
4 | 3 | nnrpd 11136 |
. . . . . . . . 9
           |
5 | | rpdivcl 11123 |
. . . . . . . . 9
       |
6 | 2, 4, 5 | syl2an 477 |
. . . . . . . 8
   
             |
7 | 6 | relogcld 22204 |
. . . . . . 7
   
                 |
8 | | simpll 753 |
. . . . . . 7
   
           |
9 | 7, 8 | reexpcld 12141 |
. . . . . 6
   
                     |
10 | 1, 9 | fsumrecl 13328 |
. . . . 5
 
                       |
11 | | relogcl 22159 |
. . . . . . 7

      |
12 | | id 22 |
. . . . . . 7

  |
13 | | reexpcl 11998 |
. . . . . . 7
     
           |
14 | 11, 12, 13 | syl2anr 478 |
. . . . . 6
 
           |
15 | | faccl 12177 |
. . . . . . . . 9

      |
16 | 15 | adantr 465 |
. . . . . . . 8
 
       |
17 | 16 | nnred 10447 |
. . . . . . 7
 
       |
18 | | fzfid 11911 |
. . . . . . . 8
 
       |
19 | 11 | adantl 466 |
. . . . . . . . . 10
 
       |
20 | | elfznn0 11597 |
. . . . . . . . . 10
       |
21 | | reexpcl 11998 |
. . . . . . . . . 10
     
           |
22 | 19, 20, 21 | syl2an 477 |
. . . . . . . . 9
   
               |
23 | 20 | adantl 466 |
. . . . . . . . . 10
   
       |
24 | | faccl 12177 |
. . . . . . . . . 10

      |
25 | 23, 24 | syl 16 |
. . . . . . . . 9
   
           |
26 | 22, 25 | nndivred 10480 |
. . . . . . . 8
   
                     |
27 | 18, 26 | fsumrecl 13328 |
. . . . . . 7
 
                       |
28 | 17, 27 | remulcld 9524 |
. . . . . 6
 
      
                      |
29 | 14, 28 | resubcld 9886 |
. . . . 5
 
                                       |
30 | 10, 29 | resubcld 9886 |
. . . 4
 
                                    
                        |
31 | 30, 2 | rerpdivcld 11164 |
. . 3
 
                                     
                         |
32 | | rerpdivcl 11128 |
. . . 4
                                                      
                        |
33 | 29, 32 | sylancom 667 |
. . 3
 
                
                        |
34 | | 1red 9511 |
. . . 4

  |
35 | 15 | nncnd 10448 |
. . . 4

      |
36 | | simpl 457 |
. . . . . . . . 9
 
   |
37 | 36 | oveq2d 6215 |
. . . . . . . 8
 
                   |
38 | 37 | oveq1d 6214 |
. . . . . . 7
 
                       |
39 | 38 | mpteq2dva 4485 |
. . . . . 6
                           |
40 | 39 | breq1d 4409 |
. . . . 5
                               |
41 | 11 | recnd 9522 |
. . . . . . . . 9

      |
42 | | id 22 |
. . . . . . . . 9

  |
43 | | cxpexp 22245 |
. . . . . . . . 9
     
                  |
44 | 41, 42, 43 | syl2anr 478 |
. . . . . . . 8
 
                  |
45 | | rpcn 11109 |
. . . . . . . . . 10

  |
46 | 45 | adantl 466 |
. . . . . . . . 9
 

  |
47 | 46 | cxp1d 22283 |
. . . . . . . 8
 
      |
48 | 44, 47 | oveq12d 6217 |
. . . . . . 7
 
                         |
49 | 48 | mpteq2dva 4485 |
. . . . . 6


                           |
50 | | nn0cn 10699 |
. . . . . . 7

  |
51 | | 1rp 11105 |
. . . . . . 7
 |
52 | | cxploglim2 22504 |
. . . . . . 7
 
                  |
53 | 50, 51, 52 | sylancl 662 |
. . . . . 6


                |
54 | 49, 53 | eqbrtrrd 4421 |
. . . . 5


              |
55 | 40, 54 | vtoclga 3140 |
. . . 4


              |
56 | | rerpdivcl 11128 |
. . . . . 6
                       |
57 | 14, 56 | sylancom 667 |
. . . . 5
 
             |
58 | 57 | recnd 9522 |
. . . 4
 
             |
59 | 10 | recnd 9522 |
. . . . . 6
 
                       |
60 | 14 | recnd 9522 |
. . . . . . 7
 
           |
61 | 35 | adantr 465 |
. . . . . . . 8
 
       |
62 | 27 | recnd 9522 |
. . . . . . . 8
 
                       |
63 | 61, 62 | mulcld 9516 |
. . . . . . 7
 
      
                      |
64 | 60, 63 | subcld 9829 |
. . . . . 6
 
                                       |
65 | 59, 64 | subcld 9829 |
. . . . 5
 
                                    
                        |
66 | | rpcnne0 11118 |
. . . . . . 7

    |
67 | 66 | adantl 466 |
. . . . . 6
 
     |
68 | 67 | simpld 459 |
. . . . 5
 

  |
69 | 67 | simprd 463 |
. . . . 5
 
   |
70 | 65, 68, 69 | divcld 10217 |
. . . 4
 
                                     
                         |
71 | 70 | adantrr 716 |
. . . . . . . 8
  
                                      
                         |
72 | 15 | adantr 465 |
. . . . . . . . 9
  
        |
73 | 72 | nncnd 10448 |
. . . . . . . 8
  
        |
74 | 71, 73 | subcld 9829 |
. . . . . . 7
  
                                                                      |
75 | 74 | abscld 13039 |
. . . . . 6
  
                                          
                               |
76 | 57 | adantrr 716 |
. . . . . 6
  
              |
77 | 76 | recnd 9522 |
. . . . . . 7
  
              |
78 | 77 | abscld 13039 |
. . . . . 6
  
                  |
79 | | ioorp 11483 |
. . . . . . . . . 10
    |
80 | 79 | eqcomi 2467 |
. . . . . . . . 9
    |
81 | | nnuz 11006 |
. . . . . . . . 9
     |
82 | | 1z 10786 |
. . . . . . . . . 10
 |
83 | 82 | a1i 11 |
. . . . . . . . 9
  
    |
84 | | 1red 9511 |
. . . . . . . . 9
  
    |
85 | | 1re 9495 |
. . . . . . . . . . 11
 |
86 | | 1nn0 10705 |
. . . . . . . . . . 11
 |
87 | 85, 86 | nn0addge1i 10738 |
. . . . . . . . . 10
   |
88 | 87 | a1i 11 |
. . . . . . . . 9
  
 
    |
89 | | 0red 9497 |
. . . . . . . . 9
  
    |
90 | 72 | adantr 465 |
. . . . . . . . . . 11
   
 

      |
91 | 90 | nnred 10447 |
. . . . . . . . . 10
   
 

      |
92 | | rpre 11107 |
. . . . . . . . . . . 12

  |
93 | 92 | adantl 466 |
. . . . . . . . . . 11
   
 

  |
94 | | fzfid 11911 |
. . . . . . . . . . . 12
   
 

      |
95 | | simprl 755 |
. . . . . . . . . . . . . . . 16
  
 
  |
96 | | rpdivcl 11123 |
. . . . . . . . . . . . . . . 16
       |
97 | 95, 96 | sylan 471 |
. . . . . . . . . . . . . . 15
   
 

    |
98 | 97 | relogcld 22204 |
. . . . . . . . . . . . . 14
   
 

        |
99 | | reexpcl 11998 |
. . . . . . . . . . . . . 14
       
             |
100 | 98, 20, 99 | syl2an 477 |
. . . . . . . . . . . . 13
   
  

                 |
101 | 20 | adantl 466 |
. . . . . . . . . . . . . 14
   
  

       |
102 | 101, 24 | syl 16 |
. . . . . . . . . . . . 13
   
  

           |
103 | 100, 102 | nndivred 10480 |
. . . . . . . . . . . 12
   
  

                       |
104 | 94, 103 | fsumrecl 13328 |
. . . . . . . . . . 11
   
 

                        |
105 | 93, 104 | remulcld 9524 |
. . . . . . . . . 10
   
 

                          |
106 | 91, 105 | remulcld 9524 |
. . . . . . . . 9
   
 

      
                         |
107 | | simpll 753 |
. . . . . . . . . 10
   
 

  |
108 | 98, 107 | reexpcld 12141 |
. . . . . . . . 9
   
 

            |
109 | | nnrp 11110 |
. . . . . . . . . 10
   |
110 | 109, 108 | sylan2 474 |
. . . . . . . . 9
   
 

            |
111 | | reelprrecn 9484 |
. . . . . . . . . . . 12
    |
112 | 111 | a1i 11 |
. . . . . . . . . . 11
  
       |
113 | 105 | recnd 9522 |
. . . . . . . . . . 11
   
 

                          |
114 | 108, 90 | nndivred 10480 |
. . . . . . . . . . 11
   
 

                  |
115 | | simpl 457 |
. . . . . . . . . . . 12
  
 
  |
116 | | advlogexp 22232 |
. . . . . . . . . . . 12
                                                   |
117 | 95, 115, 116 | syl2anc 661 |
. . . . . . . . . . 11
  
                                                  |
118 | 112, 113,
114, 117, 73 | dvmptcmul 21570 |
. . . . . . . . . 10
  
                                                              |
119 | 108 | recnd 9522 |
. . . . . . . . . . . 12
   
 

            |
120 | 73 | adantr 465 |
. . . . . . . . . . . 12
   
 

      |
121 | 72 | nnne0d 10476 |
. . . . . . . . . . . . 13
  
        |
122 | 121 | adantr 465 |
. . . . . . . . . . . 12
   
 

      |
123 | 119, 120,
122 | divcan2d 10219 |
. . . . . . . . . . 11
   
 

                                  |
124 | 123 | mpteq2dva 4485 |
. . . . . . . . . 10
  
                          
             |
125 | 118, 124 | eqtrd 2495 |
. . . . . . . . 9
  
                                                  |
126 | | oveq2 6207 |
. . . . . . . . . . 11
       |
127 | 126 | fveq2d 5802 |
. . . . . . . . . 10
               |
128 | 127 | oveq1d 6214 |
. . . . . . . . 9
                       |
129 | 95 | rpxrd 11138 |
. . . . . . . . 9
  
 
  |
130 | | simp1rl 1053 |
. . . . . . . . . . . 12
   
 
 

 
  |
131 | | simp2r 1015 |
. . . . . . . . . . . 12
   
 
 

 
  |
132 | 130, 131 | rpdivcld 11154 |
. . . . . . . . . . 11
   
 
 

      |
133 | 132 | relogcld 22204 |
. . . . . . . . . 10
   
 
 

          |
134 | | simp2l 1014 |
. . . . . . . . . . . 12
   
 
 

    |
135 | 130, 134 | rpdivcld 11154 |
. . . . . . . . . . 11
   
 
 

      |
136 | 135 | relogcld 22204 |
. . . . . . . . . 10
   
 
 

          |
137 | | simp1l 1012 |
. . . . . . . . . 10
   
 
 

 
  |
138 | | log1 22166 |
. . . . . . . . . . 11
     |
139 | 131 | rpcnd 11139 |
. . . . . . . . . . . . . . 15
   
 
 

 
  |
140 | 139 | mulid2d 9514 |
. . . . . . . . . . . . . 14
   
 
 

      |
141 | | simp33 1026 |
. . . . . . . . . . . . . 14
   
 
 

    |
142 | 140, 141 | eqbrtrd 4419 |
. . . . . . . . . . . . 13
   
 
 

   
  |
143 | | 1red 9511 |
. . . . . . . . . . . . . 14
   
 
 

    |
144 | 130 | rpred 11137 |
. . . . . . . . . . . . . 14
   
 
 

 
  |
145 | 143, 144,
131 | lemuldivd 11182 |
. . . . . . . . . . . . 13
   
 
 

          |
146 | 142, 145 | mpbid 210 |
. . . . . . . . . . . 12
   
 
 

 
    |
147 | | logleb 22184 |
. . . . . . . . . . . . 13
     
 
             |
148 | 51, 132, 147 | sylancr 663 |
. . . . . . . . . . . 12
   
 
 

        
         |
149 | 146, 148 | mpbid 210 |
. . . . . . . . . . 11
   
 
 

     
        |
150 | 138, 149 | syl5eqbrr 4433 |
. . . . . . . . . 10
   
 
 

 
        |
151 | | simp32 1025 |
. . . . . . . . . . . 12
   
 
 

 
  |
152 | 134, 131,
130 | lediv2d 11161 |
. . . . . . . . . . . 12
   
 
 

          |
153 | 151, 152 | mpbid 210 |
. . . . . . . . . . 11
   
 
 

   
    |
154 | 132, 135 | logled 22208 |
. . . . . . . . . . 11
   
 
 

            
         |
155 | 153, 154 | mpbid 210 |
. . . . . . . . . 10
   
 
 

       
        |
156 | | leexp1a 12038 |
. . . . . . . . . 10
                
                                          |
157 | 133, 136,
137, 150, 155, 156 | syl32anc 1227 |
. . . . . . . . 9
   
 
 

                        |
158 | | eqid 2454 |
. . . . . . . . 9

                                                                                                            |
159 | 97 | 3ad2antr1 1153 |
. . . . . . . . . . 11
   
 

      |
160 | 159 | relogcld 22204 |
. . . . . . . . . 10
   
 

          |
161 | | simpll 753 |
. . . . . . . . . 10
   
 

    |
162 | | rpcn 11109 |
. . . . . . . . . . . . . . . . 17

  |
163 | 162 | adantl 466 |
. . . . . . . . . . . . . . . 16
   
 

  |
164 | 163 | 3ad2antr1 1153 |
. . . . . . . . . . . . . . 15
   
 

    |
165 | 164 | mulid2d 9514 |
. . . . . . . . . . . . . 14
   
 

      |
166 | | simpr3 996 |
. . . . . . . . . . . . . 14
   
 

    |
167 | 165, 166 | eqbrtrd 4419 |
. . . . . . . . . . . . 13
   
 

      |
168 | | 1red 9511 |
. . . . . . . . . . . . . 14
   
 

    |
169 | 95 | rpred 11137 |
. . . . . . . . . . . . . . 15
  
 
  |
170 | 169 | adantr 465 |
. . . . . . . . . . . . . 14
   
 

    |
171 | | simpr1 994 |
. . . . . . . . . . . . . 14
   
 

    |
172 | 168, 170,
171 | lemuldivd 11182 |
. . . . . . . . . . . . 13
   
 

    
     |
173 | 167, 172 | mpbid 210 |
. . . . . . . . . . . 12
   
 

      |
174 | | logleb 22184 |
. . . . . . . . . . . . 13
     
 
             |
175 | 51, 159, 174 | sylancr 663 |
. . . . . . . . . . . 12
   
 

  
 
             |
176 | 173, 175 | mpbid 210 |
. . . . . . . . . . 11
   
 

              |
177 | 138, 176 | syl5eqbrr 4433 |
. . . . . . . . . 10
   
 

          |
178 | 160, 161,
177 | expge0d 12142 |
. . . . . . . . 9
   
 

              |
179 | 51 | a1i 11 |
. . . . . . . . 9
  
    |
180 | | 1le1 10074 |
. . . . . . . . . 10
 |
181 | 180 | a1i 11 |
. . . . . . . . 9
  
 
  |
182 | | simprr 756 |
. . . . . . . . 9
  
 
  |
183 | 169 | leidd 10016 |
. . . . . . . . 9
  
    |
184 | 80, 81, 83, 84, 88, 89, 106, 108, 110, 125, 128, 129, 157, 158, 178, 179, 95, 181, 182, 183 | dvfsumlem4 21633 |
. . . . . . . 8
  
                                   
                                                         
                                ![]_ ]_](_urbrack.gif)             |
185 | | fzfid 11911 |
. . . . . . . . . . . . . 14
  
            |
186 | 95, 4, 5 | syl2an 477 |
. . . . . . . . . . . . . . . 16
   
 
        
    |
187 | 186 | relogcld 22204 |
. . . . . . . . . . . . . . 15
   
 
        
        |
188 | | simpll 753 |
. . . . . . . . . . . . . . 15
   
 
        
  |
189 | 187, 188 | reexpcld 12141 |
. . . . . . . . . . . . . 14
   
 
        
            |
190 | 185, 189 | fsumrecl 13328 |
. . . . . . . . . . . . 13
  
                        |
191 | 190 | recnd 9522 |
. . . . . . . . . . . 12
  
                        |
192 | 95 | rpcnd 11139 |
. . . . . . . . . . . . 13
  
 
  |
193 | 73, 192 | mulcld 9516 |
. . . . . . . . . . . 12
  
          |
194 | 11 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
  
        |
195 | 194 | recnd 9522 |
. . . . . . . . . . . . . 14
  
        |
196 | 195, 115 | expcld 12124 |
. . . . . . . . . . . . 13
  
            |
197 | | fzfid 11911 |
. . . . . . . . . . . . . . 15
  
        |
198 | 194, 20, 21 | syl2an 477 |
. . . . . . . . . . . . . . . . 17
   
 
               |
199 | 20 | adantl 466 |
. . . . . . . . . . . . . . . . . 18
   
 
       |
200 | 199, 24 | syl 16 |
. . . . . . . . . . . . . . . . 17
   
 
           |
201 | 198, 200 | nndivred 10480 |
. . . . . . . . . . . . . . . 16
   
 
                     |
202 | 201 | recnd 9522 |
. . . . . . . . . . . . . . 15
   
 
                     |
203 | 197, 202 | fsumcl 13327 |
. . . . . . . . . . . . . 14
  
                        |
204 | 73, 203 | mulcld 9516 |
. . . . . . . . . . . . 13
  
       
                      |
205 | 196, 204 | subcld 9829 |
. . . . . . . . . . . 12
  
                                        |
206 | 191, 193,
205 | sub32d 9861 |
. . . . . . . . . . 11
  
                                                                                                        
                               |
207 | | eqidd 2455 |
. . . . . . . . . . . . 13
  
                              
                                                     
                           |
208 | | simpr 461 |
. . . . . . . . . . . . . . . . 17
   
 
   |
209 | 208 | fveq2d 5802 |
. . . . . . . . . . . . . . . 16
   
 
           |
210 | 209 | oveq2d 6215 |
. . . . . . . . . . . . . . 15
   
 
                   |
211 | 210 | sumeq1d 13295 |
. . . . . . . . . . . . . 14
   
 
                                           |
212 | | oveq2 6207 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       |
213 | 66 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
      |
214 | | divid 10131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       |
215 | 213, 214 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  
      |
216 | 212, 215 | sylan9eqr 2517 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
 
     |
217 | 216 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
  

         |
218 | 217 | fveq2d 5802 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
  

                 |
219 | 218, 138 | syl6eq 2511 |
. . . . . . . . . . . . . . . . . . . . . 22
   
  

             |
220 | 219 | oveq1d 6214 |
. . . . . . . . . . . . . . . . . . . . 21
   
  

                     |
221 | 220 | oveq1d 6214 |
. . . . . . . . . . . . . . . . . . . 20
   
  

                                 |
222 | 221 | sumeq2dv 13297 |
. . . . . . . . . . . . . . . . . . 19
   
 
                       
                 |
223 | | nn0uz 11005 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
224 | 115, 223 | syl6eleq 2552 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
 
      |
225 | | eluzfz1 11574 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
      |
226 | 224, 225 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . 22
  
        |
227 | 226 | adantr 465 |
. . . . . . . . . . . . . . . . . . . . 21
   
 
       |
228 | 227 | snssd 4125 |
. . . . . . . . . . . . . . . . . . . 20
   
 
  
      |
229 | | elsni 4009 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
230 | 229 | adantl 466 |
. . . . . . . . . . . . . . . . . . . . . 22
   
  

     |
231 | | oveq2 6207 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
232 | | 0exp0e1 11986 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
233 | 231, 232 | syl6eq 2511 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
234 | | fveq2 5798 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
235 | | fac0 12170 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
236 | 234, 235 | syl6eq 2511 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
237 | 233, 236 | oveq12d 6217 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
238 | | 1div1e1 10134 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
239 | 237, 238 | syl6eq 2511 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
240 | 230, 239 | syl 16 |
. . . . . . . . . . . . . . . . . . . . 21
   
  

               |
241 | | ax-1cn 9450 |
. . . . . . . . . . . . . . . . . . . . 21
 |
242 | 240, 241 | syl6eqel 2550 |
. . . . . . . . . . . . . . . . . . . 20
   
  

               |
243 | | eldifi 3585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
               |
244 | 243 | adantl 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
  

    
          |
245 | 244, 20 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
  

    
      |
246 | | eldifsni 4108 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
247 | 246 | adantl 466 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
  

    
      |
248 | | eldifsn 4107 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
    |
249 | 245, 247,
248 | sylanbrc 664 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
  

    
          |
250 | | dfn2 10702 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
251 | 249, 250 | syl6eleqr 2553 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
  

    
      |
252 | 251 | 0expd 12140 |
. . . . . . . . . . . . . . . . . . . . . 22
   
  

    
          |
253 | 252 | oveq1d 6214 |
. . . . . . . . . . . . . . . . . . . . 21
   
  

    
                      |
254 | 245, 24 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
  

    
          |
255 | 254 | nncnd 10448 |
. . . . . . . . . . . . . . . . . . . . . 22
   
  

    
          |
256 | 254 | nnne0d 10476 |
. . . . . . . . . . . . . . . . . . . . . 22
   
  

    
          |
257 | 255, 256 | div0d 10216 |
. . . . . . . . . . . . . . . . . . . . 21
   
  

    
            |
258 | 253, 257 | eqtrd 2495 |
. . . . . . . . . . . . . . . . . . . 20
   
  

    
                |
259 | | fzfid 11911 |
. . . . . . . . . . . . . . . . . . . 20
   
 
       |
260 | 228, 242,
258, 259 | fsumss 13319 |
. . . . . . . . . . . . . . . . . . 19
   
 
                                |
261 | 222, 260 | eqtr4d 2498 |
. . . . . . . . . . . . . . . . . 18
   
 
                       
              |
262 | | 0cn 9488 |
. . . . . . . . . . . . . . . . . . 19
 |
263 | 239 | sumsn 13334 |
. . . . . . . . . . . . . . . . . . 19
 
                |
264 | 262, 241,
263 | mp2an 672 |
. . . . . . . . . . . . . . . . . 18
              |
265 | 261, 264 | syl6eq 2511 |
. . . . . . . . . . . . . . . . 17
   
 
                         |
266 | 208, 265 | oveq12d 6217 |
. . . . . . . . . . . . . . . 16
   
 
                             |
267 | 192 | mulid1d 9513 |
. . . . . . . . . . . . . . . . 17
  
      |
268 | 267 | adantr 465 |
. . . . . . . . . . . . . . . 16
   
 
     |
269 | 266, 268 | eqtrd 2495 |
. . . . . . . . . . . . . . 15
   
 
                           |
270 | 269 | oveq2d 6215 |
. . . . . . . . . . . . . 14
   
 
                                       |
271 | 211, 270 | oveq12d 6217 |
. . . . . . . . . . . . 13
   
 
                            
                         
                            |
272 | | ovex 6224 |
. . . . . . . . . . . . . 14
                             |
273 | 272 | a1i 11 |
. . . . . . . . . . . . 13
  
                                |
274 | 207, 271,
95, 273 | fvmptd 5887 |
. . . . . . . . . . . 12
  
                               
                             
                            |
275 | | simpr 461 |
. . . . . . . . . . . . . . . . . . 19
   
 
   |
276 | 275 | fveq2d 5802 |
. . . . . . . . . . . . . . . . . 18
   
 
           |
277 | | flid 11773 |
. . . . . . . . . . . . . . . . . . 19
       |
278 | 82, 277 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
     |
279 | 276, 278 | syl6eq 2511 |
. . . . . . . . . . . . . . . . 17
   
 
       |
280 | 279 | oveq2d 6215 |
. . . . . . . . . . . . . . . 16
   
 
               |
281 | 280 | sumeq1d 13295 |
. . . . . . . . . . . . . . 15
   
 
                                       |
282 | 192 | div1d 10209 |
. . . . . . . . . . . . . . . . . . . 20
  
      |
283 | 282 | adantr 465 |
. . . . . . . . . . . . . . . . . . 19
   
 
     |
284 | 283 | fveq2d 5802 |
. . . . . . . . . . . . . . . . . 18
   
 
             |
285 | 284 | oveq1d 6214 |
. . . . . . . . . . . . . . . . 17
   
 
                     |
286 | 196 | adantr 465 |
. . . . . . . . . . . . . . . . 17
   
 
           |
287 | 285, 286 | eqeltrd 2542 |
. . . . . . . . . . . . . . . 16
   
 
             |
288 | | oveq2 6207 |
. . . . . . . . . . . . . . . . . . 19
       |
289 | 288 | fveq2d 5802 |
. . . . . . . . . . . . . . . . . 18
               |
290 | 289 | oveq1d 6214 |
. . . . . . . . . . . . . . . . 17
                       |
291 | 290 | fsum1 13335 |
. . . . . . . . . . . . . . . 16
                                         |
292 | 82, 287, 291 | sylancr 663 |
. . . . . . . . . . . . . . 15
   
 
                             |
293 | 281, 292,
285 | 3eqtrd 2499 |
. . . . . . . . . . . . . 14
   
 
                               |
294 | 275 | oveq2d 6215 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
 
       |
295 | 294, 283 | eqtrd 2495 |
. . . . . . . . . . . . . . . . . . . . . 22
   
 
     |
296 | 295 | fveq2d 5802 |
. . . . . . . . . . . . . . . . . . . . 21
   
 
             |
297 | 296 | adantr 465 |
. . . . . . . . . . . . . . . . . . . 20
   
  
     
            |
298 | 297 | oveq1d 6214 |
. . . . . . . . . . . . . . . . . . 19
   
  
     
                    |
299 | 298 | oveq1d 6214 |
. . . . . . . . . . . . . . . . . 18
   
  
     
                                |
300 | 299 | sumeq2dv 13297 |
. . . . . . . . . . . . . . . . 17
   
 
                       
                     |
301 | 275, 300 | oveq12d 6217 |
. . . . . . . . . . . . . . . 16
   
 
                          
                      |
302 | 203 | adantr 465 |
. . . . . . . . . . . . . . . . 17
   
 
                       |
303 | 302 | mulid2d 9514 |
. . . . . . . . . . . . . . . 16
   
 
                                             |
304 | 301, 303 | eqtrd 2495 |
. . . . . . . . . . . . . . 15
   
 
                                               |
305 | 304 | oveq2d 6215 |
. . . . . . . . . . . . . 14
   
 
                                                           |
306 | 293, 305 | oveq12d 6217 |
. . . . . . . . . . . . 13
   
 
                            
                                                              |
307 | | ovex 6224 |
. . . . . . . . . . . . . 14
                                     |
308 | 307 | a1i 11 |
. . . . . . . . . . . . 13
  
                                        |
309 | 207, 306,
179, 308 | fvmptd 5887 |
. . . . . . . . . . . 12
  
                               
                                                                  |
310 | 274, 309 | oveq12d 6217 |
. . . . . . . . . . 11
  
    
                                                                                                                                                                                       |
311 | 71, 73, 192 | subdird 9911 |
. . . . . . . . . . . 12
  
      
                                 
                                 
                                 
                                 |
312 | 65 | adantrr 716 |
. . . . . . . . . . . . . 14
  
                                     
                        |
313 | 213 | simprd 463 |
. . . . . . . . . . . . . 14
  
    |
314 | 312, 192,
313 | divcan1d 10218 |
. . . . . . . . . . . . 13
  
                                                                                                                            |
315 | 314 | oveq1d 6214 |
. . . . . . . . . . . 12
  
      
                                 
                                                                   
                               |
316 | 311, 315 | eqtrd 2495 |
. . . . . . . . . . 11
  
      
                                 
                                                                 
                               |
317 | 206, 310,
316 | 3eqtr4d 2505 |
. . . . . . . . . 10
  
    
                                                                                                                                                                                         |
318 | 317 | fveq2d 5802 |
. . . . . . . . 9
  
                                   
                                                         
                                                                                                        |
319 | 74, 192 | absmuld 13057 |
. . . . . . . . 9
  
                                                                                                                   
                                    |
320 | | rprege0 11115 |
. . . . . . . . . . . 12

    |
321 | 320 | ad2antrl 727 |
. . . . . . . . . . 11
  
  
   |
322 | | absid 12902 |
. . . . . . . . . . 11
         |
323 | 321, 322 | syl 16 |
. . . . . . . . . 10
  
        |
324 | 323 | oveq2d 6215 |
. . . . . . . . 9
  
                                           
                                                                           
                                |
325 | 318, 319,
324 | 3eqtrd 2499 |
. . . . . . . 8
  
                                   
                                                         
                                                                                                        |
326 | | 1cnd 9512 |
. . . . . . . . 9
  
    |
327 | 296 | oveq1d 6214 |
. . . . . . . . 9
   
 
                     |
328 | 326, 327 | csbied 3421 |
. . . . . . . 8
  
  
 ![]_ ]_](_urbrack.gif)                     |
329 | 184, 325,
328 | 3brtr3d 4428 |
. . . . . . 7
  
                                           
                                        |
330 | 14 | adantrr 716 |
. . . . . . . 8
  
            |
331 | 75, 330, 95 | lemuldivd 11182 |
. . . . . . 7
  
                                                                          
       
                                |