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

Theorem iblss 25091
Description: A subset of an integrable function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.)
Hypotheses
Ref Expression
iblss.1 (šœ‘ ā†’ š“ āŠ† šµ)
iblss.2 (šœ‘ ā†’ š“ āˆˆ dom vol)
iblss.3 ((šœ‘ āˆ§ š‘„ āˆˆ šµ) ā†’ š¶ āˆˆ š‘‰)
iblss.4 (šœ‘ ā†’ (š‘„ āˆˆ šµ ā†¦ š¶) āˆˆ šæ1)
Assertion
Ref Expression
iblss (šœ‘ ā†’ (š‘„ āˆˆ š“ ā†¦ š¶) āˆˆ šæ1)
Distinct variable groups:   š‘„,š“   š‘„,šµ   šœ‘,š‘„   š‘„,š‘‰
Allowed substitution hint:   š¶(š‘„)

Proof of Theorem iblss
Dummy variable š‘˜ is distinct from all other variables.
StepHypRef Expression
1 iblss.1 . . . 4 (šœ‘ ā†’ š“ āŠ† šµ)
21resmptd 5991 . . 3 (šœ‘ ā†’ ((š‘„ āˆˆ šµ ā†¦ š¶) ā†¾ š“) = (š‘„ āˆˆ š“ ā†¦ š¶))
3 iblss.4 . . . . 5 (šœ‘ ā†’ (š‘„ āˆˆ šµ ā†¦ š¶) āˆˆ šæ1)
4 iblmbf 25054 . . . . 5 ((š‘„ āˆˆ šµ ā†¦ š¶) āˆˆ šæ1 ā†’ (š‘„ āˆˆ šµ ā†¦ š¶) āˆˆ MblFn)
53, 4syl 17 . . . 4 (šœ‘ ā†’ (š‘„ āˆˆ šµ ā†¦ š¶) āˆˆ MblFn)
6 iblss.2 . . . 4 (šœ‘ ā†’ š“ āˆˆ dom vol)
7 mbfres 24930 . . . 4 (((š‘„ āˆˆ šµ ā†¦ š¶) āˆˆ MblFn āˆ§ š“ āˆˆ dom vol) ā†’ ((š‘„ āˆˆ šµ ā†¦ š¶) ā†¾ š“) āˆˆ MblFn)
85, 6, 7syl2anc 585 . . 3 (šœ‘ ā†’ ((š‘„ āˆˆ šµ ā†¦ š¶) ā†¾ š“) āˆˆ MblFn)
92, 8eqeltrrd 2840 . 2 (šœ‘ ā†’ (š‘„ āˆˆ š“ ā†¦ š¶) āˆˆ MblFn)
10 ifan 4538 . . . . . 6 if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) = if(š‘„ āˆˆ š“, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0)
111sselda 3943 . . . . . . . . 9 ((šœ‘ āˆ§ š‘„ āˆˆ š“) ā†’ š‘„ āˆˆ šµ)
1211ad4ant14 751 . . . . . . . 8 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ š“) ā†’ š‘„ āˆˆ šµ)
13 iblss.3 . . . . . . . . . . . . . . 15 ((šœ‘ āˆ§ š‘„ āˆˆ šµ) ā†’ š¶ āˆˆ š‘‰)
145, 13mbfmptcl 24922 . . . . . . . . . . . . . 14 ((šœ‘ āˆ§ š‘„ āˆˆ šµ) ā†’ š¶ āˆˆ ā„‚)
1514ad4ant14 751 . . . . . . . . . . . . 13 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ š¶ āˆˆ ā„‚)
16 ax-icn 11044 . . . . . . . . . . . . . 14 i āˆˆ ā„‚
17 ine0 11524 . . . . . . . . . . . . . 14 i ā‰  0
18 elfzelz 13370 . . . . . . . . . . . . . . 15 (š‘˜ āˆˆ (0...3) ā†’ š‘˜ āˆˆ ā„¤)
1918ad3antlr 730 . . . . . . . . . . . . . 14 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ š‘˜ āˆˆ ā„¤)
20 expclz 13921 . . . . . . . . . . . . . 14 ((i āˆˆ ā„‚ āˆ§ i ā‰  0 āˆ§ š‘˜ āˆˆ ā„¤) ā†’ (iā†‘š‘˜) āˆˆ ā„‚)
2116, 17, 19, 20mp3an12i 1466 . . . . . . . . . . . . 13 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ (iā†‘š‘˜) āˆˆ ā„‚)
22 expne0i 13929 . . . . . . . . . . . . . 14 ((i āˆˆ ā„‚ āˆ§ i ā‰  0 āˆ§ š‘˜ āˆˆ ā„¤) ā†’ (iā†‘š‘˜) ā‰  0)
2316, 17, 19, 22mp3an12i 1466 . . . . . . . . . . . . 13 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ (iā†‘š‘˜) ā‰  0)
2415, 21, 23divcld 11865 . . . . . . . . . . . 12 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ (š¶ / (iā†‘š‘˜)) āˆˆ ā„‚)
2524recld 15013 . . . . . . . . . . 11 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ (ā„œā€˜(š¶ / (iā†‘š‘˜))) āˆˆ ā„)
26 0re 11091 . . . . . . . . . . 11 0 āˆˆ ā„
27 ifcl 4530 . . . . . . . . . . 11 (((ā„œā€˜(š¶ / (iā†‘š‘˜))) āˆˆ ā„ āˆ§ 0 āˆˆ ā„) ā†’ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) āˆˆ ā„)
2825, 26, 27sylancl 587 . . . . . . . . . 10 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) āˆˆ ā„)
2928rexrd 11139 . . . . . . . . 9 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) āˆˆ ā„*)
30 max1 13033 . . . . . . . . . 10 ((0 āˆˆ ā„ āˆ§ (ā„œā€˜(š¶ / (iā†‘š‘˜))) āˆˆ ā„) ā†’ 0 ā‰¤ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))
3126, 25, 30sylancr 588 . . . . . . . . 9 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ 0 ā‰¤ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))
32 elxrge0 13303 . . . . . . . . 9 (if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) āˆˆ (0[,]+āˆž) ā†” (if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) āˆˆ ā„* āˆ§ 0 ā‰¤ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)))
3329, 31, 32sylanbrc 584 . . . . . . . 8 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) āˆˆ (0[,]+āˆž))
3412, 33syldan 592 . . . . . . 7 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ š“) ā†’ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) āˆˆ (0[,]+āˆž))
35 0e0iccpnf 13305 . . . . . . . 8 0 āˆˆ (0[,]+āˆž)
3635a1i 11 . . . . . . 7 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ Ā¬ š‘„ āˆˆ š“) ā†’ 0 āˆˆ (0[,]+āˆž))
3734, 36ifclda 4520 . . . . . 6 (((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) ā†’ if(š‘„ āˆˆ š“, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) āˆˆ (0[,]+āˆž))
3810, 37eqeltrid 2843 . . . . 5 (((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) ā†’ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) āˆˆ (0[,]+āˆž))
3938fmpttd 7058 . . . 4 ((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) ā†’ (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)):ā„āŸ¶(0[,]+āˆž))
40 eqidd 2739 . . . . . 6 (šœ‘ ā†’ (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)) = (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)))
41 eqidd 2739 . . . . . 6 ((šœ‘ āˆ§ š‘„ āˆˆ šµ) ā†’ (ā„œā€˜(š¶ / (iā†‘š‘˜))) = (ā„œā€˜(š¶ / (iā†‘š‘˜))))
4240, 41, 3, 13iblitg 25055 . . . . 5 ((šœ‘ āˆ§ š‘˜ āˆˆ ā„¤) ā†’ (āˆ«2ā€˜(š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))) āˆˆ ā„)
4318, 42sylan2 594 . . . 4 ((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) ā†’ (āˆ«2ā€˜(š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))) āˆˆ ā„)
44 ifan 4538 . . . . . . 7 if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) = if(š‘„ āˆˆ šµ, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0)
4535a1i 11 . . . . . . . 8 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ Ā¬ š‘„ āˆˆ šµ) ā†’ 0 āˆˆ (0[,]+āˆž))
4633, 45ifclda 4520 . . . . . . 7 (((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) ā†’ if(š‘„ āˆˆ šµ, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) āˆˆ (0[,]+āˆž))
4744, 46eqeltrid 2843 . . . . . 6 (((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) ā†’ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) āˆˆ (0[,]+āˆž))
4847fmpttd 7058 . . . . 5 ((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) ā†’ (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)):ā„āŸ¶(0[,]+āˆž))
4928leidd 11655 . . . . . . . . . . 11 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) ā‰¤ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))
50 breq1 5107 . . . . . . . . . . . 12 (if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) = if(š‘„ āˆˆ š“, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) ā†’ (if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) ā‰¤ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) ā†” if(š‘„ āˆˆ š“, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) ā‰¤ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)))
51 breq1 5107 . . . . . . . . . . . 12 (0 = if(š‘„ āˆˆ š“, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) ā†’ (0 ā‰¤ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) ā†” if(š‘„ āˆˆ š“, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) ā‰¤ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)))
5250, 51ifboth 4524 . . . . . . . . . . 11 ((if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) ā‰¤ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) āˆ§ 0 ā‰¤ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)) ā†’ if(š‘„ āˆˆ š“, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) ā‰¤ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))
5349, 31, 52syl2anc 585 . . . . . . . . . 10 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ if(š‘„ āˆˆ š“, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) ā‰¤ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))
54 iftrue 4491 . . . . . . . . . . 11 (š‘„ āˆˆ šµ ā†’ if(š‘„ āˆˆ šµ, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) = if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))
5554adantl 483 . . . . . . . . . 10 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ if(š‘„ āˆˆ šµ, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) = if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))
5653, 55breqtrrd 5132 . . . . . . . . 9 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ if(š‘„ āˆˆ š“, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) ā‰¤ if(š‘„ āˆˆ šµ, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0))
57 0le0 12188 . . . . . . . . . . 11 0 ā‰¤ 0
5857a1i 11 . . . . . . . . . 10 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ Ā¬ š‘„ āˆˆ šµ) ā†’ 0 ā‰¤ 0)
5912stoic1a 1775 . . . . . . . . . . 11 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ Ā¬ š‘„ āˆˆ šµ) ā†’ Ā¬ š‘„ āˆˆ š“)
6059iffalsed 4496 . . . . . . . . . 10 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ Ā¬ š‘„ āˆˆ šµ) ā†’ if(š‘„ āˆˆ š“, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) = 0)
61 iffalse 4494 . . . . . . . . . . 11 (Ā¬ š‘„ āˆˆ šµ ā†’ if(š‘„ āˆˆ šµ, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) = 0)
6261adantl 483 . . . . . . . . . 10 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ Ā¬ š‘„ āˆˆ šµ) ā†’ if(š‘„ āˆˆ šµ, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) = 0)
6358, 60, 623brtr4d 5136 . . . . . . . . 9 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ Ā¬ š‘„ āˆˆ šµ) ā†’ if(š‘„ āˆˆ š“, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) ā‰¤ if(š‘„ āˆˆ šµ, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0))
6456, 63pm2.61dan 812 . . . . . . . 8 (((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) ā†’ if(š‘„ āˆˆ š“, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) ā‰¤ if(š‘„ āˆˆ šµ, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0))
6564, 10, 443brtr4g 5138 . . . . . . 7 (((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) ā†’ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) ā‰¤ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))
6665ralrimiva 3142 . . . . . 6 ((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) ā†’ āˆ€š‘„ āˆˆ ā„ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) ā‰¤ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))
67 reex 11076 . . . . . . . 8 ā„ āˆˆ V
6867a1i 11 . . . . . . 7 ((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) ā†’ ā„ āˆˆ V)
69 eqidd 2739 . . . . . . 7 ((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) ā†’ (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)) = (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)))
70 eqidd 2739 . . . . . . 7 ((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) ā†’ (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)) = (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)))
7168, 38, 47, 69, 70ofrfval2 7629 . . . . . 6 ((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) ā†’ ((š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)) āˆ˜r ā‰¤ (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)) ā†” āˆ€š‘„ āˆˆ ā„ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) ā‰¤ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)))
7266, 71mpbird 257 . . . . 5 ((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) ā†’ (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)) āˆ˜r ā‰¤ (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)))
73 itg2le 25026 . . . . 5 (((š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)):ā„āŸ¶(0[,]+āˆž) āˆ§ (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)):ā„āŸ¶(0[,]+āˆž) āˆ§ (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)) āˆ˜r ā‰¤ (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))) ā†’ (āˆ«2ā€˜(š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))) ā‰¤ (āˆ«2ā€˜(š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))))
7439, 48, 72, 73syl3anc 1372 . . . 4 ((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) ā†’ (āˆ«2ā€˜(š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))) ā‰¤ (āˆ«2ā€˜(š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))))
75 itg2lecl 25025 . . . 4 (((š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)):ā„āŸ¶(0[,]+āˆž) āˆ§ (āˆ«2ā€˜(š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))) āˆˆ ā„ āˆ§ (āˆ«2ā€˜(š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))) ā‰¤ (āˆ«2ā€˜(š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)))) ā†’ (āˆ«2ā€˜(š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))) āˆˆ ā„)
7639, 43, 74, 75syl3anc 1372 . . 3 ((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) ā†’ (āˆ«2ā€˜(š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))) āˆˆ ā„)
7776ralrimiva 3142 . 2 (šœ‘ ā†’ āˆ€š‘˜ āˆˆ (0...3)(āˆ«2ā€˜(š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))) āˆˆ ā„)
78 eqidd 2739 . . 3 (šœ‘ ā†’ (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)) = (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)))
79 eqidd 2739 . . 3 ((šœ‘ āˆ§ š‘„ āˆˆ š“) ā†’ (ā„œā€˜(š¶ / (iā†‘š‘˜))) = (ā„œā€˜(š¶ / (iā†‘š‘˜))))
8011, 14syldan 592 . . 3 ((šœ‘ āˆ§ š‘„ āˆˆ š“) ā†’ š¶ āˆˆ ā„‚)
8178, 79, 80isibl2 25053 . 2 (šœ‘ ā†’ ((š‘„ āˆˆ š“ ā†¦ š¶) āˆˆ šæ1 ā†” ((š‘„ āˆˆ š“ ā†¦ š¶) āˆˆ MblFn āˆ§ āˆ€š‘˜ āˆˆ (0...3)(āˆ«2ā€˜(š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))) āˆˆ ā„)))
829, 77, 81mpbir2and 712 1 (šœ‘ ā†’ (š‘„ āˆˆ š“ ā†¦ š¶) āˆˆ šæ1)
Colors of variables: wff setvar class
Syntax hints:  Ā¬ wn 3   ā†’ wi 4   āˆ§ wa 397   = wceq 1542   āˆˆ wcel 2107   ā‰  wne 2942  āˆ€wral 3063  Vcvv 3444   āŠ† wss 3909  ifcif 4485   class class class wbr 5104   ā†¦ cmpt 5187  dom cdm 5631   ā†¾ cres 5633  āŸ¶wf 6488  ā€˜cfv 6492  (class class class)co 7350   āˆ˜r cofr 7607  ā„‚cc 10983  ā„cr 10984  0cc0 10985  ici 10987  +āˆžcpnf 11120  ā„*cxr 11122   ā‰¤ cle 11124   / cdiv 11746  3c3 12143  ā„¤cz 12433  [,]cicc 13196  ...cfz 13353  ā†‘cexp 13896  ā„œcre 14916  volcvol 24749  MblFncmbf 24900  āˆ«2citg2 24902  šæ1cibl 24903
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-rep 5241  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7663  ax-inf2 9511  ax-cnex 11041  ax-resscn 11042  ax-1cn 11043  ax-icn 11044  ax-addcl 11045  ax-addrcl 11046  ax-mulcl 11047  ax-mulrcl 11048  ax-mulcom 11049  ax-addass 11050  ax-mulass 11051  ax-distr 11052  ax-i2m1 11053  ax-1ne0 11054  ax-1rid 11055  ax-rnegex 11056  ax-rrecex 11057  ax-cnre 11058  ax-pre-lttri 11059  ax-pre-lttrn 11060  ax-pre-ltadd 11061  ax-pre-mulgt0 11062  ax-pre-sup 11063
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-int 4907  df-iun 4955  df-br 5105  df-opab 5167  df-mpt 5188  df-tr 5222  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-se 5587  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6250  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6444  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7306  df-ov 7353  df-oprab 7354  df-mpo 7355  df-of 7608  df-ofr 7609  df-om 7794  df-1st 7912  df-2nd 7913  df-frecs 8180  df-wrecs 8211  df-recs 8285  df-rdg 8324  df-1o 8380  df-2o 8381  df-er 8582  df-map 8701  df-pm 8702  df-en 8818  df-dom 8819  df-sdom 8820  df-fin 8821  df-sup 9312  df-inf 9313  df-oi 9380  df-dju 9771  df-card 9809  df-pnf 11125  df-mnf 11126  df-xr 11127  df-ltxr 11128  df-le 11129  df-sub 11321  df-neg 11322  df-div 11747  df-nn 12088  df-2 12150  df-3 12151  df-4 12152  df-n0 12348  df-z 12434  df-uz 12697  df-q 12803  df-rp 12845  df-xadd 12963  df-ioo 13197  df-ico 13199  df-icc 13200  df-fz 13354  df-fzo 13497  df-fl 13626  df-mod 13704  df-seq 13836  df-exp 13897  df-hash 14159  df-cj 14918  df-re 14919  df-im 14920  df-sqrt 15054  df-abs 15055  df-clim 15305  df-sum 15506  df-xmet 20712  df-met 20713  df-ovol 24750  df-vol 24751  df-mbf 24905  df-itg1 24906  df-itg2 24907  df-ibl 24908
This theorem is referenced by:  itgss3  25101  itgless  25103  bddmulibl  25125  itgcn  25131  ditgcl  25144  ditgswap  25145  ditgsplitlem  25146  ftc1lem1  25321  ftc1lem2  25322  ftc1a  25323  ftc1lem4  25325  ftc2  25330  ftc2ditglem  25331  itgsubstlem  25334  itgpowd  25336  fdvposlt  32973  fdvposle  32975  circlemeth  33014  ftc1cnnclem  36035  ftc1anc  36045  ftc2nc  36046  areacirc  36057  lcmineqlem10  40381  lcmineqlem12  40383  lhe4.4ex1a  42342  itgsin0pilem1  43901  iblioosinexp  43904  itgsinexplem1  43905  itgsinexp  43906  itgcoscmulx  43920  itgsincmulx  43925  iblcncfioo  43929  dirkeritg  44053  fourierdlem87  44144  fourierdlem95  44152  fourierdlem103  44160  fourierdlem104  44161  fourierdlem107  44164  fourierdlem111  44168  fourierdlem112  44169  sqwvfoura  44179  sqwvfourb  44180  etransclem18  44203
  Copyright terms: Public domain W3C validator