# Metamath Proof Explorer

## Theorem itgposval

Description: The integral 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 ℝ$
itgreval.2 ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}$
itgposval.3 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to 0\le {B}$
Assertion itgposval ${⊢}{\phi }\to {\int }_{{A}}{B}d{x}={\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},{B},0\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 iblrelem.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℝ$
2 itgreval.2 ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}$
3 itgposval.3 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to 0\le {B}$
4 1 2 itgrevallem1 ${⊢}{\phi }\to {\int }_{{A}}{B}d{x}={\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(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)$
5 3 ex ${⊢}{\phi }\to \left({x}\in {A}\to 0\le {B}\right)$
6 5 pm4.71rd ${⊢}{\phi }\to \left({x}\in {A}↔\left(0\le {B}\wedge {x}\in {A}\right)\right)$
7 ancom ${⊢}\left(0\le {B}\wedge {x}\in {A}\right)↔\left({x}\in {A}\wedge 0\le {B}\right)$
8 6 7 syl6rbb ${⊢}{\phi }\to \left(\left({x}\in {A}\wedge 0\le {B}\right)↔{x}\in {A}\right)$
9 8 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)$
10 9 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)$
11 10 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)$
12 1 3 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$
13 11 12 oveq12d ${⊢}{\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(\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)-0$
14 1 3 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)$
15 2 14 mpbid ${⊢}{\phi }\to \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)$
16 15 simprd ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},{B},0\right)\right)\right)\in ℝ$
17 16 recnd ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},{B},0\right)\right)\right)\in ℂ$
18 17 subid1d ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},{B},0\right)\right)\right)-0={\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},{B},0\right)\right)\right)$
19 4 13 18 3eqtrd ${⊢}{\phi }\to {\int }_{{A}}{B}d{x}={\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},{B},0\right)\right)\right)$