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 syl6eqr φ 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 syl6eqr φ 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