Metamath Proof Explorer

Theorem itgmulc2nclem2

Description: Lemma for itgmulc2nc ; cf. itgmulc2lem2 . (Contributed by Brendan Leahy, 19-Nov-2017)

Ref Expression
Hypotheses itgmulc2nc.1 ⊢ φ → C ∈ ℂ
itgmulc2nc.2 ⊢ φ ∧ x ∈ A → B ∈ V
itgmulc2nc.3 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
itgmulc2nc.m ⊢ φ → x ∈ A ⟼ C ⁢ B ∈ MblFn
itgmulc2nc.4 ⊢ φ → C ∈ ℝ
itgmulc2nc.5 ⊢ φ ∧ x ∈ A → B ∈ ℝ
Assertion itgmulc2nclem2 ⊢ φ → C ⁢ ∫ A B dx = ∫ A C ⁢ B dx

Proof

Step Hyp Ref Expression
1 itgmulc2nc.1 ⊢ φ → C ∈ ℂ
2 itgmulc2nc.2 ⊢ φ ∧ x ∈ A → B ∈ V
3 itgmulc2nc.3 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
4 itgmulc2nc.m ⊢ φ → x ∈ A ⟼ C ⁢ B ∈ MblFn
5 itgmulc2nc.4 ⊢ φ → C ∈ ℝ
6 itgmulc2nc.5 ⊢ φ ∧ x ∈ A → B ∈ ℝ
7 max0sub ⊢ C ∈ ℝ → if 0 ≤ C C 0 − if 0 ≤ − C − C 0 = C
8 5 7 syl ⊢ φ → if 0 ≤ C C 0 − if 0 ≤ − C − C 0 = C
9 8 oveq1d ⊢ φ → if 0 ≤ C C 0 − if 0 ≤ − C − C 0 ⁢ B = C ⁢ B
10 9 adantr ⊢ φ ∧ x ∈ A → if 0 ≤ C C 0 − if 0 ≤ − C − C 0 ⁢ B = C ⁢ B
11 0re ⊢ 0 ∈ ℝ
12 ifcl ⊢ C ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ C C 0 ∈ ℝ
13 5 11 12 sylancl ⊢ φ → if 0 ≤ C C 0 ∈ ℝ
14 13 recnd ⊢ φ → if 0 ≤ C C 0 ∈ ℂ
15 14 adantr ⊢ φ ∧ x ∈ A → if 0 ≤ C C 0 ∈ ℂ
16 5 renegcld ⊢ φ → − C ∈ ℝ
17 ifcl ⊢ − C ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ − C − C 0 ∈ ℝ
18 16 11 17 sylancl ⊢ φ → if 0 ≤ − C − C 0 ∈ ℝ
19 18 recnd ⊢ φ → if 0 ≤ − C − C 0 ∈ ℂ
20 19 adantr ⊢ φ ∧ x ∈ A → if 0 ≤ − C − C 0 ∈ ℂ
21 6 recnd ⊢ φ ∧ x ∈ A → B ∈ ℂ
22 15 20 21 subdird ⊢ φ ∧ x ∈ A → if 0 ≤ C C 0 − if 0 ≤ − C − C 0 ⁢ B = if 0 ≤ C C 0 ⁢ B − if 0 ≤ − C − C 0 ⁢ B
23 10 22 eqtr3d ⊢ φ ∧ x ∈ A → C ⁢ B = if 0 ≤ C C 0 ⁢ B − if 0 ≤ − C − C 0 ⁢ B
24 23 itgeq2dv ⊢ φ → ∫ A C ⁢ B dx = ∫ A if 0 ≤ C C 0 ⁢ B − if 0 ≤ − C − C 0 ⁢ B dx
25 ovexd ⊢ φ ∧ x ∈ A → if 0 ≤ C C 0 ⁢ B ∈ V
26 ovexd ⊢ φ ∧ x ∈ A → C ⁢ B ∈ V
27 4 26 mbfdm2 ⊢ φ → A ∈ dom ⁡ vol
28 13 adantr ⊢ φ ∧ x ∈ A → if 0 ≤ C C 0 ∈ ℝ
29 fconstmpt ⊢ A × if 0 ≤ C C 0 = x ∈ A ⟼ if 0 ≤ C C 0
30 29 a1i ⊢ φ → A × if 0 ≤ C C 0 = x ∈ A ⟼ if 0 ≤ C C 0
31 eqidd ⊢ φ → x ∈ A ⟼ B = x ∈ A ⟼ B
32 27 28 6 30 31 offval2 ⊢ φ → A × if 0 ≤ C C 0 × f x ∈ A ⟼ B = x ∈ A ⟼ if 0 ≤ C C 0 ⁢ B
33 iblmbf ⊢ x ∈ A ⟼ B ∈ 𝐿 1 → x ∈ A ⟼ B ∈ MblFn
34 3 33 syl ⊢ φ → x ∈ A ⟼ B ∈ MblFn
35 21 fmpttd ⊢ φ → x ∈ A ⟼ B : A ⟶ ℂ
36 34 13 35 mbfmulc2re ⊢ φ → A × if 0 ≤ C C 0 × f x ∈ A ⟼ B ∈ MblFn
37 32 36 eqeltrrd ⊢ φ → x ∈ A ⟼ if 0 ≤ C C 0 ⁢ B ∈ MblFn
38 14 6 3 37 iblmulc2nc ⊢ φ → x ∈ A ⟼ if 0 ≤ C C 0 ⁢ B ∈ 𝐿 1
39 ovexd ⊢ φ ∧ x ∈ A → if 0 ≤ − C − C 0 ⁢ B ∈ V
40 18 adantr ⊢ φ ∧ x ∈ A → if 0 ≤ − C − C 0 ∈ ℝ
41 fconstmpt ⊢ A × if 0 ≤ − C − C 0 = x ∈ A ⟼ if 0 ≤ − C − C 0
42 41 a1i ⊢ φ → A × if 0 ≤ − C − C 0 = x ∈ A ⟼ if 0 ≤ − C − C 0
43 27 40 6 42 31 offval2 ⊢ φ → A × if 0 ≤ − C − C 0 × f x ∈ A ⟼ B = x ∈ A ⟼ if 0 ≤ − C − C 0 ⁢ B
44 34 18 35 mbfmulc2re ⊢ φ → A × if 0 ≤ − C − C 0 × f x ∈ A ⟼ B ∈ MblFn
45 43 44 eqeltrrd ⊢ φ → x ∈ A ⟼ if 0 ≤ − C − C 0 ⁢ B ∈ MblFn
46 19 6 3 45 iblmulc2nc ⊢ φ → x ∈ A ⟼ if 0 ≤ − C − C 0 ⁢ B ∈ 𝐿 1
47 23 mpteq2dva ⊢ φ → x ∈ A ⟼ C ⁢ B = x ∈ A ⟼ if 0 ≤ C C 0 ⁢ B − if 0 ≤ − C − C 0 ⁢ B
48 47 4 eqeltrrd ⊢ φ → x ∈ A ⟼ if 0 ≤ C C 0 ⁢ B − if 0 ≤ − C − C 0 ⁢ B ∈ MblFn
49 25 38 39 46 48 itgsubnc ⊢ φ → ∫ A if 0 ≤ C C 0 ⁢ B − if 0 ≤ − C − C 0 ⁢ B dx = ∫ A if 0 ≤ C C 0 ⁢ B dx − ∫ A if 0 ≤ − C − C 0 ⁢ B dx
50 ovexd ⊢ φ ∧ x ∈ A → if 0 ≤ C C 0 ⁢ if 0 ≤ B B 0 ∈ V
51 ifcl ⊢ B ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ B B 0 ∈ ℝ
52 6 11 51 sylancl ⊢ φ ∧ x ∈ A → if 0 ≤ B B 0 ∈ ℝ
53 6 iblre ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1 ↔ x ∈ A ⟼ if 0 ≤ B B 0 ∈ 𝐿 1 ∧ x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ 𝐿 1
54 3 53 mpbid ⊢ φ → x ∈ A ⟼ if 0 ≤ B B 0 ∈ 𝐿 1 ∧ x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ 𝐿 1
55 54 simpld ⊢ φ → x ∈ A ⟼ if 0 ≤ B B 0 ∈ 𝐿 1
56 eqidd ⊢ φ → x ∈ A ⟼ if 0 ≤ B B 0 = x ∈ A ⟼ if 0 ≤ B B 0
57 27 28 52 30 56 offval2 ⊢ φ → A × if 0 ≤ C C 0 × f x ∈ A ⟼ if 0 ≤ B B 0 = x ∈ A ⟼ if 0 ≤ C C 0 ⁢ if 0 ≤ B B 0
58 6 34 mbfpos ⊢ φ → x ∈ A ⟼ if 0 ≤ B B 0 ∈ MblFn
59 52 recnd ⊢ φ ∧ x ∈ A → if 0 ≤ B B 0 ∈ ℂ
60 59 fmpttd ⊢ φ → x ∈ A ⟼ if 0 ≤ B B 0 : A ⟶ ℂ
61 58 13 60 mbfmulc2re ⊢ φ → A × if 0 ≤ C C 0 × f x ∈ A ⟼ if 0 ≤ B B 0 ∈ MblFn
62 57 61 eqeltrrd ⊢ φ → x ∈ A ⟼ if 0 ≤ C C 0 ⁢ if 0 ≤ B B 0 ∈ MblFn
63 14 52 55 62 iblmulc2nc ⊢ φ → x ∈ A ⟼ if 0 ≤ C C 0 ⁢ if 0 ≤ B B 0 ∈ 𝐿 1
64 ovexd ⊢ φ ∧ x ∈ A → if 0 ≤ C C 0 ⁢ if 0 ≤ − B − B 0 ∈ V
65 6 renegcld ⊢ φ ∧ x ∈ A → − B ∈ ℝ
66 ifcl ⊢ − B ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ − B − B 0 ∈ ℝ
67 65 11 66 sylancl ⊢ φ ∧ x ∈ A → if 0 ≤ − B − B 0 ∈ ℝ
68 54 simprd ⊢ φ → x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ 𝐿 1
69 eqidd ⊢ φ → x ∈ A ⟼ if 0 ≤ − B − B 0 = x ∈ A ⟼ if 0 ≤ − B − B 0
70 27 28 67 30 69 offval2 ⊢ φ → A × if 0 ≤ C C 0 × f x ∈ A ⟼ if 0 ≤ − B − B 0 = x ∈ A ⟼ if 0 ≤ C C 0 ⁢ if 0 ≤ − B − B 0
71 6 34 mbfneg ⊢ φ → x ∈ A ⟼ − B ∈ MblFn
72 65 71 mbfpos ⊢ φ → x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ MblFn
73 67 recnd ⊢ φ ∧ x ∈ A → if 0 ≤ − B − B 0 ∈ ℂ
74 73 fmpttd ⊢ φ → x ∈ A ⟼ if 0 ≤ − B − B 0 : A ⟶ ℂ
75 72 13 74 mbfmulc2re ⊢ φ → A × if 0 ≤ C C 0 × f x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ MblFn
76 70 75 eqeltrrd ⊢ φ → x ∈ A ⟼ if 0 ≤ C C 0 ⁢ if 0 ≤ − B − B 0 ∈ MblFn
77 14 67 68 76 iblmulc2nc ⊢ φ → x ∈ A ⟼ if 0 ≤ C C 0 ⁢ if 0 ≤ − B − B 0 ∈ 𝐿 1
78 max0sub ⊢ B ∈ ℝ → if 0 ≤ B B 0 − if 0 ≤ − B − B 0 = B
79 6 78 syl ⊢ φ ∧ x ∈ A → if 0 ≤ B B 0 − if 0 ≤ − B − B 0 = B
80 79 oveq2d ⊢ φ ∧ x ∈ A → if 0 ≤ C C 0 ⁢ if 0 ≤ B B 0 − if 0 ≤ − B − B 0 = if 0 ≤ C C 0 ⁢ B
81 15 59 73 subdid ⊢ φ ∧ x ∈ A → if 0 ≤ C C 0 ⁢ if 0 ≤ B B 0 − if 0 ≤ − B − B 0 = if 0 ≤ C C 0 ⁢ if 0 ≤ B B 0 − if 0 ≤ C C 0 ⁢ if 0 ≤ − B − B 0
82 80 81 eqtr3d ⊢ φ ∧ x ∈ A → if 0 ≤ C C 0 ⁢ B = if 0 ≤ C C 0 ⁢ if 0 ≤ B B 0 − if 0 ≤ C C 0 ⁢ if 0 ≤ − B − B 0
83 82 mpteq2dva ⊢ φ → x ∈ A ⟼ if 0 ≤ C C 0 ⁢ B = x ∈ A ⟼ if 0 ≤ C C 0 ⁢ if 0 ≤ B B 0 − if 0 ≤ C C 0 ⁢ if 0 ≤ − B − B 0
84 32 83 eqtrd ⊢ φ → A × if 0 ≤ C C 0 × f x ∈ A ⟼ B = x ∈ A ⟼ if 0 ≤ C C 0 ⁢ if 0 ≤ B B 0 − if 0 ≤ C C 0 ⁢ if 0 ≤ − B − B 0
85 84 36 eqeltrrd ⊢ φ → x ∈ A ⟼ if 0 ≤ C C 0 ⁢ if 0 ≤ B B 0 − if 0 ≤ C C 0 ⁢ if 0 ≤ − B − B 0 ∈ MblFn
86 50 63 64 77 85 itgsubnc ⊢ φ → ∫ A if 0 ≤ C C 0 ⁢ if 0 ≤ B B 0 − if 0 ≤ C C 0 ⁢ if 0 ≤ − B − B 0 dx = ∫ A if 0 ≤ C C 0 ⁢ if 0 ≤ B B 0 dx − ∫ A if 0 ≤ C C 0 ⁢ if 0 ≤ − B − B 0 dx
87 82 itgeq2dv ⊢ φ → ∫ A if 0 ≤ C C 0 ⁢ B dx = ∫ A if 0 ≤ C C 0 ⁢ if 0 ≤ B B 0 − if 0 ≤ C C 0 ⁢ if 0 ≤ − B − B 0 dx
88 6 3 itgreval ⊢ φ → ∫ A B dx = ∫ A if 0 ≤ B B 0 dx − ∫ A if 0 ≤ − B − B 0 dx
89 88 oveq2d ⊢ φ → if 0 ≤ C C 0 ⁢ ∫ A B dx = if 0 ≤ C C 0 ⁢ ∫ A if 0 ≤ B B 0 dx − ∫ A if 0 ≤ − B − B 0 dx
90 52 55 itgcl ⊢ φ → ∫ A if 0 ≤ B B 0 dx ∈ ℂ
91 67 68 itgcl ⊢ φ → ∫ A if 0 ≤ − B − B 0 dx ∈ ℂ
92 14 90 91 subdid ⊢ φ → if 0 ≤ C C 0 ⁢ ∫ A if 0 ≤ B B 0 dx − ∫ A if 0 ≤ − B − B 0 dx = if 0 ≤ C C 0 ⁢ ∫ A if 0 ≤ B B 0 dx − if 0 ≤ C C 0 ⁢ ∫ A if 0 ≤ − B − B 0 dx
93 max1 ⊢ 0 ∈ ℝ ∧ C ∈ ℝ → 0 ≤ if 0 ≤ C C 0
94 11 5 93 sylancr ⊢ φ → 0 ≤ if 0 ≤ C C 0
95 max1 ⊢ 0 ∈ ℝ ∧ B ∈ ℝ → 0 ≤ if 0 ≤ B B 0
96 11 6 95 sylancr ⊢ φ ∧ x ∈ A → 0 ≤ if 0 ≤ B B 0
97 14 52 55 62 13 52 94 96 itgmulc2nclem1 ⊢ φ → if 0 ≤ C C 0 ⁢ ∫ A if 0 ≤ B B 0 dx = ∫ A if 0 ≤ C C 0 ⁢ if 0 ≤ B B 0 dx
98 max1 ⊢ 0 ∈ ℝ ∧ − B ∈ ℝ → 0 ≤ if 0 ≤ − B − B 0
99 11 65 98 sylancr ⊢ φ ∧ x ∈ A → 0 ≤ if 0 ≤ − B − B 0
100 14 67 68 76 13 67 94 99 itgmulc2nclem1 ⊢ φ → if 0 ≤ C C 0 ⁢ ∫ A if 0 ≤ − B − B 0 dx = ∫ A if 0 ≤ C C 0 ⁢ if 0 ≤ − B − B 0 dx
101 97 100 oveq12d ⊢ φ → if 0 ≤ C C 0 ⁢ ∫ A if 0 ≤ B B 0 dx − if 0 ≤ C C 0 ⁢ ∫ A if 0 ≤ − B − B 0 dx = ∫ A if 0 ≤ C C 0 ⁢ if 0 ≤ B B 0 dx − ∫ A if 0 ≤ C C 0 ⁢ if 0 ≤ − B − B 0 dx
102 89 92 101 3eqtrd ⊢ φ → if 0 ≤ C C 0 ⁢ ∫ A B dx = ∫ A if 0 ≤ C C 0 ⁢ if 0 ≤ B B 0 dx − ∫ A if 0 ≤ C C 0 ⁢ if 0 ≤ − B − B 0 dx
103 86 87 102 3eqtr4d ⊢ φ → ∫ A if 0 ≤ C C 0 ⁢ B dx = if 0 ≤ C C 0 ⁢ ∫ A B dx
104 ovexd ⊢ φ ∧ x ∈ A → if 0 ≤ − C − C 0 ⁢ if 0 ≤ B B 0 ∈ V
105 27 40 52 42 56 offval2 ⊢ φ → A × if 0 ≤ − C − C 0 × f x ∈ A ⟼ if 0 ≤ B B 0 = x ∈ A ⟼ if 0 ≤ − C − C 0 ⁢ if 0 ≤ B B 0
106 58 18 60 mbfmulc2re ⊢ φ → A × if 0 ≤ − C − C 0 × f x ∈ A ⟼ if 0 ≤ B B 0 ∈ MblFn
107 105 106 eqeltrrd ⊢ φ → x ∈ A ⟼ if 0 ≤ − C − C 0 ⁢ if 0 ≤ B B 0 ∈ MblFn
108 19 52 55 107 iblmulc2nc ⊢ φ → x ∈ A ⟼ if 0 ≤ − C − C 0 ⁢ if 0 ≤ B B 0 ∈ 𝐿 1
109 ovexd ⊢ φ ∧ x ∈ A → if 0 ≤ − C − C 0 ⁢ if 0 ≤ − B − B 0 ∈ V
110 27 40 67 42 69 offval2 ⊢ φ → A × if 0 ≤ − C − C 0 × f x ∈ A ⟼ if 0 ≤ − B − B 0 = x ∈ A ⟼ if 0 ≤ − C − C 0 ⁢ if 0 ≤ − B − B 0
111 72 18 74 mbfmulc2re ⊢ φ → A × if 0 ≤ − C − C 0 × f x ∈ A ⟼ if 0 ≤ − B − B 0 ∈ MblFn
112 110 111 eqeltrrd ⊢ φ → x ∈ A ⟼ if 0 ≤ − C − C 0 ⁢ if 0 ≤ − B − B 0 ∈ MblFn
113 19 67 68 112 iblmulc2nc ⊢ φ → x ∈ A ⟼ if 0 ≤ − C − C 0 ⁢ if 0 ≤ − B − B 0 ∈ 𝐿 1
114 79 oveq2d ⊢ φ ∧ x ∈ A → if 0 ≤ − C − C 0 ⁢ if 0 ≤ B B 0 − if 0 ≤ − B − B 0 = if 0 ≤ − C − C 0 ⁢ B
115 20 59 73 subdid ⊢ φ ∧ x ∈ A → if 0 ≤ − C − C 0 ⁢ if 0 ≤ B B 0 − if 0 ≤ − B − B 0 = if 0 ≤ − C − C 0 ⁢ if 0 ≤ B B 0 − if 0 ≤ − C − C 0 ⁢ if 0 ≤ − B − B 0
116 114 115 eqtr3d ⊢ φ ∧ x ∈ A → if 0 ≤ − C − C 0 ⁢ B = if 0 ≤ − C − C 0 ⁢ if 0 ≤ B B 0 − if 0 ≤ − C − C 0 ⁢ if 0 ≤ − B − B 0
117 116 mpteq2dva ⊢ φ → x ∈ A ⟼ if 0 ≤ − C − C 0 ⁢ B = x ∈ A ⟼ if 0 ≤ − C − C 0 ⁢ if 0 ≤ B B 0 − if 0 ≤ − C − C 0 ⁢ if 0 ≤ − B − B 0
118 43 117 eqtrd ⊢ φ → A × if 0 ≤ − C − C 0 × f x ∈ A ⟼ B = x ∈ A ⟼ if 0 ≤ − C − C 0 ⁢ if 0 ≤ B B 0 − if 0 ≤ − C − C 0 ⁢ if 0 ≤ − B − B 0
119 118 44 eqeltrrd ⊢ φ → x ∈ A ⟼ if 0 ≤ − C − C 0 ⁢ if 0 ≤ B B 0 − if 0 ≤ − C − C 0 ⁢ if 0 ≤ − B − B 0 ∈ MblFn
120 104 108 109 113 119 itgsubnc ⊢ φ → ∫ A if 0 ≤ − C − C 0 ⁢ if 0 ≤ B B 0 − if 0 ≤ − C − C 0 ⁢ if 0 ≤ − B − B 0 dx = ∫ A if 0 ≤ − C − C 0 ⁢ if 0 ≤ B B 0 dx − ∫ A if 0 ≤ − C − C 0 ⁢ if 0 ≤ − B − B 0 dx
121 116 itgeq2dv ⊢ φ → ∫ A if 0 ≤ − C − C 0 ⁢ B dx = ∫ A if 0 ≤ − C − C 0 ⁢ if 0 ≤ B B 0 − if 0 ≤ − C − C 0 ⁢ if 0 ≤ − B − B 0 dx
122 88 oveq2d ⊢ φ → if 0 ≤ − C − C 0 ⁢ ∫ A B dx = if 0 ≤ − C − C 0 ⁢ ∫ A if 0 ≤ B B 0 dx − ∫ A if 0 ≤ − B − B 0 dx
123 19 90 91 subdid ⊢ φ → if 0 ≤ − C − C 0 ⁢ ∫ A if 0 ≤ B B 0 dx − ∫ A if 0 ≤ − B − B 0 dx = if 0 ≤ − C − C 0 ⁢ ∫ A if 0 ≤ B B 0 dx − if 0 ≤ − C − C 0 ⁢ ∫ A if 0 ≤ − B − B 0 dx
124 max1 ⊢ 0 ∈ ℝ ∧ − C ∈ ℝ → 0 ≤ if 0 ≤ − C − C 0
125 11 16 124 sylancr ⊢ φ → 0 ≤ if 0 ≤ − C − C 0
126 19 52 55 107 18 52 125 96 itgmulc2nclem1 ⊢ φ → if 0 ≤ − C − C 0 ⁢ ∫ A if 0 ≤ B B 0 dx = ∫ A if 0 ≤ − C − C 0 ⁢ if 0 ≤ B B 0 dx
127 19 67 68 112 18 67 125 99 itgmulc2nclem1 ⊢ φ → if 0 ≤ − C − C 0 ⁢ ∫ A if 0 ≤ − B − B 0 dx = ∫ A if 0 ≤ − C − C 0 ⁢ if 0 ≤ − B − B 0 dx
128 126 127 oveq12d ⊢ φ → if 0 ≤ − C − C 0 ⁢ ∫ A if 0 ≤ B B 0 dx − if 0 ≤ − C − C 0 ⁢ ∫ A if 0 ≤ − B − B 0 dx = ∫ A if 0 ≤ − C − C 0 ⁢ if 0 ≤ B B 0 dx − ∫ A if 0 ≤ − C − C 0 ⁢ if 0 ≤ − B − B 0 dx
129 122 123 128 3eqtrd ⊢ φ → if 0 ≤ − C − C 0 ⁢ ∫ A B dx = ∫ A if 0 ≤ − C − C 0 ⁢ if 0 ≤ B B 0 dx − ∫ A if 0 ≤ − C − C 0 ⁢ if 0 ≤ − B − B 0 dx
130 120 121 129 3eqtr4d ⊢ φ → ∫ A if 0 ≤ − C − C 0 ⁢ B dx = if 0 ≤ − C − C 0 ⁢ ∫ A B dx
131 103 130 oveq12d ⊢ φ → ∫ A if 0 ≤ C C 0 ⁢ B dx − ∫ A if 0 ≤ − C − C 0 ⁢ B dx = if 0 ≤ C C 0 ⁢ ∫ A B dx − if 0 ≤ − C − C 0 ⁢ ∫ A B dx
132 6 3 itgcl ⊢ φ → ∫ A B dx ∈ ℂ
133 14 19 132 subdird ⊢ φ → if 0 ≤ C C 0 − if 0 ≤ − C − C 0 ⁢ ∫ A B dx = if 0 ≤ C C 0 ⁢ ∫ A B dx − if 0 ≤ − C − C 0 ⁢ ∫ A B dx
134 8 oveq1d ⊢ φ → if 0 ≤ C C 0 − if 0 ≤ − C − C 0 ⁢ ∫ A B dx = C ⁢ ∫ A B dx
135 131 133 134 3eqtr2d ⊢ φ → ∫ A if 0 ≤ C C 0 ⁢ B dx − ∫ A if 0 ≤ − C − C 0 ⁢ B dx = C ⁢ ∫ A B dx
136 24 49 135 3eqtrrd ⊢ φ → C ⁢ ∫ A B dx = ∫ A C ⁢ B dx