# Metamath Proof Explorer

## Theorem iblpos

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

Ref Expression
Hypotheses iblrelem.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℝ$
iblpos.2 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to 0\le {B}$
Assertion iblpos ${⊢}{\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({x}\in {A},{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 iblpos.2 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to 0\le {B}$
3 1 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)$
4 df-3an ${⊢}\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(\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 ℝ\right)\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)$
5 3 4 syl6bb ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}↔\left(\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 ℝ\right)\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)$
6 1 2 iblposlem ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)=0$
7 0re ${⊢}0\in ℝ$
8 6 7 eqeltrdi ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)\in ℝ$
9 8 biantrud ${⊢}{\phi }\to \left(\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 ℝ\right)↔\left(\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 ℝ\right)\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)$
10 2 ex ${⊢}{\phi }\to \left({x}\in {A}\to 0\le {B}\right)$
11 10 pm4.71rd ${⊢}{\phi }\to \left({x}\in {A}↔\left(0\le {B}\wedge {x}\in {A}\right)\right)$
12 ancom ${⊢}\left(0\le {B}\wedge {x}\in {A}\right)↔\left({x}\in {A}\wedge 0\le {B}\right)$
13 11 12 syl6rbb ${⊢}{\phi }\to \left(\left({x}\in {A}\wedge 0\le {B}\right)↔{x}\in {A}\right)$
14 13 ifbid ${⊢}{\phi }\to if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)=if\left({x}\in {A},{B},0\right)$
15 14 mpteq2dv ${⊢}{\phi }\to \left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)=\left({x}\in ℝ⟼if\left({x}\in {A},{B},0\right)\right)$
16 15 fveq2d ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)\right)={\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},{B},0\right)\right)\right)$
17 16 eleq1d ${⊢}{\phi }\to \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)\right)\in ℝ↔{\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},{B},0\right)\right)\right)\in ℝ\right)$
18 17 anbi2d ${⊢}{\phi }\to \left(\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 ℝ\right)↔\left(\left({x}\in {A}⟼{B}\right)\in MblFn\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},{B},0\right)\right)\right)\in ℝ\right)\right)$
19 5 9 18 3bitr2d ${⊢}{\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({x}\in {A},{B},0\right)\right)\right)\in ℝ\right)\right)$