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

Theorem ibl0 21928
 Description: The zero function is integrable on any measurable set. (Unlike iblconst 21959, this does not require to have finite measure.) (Contributed by Mario Carneiro, 23-Aug-2014.)
Assertion
Ref Expression
ibl0

Proof of Theorem ibl0
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0cn 9584 . . 3
2 mbfconst 21777 . . 3 MblFn
31, 2mpan2 671 . 2 MblFn
4 elfzelz 11684 . . . . . . . . 9
54ad2antlr 726 . . . . . . . 8
6 ax-icn 9547 . . . . . . . . 9
7 ine0 9988 . . . . . . . . 9
8 expclz 12155 . . . . . . . . . 10
9 expne0i 12162 . . . . . . . . . 10
108, 9div0d 10315 . . . . . . . . 9
116, 7, 10mp3an12 1314 . . . . . . . 8
125, 11syl 16 . . . . . . 7
1312fveq2d 5868 . . . . . 6
14 re0 12944 . . . . . 6
1513, 14syl6eq 2524 . . . . 5
1615itgvallem3 21927 . . . 4
17 0re 9592 . . . 4
1816, 17syl6eqel 2563 . . 3
1918ralrimiva 2878 . 2
20 eqidd 2468 . . 3
21 eqidd 2468 . . 3
22 c0ex 9586 . . . . 5
2322fconst 5769 . . . 4
24 fdm 5733 . . . 4
2523, 24mp1i 12 . . 3
2622fvconst2 6114 . . . 4