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 ⊢ φ → ∫ A B dx = ∫ A if 0 ≤ B B 0 dx − ∫ A if 0 ≤ − B − B 0 dx

Proof

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