Step | Hyp | Ref
| Expression |
1 | | prodeq1 13963 |
. . . . . . . . 9


                   |
2 | 1 | mpteq2dv 4490 |
. . . . . . . 8

 
          
           |
3 | 2 | oveq2d 6306 |
. . . . . . 7

    
                           |
4 | 3 | fveq1d 5867 |
. . . . . 6

                                        |
5 | | fveq2 5865 |
. . . . . . . . . 10

          |
6 | 5 | fveq1d 5867 |
. . . . . . . . 9

                  |
7 | 6 | sumeq1d 13767 |
. . . . . . . 8

                                                                          
                       |
8 | | prodeq1 13963 |
. . . . . . . . . . 11


                   |
9 | 8 | oveq2d 6306 |
. . . . . . . . . 10

                                |
10 | | prodeq1 13963 |
. . . . . . . . . 10


                                           |
11 | 9, 10 | oveq12d 6308 |
. . . . . . . . 9

      
         
                                                             |
12 | 11 | sumeq2ad 37644 |
. . . . . . . 8

                          
                                                                       |
13 | 7, 12 | eqtrd 2485 |
. . . . . . 7

                                                                                                  |
14 | 13 | mpteq2dv 4490 |
. . . . . 6

                                                                             
                        |
15 | 4, 14 | eqeq12d 2466 |
. . . . 5

      
                                                                                                             
                         |
16 | 15 | ralbidv 2827 |
. . . 4

 
          
                                                               
          
                                        
                         |
17 | | prodeq1 13963 |
. . . . . . . . 9
          
          |
18 | 17 | mpteq2dv 4490 |
. . . . . . . 8
             
           |
19 | 18 | oveq2d 6306 |
. . . . . . 7
     
                           |
20 | 19 | fveq1d 5867 |
. . . . . 6
      
                  
               |
21 | | fveq2 5865 |
. . . . . . . . . 10
           |
22 | 21 | fveq1d 5867 |
. . . . . . . . 9
                   |
23 | 22 | sumeq1d 13767 |
. . . . . . . 8
                                                                                                   |
24 | | prodeq1 13963 |
. . . . . . . . . . 11
          
          |
25 | 24 | oveq2d 6306 |
. . . . . . . . . 10
      
                          |
26 | | prodeq1 13963 |
. . . . . . . . . 10
                                             |
27 | 25, 26 | oveq12d 6308 |
. . . . . . . . 9
                                                       
                       |
28 | 27 | sumeq2ad 37644 |
. . . . . . . 8
                                                                                                   |
29 | 23, 28 | eqtrd 2485 |
. . . . . . 7
                                                                                                   |
30 | 29 | mpteq2dv 4490 |
. . . . . 6
                                                                              
                        |
31 | 20, 30 | eqeq12d 2466 |
. . . . 5
                                                                                                                                               |
32 | 31 | ralbidv 2827 |
. . . 4
  
          
                                                               
          
                                                                  |
33 | | prodeq1 13963 |
. . . . . . . . 9
                              |
34 | 33 | mpteq2dv 4490 |
. . . . . . . 8
                                  |
35 | 34 | oveq2d 6306 |
. . . . . . 7
                        
                 |
36 | 35 | fveq1d 5867 |
. . . . . 6
          
                                       |
37 | | fveq2 5865 |
. . . . . . . . . 10
                   |
38 | 37 | fveq1d 5867 |
. . . . . . . . 9
                           |
39 | 38 | sumeq1d 13767 |
. . . . . . . 8
                               
                                                                           |
40 | | prodeq1 13963 |
. . . . . . . . . . 11
                              |
41 | 40 | oveq2d 6306 |
. . . . . . . . . 10
                                          |
42 | | prodeq1 13963 |
. . . . . . . . . 10
                                                      |
43 | 41, 42 | oveq12d 6308 |
. . . . . . . . 9
                                                                                             |
44 | 43 | sumeq2ad 37644 |
. . . . . . . 8
                         
         
                                                                                     |
45 | 39, 44 | eqtrd 2485 |
. . . . . . 7
                               
                                                                                     |
46 | 45 | mpteq2dv 4490 |
. . . . . 6
                                
                                                                                        |
47 | 36, 46 | eqeq12d 2466 |
. . . . 5
                                                                          
                                                                                           |
48 | 47 | ralbidv 2827 |
. . . 4
                 
                                        
                     
                                                                                                 |
49 | | prodeq1 13963 |
. . . . . . . . . 10
          
          |
50 | 49 | mpteq2dv 4490 |
. . . . . . . . 9
             
           |
51 | | dvnprodlem3.f |
. . . . . . . . . . 11
 
          |
52 | 51 | a1i 11 |
. . . . . . . . . 10
              |
53 | 52 | eqcomd 2457 |
. . . . . . . . 9
              |
54 | 50, 53 | eqtrd 2485 |
. . . . . . . 8
              |
55 | 54 | oveq2d 6306 |
. . . . . . 7
     
                |
56 | 55 | fveq1d 5867 |
. . . . . 6
      
                       |
57 | | fveq2 5865 |
. . . . . . . . . 10
           |
58 | 57 | fveq1d 5867 |
. . . . . . . . 9
                   |
59 | 58 | sumeq1d 13767 |
. . . . . . . 8
                                                                                                   |
60 | | prodeq1 13963 |
. . . . . . . . . . 11
          
          |
61 | 60 | oveq2d 6306 |
. . . . . . . . . 10
      
                          |
62 | | prodeq1 13963 |
. . . . . . . . . 10
                                             |
63 | 61, 62 | oveq12d 6308 |
. . . . . . . . 9
                                                       
                       |
64 | 63 | sumeq2ad 37644 |
. . . . . . . 8
                                                                           
                       |
65 | 59, 64 | eqtrd 2485 |
. . . . . . 7
                                                                           
                       |
66 | 65 | mpteq2dv 4490 |
. . . . . 6
                                                                              
                        |
67 | 56, 66 | eqeq12d 2466 |
. . . . 5
                                                                                                                                    |
68 | 67 | ralbidv 2827 |
. . . 4
  
          
                                                               
                                        
                         |
69 | | prod0 13997 |
. . . . . . . . . . . . 13
          |
70 | 69 | mpteq2i 4486 |
. . . . . . . . . . . 12
              |
71 | 70 | oveq2i 6301 |
. . . . . . . . . . 11
                      |
72 | 71 | a1i 11 |
. . . . . . . . . 10
                        |
73 | | id 22 |
. . . . . . . . . 10
   |
74 | 72, 73 | fveq12d 5871 |
. . . . . . . . 9
      
                         |
75 | 74 | adantl 468 |
. . . . . . . 8
 
      
                         |
76 | | dvnprodlem3.s |
. . . . . . . . . . 11
      |
77 | | recnprss 22859 |
. . . . . . . . . . 11
   
  |
78 | 76, 77 | syl 17 |
. . . . . . . . . 10

  |
79 | | 1cnd 9659 |
. . . . . . . . . . . . . 14
 
   |
80 | | eqid 2451 |
. . . . . . . . . . . . . 14
     |
81 | 79, 80 | fmptd 6046 |
. . . . . . . . . . . . 13
         |
82 | | 1re 9642 |
. . . . . . . . . . . . . . . . 17
 |
83 | 82 | rgenw 2749 |
. . . . . . . . . . . . . . . 16

 |
84 | | dmmptg 5332 |
. . . . . . . . . . . . . . . 16
 
    |
85 | 83, 84 | ax-mp 5 |
. . . . . . . . . . . . . . 15
   |
86 | 85 | a1i 11 |
. . . . . . . . . . . . . 14
     |
87 | 86 | feq2d 5715 |
. . . . . . . . . . . . 13
                   |
88 | 81, 87 | mpbird 236 |
. . . . . . . . . . . 12
     
     |
89 | | restsspw 15330 |
. . . . . . . . . . . . . . 15
   ℂfld ↾t    |
90 | | dvnprodlem3.x |
. . . . . . . . . . . . . . 15
    ℂfld ↾t    |
91 | 89, 90 | sseldi 3430 |
. . . . . . . . . . . . . 14
    |
92 | | elpwi 3960 |
. . . . . . . . . . . . . 14
    |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . 13

  |
94 | 86, 93 | eqsstrd 3466 |
. . . . . . . . . . . 12
     |
95 | 88, 94 | jca 535 |
. . . . . . . . . . 11
         

    |
96 | | cnex 9620 |
. . . . . . . . . . . . 13
 |
97 | 96 | a1i 11 |
. . . . . . . . . . . 12
   |
98 | | elpm2g 7488 |
. . . . . . . . . . . 12
 
                   
    |
99 | 97, 76, 98 | syl2anc 667 |
. . . . . . . . . . 11
                
    |
100 | 95, 99 | mpbird 236 |
. . . . . . . . . 10
   
   |
101 | | dvn0 22878 |
. . . . . . . . . 10
 
                   |
102 | 78, 100, 101 | syl2anc 667 |
. . . . . . . . 9
               |
103 | 102 | adantr 467 |
. . . . . . . 8
 
               |
104 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
                   |
105 | 104 | adantl 468 |
. . . . . . . . . . . . . 14
 
                   |
106 | | dvnprodlem3.d |
. . . . . . . . . . . . . . . . . 18
          
        |
107 | 106 | a1i 11 |
. . . . . . . . . . . . . . . . 17
           
         |
108 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . . . . . 22

              |
109 | | elmapfn 7494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      
  |
110 | | fn0 5695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

  |
111 | 109, 110 | sylib 200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
      
  |
112 | | elsn 3982 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
  |
113 | 111, 112 | sylibr 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      
    |
114 | 112 | biimpi 198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     |
115 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

  |
116 | | f0 5764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
         |
117 | | ovex 6318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     |
118 | | 0ex 4535 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 |
119 | 117, 118 | elmap 7500 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
      
          |
120 | 116, 119 | mpbir 213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
  |
121 | 120 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

    
   |
122 | 115, 121 | eqeltrd 2529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

        |
123 | 114, 122 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
124 | 113, 123 | impbii 191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
    |
125 | 124 | ax-gen 1669 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       

    |
126 | | dfcleq 2445 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
  
       

     |
127 | 125, 126 | mpbir 213 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
128 | 127 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22

          |
129 | 108, 128 | eqtrd 2485 |
. . . . . . . . . . . . . . . . . . . . 21

          |
130 | | rabeq 3038 |
. . . . . . . . . . . . . . . . . . . . 21
     
          
                |
131 | 129, 130 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20

       
                |
132 | | sumeq1 13755 |
. . . . . . . . . . . . . . . . . . . . . 22


    
      |
133 | 132 | eqeq1d 2453 |
. . . . . . . . . . . . . . . . . . . . 21

 
   
        |
134 | 133 | rabbidv 3036 |
. . . . . . . . . . . . . . . . . . . 20

                    |
135 | 131, 134 | eqtrd 2485 |
. . . . . . . . . . . . . . . . . . 19

       
                |
136 | 135 | mpteq2dv 4490 |
. . . . . . . . . . . . . . . . . 18


       
                   |
137 | 136 | adantl 468 |
. . . . . . . . . . . . . . . . 17
 

        
                   |
138 | | 0elpw 4572 |
. . . . . . . . . . . . . . . . . 18
  |
139 | 138 | a1i 11 |
. . . . . . . . . . . . . . . . 17

   |
140 | | nn0ex 10875 |
. . . . . . . . . . . . . . . . . . 19
 |
141 | 140 | mptex 6136 |
. . . . . . . . . . . . . . . . . 18

           |
142 | 141 | a1i 11 |
. . . . . . . . . . . . . . . . 17
              |
143 | 107, 137,
139, 142 | fvmptd 5954 |
. . . . . . . . . . . . . . . 16
                  |
144 | | eqeq2 2462 |
. . . . . . . . . . . . . . . . . 18
               |
145 | 144 | rabbidv 3036 |
. . . . . . . . . . . . . . . . 17
                     |
146 | 145 | adantl 468 |
. . . . . . . . . . . . . . . 16
 
                     |
147 | | 0nn0 10884 |
. . . . . . . . . . . . . . . . 17
 |
148 | 147 | a1i 11 |
. . . . . . . . . . . . . . . 16
   |
149 | | p0ex 4590 |
. . . . . . . . . . . . . . . . . 18
   |
150 | 149 | rabex 4554 |
. . . . . . . . . . . . . . . . 17
          |
151 | 150 | a1i 11 |
. . . . . . . . . . . . . . . 16
            |
152 | 143, 146,
148, 151 | fvmptd 5954 |
. . . . . . . . . . . . . . 15
            
       |
153 | 152 | adantr 467 |
. . . . . . . . . . . . . 14
 
                    |
154 | | snidg 3994 |
. . . . . . . . . . . . . . . . . . . . . 22

    |
155 | 118, 154 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
   |
156 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . . 21
 |
157 | 155, 156 | pm3.2i 457 |
. . . . . . . . . . . . . . . . . . . 20
     |
158 | | sum0 13787 |
. . . . . . . . . . . . . . . . . . . . . . 23
      |
159 | 158 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22

       |
160 | 159 | eqeq1d 2453 |
. . . . . . . . . . . . . . . . . . . . 21

 
       |
161 | 160 | elrab 3196 |
. . . . . . . . . . . . . . . . . . . 20
            
   |
162 | 157, 161 | mpbir 213 |
. . . . . . . . . . . . . . . . . . 19
          |
163 | 162 | ne0ii 3738 |
. . . . . . . . . . . . . . . . . 18
          |
164 | 163 | neii 2626 |
. . . . . . . . . . . . . . . . 17
          |
165 | | eqid 2451 |
. . . . . . . . . . . . . . . . . 18
                   |
166 | | rabrsn 4042 |
. . . . . . . . . . . . . . . . . 18
             
                             |
167 | 165, 166 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
         
             |
168 | 164, 167 | mtpor 1653 |
. . . . . . . . . . . . . . . 16
            |
169 | 168 | a1i 11 |
. . . . . . . . . . . . . . 15
 
              |
170 | | iftrue 3887 |
. . . . . . . . . . . . . . . 16
            |
171 | 170 | adantl 468 |
. . . . . . . . . . . . . . 15
 
            |
172 | 169, 171 | eqtr4d 2488 |
. . . . . . . . . . . . . 14
 
                   |
173 | 105, 153,
172 | 3eqtrd 2489 |
. . . . . . . . . . . . 13
 
                  |
174 | 173, 171 | eqtrd 2485 |
. . . . . . . . . . . 12
 
             |
175 | 174 | sumeq1d 13767 |
. . . . . . . . . . 11
 
                                                                                            |
176 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . 18
           |
177 | | fac0 12462 |
. . . . . . . . . . . . . . . . . . 19
     |
178 | 177 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
       |
179 | 176, 178 | eqtrd 2485 |
. . . . . . . . . . . . . . . . 17
       |
180 | 179 | oveq1d 6305 |
. . . . . . . . . . . . . . . 16
                             |
181 | | prod0 13997 |
. . . . . . . . . . . . . . . . . 18
          |
182 | 181 | oveq2i 6301 |
. . . . . . . . . . . . . . . . 17
              |
183 | | 1div1e1 10300 |
. . . . . . . . . . . . . . . . 17
   |
184 | 182, 183 | eqtri 2473 |
. . . . . . . . . . . . . . . 16
            |
185 | 180, 184 | syl6eq 2501 |
. . . . . . . . . . . . . . 15
                  |
186 | | prod0 13997 |
. . . . . . . . . . . . . . . 16
                      |
187 | 186 | a1i 11 |
. . . . . . . . . . . . . . 15
                        |
188 | 185, 187 | oveq12d 6308 |
. . . . . . . . . . . . . 14
                 
                         |
189 | 188 | ad2antlr 733 |
. . . . . . . . . . . . 13
   
                                             |
190 | | 1t1e1 10757 |
. . . . . . . . . . . . . 14
   |
191 | 190 | a1i 11 |
. . . . . . . . . . . . 13
   
       |
192 | 189, 191 | eqtrd 2485 |
. . . . . . . . . . . 12
   
                                           |
193 | 192 | sumeq2dv 13769 |
. . . . . . . . . . 11
 
                    
                           |
194 | | ax-1cn 9597 |
. . . . . . . . . . . . 13
 |
195 | | eqidd 2452 |
. . . . . . . . . . . . . 14

  |
196 | 195 | sumsn 13807 |
. . . . . . . . . . . . 13
 
       |
197 | 118, 194,
196 | mp2an 678 |
. . . . . . . . . . . 12
     |
198 | 197 | a1i 11 |
. . . . . . . . . . 11
 
       |
199 | 175, 193,
198 | 3eqtrd 2489 |
. . . . . . . . . 10
 
                                                   |
200 | 199 | mpteq2dv 4490 |
. . . . . . . . 9
 
                            
                          |
201 | 200 | eqcomd 2457 |
. . . . . . . 8
 
                                                       |
202 | 75, 103, 201 | 3eqtrd 2489 |
. . . . . . 7
 
      
                                        
                        |
203 | 202 | a1d 26 |
. . . . . 6
 
                                                    
                         |
204 | 71 | fveq1i 5866 |
. . . . . . . . 9
                              |
205 | 204 | a1i 11 |
. . . . . . . 8
  
     
                               |
206 | 76 | adantr 467 |
. . . . . . . . . 10
 

     |
207 | 206 | adantr 467 |
. . . . . . . . 9
  
     
     |
208 | 90 | adantr 467 |
. . . . . . . . . 10
 

   ℂfld ↾t    |
209 | 208 | adantr 467 |
. . . . . . . . 9
  
     
   ℂfld
↾t    |
210 | 194 | a1i 11 |
. . . . . . . . 9
  
     
  |
211 | | elfznn0 11887 |
. . . . . . . . . . . . 13
       |
212 | 211 | adantl 468 |
. . . . . . . . . . . 12
      
  |
213 | | neqne 37374 |
. . . . . . . . . . . . 13
   |
214 | 213 | adantr 467 |
. . . . . . . . . . . 12
      
  |
215 | 212, 214 | jca 535 |
. . . . . . . . . . 11
      
    |
216 | | elnnne0 10883 |
. . . . . . . . . . 11

    |
217 | 215, 216 | sylibr 216 |
. . . . . . . . . 10
      
  |
218 | 217 | adantll 720 |
. . . . . . . . 9
  
     
  |
219 | 207, 209,
210, 218 | dvnmptconst 37816 |
. . . . . . . 8
  
     
              |
220 | 143 | ad2antrr 732 |
. . . . . . . . . . . 12
  
     
                 |
221 | | eqeq2 2462 |
. . . . . . . . . . . . . . . . 17
               |
222 | 221 | rabbidv 3036 |
. . . . . . . . . . . . . . . 16
                     |
223 | 222 | adantl 468 |
. . . . . . . . . . . . . . 15
  
   
                |
224 | | eqidd 2452 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   
  |
225 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   
       |
226 | 225 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   
       |
227 | 158 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   
       |
228 | 224, 226,
227 | 3eqtrd 2489 |
. . . . . . . . . . . . . . . . . . . . 21
 
   
  |
229 | 228 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
            |
230 | 229 | adantll 720 |
. . . . . . . . . . . . . . . . . . 19
              |
231 | | simpll 760 |
. . . . . . . . . . . . . . . . . . 19
           
  |
232 | 230, 231 | pm2.65da 580 |
. . . . . . . . . . . . . . . . . 18
            |
233 | 232 | ralrimiva 2802 |
. . . . . . . . . . . . . . . . 17
 
         |
234 | | rabeq0 3754 |
. . . . . . . . . . . . . . . . 17
         
          |
235 | 233, 234 | sylibr 216 |
. . . . . . . . . . . . . . . 16
            |
236 | 235 | adantr 467 |
. . . . . . . . . . . . . . 15
  
   
       |
237 | 223, 236 | eqtrd 2485 |
. . . . . . . . . . . . . 14
  
   
       |
238 | 237 | adantll 720 |
. . . . . . . . . . . . 13
  
 
   
       |
239 | 238 | adantlr 721 |
. . . . . . . . . . . 12
   

                 |
240 | 211 | adantl 468 |
. . . . . . . . . . . 12
  
     
  |
241 | 118 | a1i 11 |
. . . . . . . . . . . 12
  
     
  |
242 | 220, 239,
240, 241 | fvmptd 5954 |
. . . . . . . . . . 11
  
     
          |
243 | 242 | sumeq1d 13767 |
. . . . . . . . . 10
  
     
                                                                                         |
244 | | sum0 13787 |
. . . . . . . . . . 11
                                        |
245 | 244 | a1i 11 |
. . . . . . . . . 10
  
     
                                         |
246 | 243, 245 | eqtr2d 2486 |
. . . . . . . . 9
  
     
                          
                       |
247 | 246 | mpteq2dv 4490 |
. . . . . . . 8
  
     

                            
                        |
248 | 205, 219,
247 | 3eqtrd 2489 |
. . . . . . 7
  
     
                                              
                        |
249 | 248 | ex 436 |
. . . . . 6
 
                                                    
                         |
250 | 203, 249 | pm2.61dan 800 |
. . . . 5
                                                    
                         |
251 | 250 | ralrimiv 2800 |
. . . 4
                                                     
                        |
252 | | simpll 760 |
. . . . . . . 8
    
               
                                        
                      
      
      |
253 | | fveq2 5865 |
. . . . . . . . . . . . . . . . 17
                   |
254 | 253 | prodeq2ad 37672 |
. . . . . . . . . . . . . . . 16
          
          |
255 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . 19
           |
256 | 255 | fveq1d 5867 |
. . . . . . . . . . . . . . . . . 18
                   |
257 | 256 | cbvprodv 13970 |
. . . . . . . . . . . . . . . . 17

                  |
258 | 257 | a1i 11 |
. . . . . . . . . . . . . . . 16
          
          |
259 | 254, 258 | eqtrd 2485 |
. . . . . . . . . . . . . . 15
          
          |
260 | 259 | cbvmptv 4495 |
. . . . . . . . . . . . . 14
 
          
          |
261 | 260 | oveq2i 6301 |
. . . . . . . . . . . . 13
    
                          |
262 | 261 | fveq1i 5866 |
. . . . . . . . . . . 12
                                       |
263 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . 20
           |
264 | 263 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . 19
                   |
265 | 264 | cbvprodv 13970 |
. . . . . . . . . . . . . . . . . 18

                  |
266 | 265 | oveq2i 6301 |
. . . . . . . . . . . . . . . . 17
                    
          |
267 | 266 | a1i 11 |
. . . . . . . . . . . . . . . 16
      
                          |
268 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . 18
                                           |
269 | 268 | prodeq2ad 37672 |
. . . . . . . . . . . . . . . . 17
                                             |
270 | 255 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . . . 21
                   |
271 | 270, 263 | fveq12d 5871 |
. . . . . . . . . . . . . . . . . . . 20
                                   |
272 | 271 | fveq1d 5867 |
. . . . . . . . . . . . . . . . . . 19
                                           |
273 | 272 | cbvprodv 13970 |
. . . . . . . . . . . . . . . . . 18

                                          |
274 | 273 | a1i 11 |
. . . . . . . . . . . . . . . . 17
                                             |
275 | 269, 274 | eqtrd 2485 |
. . . . . . . . . . . . . . . 16
                                             |
276 | 267, 275 | oveq12d 6308 |
. . . . . . . . . . . . . . 15
                                                       
                       |
277 | 276 | sumeq2ad 37644 |
. . . . . . . . . . . . . 14
                                                                                                   |
278 | | fveq1 5864 |
. . . . . . . . . . . . . . . . . . . 20
           |
279 | 278 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . 19
                   |
280 | 279 | prodeq2ad 37672 |
. . . . . . . . . . . . . . . . . 18
          
          |
281 | 280 | oveq2d 6306 |
. . . . . . . . . . . . . . . . 17
      
                          |
282 | 278 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . 19
                                   |
283 | 282 | fveq1d 5867 |
. . . . . . . . . . . . . . . . . 18
                                           |
284 | 283 | prodeq2ad 37672 |
. . . . . . . . . . . . . . . . 17
                                             |
285 | 281, 284 | oveq12d 6308 |
. . . . . . . . . . . . . . . 16
                                                       
                       |
286 | 285 | cbvsumv 13762 |
. . . . . . . . . . . . . . 15
                                                                                                 |
287 | 286 | a1i 11 |
. . . . . . . . . . . . . 14
                                                                                                   |
288 | 277, 287 | eqtrd 2485 |
. . . . . . . . . . . . 13
                                                                                                   |
289 | 288 | cbvmptv 4495 |
. . . . . . . . . . . 12
                                                                                                     |
290 | 262, 289 | eqeq12i 2465 |
. . . . . . . . . . 11
      
                                                                                                                                      |
291 | 290 | ralbii 2819 |
. . . . . . . . . 10
 
          
                                                               
          
                                                                 |
292 | 291 | biimpi 198 |
. . . . . . . . 9
 
          
                                                                                                                                            |
293 | 292 | ad2antlr 733 |
. . . . . . . 8
    
               
                                        
                      
                                                                                  |
294 | | simpr 463 |
. . . . . . . 8
    
               
                                        
                      
           |
295 | 76 | ad3antrrr 736 |
. . . . . . . . 9
    
               
                                        
                      
      
   |
296 | 90 | ad3antrrr 736 |
. . . . . . . . 9
    
               
                                        
                      
        ℂfld
↾t    |
297 | | dvnprodlem3.t |
. . . . . . . . . 10
   |
298 | 297 | ad3antrrr 736 |
. . . . . . . . 9
    
               
                                        
                      
       |
299 | | simp-4l 776 |
. . . . . . . . . 10
     
               
                            ![]() |