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 ⊢φ∧x∈A→B∈ℝ
itgreval.2 ⊢φ→x∈A⟼B∈𝐿1
Assertion itgreval ⊢φ→∫ABdx=∫Aif0≤BB0dx−∫Aif0≤−B−B0dx

Proof

Step Hyp Ref Expression
1 iblrelem.1 ⊢φ∧x∈A→B∈ℝ
2 itgreval.2 ⊢φ→x∈A⟼B∈𝐿1
3 1 2 itgrevallem1 ⊢φ→∫ABdx=∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0−∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0
4 0re ⊢0∈ℝ
5 ifcl ⊢B∈ℝ∧0∈ℝ→if0≤BB0∈ℝ
6 1 4 5 sylancl ⊢φ∧x∈A→if0≤BB0∈ℝ
7 1 iblrelem ⊢φ→x∈A⟼B∈𝐿1↔x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0∈ℝ
8 2 7 mpbid ⊢φ→x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0∈ℝ
9 8 simp1d ⊢φ→x∈A⟼B∈MblFn
10 1 9 mbfpos ⊢φ→x∈A⟼if0≤BB0∈MblFn
11 ifan ⊢ifx∈A∧0≤BB0=ifx∈Aif0≤BB00
12 11 mpteq2i ⊢x∈ℝ⟼ifx∈A∧0≤BB0=x∈ℝ⟼ifx∈Aif0≤BB00
13 12 fveq2i ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0=∫2⁡x∈ℝ⟼ifx∈Aif0≤BB00
14 8 simp2d ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0∈ℝ
15 13 14 eqeltrrid ⊢φ→∫2⁡x∈ℝ⟼ifx∈Aif0≤BB00∈ℝ
16 max1 ⊢0∈ℝ∧B∈ℝ→0≤if0≤BB0
17 4 1 16 sylancr ⊢φ∧x∈A→0≤if0≤BB0
18 6 17 iblpos ⊢φ→x∈A⟼if0≤BB0∈𝐿1↔x∈A⟼if0≤BB0∈MblFn∧∫2⁡x∈ℝ⟼ifx∈Aif0≤BB00∈ℝ
19 10 15 18 mpbir2and ⊢φ→x∈A⟼if0≤BB0∈𝐿1
20 6 19 17 itgposval ⊢φ→∫Aif0≤BB0dx=∫2⁡x∈ℝ⟼ifx∈Aif0≤BB00
21 20 13 eqtr4di ⊢φ→∫Aif0≤BB0dx=∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0
22 1 renegcld ⊢φ∧x∈A→−B∈ℝ
23 ifcl ⊢−B∈ℝ∧0∈ℝ→if0≤−B−B0∈ℝ
24 22 4 23 sylancl ⊢φ∧x∈A→if0≤−B−B0∈ℝ
25 1 9 mbfneg ⊢φ→x∈A⟼−B∈MblFn
26 22 25 mbfpos ⊢φ→x∈A⟼if0≤−B−B0∈MblFn
27 ifan ⊢ifx∈A∧0≤−B−B0=ifx∈Aif0≤−B−B00
28 27 mpteq2i ⊢x∈ℝ⟼ifx∈A∧0≤−B−B0=x∈ℝ⟼ifx∈Aif0≤−B−B00
29 28 fveq2i ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0=∫2⁡x∈ℝ⟼ifx∈Aif0≤−B−B00
30 8 simp3d ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0∈ℝ
31 29 30 eqeltrrid ⊢φ→∫2⁡x∈ℝ⟼ifx∈Aif0≤−B−B00∈ℝ
32 max1 ⊢0∈ℝ∧−B∈ℝ→0≤if0≤−B−B0
33 4 22 32 sylancr ⊢φ∧x∈A→0≤if0≤−B−B0
34 24 33 iblpos ⊢φ→x∈A⟼if0≤−B−B0∈𝐿1↔x∈A⟼if0≤−B−B0∈MblFn∧∫2⁡x∈ℝ⟼ifx∈Aif0≤−B−B00∈ℝ
35 26 31 34 mpbir2and ⊢φ→x∈A⟼if0≤−B−B0∈𝐿1
36 24 35 33 itgposval ⊢φ→∫Aif0≤−B−B0dx=∫2⁡x∈ℝ⟼ifx∈Aif0≤−B−B00
37 36 29 eqtr4di ⊢φ→∫Aif0≤−B−B0dx=∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0
38 21 37 oveq12d ⊢φ→∫Aif0≤BB0dx−∫Aif0≤−B−B0dx=∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0−∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0
39 3 38 eqtr4d ⊢φ→∫ABdx=∫Aif0≤BB0dx−∫Aif0≤−B−B0dx