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 φ x A B V
ibladdnc.2 φ x A B 𝐿 1
ibladdnc.3 φ x A C V
ibladdnc.4 φ x A C 𝐿 1
ibladdnc.m φ x A B + C MblFn
itgaddnclem.1 φ x A B
itgaddnclem.2 φ x A C
Assertion itgaddnclem2 φ A B + C dx = A B dx + A C dx

Proof

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