Step | Hyp | Ref
| Expression |
1 | | inss1 3833 |
. . . . 5
|
2 | 1 | a1i 11 |
. . . 4
|
3 | | uniioombl.s |
. . . . 5
|
4 | | uniioombl.g |
. . . . . . . 8
|
5 | 4 | uniiccdif 23346 |
. . . . . . 7
|
6 | 5 | simpld 475 |
. . . . . 6
|
7 | | ovolficcss 23238 |
. . . . . . 7
|
8 | 4, 7 | syl 17 |
. . . . . 6
|
9 | 6, 8 | sstrd 3613 |
. . . . 5
|
10 | 3, 9 | sstrd 3613 |
. . . 4
|
11 | | uniioombl.e |
. . . 4
|
12 | | ovolsscl 23254 |
. . . 4
|
13 | 2, 10, 11, 12 | syl3anc 1326 |
. . 3
|
14 | | difssd 3738 |
. . . 4
|
15 | | ovolsscl 23254 |
. . . 4
|
16 | 14, 10, 11, 15 | syl3anc 1326 |
. . 3
|
17 | | inss1 3833 |
. . . . . 6
|
18 | 17 | a1i 11 |
. . . . 5
|
19 | | uniioombl.1 |
. . . . . . . 8
|
20 | | uniioombl.2 |
. . . . . . . 8
Disj
|
21 | | uniioombl.3 |
. . . . . . . 8
|
22 | | uniioombl.a |
. . . . . . . 8
|
23 | | uniioombl.c |
. . . . . . . 8
|
24 | | uniioombl.t |
. . . . . . . 8
|
25 | | uniioombl.v |
. . . . . . . 8
|
26 | | uniioombl.m |
. . . . . . . 8
|
27 | | uniioombl.m2 |
. . . . . . . 8
|
28 | | uniioombl.k |
. . . . . . . 8
|
29 | 19, 20, 21, 22, 11, 23, 4, 3, 24, 25, 26, 27, 28 | uniioombllem3a 23352 |
. . . . . . 7
|
30 | 29 | simpld 475 |
. . . . . 6
|
31 | | inss2 3834 |
. . . . . . . . . . . . 13
|
32 | | elfznn 12370 |
. . . . . . . . . . . . . 14
|
33 | | ffvelrn 6357 |
. . . . . . . . . . . . . 14
|
34 | 4, 32, 33 | syl2an 494 |
. . . . . . . . . . . . 13
|
35 | 31, 34 | sseldi 3601 |
. . . . . . . . . . . 12
|
36 | | 1st2nd2 7205 |
. . . . . . . . . . . 12
|
37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
|
38 | 37 | fveq2d 6195 |
. . . . . . . . . 10
|
39 | | df-ov 6653 |
. . . . . . . . . 10
|
40 | 38, 39 | syl6eqr 2674 |
. . . . . . . . 9
|
41 | | ioossre 12235 |
. . . . . . . . 9
|
42 | 40, 41 | syl6eqss 3655 |
. . . . . . . 8
|
43 | 42 | ralrimiva 2966 |
. . . . . . 7
|
44 | | iunss 4561 |
. . . . . . 7
|
45 | 43, 44 | sylibr 224 |
. . . . . 6
|
46 | 30, 45 | eqsstrd 3639 |
. . . . 5
|
47 | 29 | simprd 479 |
. . . . 5
|
48 | | ovolsscl 23254 |
. . . . 5
|
49 | 18, 46, 47, 48 | syl3anc 1326 |
. . . 4
|
50 | 23 | rpred 11872 |
. . . 4
|
51 | 49, 50 | readdcld 10069 |
. . 3
|
52 | | difssd 3738 |
. . . . 5
|
53 | | ovolsscl 23254 |
. . . . 5
|
54 | 52, 46, 47, 53 | syl3anc 1326 |
. . . 4
|
55 | 54, 50 | readdcld 10069 |
. . 3
|
56 | | ssun2 3777 |
. . . . . . 7
|
57 | | ioof 12271 |
. . . . . . . . . . . . . . 15
|
58 | | rexpssxrxp 10084 |
. . . . . . . . . . . . . . . . 17
|
59 | 31, 58 | sstri 3612 |
. . . . . . . . . . . . . . . 16
|
60 | | fss 6056 |
. . . . . . . . . . . . . . . 16
|
61 | 4, 59, 60 | sylancl 694 |
. . . . . . . . . . . . . . 15
|
62 | | fco 6058 |
. . . . . . . . . . . . . . 15
|
63 | 57, 61, 62 | sylancr 695 |
. . . . . . . . . . . . . 14
|
64 | | ffn 6045 |
. . . . . . . . . . . . . 14
|
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . 13
|
66 | | fnima 6010 |
. . . . . . . . . . . . 13
|
67 | 65, 66 | syl 17 |
. . . . . . . . . . . 12
|
68 | | nnuz 11723 |
. . . . . . . . . . . . . . 15
|
69 | 26 | peano2nnd 11037 |
. . . . . . . . . . . . . . . . 17
|
70 | 69, 68 | syl6eleq 2711 |
. . . . . . . . . . . . . . . 16
|
71 | | uzsplit 12412 |
. . . . . . . . . . . . . . . 16
|
72 | 70, 71 | syl 17 |
. . . . . . . . . . . . . . 15
|
73 | 68, 72 | syl5eq 2668 |
. . . . . . . . . . . . . 14
|
74 | 26 | nncnd 11036 |
. . . . . . . . . . . . . . . . 17
|
75 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . 17
|
76 | | pncan 10287 |
. . . . . . . . . . . . . . . . 17
|
77 | 74, 75, 76 | sylancl 694 |
. . . . . . . . . . . . . . . 16
|
78 | 77 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
79 | 78 | uneq1d 3766 |
. . . . . . . . . . . . . 14
|
80 | 73, 79 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
81 | 80 | imaeq2d 5466 |
. . . . . . . . . . . 12
|
82 | 67, 81 | eqtr3d 2658 |
. . . . . . . . . . 11
|
83 | | imaundi 5545 |
. . . . . . . . . . 11
|
84 | 82, 83 | syl6eq 2672 |
. . . . . . . . . 10
|
85 | 84 | unieqd 4446 |
. . . . . . . . 9
|
86 | | uniun 4456 |
. . . . . . . . 9
|
87 | 85, 86 | syl6eq 2672 |
. . . . . . . 8
|
88 | 28 | uneq1i 3763 |
. . . . . . . 8
|
89 | 87, 88 | syl6eqr 2674 |
. . . . . . 7
|
90 | 56, 89 | syl5sseqr 3654 |
. . . . . 6
|
91 | 19, 20, 21, 22, 11, 23, 4, 3, 24, 25 | uniioombllem1 23349 |
. . . . . . 7
|
92 | | ssid 3624 |
. . . . . . . 8
|
93 | 24 | ovollb 23247 |
. . . . . . . 8
|
94 | 4, 92, 93 | sylancl 694 |
. . . . . . 7
|
95 | | ovollecl 23251 |
. . . . . . 7
|
96 | 9, 91, 94, 95 | syl3anc 1326 |
. . . . . 6
|
97 | | ovolsscl 23254 |
. . . . . 6
|
98 | 90, 9, 96, 97 | syl3anc 1326 |
. . . . 5
|
99 | 49, 98 | readdcld 10069 |
. . . 4
|
100 | | unss1 3782 |
. . . . . . . 8
|
101 | 17, 100 | ax-mp 5 |
. . . . . . 7
|
102 | 101, 89 | syl5sseqr 3654 |
. . . . . 6
|
103 | | ovolsscl 23254 |
. . . . . 6
|
104 | 102, 9, 96, 103 | syl3anc 1326 |
. . . . 5
|
105 | 3, 89 | sseqtrd 3641 |
. . . . . . . 8
|
106 | | ssrin 3838 |
. . . . . . . 8
|
107 | 105, 106 | syl 17 |
. . . . . . 7
|
108 | | indir 3875 |
. . . . . . . 8
|
109 | | inss1 3833 |
. . . . . . . . 9
|
110 | | unss2 3784 |
. . . . . . . . 9
|
111 | 109, 110 | ax-mp 5 |
. . . . . . . 8
|
112 | 108, 111 | eqsstri 3635 |
. . . . . . 7
|
113 | 107, 112 | syl6ss 3615 |
. . . . . 6
|
114 | 102, 9 | sstrd 3613 |
. . . . . 6
|
115 | | ovolss 23253 |
. . . . . 6
|
116 | 113, 114,
115 | syl2anc 693 |
. . . . 5
|
117 | 18, 46 | sstrd 3613 |
. . . . . 6
|
118 | 90, 9 | sstrd 3613 |
. . . . . 6
|
119 | | ovolun 23267 |
. . . . . 6
|
120 | 117, 49, 118, 98, 119 | syl22anc 1327 |
. . . . 5
|
121 | 13, 104, 99, 116, 120 | letrd 10194 |
. . . 4
|
122 | | rge0ssre 12280 |
. . . . . . . 8
|
123 | | eqid 2622 |
. . . . . . . . . . 11
|
124 | 123, 24 | ovolsf 23241 |
. . . . . . . . . 10
|
125 | 4, 124 | syl 17 |
. . . . . . . . 9
|
126 | 125, 26 | ffvelrnd 6360 |
. . . . . . . 8
|
127 | 122, 126 | sseldi 3601 |
. . . . . . 7
|
128 | 91, 127 | resubcld 10458 |
. . . . . 6
|
129 | 98 | rexrd 10089 |
. . . . . . 7
|
130 | | id 22 |
. . . . . . . . . . . . . 14
|
131 | | nnaddcl 11042 |
. . . . . . . . . . . . . 14
|
132 | 130, 26, 131 | syl2anr 495 |
. . . . . . . . . . . . 13
|
133 | 4 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
|
134 | 132, 133 | syldan 487 |
. . . . . . . . . . . 12
|
135 | | eqid 2622 |
. . . . . . . . . . . 12
|
136 | 134, 135 | fmptd 6385 |
. . . . . . . . . . 11
|
137 | | eqid 2622 |
. . . . . . . . . . . 12
|
138 | | eqid 2622 |
. . . . . . . . . . . 12
|
139 | 137, 138 | ovolsf 23241 |
. . . . . . . . . . 11
|
140 | 136, 139 | syl 17 |
. . . . . . . . . 10
|
141 | | frn 6053 |
. . . . . . . . . 10
|
142 | 140, 141 | syl 17 |
. . . . . . . . 9
|
143 | | icossxr 12258 |
. . . . . . . . 9
|
144 | 142, 143 | syl6ss 3615 |
. . . . . . . 8
|
145 | | supxrcl 12145 |
. . . . . . . 8
|
146 | 144, 145 | syl 17 |
. . . . . . 7
|
147 | 128 | rexrd 10089 |
. . . . . . 7
|
148 | | 1zzd 11408 |
. . . . . . . . . . . . . . . . . . 19
|
149 | 26 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . 20
|
150 | 149 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
151 | | addcom 10222 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
152 | 74, 75, 151 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . 22
|
153 | 152 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
|
154 | 153 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . 20
|
155 | 154 | biimpa 501 |
. . . . . . . . . . . . . . . . . . 19
|
156 | | eluzsub 11717 |
. . . . . . . . . . . . . . . . . . 19
|
157 | 148, 150,
155, 156 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
|
158 | 157, 68 | syl6eleqr 2712 |
. . . . . . . . . . . . . . . . 17
|
159 | | eluzelz 11697 |
. . . . . . . . . . . . . . . . . . . . 21
|
160 | 159 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
161 | 160 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . 19
|
162 | 74 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
163 | 161, 162 | npcand 10396 |
. . . . . . . . . . . . . . . . . 18
|
164 | 163 | eqcomd 2628 |
. . . . . . . . . . . . . . . . 17
|
165 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . 19
|
166 | 165 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . 18
|
167 | 166 | rspcev 3309 |
. . . . . . . . . . . . . . . . 17
|
168 | 158, 164,
167 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
169 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
|
170 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
|
171 | 170 | elrnmpt 5372 |
. . . . . . . . . . . . . . . . 17
|
172 | 169, 171 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
|
173 | 168, 172 | sylibr 224 |
. . . . . . . . . . . . . . 15
|
174 | 173 | ex 450 |
. . . . . . . . . . . . . 14
|
175 | 174 | ssrdv 3609 |
. . . . . . . . . . . . 13
|
176 | | imass2 5501 |
. . . . . . . . . . . . 13
|
177 | 175, 176 | syl 17 |
. . . . . . . . . . . 12
|
178 | | rnco2 5642 |
. . . . . . . . . . . . 13
|
179 | | eqidd 2623 |
. . . . . . . . . . . . . . 15
|
180 | 4 | feqmptd 6249 |
. . . . . . . . . . . . . . 15
|
181 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
182 | 132, 179,
180, 181 | fmptco 6396 |
. . . . . . . . . . . . . 14
|
183 | 182 | rneqd 5353 |
. . . . . . . . . . . . 13
|
184 | 178, 183 | syl5eqr 2670 |
. . . . . . . . . . . 12
|
185 | 177, 184 | sseqtrd 3641 |
. . . . . . . . . . 11
|
186 | | imass2 5501 |
. . . . . . . . . . 11
|
187 | 185, 186 | syl 17 |
. . . . . . . . . 10
|
188 | | imaco 5640 |
. . . . . . . . . 10
|
189 | | rnco2 5642 |
. . . . . . . . . 10
|
190 | 187, 188,
189 | 3sstr4g 3646 |
. . . . . . . . 9
|
191 | 190 | unissd 4462 |
. . . . . . . 8
|
192 | 138 | ovollb 23247 |
. . . . . . . 8
|
193 | 136, 191,
192 | syl2anc 693 |
. . . . . . 7
|
194 | | frn 6053 |
. . . . . . . . . . . . . . 15
|
195 | 125, 194 | syl 17 |
. . . . . . . . . . . . . 14
|
196 | 195, 143 | syl6ss 3615 |
. . . . . . . . . . . . 13
|
197 | 196 | adantr 481 |
. . . . . . . . . . . 12
|
198 | 24 | fveq1i 6192 |
. . . . . . . . . . . . . 14
|
199 | 26 | nnred 11035 |
. . . . . . . . . . . . . . . . . . 19
|
200 | 199 | ltp1d 10954 |
. . . . . . . . . . . . . . . . . 18
|
201 | | fzdisj 12368 |
. . . . . . . . . . . . . . . . . 18
|
202 | 200, 201 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
203 | 202 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
204 | | nnnn0 11299 |
. . . . . . . . . . . . . . . . . . 19
|
205 | | nn0addge1 11339 |
. . . . . . . . . . . . . . . . . . 19
|
206 | 199, 204,
205 | syl2an 494 |
. . . . . . . . . . . . . . . . . 18
|
207 | 26 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
208 | 207, 68 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . 19
|
209 | | nnaddcl 11042 |
. . . . . . . . . . . . . . . . . . . . 21
|
210 | 26, 209 | sylan 488 |
. . . . . . . . . . . . . . . . . . . 20
|
211 | 210 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . 19
|
212 | | elfz5 12334 |
. . . . . . . . . . . . . . . . . . 19
|
213 | 208, 211,
212 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
214 | 206, 213 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
|
215 | | fzsplit 12367 |
. . . . . . . . . . . . . . . . 17
|
216 | 214, 215 | syl 17 |
. . . . . . . . . . . . . . . 16
|
217 | | fzfid 12772 |
. . . . . . . . . . . . . . . 16
|
218 | 4 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
219 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . 20
|
220 | | ovolfcl 23235 |
. . . . . . . . . . . . . . . . . . . 20
|
221 | 218, 219,
220 | syl2an 494 |
. . . . . . . . . . . . . . . . . . 19
|
222 | 221 | simp2d 1074 |
. . . . . . . . . . . . . . . . . 18
|
223 | 221 | simp1d 1073 |
. . . . . . . . . . . . . . . . . 18
|
224 | 222, 223 | resubcld 10458 |
. . . . . . . . . . . . . . . . 17
|
225 | 224 | recnd 10068 |
. . . . . . . . . . . . . . . 16
|
226 | 203, 216,
217, 225 | fsumsplit 14471 |
. . . . . . . . . . . . . . 15
|
227 | 123 | ovolfsval 23239 |
. . . . . . . . . . . . . . . . 17
|
228 | 218, 219,
227 | syl2an 494 |
. . . . . . . . . . . . . . . 16
|
229 | 210, 68 | syl6eleq 2711 |
. . . . . . . . . . . . . . . 16
|
230 | 228, 229,
225 | fsumser 14461 |
. . . . . . . . . . . . . . 15
|
231 | 4 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
|
232 | 32 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
233 | 231, 232,
227 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
|
234 | 4, 32, 220 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . 22
|
235 | 234 | simp2d 1074 |
. . . . . . . . . . . . . . . . . . . . 21
|
236 | 234 | simp1d 1073 |
. . . . . . . . . . . . . . . . . . . . 21
|
237 | 235, 236 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . . 20
|
238 | 237 | adantlr 751 |
. . . . . . . . . . . . . . . . . . 19
|
239 | 238 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
|
240 | 233, 208,
239 | fsumser 14461 |
. . . . . . . . . . . . . . . . 17
|
241 | 24 | fveq1i 6192 |
. . . . . . . . . . . . . . . . 17
|
242 | 240, 241 | syl6eqr 2674 |
. . . . . . . . . . . . . . . 16
|
243 | 207 | nnzd 11481 |
. . . . . . . . . . . . . . . . . 18
|
244 | 243 | peano2zd 11485 |
. . . . . . . . . . . . . . . . . 18
|
245 | 4 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
|
246 | 207 | peano2nnd 11037 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
247 | | elfzuz 12338 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
248 | | eluznn 11758 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
249 | 246, 247,
248 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . 22
|
250 | 245, 249,
220 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
|
251 | 250 | simp2d 1074 |
. . . . . . . . . . . . . . . . . . . 20
|
252 | 250 | simp1d 1073 |
. . . . . . . . . . . . . . . . . . . 20
|
253 | 251, 252 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . 19
|
254 | 253 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
|
255 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
|
256 | 255 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
|
257 | 255 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
|
258 | 256, 257 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
|
259 | 243, 244,
211, 254, 258 | fsumshftm 14513 |
. . . . . . . . . . . . . . . . 17
|
260 | 207 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . 20
|
261 | | pncan2 10288 |
. . . . . . . . . . . . . . . . . . . 20
|
262 | 260, 75, 261 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
|
263 | | nncn 11028 |
. . . . . . . . . . . . . . . . . . . . 21
|
264 | 263 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
265 | 260, 264 | pncan2d 10394 |
. . . . . . . . . . . . . . . . . . 19
|
266 | 262, 265 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
|
267 | 266 | sumeq1d 14431 |
. . . . . . . . . . . . . . . . 17
|
268 | 136 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
269 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . 20
|
270 | 137 | ovolfsval 23239 |
. . . . . . . . . . . . . . . . . . . 20
|
271 | 268, 269,
270 | syl2an 494 |
. . . . . . . . . . . . . . . . . . 19
|
272 | 269 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
273 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
274 | 273 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
275 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
276 | 274, 135,
275 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . . 22
|
277 | 272, 276 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
278 | 277 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
|
279 | 277 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
|
280 | 278, 279 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . 19
|
281 | 271, 280 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
|
282 | | simpr 477 |
. . . . . . . . . . . . . . . . . . 19
|
283 | 282, 68 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . 18
|
284 | 4 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
|
285 | | nnaddcl 11042 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
286 | 269, 207,
285 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . . . . 22
|
287 | | ovolfcl 23235 |
. . . . . . . . . . . . . . . . . . . . . 22
|
288 | 284, 286,
287 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
|
289 | 288 | simp2d 1074 |
. . . . . . . . . . . . . . . . . . . 20
|
290 | 288 | simp1d 1073 |
. . . . . . . . . . . . . . . . . . . 20
|
291 | 289, 290 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . 19
|
292 | 291 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
|
293 | 281, 283,
292 | fsumser 14461 |
. . . . . . . . . . . . . . . . 17
|
294 | 259, 267,
293 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . 16
|
295 | 242, 294 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
|
296 | 226, 230,
295 | 3eqtr3d 2664 |
. . . . . . . . . . . . . 14
|
297 | 198, 296 | syl5eq 2668 |
. . . . . . . . . . . . 13
|
298 | | ffn 6045 |
. . . . . . . . . . . . . . . 16
|
299 | 125, 298 | syl 17 |
. . . . . . . . . . . . . . 15
|
300 | 299 | adantr 481 |
. . . . . . . . . . . . . 14
|
301 | | fnfvelrn 6356 |
. . . . . . . . . . . . . 14
|
302 | 300, 210,
301 | syl2anc 693 |
. . . . . . . . . . . . 13
|
303 | 297, 302 | eqeltrrd 2702 |
. . . . . . . . . . . 12
|
304 | | supxrub 12154 |
. . . . . . . . . . . 12
|
305 | 197, 303,
304 | syl2anc 693 |
. . . . . . . . . . 11
|
306 | 127 | adantr 481 |
. . . . . . . . . . . 12
|
307 | 140 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
|
308 | 122, 307 | sseldi 3601 |
. . . . . . . . . . . 12
|
309 | 91 | adantr 481 |
. . . . . . . . . . . 12
|
310 | 306, 308,
309 | leaddsub2d 10629 |
. . . . . . . . . . 11
|
311 | 305, 310 | mpbid 222 |
. . . . . . . . . 10
|
312 | 311 | ralrimiva 2966 |
. . . . . . . . 9
|
313 | | ffn 6045 |
. . . . . . . . . . 11
|
314 | 140, 313 | syl 17 |
. . . . . . . . . 10
|
315 | | breq1 4656 |
. . . . . . . . . . 11
|
316 | 315 | ralrn 6362 |
. . . . . . . . . 10
|
317 | 314, 316 | syl 17 |
. . . . . . . . 9
|
318 | 312, 317 | mpbird 247 |
. . . . . . . 8
|
319 | | supxrleub 12156 |
. . . . . . . . 9
|
320 | 144, 147,
319 | syl2anc 693 |
. . . . . . . 8
|
321 | 318, 320 | mpbird 247 |
. . . . . . 7
|
322 | 129, 146,
147, 193, 321 | xrletrd 11993 |
. . . . . 6
|
323 | 127, 91, 50 | absdifltd 14172 |
. . . . . . . . 9
|
324 | 27, 323 | mpbid 222 |
. . . . . . . 8
|
325 | 324 | simpld 475 |
. . . . . . 7
|
326 | 91, 50, 127, 325 | ltsub23d 10632 |
. . . . . 6
|
327 | 98, 128, 50, 322, 326 | lelttrd 10195 |
. . . . 5
|
328 | 98, 50, 49, 327 | ltadd2dd 10196 |
. . . 4
|
329 | 13, 99, 51, 121, 328 | lelttrd 10195 |
. . 3
|
330 | 54, 98 | readdcld 10069 |
. . . 4
|
331 | | difss 3737 |
. . . . . . . 8
|
332 | | unss1 3782 |
. . . . . . . 8
|
333 | 331, 332 | ax-mp 5 |
. . . . . . 7
|
334 | 333, 89 | syl5sseqr 3654 |
. . . . . 6
|
335 | | ovolsscl 23254 |
. . . . . 6
|
336 | 334, 9, 96, 335 | syl3anc 1326 |
. . . . 5
|
337 | 105 | ssdifd 3746 |
. . . . . . 7
|
338 | | difundir 3880 |
. . . . . . . 8
|
339 | | difss 3737 |
. . . . . . . . 9
|
340 | | unss2 3784 |
. . . . . . . . 9
|
341 | 339, 340 | ax-mp 5 |
. . . . . . . 8
|
342 | 338, 341 | eqsstri 3635 |
. . . . . . 7
|
343 | 337, 342 | syl6ss 3615 |
. . . . . 6
|
344 | 334, 9 | sstrd 3613 |
. . . . . 6
|
345 | | ovolss 23253 |
. . . . . 6
|
346 | 343, 344,
345 | syl2anc 693 |
. . . . 5
|
347 | 52, 46 | sstrd 3613 |
. . . . . 6
|
348 | | ovolun 23267 |
. . . . . 6
|
349 | 347, 54, 118, 98, 348 | syl22anc 1327 |
. . . . 5
|
350 | 16, 336, 330, 346, 349 | letrd 10194 |
. . . 4
|
351 | 98, 50, 54, 327 | ltadd2dd 10196 |
. . . 4
|
352 | 16, 330, 55, 350, 351 | lelttrd 10195 |
. . 3
|
353 | 13, 16, 51, 55, 329, 352 | lt2addd 10650 |
. 2
|
354 | 49 | recnd 10068 |
. . 3
|
355 | 50 | recnd 10068 |
. . 3
|
356 | 54 | recnd 10068 |
. . 3
|
357 | 354, 355,
356, 355 | add4d 10264 |
. 2
|
358 | 353, 357 | breqtrd 4679 |
1
|