Step | Hyp | Ref
| Expression |
1 | | nfv 1761 |
. . . . . 6
     |
2 | | nfcv 2592 |
. . . . . 6
           |
3 | | dvnprodlem2.t |
. . . . . . . 8
   |
4 | | dvnprodlem2.r |
. . . . . . . 8

  |
5 | | ssfi 7792 |
. . . . . . . 8
  
  |
6 | 3, 4, 5 | syl2anc 667 |
. . . . . . 7
   |
7 | 6 | adantr 467 |
. . . . . 6
 
   |
8 | | dvnprodlem2.z |
. . . . . . 7
     |
9 | 8 | adantr 467 |
. . . . . 6
 
     |
10 | 8 | eldifbd 3417 |
. . . . . . 7
   |
11 | 10 | adantr 467 |
. . . . . 6
 

  |
12 | | simpl 459 |
. . . . . . . . 9
 
   |
13 | 4 | sselda 3432 |
. . . . . . . . 9
 
   |
14 | | dvnprodlem2.h |
. . . . . . . . 9
 
           |
15 | 12, 13, 14 | syl2anc 667 |
. . . . . . . 8
 
           |
16 | 15 | adantlr 721 |
. . . . . . 7
               |
17 | | simplr 762 |
. . . . . . 7
       |
18 | 16, 17 | ffvelrnd 6023 |
. . . . . 6
               |
19 | | fveq2 5865 |
. . . . . . 7
           |
20 | 19 | fveq1d 5867 |
. . . . . 6
                   |
21 | | id 22 |
. . . . . . . . 9
   |
22 | | eldifi 3555 |
. . . . . . . . . 10
     |
23 | 8, 22 | syl 17 |
. . . . . . . . 9
   |
24 | | simpr 463 |
. . . . . . . . . 10
 
   |
25 | | id 22 |
. . . . . . . . . 10
 
     |
26 | | eleq1 2517 |
. . . . . . . . . . . . 13
 
   |
27 | 26 | anbi2d 710 |
. . . . . . . . . . . 12
  

     |
28 | 19 | feq1d 5714 |
. . . . . . . . . . . 12
         
           |
29 | 27, 28 | imbi12d 322 |
. . . . . . . . . . 11
   
           
             |
30 | 29, 14 | vtoclg 3107 |
. . . . . . . . . 10
  
            |
31 | 24, 25, 30 | sylc 62 |
. . . . . . . . 9
 
           |
32 | 21, 23, 31 | syl2anc 667 |
. . . . . . . 8
           |
33 | 32 | adantr 467 |
. . . . . . 7
 
           |
34 | | simpr 463 |
. . . . . . 7
 
   |
35 | 33, 34 | ffvelrnd 6023 |
. . . . . 6
 
           |
36 | 1, 2, 7, 9, 11, 18, 20, 35 | fprodsplitsn 14043 |
. . . . 5
 
                
                   |
37 | 36 | mpteq2dva 4489 |
. . . 4
  

               
                    |
38 | 37 | oveq2d 6306 |
. . 3
     

                                         |
39 | 38 | fveq1d 5867 |
. 2
                                                        |
40 | | dvnprodlem2.s |
. . 3
      |
41 | | dvnprodlem2.x |
. . 3
    ℂfld ↾t    |
42 | 1, 7, 18 | fprodclf 14046 |
. . 3
 
            |
43 | | dvnprodlem2.j |
. . . 4
       |
44 | | elfznn0 11887 |
. . . 4
       |
45 | 43, 44 | syl 17 |
. . 3
   |
46 | | eqid 2451 |
. . 3
 
          
          |
47 | | eqid 2451 |
. . 3
                     |
48 | | dvnprodlem2.c |
. . . . . . . . . . 11
          
        |
49 | 48 | a1i 11 |
. . . . . . . . . 10
 
       
       
         |
50 | | oveq2 6298 |
. . . . . . . . . . . . . 14
     
         |
51 | | rabeq 3038 |
. . . . . . . . . . . . . 14
     
              
                    |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . 13
        
                    |
53 | | sumeq1 13755 |
. . . . . . . . . . . . . . 15
 
    
      |
54 | 53 | eqeq1d 2453 |
. . . . . . . . . . . . . 14
      
        |
55 | 54 | rabbidv 3036 |
. . . . . . . . . . . . 13
        
                    |
56 | 52, 55 | eqtrd 2485 |
. . . . . . . . . . . 12
        
                    |
57 | 56 | mpteq2dv 4490 |
. . . . . . . . . . 11
         
            
          |
58 | 57 | adantl 468 |
. . . . . . . . . 10
                 
            
          |
59 | | ssexg 4549 |
. . . . . . . . . . . . . 14
 
   |
60 | 4, 3, 59 | syl2anc 667 |
. . . . . . . . . . . . 13
   |
61 | | elpwg 3959 |
. . . . . . . . . . . . 13
 
    |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . 12
  
   |
63 | 4, 62 | mpbird 236 |
. . . . . . . . . . 11
    |
64 | 63 | adantr 467 |
. . . . . . . . . 10
 
        |
65 | | nn0ex 10875 |
. . . . . . . . . . . 12
 |
66 | 65 | mptex 6136 |
. . . . . . . . . . 11

       
       |
67 | 66 | a1i 11 |
. . . . . . . . . 10
 
             
        |
68 | 49, 58, 64, 67 | fvmptd 5954 |
. . . . . . . . 9
 
                 
        |
69 | | oveq2 6298 |
. . . . . . . . . . . . 13
           |
70 | 69 | oveq1d 6305 |
. . . . . . . . . . . 12
     
         |
71 | | rabeq 3038 |
. . . . . . . . . . . 12
     
              
                    |
72 | 70, 71 | syl 17 |
. . . . . . . . . . 11
        
                    |
73 | | eqeq2 2462 |
. . . . . . . . . . . 12
      
        |
74 | 73 | rabbidv 3036 |
. . . . . . . . . . 11
        
                    |
75 | 72, 74 | eqtrd 2485 |
. . . . . . . . . 10
        
                    |
76 | 75 | adantl 468 |
. . . . . . . . 9
              
            
         |
77 | | elfznn0 11887 |
. . . . . . . . . 10
       |
78 | 77 | adantl 468 |
. . . . . . . . 9
 
       |
79 | | fzfid 12186 |
. . . . . . . . . . . 12
       |
80 | | mapfi 7870 |
. . . . . . . . . . . 12
     
         |
81 | 79, 6, 80 | syl2anc 667 |
. . . . . . . . . . 11
         |
82 | 81 | adantr 467 |
. . . . . . . . . 10
 
         
   |
83 | | ssrab2 3514 |
. . . . . . . . . . 11
       
            |
84 | 83 | a1i 11 |
. . . . . . . . . 10
 
            
             |
85 | 82, 84 | ssexd 4550 |
. . . . . . . . 9
 
            
       |
86 | 68, 76, 78, 85 | fvmptd 5954 |
. . . . . . . 8
 
                  
         |
87 | | ssfi 7792 |
. . . . . . . . . 10
                                 
         |
88 | 81, 83, 87 | sylancl 668 |
. . . . . . . . 9
      
         |
89 | 88 | adantr 467 |
. . . . . . . 8
 
            
       |
90 | 86, 89 | eqeltrd 2529 |
. . . . . . 7
 
               |
91 | 90 | adantr 467 |
. . . . . 6
                   |
92 | 77 | faccld 37533 |
. . . . . . . . . . 11
           |
93 | 92 | nncnd 10625 |
. . . . . . . . . 10
           |
94 | 93 | ad2antlr 733 |
. . . . . . . . 9
                       |
95 | 6 | adantr 467 |
. . . . . . . . . . 11
 
           |
96 | 95 | adantlr 721 |
. . . . . . . . . 10
                   |
97 | | elfznn0 11887 |
. . . . . . . . . . . . . . 15
       |
98 | 97 | ssriv 3436 |
. . . . . . . . . . . . . 14
     |
99 | 98 | a1i 11 |
. . . . . . . . . . . . 13
   
             
       |
100 | | simpr 463 |
. . . . . . . . . . . . . . . . . 18
                           |
101 | 86 | eleq2d 2514 |
. . . . . . . . . . . . . . . . . . 19
 
             
                |
102 | 101 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
                         
                |
103 | 100, 102 | mpbid 214 |
. . . . . . . . . . . . . . . . 17
                      
         |
104 | 83 | sseli 3428 |
. . . . . . . . . . . . . . . . 17
        
    
        |
105 | 103, 104 | syl 17 |
. . . . . . . . . . . . . . . 16
                         |
106 | | elmapi 7493 |
. . . . . . . . . . . . . . . 16
                 |
107 | 105, 106 | syl 17 |
. . . . . . . . . . . . . . 15
                           |
108 | 107 | adantr 467 |
. . . . . . . . . . . . . 14
   
             
           |
109 | | simpr 463 |
. . . . . . . . . . . . . 14
   
             
   |
110 | 108, 109 | ffvelrnd 6023 |
. . . . . . . . . . . . 13
   
             
           |
111 | 99, 110 | sseldd 3433 |
. . . . . . . . . . . 12
   
             
       |
112 | 111 | faccld 37533 |
. . . . . . . . . . 11
   
             
           |
113 | 112 | nncnd 10625 |
. . . . . . . . . 10
   
             
           |
114 | 96, 113 | fprodcl 14006 |
. . . . . . . . 9
                            |
115 | 112 | nnne0d 10654 |
. . . . . . . . . 10
   
             
           |
116 | 96, 113, 115 | fprodn0 14033 |
. . . . . . . . 9
                            |
117 | 94, 114, 116 | divcld 10383 |
. . . . . . . 8
                      
           |
118 | 117 | adantlr 721 |
. . . . . . 7
   
     
              
           |
119 | 96 | adantlr 721 |
. . . . . . . 8
   
     
           |
120 | 21 | ad4antr 738 |
. . . . . . . . . 10
          
            |
121 | 120, 13 | sylancom 673 |
. . . . . . . . . 10
          
            |
122 | | elfzuz3 11797 |
. . . . . . . . . . . . . . . 16
           |
123 | | fzss2 11838 |
. . . . . . . . . . . . . . . 16
    
          |
124 | 122, 123 | syl 17 |
. . . . . . . . . . . . . . 15
               |
125 | 124 | adantl 468 |
. . . . . . . . . . . . . 14
 
               |
126 | 45 | nn0zd 11038 |
. . . . . . . . . . . . . . . . . 18
   |
127 | | dvnprodlem2.n |
. . . . . . . . . . . . . . . . . . 19
   |
128 | 127 | nn0zd 11038 |
. . . . . . . . . . . . . . . . . 18
   |
129 | | elfzle2 11803 |
. . . . . . . . . . . . . . . . . . 19
       |
130 | 43, 129 | syl 17 |
. . . . . . . . . . . . . . . . . 18

  |
131 | 126, 128,
130 | 3jca 1188 |
. . . . . . . . . . . . . . . . 17
     |
132 | | eluz2 11165 |
. . . . . . . . . . . . . . . . 17
         |
133 | 131, 132 | sylibr 216 |
. . . . . . . . . . . . . . . 16
       |
134 | | fzss2 11838 |
. . . . . . . . . . . . . . . 16
    
          |
135 | 133, 134 | syl 17 |
. . . . . . . . . . . . . . 15
    
      |
136 | 135 | adantr 467 |
. . . . . . . . . . . . . 14
 
               |
137 | 125, 136 | sstrd 3442 |
. . . . . . . . . . . . 13
 
               |
138 | 137 | ad2antrr 732 |
. . . . . . . . . . . 12
   
             
           |
139 | 138, 110 | sseldd 3433 |
. . . . . . . . . . 11
   
             
           |
140 | 139 | adantllr 725 |
. . . . . . . . . 10
          
                    |
141 | | fvex 5875 |
. . . . . . . . . . 11
     |
142 | | eleq1 2517 |
. . . . . . . . . . . . 13
         
           |
143 | 142 | 3anbi3d 1345 |
. . . . . . . . . . . 12
      
    
             |
144 | | fveq2 5865 |
. . . . . . . . . . . . 13
                                   |
145 | 144 | feq1d 5714 |
. . . . . . . . . . . 12
                                             |
146 | 143, 145 | imbi12d 322 |
. . . . . . . . . . 11
       
                     
                                   |
147 | | dvnprodlem2.dvnh |
. . . . . . . . . . 11
 
    
                  |
148 | 141, 146,
147 | vtocl 3100 |
. . . . . . . . . 10
 
        
                      |
149 | 120, 121,
140, 148 | syl3anc 1268 |
. . . . . . . . 9
          
                                |
150 | | simpllr 769 |
. . . . . . . . 9
          
            |
151 | 149, 150 | ffvelrnd 6023 |
. . . . . . . 8
          
                                |
152 | 119, 151 | fprodcl 14006 |
. . . . . . 7
   
     
                                |
153 | 118, 152 | mulcld 9663 |
. . . . . 6
   
     
                                                 |
154 | 91, 153 | fsumcl 13799 |
. . . . 5
                                   
                       |
155 | | eqid 2451 |
. . . . 5
                           
                                                                         |
156 | 154, 155 | fmptd 6046 |
. . . 4
 
                                                             |
157 | | dvnprodlem2.ind |
. . . . . . 7
                                                                              |
158 | 157 | adantr 467 |
. . . . . 6
 
                
                                        
                        |
159 | | 0zd 10949 |
. . . . . . . . 9
 
       |
160 | 128 | adantr 467 |
. . . . . . . . 9
 
       |
161 | | elfzelz 11800 |
. . . . . . . . . 10
       |
162 | 161 | adantl 468 |
. . . . . . . . 9
 
       |
163 | 159, 160,
162 | 3jca 1188 |
. . . . . . . 8
 
     
   |
164 | | elfzle1 11802 |
. . . . . . . . 9
       |
165 | 164 | adantl 468 |
. . . . . . . 8
 
       |
166 | 162 | zred 11040 |
. . . . . . . . 9
 
       |
167 | 45 | nn0red 10926 |
. . . . . . . . . 10
   |
168 | 167 | adantr 467 |
. . . . . . . . 9
 
       |
169 | 160 | zred 11040 |
. . . . . . . . 9
 
       |
170 | | elfzle2 11803 |
. . . . . . . . . 10
       |
171 | 170 | adantl 468 |
. . . . . . . . 9
 
       |
172 | 130 | adantr 467 |
. . . . . . . . 9
 
       |
173 | 166, 168,
169, 171, 172 | letrd 9792 |
. . . . . . . 8
 
       |
174 | 163, 165,
173 | jca32 538 |
. . . . . . 7
 
      
 
    |
175 | | elfz2 11791 |
. . . . . . 7
    
 
 
    |
176 | 174, 175 | sylibr 216 |
. . . . . 6
 
           |
177 | | rspa 2755 |
. . . . . 6
                                                                                 
     
                                        
                        |
178 | 158, 176,
177 | syl2anc 667 |
. . . . 5
 
          
                                                                 |
179 | 178 | feq1d 5714 |
. . . 4
 
                                                        
                             |
180 | 156, 179 | mpbird 236 |
. . 3
 
          
                   |
181 | 23 | adantr 467 |
. . . . 5
 
       |
182 | | simpl 459 |
. . . . . 6
 
       |
183 | 182, 181,
176 | 3jca 1188 |
. . . . 5
 
     
       |
184 | 26 | 3anbi2d 1344 |
. . . . . . 7
  
    

        |
185 | 19 | oveq2d 6306 |
. . . . . . . . 9
                   |
186 | 185 | fveq1d 5867 |
. . . . . . . 8
                           |
187 | 186 | feq1d 5714 |
. . . . . . 7
                                     |
188 | 184, 187 | imbi12d 322 |
. . . . . 6
   
                     
 
                         |
189 | | eleq1 2517 |
. . . . . . . . 9
     
       |
190 | 189 | 3anbi3d 1345 |
. . . . . . . 8
  
    

        |
191 | | fveq2 5865 |
. . . . . . . . 9
                           |
192 | 191 | feq1d 5714 |
. . . . . . . 8
                                     |
193 | 190, 192 | imbi12d 322 |
. . . . . . 7
   
                     
 
                         |
194 | 193, 147 | chvarv 2107 |
. . . . . 6
 
    
                  |
195 | 188, 194 | vtoclg 3107 |
. . . . 5
  
                        |
196 | 181, 183,
195 | sylc 62 |
. . . 4
 
                       |
197 | 32 | feqmptd 5918 |
. . . . . . . . 9
                 |
198 | 197 | eqcomd 2457 |
. . . . . . . 8
                 |
199 | 198 | oveq2d 6306 |
. . . . . . 7
                         |
200 | 199 | fveq1d 5867 |
. . . . . 6
                                 |
201 | 200 | adantr 467 |
. . . . 5
 
                                     |
202 | 201 | feq1d 5714 |
. . . 4
 
                           
                   |
203 | 196, 202 | mpbird 236 |
. . 3
 
                             |
204 | | fveq2 5865 |
. . . . . . . 8
                   |
205 | 204 | prodeq2ad 37672 |
. . . . . . 7
          
          |
206 | 205 | cbvmptv 4495 |
. . . . . 6
 
          
          |
207 | 206 | oveq2i 6301 |
. . . . 5
    
                          |
208 | 207 | fveq1i 5866 |
. . . 4
                                       |
209 | 208 | mpteq2i 4486 |
. . 3
                                   
               |
210 | | fveq2 5865 |
. . . . . . 7
                   |
211 | 210 | cbvmptv 4495 |
. . . . . 6
                     |
212 | 211 | oveq2i 6301 |
. . . . 5
                             |
213 | 212 | fveq1i 5866 |
. . . 4
                                     |
214 | 213 | mpteq2i 4486 |
. . 3
                                                 |
215 | 40, 41, 42, 35, 45, 46, 47, 180, 203, 209, 214 | dvnmul 37818 |
. 2
       
                                             
                                                           |
216 | 208 | a1i 11 |
. . . . . . . . . . . . . 14
 
          
                  
               |
217 | 157 | r19.21bi 2757 |
. . . . . . . . . . . . . . 15
 
          
                                                                 |
218 | 182, 176,
217 | syl2anc 667 |
. . . . . . . . . . . . . 14
 
          
                                                                 |
219 | 216, 218 | eqtrd 2485 |
. . . . . . . . . . . . 13
 
          
                                                                 |
220 | 219 | mpteq2dva 4489 |
. . . . . . . . . . . 12
                                                          
                         |
221 | | mptexg 6135 |
. . . . . . . . . . . . . 14
    ℂfld ↾t 

                          
                        |
222 | 41, 221 | syl 17 |
. . . . . . . . . . . . 13
                            
                        |
223 | 222 | adantr 467 |
. . . . . . . . . . . 12
 
                                                         |
224 | 220, 223 | fvmpt2d 5959 |
. . . . . . . . . . 11
 
                                                                                      |
225 | 224 | adantlr 721 |
. . . . . . . . . 10
                                                                                          |
226 | 225 | fveq1d 5867 |
. . . . . . . . 9
                     
                                                
                           |
227 | 34 | adantr 467 |
. . . . . . . . . 10
           |
228 | 154 | an32s 813 |
. . . . . . . . . 10
                                   
                       |
229 | 155 | fvmpt2 5957 |
. . . . . . . . . 10
                                                                               
                                                   
                       |
230 | 227, 228,
229 | syl2anc 667 |
. . . . . . . . 9
                                     
                                                   
                       |
231 | 226, 230 | eqtrd 2485 |
. . . . . . . 8
                     
                    
               
         
                       |
232 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
                                       |
233 | 232 | cbvmptv 4495 |
. . . . . . . . . . . . . 14
                                                 |
234 | 233 | a1i 11 |
. . . . . . . . . . . . 13
                                                   |
235 | 212, 199 | syl5eq 2497 |
. . . . . . . . . . . . . . 15
                         |
236 | 235 | fveq1d 5867 |
. . . . . . . . . . . . . 14
                                 |
237 | 236 | mpteq2dv 4490 |
. . . . . . . . . . . . 13
                                             |
238 | 234, 237 | eqtrd 2485 |
. . . . . . . . . . . 12
                                             |
239 | 238 | adantr 467 |
. . . . . . . . . . 11
 
                                                 |
240 | | fveq2 5865 |
. . . . . . . . . . . 12
                               |
241 | 240 | adantl 468 |
. . . . . . . . . . 11
                                  
    |
242 | | 0zd 10949 |
. . . . . . . . . . . . . . 15
       |
243 | | elfzel2 11798 |
. . . . . . . . . . . . . . 15
       |
244 | 243, 161 | zsubcld 11045 |
. . . . . . . . . . . . . . 15
     
   |
245 | 242, 243,
244 | 3jca 1188 |
. . . . . . . . . . . . . 14
     

    |
246 | 243 | zred 11040 |
. . . . . . . . . . . . . . . 16
       |
247 | 77 | nn0red 10926 |
. . . . . . . . . . . . . . . 16
       |
248 | 246, 247 | subge0d 10203 |
. . . . . . . . . . . . . . 15
     
 
   |
249 | 170, 248 | mpbird 236 |
. . . . . . . . . . . . . 14
         |
250 | 246, 247 | subge02d 10205 |
. . . . . . . . . . . . . . 15
     
     |
251 | 164, 250 | mpbid 214 |
. . . . . . . . . . . . . 14
     
   |
252 | 245, 249,
251 | jca32 538 |
. . . . . . . . . . . . 13
       
    
      |
253 | 252 | adantl 468 |
. . . . . . . . . . . 12
 
       
    
      |
254 | | elfz2 11791 |
. . . . . . . . . . . 12
      
 

  
  

    |
255 | 253, 254 | sylibr 216 |
. . . . . . . . . . 11
 
     
       |
256 | | fvex 5875 |
. . . . . . . . . . . 12
               |
257 | 256 | a1i 11 |
. . . . . . . . . . 11
 
                
    |
258 | 239, 241,
255, 257 | fvmptd 5954 |
. . . . . . . . . 10
 
                                              
    |
259 | 258 | adantlr 721 |
. . . . . . . . 9
                                                  
    |
260 | 259 | fveq1d 5867 |
. . . . . . . 8
                                                               |
261 | 231, 260 | oveq12d 6308 |
. . . . . . 7
                                                                       
       
               
         
                                          |
262 | 261 | oveq2d 6306 |
. . . . . 6
                         
                                                                                      
                                 
         |
263 | 90 | adantlr 721 |
. . . . . . . 8
                   |
264 | | ovex 6318 |
. . . . . . . . . . . 12
   |
265 | | eleq1 2517 |
. . . . . . . . . . . . . 14
       
         |
266 | 265 | anbi2d 710 |
. . . . . . . . . . . . 13
    
    
           |
267 | 240 | feq1d 5714 |
. . . . . . . . . . . . 13
                               
         |
268 | 266, 267 | imbi12d 322 |
. . . . . . . . . . . 12
     
                     
        
                      |
269 | | eleq1 2517 |
. . . . . . . . . . . . . . 15
     
       |
270 | 269 | anbi2d 710 |
. . . . . . . . . . . . . 14
  
    
         |
271 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
                           |
272 | 271 | feq1d 5714 |
. . . . . . . . . . . . . 14
                                     |
273 | 270, 272 | imbi12d 322 |
. . . . . . . . . . . . 13
   
                     
      
                    |
274 | 273, 196 | chvarv 2107 |
. . . . . . . . . . . 12
 
                       |
275 | 264, 268,
274 | vtocl 3100 |
. . . . . . . . . . 11
 
                  
        |
276 | 182, 255,
275 | syl2anc 667 |
. . . . . . . . . 10
 
                
        |
277 | 276 | adantlr 721 |
. . . . . . . . 9
                    
        |
278 | 277, 227 | ffvelrnd 6023 |
. . . . . . . 8
                     
       |
279 | | anass 655 |
. . . . . . . . . . . 12
        
          |
280 | | ancom 452 |
. . . . . . . . . . . . . 14
     
 
       |
281 | 280 | anbi2i 700 |
. . . . . . . . . . . . 13
 
    
 
 
        |
282 | | anass 655 |
. . . . . . . . . . . . . 14
        
 
        |
283 | 282 | bicomi 206 |
. . . . . . . . . . . . 13
 

     
  
       |
284 | 281, 283 | bitri 253 |
. . . . . . . . . . . 12
 
    
 
  
       |
285 | 279, 284 | bitri 253 |
. . . . . . . . . . 11
        
  
       |
286 | 285 | anbi1i 701 |
. . . . . . . . . 10
   
     
        
  
                 |
287 | 286 | imbi1i 327 |
. . . . . . . . 9
          
                                               
   

             
      
         
                        |
288 | 153, 287 | mpbi 212 |
. . . . . . . 8
   

             
      
         
                       |
289 | 263, 278,
288 | fsummulc1 13846 |
. . . . . . 7
                                                                                                        
                                 
        |
290 | 289 | oveq2d 6306 |
. . . . . 6
             
               
         
                                                                       
                                 
         |
291 | 182, 45 | syl 17 |
. . . . . . . . . 10
 
       |
292 | 291, 162 | bccld 37537 |
. . . . . . . . 9
 
         |
293 | 292 | nn0cnd 10927 |
. . . . . . . 8
 
         |
294 | 293 | adantlr 721 |
. . . . . . 7
             |
295 | 278 | adantr 467 |
. . . . . . . 8
   

             
            
       |
296 | 288, 295 | mulcld 9663 |
. . . . . . 7
   

             
                                                            |
297 | 263, 294,
296 | fsummulc2 13845 |
. . . . . 6
                             
         
                                                                       
                                 
         |
298 | 262, 290,
297 | 3eqtrd 2489 |
. . . . 5
                         
                                                                                      
                                 
         |
299 | 298 | sumeq2dv 13769 |
. . . 4
 
                       
                                                                                            
                                 
         |
300 | | vex 3048 |
. . . . . . . 8
 |
301 | | vex 3048 |
. . . . . . . 8
 |
302 | 300, 301 | op1std 6803 |
. . . . . . 7
          |
303 | 302 | oveq2d 6306 |
. . . . . 6
              |
304 | 302 | fveq2d 5869 |
. . . . . . . . 9
                  |
305 | 300, 301 | op2ndd 6804 |
. . . . . . . . . . . 12
          |
306 | 305 | fveq1d 5867 |
. . . . . . . . . . 11
                  |
307 | 306 | fveq2d 5869 |
. . . . . . . . . 10
                          |
308 | 307 | prodeq2ad 37672 |
. . . . . . . . 9
                            |
309 | 304, 308 | oveq12d 6308 |
. . . . . . . 8
                                            |
310 | 306 | fveq2d 5869 |
. . . . . . . . . 10
                                          |
311 | 310 | fveq1d 5867 |
. . . . . . . . 9
                                                  |
312 | 311 | prodeq2ad 37672 |
. . . . . . . 8
                             
                      |
313 | 309, 312 | oveq12d 6308 |
. . . . . . 7
                            
                               
         
                       |
314 | 302 | oveq2d 6306 |
. . . . . . . . 9
              |
315 | 314 | fveq2d 5869 |
. . . . . . . 8
                                 
    |
316 | 315 | fveq1d 5867 |
. . . . . . 7
                                      
       |
317 | 313, 316 | oveq12d 6308 |
. . . . . 6
                             
                                     
                 
         
                                          |
318 | 303, 317 | oveq12d 6308 |
. . . . 5
                                    
                                     
                                                                           |
319 | | fzfid 12186 |
. . . . 5
 
       |
320 | 294 | adantrr 723 |
. . . . . 6
        
              |
321 | 296 | anasss 653 |
. . . . . 6
        
                 
         
                                          |
322 | 320, 321 | mulcld 9663 |
. . . . 5
        
                              
                                 
         |
323 | 318, 319,
263, 322 | fsum2d 13832 |
. . . 4
 
                                     
                                 
       
                                    
                                                   
             |
324 | | ovex 6318 |
. . . . . . . . 9
       |
325 | 301 | resex 5148 |
. . . . . . . . 9
  |