Metamath Proof Explorer

Theorem itgaddnclem2

Description: Lemma for itgaddnc ; cf. itgaddlem2 . (Contributed by Brendan Leahy, 10-Nov-2017) (Revised by Brendan Leahy, 3-Apr-2018)

Ref Expression
Hypotheses ibladdnc.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
ibladdnc.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
ibladdnc.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
ibladdnc.4 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
ibladdnc.m ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ MblFn )
itgaddnclem.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
itgaddnclem.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
Assertion itgaddnclem2 ( 𝜑 → ∫ 𝐴 ( 𝐵 + 𝐶 ) d 𝑥 = ( ∫ 𝐴 𝐵 d 𝑥 + ∫ 𝐴 𝐶 d 𝑥 ) )

Proof

Step Hyp Ref Expression
1 ibladdnc.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2 ibladdnc.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
3 ibladdnc.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
4 ibladdnc.4 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
5 ibladdnc.m ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ MblFn )
6 itgaddnclem.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
7 itgaddnclem.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
8 max0sub ⊢ ( 𝐵 ∈ ℝ → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) − if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) = 𝐵 )
9 6 8 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) − if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) = 𝐵 )
10 max0sub ⊢ ( 𝐶 ∈ ℝ → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) − if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) = 𝐶 )
11 7 10 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) − if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) = 𝐶 )
12 9 11 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) − if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) + ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) − if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ) = ( 𝐵 + 𝐶 ) )
13 0re ⊢ 0 ∈ ℝ
14 ifcl ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ )
15 6 13 14 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ )
16 15 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℂ )
17 ifcl ⊢ ( ( 𝐶 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℝ )
18 7 13 17 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℝ )
19 18 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℂ )
20 6 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 ∈ ℝ )
21 ifcl ⊢ ( ( - 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ℝ )
22 20 13 21 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ℝ )
23 22 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ℂ )
24 7 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐶 ∈ ℝ )
25 ifcl ⊢ ( ( - 𝐶 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ∈ ℝ )
26 24 13 25 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ∈ ℝ )
27 26 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ∈ ℂ )
28 16 19 23 27 addsub4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) − ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ) = ( ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) − if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) + ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) − if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ) )
29 6 7 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) ∈ ℝ )
30 max0sub ⊢ ( ( 𝐵 + 𝐶 ) ∈ ℝ → ( if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) − if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) ) = ( 𝐵 + 𝐶 ) )
31 29 30 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) − if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) ) = ( 𝐵 + 𝐶 ) )
32 12 28 31 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) − if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) ) = ( ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) − ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ) )
33 29 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( 𝐵 + 𝐶 ) ∈ ℝ )
34 ifcl ⊢ ( ( - ( 𝐵 + 𝐶 ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) ∈ ℝ )
35 33 13 34 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) ∈ ℝ )
36 35 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) ∈ ℂ )
37 15 18 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ∈ ℝ )
38 37 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ∈ ℂ )
39 ifcl ⊢ ( ( ( 𝐵 + 𝐶 ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) ∈ ℝ )
40 29 13 39 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) ∈ ℝ )
41 40 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) ∈ ℂ )
42 22 26 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ∈ ℝ )
43 42 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ∈ ℂ )
44 36 38 41 43 addsubeq4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) + ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) = ( if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) + ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ) ↔ ( if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) − if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) ) = ( ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) − ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ) ) )
45 32 44 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) + ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) = ( if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) + ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ) )
46 45 itgeq2dv ⊢ ( 𝜑 → ∫ 𝐴 ( if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) + ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) d 𝑥 = ∫ 𝐴 ( if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) + ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ) d 𝑥 )
47 6 2 7 4 5 ibladdnc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ 𝐿1 )
48 29 iblre ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) ) ∈ 𝐿1 ) ) )
49 47 48 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) ) ∈ 𝐿1 ) )
50 49 simprd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) ) ∈ 𝐿1 )
51 6 iblre ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ 𝐿1 ) ) )
52 2 51 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ 𝐿1 ) )
53 52 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ 𝐿1 )
54 7 iblre ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ∈ 𝐿1 ) ) )
55 4 54 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ∈ 𝐿1 ) )
56 55 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ∈ 𝐿1 )
57 iblmbf ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
58 2 57 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
59 iblmbf ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
60 4 59 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
61 58 6 60 7 5 mbfposadd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ∈ MblFn )
62 15 53 18 56 61 ibladdnc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ∈ 𝐿1 )
63 max1 ⊢ ( ( 0 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 0 ≤ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
64 13 6 63 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
65 max1 ⊢ ( ( 0 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 0 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
66 13 7 65 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
67 15 18 64 66 addge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
68 67 iftrued ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) = ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
69 68 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) + if ( 0 ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) = ( if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) + ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) )
70 69 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) + if ( 0 ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) + ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ) )
71 29 5 mbfneg ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - ( 𝐵 + 𝐶 ) ) ∈ MblFn )
72 6 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
73 7 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
74 72 73 negdid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( 𝐵 + 𝐶 ) = ( - 𝐵 + - 𝐶 ) )
75 74 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - ( 𝐵 + 𝐶 ) + ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) = ( ( - 𝐵 + - 𝐶 ) + ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) )
76 20 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 ∈ ℂ )
77 24 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐶 ∈ ℂ )
78 76 77 16 19 add4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( - 𝐵 + - 𝐶 ) + ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) = ( ( - 𝐵 + if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) + ( - 𝐶 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) )
79 negeq ⊢ ( 𝐵 = 0 → - 𝐵 = - 0 )
80 neg0 ⊢ - 0 = 0
81 79 80 eqtrdi ⊢ ( 𝐵 = 0 → - 𝐵 = 0 )
82 0le0 ⊢ 0 ≤ 0
83 82 81 breqtrrid ⊢ ( 𝐵 = 0 → 0 ≤ - 𝐵 )
84 83 iftrued ⊢ ( 𝐵 = 0 → if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) = - 𝐵 )
85 id ⊢ ( 𝐵 = 0 → 𝐵 = 0 )
86 82 85 breqtrrid ⊢ ( 𝐵 = 0 → 0 ≤ 𝐵 )
87 86 iftrued ⊢ ( 𝐵 = 0 → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) = 𝐵 )
88 87 85 eqtrd ⊢ ( 𝐵 = 0 → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) = 0 )
89 81 88 oveq12d ⊢ ( 𝐵 = 0 → ( - 𝐵 + if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) = ( 0 + 0 ) )
90 00id ⊢ ( 0 + 0 ) = 0
91 89 90 eqtrdi ⊢ ( 𝐵 = 0 → ( - 𝐵 + if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) = 0 )
92 81 84 91 3eqtr4rd ⊢ ( 𝐵 = 0 → ( - 𝐵 + if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) = if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) )
93 92 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 = 0 ) → ( - 𝐵 + if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) = if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) )
94 ovif2 ⊢ ( - 𝐵 + if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) = if ( 0 ≤ 𝐵 , ( - 𝐵 + 𝐵 ) , ( - 𝐵 + 0 ) )
95 72 negne0bd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ≠ 0 ↔ - 𝐵 ≠ 0 ) )
96 95 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≠ 0 ) → - 𝐵 ≠ 0 )
97 6 le0neg2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 0 ≤ 𝐵 ↔ - 𝐵 ≤ 0 ) )
98 leloe ⊢ ( ( - 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → ( - 𝐵 ≤ 0 ↔ ( - 𝐵 < 0 ∨ - 𝐵 = 0 ) ) )
99 20 13 98 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐵 ≤ 0 ↔ ( - 𝐵 < 0 ∨ - 𝐵 = 0 ) ) )
100 97 99 bitrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 0 ≤ 𝐵 ↔ ( - 𝐵 < 0 ∨ - 𝐵 = 0 ) ) )
101 df-ne ⊢ ( - 𝐵 ≠ 0 ↔ ¬ - 𝐵 = 0 )
102 biorf ⊢ ( ¬ - 𝐵 = 0 → ( - 𝐵 < 0 ↔ ( - 𝐵 = 0 ∨ - 𝐵 < 0 ) ) )
103 101 102 sylbi ⊢ ( - 𝐵 ≠ 0 → ( - 𝐵 < 0 ↔ ( - 𝐵 = 0 ∨ - 𝐵 < 0 ) ) )
104 orcom ⊢ ( ( - 𝐵 = 0 ∨ - 𝐵 < 0 ) ↔ ( - 𝐵 < 0 ∨ - 𝐵 = 0 ) )
105 103 104 bitr2di ⊢ ( - 𝐵 ≠ 0 → ( ( - 𝐵 < 0 ∨ - 𝐵 = 0 ) ↔ - 𝐵 < 0 ) )
106 100 105 sylan9bb ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ - 𝐵 ≠ 0 ) → ( 0 ≤ 𝐵 ↔ - 𝐵 < 0 ) )
107 96 106 syldan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≠ 0 ) → ( 0 ≤ 𝐵 ↔ - 𝐵 < 0 ) )
108 ltnle ⊢ ( ( - 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → ( - 𝐵 < 0 ↔ ¬ 0 ≤ - 𝐵 ) )
109 20 13 108 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐵 < 0 ↔ ¬ 0 ≤ - 𝐵 ) )
110 109 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≠ 0 ) → ( - 𝐵 < 0 ↔ ¬ 0 ≤ - 𝐵 ) )
111 107 110 bitrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≠ 0 ) → ( 0 ≤ 𝐵 ↔ ¬ 0 ≤ - 𝐵 ) )
112 76 72 addcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐵 + 𝐵 ) = ( 𝐵 + - 𝐵 ) )
113 72 negidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + - 𝐵 ) = 0 )
114 112 113 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐵 + 𝐵 ) = 0 )
115 114 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≠ 0 ) → ( - 𝐵 + 𝐵 ) = 0 )
116 76 addid1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐵 + 0 ) = - 𝐵 )
117 116 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≠ 0 ) → ( - 𝐵 + 0 ) = - 𝐵 )
118 111 115 117 ifbieq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≠ 0 ) → if ( 0 ≤ 𝐵 , ( - 𝐵 + 𝐵 ) , ( - 𝐵 + 0 ) ) = if ( ¬ 0 ≤ - 𝐵 , 0 , - 𝐵 ) )
119 ifnot ⊢ if ( ¬ 0 ≤ - 𝐵 , 0 , - 𝐵 ) = if ( 0 ≤ - 𝐵 , - 𝐵 , 0 )
120 118 119 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≠ 0 ) → if ( 0 ≤ 𝐵 , ( - 𝐵 + 𝐵 ) , ( - 𝐵 + 0 ) ) = if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) )
121 94 120 syl5eq ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≠ 0 ) → ( - 𝐵 + if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) = if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) )
122 93 121 pm2.61dane ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐵 + if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) = if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) )
123 negeq ⊢ ( 𝐶 = 0 → - 𝐶 = - 0 )
124 123 80 eqtrdi ⊢ ( 𝐶 = 0 → - 𝐶 = 0 )
125 82 124 breqtrrid ⊢ ( 𝐶 = 0 → 0 ≤ - 𝐶 )
126 125 iftrued ⊢ ( 𝐶 = 0 → if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) = - 𝐶 )
127 id ⊢ ( 𝐶 = 0 → 𝐶 = 0 )
128 82 127 breqtrrid ⊢ ( 𝐶 = 0 → 0 ≤ 𝐶 )
129 128 iftrued ⊢ ( 𝐶 = 0 → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) = 𝐶 )
130 129 127 eqtrd ⊢ ( 𝐶 = 0 → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) = 0 )
131 124 130 oveq12d ⊢ ( 𝐶 = 0 → ( - 𝐶 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) = ( 0 + 0 ) )
132 131 90 eqtrdi ⊢ ( 𝐶 = 0 → ( - 𝐶 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) = 0 )
133 124 126 132 3eqtr4rd ⊢ ( 𝐶 = 0 → ( - 𝐶 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) = if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) )
134 133 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 = 0 ) → ( - 𝐶 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) = if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) )
135 ovif2 ⊢ ( - 𝐶 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) = if ( 0 ≤ 𝐶 , ( - 𝐶 + 𝐶 ) , ( - 𝐶 + 0 ) )
136 73 negne0bd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 ≠ 0 ↔ - 𝐶 ≠ 0 ) )
137 136 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≠ 0 ) → - 𝐶 ≠ 0 )
138 7 le0neg2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 0 ≤ 𝐶 ↔ - 𝐶 ≤ 0 ) )
139 leloe ⊢ ( ( - 𝐶 ∈ ℝ ∧ 0 ∈ ℝ ) → ( - 𝐶 ≤ 0 ↔ ( - 𝐶 < 0 ∨ - 𝐶 = 0 ) ) )
140 24 13 139 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐶 ≤ 0 ↔ ( - 𝐶 < 0 ∨ - 𝐶 = 0 ) ) )
141 138 140 bitrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 0 ≤ 𝐶 ↔ ( - 𝐶 < 0 ∨ - 𝐶 = 0 ) ) )
142 df-ne ⊢ ( - 𝐶 ≠ 0 ↔ ¬ - 𝐶 = 0 )
143 biorf ⊢ ( ¬ - 𝐶 = 0 → ( - 𝐶 < 0 ↔ ( - 𝐶 = 0 ∨ - 𝐶 < 0 ) ) )
144 142 143 sylbi ⊢ ( - 𝐶 ≠ 0 → ( - 𝐶 < 0 ↔ ( - 𝐶 = 0 ∨ - 𝐶 < 0 ) ) )
145 orcom ⊢ ( ( - 𝐶 = 0 ∨ - 𝐶 < 0 ) ↔ ( - 𝐶 < 0 ∨ - 𝐶 = 0 ) )
146 144 145 bitr2di ⊢ ( - 𝐶 ≠ 0 → ( ( - 𝐶 < 0 ∨ - 𝐶 = 0 ) ↔ - 𝐶 < 0 ) )
147 141 146 sylan9bb ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ - 𝐶 ≠ 0 ) → ( 0 ≤ 𝐶 ↔ - 𝐶 < 0 ) )
148 137 147 syldan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≠ 0 ) → ( 0 ≤ 𝐶 ↔ - 𝐶 < 0 ) )
149 ltnle ⊢ ( ( - 𝐶 ∈ ℝ ∧ 0 ∈ ℝ ) → ( - 𝐶 < 0 ↔ ¬ 0 ≤ - 𝐶 ) )
150 24 13 149 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐶 < 0 ↔ ¬ 0 ≤ - 𝐶 ) )
151 150 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≠ 0 ) → ( - 𝐶 < 0 ↔ ¬ 0 ≤ - 𝐶 ) )
152 148 151 bitrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≠ 0 ) → ( 0 ≤ 𝐶 ↔ ¬ 0 ≤ - 𝐶 ) )
153 77 73 addcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐶 + 𝐶 ) = ( 𝐶 + - 𝐶 ) )
154 73 negidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 + - 𝐶 ) = 0 )
155 153 154 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐶 + 𝐶 ) = 0 )
156 155 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≠ 0 ) → ( - 𝐶 + 𝐶 ) = 0 )
157 77 addid1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐶 + 0 ) = - 𝐶 )
158 157 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≠ 0 ) → ( - 𝐶 + 0 ) = - 𝐶 )
159 152 156 158 ifbieq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≠ 0 ) → if ( 0 ≤ 𝐶 , ( - 𝐶 + 𝐶 ) , ( - 𝐶 + 0 ) ) = if ( ¬ 0 ≤ - 𝐶 , 0 , - 𝐶 ) )
160 ifnot ⊢ if ( ¬ 0 ≤ - 𝐶 , 0 , - 𝐶 ) = if ( 0 ≤ - 𝐶 , - 𝐶 , 0 )
161 159 160 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≠ 0 ) → if ( 0 ≤ 𝐶 , ( - 𝐶 + 𝐶 ) , ( - 𝐶 + 0 ) ) = if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) )
162 135 161 syl5eq ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≠ 0 ) → ( - 𝐶 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) = if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) )
163 134 162 pm2.61dane ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐶 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) = if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) )
164 122 163 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( - 𝐵 + if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) + ( - 𝐶 + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) = ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) )
165 75 78 164 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - ( 𝐵 + 𝐶 ) + ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) = ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) )
166 165 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( - ( 𝐵 + 𝐶 ) + ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ) )
167 6 58 mbfneg ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ∈ MblFn )
168 7 60 mbfneg ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - 𝐶 ) ∈ MblFn )
169 74 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - ( 𝐵 + 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( - 𝐵 + - 𝐶 ) ) )
170 169 71 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( - 𝐵 + - 𝐶 ) ) ∈ MblFn )
171 167 20 168 24 170 mbfposadd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ) ∈ MblFn )
172 166 171 eqeltrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( - ( 𝐵 + 𝐶 ) + ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ) ∈ MblFn )
173 71 33 61 37 172 mbfposadd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) + if ( 0 ≤ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) , 0 ) ) ) ∈ MblFn )
174 70 173 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) + ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) ) ∈ MblFn )
175 max1 ⊢ ( ( 0 ∈ ℝ ∧ - ( 𝐵 + 𝐶 ) ∈ ℝ ) → 0 ≤ if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) )
176 13 33 175 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) )
177 35 50 37 62 174 35 37 176 67 itgaddnclem1 ⊢ ( 𝜑 → ∫ 𝐴 ( if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) + ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) d 𝑥 = ( ∫ 𝐴 if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) d 𝑥 + ∫ 𝐴 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) d 𝑥 ) )
178 49 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) ) ∈ 𝐿1 )
179 52 simprd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ 𝐿1 )
180 55 simprd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ∈ 𝐿1 )
181 22 179 26 180 171 ibladdnc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ) ∈ 𝐿1 )
182 max1 ⊢ ( ( 0 ∈ ℝ ∧ - 𝐵 ∈ ℝ ) → 0 ≤ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) )
183 13 20 182 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) )
184 max1 ⊢ ( ( 0 ∈ ℝ ∧ - 𝐶 ∈ ℝ ) → 0 ≤ if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) )
185 13 24 184 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) )
186 22 26 183 185 addge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) )
187 186 iftrued ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) , ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) , 0 ) = ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) )
188 187 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) + if ( 0 ≤ ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) , ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) , 0 ) ) = ( if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) + ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ) )
189 188 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) + if ( 0 ≤ ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) , ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) , 0 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) + ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ) ) )
190 72 73 23 27 add4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐵 + 𝐶 ) + ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ) = ( ( 𝐵 + if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) + ( 𝐶 + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ) )
191 84 81 eqtrd ⊢ ( 𝐵 = 0 → if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) = 0 )
192 85 191 oveq12d ⊢ ( 𝐵 = 0 → ( 𝐵 + if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) = ( 0 + 0 ) )
193 192 90 eqtrdi ⊢ ( 𝐵 = 0 → ( 𝐵 + if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) = 0 )
194 85 87 193 3eqtr4rd ⊢ ( 𝐵 = 0 → ( 𝐵 + if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) = if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
195 194 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 = 0 ) → ( 𝐵 + if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) = if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
196 ovif2 ⊢ ( 𝐵 + if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) = if ( 0 ≤ - 𝐵 , ( 𝐵 + - 𝐵 ) , ( 𝐵 + 0 ) )
197 6 le0neg1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ≤ 0 ↔ 0 ≤ - 𝐵 ) )
198 leloe ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐵 ≤ 0 ↔ ( 𝐵 < 0 ∨ 𝐵 = 0 ) ) )
199 6 13 198 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ≤ 0 ↔ ( 𝐵 < 0 ∨ 𝐵 = 0 ) ) )
200 197 199 bitr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 0 ≤ - 𝐵 ↔ ( 𝐵 < 0 ∨ 𝐵 = 0 ) ) )
201 df-ne ⊢ ( 𝐵 ≠ 0 ↔ ¬ 𝐵 = 0 )
202 biorf ⊢ ( ¬ 𝐵 = 0 → ( 𝐵 < 0 ↔ ( 𝐵 = 0 ∨ 𝐵 < 0 ) ) )
203 201 202 sylbi ⊢ ( 𝐵 ≠ 0 → ( 𝐵 < 0 ↔ ( 𝐵 = 0 ∨ 𝐵 < 0 ) ) )
204 orcom ⊢ ( ( 𝐵 = 0 ∨ 𝐵 < 0 ) ↔ ( 𝐵 < 0 ∨ 𝐵 = 0 ) )
205 203 204 bitr2di ⊢ ( 𝐵 ≠ 0 → ( ( 𝐵 < 0 ∨ 𝐵 = 0 ) ↔ 𝐵 < 0 ) )
206 200 205 sylan9bb ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≠ 0 ) → ( 0 ≤ - 𝐵 ↔ 𝐵 < 0 ) )
207 ltnle ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐵 < 0 ↔ ¬ 0 ≤ 𝐵 ) )
208 6 13 207 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 < 0 ↔ ¬ 0 ≤ 𝐵 ) )
209 208 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≠ 0 ) → ( 𝐵 < 0 ↔ ¬ 0 ≤ 𝐵 ) )
210 206 209 bitrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≠ 0 ) → ( 0 ≤ - 𝐵 ↔ ¬ 0 ≤ 𝐵 ) )
211 113 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≠ 0 ) → ( 𝐵 + - 𝐵 ) = 0 )
212 72 addid1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + 0 ) = 𝐵 )
213 212 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≠ 0 ) → ( 𝐵 + 0 ) = 𝐵 )
214 210 211 213 ifbieq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≠ 0 ) → if ( 0 ≤ - 𝐵 , ( 𝐵 + - 𝐵 ) , ( 𝐵 + 0 ) ) = if ( ¬ 0 ≤ 𝐵 , 0 , 𝐵 ) )
215 ifnot ⊢ if ( ¬ 0 ≤ 𝐵 , 0 , 𝐵 ) = if ( 0 ≤ 𝐵 , 𝐵 , 0 )
216 214 215 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≠ 0 ) → if ( 0 ≤ - 𝐵 , ( 𝐵 + - 𝐵 ) , ( 𝐵 + 0 ) ) = if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
217 196 216 syl5eq ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≠ 0 ) → ( 𝐵 + if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) = if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
218 195 217 pm2.61dane ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) = if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
219 126 124 eqtrd ⊢ ( 𝐶 = 0 → if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) = 0 )
220 127 219 oveq12d ⊢ ( 𝐶 = 0 → ( 𝐶 + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) = ( 0 + 0 ) )
221 220 90 eqtrdi ⊢ ( 𝐶 = 0 → ( 𝐶 + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) = 0 )
222 127 129 221 3eqtr4rd ⊢ ( 𝐶 = 0 → ( 𝐶 + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) = if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
223 222 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 = 0 ) → ( 𝐶 + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) = if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
224 ovif2 ⊢ ( 𝐶 + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) = if ( 0 ≤ - 𝐶 , ( 𝐶 + - 𝐶 ) , ( 𝐶 + 0 ) )
225 7 le0neg1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 ≤ 0 ↔ 0 ≤ - 𝐶 ) )
226 leloe ⊢ ( ( 𝐶 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐶 ≤ 0 ↔ ( 𝐶 < 0 ∨ 𝐶 = 0 ) ) )
227 7 13 226 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 ≤ 0 ↔ ( 𝐶 < 0 ∨ 𝐶 = 0 ) ) )
228 225 227 bitr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 0 ≤ - 𝐶 ↔ ( 𝐶 < 0 ∨ 𝐶 = 0 ) ) )
229 df-ne ⊢ ( 𝐶 ≠ 0 ↔ ¬ 𝐶 = 0 )
230 biorf ⊢ ( ¬ 𝐶 = 0 → ( 𝐶 < 0 ↔ ( 𝐶 = 0 ∨ 𝐶 < 0 ) ) )
231 229 230 sylbi ⊢ ( 𝐶 ≠ 0 → ( 𝐶 < 0 ↔ ( 𝐶 = 0 ∨ 𝐶 < 0 ) ) )
232 orcom ⊢ ( ( 𝐶 = 0 ∨ 𝐶 < 0 ) ↔ ( 𝐶 < 0 ∨ 𝐶 = 0 ) )
233 231 232 bitr2di ⊢ ( 𝐶 ≠ 0 → ( ( 𝐶 < 0 ∨ 𝐶 = 0 ) ↔ 𝐶 < 0 ) )
234 228 233 sylan9bb ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≠ 0 ) → ( 0 ≤ - 𝐶 ↔ 𝐶 < 0 ) )
235 ltnle ⊢ ( ( 𝐶 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐶 < 0 ↔ ¬ 0 ≤ 𝐶 ) )
236 7 13 235 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 < 0 ↔ ¬ 0 ≤ 𝐶 ) )
237 236 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≠ 0 ) → ( 𝐶 < 0 ↔ ¬ 0 ≤ 𝐶 ) )
238 234 237 bitrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≠ 0 ) → ( 0 ≤ - 𝐶 ↔ ¬ 0 ≤ 𝐶 ) )
239 154 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≠ 0 ) → ( 𝐶 + - 𝐶 ) = 0 )
240 73 addid1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 + 0 ) = 𝐶 )
241 240 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≠ 0 ) → ( 𝐶 + 0 ) = 𝐶 )
242 238 239 241 ifbieq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≠ 0 ) → if ( 0 ≤ - 𝐶 , ( 𝐶 + - 𝐶 ) , ( 𝐶 + 0 ) ) = if ( ¬ 0 ≤ 𝐶 , 0 , 𝐶 ) )
243 ifnot ⊢ if ( ¬ 0 ≤ 𝐶 , 0 , 𝐶 ) = if ( 0 ≤ 𝐶 , 𝐶 , 0 )
244 242 243 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≠ 0 ) → if ( 0 ≤ - 𝐶 , ( 𝐶 + - 𝐶 ) , ( 𝐶 + 0 ) ) = if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
245 224 244 syl5eq ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≠ 0 ) → ( 𝐶 + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) = if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
246 223 245 pm2.61dane ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) = if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
247 218 246 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐵 + if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) + ( 𝐶 + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ) = ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
248 190 247 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐵 + 𝐶 ) + ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ) = ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
249 248 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐵 + 𝐶 ) + ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) ) )
250 249 61 eqeltrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐵 + 𝐶 ) + ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ) ) ∈ MblFn )
251 5 29 171 42 250 mbfposadd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) + if ( 0 ≤ ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) , ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) , 0 ) ) ) ∈ MblFn )
252 189 251 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) + ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ) ) ∈ MblFn )
253 max1 ⊢ ( ( 0 ∈ ℝ ∧ ( 𝐵 + 𝐶 ) ∈ ℝ ) → 0 ≤ if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) )
254 13 29 253 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) )
255 40 178 42 181 252 40 42 254 186 itgaddnclem1 ⊢ ( 𝜑 → ∫ 𝐴 ( if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) + ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) ) d 𝑥 = ( ∫ 𝐴 if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) d 𝑥 + ∫ 𝐴 ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) d 𝑥 ) )
256 46 177 255 3eqtr3d ⊢ ( 𝜑 → ( ∫ 𝐴 if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) d 𝑥 + ∫ 𝐴 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) d 𝑥 ) = ( ∫ 𝐴 if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) d 𝑥 + ∫ 𝐴 ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) d 𝑥 ) )
257 35 50 itgcl ⊢ ( 𝜑 → ∫ 𝐴 if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) d 𝑥 ∈ ℂ )
258 15 53 18 56 61 15 18 64 66 itgaddnclem1 ⊢ ( 𝜑 → ∫ 𝐴 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) d 𝑥 = ( ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 + ∫ 𝐴 if ( 0 ≤ 𝐶 , 𝐶 , 0 ) d 𝑥 ) )
259 15 53 itgcl ⊢ ( 𝜑 → ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 ∈ ℂ )
260 18 56 itgcl ⊢ ( 𝜑 → ∫ 𝐴 if ( 0 ≤ 𝐶 , 𝐶 , 0 ) d 𝑥 ∈ ℂ )
261 259 260 addcld ⊢ ( 𝜑 → ( ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 + ∫ 𝐴 if ( 0 ≤ 𝐶 , 𝐶 , 0 ) d 𝑥 ) ∈ ℂ )
262 258 261 eqeltrd ⊢ ( 𝜑 → ∫ 𝐴 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) d 𝑥 ∈ ℂ )
263 40 178 itgcl ⊢ ( 𝜑 → ∫ 𝐴 if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) d 𝑥 ∈ ℂ )
264 22 179 26 180 171 22 26 183 185 itgaddnclem1 ⊢ ( 𝜑 → ∫ 𝐴 ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) d 𝑥 = ( ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 + ∫ 𝐴 if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) d 𝑥 ) )
265 22 179 itgcl ⊢ ( 𝜑 → ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 ∈ ℂ )
266 26 180 itgcl ⊢ ( 𝜑 → ∫ 𝐴 if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) d 𝑥 ∈ ℂ )
267 265 266 addcld ⊢ ( 𝜑 → ( ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 + ∫ 𝐴 if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) d 𝑥 ) ∈ ℂ )
268 264 267 eqeltrd ⊢ ( 𝜑 → ∫ 𝐴 ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) d 𝑥 ∈ ℂ )
269 257 262 263 268 addsubeq4d ⊢ ( 𝜑 → ( ( ∫ 𝐴 if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) d 𝑥 + ∫ 𝐴 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) d 𝑥 ) = ( ∫ 𝐴 if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) d 𝑥 + ∫ 𝐴 ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) d 𝑥 ) ↔ ( ∫ 𝐴 if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) d 𝑥 − ∫ 𝐴 if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) d 𝑥 ) = ( ∫ 𝐴 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) d 𝑥 − ∫ 𝐴 ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) d 𝑥 ) ) )
270 256 269 mpbid ⊢ ( 𝜑 → ( ∫ 𝐴 if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) d 𝑥 − ∫ 𝐴 if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) d 𝑥 ) = ( ∫ 𝐴 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) d 𝑥 − ∫ 𝐴 ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) d 𝑥 ) )
271 258 264 oveq12d ⊢ ( 𝜑 → ( ∫ 𝐴 ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) + if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) d 𝑥 − ∫ 𝐴 ( if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) + if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) d 𝑥 ) = ( ( ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 + ∫ 𝐴 if ( 0 ≤ 𝐶 , 𝐶 , 0 ) d 𝑥 ) − ( ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 + ∫ 𝐴 if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) d 𝑥 ) ) )
272 259 260 265 266 addsub4d ⊢ ( 𝜑 → ( ( ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 + ∫ 𝐴 if ( 0 ≤ 𝐶 , 𝐶 , 0 ) d 𝑥 ) − ( ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 + ∫ 𝐴 if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) d 𝑥 ) ) = ( ( ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 − ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 ) + ( ∫ 𝐴 if ( 0 ≤ 𝐶 , 𝐶 , 0 ) d 𝑥 − ∫ 𝐴 if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) d 𝑥 ) ) )
273 270 271 272 3eqtrd ⊢ ( 𝜑 → ( ∫ 𝐴 if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) d 𝑥 − ∫ 𝐴 if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) d 𝑥 ) = ( ( ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 − ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 ) + ( ∫ 𝐴 if ( 0 ≤ 𝐶 , 𝐶 , 0 ) d 𝑥 − ∫ 𝐴 if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) d 𝑥 ) ) )
274 29 47 itgreval ⊢ ( 𝜑 → ∫ 𝐴 ( 𝐵 + 𝐶 ) d 𝑥 = ( ∫ 𝐴 if ( 0 ≤ ( 𝐵 + 𝐶 ) , ( 𝐵 + 𝐶 ) , 0 ) d 𝑥 − ∫ 𝐴 if ( 0 ≤ - ( 𝐵 + 𝐶 ) , - ( 𝐵 + 𝐶 ) , 0 ) d 𝑥 ) )
275 6 2 itgreval ⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = ( ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 − ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 ) )
276 7 4 itgreval ⊢ ( 𝜑 → ∫ 𝐴 𝐶 d 𝑥 = ( ∫ 𝐴 if ( 0 ≤ 𝐶 , 𝐶 , 0 ) d 𝑥 − ∫ 𝐴 if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) d 𝑥 ) )
277 275 276 oveq12d ⊢ ( 𝜑 → ( ∫ 𝐴 𝐵 d 𝑥 + ∫ 𝐴 𝐶 d 𝑥 ) = ( ( ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 − ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 ) + ( ∫ 𝐴 if ( 0 ≤ 𝐶 , 𝐶 , 0 ) d 𝑥 − ∫ 𝐴 if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) d 𝑥 ) ) )
278 273 274 277 3eqtr4d ⊢ ( 𝜑 → ∫ 𝐴 ( 𝐵 + 𝐶 ) d 𝑥 = ( ∫ 𝐴 𝐵 d 𝑥 + ∫ 𝐴 𝐶 d 𝑥 ) )