Proof of Theorem dvmptfprodlem
Step | Hyp | Ref
| Expression |
1 | | dvmptfprodlem.xph |
. . . 4
   |
2 | | dvmptfprodlem.iph |
. . . . . . 7
   |
3 | | nfcv 2592 |
. . . . . . . 8
   |
4 | | nfcv 2592 |
. . . . . . . 8
   |
5 | 3, 4 | nfel 2604 |
. . . . . . 7
  |
6 | 2, 5 | nfan 2011 |
. . . . . 6
     |
7 | | dvmptfprodlem.if |
. . . . . . 7
   |
8 | 7 | a1i 11 |
. . . . . 6
 
     |
9 | | dvmptfprodlem.d |
. . . . . . . 8
   |
10 | | snfi 7650 |
. . . . . . . . 9
 
 |
11 | 10 | a1i 11 |
. . . . . . . 8
     |
12 | | unfi 7838 |
. . . . . . . 8
           |
13 | 9, 11, 12 | syl2anc 667 |
. . . . . . 7
       |
14 | 13 | adantr 467 |
. . . . . 6
 
 
     |
15 | | simpll 760 |
. . . . . . 7
           |
16 | | dvmptfprodlem.ss |
. . . . . . . . 9
       |
17 | 16 | sselda 3432 |
. . . . . . . 8
 

      |
18 | 17 | adantlr 721 |
. . . . . . 7
           |
19 | | simplr 762 |
. . . . . . 7
        
  |
20 | | dvmptfprodlem.a |
. . . . . . 7
 

  |
21 | 15, 18, 19, 20 | syl3anc 1268 |
. . . . . 6
        
  |
22 | | dvmptfprodlem.e |
. . . . . . . . 9
   |
23 | | snidg 3994 |
. . . . . . . . 9
     |
24 | 22, 23 | syl 17 |
. . . . . . . 8
     |
25 | | elun2 3602 |
. . . . . . . 8
         |
26 | 24, 25 | syl 17 |
. . . . . . 7
       |
27 | 26 | adantr 467 |
. . . . . 6
 
       |
28 | | dvmptfprodlem.f |
. . . . . . 7
   |
29 | 28 | adantl 468 |
. . . . . 6
       |
30 | 6, 8, 14, 21, 27, 29 | fprodsplit1f 14044 |
. . . . 5
 
                     |
31 | | difundir 3696 |
. . . . . . . . . 10
                     |
32 | 31 | a1i 11 |
. . . . . . . . 9
                       |
33 | | dvmptfprodlem.db |
. . . . . . . . . . 11
   |
34 | | difsn 4106 |
. . . . . . . . . . 11
       |
35 | 33, 34 | syl 17 |
. . . . . . . . . 10
       |
36 | | difid 3835 |
. . . . . . . . . . 11
       |
37 | 36 | a1i 11 |
. . . . . . . . . 10
         |
38 | 35, 37 | uneq12d 3589 |
. . . . . . . . 9
                 |
39 | | un0 3759 |
. . . . . . . . . 10
   |
40 | 39 | a1i 11 |
. . . . . . . . 9
     |
41 | 32, 38, 40 | 3eqtrd 2489 |
. . . . . . . 8
           |
42 | 41 | prodeq1d 13975 |
. . . . . . 7
           
  |
43 | 42 | oveq2d 6306 |
. . . . . 6
       
          |
44 | 43 | adantr 467 |
. . . . 5
 
 
                |
45 | 30, 44 | eqtrd 2485 |
. . . 4
 
            |
46 | 1, 45 | mpteq2da 4488 |
. . 3
  

            |
47 | 46 | oveq2d 6306 |
. 2
            
       |
48 | | dvmptfprodlem.s |
. . 3
      |
49 | 16, 26 | sseldd 3433 |
. . . . 5
   |
50 | 49 | adantr 467 |
. . . 4
 
   |
51 | | simpl 459 |
. . . . 5
 
   |
52 | | simpr 463 |
. . . . 5
 
   |
53 | 51, 50, 52 | 3jca 1188 |
. . . 4
 
 
   |
54 | | nfcv 2592 |
. . . . 5
   |
55 | | nfv 1761 |
. . . . . . 7
  |
56 | 2, 55, 5 | nf3an 2013 |
. . . . . 6
  
  |
57 | | nfcv 2592 |
. . . . . . 7
   |
58 | 7, 57 | nfel 2604 |
. . . . . 6
  |
59 | 56, 58 | nfim 2003 |
. . . . 5
   
   |
60 | | ancom 452 |
. . . . . . . . . . . . 13
    

     |
61 | 60 | imbi1i 327 |
. . . . . . . . . . . 12
   



    
   |
62 | | eqcom 2458 |
. . . . . . . . . . . . 13

  |
63 | 62 | imbi2i 314 |
. . . . . . . . . . . 12
   
 

    
   |
64 | 61, 63 | bitri 253 |
. . . . . . . . . . 11
   



    
   |
65 | 29, 64 | mpbi 212 |
. . . . . . . . . 10
    
  |
66 | 65 | 3adantr2 1168 |
. . . . . . . . 9
    
  |
67 | 66 | 3adant2 1027 |
. . . . . . . 8
   
  
 
  |
68 | | simp3 1010 |
. . . . . . . . 9
   
  
 

   |
69 | | eleq1 2517 |
. . . . . . . . . . . . 13
 
   |
70 | 69 | 3anbi2d 1344 |
. . . . . . . . . . . 12
  


    |
71 | 70 | imbi1d 319 |
. . . . . . . . . . 11
   
   
     |
72 | 71 | biimpa 487 |
. . . . . . . . . 10
   
  
 

   |
73 | 72 | 3adant3 1028 |
. . . . . . . . 9
   
  
 
 

   |
74 | 68, 73 | mpd 15 |
. . . . . . . 8
   
  
 
  |
75 | 67, 74 | eqeltrd 2529 |
. . . . . . 7
   
  
 
  |
76 | 75 | 3exp 1207 |
. . . . . 6
   
   
     |
77 | 20 | 2a1i 12 |
. . . . . 6
   
   
     |
78 | 76, 77 | impbid 194 |
. . . . 5
   
   
     |
79 | 54, 59, 78, 20 | vtoclgf 3105 |
. . . 4
  
    |
80 | 50, 53, 79 | sylc 62 |
. . 3
 
   |
81 | | dvmptfprodlem.14 |
. . 3
 
   |
82 | | dvmptfprodlem.dvf |
. . 3
         |
83 | 51, 9 | syl 17 |
. . . 4
 
   |
84 | 51 | adantr 467 |
. . . . 5
       |
85 | 16 | adantr 467 |
. . . . . . 7
 
 
     |
86 | | elun1 3601 |
. . . . . . . 8
       |
87 | 86 | adantl 468 |
. . . . . . 7
 
       |
88 | 85, 87 | sseldd 3433 |
. . . . . 6
 
   |
89 | 88 | adantlr 721 |
. . . . 5
       |
90 | 52 | adantr 467 |
. . . . 5
       |
91 | 84, 89, 90, 20 | syl3anc 1268 |
. . . 4
       |
92 | 6, 83, 91 | fprodclf 14046 |
. . 3
 
    |
93 | | dvmptfprodlem.jph |
. . . . 5
   |
94 | | nfv 1761 |
. . . . 5
  |
95 | 93, 94 | nfan 2011 |
. . . 4
     |
96 | | dvmptfprodlem.c |
. . . . 5
       |
97 | | diffi 7803 |
. . . . . . . . 9
       |
98 | 9, 97 | syl 17 |
. . . . . . . 8
       |
99 | 98 | adantr 467 |
. . . . . . 7
 
       |
100 | | eldifi 3555 |
. . . . . . . . 9
       |
101 | 100 | adantl 468 |
. . . . . . . 8
           |
102 | 101, 91 | syldan 473 |
. . . . . . 7
           |
103 | 6, 99, 102 | fprodclf 14046 |
. . . . . 6
 
         |
104 | 103 | adantr 467 |
. . . . 5
             |
105 | 96, 104 | mulcld 9663 |
. . . 4
     
         |
106 | 95, 83, 105 | fsumclf 37645 |
. . 3
 
 
          |
107 | | dvmptfprodlem.dvp |
. . 3
                   |
108 | 1, 48, 80, 81, 82, 92, 106, 107 | dvmptmulf 37812 |
. 2
    
         
             |
109 | | dvmptfprodlem.jg |
. . . . . 6
   |
110 | | nfcv 2592 |
. . . . . 6
  |
111 | | nfcv 2592 |
. . . . . 6
             |
112 | 109, 110,
111 | nfov 6316 |
. . . . 5
        
      |
113 | 51, 22 | syl 17 |
. . . . 5
 
   |
114 | 51, 33 | syl 17 |
. . . . 5
 

  |
115 | | diffi 7803 |
. . . . . . . . . 10
               |
116 | 13, 115 | syl 17 |
. . . . . . . . 9
           |
117 | 116 | adantr 467 |
. . . . . . . 8
 
           |
118 | | eldifi 3555 |
. . . . . . . . . 10
     
         |
119 | 118 | adantl 468 |
. . . . . . . . 9
            

     |
120 | 119, 21 | syldan 473 |
. . . . . . . 8
            
  |
121 | 6, 117, 120 | fprodclf 14046 |
. . . . . . 7
 
      
      |
122 | 121 | adantr 467 |
. . . . . 6
          
      |
123 | 96, 122 | mulcld 9663 |
. . . . 5
     
             |
124 | | dvmptfprodlem.cg |
. . . . . 6
   |
125 | | sneq 3978 |
. . . . . . . 8
       |
126 | 125 | difeq2d 3551 |
. . . . . . 7
                   |
127 | 126 | prodeq1d 13975 |
. . . . . 6
      
    
           |
128 | 124, 127 | oveq12d 6308 |
. . . . 5
 
                         |
129 | 41, 9 | eqeltrd 2529 |
. . . . . . . 8
           |
130 | 129 | adantr 467 |
. . . . . . 7
 
           |
131 | 51 | adantr 467 |
. . . . . . . 8
               |
132 | 16 | adantr 467 |
. . . . . . . . . 10
 
               |
133 | | eldifi 3555 |
. . . . . . . . . . 11
     
         |
134 | 133 | adantl 468 |
. . . . . . . . . 10
 
               |
135 | 132, 134 | sseldd 3433 |
. . . . . . . . 9
 
           |
136 | 135 | adantlr 721 |
. . . . . . . 8
               |
137 | 52 | adantr 467 |
. . . . . . . 8
               |
138 | 131, 136,
137, 20 | syl3anc 1268 |
. . . . . . 7
               |
139 | 6, 130, 138 | fprodclf 14046 |
. . . . . 6
 
      
      |
140 | 81, 139 | mulcld 9663 |
. . . . 5
 
 
             |
141 | 95, 112, 83, 113, 114, 123, 128, 140 | fsumsplitsn 37649 |
. . . 4
 
                    

                          |
142 | | difundir 3696 |
. . . . . . . . . . . . . . . . 17
                     |
143 | 142 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
                       |
144 | | nfv 1761 |
. . . . . . . . . . . . . . . . . . . . 21

 |
145 | 1, 144 | nfan 2011 |
. . . . . . . . . . . . . . . . . . . 20
  
  |
146 | | elsni 3993 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     |
147 | 146 | eqcomd 2457 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     |
148 | 147 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    
  |
149 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    
  |
150 | | eqidd 2452 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    
  |
151 | 148, 149,
150 | 3eqtrd 2489 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
  |
152 | 151 | adantll 720 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   

   
  |
153 | | simpllr 769 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   

      |
154 | 152, 153 | eqeltrd 2529 |
. . . . . . . . . . . . . . . . . . . . . . 23
   

   
  |
155 | 33 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . . . . . . 23
   

   
  |
156 | 154, 155 | pm2.65da 580 |
. . . . . . . . . . . . . . . . . . . . . 22
      
  |
157 | | elsn 3982 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
158 | 156, 157 | sylnibr 307 |
. . . . . . . . . . . . . . . . . . . . 21
      
    |
159 | 158 | ex 436 |
. . . . . . . . . . . . . . . . . . . 20
 
   
     |
160 | 145, 159 | ralrimi 2788 |
. . . . . . . . . . . . . . . . . . 19
 
   
    |
161 | | disj 3805 |
. . . . . . . . . . . . . . . . . . 19
         
    |
162 | 160, 161 | sylibr 216 |
. . . . . . . . . . . . . . . . . 18
 
         |
163 | | disjdif2 3846 |
. . . . . . . . . . . . . . . . . 18
                 |
164 | 162, 163 | syl 17 |
. . . . . . . . . . . . . . . . 17
 
           |
165 | 164 | uneq2d 3588 |
. . . . . . . . . . . . . . . 16
 
                       |
166 | 143, 165 | eqtrd 2485 |
. . . . . . . . . . . . . . 15
 
                   |
167 | 166 | prodeq1d 13975 |
. . . . . . . . . . . . . 14
 
      
    
           |
168 | 167 | adantlr 721 |
. . . . . . . . . . . . 13
          
    
           |
169 | | nfv 1761 |
. . . . . . . . . . . . . . 15
  |
170 | 6, 169 | nfan 2011 |
. . . . . . . . . . . . . 14
   

  |
171 | 99 | adantr 467 |
. . . . . . . . . . . . . 14
           |
172 | 51 | adantr 467 |
. . . . . . . . . . . . . . 15
       |
173 | 172, 22 | syl 17 |
. . . . . . . . . . . . . 14
       |
174 | | id 22 |
. . . . . . . . . . . . . . . . . 18

  |
175 | 174 | intnanrd 928 |
. . . . . . . . . . . . . . . . . 18
       |
176 | 174, 175 | syl 17 |
. . . . . . . . . . . . . . . . 17
       |
177 | | eldif 3414 |
. . . . . . . . . . . . . . . . 17
           |
178 | 176, 177 | sylnibr 307 |
. . . . . . . . . . . . . . . 16

      |
179 | 33, 178 | syl 17 |
. . . . . . . . . . . . . . 15
       |
180 | 172, 179 | syl 17 |
. . . . . . . . . . . . . 14
    
      |
181 | 102 | adantlr 721 |
. . . . . . . . . . . . . 14
   



   
  |
182 | 80 | adantr 467 |
. . . . . . . . . . . . . 14
       |
183 | 170, 7, 171, 173, 180, 181, 28, 182 | fprodsplitsn 14043 |
. . . . . . . . . . . . 13
                         |
184 | | eqidd 2452 |
. . . . . . . . . . . . 13
                       |
185 | 168, 183,
184 | 3eqtrd 2489 |
. . . . . . . . . . . 12
          
              |
186 | 185 | oveq2d 6306 |
. . . . . . . . . . 11
     
                       |
187 | 96, 104, 182 | mulassd 9666 |
. . . . . . . . . . . 12
                           |
188 | 187 | eqcomd 2457 |
. . . . . . . . . . 11
     
                     |
189 | 186, 188 | eqtrd 2485 |
. . . . . . . . . 10
     
                       |
190 | 189 | ex 436 |
. . . . . . . . 9
 
        
                  |
191 | 95, 190 | ralrimi 2788 |
. . . . . . . 8
 
 
                        |
192 | 191 | sumeq2d 13768 |
. . . . . . 7
 
 
            
 
          |
193 | 95, 83, 80, 105 | fsummulc1f 37647 |
. . . . . . . 8
 
                         |
194 | 193 | eqcomd 2457 |
. . . . . . 7
 
 
 
         
           |
195 | | eqidd 2452 |
. . . . . . 7
 
             
           |
196 | 192, 194,
195 | 3eqtrd 2489 |
. . . . . 6
 
 
             

          |
197 | 106, 80 | mulcld 9663 |
. . . . . 6
 
              |
198 | 196, 197 | eqeltrd 2529 |
. . . . 5
 
 
              |
199 | 198, 140 | addcomd 9835 |
. . . 4
 
                                   
      
     
        |
200 | 42 | oveq2d 6306 |
. . . . . 6
       
          |
201 | 200 | adantr 467 |
. . . . 5
 
 
                |
202 | 201, 196 | oveq12d 6308 |
. . . 4
 
        
      
     
        
  
            |
203 | 141, 199,
202 | 3eqtrrd 2490 |
. . 3
 
      
                              |
204 | 1, 203 | mpteq2da 4488 |
. 2
       

                                |
205 | 47, 108, 204 | 3eqtrd 2489 |
1
                                 |