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 5990 . . 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 584 . . 3 (šœ‘ ā†’ ((š‘„ āˆˆ šµ ā†¦ š¶) ā†¾ š“) āˆˆ MblFn)
92, 8eqeltrrd 2839 . 2 (šœ‘ ā†’ (š‘„ āˆˆ š“ ā†¦ š¶) āˆˆ MblFn)
10 ifan 4537 . . . . . 6 if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) = if(š‘„ āˆˆ š“, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0)
111sselda 3942 . . . . . . . . 9 ((šœ‘ āˆ§ š‘„ āˆˆ š“) ā†’ š‘„ āˆˆ šµ)
1211ad4ant14 750 . . . . . . . 8 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ š“) ā†’ š‘„ āˆˆ šµ)
13 iblss.3 . . . . . . . . . . . . . . 15 ((šœ‘ āˆ§ š‘„ āˆˆ šµ) ā†’ š¶ āˆˆ š‘‰)
145, 13mbfmptcl 24922 . . . . . . . . . . . . . 14 ((šœ‘ āˆ§ š‘„ āˆˆ šµ) ā†’ š¶ āˆˆ ā„‚)
1514ad4ant14 750 . . . . . . . . . . . . 13 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ š¶ āˆˆ ā„‚)
16 ax-icn 11043 . . . . . . . . . . . . . 14 i āˆˆ ā„‚
17 ine0 11523 . . . . . . . . . . . . . 14 i ā‰  0
18 elfzelz 13369 . . . . . . . . . . . . . . 15 (š‘˜ āˆˆ (0...3) ā†’ š‘˜ āˆˆ ā„¤)
1918ad3antlr 729 . . . . . . . . . . . . . 14 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ š‘˜ āˆˆ ā„¤)
20 expclz 13920 . . . . . . . . . . . . . 14 ((i āˆˆ ā„‚ āˆ§ i ā‰  0 āˆ§ š‘˜ āˆˆ ā„¤) ā†’ (iā†‘š‘˜) āˆˆ ā„‚)
2116, 17, 19, 20mp3an12i 1465 . . . . . . . . . . . . 13 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ (iā†‘š‘˜) āˆˆ ā„‚)
22 expne0i 13928 . . . . . . . . . . . . . 14 ((i āˆˆ ā„‚ āˆ§ i ā‰  0 āˆ§ š‘˜ āˆˆ ā„¤) ā†’ (iā†‘š‘˜) ā‰  0)
2316, 17, 19, 22mp3an12i 1465 . . . . . . . . . . . . 13 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ (iā†‘š‘˜) ā‰  0)
2415, 21, 23divcld 11864 . . . . . . . . . . . 12 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ (š¶ / (iā†‘š‘˜)) āˆˆ ā„‚)
2524recld 15012 . . . . . . . . . . 11 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ (ā„œā€˜(š¶ / (iā†‘š‘˜))) āˆˆ ā„)
26 0re 11090 . . . . . . . . . . 11 0 āˆˆ ā„
27 ifcl 4529 . . . . . . . . . . 11 (((ā„œā€˜(š¶ / (iā†‘š‘˜))) āˆˆ ā„ āˆ§ 0 āˆˆ ā„) ā†’ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) āˆˆ ā„)
2825, 26, 27sylancl 586 . . . . . . . . . 10 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) āˆˆ ā„)
2928rexrd 11138 . . . . . . . . 9 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) āˆˆ ā„*)
30 max1 13032 . . . . . . . . . 10 ((0 āˆˆ ā„ āˆ§ (ā„œā€˜(š¶ / (iā†‘š‘˜))) āˆˆ ā„) ā†’ 0 ā‰¤ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))
3126, 25, 30sylancr 587 . . . . . . . . 9 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ 0 ā‰¤ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))
32 elxrge0 13302 . . . . . . . . 9 (if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) āˆˆ (0[,]+āˆž) ā†” (if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) āˆˆ ā„* āˆ§ 0 ā‰¤ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)))
3329, 31, 32sylanbrc 583 . . . . . . . 8 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) āˆˆ (0[,]+āˆž))
3412, 33syldan 591 . . . . . . 7 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ š“) ā†’ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) āˆˆ (0[,]+āˆž))
35 0e0iccpnf 13304 . . . . . . . 8 0 āˆˆ (0[,]+āˆž)
3635a1i 11 . . . . . . 7 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ Ā¬ š‘„ āˆˆ š“) ā†’ 0 āˆˆ (0[,]+āˆž))
3734, 36ifclda 4519 . . . . . 6 (((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) ā†’ if(š‘„ āˆˆ š“, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) āˆˆ (0[,]+āˆž))
3810, 37eqeltrid 2842 . . . . 5 (((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) ā†’ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) āˆˆ (0[,]+āˆž))
3938fmpttd 7057 . . . 4 ((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) ā†’ (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)):ā„āŸ¶(0[,]+āˆž))
40 eqidd 2738 . . . . . 6 (šœ‘ ā†’ (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)) = (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)))
41 eqidd 2738 . . . . . 6 ((šœ‘ āˆ§ š‘„ āˆˆ šµ) ā†’ (ā„œā€˜(š¶ / (iā†‘š‘˜))) = (ā„œā€˜(š¶ / (iā†‘š‘˜))))
4240, 41, 3, 13iblitg 25055 . . . . 5 ((šœ‘ āˆ§ š‘˜ āˆˆ ā„¤) ā†’ (āˆ«2ā€˜(š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))) āˆˆ ā„)
4318, 42sylan2 593 . . . 4 ((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) ā†’ (āˆ«2ā€˜(š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))) āˆˆ ā„)
44 ifan 4537 . . . . . . 7 if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) = if(š‘„ āˆˆ šµ, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0)
4535a1i 11 . . . . . . . 8 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ Ā¬ š‘„ āˆˆ šµ) ā†’ 0 āˆˆ (0[,]+āˆž))
4633, 45ifclda 4519 . . . . . . 7 (((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) ā†’ if(š‘„ āˆˆ šµ, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) āˆˆ (0[,]+āˆž))
4744, 46eqeltrid 2842 . . . . . 6 (((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) ā†’ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) āˆˆ (0[,]+āˆž))
4847fmpttd 7057 . . . . 5 ((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) ā†’ (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)):ā„āŸ¶(0[,]+āˆž))
4928leidd 11654 . . . . . . . . . . 11 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) ā‰¤ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))
50 breq1 5106 . . . . . . . . . . . 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 5106 . . . . . . . . . . . 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 4523 . . . . . . . . . . 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 584 . . . . . . . . . 10 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ if(š‘„ āˆˆ š“, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) ā‰¤ if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))
54 iftrue 4490 . . . . . . . . . . 11 (š‘„ āˆˆ šµ ā†’ if(š‘„ āˆˆ šµ, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) = if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))
5554adantl 482 . . . . . . . . . 10 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ if(š‘„ āˆˆ šµ, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) = if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))
5653, 55breqtrrd 5131 . . . . . . . . 9 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ š‘„ āˆˆ šµ) ā†’ if(š‘„ āˆˆ š“, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) ā‰¤ if(š‘„ āˆˆ šµ, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0))
57 0le0 12187 . . . . . . . . . . 11 0 ā‰¤ 0
5857a1i 11 . . . . . . . . . 10 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ Ā¬ š‘„ āˆˆ šµ) ā†’ 0 ā‰¤ 0)
5912stoic1a 1774 . . . . . . . . . . 11 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ Ā¬ š‘„ āˆˆ šµ) ā†’ Ā¬ š‘„ āˆˆ š“)
6059iffalsed 4495 . . . . . . . . . 10 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ Ā¬ š‘„ āˆˆ šµ) ā†’ if(š‘„ āˆˆ š“, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) = 0)
61 iffalse 4493 . . . . . . . . . . 11 (Ā¬ š‘„ āˆˆ šµ ā†’ if(š‘„ āˆˆ šµ, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) = 0)
6261adantl 482 . . . . . . . . . 10 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ Ā¬ š‘„ āˆˆ šµ) ā†’ if(š‘„ āˆˆ šµ, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) = 0)
6358, 60, 623brtr4d 5135 . . . . . . . . 9 ((((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) āˆ§ Ā¬ š‘„ āˆˆ šµ) ā†’ if(š‘„ āˆˆ š“, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) ā‰¤ if(š‘„ āˆˆ šµ, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0))
6456, 63pm2.61dan 811 . . . . . . . 8 (((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) ā†’ if(š‘„ āˆˆ š“, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0) ā‰¤ if(š‘„ āˆˆ šµ, if(0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0), 0))
6564, 10, 443brtr4g 5137 . . . . . . 7 (((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) āˆ§ š‘„ āˆˆ ā„) ā†’ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) ā‰¤ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))
6665ralrimiva 3141 . . . . . 6 ((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) ā†’ āˆ€š‘„ āˆˆ ā„ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0) ā‰¤ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))
67 reex 11075 . . . . . . . 8 ā„ āˆˆ V
6867a1i 11 . . . . . . 7 ((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) ā†’ ā„ āˆˆ V)
69 eqidd 2738 . . . . . . 7 ((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) ā†’ (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)) = (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)))
70 eqidd 2738 . . . . . . 7 ((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) ā†’ (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)) = (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ šµ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)))
7168, 38, 47, 69, 70ofrfval2 7628 . . . . . 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 256 . . . . 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 1371 . . . 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 1371 . . 3 ((šœ‘ āˆ§ š‘˜ āˆˆ (0...3)) ā†’ (āˆ«2ā€˜(š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))) āˆˆ ā„)
7776ralrimiva 3141 . 2 (šœ‘ ā†’ āˆ€š‘˜ āˆˆ (0...3)(āˆ«2ā€˜(š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))) āˆˆ ā„)
78 eqidd 2738 . . 3 (šœ‘ ā†’ (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)) = (š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0)))
79 eqidd 2738 . . 3 ((šœ‘ āˆ§ š‘„ āˆˆ š“) ā†’ (ā„œā€˜(š¶ / (iā†‘š‘˜))) = (ā„œā€˜(š¶ / (iā†‘š‘˜))))
8011, 14syldan 591 . . 3 ((šœ‘ āˆ§ š‘„ āˆˆ š“) ā†’ š¶ āˆˆ ā„‚)
8178, 79, 80isibl2 25053 . 2 (šœ‘ ā†’ ((š‘„ āˆˆ š“ ā†¦ š¶) āˆˆ šæ1 ā†” ((š‘„ āˆˆ š“ ā†¦ š¶) āˆˆ MblFn āˆ§ āˆ€š‘˜ āˆˆ (0...3)(āˆ«2ā€˜(š‘„ āˆˆ ā„ ā†¦ if((š‘„ āˆˆ š“ āˆ§ 0 ā‰¤ (ā„œā€˜(š¶ / (iā†‘š‘˜)))), (ā„œā€˜(š¶ / (iā†‘š‘˜))), 0))) āˆˆ ā„)))
829, 77, 81mpbir2and 711 1 (šœ‘ ā†’ (š‘„ āˆˆ š“ ā†¦ š¶) āˆˆ šæ1)
Colors of variables: wff setvar class
Syntax hints:  Ā¬ wn 3   ā†’ wi 4   āˆ§ wa 396   = wceq 1541   āˆˆ wcel 2106   ā‰  wne 2941  āˆ€wral 3062  Vcvv 3443   āŠ† wss 3908  ifcif 4484   class class class wbr 5103   ā†¦ cmpt 5186  dom cdm 5630   ā†¾ cres 5632  āŸ¶wf 6487  ā€˜cfv 6491  (class class class)co 7349   āˆ˜r cofr 7606  ā„‚cc 10982  ā„cr 10983  0cc0 10984  ici 10986  +āˆžcpnf 11119  ā„*cxr 11121   ā‰¤ cle 11123   / cdiv 11745  3c3 12142  ā„¤cz 12432  [,]cicc 13195  ...cfz 13352  ā†‘cexp 13895  ā„œcre 14915  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 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7662  ax-inf2 9510  ax-cnex 11040  ax-resscn 11041  ax-1cn 11042  ax-icn 11043  ax-addcl 11044  ax-addrcl 11045  ax-mulcl 11046  ax-mulrcl 11047  ax-mulcom 11048  ax-addass 11049  ax-mulass 11050  ax-distr 11051  ax-i2m1 11052  ax-1ne0 11053  ax-1rid 11054  ax-rnegex 11055  ax-rrecex 11056  ax-cnre 11057  ax-pre-lttri 11058  ax-pre-lttrn 11059  ax-pre-ltadd 11060  ax-pre-mulgt0 11061  ax-pre-sup 11062
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-int 4906  df-iun 4954  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5528  df-eprel 5534  df-po 5542  df-so 5543  df-fr 5585  df-se 5586  df-we 5587  df-xp 5636  df-rel 5637  df-cnv 5638  df-co 5639  df-dm 5640  df-rn 5641  df-res 5642  df-ima 5643  df-pred 6249  df-ord 6316  df-on 6317  df-lim 6318  df-suc 6319  df-iota 6443  df-fun 6493  df-fn 6494  df-f 6495  df-f1 6496  df-fo 6497  df-f1o 6498  df-fv 6499  df-isom 6500  df-riota 7305  df-ov 7352  df-oprab 7353  df-mpo 7354  df-of 7607  df-ofr 7608  df-om 7793  df-1st 7911  df-2nd 7912  df-frecs 8179  df-wrecs 8210  df-recs 8284  df-rdg 8323  df-1o 8379  df-2o 8380  df-er 8581  df-map 8700  df-pm 8701  df-en 8817  df-dom 8818  df-sdom 8819  df-fin 8820  df-sup 9311  df-inf 9312  df-oi 9379  df-dju 9770  df-card 9808  df-pnf 11124  df-mnf 11125  df-xr 11126  df-ltxr 11127  df-le 11128  df-sub 11320  df-neg 11321  df-div 11746  df-nn 12087  df-2 12149  df-3 12150  df-4 12151  df-n0 12347  df-z 12433  df-uz 12696  df-q 12802  df-rp 12844  df-xadd 12962  df-ioo 13196  df-ico 13198  df-icc 13199  df-fz 13353  df-fzo 13496  df-fl 13625  df-mod 13703  df-seq 13835  df-exp 13896  df-hash 14158  df-cj 14917  df-re 14918  df-im 14919  df-sqrt 15053  df-abs 15054  df-clim 15304  df-sum 15505  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  32985  fdvposle  32987  circlemeth  33026  ftc1cnnclem  36044  ftc1anc  36054  ftc2nc  36055  areacirc  36066  lcmineqlem10  40390  lcmineqlem12  40392  lhe4.4ex1a  42373  itgsin0pilem1  43944  iblioosinexp  43947  itgsinexplem1  43948  itgsinexp  43949  itgcoscmulx  43963  itgsincmulx  43968  iblcncfioo  43972  dirkeritg  44096  fourierdlem87  44187  fourierdlem95  44195  fourierdlem103  44203  fourierdlem104  44204  fourierdlem107  44207  fourierdlem111  44211  fourierdlem112  44212  sqwvfoura  44222  sqwvfourb  44223  etransclem18  44246
  Copyright terms: Public domain W3C validator