Step | Hyp | Ref
| Expression |
1 | | i1fadd.1 |
. . . . 5
|
2 | | i1fadd.2 |
. . . . 5
|
3 | 1, 2 | i1fadd 23462 |
. . . 4
|
4 | | i1frn 23444 |
. . . . . . . 8
|
5 | 1, 4 | syl 17 |
. . . . . . 7
|
6 | | i1frn 23444 |
. . . . . . . 8
|
7 | 2, 6 | syl 17 |
. . . . . . 7
|
8 | | xpfi 8231 |
. . . . . . 7
|
9 | 5, 7, 8 | syl2anc 693 |
. . . . . 6
|
10 | | ax-addf 10015 |
. . . . . . . . . 10
|
11 | | ffn 6045 |
. . . . . . . . . 10
|
12 | 10, 11 | ax-mp 5 |
. . . . . . . . 9
|
13 | | i1ff 23443 |
. . . . . . . . . . . . 13
|
14 | 1, 13 | syl 17 |
. . . . . . . . . . . 12
|
15 | | frn 6053 |
. . . . . . . . . . . 12
|
16 | 14, 15 | syl 17 |
. . . . . . . . . . 11
|
17 | | ax-resscn 9993 |
. . . . . . . . . . 11
|
18 | 16, 17 | syl6ss 3615 |
. . . . . . . . . 10
|
19 | | i1ff 23443 |
. . . . . . . . . . . . 13
|
20 | 2, 19 | syl 17 |
. . . . . . . . . . . 12
|
21 | | frn 6053 |
. . . . . . . . . . . 12
|
22 | 20, 21 | syl 17 |
. . . . . . . . . . 11
|
23 | 22, 17 | syl6ss 3615 |
. . . . . . . . . 10
|
24 | | xpss12 5225 |
. . . . . . . . . 10
|
25 | 18, 23, 24 | syl2anc 693 |
. . . . . . . . 9
|
26 | | fnssres 6004 |
. . . . . . . . 9
|
27 | 12, 25, 26 | sylancr 695 |
. . . . . . . 8
|
28 | | itg1add.4 |
. . . . . . . . 9
|
29 | 28 | fneq1i 5985 |
. . . . . . . 8
|
30 | 27, 29 | sylibr 224 |
. . . . . . 7
|
31 | | dffn4 6121 |
. . . . . . 7
|
32 | 30, 31 | sylib 208 |
. . . . . 6
|
33 | | fofi 8252 |
. . . . . 6
|
34 | 9, 32, 33 | syl2anc 693 |
. . . . 5
|
35 | | difss 3737 |
. . . . 5
|
36 | | ssfi 8180 |
. . . . 5
|
37 | 34, 35, 36 | sylancl 694 |
. . . 4
|
38 | | opelxpi 5148 |
. . . . . . . . . 10
|
39 | | ffun 6048 |
. . . . . . . . . . . 12
|
40 | 10, 39 | ax-mp 5 |
. . . . . . . . . . 11
|
41 | 10 | fdmi 6052 |
. . . . . . . . . . . 12
|
42 | 25, 41 | syl6sseqr 3652 |
. . . . . . . . . . 11
|
43 | | funfvima2 6493 |
. . . . . . . . . . 11
|
44 | 40, 42, 43 | sylancr 695 |
. . . . . . . . . 10
|
45 | 38, 44 | syl5 34 |
. . . . . . . . 9
|
46 | 45 | imp 445 |
. . . . . . . 8
|
47 | | df-ov 6653 |
. . . . . . . 8
|
48 | 28 | rneqi 5352 |
. . . . . . . . 9
|
49 | | df-ima 5127 |
. . . . . . . . 9
|
50 | 48, 49 | eqtr4i 2647 |
. . . . . . . 8
|
51 | 46, 47, 50 | 3eltr4g 2718 |
. . . . . . 7
|
52 | | ffn 6045 |
. . . . . . . . 9
|
53 | 14, 52 | syl 17 |
. . . . . . . 8
|
54 | | dffn3 6054 |
. . . . . . . 8
|
55 | 53, 54 | sylib 208 |
. . . . . . 7
|
56 | | ffn 6045 |
. . . . . . . . 9
|
57 | 20, 56 | syl 17 |
. . . . . . . 8
|
58 | | dffn3 6054 |
. . . . . . . 8
|
59 | 57, 58 | sylib 208 |
. . . . . . 7
|
60 | | reex 10027 |
. . . . . . . 8
|
61 | 60 | a1i 11 |
. . . . . . 7
|
62 | | inidm 3822 |
. . . . . . 7
|
63 | 51, 55, 59, 61, 61, 62 | off 6912 |
. . . . . 6
|
64 | | frn 6053 |
. . . . . 6
|
65 | 63, 64 | syl 17 |
. . . . 5
|
66 | 65 | ssdifd 3746 |
. . . 4
|
67 | 16 | sselda 3603 |
. . . . . . . . . 10
|
68 | 22 | sselda 3603 |
. . . . . . . . . 10
|
69 | 67, 68 | anim12dan 882 |
. . . . . . . . 9
|
70 | | readdcl 10019 |
. . . . . . . . 9
|
71 | 69, 70 | syl 17 |
. . . . . . . 8
|
72 | 71 | ralrimivva 2971 |
. . . . . . 7
|
73 | | funimassov 6811 |
. . . . . . . 8
|
74 | 40, 42, 73 | sylancr 695 |
. . . . . . 7
|
75 | 72, 74 | mpbird 247 |
. . . . . 6
|
76 | 50, 75 | syl5eqss 3649 |
. . . . 5
|
77 | 76 | ssdifd 3746 |
. . . 4
|
78 | | itg1val2 23451 |
. . . 4
|
79 | 3, 37, 66, 77, 78 | syl13anc 1328 |
. . 3
|
80 | 20 | adantr 481 |
. . . . . . . 8
|
81 | 7 | adantr 481 |
. . . . . . . 8
|
82 | | inss2 3834 |
. . . . . . . . 9
|
83 | 82 | a1i 11 |
. . . . . . . 8
|
84 | | i1fima 23445 |
. . . . . . . . . . 11
|
85 | 1, 84 | syl 17 |
. . . . . . . . . 10
|
86 | | i1fima 23445 |
. . . . . . . . . . 11
|
87 | 2, 86 | syl 17 |
. . . . . . . . . 10
|
88 | | inmbl 23310 |
. . . . . . . . . 10
|
89 | 85, 87, 88 | syl2anc 693 |
. . . . . . . . 9
|
90 | 89 | ad2antrr 762 |
. . . . . . . 8
|
91 | 35, 76 | syl5ss 3614 |
. . . . . . . . . . . . 13
|
92 | 91 | sselda 3603 |
. . . . . . . . . . . 12
|
93 | 92 | adantr 481 |
. . . . . . . . . . 11
|
94 | 68 | adantlr 751 |
. . . . . . . . . . 11
|
95 | 93, 94 | resubcld 10458 |
. . . . . . . . . 10
|
96 | 93 | recnd 10068 |
. . . . . . . . . . . . 13
|
97 | 94 | recnd 10068 |
. . . . . . . . . . . . 13
|
98 | 96, 97 | npcand 10396 |
. . . . . . . . . . . 12
|
99 | | eldifsni 4320 |
. . . . . . . . . . . . 13
|
100 | 99 | ad2antlr 763 |
. . . . . . . . . . . 12
|
101 | 98, 100 | eqnetrd 2861 |
. . . . . . . . . . 11
|
102 | | oveq12 6659 |
. . . . . . . . . . . . 13
|
103 | | 00id 10211 |
. . . . . . . . . . . . 13
|
104 | 102, 103 | syl6eq 2672 |
. . . . . . . . . . . 12
|
105 | 104 | necon3ai 2819 |
. . . . . . . . . . 11
|
106 | 101, 105 | syl 17 |
. . . . . . . . . 10
|
107 | | itg1add.3 |
. . . . . . . . . . 11
|
108 | 1, 2, 107 | itg1addlem3 23465 |
. . . . . . . . . 10
|
109 | 95, 94, 106, 108 | syl21anc 1325 |
. . . . . . . . 9
|
110 | 1, 2, 107 | itg1addlem2 23464 |
. . . . . . . . . . 11
|
111 | 110 | ad2antrr 762 |
. . . . . . . . . 10
|
112 | 111, 95, 94 | fovrnd 6806 |
. . . . . . . . 9
|
113 | 109, 112 | eqeltrrd 2702 |
. . . . . . . 8
|
114 | 80, 81, 83, 90, 113 | itg1addlem1 23459 |
. . . . . . 7
|
115 | 92 | recnd 10068 |
. . . . . . . . 9
|
116 | 1, 2 | i1faddlem 23460 |
. . . . . . . . 9
|
117 | 115, 116 | syldan 487 |
. . . . . . . 8
|
118 | 117 | fveq2d 6195 |
. . . . . . 7
|
119 | 109 | sumeq2dv 14433 |
. . . . . . 7
|
120 | 114, 118,
119 | 3eqtr4d 2666 |
. . . . . 6
|
121 | 120 | oveq2d 6666 |
. . . . 5
|
122 | 112 | recnd 10068 |
. . . . . 6
|
123 | 81, 115, 122 | fsummulc2 14516 |
. . . . 5
|
124 | 121, 123 | eqtrd 2656 |
. . . 4
|
125 | 124 | sumeq2dv 14433 |
. . 3
|
126 | 96, 122 | mulcld 10060 |
. . . . 5
|
127 | 126 | anasss 679 |
. . . 4
|
128 | 37, 7, 127 | fsumcom 14507 |
. . 3
|
129 | 79, 125, 128 | 3eqtrd 2660 |
. 2
|
130 | | oveq1 6657 |
. . . . . . 7
|
131 | | oveq1 6657 |
. . . . . . 7
|
132 | 130, 131 | oveq12d 6668 |
. . . . . 6
|
133 | 34 | adantr 481 |
. . . . . 6
|
134 | 76 | adantr 481 |
. . . . . . . . . . 11
|
135 | 134 | sselda 3603 |
. . . . . . . . . 10
|
136 | 68 | adantr 481 |
. . . . . . . . . 10
|
137 | 135, 136 | resubcld 10458 |
. . . . . . . . 9
|
138 | 137 | ex 450 |
. . . . . . . 8
|
139 | 135 | recnd 10068 |
. . . . . . . . . . 11
|
140 | 139 | adantrr 753 |
. . . . . . . . . 10
|
141 | 76 | sselda 3603 |
. . . . . . . . . . . 12
|
142 | 141 | ad2ant2rl 785 |
. . . . . . . . . . 11
|
143 | 142 | recnd 10068 |
. . . . . . . . . 10
|
144 | 68 | recnd 10068 |
. . . . . . . . . . 11
|
145 | 144 | adantr 481 |
. . . . . . . . . 10
|
146 | 140, 143,
145 | subcan2ad 10437 |
. . . . . . . . 9
|
147 | 146 | ex 450 |
. . . . . . . 8
|
148 | 138, 147 | dom2lem 7995 |
. . . . . . 7
|
149 | | f1f1orn 6148 |
. . . . . . 7
|
150 | 148, 149 | syl 17 |
. . . . . 6
|
151 | | oveq1 6657 |
. . . . . . . 8
|
152 | | eqid 2622 |
. . . . . . . 8
|
153 | | ovex 6678 |
. . . . . . . 8
|
154 | 151, 152,
153 | fvmpt 6282 |
. . . . . . 7
|
155 | 154 | adantl 482 |
. . . . . 6
|
156 | | f1f 6101 |
. . . . . . . . . . 11
|
157 | | frn 6053 |
. . . . . . . . . . 11
|
158 | 148, 156,
157 | 3syl 18 |
. . . . . . . . . 10
|
159 | 158 | sselda 3603 |
. . . . . . . . 9
|
160 | 68 | adantr 481 |
. . . . . . . . 9
|
161 | 159, 160 | readdcld 10069 |
. . . . . . . 8
|
162 | 110 | ad2antrr 762 |
. . . . . . . . 9
|
163 | 162, 159,
160 | fovrnd 6806 |
. . . . . . . 8
|
164 | 161, 163 | remulcld 10070 |
. . . . . . 7
|
165 | 164 | recnd 10068 |
. . . . . 6
|
166 | 132, 133,
150, 155, 165 | fsumf1o 14454 |
. . . . 5
|
167 | 134 | sselda 3603 |
. . . . . . . . 9
|
168 | 167 | recnd 10068 |
. . . . . . . 8
|
169 | 144 | adantr 481 |
. . . . . . . 8
|
170 | 168, 169 | npcand 10396 |
. . . . . . 7
|
171 | 170 | oveq1d 6665 |
. . . . . 6
|
172 | 171 | sumeq2dv 14433 |
. . . . 5
|
173 | 166, 172 | eqtrd 2656 |
. . . 4
|
174 | 42 | ad2antrr 762 |
. . . . . . . . . . 11
|
175 | | simpr 477 |
. . . . . . . . . . . 12
|
176 | | simplr 792 |
. . . . . . . . . . . 12
|
177 | | opelxpi 5148 |
. . . . . . . . . . . 12
|
178 | 175, 176,
177 | syl2anc 693 |
. . . . . . . . . . 11
|
179 | | funfvima2 6493 |
. . . . . . . . . . . 12
|
180 | 40, 179 | mpan 706 |
. . . . . . . . . . 11
|
181 | 174, 178,
180 | sylc 65 |
. . . . . . . . . 10
|
182 | | df-ov 6653 |
. . . . . . . . . 10
|
183 | 181, 182,
50 | 3eltr4g 2718 |
. . . . . . . . 9
|
184 | 67 | adantlr 751 |
. . . . . . . . . . . 12
|
185 | 184 | recnd 10068 |
. . . . . . . . . . 11
|
186 | 144 | adantr 481 |
. . . . . . . . . . 11
|
187 | 185, 186 | pncand 10393 |
. . . . . . . . . 10
|
188 | 187 | eqcomd 2628 |
. . . . . . . . 9
|
189 | | oveq1 6657 |
. . . . . . . . . . 11
|
190 | 189 | eqeq2d 2632 |
. . . . . . . . . 10
|
191 | 190 | rspcev 3309 |
. . . . . . . . 9
|
192 | 183, 188,
191 | syl2anc 693 |
. . . . . . . 8
|
193 | 192 | ralrimiva 2966 |
. . . . . . 7
|
194 | | ssabral 3673 |
. . . . . . 7
|
195 | 193, 194 | sylibr 224 |
. . . . . 6
|
196 | 152 | rnmpt 5371 |
. . . . . 6
|
197 | 195, 196 | syl6sseqr 3652 |
. . . . 5
|
198 | 68 | adantr 481 |
. . . . . . . 8
|
199 | 184, 198 | readdcld 10069 |
. . . . . . 7
|
200 | 110 | ad2antrr 762 |
. . . . . . . 8
|
201 | 200, 184,
198 | fovrnd 6806 |
. . . . . . 7
|
202 | 199, 201 | remulcld 10070 |
. . . . . 6
|
203 | 202 | recnd 10068 |
. . . . 5
|
204 | 158 | ssdifd 3746 |
. . . . . . 7
|
205 | 204 | sselda 3603 |
. . . . . 6
|
206 | | eldifi 3732 |
. . . . . . . . . . . . 13
|
207 | 206 | ad2antrl 764 |
. . . . . . . . . . . 12
|
208 | 68 | adantr 481 |
. . . . . . . . . . . 12
|
209 | | simprr 796 |
. . . . . . . . . . . 12
|
210 | 1, 2, 107 | itg1addlem3 23465 |
. . . . . . . . . . . 12
|
211 | 207, 208,
209, 210 | syl21anc 1325 |
. . . . . . . . . . 11
|
212 | | inss1 3833 |
. . . . . . . . . . . . . . 15
|
213 | | eldifn 3733 |
. . . . . . . . . . . . . . . . . . 19
|
214 | 213 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . 18
|
215 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . 20
|
216 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . 21
|
217 | 216 | eliniseg 5494 |
. . . . . . . . . . . . . . . . . . . 20
|
218 | 215, 217 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
|
219 | 216, 215 | brelrn 5356 |
. . . . . . . . . . . . . . . . . . 19
|
220 | 218, 219 | sylbi 207 |
. . . . . . . . . . . . . . . . . 18
|
221 | 214, 220 | nsyl 135 |
. . . . . . . . . . . . . . . . 17
|
222 | 221 | pm2.21d 118 |
. . . . . . . . . . . . . . . 16
|
223 | 222 | ssrdv 3609 |
. . . . . . . . . . . . . . 15
|
224 | 212, 223 | syl5ss 3614 |
. . . . . . . . . . . . . 14
|
225 | | ss0 3974 |
. . . . . . . . . . . . . 14
|
226 | 224, 225 | syl 17 |
. . . . . . . . . . . . 13
|
227 | 226 | fveq2d 6195 |
. . . . . . . . . . . 12
|
228 | | 0mbl 23307 |
. . . . . . . . . . . . . 14
|
229 | | mblvol 23298 |
. . . . . . . . . . . . . 14
|
230 | 228, 229 | ax-mp 5 |
. . . . . . . . . . . . 13
|
231 | | ovol0 23261 |
. . . . . . . . . . . . 13
|
232 | 230, 231 | eqtri 2644 |
. . . . . . . . . . . 12
|
233 | 227, 232 | syl6eq 2672 |
. . . . . . . . . . 11
|
234 | 211, 233 | eqtrd 2656 |
. . . . . . . . . 10
|
235 | 234 | oveq2d 6666 |
. . . . . . . . 9
|
236 | 207, 208 | readdcld 10069 |
. . . . . . . . . . 11
|
237 | 236 | recnd 10068 |
. . . . . . . . . 10
|
238 | 237 | mul01d 10235 |
. . . . . . . . 9
|
239 | 235, 238 | eqtrd 2656 |
. . . . . . . 8
|
240 | 239 | expr 643 |
. . . . . . 7
|
241 | | oveq12 6659 |
. . . . . . . . . 10
|
242 | 241, 103 | syl6eq 2672 |
. . . . . . . . 9
|
243 | | oveq12 6659 |
. . . . . . . . . 10
|
244 | | 0re 10040 |
. . . . . . . . . . 11
|
245 | | iftrue 4092 |
. . . . . . . . . . . 12
|
246 | | c0ex 10034 |
. . . . . . . . . . . 12
|
247 | 245, 107,
246 | ovmpt2a 6791 |
. . . . . . . . . . 11
|
248 | 244, 244,
247 | mp2an 708 |
. . . . . . . . . 10
|
249 | 243, 248 | syl6eq 2672 |
. . . . . . . . 9
|
250 | 242, 249 | oveq12d 6668 |
. . . . . . . 8
|
251 | | 0cn 10032 |
. . . . . . . . 9
|
252 | 251 | mul01i 10226 |
. . . . . . . 8
|
253 | 250, 252 | syl6eq 2672 |
. . . . . . 7
|
254 | 240, 253 | pm2.61d2 172 |
. . . . . 6
|
255 | 205, 254 | syldan 487 |
. . . . 5
|
256 | | f1ofo 6144 |
. . . . . . 7
|
257 | 150, 256 | syl 17 |
. . . . . 6
|
258 | | fofi 8252 |
. . . . . 6
|
259 | 133, 257,
258 | syl2anc 693 |
. . . . 5
|
260 | 197, 203,
255, 259 | fsumss 14456 |
. . . 4
|
261 | 35 | a1i 11 |
. . . . 5
|
262 | 126 | an32s 846 |
. . . . 5
|
263 | | dfin4 3867 |
. . . . . . . 8
|
264 | | inss2 3834 |
. . . . . . . 8
|
265 | 263, 264 | eqsstr3i 3636 |
. . . . . . 7
|
266 | 265 | sseli 3599 |
. . . . . 6
|
267 | | elsni 4194 |
. . . . . . . . 9
|
268 | 267 | adantl 482 |
. . . . . . . 8
|
269 | 268 | oveq1d 6665 |
. . . . . . 7
|
270 | 110 | ad2antrr 762 |
. . . . . . . . . 10
|
271 | 268, 244 | syl6eqel 2709 |
. . . . . . . . . . 11
|
272 | 68 | adantr 481 |
. . . . . . . . . . 11
|
273 | 271, 272 | resubcld 10458 |
. . . . . . . . . 10
|
274 | 270, 273,
272 | fovrnd 6806 |
. . . . . . . . 9
|
275 | 274 | recnd 10068 |
. . . . . . . 8
|
276 | 275 | mul02d 10234 |
. . . . . . 7
|
277 | 269, 276 | eqtrd 2656 |
. . . . . 6
|
278 | 266, 277 | sylan2 491 |
. . . . 5
|
279 | 261, 262,
278, 133 | fsumss 14456 |
. . . 4
|
280 | 173, 260,
279 | 3eqtr4d 2666 |
. . 3
|
281 | 280 | sumeq2dv 14433 |
. 2
|
282 | 203 | anasss 679 |
. . 3
|
283 | 7, 5, 282 | fsumcom 14507 |
. 2
|
284 | 129, 281,
283 | 3eqtr2d 2662 |
1
|