# Metamath Proof Explorer

## Theorem ibl0

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

Ref Expression
Assertion ibl0 ${⊢}{A}\in \mathrm{dom}vol\to {A}×\left\{0\right\}\in {𝐿}^{1}$

### Proof

Step Hyp Ref Expression
1 0cn ${⊢}0\in ℂ$
2 mbfconst ${⊢}\left({A}\in \mathrm{dom}vol\wedge 0\in ℂ\right)\to {A}×\left\{0\right\}\in MblFn$
3 1 2 mpan2 ${⊢}{A}\in \mathrm{dom}vol\to {A}×\left\{0\right\}\in MblFn$
4 ax-icn ${⊢}\mathrm{i}\in ℂ$
5 ine0 ${⊢}\mathrm{i}\ne 0$
6 elfzelz ${⊢}{k}\in \left(0\dots 3\right)\to {k}\in ℤ$
7 6 ad2antlr ${⊢}\left(\left({A}\in \mathrm{dom}vol\wedge {k}\in \left(0\dots 3\right)\right)\wedge {x}\in {A}\right)\to {k}\in ℤ$
8 expclz ${⊢}\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\wedge {k}\in ℤ\right)\to {\mathrm{i}}^{{k}}\in ℂ$
9 expne0i ${⊢}\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\wedge {k}\in ℤ\right)\to {\mathrm{i}}^{{k}}\ne 0$
10 8 9 div0d ${⊢}\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\wedge {k}\in ℤ\right)\to \frac{0}{{\mathrm{i}}^{{k}}}=0$
11 4 5 7 10 mp3an12i ${⊢}\left(\left({A}\in \mathrm{dom}vol\wedge {k}\in \left(0\dots 3\right)\right)\wedge {x}\in {A}\right)\to \frac{0}{{\mathrm{i}}^{{k}}}=0$
12 11 fveq2d ${⊢}\left(\left({A}\in \mathrm{dom}vol\wedge {k}\in \left(0\dots 3\right)\right)\wedge {x}\in {A}\right)\to \Re \left(\frac{0}{{\mathrm{i}}^{{k}}}\right)=\Re \left(0\right)$
13 re0 ${⊢}\Re \left(0\right)=0$
14 12 13 eqtrdi ${⊢}\left(\left({A}\in \mathrm{dom}vol\wedge {k}\in \left(0\dots 3\right)\right)\wedge {x}\in {A}\right)\to \Re \left(\frac{0}{{\mathrm{i}}^{{k}}}\right)=0$
15 14 itgvallem3 ${⊢}\left({A}\in \mathrm{dom}vol\wedge {k}\in \left(0\dots 3\right)\right)\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(\frac{0}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{0}{{\mathrm{i}}^{{k}}}\right),0\right)\right)\right)=0$
16 0re ${⊢}0\in ℝ$
17 15 16 eqeltrdi ${⊢}\left({A}\in \mathrm{dom}vol\wedge {k}\in \left(0\dots 3\right)\right)\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(\frac{0}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{0}{{\mathrm{i}}^{{k}}}\right),0\right)\right)\right)\in ℝ$
18 17 ralrimiva ${⊢}{A}\in \mathrm{dom}vol\to \forall {k}\in \left(0\dots 3\right)\phantom{\rule{.4em}{0ex}}{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(\frac{0}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{0}{{\mathrm{i}}^{{k}}}\right),0\right)\right)\right)\in ℝ$
19 eqidd ${⊢}{A}\in \mathrm{dom}vol\to \left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(\frac{0}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{0}{{\mathrm{i}}^{{k}}}\right),0\right)\right)=\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(\frac{0}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{0}{{\mathrm{i}}^{{k}}}\right),0\right)\right)$
20 eqidd ${⊢}\left({A}\in \mathrm{dom}vol\wedge {x}\in {A}\right)\to \Re \left(\frac{0}{{\mathrm{i}}^{{k}}}\right)=\Re \left(\frac{0}{{\mathrm{i}}^{{k}}}\right)$
21 c0ex ${⊢}0\in \mathrm{V}$
22 21 fconst ${⊢}\left({A}×\left\{0\right\}\right):{A}⟶\left\{0\right\}$
23 fdm ${⊢}\left({A}×\left\{0\right\}\right):{A}⟶\left\{0\right\}\to \mathrm{dom}\left({A}×\left\{0\right\}\right)={A}$
24 22 23 mp1i ${⊢}{A}\in \mathrm{dom}vol\to \mathrm{dom}\left({A}×\left\{0\right\}\right)={A}$
25 21 fvconst2 ${⊢}{x}\in {A}\to \left({A}×\left\{0\right\}\right)\left({x}\right)=0$
26 25 adantl ${⊢}\left({A}\in \mathrm{dom}vol\wedge {x}\in {A}\right)\to \left({A}×\left\{0\right\}\right)\left({x}\right)=0$
27 19 20 24 26 isibl ${⊢}{A}\in \mathrm{dom}vol\to \left({A}×\left\{0\right\}\in {𝐿}^{1}↔\left({A}×\left\{0\right\}\in MblFn\wedge \forall {k}\in \left(0\dots 3\right)\phantom{\rule{.4em}{0ex}}{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(\frac{0}{{\mathrm{i}}^{{k}}}\right)\right),\Re \left(\frac{0}{{\mathrm{i}}^{{k}}}\right),0\right)\right)\right)\in ℝ\right)\right)$
28 3 18 27 mpbir2and ${⊢}{A}\in \mathrm{dom}vol\to {A}×\left\{0\right\}\in {𝐿}^{1}$