Proof of Theorem dvmptfprodlem
Step | Hyp | Ref
| Expression |
1 | | dvmptfprodlem.xph |
. . . 4
|
2 | | dvmptfprodlem.iph |
. . . . . . 7
|
3 | | nfcv 2764 |
. . . . . . . 8
|
4 | | nfcv 2764 |
. . . . . . . 8
|
5 | 3, 4 | nfel 2777 |
. . . . . . 7
|
6 | 2, 5 | nfan 1828 |
. . . . . 6
|
7 | | dvmptfprodlem.if |
. . . . . . 7
|
8 | 7 | a1i 11 |
. . . . . 6
|
9 | | dvmptfprodlem.d |
. . . . . . . 8
|
10 | | snfi 8038 |
. . . . . . . . 9
|
11 | 10 | a1i 11 |
. . . . . . . 8
|
12 | | unfi 8227 |
. . . . . . . 8
|
13 | 9, 11, 12 | syl2anc 693 |
. . . . . . 7
|
14 | 13 | adantr 481 |
. . . . . 6
|
15 | | simpll 790 |
. . . . . . 7
|
16 | | dvmptfprodlem.ss |
. . . . . . . . 9
|
17 | 16 | sselda 3603 |
. . . . . . . 8
|
18 | 17 | adantlr 751 |
. . . . . . 7
|
19 | | simplr 792 |
. . . . . . 7
|
20 | | dvmptfprodlem.a |
. . . . . . 7
|
21 | 15, 18, 19, 20 | syl3anc 1326 |
. . . . . 6
|
22 | | dvmptfprodlem.e |
. . . . . . . . 9
|
23 | | snidg 4206 |
. . . . . . . . 9
|
24 | 22, 23 | syl 17 |
. . . . . . . 8
|
25 | | elun2 3781 |
. . . . . . . 8
|
26 | 24, 25 | syl 17 |
. . . . . . 7
|
27 | 26 | adantr 481 |
. . . . . 6
|
28 | | dvmptfprodlem.f |
. . . . . . 7
|
29 | 28 | adantl 482 |
. . . . . 6
|
30 | 6, 8, 14, 21, 27, 29 | fprodsplit1f 14721 |
. . . . 5
|
31 | | difundir 3880 |
. . . . . . . . . 10
|
32 | 31 | a1i 11 |
. . . . . . . . 9
|
33 | | dvmptfprodlem.db |
. . . . . . . . . . 11
|
34 | | difsn 4328 |
. . . . . . . . . . 11
|
35 | 33, 34 | syl 17 |
. . . . . . . . . 10
|
36 | | difid 3948 |
. . . . . . . . . . 11
|
37 | 36 | a1i 11 |
. . . . . . . . . 10
|
38 | 35, 37 | uneq12d 3768 |
. . . . . . . . 9
|
39 | | un0 3967 |
. . . . . . . . . 10
|
40 | 39 | a1i 11 |
. . . . . . . . 9
|
41 | 32, 38, 40 | 3eqtrd 2660 |
. . . . . . . 8
|
42 | 41 | prodeq1d 14651 |
. . . . . . 7
|
43 | 42 | oveq2d 6666 |
. . . . . 6
|
44 | 43 | adantr 481 |
. . . . 5
|
45 | 30, 44 | eqtrd 2656 |
. . . 4
|
46 | 1, 45 | mpteq2da 4743 |
. . 3
|
47 | 46 | oveq2d 6666 |
. 2
|
48 | | dvmptfprodlem.s |
. . 3
|
49 | 16, 26 | sseldd 3604 |
. . . . 5
|
50 | 49 | adantr 481 |
. . . 4
|
51 | | simpl 473 |
. . . . 5
|
52 | | simpr 477 |
. . . . 5
|
53 | 51, 50, 52 | 3jca 1242 |
. . . 4
|
54 | | nfcv 2764 |
. . . . 5
|
55 | | nfv 1843 |
. . . . . . 7
|
56 | 2, 55, 5 | nf3an 1831 |
. . . . . 6
|
57 | | nfcv 2764 |
. . . . . . 7
|
58 | 7, 57 | nfel 2777 |
. . . . . 6
|
59 | 56, 58 | nfim 1825 |
. . . . 5
|
60 | | ancom 466 |
. . . . . . . . . . . . 13
|
61 | 60 | imbi1i 339 |
. . . . . . . . . . . 12
|
62 | | eqcom 2629 |
. . . . . . . . . . . . 13
|
63 | 62 | imbi2i 326 |
. . . . . . . . . . . 12
|
64 | 61, 63 | bitri 264 |
. . . . . . . . . . 11
|
65 | 29, 64 | mpbi 220 |
. . . . . . . . . 10
|
66 | 65 | 3adantr2 1221 |
. . . . . . . . 9
|
67 | 66 | 3adant2 1080 |
. . . . . . . 8
|
68 | | simp3 1063 |
. . . . . . . . 9
|
69 | | eleq1 2689 |
. . . . . . . . . . . . 13
|
70 | 69 | 3anbi2d 1404 |
. . . . . . . . . . . 12
|
71 | 70 | imbi1d 331 |
. . . . . . . . . . 11
|
72 | 71 | biimpa 501 |
. . . . . . . . . 10
|
73 | 72 | 3adant3 1081 |
. . . . . . . . 9
|
74 | 68, 73 | mpd 15 |
. . . . . . . 8
|
75 | 67, 74 | eqeltrd 2701 |
. . . . . . 7
|
76 | 75 | 3exp 1264 |
. . . . . 6
|
77 | 20 | 2a1i 12 |
. . . . . 6
|
78 | 76, 77 | impbid 202 |
. . . . 5
|
79 | 54, 59, 78, 20 | vtoclgf 3264 |
. . . 4
|
80 | 50, 53, 79 | sylc 65 |
. . 3
|
81 | | dvmptfprodlem.14 |
. . 3
|
82 | | dvmptfprodlem.dvf |
. . 3
|
83 | 51, 9 | syl 17 |
. . . 4
|
84 | 51 | adantr 481 |
. . . . 5
|
85 | 16 | adantr 481 |
. . . . . . 7
|
86 | | elun1 3780 |
. . . . . . . 8
|
87 | 86 | adantl 482 |
. . . . . . 7
|
88 | 85, 87 | sseldd 3604 |
. . . . . 6
|
89 | 88 | adantlr 751 |
. . . . 5
|
90 | 52 | adantr 481 |
. . . . 5
|
91 | 84, 89, 90, 20 | syl3anc 1326 |
. . . 4
|
92 | 6, 83, 91 | fprodclf 14723 |
. . 3
|
93 | | dvmptfprodlem.jph |
. . . . 5
|
94 | | nfv 1843 |
. . . . 5
|
95 | 93, 94 | nfan 1828 |
. . . 4
|
96 | | dvmptfprodlem.c |
. . . . 5
|
97 | | diffi 8192 |
. . . . . . . . 9
|
98 | 9, 97 | syl 17 |
. . . . . . . 8
|
99 | 98 | adantr 481 |
. . . . . . 7
|
100 | | eldifi 3732 |
. . . . . . . . 9
|
101 | 100 | adantl 482 |
. . . . . . . 8
|
102 | 101, 91 | syldan 487 |
. . . . . . 7
|
103 | 6, 99, 102 | fprodclf 14723 |
. . . . . 6
|
104 | 103 | adantr 481 |
. . . . 5
|
105 | 96, 104 | mulcld 10060 |
. . . 4
|
106 | 95, 83, 105 | fsumclf 39801 |
. . 3
|
107 | | dvmptfprodlem.dvp |
. . 3
|
108 | 1, 48, 80, 81, 82, 92, 106, 107 | dvmptmulf 40152 |
. 2
|
109 | | dvmptfprodlem.jg |
. . . . . 6
|
110 | | nfcv 2764 |
. . . . . 6
|
111 | | nfcv 2764 |
. . . . . 6
|
112 | 109, 110,
111 | nfov 6676 |
. . . . 5
|
113 | 51, 22 | syl 17 |
. . . . 5
|
114 | 51, 33 | syl 17 |
. . . . 5
|
115 | | diffi 8192 |
. . . . . . . . . 10
|
116 | 13, 115 | syl 17 |
. . . . . . . . 9
|
117 | 116 | adantr 481 |
. . . . . . . 8
|
118 | | eldifi 3732 |
. . . . . . . . . 10
|
119 | 118 | adantl 482 |
. . . . . . . . 9
|
120 | 119, 21 | syldan 487 |
. . . . . . . 8
|
121 | 6, 117, 120 | fprodclf 14723 |
. . . . . . 7
|
122 | 121 | adantr 481 |
. . . . . 6
|
123 | 96, 122 | mulcld 10060 |
. . . . 5
|
124 | | dvmptfprodlem.cg |
. . . . . 6
|
125 | | sneq 4187 |
. . . . . . . 8
|
126 | 125 | difeq2d 3728 |
. . . . . . 7
|
127 | 126 | prodeq1d 14651 |
. . . . . 6
|
128 | 124, 127 | oveq12d 6668 |
. . . . 5
|
129 | 41, 9 | eqeltrd 2701 |
. . . . . . . 8
|
130 | 129 | adantr 481 |
. . . . . . 7
|
131 | 51 | adantr 481 |
. . . . . . . 8
|
132 | 16 | adantr 481 |
. . . . . . . . . 10
|
133 | | eldifi 3732 |
. . . . . . . . . . 11
|
134 | 133 | adantl 482 |
. . . . . . . . . 10
|
135 | 132, 134 | sseldd 3604 |
. . . . . . . . 9
|
136 | 135 | adantlr 751 |
. . . . . . . 8
|
137 | 52 | adantr 481 |
. . . . . . . 8
|
138 | 131, 136,
137, 20 | syl3anc 1326 |
. . . . . . 7
|
139 | 6, 130, 138 | fprodclf 14723 |
. . . . . 6
|
140 | 81, 139 | mulcld 10060 |
. . . . 5
|
141 | 95, 112, 83, 113, 114, 123, 128, 140 | fsumsplitsn 14474 |
. . . 4
|
142 | | difundir 3880 |
. . . . . . . . . . . . . . . . 17
|
143 | 142 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
144 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . . 21
|
145 | 1, 144 | nfan 1828 |
. . . . . . . . . . . . . . . . . . . 20
|
146 | | elsni 4194 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
147 | 146 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
148 | 147 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
149 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
150 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
151 | 148, 149,
150 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
152 | 151 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
153 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
154 | 152, 153 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
155 | 33 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
156 | 154, 155 | pm2.65da 600 |
. . . . . . . . . . . . . . . . . . . . . 22
|
157 | | velsn 4193 |
. . . . . . . . . . . . . . . . . . . . . 22
|
158 | 156, 157 | sylnibr 319 |
. . . . . . . . . . . . . . . . . . . . 21
|
159 | 158 | ex 450 |
. . . . . . . . . . . . . . . . . . . 20
|
160 | 145, 159 | ralrimi 2957 |
. . . . . . . . . . . . . . . . . . 19
|
161 | | disj 4017 |
. . . . . . . . . . . . . . . . . . 19
|
162 | 160, 161 | sylibr 224 |
. . . . . . . . . . . . . . . . . 18
|
163 | | disjdif2 4047 |
. . . . . . . . . . . . . . . . . 18
|
164 | 162, 163 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
165 | 164 | uneq2d 3767 |
. . . . . . . . . . . . . . . 16
|
166 | 143, 165 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
167 | 166 | prodeq1d 14651 |
. . . . . . . . . . . . . 14
|
168 | 167 | adantlr 751 |
. . . . . . . . . . . . 13
|
169 | | nfv 1843 |
. . . . . . . . . . . . . . 15
|
170 | 6, 169 | nfan 1828 |
. . . . . . . . . . . . . 14
|
171 | 99 | adantr 481 |
. . . . . . . . . . . . . 14
|
172 | 51 | adantr 481 |
. . . . . . . . . . . . . . 15
|
173 | 172, 22 | syl 17 |
. . . . . . . . . . . . . 14
|
174 | | id 22 |
. . . . . . . . . . . . . . . . . 18
|
175 | 174 | intnanrd 963 |
. . . . . . . . . . . . . . . . . 18
|
176 | 174, 175 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
177 | | eldif 3584 |
. . . . . . . . . . . . . . . . 17
|
178 | 176, 177 | sylnibr 319 |
. . . . . . . . . . . . . . . 16
|
179 | 33, 178 | syl 17 |
. . . . . . . . . . . . . . 15
|
180 | 172, 179 | syl 17 |
. . . . . . . . . . . . . 14
|
181 | 102 | adantlr 751 |
. . . . . . . . . . . . . 14
|
182 | 80 | adantr 481 |
. . . . . . . . . . . . . 14
|
183 | 170, 7, 171, 173, 180, 181, 28, 182 | fprodsplitsn 14720 |
. . . . . . . . . . . . 13
|
184 | | eqidd 2623 |
. . . . . . . . . . . . 13
|
185 | 168, 183,
184 | 3eqtrd 2660 |
. . . . . . . . . . . 12
|
186 | 185 | oveq2d 6666 |
. . . . . . . . . . 11
|
187 | 96, 104, 182 | mulassd 10063 |
. . . . . . . . . . . 12
|
188 | 187 | eqcomd 2628 |
. . . . . . . . . . 11
|
189 | 186, 188 | eqtrd 2656 |
. . . . . . . . . 10
|
190 | 189 | ex 450 |
. . . . . . . . 9
|
191 | 95, 190 | ralrimi 2957 |
. . . . . . . 8
|
192 | 191 | sumeq2d 14432 |
. . . . . . 7
|
193 | 95, 83, 80, 105 | fsummulc1f 39802 |
. . . . . . . 8
|
194 | 193 | eqcomd 2628 |
. . . . . . 7
|
195 | | eqidd 2623 |
. . . . . . 7
|
196 | 192, 194,
195 | 3eqtrd 2660 |
. . . . . 6
|
197 | 106, 80 | mulcld 10060 |
. . . . . 6
|
198 | 196, 197 | eqeltrd 2701 |
. . . . 5
|
199 | 198, 140 | addcomd 10238 |
. . . 4
|
200 | 42 | oveq2d 6666 |
. . . . . 6
|
201 | 200 | adantr 481 |
. . . . 5
|
202 | 201, 196 | oveq12d 6668 |
. . . 4
|
203 | 141, 199,
202 | 3eqtrrd 2661 |
. . 3
|
204 | 1, 203 | mpteq2da 4743 |
. 2
|
205 | 47, 108, 204 | 3eqtrd 2660 |
1
|