Step | Hyp | Ref
| Expression |
1 | | ovex 6336 |
. . . . . . . 8
     |
2 | 1 | mptex 6152 |
. . . . . . 7
               |
3 | | fmuldfeqlem1.6 |
. . . . . . . 8
                 |
4 | 3 | fvmpt2 5972 |
. . . . . . 7
                                     |
5 | 2, 4 | mpan2 685 |
. . . . . 6
                     |
6 | | fveq2 5879 |
. . . . . . . 8
           |
7 | 6 | fveq1d 5881 |
. . . . . . 7
                   |
8 | 7 | cbvmptv 4488 |
. . . . . 6
                             |
9 | 5, 8 | syl6eq 2521 |
. . . . 5
                     |
10 | 9 | adantl 473 |
. . . 4
 
                     |
11 | | fveq2 5879 |
. . . . . 6
          
    |
12 | 11 | fveq1d 5881 |
. . . . 5
                       |
13 | 12 | adantl 473 |
. . . 4
                           |
14 | | fmuldfeqlem1.11 |
. . . . 5
         |
15 | 14 | adantr 472 |
. . . 4
 
 
       |
16 | | fmuldfeqlem1.8 |
. . . . . . 7
           |
17 | 16, 14 | ffvelrnd 6038 |
. . . . . 6
    
    |
18 | 17 | ancli 560 |
. . . . . 6
           |
19 | | nfcv 2612 |
. . . . . . 7
     
   |
20 | | fmuldfeqlem1.1 |
. . . . . . . . 9
   |
21 | | nfv 1769 |
. . . . . . . . 9
     
   |
22 | 20, 21 | nfan 2031 |
. . . . . . . 8
           |
23 | | nfv 1769 |
. . . . . . . 8
     
       |
24 | 22, 23 | nfim 2023 |
. . . . . . 7
              
        |
25 | | eleq1 2537 |
. . . . . . . . 9
    
  
         |
26 | 25 | anbi2d 718 |
. . . . . . . 8
    
   

    
      |
27 | | feq1 5720 |
. . . . . . . 8
    
      
             |
28 | 26, 27 | imbi12d 327 |
. . . . . . 7
    
    
                  
          |
29 | | fmuldfeqlem1.13 |
. . . . . . 7
 
       |
30 | 19, 24, 28, 29 | vtoclgf 3091 |
. . . . . 6
        
          
         |
31 | 17, 18, 30 | sylc 61 |
. . . . 5
    
        |
32 | 31 | fnvinran 37398 |
. . . 4
 
     
       |
33 | 10, 13, 15, 32 | fvmptd 5969 |
. . 3
 
                       |
34 | 33 | oveq2d 6324 |
. 2
 
                                      
        |
35 | | fmuldfeqlem1.10 |
. . . . 5
       |
36 | | elfzuz 11822 |
. . . . 5
           |
37 | 35, 36 | syl 17 |
. . . 4
       |
38 | | seqp1 12266 |
. . . 4
    
         
                          |
39 | 37, 38 | syl 17 |
. . 3
                               
     |
40 | 39 | adantr 472 |
. 2
 
          
                          |
41 | | seqp1 12266 |
. . . . . 6
    
       
                      |
42 | 37, 41 | syl 17 |
. . . . 5
                         
     |
43 | | fmuldfeqlem1.5 |
. . . . . . . 8
 
              |
44 | | nfcv 2612 |
. . . . . . . . 9
               |
45 | | nfcv 2612 |
. . . . . . . . 9
               |
46 | | nfcv 2612 |
. . . . . . . . 9
               |
47 | | nfcv 2612 |
. . . . . . . . 9
               |
48 | | fveq1 5878 |
. . . . . . . . . . 11
           |
49 | | fveq1 5878 |
. . . . . . . . . . 11
           |
50 | 48, 49 | oveqan12d 6327 |
. . . . . . . . . 10
 
                       |
51 | 50 | mpteq2dv 4483 |
. . . . . . . . 9
 
                           |
52 | 44, 45, 46, 47, 51 | cbvmpt2 6389 |
. . . . . . . 8
                               |
53 | 43, 52 | eqtri 2493 |
. . . . . . 7
 
              |
54 | 53 | a1i 11 |
. . . . . 6
                  |
55 | | nfcv 2612 |
. . . . . . . . . . . 12
   |
56 | | fmuldfeqlem1.3 |
. . . . . . . . . . . . . 14
   |
57 | | nfmpt1 4485 |
. . . . . . . . . . . . . 14
               |
58 | 56, 56, 57 | nfmpt2 6379 |
. . . . . . . . . . . . 13
   
              |
59 | 43, 58 | nfcxfr 2610 |
. . . . . . . . . . . 12
   |
60 | | nfcv 2612 |
. . . . . . . . . . . 12
   |
61 | 55, 59, 60 | nfseq 12261 |
. . . . . . . . . . 11
       |
62 | | nfcv 2612 |
. . . . . . . . . . 11
   |
63 | 61, 62 | nffv 5886 |
. . . . . . . . . 10
           |
64 | 63 | nfeq2 2627 |
. . . . . . . . 9
          |
65 | | nfv 1769 |
. . . . . . . . 9
        |
66 | 64, 65 | nfan 2031 |
. . . . . . . 8
              
    |
67 | | fveq1 5878 |
. . . . . . . . . 10
                           |
68 | 67 | ad2antrr 740 |
. . . . . . . . 9
              
  
                   |
69 | | fveq1 5878 |
. . . . . . . . . 10
    
                  |
70 | 69 | ad2antlr 741 |
. . . . . . . . 9
              
  
                 |
71 | 68, 70 | oveq12d 6326 |
. . . . . . . 8
              
  
                            
        |
72 | 66, 71 | mpteq2da 4481 |
. . . . . . 7
         
      

                                       |
73 | 72 | adantl 473 |
. . . . . 6
 

       
                                      
         |
74 | | eqid 2471 |
. . . . . . 7
                 |
75 | | 3simpc 1029 |
. . . . . . . 8
 


   |
76 | | nfcv 2612 |
. . . . . . . . 9
   |
77 | | nfcv 2612 |
. . . . . . . . 9
   |
78 | | nfcv 2612 |
. . . . . . . . 9
   |
79 | | nfv 1769 |
. . . . . . . . . . 11
  |
80 | | nfv 1769 |
. . . . . . . . . . 11
  |
81 | 20, 79, 80 | nf3an 2033 |
. . . . . . . . . 10
  
  |
82 | | nfv 1769 |
. . . . . . . . . 10
               |
83 | 81, 82 | nfim 2023 |
. . . . . . . . 9
   
               |
84 | | fmuldfeqlem1.2 |
. . . . . . . . . . 11
   |
85 | | nfv 1769 |
. . . . . . . . . . 11
  |
86 | | nfv 1769 |
. . . . . . . . . . 11
  |
87 | 84, 85, 86 | nf3an 2033 |
. . . . . . . . . 10
  
  |
88 | | nfv 1769 |
. . . . . . . . . 10
               |
89 | 87, 88 | nfim 2023 |
. . . . . . . . 9
   
               |
90 | | eleq1 2537 |
. . . . . . . . . . 11
 
   |
91 | 90 | 3anbi2d 1370 |
. . . . . . . . . 10
  


    |
92 | 48 | oveq1d 6323 |
. . . . . . . . . . . 12
                       |
93 | 92 | mpteq2dv 4483 |
. . . . . . . . . . 11
                           |
94 | 93 | eleq1d 2533 |
. . . . . . . . . 10
                             |
95 | 91, 94 | imbi12d 327 |
. . . . . . . . 9
   
               
                 |
96 | | eleq1 2537 |
. . . . . . . . . . 11
 
   |
97 | 96 | 3anbi3d 1371 |
. . . . . . . . . 10
  


    |
98 | 49 | oveq2d 6324 |
. . . . . . . . . . . 12
                       |
99 | 98 | mpteq2dv 4483 |
. . . . . . . . . . 11
                           |
100 | 99 | eleq1d 2533 |
. . . . . . . . . 10
                             |
101 | 97, 100 | imbi12d 327 |
. . . . . . . . 9
   
               
                 |
102 | | fmuldfeqlem1.9 |
. . . . . . . . 9
 


             |
103 | 76, 77, 78, 83, 89, 95, 101, 102 | vtocl2gf 3095 |
. . . . . . . 8
 
  
                |
104 | 75, 103 | mpcom 36 |
. . . . . . 7
 


             |
105 | | fmuldfeqlem1.7 |
. . . . . . 7
   |
106 | 53, 74, 35, 16, 104, 105 | fmulcl 37756 |
. . . . . 6
           |
107 | | mptexg 6151 |
. . . . . . 7
                   
         |
108 | 105, 107 | syl 17 |
. . . . . 6
                   
         |
109 | 54, 73, 106, 17, 108 | ovmpt2d 6443 |
. . . . 5
               
                     
         |
110 | 42, 109 | eqtrd 2505 |
. . . 4
                             
         |
111 | 106 | ancli 560 |
. . . . . . 7
             |
112 | | nfcv 2612 |
. . . . . . . . . 10
   |
113 | | nfmpt21 6377 |
. . . . . . . . . . 11
   
              |
114 | 43, 113 | nfcxfr 2610 |
. . . . . . . . . 10
   |
115 | | nfcv 2612 |
. . . . . . . . . 10
   |
116 | 112, 114,
115 | nfseq 12261 |
. . . . . . . . 9
       |
117 | | nfcv 2612 |
. . . . . . . . 9
   |
118 | 116, 117 | nffv 5886 |
. . . . . . . 8
           |
119 | 118 | nfel1 2626 |
. . . . . . . . . 10
           |
120 | 20, 119 | nfan 2031 |
. . . . . . . . 9
             |
121 | | nfcv 2612 |
. . . . . . . . . 10
   |
122 | | nfcv 2612 |
. . . . . . . . . 10
   |
123 | 118, 121,
122 | nff 5735 |
. . . . . . . . 9
               |
124 | 120, 123 | nfim 2023 |
. . . . . . . 8
            
              |
125 | | eleq1 2537 |
. . . . . . . . . 10
                     |
126 | 125 | anbi2d 718 |
. . . . . . . . 9
          
 
            |
127 | | feq1 5720 |
. . . . . . . . 9
                             |
128 | 126, 127 | imbi12d 327 |
. . . . . . . 8
                 
                           |
129 | 118, 124,
128, 29 | vtoclgf 3091 |
. . . . . . 7
                   
               |
130 | 106, 111,
129 | sylc 61 |
. . . . . 6
               |
131 | 130 | fnvinran 37398 |
. . . . 5
 
               |
132 | 131, 32 | remulcld 9689 |
. . . 4
 
                  
        |
133 | 110, 132 | fvmpt2d 5974 |
. . 3
 
         
                      
        |
134 | | fmuldfeqlem1.12 |
. . . . 5
                         |
135 | 134 | oveq1d 6323 |
. . . 4
                  
                     
        |
136 | 135 | adantr 472 |
. . 3
 
                  
                     
        |
137 | 133, 136 | eqtrd 2505 |
. 2
 
         
                    
        |
138 | 34, 40, 137 | 3eqtr4rd 2516 |
1
 
         
              
    |