Step | Hyp | Ref
| Expression |
1 | | rge0ssre 12280 |
. . 3
|
2 | | hoidmvlelem4.l |
. . . 4
|
3 | | hoidmvlelem4.x |
. . . . 5
|
4 | | hoidmvlelem4.w |
. . . . . 6
|
5 | | hoidmvlelem4.y |
. . . . . . 7
|
6 | | hoidmvlelem4.z |
. . . . . . . . 9
|
7 | 6 | eldifad 3586 |
. . . . . . . 8
|
8 | | snssi 4339 |
. . . . . . . 8
|
9 | 7, 8 | syl 17 |
. . . . . . 7
|
10 | 5, 9 | unssd 3789 |
. . . . . 6
|
11 | 4, 10 | syl5eqss 3649 |
. . . . 5
|
12 | | ssfi 8180 |
. . . . 5
|
13 | 3, 11, 12 | syl2anc 693 |
. . . 4
|
14 | | hoidmvlelem4.a |
. . . 4
|
15 | | hoidmvlelem4.b |
. . . 4
|
16 | 2, 13, 14, 15 | hoidmvcl 40796 |
. . 3
|
17 | 1, 16 | sseldi 3601 |
. 2
|
18 | | 1red 10055 |
. . . 4
|
19 | | hoidmvlelem4.e |
. . . . 5
|
20 | 19 | rpred 11872 |
. . . 4
|
21 | 18, 20 | readdcld 10069 |
. . 3
|
22 | | nfv 1843 |
. . . . 5
|
23 | | nnex 11026 |
. . . . . 6
|
24 | 23 | a1i 11 |
. . . . 5
|
25 | | icossicc 12260 |
. . . . . 6
|
26 | 13 | adantr 481 |
. . . . . . 7
|
27 | | hoidmvlelem4.c |
. . . . . . . . 9
|
28 | 27 | ffvelrnda 6359 |
. . . . . . . 8
|
29 | | elmapi 7879 |
. . . . . . . 8
|
30 | 28, 29 | syl 17 |
. . . . . . 7
|
31 | | hoidmvlelem4.h |
. . . . . . . . 9
|
32 | | eleq1 2689 |
. . . . . . . . . . . . 13
|
33 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
34 | 33 | breq1d 4663 |
. . . . . . . . . . . . . 14
|
35 | 34, 33 | ifbieq1d 4109 |
. . . . . . . . . . . . 13
|
36 | 32, 33, 35 | ifbieq12d 4113 |
. . . . . . . . . . . 12
|
37 | 36 | cbvmptv 4750 |
. . . . . . . . . . 11
|
38 | 37 | mpteq2i 4741 |
. . . . . . . . . 10
|
39 | 38 | mpteq2i 4741 |
. . . . . . . . 9
|
40 | 31, 39 | eqtri 2644 |
. . . . . . . 8
|
41 | | snidg 4206 |
. . . . . . . . . . . . 13
|
42 | 6, 41 | syl 17 |
. . . . . . . . . . . 12
|
43 | | elun2 3781 |
. . . . . . . . . . . 12
|
44 | 42, 43 | syl 17 |
. . . . . . . . . . 11
|
45 | 4 | a1i 11 |
. . . . . . . . . . . 12
|
46 | 45 | eqcomd 2628 |
. . . . . . . . . . 11
|
47 | 44, 46 | eleqtrd 2703 |
. . . . . . . . . 10
|
48 | 15, 47 | ffvelrnd 6360 |
. . . . . . . . 9
|
49 | 48 | adantr 481 |
. . . . . . . 8
|
50 | | hoidmvlelem4.d |
. . . . . . . . . 10
|
51 | 50 | ffvelrnda 6359 |
. . . . . . . . 9
|
52 | | elmapi 7879 |
. . . . . . . . 9
|
53 | 51, 52 | syl 17 |
. . . . . . . 8
|
54 | 40, 49, 26, 53 | hsphoif 40790 |
. . . . . . 7
|
55 | 2, 26, 30, 54 | hoidmvcl 40796 |
. . . . . 6
|
56 | 25, 55 | sseldi 3601 |
. . . . 5
|
57 | 22, 24, 56 | sge0clmpt 40642 |
. . . 4
Σ^ |
58 | 22, 24, 56 | sge0xrclmpt 40645 |
. . . . 5
Σ^ |
59 | | pnfxr 10092 |
. . . . . 6
|
60 | 59 | a1i 11 |
. . . . 5
|
61 | | hoidmvlelem4.r |
. . . . . . 7
Σ^ |
62 | 61 | rexrd 10089 |
. . . . . 6
Σ^ |
63 | 2, 26, 30, 53 | hoidmvcl 40796 |
. . . . . . . 8
|
64 | 25, 63 | sseldi 3601 |
. . . . . . 7
|
65 | 6 | eldifbd 3587 |
. . . . . . . . . 10
|
66 | 47, 65 | eldifd 3585 |
. . . . . . . . 9
|
67 | 66 | adantr 481 |
. . . . . . . 8
|
68 | 2, 26, 67, 4, 49, 40, 30, 53 | hsphoidmvle 40800 |
. . . . . . 7
|
69 | 22, 24, 56, 64, 68 | sge0lempt 40627 |
. . . . . 6
Σ^ Σ^ |
70 | 61 | ltpnfd 11955 |
. . . . . 6
Σ^ |
71 | 58, 62, 60, 69, 70 | xrlelttrd 11991 |
. . . . 5
Σ^ |
72 | 58, 60, 71 | xrltned 39573 |
. . . 4
Σ^ |
73 | | ge0xrre 39758 |
. . . 4
Σ^ Σ^ Σ^ |
74 | 57, 72, 73 | syl2anc 693 |
. . 3
Σ^ |
75 | 21, 74 | remulcld 10070 |
. 2
Σ^ |
76 | 21, 61 | remulcld 10070 |
. 2
Σ^ |
77 | | hoidmvlelem4.14 |
. . . . . . 7
|
78 | | hoidmvlelem4.u |
. . . . . . 7
Σ^ |
79 | | hoidmvlelem4.s |
. . . . . . 7
|
80 | 47 | ancli 574 |
. . . . . . . 8
|
81 | | eleq1 2689 |
. . . . . . . . . . 11
|
82 | 81 | anbi2d 740 |
. . . . . . . . . 10
|
83 | | fveq2 6191 |
. . . . . . . . . . 11
|
84 | | fveq2 6191 |
. . . . . . . . . . 11
|
85 | 83, 84 | breq12d 4666 |
. . . . . . . . . 10
|
86 | 82, 85 | imbi12d 334 |
. . . . . . . . 9
|
87 | | hoidmvlelem4.k |
. . . . . . . . 9
|
88 | 86, 87 | vtoclg 3266 |
. . . . . . . 8
|
89 | 47, 80, 88 | sylc 65 |
. . . . . . 7
|
90 | 2, 3, 5, 6, 4, 14,
15, 27, 50, 61, 31, 77, 19, 78, 79, 89 | hoidmvlelem1 40809 |
. . . . . 6
|
91 | 48 | rexrd 10089 |
. . . . . . . 8
|
92 | | iccssxr 12256 |
. . . . . . . . 9
|
93 | | ssrab2 3687 |
. . . . . . . . . . 11
Σ^ |
94 | 78, 93 | eqsstri 3635 |
. . . . . . . . . 10
|
95 | 94, 90 | sseldi 3601 |
. . . . . . . . 9
|
96 | 92, 95 | sseldi 3601 |
. . . . . . . 8
|
97 | | simpl 473 |
. . . . . . . . . 10
|
98 | | simpr 477 |
. . . . . . . . . . 11
|
99 | 14, 47 | ffvelrnd 6360 |
. . . . . . . . . . . . . . 15
|
100 | 99, 48 | iccssred 39727 |
. . . . . . . . . . . . . 14
|
101 | 100, 95 | sseldd 3604 |
. . . . . . . . . . . . 13
|
102 | 101 | adantr 481 |
. . . . . . . . . . . 12
|
103 | 97, 48 | syl 17 |
. . . . . . . . . . . 12
|
104 | 102, 103 | ltnled 10184 |
. . . . . . . . . . 11
|
105 | 98, 104 | mpbird 247 |
. . . . . . . . . 10
|
106 | 3 | adantr 481 |
. . . . . . . . . . 11
|
107 | 5 | adantr 481 |
. . . . . . . . . . 11
|
108 | 6 | adantr 481 |
. . . . . . . . . . 11
|
109 | 14 | adantr 481 |
. . . . . . . . . . 11
|
110 | 15 | adantr 481 |
. . . . . . . . . . 11
|
111 | 87 | adantlr 751 |
. . . . . . . . . . 11
|
112 | | eqid 2622 |
. . . . . . . . . . 11
|
113 | 27 | adantr 481 |
. . . . . . . . . . 11
|
114 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
115 | 114 | fveq1d 6193 |
. . . . . . . . . . . . . . 15
|
116 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
117 | 116 | fveq1d 6193 |
. . . . . . . . . . . . . . 15
|
118 | 115, 117 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
119 | 118 | eleq2d 2687 |
. . . . . . . . . . . . 13
|
120 | 114 | reseq1d 5395 |
. . . . . . . . . . . . 13
|
121 | 119, 120 | ifbieq1d 4109 |
. . . . . . . . . . . 12
|
122 | 121 | cbvmptv 4750 |
. . . . . . . . . . 11
|
123 | 50 | adantr 481 |
. . . . . . . . . . 11
|
124 | 116 | reseq1d 5395 |
. . . . . . . . . . . . 13
|
125 | 119, 124 | ifbieq1d 4109 |
. . . . . . . . . . . 12
|
126 | 125 | cbvmptv 4750 |
. . . . . . . . . . 11
|
127 | 61 | adantr 481 |
. . . . . . . . . . 11
Σ^ |
128 | 19 | adantr 481 |
. . . . . . . . . . 11
|
129 | 90 | adantr 481 |
. . . . . . . . . . 11
|
130 | | simpr 477 |
. . . . . . . . . . 11
|
131 | | biid 251 |
. . . . . . . . . . . . . . . . 17
|
132 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . 18
|
133 | 132 | cbvmptv 4750 |
. . . . . . . . . . . . . . . . 17
|
134 | 131, 133 | ifbieq2i 4110 |
. . . . . . . . . . . . . . . 16
|
135 | 134 | mpteq2i 4741 |
. . . . . . . . . . . . . . 15
|
136 | 135 | a1i 11 |
. . . . . . . . . . . . . 14
|
137 | | id 22 |
. . . . . . . . . . . . . 14
|
138 | 136, 137 | fveq12d 6197 |
. . . . . . . . . . . . 13
|
139 | 131, 133 | ifbieq2i 4110 |
. . . . . . . . . . . . . . . 16
|
140 | 139 | mpteq2i 4741 |
. . . . . . . . . . . . . . 15
|
141 | 140 | a1i 11 |
. . . . . . . . . . . . . 14
|
142 | 141, 137 | fveq12d 6197 |
. . . . . . . . . . . . 13
|
143 | 138, 142 | oveq12d 6668 |
. . . . . . . . . . . 12
|
144 | 143 | cbvmptv 4750 |
. . . . . . . . . . 11
|
145 | | hoidmvlelem4.i |
. . . . . . . . . . . 12
Σ^ |
146 | 145 | adantr 481 |
. . . . . . . . . . 11
Σ^ |
147 | | hoidmvlelem4.i2 |
. . . . . . . . . . . 12
|
148 | 147 | adantr 481 |
. . . . . . . . . . 11
|
149 | | eqid 2622 |
. . . . . . . . . . . 12
|
150 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
151 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
152 | 150, 151 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
153 | 152 | cbvixpv 7926 |
. . . . . . . . . . . . 13
|
154 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
|
155 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
156 | 154, 155 | ifbieq1d 4109 |
. . . . . . . . . . . . . 14
|
157 | 156 | cbvmptv 4750 |
. . . . . . . . . . . . 13
|
158 | 153, 157 | mpteq12i 4742 |
. . . . . . . . . . . 12
|
159 | 149, 158 | eqtri 2644 |
. . . . . . . . . . 11
|
160 | 2, 106, 107, 108, 4, 109, 110, 111, 112, 113, 122, 123, 126, 127, 31, 77, 128, 78, 129, 130, 144, 146, 148, 159 | hoidmvlelem3 40811 |
. . . . . . . . . 10
|
161 | 97, 105, 160 | syl2anc 693 |
. . . . . . . . 9
|
162 | 94 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
163 | 162, 100 | sstrd 3613 |
. . . . . . . . . . . . . . . . 17
|
164 | 163 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
165 | | ne0i 3921 |
. . . . . . . . . . . . . . . . 17
|
166 | 165 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
167 | 99 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . 21
|
168 | 167 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
169 | 91 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
170 | 162 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . 20
|
171 | | iccleub 12229 |
. . . . . . . . . . . . . . . . . . . 20
|
172 | 168, 169,
170, 171 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
|
173 | 172 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . 18
|
174 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . 20
|
175 | 174 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . 19
|
176 | 175 | rspcev 3309 |
. . . . . . . . . . . . . . . . . 18
|
177 | 48, 173, 176 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
178 | 177 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
179 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
180 | | suprub 10984 |
. . . . . . . . . . . . . . . 16
|
181 | 164, 166,
178, 179, 180 | syl31anc 1329 |
. . . . . . . . . . . . . . 15
|
182 | 181, 79 | syl6breqr 4695 |
. . . . . . . . . . . . . 14
|
183 | 182 | ralrimiva 2966 |
. . . . . . . . . . . . 13
|
184 | 164, 179 | sseldd 3604 |
. . . . . . . . . . . . . . 15
|
185 | 101 | adantr 481 |
. . . . . . . . . . . . . . 15
|
186 | 184, 185 | lenltd 10183 |
. . . . . . . . . . . . . 14
|
187 | 186 | ralbidva 2985 |
. . . . . . . . . . . . 13
|
188 | 183, 187 | mpbid 222 |
. . . . . . . . . . . 12
|
189 | | ralnex 2992 |
. . . . . . . . . . . 12
|
190 | 188, 189 | sylib 208 |
. . . . . . . . . . 11
|
191 | 190 | adantr 481 |
. . . . . . . . . 10
|
192 | 97, 105, 191 | syl2anc 693 |
. . . . . . . . 9
|
193 | 161, 192 | condan 835 |
. . . . . . . 8
|
194 | | iccleub 12229 |
. . . . . . . . 9
|
195 | 167, 91, 95, 194 | syl3anc 1326 |
. . . . . . . 8
|
196 | 91, 96, 193, 195 | xrletrid 11986 |
. . . . . . 7
|
197 | 78 | eqcomi 2631 |
. . . . . . . 8
Σ^ |
198 | 197 | a1i 11 |
. . . . . . 7
Σ^ |
199 | 196, 198 | eleq12d 2695 |
. . . . . 6
Σ^ |
200 | 90, 199 | mpbird 247 |
. . . . 5
Σ^ |
201 | | oveq1 6657 |
. . . . . . . 8
|
202 | 201 | oveq2d 6666 |
. . . . . . 7
|
203 | | fveq2 6191 |
. . . . . . . . . . . 12
|
204 | 203 | fveq1d 6193 |
. . . . . . . . . . 11
|
205 | 204 | oveq2d 6666 |
. . . . . . . . . 10
|
206 | 205 | mpteq2dv 4745 |
. . . . . . . . 9
|
207 | 206 | fveq2d 6195 |
. . . . . . . 8
Σ^ Σ^ |
208 | 207 | oveq2d 6666 |
. . . . . . 7
Σ^ Σ^ |
209 | 202, 208 | breq12d 4666 |
. . . . . 6
Σ^
Σ^ |
210 | 209 | elrab 3363 |
. . . . 5
Σ^ Σ^ |
211 | 200, 210 | sylib 208 |
. . . 4
Σ^ |
212 | 211 | simprd 479 |
. . 3
Σ^ |
213 | 3, 5 | ssfid 8183 |
. . . . . 6
|
214 | | eqid 2622 |
. . . . . 6
|
215 | 2, 213, 6, 65, 4, 14, 15, 214 | hoiprodp1 40802 |
. . . . 5
|
216 | | eqidd 2623 |
. . . . . . 7
|
217 | 14 | adantr 481 |
. . . . . . . . . 10
|
218 | | ssun1 3776 |
. . . . . . . . . . . 12
|
219 | 4 | eqcomi 2631 |
. . . . . . . . . . . 12
|
220 | 218, 219 | sseqtri 3637 |
. . . . . . . . . . 11
|
221 | | simpr 477 |
. . . . . . . . . . 11
|
222 | 220, 221 | sseldi 3601 |
. . . . . . . . . 10
|
223 | 217, 222 | ffvelrnd 6360 |
. . . . . . . . 9
|
224 | 15 | adantr 481 |
. . . . . . . . . 10
|
225 | 224, 222 | ffvelrnd 6360 |
. . . . . . . . 9
|
226 | 222, 87 | syldan 487 |
. . . . . . . . 9
|
227 | 223, 225,
226 | volicon0 40789 |
. . . . . . . 8
|
228 | 227 | prodeq2dv 14653 |
. . . . . . 7
|
229 | 77 | a1i 11 |
. . . . . . . 8
|
230 | | hoidmvlelem4.n |
. . . . . . . . 9
|
231 | 220 | a1i 11 |
. . . . . . . . . 10
|
232 | 14, 231 | fssresd 6071 |
. . . . . . . . 9
|
233 | 15, 231 | fssresd 6071 |
. . . . . . . . 9
|
234 | 2, 213, 230, 232, 233 | hoidmvn0val 40798 |
. . . . . . . 8
|
235 | | fvres 6207 |
. . . . . . . . . . . . 13
|
236 | | fvres 6207 |
. . . . . . . . . . . . 13
|
237 | 235, 236 | oveq12d 6668 |
. . . . . . . . . . . 12
|
238 | 237 | fveq2d 6195 |
. . . . . . . . . . 11
|
239 | 238 | adantl 482 |
. . . . . . . . . 10
|
240 | | volico 40200 |
. . . . . . . . . . 11
|
241 | 223, 225,
240 | syl2anc 693 |
. . . . . . . . . 10
|
242 | 241, 227 | eqtr3d 2658 |
. . . . . . . . . 10
|
243 | 239, 241,
242 | 3eqtrd 2660 |
. . . . . . . . 9
|
244 | 243 | prodeq2dv 14653 |
. . . . . . . 8
|
245 | 229, 234,
244 | 3eqtrd 2660 |
. . . . . . 7
|
246 | 216, 228,
245 | 3eqtr4d 2666 |
. . . . . 6
|
247 | 99, 48, 89 | volicon0 40789 |
. . . . . 6
|
248 | 246, 247 | oveq12d 6668 |
. . . . 5
|
249 | 215, 248 | eqtrd 2656 |
. . . 4
|
250 | 249 | breq1d 4663 |
. . 3
Σ^
Σ^ |
251 | 212, 250 | mpbird 247 |
. 2
Σ^ |
252 | | 0le1 10551 |
. . . . 5
|
253 | 252 | a1i 11 |
. . . 4
|
254 | 19 | rpge0d 11876 |
. . . 4
|
255 | 18, 20, 253, 254 | addge0d 10603 |
. . 3
|
256 | 74, 61, 21, 255, 69 | lemul2ad 10964 |
. 2
Σ^ Σ^ |
257 | 17, 75, 76, 251, 256 | letrd 10194 |
1
Σ^ |