Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  itg2splitlem Structured version   Visualization version   Unicode version

Theorem itg2splitlem 22785
 Description: Lemma for itg2split 22786. (Contributed by Mario Carneiro, 11-Aug-2014.)
Hypotheses
Ref Expression
itg2split.a
itg2split.b
itg2split.i
itg2split.u
itg2split.c
itg2split.f
itg2split.g
itg2split.h
itg2split.sf
itg2split.sg
Assertion
Ref Expression
itg2splitlem
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()

Proof of Theorem itg2splitlem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simprl 772 . . . . . 6
2 itg1cl 22722 . . . . . 6
31, 2syl 17 . . . . 5
4 itg2split.a . . . . . . . . 9
54adantr 472 . . . . . . . 8
6 eqid 2471 . . . . . . . . 9
76i1fres 22742 . . . . . . . 8
81, 5, 7syl2anc 673 . . . . . . 7
9 itg1cl 22722 . . . . . . 7
108, 9syl 17 . . . . . 6
11 itg2split.b . . . . . . . . 9
1211adantr 472 . . . . . . . 8
13 eqid 2471 . . . . . . . . 9
1413i1fres 22742 . . . . . . . 8
151, 12, 14syl2anc 673 . . . . . . 7
16 itg1cl 22722 . . . . . . 7
1715, 16syl 17 . . . . . 6
1810, 17readdcld 9688 . . . . 5
19 itg2split.sf . . . . . . 7
20 itg2split.sg . . . . . . 7
2119, 20readdcld 9688 . . . . . 6
2221adantr 472 . . . . 5
23 inss1 3643 . . . . . . . . 9
24 mblss 22563 . . . . . . . . . 10
254, 24syl 17 . . . . . . . . 9
2623, 25syl5ss 3429 . . . . . . . 8
2726adantr 472 . . . . . . 7
28 itg2split.i . . . . . . . 8
2928adantr 472 . . . . . . 7
30 reex 9648 . . . . . . . . . . 11
3130a1i 11 . . . . . . . . . 10
32 fvex 5889 . . . . . . . . . . . 12
33 c0ex 9655 . . . . . . . . . . . 12
3432, 33ifex 3940 . . . . . . . . . . 11
3534a1i 11 . . . . . . . . . 10
3632, 33ifex 3940 . . . . . . . . . . 11
3736a1i 11 . . . . . . . . . 10
38 eqidd 2472 . . . . . . . . . 10
39 eqidd 2472 . . . . . . . . . 10
4031, 35, 37, 38, 39offval2 6567 . . . . . . . . 9
4140adantr 472 . . . . . . . 8
428, 15i1fadd 22732 . . . . . . . 8
4341, 42eqeltrrd 2550 . . . . . . 7
44 i1ff 22713 . . . . . . . . . . . . . 14
451, 44syl 17 . . . . . . . . . . . . 13
46 eldifi 3544 . . . . . . . . . . . . 13
47 ffvelrn 6035 . . . . . . . . . . . . 13
4845, 46, 47syl2an 485 . . . . . . . . . . . 12
4948leidd 10201 . . . . . . . . . . 11
5049adantr 472 . . . . . . . . . 10
51 iftrue 3878 . . . . . . . . . . . . 13
5251adantl 473 . . . . . . . . . . . 12
53 eldifn 3545 . . . . . . . . . . . . . . . . 17
5453adantl 473 . . . . . . . . . . . . . . . 16
55 elin 3608 . . . . . . . . . . . . . . . 16
5654, 55sylnib 311 . . . . . . . . . . . . . . 15
57 imnan 429 . . . . . . . . . . . . . . 15
5856, 57sylibr 217 . . . . . . . . . . . . . 14
5958imp 436 . . . . . . . . . . . . 13
60 iffalse 3881 . . . . . . . . . . . . 13
6159, 60syl 17 . . . . . . . . . . . 12
6252, 61oveq12d 6326 . . . . . . . . . . 11
6348recnd 9687 . . . . . . . . . . . . 13
6463adantr 472 . . . . . . . . . . . 12
6564addid1d 9851 . . . . . . . . . . 11
6662, 65eqtrd 2505 . . . . . . . . . 10
6750, 66breqtrrd 4422 . . . . . . . . 9
6849ad2antrr 740 . . . . . . . . . . . 12
69 iftrue 3878 . . . . . . . . . . . . 13
7069adantl 473 . . . . . . . . . . . 12
7168, 70breqtrrd 4422 . . . . . . . . . . 11
72 itg2split.u . . . . . . . . . . . . . . . . . . . 20
7372ad2antrr 740 . . . . . . . . . . . . . . . . . . 19
7473eleq2d 2534 . . . . . . . . . . . . . . . . . 18
75 elun 3565 . . . . . . . . . . . . . . . . . 18
7674, 75syl6bb 269 . . . . . . . . . . . . . . . . 17
7776notbid 301 . . . . . . . . . . . . . . . 16
78 ioran 498 . . . . . . . . . . . . . . . 16
7977, 78syl6bb 269 . . . . . . . . . . . . . . 15
8079biimpar 493 . . . . . . . . . . . . . 14
81 simprr 774 . . . . . . . . . . . . . . . . . . 19
82 ffn 5739 . . . . . . . . . . . . . . . . . . . . 21
8345, 82syl 17 . . . . . . . . . . . . . . . . . . . 20
84 itg2split.c . . . . . . . . . . . . . . . . . . . . . . . . 25
8584adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . 24
86 0e0iccpnf 11769 . . . . . . . . . . . . . . . . . . . . . . . . 25
8786a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24
8885, 87ifclda 3904 . . . . . . . . . . . . . . . . . . . . . . 23
89 itg2split.h . . . . . . . . . . . . . . . . . . . . . . 23
9088, 89fmptd 6061 . . . . . . . . . . . . . . . . . . . . . 22
91 ffn 5739 . . . . . . . . . . . . . . . . . . . . . 22
9290, 91syl 17 . . . . . . . . . . . . . . . . . . . . 21
9392adantr 472 . . . . . . . . . . . . . . . . . . . 20
9430a1i 11 . . . . . . . . . . . . . . . . . . . 20
95 inidm 3632 . . . . . . . . . . . . . . . . . . . 20
96 eqidd 2472 . . . . . . . . . . . . . . . . . . . 20
97 eqidd 2472 . . . . . . . . . . . . . . . . . . . 20
9883, 93, 94, 94, 95, 96, 97ofrfval 6558 . . . . . . . . . . . . . . . . . . 19
9981, 98mpbid 215 . . . . . . . . . . . . . . . . . 18
10099r19.21bi 2776 . . . . . . . . . . . . . . . . 17
10146, 100sylan2 482 . . . . . . . . . . . . . . . 16
102101adantr 472 . . . . . . . . . . . . . . 15
10346adantl 473 . . . . . . . . . . . . . . . 16
104 eldif 3400 . . . . . . . . . . . . . . . . 17
105 nfcv 2612 . . . . . . . . . . . . . . . . . 18
106 nfmpt1 4485 . . . . . . . . . . . . . . . . . . . . 21
10789, 106nfcxfr 2610 . . . . . . . . . . . . . . . . . . . 20
108107, 105nffv 5886 . . . . . . . . . . . . . . . . . . 19
109108nfeq1 2625 . . . . . . . . . . . . . . . . . 18
110 fveq2 5879 . . . . . . . . . . . . . . . . . . 19
111110eqeq1d 2473 . . . . . . . . . . . . . . . . . 18
112 eldif 3400 . . . . . . . . . . . . . . . . . . 19
11389fvmpt2i 5971 . . . . . . . . . . . . . . . . . . . 20
114 iffalse 3881 . . . . . . . . . . . . . . . . . . . . . 22
115114fveq2d 5883 . . . . . . . . . . . . . . . . . . . . 21
116 0cn 9653 . . . . . . . . . . . . . . . . . . . . . 22
117 fvi 5937 . . . . . . . . . . . . . . . . . . . . . 22
118116, 117ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21
119115, 118syl6eq 2521 . . . . . . . . . . . . . . . . . . . 20
120113, 119sylan9eq 2525 . . . . . . . . . . . . . . . . . . 19
121112, 120sylbi 200 . . . . . . . . . . . . . . . . . 18
122105, 109, 111, 121vtoclgaf 3098 . . . . . . . . . . . . . . . . 17
123104, 122sylbir 218 . . . . . . . . . . . . . . . 16
124103, 123sylan 479 . . . . . . . . . . . . . . 15
125102, 124breqtrd 4420 . . . . . . . . . . . . . 14
12680, 125syldan 478 . . . . . . . . . . . . 13
127126anassrs 660 . . . . . . . . . . . 12
12860adantl 473 . . . . . . . . . . . 12
129127, 128breqtrrd 4422 . . . . . . . . . . 11
13071, 129pm2.61dan 808 . . . . . . . . . 10
131 iffalse 3881 . . . . . . . . . . . . 13
132131adantl 473 . . . . . . . . . . . 12
133132oveq1d 6323 . . . . . . . . . . 11
134 0re 9661 . . . . . . . . . . . . . . 15
135 ifcl 3914 . . . . . . . . . . . . . . 15
13648, 134, 135sylancl 675 . . . . . . . . . . . . . 14
137136recnd 9687 . . . . . . . . . . . . 13
138137adantr 472 . . . . . . . . . . . 12
139138addid2d 9852 . . . . . . . . . . 11
140133, 139eqtrd 2505 . . . . . . . . . 10
141130, 140breqtrrd 4422 . . . . . . . . 9
14267, 141pm2.61dan 808 . . . . . . . 8
143 eleq1 2537 . . . . . . . . . . . 12
144 fveq2 5879 . . . . . . . . . . . 12
145143, 144ifbieq1d 3895 . . . . . . . . . . 11
146 eleq1 2537 . . . . . . . . . . . 12
147146, 144ifbieq1d 3895 . . . . . . . . . . 11
148145, 147oveq12d 6326 . . . . . . . . . 10
149 eqid 2471 . . . . . . . . . 10
150 ovex 6336 . . . . . . . . . 10
151148, 149, 150fvmpt 5963 . . . . . . . . 9
152103, 151syl 17 . . . . . . . 8
153142, 152breqtrrd 4422 . . . . . . 7
1541, 27, 29, 43, 153itg1lea 22749 . . . . . 6
15541fveq2d 5883 . . . . . . 7
1568, 15itg1add 22738 . . . . . . 7
157155, 156eqtr3d 2507 . . . . . 6
158154, 157breqtrd 4420 . . . . 5
15919adantr 472 . . . . . 6
16020adantr 472 . . . . . 6
161 ssun1 3588 . . . . . . . . . . . . . 14
162161, 72syl5sseqr 3467 . . . . . . . . . . . . 13
163162sselda 3418 . . . . . . . . . . . 12
164163adantlr 729 . . . . . . . . . . 11
165164, 85syldan 478 . . . . . . . . . 10
16686a1i 11 . . . . . . . . . 10
167165, 166ifclda 3904 . . . . . . . . 9
168 itg2split.f . . . . . . . . 9
169167, 168fmptd 6061 . . . . . . . 8
170169adantr 472 . . . . . . 7
171 nfv 1769 . . . . . . . . . 10
172 nfv 1769 . . . . . . . . . . 11
173 nfcv 2612 . . . . . . . . . . . 12
174 nfcv 2612 . . . . . . . . . . . 12
175173, 174, 107nfbr 4440 . . . . . . . . . . 11
176172, 175nfan 2031 . . . . . . . . . 10
177171, 176nfan 2031 . . . . . . . . 9
1785, 24syl 17 . . . . . . . . . . . . . . 15
179178sselda 3418 . . . . . . . . . . . . . 14
18030a1i 11 . . . . . . . . . . . . . . . . . 18
18132a1i 11 . . . . . . . . . . . . . . . . . 18
18288adantlr 729 . . . . . . . . . . . . . . . . . 18
18344adantl 473 . . . . . . . . . . . . . . . . . . 19
184183feqmptd 5932 . . . . . . . . . . . . . . . . . 18
18589a1i 11 . . . . . . . . . . . . . . . . . 18
186180, 181, 182, 184, 185ofrfval2 6568 . . . . . . . . . . . . . . . . 17
187186biimpd 212 . . . . . . . . . . . . . . . 16
188187impr 631 . . . . . . . . . . . . . . 15
189188r19.21bi 2776 . . . . . . . . . . . . . 14
190179, 189syldan 478 . . . . . . . . . . . . 13
191163adantlr 729 . . . . . . . . . . . . . 14
192191iftrued 3880 . . . . . . . . . . . . 13
193190, 192breqtrd 4420 . . . . . . . . . . . 12
194 iftrue 3878 . . . . . . . . . . . . 13
195194adantl 473 . . . . . . . . . . . 12
196 iftrue 3878 . . . . . . . . . . . . 13
197196adantl 473 . . . . . . . . . . . 12
198193, 195, 1973brtr4d 4426 . . . . . . . . . . 11
199 0le0 10721 . . . . . . . . . . . . . 14
200199a1i 11 . . . . . . . . . . . . 13
201 iffalse 3881 . . . . . . . . . . . . 13
202 iffalse 3881 . . . . . . . . . . . . 13
203200, 201, 2023brtr4d 4426 . . . . . . . . . . . 12
204203adantl 473 . . . . . . . . . . 11
205198, 204pm2.61dan 808 . . . . . . . . . 10
206205a1d 25 . . . . . . . . 9
207177, 206ralrimi 2800 . . . . . . . 8
208168a1i 11 . . . . . . . . . 10
20931, 35, 167, 38, 208ofrfval2 6568 . . . . . . . . 9
210209adantr 472 . . . . . . . 8
211207, 210mpbird 240 . . . . . . 7
212 itg2ub 22770 . . . . . . 7
213170, 8, 211, 212syl3anc 1292 . . . . . 6
214 ssun2 3589 . . . . . . . . . . . . . 14
215214, 72syl5sseqr 3467 . . . . . . . . . . . . 13
216215sselda 3418 . . . . . . . . . . . 12
217216adantlr 729 . . . . . . . . . . 11
218217, 85syldan 478 . . . . . . . . . 10
21986a1i 11 . . . . . . . . . 10
220218, 219ifclda 3904 . . . . . . . . 9
221 itg2split.g . . . . . . . . 9
222220, 221fmptd 6061 . . . . . . . 8
223222adantr 472 . . . . . . 7
224 mblss 22563 . . . . . . . . . . . . . . . 16
22512, 224syl 17 . . . . . . . . . . . . . . 15
226225sselda 3418 . . . . . . . . . . . . . 14
227226, 189syldan 478 . . . . . . . . . . . . 13
228216adantlr 729 . . . . . . . . . . . . . 14
229228iftrued 3880 . . . . . . . . . . . . 13
230227, 229breqtrd 4420 . . . . . . . . . . . 12
231 iftrue 3878 . . . . . . . . . . . . 13
232231adantl 473 . . . . . . . . . . . 12
233 iftrue 3878 . . . . . . . . . . . . 13
234233adantl 473 . . . . . . . . . . . 12
235230, 232, 2343brtr4d 4426 . . . . . . . . . . 11
236199a1i 11 . . . . . . . . . . . . 13
237 iffalse 3881 . . . . . . . . . . . . 13
238 iffalse 3881 . . . . . . . . . . . . 13
239236, 237, 2383brtr4d 4426 . . . . . . . . . . . 12
240239adantl 473 . . . . . . . . . . 11
241235, 240pm2.61dan 808 . . . . . . . . . 10
242241a1d 25 . . . . . . . . 9
243177, 242ralrimi 2800 . . . . . . . 8
244221a1i 11 . . . . . . . . . 10
24531, 37, 220, 39, 244ofrfval2 6568 . . . . . . . . 9
246245adantr 472 . . . . . . . 8
247243, 246mpbird 240 . . . . . . 7
248 itg2ub 22770 . . . . . . 7
249223, 15, 247, 248syl3anc 1292 . . . . . 6
25010, 17, 159, 160, 213, 249le2addd 10253 . . . . 5
2513, 18, 22, 158, 250letrd 9809 . . . 4
252251expr 626 . . 3
253252ralrimiva 2809 . 2
25421rexrd 9708 . . 3
255 itg2leub 22771 . . 3
25690, 254, 255syl2anc 673 . 2
257253, 256mpbird 240 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 189   wo 375   wa 376   wceq 1452   wcel 1904  wral 2756  cvv 3031   cdif 3387   cun 3388   cin 3389   wss 3390  cif 3872   class class class wbr 4395   cmpt 4454   cid 4749   cdm 4839   wfn 5584  wf 5585  cfv 5589  (class class class)co 6308   cof 6548   cofr 6549  cc 9555  cr 9556  cc0 9557   caddc 9560   cpnf 9690  cxr 9692   cle 9694  cicc 11663  covol 22491  cvol 22493  citg1 22652  citg2 22653 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634  ax-pre-sup 9635  ax-addf 9636 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-disj 4367  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-of 6550  df-ofr 6551  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-2o 7201  df-oadd 7204  df-er 7381  df-map 7492  df-pm 7493  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-fi 7943  df-sup 7974  df-inf 7975  df-oi 8043  df-card 8391  df-cda 8616  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-3 10691  df-n0 10894  df-z 10962  df-uz 11183  df-q 11288  df-rp 11326  df-xneg 11432  df-xadd 11433  df-xmul 11434  df-ioo 11664  df-ico 11666  df-icc 11667  df-fz 11811  df-fzo 11943  df-fl 12061  df-seq 12252  df-exp 12311  df-hash 12554  df-cj 13239  df-re 13240  df-im 13241  df-sqrt 13375  df-abs 13376  df-clim 13629  df-sum 13830  df-rest 15399  df-topgen 15420  df-psmet 19039  df-xmet 19040  df-met 19041  df-bl 19042  df-mopn 19043  df-top 19998  df-bases 19999  df-topon 20000  df-cmp 20479  df-ovol 22494  df-vol 22496  df-mbf 22656  df-itg1 22657  df-itg2 22658 This theorem is referenced by:  itg2split  22786
 Copyright terms: Public domain W3C validator