Step | Hyp | Ref
| Expression |
1 | | hspmbllem2.i |
. . 3
voln* |
2 | | hspmbllem2.f |
. . 3
voln* |
3 | 1, 2 | readdcld 10069 |
. 2
voln* voln* |
4 | | hspmbllem2.r |
. . . 4
voln* |
5 | | hspmbllem2.e |
. . . . 5
|
6 | 5 | rpred 11872 |
. . . 4
|
7 | 4, 6 | readdcld 10069 |
. . 3
voln* |
8 | | nfv 1843 |
. . . 4
|
9 | | nnex 11026 |
. . . . 5
|
10 | 9 | a1i 11 |
. . . 4
|
11 | | icossicc 12260 |
. . . . 5
|
12 | | hspmbllem2.l |
. . . . . 6
|
13 | | hspmbllem2.x |
. . . . . . 7
|
14 | 13 | adantr 481 |
. . . . . 6
|
15 | | hspmbllem2.c |
. . . . . . . 8
|
16 | 15 | ffvelrnda 6359 |
. . . . . . 7
|
17 | | elmapi 7879 |
. . . . . . 7
|
18 | 16, 17 | syl 17 |
. . . . . 6
|
19 | | hspmbllem2.d |
. . . . . . . 8
|
20 | 19 | ffvelrnda 6359 |
. . . . . . 7
|
21 | | elmapi 7879 |
. . . . . . 7
|
22 | 20, 21 | syl 17 |
. . . . . 6
|
23 | 12, 14, 18, 22 | hoidmvcl 40796 |
. . . . 5
|
24 | 11, 23 | sseldi 3601 |
. . . 4
|
25 | 8, 10, 24 | sge0clmpt 40642 |
. . 3
Σ^ |
26 | | hspmbllem2.k |
. . . . . . . . 9
|
27 | | ne0i 3921 |
. . . . . . . . 9
|
28 | 26, 27 | syl 17 |
. . . . . . . 8
|
29 | 28 | adantr 481 |
. . . . . . 7
|
30 | 12, 14, 29, 18, 22 | hoidmvn0val 40798 |
. . . . . 6
|
31 | 30 | mpteq2dva 4744 |
. . . . 5
|
32 | 31 | fveq2d 6195 |
. . . 4
Σ^ Σ^ |
33 | | hspmbllem2.g |
. . . 4
Σ^
voln* |
34 | 32, 33 | eqbrtrd 4675 |
. . 3
Σ^ voln* |
35 | 7, 25, 34 | ge0lere 39759 |
. 2
Σ^ |
36 | | hspmbllem2.t |
. . . . . . . . 9
|
37 | | hspmbllem2.y |
. . . . . . . . . 10
|
38 | 37 | adantr 481 |
. . . . . . . . 9
|
39 | 36, 38, 14, 22 | hsphoif 40790 |
. . . . . . . 8
|
40 | 12, 14, 18, 39 | hoidmvcl 40796 |
. . . . . . 7
|
41 | 11, 40 | sseldi 3601 |
. . . . . 6
|
42 | 8, 10, 41 | sge0clmpt 40642 |
. . . . 5
Σ^ |
43 | | oveq2 6658 |
. . . . . . . . . . 11
|
44 | | eqeq1 2626 |
. . . . . . . . . . . 12
|
45 | | prodeq1 14639 |
. . . . . . . . . . . 12
|
46 | 44, 45 | ifbieq2d 4111 |
. . . . . . . . . . 11
|
47 | 43, 43, 46 | mpt2eq123dv 6717 |
. . . . . . . . . 10
|
48 | 47 | cbvmptv 4750 |
. . . . . . . . 9
|
49 | 12, 48 | eqtri 2644 |
. . . . . . . 8
|
50 | | diffi 8192 |
. . . . . . . . . . 11
|
51 | 13, 50 | syl 17 |
. . . . . . . . . 10
|
52 | | snfi 8038 |
. . . . . . . . . . 11
|
53 | 52 | a1i 11 |
. . . . . . . . . 10
|
54 | | unfi 8227 |
. . . . . . . . . 10
|
55 | 51, 53, 54 | syl2anc 693 |
. . . . . . . . 9
|
56 | 55 | adantr 481 |
. . . . . . . 8
|
57 | | snidg 4206 |
. . . . . . . . . . . 12
|
58 | 26, 57 | syl 17 |
. . . . . . . . . . 11
|
59 | | elun2 3781 |
. . . . . . . . . . 11
|
60 | 58, 59 | syl 17 |
. . . . . . . . . 10
|
61 | | neldifsnd 4322 |
. . . . . . . . . 10
|
62 | 60, 61 | eldifd 3585 |
. . . . . . . . 9
|
63 | 62 | adantr 481 |
. . . . . . . 8
|
64 | | eqid 2622 |
. . . . . . . 8
|
65 | | eqid 2622 |
. . . . . . . 8
|
66 | | uncom 3757 |
. . . . . . . . . . . . 13
|
67 | 66 | a1i 11 |
. . . . . . . . . . . 12
|
68 | 26 | snssd 4340 |
. . . . . . . . . . . . 13
|
69 | | undif 4049 |
. . . . . . . . . . . . 13
|
70 | 68, 69 | sylib 208 |
. . . . . . . . . . . 12
|
71 | 67, 70 | eqtrd 2656 |
. . . . . . . . . . 11
|
72 | 71 | adantr 481 |
. . . . . . . . . 10
|
73 | 72 | feq2d 6031 |
. . . . . . . . 9
|
74 | 18, 73 | mpbird 247 |
. . . . . . . 8
|
75 | 72 | feq2d 6031 |
. . . . . . . . 9
|
76 | 22, 75 | mpbird 247 |
. . . . . . . 8
|
77 | 49, 56, 63, 64, 38, 65, 74, 76 | hsphoidmvle 40800 |
. . . . . . 7
|
78 | 71 | fveq2d 6195 |
. . . . . . . . . 10
|
79 | | eqidd 2623 |
. . . . . . . . . 10
|
80 | 36 | a1i 11 |
. . . . . . . . . . . . 13
|
81 | 71 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
82 | 71 | mpteq1d 4738 |
. . . . . . . . . . . . . . . 16
|
83 | 81, 82 | mpteq12dv 4733 |
. . . . . . . . . . . . . . 15
|
84 | 83 | eqcomd 2628 |
. . . . . . . . . . . . . 14
|
85 | 84 | mpteq2dv 4745 |
. . . . . . . . . . . . 13
|
86 | 80, 85 | eqtr2d 2657 |
. . . . . . . . . . . 12
|
87 | 86 | fveq1d 6193 |
. . . . . . . . . . 11
|
88 | 87 | fveq1d 6193 |
. . . . . . . . . 10
|
89 | 78, 79, 88 | oveq123d 6671 |
. . . . . . . . 9
|
90 | 89 | adantr 481 |
. . . . . . . 8
|
91 | 78 | adantr 481 |
. . . . . . . . 9
|
92 | 91 | oveqd 6667 |
. . . . . . . 8
|
93 | 90, 92 | breq12d 4666 |
. . . . . . 7
|
94 | 77, 93 | mpbid 222 |
. . . . . 6
|
95 | 8, 10, 41, 24, 94 | sge0lempt 40627 |
. . . . 5
Σ^ Σ^ |
96 | 35, 42, 95 | ge0lere 39759 |
. . . 4
Σ^ |
97 | | hspmbllem2.s |
. . . . . . . . . 10
|
98 | 97, 38, 14, 18 | hoidifhspf 40832 |
. . . . . . . . 9
|
99 | 12, 14, 98, 22 | hoidmvcl 40796 |
. . . . . . . 8
|
100 | | eqid 2622 |
. . . . . . . 8
|
101 | 99, 100 | fmptd 6385 |
. . . . . . 7
|
102 | 11 | a1i 11 |
. . . . . . 7
|
103 | 101, 102 | fssd 6057 |
. . . . . 6
|
104 | 10, 103 | sge0cl 40598 |
. . . . 5
Σ^ |
105 | 11, 99 | sseldi 3601 |
. . . . . 6
|
106 | 26 | adantr 481 |
. . . . . . 7
|
107 | 12, 14, 18, 22, 106, 97, 38 | hoidifhspdmvle 40834 |
. . . . . 6
|
108 | 8, 10, 105, 24, 107 | sge0lempt 40627 |
. . . . 5
Σ^ Σ^ |
109 | 35, 104, 108 | ge0lere 39759 |
. . . 4
Σ^ |
110 | 37 | adantr 481 |
. . . . . . . . 9
|
111 | 13 | adantr 481 |
. . . . . . . . 9
|
112 | | eleq1 2689 |
. . . . . . . . . . . 12
|
113 | 112 | anbi2d 740 |
. . . . . . . . . . 11
|
114 | | fveq2 6191 |
. . . . . . . . . . . 12
|
115 | 114 | feq1d 6030 |
. . . . . . . . . . 11
|
116 | 113, 115 | imbi12d 334 |
. . . . . . . . . 10
|
117 | 116, 22 | chvarv 2263 |
. . . . . . . . 9
|
118 | 36, 110, 111, 117 | hsphoif 40790 |
. . . . . . . 8
|
119 | | reex 10027 |
. . . . . . . . . . . 12
|
120 | 119 | a1i 11 |
. . . . . . . . . . 11
|
121 | 120, 13 | jca 554 |
. . . . . . . . . 10
|
122 | 121 | adantr 481 |
. . . . . . . . 9
|
123 | | elmapg 7870 |
. . . . . . . . 9
|
124 | 122, 123 | syl 17 |
. . . . . . . 8
|
125 | 118, 124 | mpbird 247 |
. . . . . . 7
|
126 | | eqid 2622 |
. . . . . . 7
|
127 | 125, 126 | fmptd 6385 |
. . . . . 6
|
128 | | simpl 473 |
. . . . . . . . . . . 12
|
129 | | elinel1 3799 |
. . . . . . . . . . . . 13
|
130 | 129 | adantl 482 |
. . . . . . . . . . . 12
|
131 | | hspmbllem2.a |
. . . . . . . . . . . . . 14
|
132 | 131 | sselda 3603 |
. . . . . . . . . . . . 13
|
133 | | eliun 4524 |
. . . . . . . . . . . . 13
|
134 | 132, 133 | sylib 208 |
. . . . . . . . . . . 12
|
135 | 128, 130,
134 | syl2anc 693 |
. . . . . . . . . . 11
|
136 | 128 | adantr 481 |
. . . . . . . . . . . . 13
|
137 | | elinel2 3800 |
. . . . . . . . . . . . . . 15
|
138 | 137 | adantl 482 |
. . . . . . . . . . . . . 14
|
139 | 138 | adantr 481 |
. . . . . . . . . . . . 13
|
140 | | simpr 477 |
. . . . . . . . . . . . 13
|
141 | | ixpfn 7914 |
. . . . . . . . . . . . . . . . 17
|
142 | 141 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
143 | | nfv 1843 |
. . . . . . . . . . . . . . . . . 18
|
144 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . 19
|
145 | | nfixp1 7928 |
. . . . . . . . . . . . . . . . . . 19
|
146 | 144, 145 | nfel 2777 |
. . . . . . . . . . . . . . . . . 18
|
147 | 143, 146 | nfan 1828 |
. . . . . . . . . . . . . . . . 17
|
148 | 18 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . 22
|
149 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . . . . 22
|
150 | 148, 149 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . . 21
|
151 | 150 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . 20
|
152 | 151 | ad5ant135 1314 |
. . . . . . . . . . . . . . . . . . 19
|
153 | 39 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . 22
|
154 | 153, 149 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . . 21
|
155 | 154 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . 20
|
156 | 155 | ad5ant135 1314 |
. . . . . . . . . . . . . . . . . . 19
|
157 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
158 | | ioossre 12235 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
159 | 158 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
160 | 157, 159 | eqsstrd 3639 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
161 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
162 | | ssid 3624 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
163 | 162 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
164 | 161, 163 | eqsstrd 3639 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
165 | 160, 164 | pm2.61i 176 |
. . . . . . . . . . . . . . . . . . . . . 22
|
166 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
167 | | hspmbllem2.h |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
168 | 167, 13, 26, 37 | hspval 40823 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
169 | 168 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
170 | 166, 169 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
171 | 170 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
172 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
173 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
174 | 173 | elixp 7915 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
175 | 174 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
176 | 175 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
177 | 176 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
178 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
179 | | rspa 2930 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
180 | 177, 178,
179 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
181 | 171, 172,
180 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
|
182 | 165, 181 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . 21
|
183 | 182 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . 20
|
184 | 183 | ad4ant14 1293 |
. . . . . . . . . . . . . . . . . . 19
|
185 | 151 | ad4ant124 1295 |
. . . . . . . . . . . . . . . . . . . . 21
|
186 | 22 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
187 | 186, 149 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
188 | 187 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . 22
|
189 | 188 | ad4ant124 1295 |
. . . . . . . . . . . . . . . . . . . . 21
|
190 | 173 | elixp 7915 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
191 | 190 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
192 | 191 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
193 | 192 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
194 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
195 | | rspa 2930 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
196 | 193, 194,
195 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
|
197 | 196 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . 21
|
198 | | icogelb 12225 |
. . . . . . . . . . . . . . . . . . . . 21
|
199 | 185, 189,
197, 198 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . 20
|
200 | 199 | ad5ant1345 1316 |
. . . . . . . . . . . . . . . . . . 19
|
201 | | icoltub 39732 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
202 | 185, 189,
197, 201 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
203 | 202 | ad5ant1345 1316 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
204 | 203 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
|
205 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
206 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
207 | 205, 206 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
208 | 207 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
209 | | simp2 1062 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
210 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
211 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
212 | 211 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
213 | 212 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
214 | 213 | iftrued 4094 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
215 | 211 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
216 | 215 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
217 | 214, 216 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
218 | 217 | 3adant1 1079 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
219 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
220 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
221 | 219, 220 | ifbieq2d 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
222 | 221 | ifeq2d 4105 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
223 | 222 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
224 | 223 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
225 | 224 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
226 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
227 | 226 | mptex 6486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
228 | 227 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
229 | 80, 225, 37, 228 | fvmptd 6288 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
230 | 229 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
231 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
232 | 231 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
233 | 232, 231 | ifbieq1d 4109 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
234 | 231, 233 | ifeq12d 4106 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
235 | 234 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
236 | 235 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
237 | | mptexg 6484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
238 | 13, 237 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
239 | 238 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
240 | 230, 236,
20, 239 | fvmptd 6288 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
241 | 240 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
242 | 241 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
243 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
244 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
245 | 243, 26 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
246 | 244, 245 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
247 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
248 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
249 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
250 | 249 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
251 | 250, 249 | ifbieq1d 4109 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
252 | 248, 249,
251 | ifbieq12d 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
253 | 252 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
254 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
255 | | fvexd 6203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
256 | | ifexg 4157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
257 | 255, 37, 256 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
258 | | ifexg 4157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
259 | 255, 257,
258 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
260 | 259 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
261 | 247, 253,
254, 260 | fvmptd 6288 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
262 | 243, 246,
261 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
263 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
264 | 212, 211 | ifbieq1d 4109 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
265 | 263, 211,
264 | ifbieq12d 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
266 | 265 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
267 | 262, 266 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
268 | 267 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
269 | | neldifsnd 4322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
270 | 269 | iffalsed 4097 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
271 | 270 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
272 | 242, 268,
271 | 3eqtrrd 2661 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
273 | 272 | 3expa 1265 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
274 | 273 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
275 | 218, 274 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
276 | 208, 209,
210, 275 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
277 | 276 | ad5ant145 1315 |
. . . . . . . . . . . . . . . . . . . . . 22
|
278 | 204, 277 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . 21
|
279 | | mnfxr 10096 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
280 | 279 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
281 | 37 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
282 | 281 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
283 | 282 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
284 | 181 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
285 | 157 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
286 | 284, 285 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
287 | | iooltub 39735 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
288 | 280, 283,
286, 287 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
289 | 288 | 3adant1r 1319 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
290 | 289 | ad4ant123 1294 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
291 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
292 | 212 | notbid 308 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
293 | 292 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
294 | 291, 293 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
295 | 294 | iffalsed 4097 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
296 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
297 | 295, 296 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
298 | 297 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
299 | 273 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
300 | 299 | adantlllr 39199 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
301 | 300 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
302 | 298, 301 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
303 | 290, 302 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . . 22
|
304 | 303 | ad5ant1345 1316 |
. . . . . . . . . . . . . . . . . . . . 21
|
305 | 278, 304 | pm2.61dan 832 |
. . . . . . . . . . . . . . . . . . . 20
|
306 | 203 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
307 | 240 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
308 | 252 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
309 | 260 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
310 | 307, 308,
149, 309 | fvmptd 6288 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
311 | 310 | 3expa 1265 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
312 | 311 | adantllr 755 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
313 | 312 | ad4ant13 1292 |
. . . . . . . . . . . . . . . . . . . . . 22
|
314 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
315 | | neqne 2802 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
316 | | nelsn 4212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
317 | 315, 316 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
318 | 317 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
319 | 314, 318 | eldifd 3585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
320 | 319 | iftrued 4094 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
321 | 320 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . 22
|
322 | 313, 321 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . . . . 21
|
323 | 306, 322 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . 20
|
324 | 305, 323 | pm2.61dan 832 |
. . . . . . . . . . . . . . . . . . 19
|
325 | 152, 156,
184, 200, 324 | elicod 12224 |
. . . . . . . . . . . . . . . . . 18
|
326 | 325 | ex 450 |
. . . . . . . . . . . . . . . . 17
|
327 | 147, 326 | ralrimi 2957 |
. . . . . . . . . . . . . . . 16
|
328 | 142, 327 | jca 554 |
. . . . . . . . . . . . . . 15
|
329 | 173 | elixp 7915 |
. . . . . . . . . . . . . . 15
|
330 | 328, 329 | sylibr 224 |
. . . . . . . . . . . . . 14
|
331 | 330 | ex 450 |
. . . . . . . . . . . . 13
|
332 | 136, 139,
140, 331 | syl21anc 1325 |
. . . . . . . . . . . 12
|
333 | 332 | reximdva 3017 |
. . . . . . . . . . 11
|
334 | 135, 333 | mpd 15 |
. . . . . . . . . 10
|
335 | | eliun 4524 |
. . . . . . . . . 10
|
336 | 334, 335 | sylibr 224 |
. . . . . . . . 9
|
337 | 336 | ralrimiva 2966 |
. . . . . . . 8
|
338 | | dfss3 3592 |
. . . . . . . 8
|
339 | 337, 338 | sylibr 224 |
. . . . . . 7
|
340 | | eqidd 2623 |
. . . . . . . . . . . 12
|
341 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
342 | 341 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
343 | 342 | adantl 482 |
. . . . . . . . . . . 12
|
344 | | id 22 |
. . . . . . . . . . . 12
|
345 | | fvexd 6203 |
. . . . . . . . . . . 12
|
346 | 340, 343,
344, 345 | fvmptd 6288 |
. . . . . . . . . . 11
|
347 | 346 | fveq1d 6193 |
. . . . . . . . . 10
|
348 | 347 | oveq2d 6666 |
. . . . . . . . 9
|
349 | 348 | ixpeq2dv 7924 |
. . . . . . . 8
|
350 | 349 | iuneq2i 4539 |
. . . . . . 7
|
351 | 339, 350 | syl6sseqr 3652 |
. . . . . 6
|
352 | 13, 15, 127, 351, 12 | ovnlecvr2 40824 |
. . . . 5
voln* Σ^ |
353 | 346 | oveq2d 6666 |
. . . . . . . 8
|
354 | 353 | mpteq2ia 4740 |
. . . . . . 7
|
355 | 354 | fveq2i 6194 |
. . . . . 6
Σ^ Σ^ |
356 | 355 | a1i 11 |
. . . . 5
Σ^ Σ^ |
357 | 352, 356 | breqtrd 4679 |
. . . 4
voln* Σ^ |
358 | 15 | ffvelrnda 6359 |
. . . . . . . . . 10
|
359 | | elmapi 7879 |
. . . . . . . . . 10
|
360 | 358, 359 | syl 17 |
. . . . . . . . 9
|
361 | 97, 110, 111, 360 | hoidifhspf 40832 |
. . . . . . . 8
|
362 | | elmapg 7870 |
. . . . . . . . . 10
|
363 | 121, 362 | syl 17 |
. . . . . . . . 9
|
364 | 363 | adantr 481 |
. . . . . . . 8
|
365 | 361, 364 | mpbird 247 |
. . . . . . 7
|
366 | | eqid 2622 |
. . . . . . 7
|
367 | 365, 366 | fmptd 6385 |
. . . . . 6
|
368 | | simpl 473 |
. . . . . . . . . . 11
|
369 | | eldifi 3732 |
. . . . . . . . . . . 12
|
370 | 369 | adantl 482 |
. . . . . . . . . . 11
|
371 | 368, 370,
134 | syl2anc 693 |
. . . . . . . . . 10
|
372 | 141 | adantl 482 |
. . . . . . . . . . . . . . 15
|
373 | | nfv 1843 |
. . . . . . . . . . . . . . . . 17
|
374 | 373, 146 | nfan 1828 |
. . . . . . . . . . . . . . . 16
|
375 | 98 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . 21
|
376 | 375, 149 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . 20
|
377 | 376 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . 19
|
378 | 377 | ad5ant135 1314 |
. . . . . . . . . . . . . . . . . 18
|
379 | 189 | adantl3r 786 |
. . . . . . . . . . . . . . . . . 18
|
380 | 150 | 3expa 1265 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
381 | 188 | 3expa 1265 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
382 | | icossre 12254 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
383 | 380, 381,
382 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
|
384 | 383 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . 21
|
385 | 384, 197 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . 20
|
386 | 385 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . 19
|
387 | 386 | ad5ant1345 1316 |
. . . . . . . . . . . . . . . . . 18
|
388 | 38 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
389 | 14 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
390 | 97, 388, 389, 148, 149 | hoidifhspval3 40833 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
391 | 390 | ad5ant134 1313 |
. . . . . . . . . . . . . . . . . . . . . 22
|
392 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
393 | 392 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
394 | 391, 393 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . 21
|
395 | 394 | adantllr 755 |
. . . . . . . . . . . . . . . . . . . 20
|
396 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
397 | 396 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
398 | 199 | adantl3r 786 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
399 | 398 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
|
400 | 397, 399 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . 21
|
401 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
402 | 401 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
403 | | simpl1 1064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
404 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
405 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
406 | 405 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
407 | 406 | notbid 308 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
408 | 407 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
409 | 404, 408 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
410 | 409 | 3ad2antl3 1225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
411 | 405 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
412 | 411 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
413 | 371 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
414 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
415 | 414 | ad4ant13 1292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
416 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
417 | 254 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
418 | 415, 416,
417, 385 | syl21anc 1325 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
419 | 418 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
420 | 419 | rexlimdva 3031 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
421 | 420 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
422 | 413, 421 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
423 | 422 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
424 | 412, 423 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
425 | 424 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
426 | 403, 368,
37 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
427 | 425, 426 | ltnled 10184 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
428 | 410, 427 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
429 | 372, 371 | r19.29a 3078 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
430 | 429 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
431 | 279 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
432 | 281 | ad4antr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
433 | 422 | ad4ant13 1292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
434 | 433 | mnfltd 11958 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
435 | 405 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
436 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
437 | 435, 436 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
438 | 437 | ad4ant24 1298 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
439 | 431, 432,
433, 434, 438 | eliood 39720 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
440 | 157 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
441 | 440 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
442 | 439, 441 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
443 | 422 | ad4ant13 1292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
444 | 161 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
445 | 444 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
446 | 443, 445 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
447 | 442, 446 | pm2.61dan 832 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
448 | 447 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
449 | 430, 448 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
450 | 403, 428,
449 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
451 | 450, 174 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
452 | 168 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
453 | 452 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
454 | 453 | 3ad2antl1 1223 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
455 | 451, 454 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
456 | | eldifn 3733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
457 | 456 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
458 | 457 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
459 | 458 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
460 | 455, 459 | condan 835 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
461 | 460 | ad5ant145 1315 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
462 | 461 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
463 | 402, 462 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . 21
|
464 | 400, 463 | pm2.61dan 832 |
. . . . . . . . . . . . . . . . . . . 20
|
465 | 395, 464 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . 19
|
466 | 390 | ad5ant124 1311 |
. . . . . . . . . . . . . . . . . . . . . 22
|
467 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
468 | 467 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
469 | 466, 468 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . 21
|
470 | 199 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
471 | 469, 470 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . 20
|
472 | 471 | adantl4r 787 |
. . . . . . . . . . . . . . . . . . 19
|
473 | 465, 472 | pm2.61dan 832 |
. . . . . . . . . . . . . . . . . 18
|
474 | 202 | adantl3r 786 |
. . . . . . . . . . . . . . . . . 18
|
475 | 378, 379,
387, 473, 474 | elicod 12224 |
. . . . . . . . . . . . . . . . 17
|
476 | 475 | ex 450 |
. . . . . . . . . . . . . . . 16
|
477 | 374, 476 | ralrimi 2957 |
. . . . . . . . . . . . . . 15
|
478 | 372, 477 | jca 554 |
. . . . . . . . . . . . . 14
|
479 | 173 | elixp 7915 |
. . . . . . . . . . . . . 14
|
480 | 478, 479 | sylibr 224 |
. . . . . . . . . . . . 13
|
481 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . 19
|
482 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
|
483 | 482 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
|
484 | 483 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
485 | | fvexd 6203 |
. . . . . . . . . . . . . . . . . . 19
|
486 | 481, 484,
344, 485 | fvmptd 6288 |
. . . . . . . . . . . . . . . . . 18
|
487 | 486 | fveq1d 6193 |
. . . . . . . . . . . . . . . . 17
|
488 | 487 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
|
489 | 488 | ixpeq2dv 7924 |
. . . . . . . . . . . . . . 15
|
490 | 489 | ad2antlr 763 |
. . . . . . . . . . . . . 14
|
491 | 490 | eleq2d 2687 |
. . . . . . . . . . . . 13
|
492 | 480, 491 | mpbird 247 |
. . . . . . . . . . . 12
|
493 | 492 | ex 450 |
. . . . . . . . . . 11
|
494 | 493 | reximdva 3017 |
. . . . . . . . . 10
|
495 | 371, 494 | mpd 15 |
. . . . . . . . 9
|
496 | | eliun 4524 |
. . . . . . . . 9
|
497 | 495, 496 | sylibr 224 |
. . . . . . . 8
|
498 | 497 | ralrimiva 2966 |
. . . . . . 7
|
499 | | dfss3 3592 |
. . . . . . 7
|
500 | 498, 499 | sylibr 224 |
. . . . . 6
|
501 | 13, 367, 19, 500, 12 | ovnlecvr2 40824 |
. . . . 5
voln* Σ^ |
502 | 486 | oveq1d 6665 |
. . . . . . . 8
|
503 | 502 | mpteq2ia 4740 |
. . . . . . 7
|
504 | 503 | fveq2i 6194 |
. . . . . 6
Σ^ Σ^ |
505 | 504 | a1i 11 |
. . . . 5
Σ^ Σ^ |
506 | 501, 505 | breqtrd 4679 |
. . . 4
voln* Σ^ |
507 | 1, 2, 96, 109, 357, 506 | leadd12dd 39532 |
. . 3
voln* voln*
Σ^ Σ^ |
508 | 14, 106, 38, 18, 22, 12, 36, 97 | hspmbllem1 40840 |
. . . . . 6
|
509 | 508 | mpteq2dva 4744 |
. . . . 5
|
510 | 509 | fveq2d 6195 |
. . . 4
Σ^ Σ^ |
511 | 8, 10, 41, 105 | sge0xadd 40652 |
. . . 4
Σ^ Σ^ Σ^ |
512 | 96, 109 | rexaddd 12065 |
. . . 4
Σ^ Σ^ Σ^ Σ^ |
513 | 510, 511,
512 | 3eqtrrd 2661 |
. . 3
Σ^ Σ^ Σ^ |
514 | 507, 513 | breqtrd 4679 |
. 2
voln* voln*
Σ^ |
515 | 3, 35, 7, 514, 34 | letrd 10194 |
1
voln* voln*
voln* |