# Metamath Proof Explorer

## Theorem itgreval

Description: Decompose the integral of a real function into positive and negative parts. (Contributed by Mario Carneiro, 31-Jul-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}$
Assertion itgreval ${⊢}{\phi }\to {\int }_{{A}}{B}d{x}={\int }_{{A}}if\left(0\le {B},{B},0\right)d{x}-{\int }_{{A}}if\left(0\le -{B},-{B},0\right)d{x}$

### 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 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)$
4 0re ${⊢}0\in ℝ$
5 ifcl ${⊢}\left({B}\in ℝ\wedge 0\in ℝ\right)\to if\left(0\le {B},{B},0\right)\in ℝ$
6 1 4 5 sylancl ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to if\left(0\le {B},{B},0\right)\in ℝ$
7 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)$
8 2 7 mpbid ${⊢}{\phi }\to \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)$
9 8 simp1d ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)\in MblFn$
10 1 9 mbfpos ${⊢}{\phi }\to \left({x}\in {A}⟼if\left(0\le {B},{B},0\right)\right)\in MblFn$
11 ifan ${⊢}if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)=if\left({x}\in {A},if\left(0\le {B},{B},0\right),0\right)$
12 11 mpteq2i ${⊢}\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},if\left(0\le {B},{B},0\right),0\right)\right)$
13 12 fveq2i ${⊢}{\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},if\left(0\le {B},{B},0\right),0\right)\right)\right)$
14 8 simp2d ${⊢}{\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 ℝ$
15 13 14 eqeltrrid ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},if\left(0\le {B},{B},0\right),0\right)\right)\right)\in ℝ$
16 max1 ${⊢}\left(0\in ℝ\wedge {B}\in ℝ\right)\to 0\le if\left(0\le {B},{B},0\right)$
17 4 1 16 sylancr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to 0\le if\left(0\le {B},{B},0\right)$
18 6 17 iblpos ${⊢}{\phi }\to \left(\left({x}\in {A}⟼if\left(0\le {B},{B},0\right)\right)\in {𝐿}^{1}↔\left(\left({x}\in {A}⟼if\left(0\le {B},{B},0\right)\right)\in MblFn\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},if\left(0\le {B},{B},0\right),0\right)\right)\right)\in ℝ\right)\right)$
19 10 15 18 mpbir2and ${⊢}{\phi }\to \left({x}\in {A}⟼if\left(0\le {B},{B},0\right)\right)\in {𝐿}^{1}$
20 6 19 17 itgposval ${⊢}{\phi }\to {\int }_{{A}}if\left(0\le {B},{B},0\right)d{x}={\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},if\left(0\le {B},{B},0\right),0\right)\right)\right)$
21 20 13 syl6eqr ${⊢}{\phi }\to {\int }_{{A}}if\left(0\le {B},{B},0\right)d{x}={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le {B}\right),{B},0\right)\right)\right)$
22 1 renegcld ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to -{B}\in ℝ$
23 ifcl ${⊢}\left(-{B}\in ℝ\wedge 0\in ℝ\right)\to if\left(0\le -{B},-{B},0\right)\in ℝ$
24 22 4 23 sylancl ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to if\left(0\le -{B},-{B},0\right)\in ℝ$
25 1 9 mbfneg ${⊢}{\phi }\to \left({x}\in {A}⟼-{B}\right)\in MblFn$
26 22 25 mbfpos ${⊢}{\phi }\to \left({x}\in {A}⟼if\left(0\le -{B},-{B},0\right)\right)\in MblFn$
27 ifan ${⊢}if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)=if\left({x}\in {A},if\left(0\le -{B},-{B},0\right),0\right)$
28 27 mpteq2i ${⊢}\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},if\left(0\le -{B},-{B},0\right),0\right)\right)$
29 28 fveq2i ${⊢}{\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},if\left(0\le -{B},-{B},0\right),0\right)\right)\right)$
30 8 simp3d ${⊢}{\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 ℝ$
31 29 30 eqeltrrid ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},if\left(0\le -{B},-{B},0\right),0\right)\right)\right)\in ℝ$
32 max1 ${⊢}\left(0\in ℝ\wedge -{B}\in ℝ\right)\to 0\le if\left(0\le -{B},-{B},0\right)$
33 4 22 32 sylancr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to 0\le if\left(0\le -{B},-{B},0\right)$
34 24 33 iblpos ${⊢}{\phi }\to \left(\left({x}\in {A}⟼if\left(0\le -{B},-{B},0\right)\right)\in {𝐿}^{1}↔\left(\left({x}\in {A}⟼if\left(0\le -{B},-{B},0\right)\right)\in MblFn\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},if\left(0\le -{B},-{B},0\right),0\right)\right)\right)\in ℝ\right)\right)$
35 26 31 34 mpbir2and ${⊢}{\phi }\to \left({x}\in {A}⟼if\left(0\le -{B},-{B},0\right)\right)\in {𝐿}^{1}$
36 24 35 33 itgposval ${⊢}{\phi }\to {\int }_{{A}}if\left(0\le -{B},-{B},0\right)d{x}={\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},if\left(0\le -{B},-{B},0\right),0\right)\right)\right)$
37 36 29 syl6eqr ${⊢}{\phi }\to {\int }_{{A}}if\left(0\le -{B},-{B},0\right)d{x}={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -{B}\right),-{B},0\right)\right)\right)$
38 21 37 oveq12d ${⊢}{\phi }\to {\int }_{{A}}if\left(0\le {B},{B},0\right)d{x}-{\int }_{{A}}if\left(0\le -{B},-{B},0\right)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)$
39 3 38 eqtr4d ${⊢}{\phi }\to {\int }_{{A}}{B}d{x}={\int }_{{A}}if\left(0\le {B},{B},0\right)d{x}-{\int }_{{A}}if\left(0\le -{B},-{B},0\right)d{x}$