# Metamath Proof Explorer

## Theorem iblrelem

Description: Integrability of a real function. (Contributed by Mario Carneiro, 31-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypothesis iblrelem.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℝ$
Assertion iblrelem ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}↔\left(\left({x}\in {A}⟼{B}\right)\in MblFn\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)\in ℝ\right)\right)$

### Proof

Step Hyp Ref Expression
1 iblrelem.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℝ$
2 eqid ${⊢}{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)\right)\right)={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)\right)\right)$
3 eqid ${⊢}{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)\right)\right)={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)\right)\right)$
4 eqid ${⊢}{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)\right)={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)\right)$
5 eqid ${⊢}{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)\right)={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)\right)$
6 2 3 4 5 1 iblcnlem ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}↔\left(\left({x}\in {A}⟼{B}\right)\in MblFn\wedge \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)\right)\right)\in ℝ\right)\wedge \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)\right)\in ℝ\right)\right)\right)$
7 1 reim0d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \Im \left({B}\right)=0$
8 7 itgvallem3 ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)\right)=0$
9 0re ${⊢}0\in ℝ$
10 8 9 eqeltrdi ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)\right)\in ℝ$
11 7 negeqd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to -\Im \left({B}\right)=-0$
12 neg0 ${⊢}-0=0$
13 11 12 syl6eq ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to -\Im \left({B}\right)=0$
14 13 itgvallem3 ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)\right)=0$
15 14 9 eqeltrdi ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)\right)\in ℝ$
16 10 15 jca ${⊢}{\phi }\to \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)\right)\in ℝ\right)$
17 16 biantrud ${⊢}{\phi }\to \left(\left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)\right)\right)\in ℝ\right)↔\left(\left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)\right)\right)\in ℝ\right)\wedge \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)\right)\in ℝ\right)\right)\right)$
18 1 rered ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \Re \left({B}\right)={B}$
19 18 ibllem ${⊢}{\phi }\to if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)=if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)$
20 19 mpteq2dv ${⊢}{\phi }\to \left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)\right)=\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)$
21 20 fveq2d ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)\right)\right)={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)\right)$
22 21 eleq1d ${⊢}{\phi }\to \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)\right)\right)\in ℝ↔{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)\right)\in ℝ\right)$
23 18 negeqd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to -\Re \left({B}\right)=-{B}$
24 23 ibllem ${⊢}{\phi }\to if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)=if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)$
25 24 mpteq2dv ${⊢}{\phi }\to \left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)\right)=\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)$
26 25 fveq2d ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)\right)\right)={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)$
27 26 eleq1d ${⊢}{\phi }\to \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)\right)\right)\in ℝ↔{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)\in ℝ\right)$
28 22 27 anbi12d ${⊢}{\phi }\to \left(\left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)\right)\right)\in ℝ\right)↔\left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)\in ℝ\right)\right)$
29 17 28 bitr3d ${⊢}{\phi }\to \left(\left(\left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)\right)\right)\in ℝ\right)\wedge \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)\right)\in ℝ\right)\right)↔\left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)\in ℝ\right)\right)$
30 29 anbi2d ${⊢}{\phi }\to \left(\left(\left({x}\in {A}⟼{B}\right)\in MblFn\wedge \left(\left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)\right)\right)\in ℝ\right)\wedge \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)\right)\in ℝ\right)\right)\right)↔\left(\left({x}\in {A}⟼{B}\right)\in MblFn\wedge \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)\in ℝ\right)\right)\right)$
31 3anass ${⊢}\left(\left({x}\in {A}⟼{B}\right)\in MblFn\wedge \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)\right)\right)\in ℝ\right)\wedge \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)\right)\in ℝ\right)\right)↔\left(\left({x}\in {A}⟼{B}\right)\in MblFn\wedge \left(\left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)\right)\right)\in ℝ\right)\wedge \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)\right)\in ℝ\right)\right)\right)$
32 3anass ${⊢}\left(\left({x}\in {A}⟼{B}\right)\in MblFn\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)\in ℝ\right)↔\left(\left({x}\in {A}⟼{B}\right)\in MblFn\wedge \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)\in ℝ\right)\right)$
33 30 31 32 3bitr4g ${⊢}{\phi }\to \left(\left(\left({x}\in {A}⟼{B}\right)\in MblFn\wedge \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)\right)\right)\in ℝ\right)\wedge \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)\right)\in ℝ\right)\right)↔\left(\left({x}\in {A}⟼{B}\right)\in MblFn\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)\in ℝ\right)\right)$
34 6 33 bitrd ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}↔\left(\left({x}\in {A}⟼{B}\right)\in MblFn\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)\in ℝ\right)\right)$