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 ⊢φ→∫AB+Cdx=∫ABdx+∫ACdx

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∈ℝ→if0≤BB0−if0≤−B−B0=B
9 6 8 syl ⊢φ∧x∈A→if0≤BB0−if0≤−B−B0=B
10 max0sub ⊢C∈ℝ→if0≤CC0−if0≤−C−C0=C
11 7 10 syl ⊢φ∧x∈A→if0≤CC0−if0≤−C−C0=C
12 9 11 oveq12d ⊢φ∧x∈A→if0≤BB0−if0≤−B−B0+if0≤CC0-if0≤−C−C0=B+C
13 0re ⊢0∈ℝ
14 ifcl ⊢B∈ℝ∧0∈ℝ→if0≤BB0∈ℝ
15 6 13 14 sylancl ⊢φ∧x∈A→if0≤BB0∈ℝ
16 15 recnd ⊢φ∧x∈A→if0≤BB0∈ℂ
17 ifcl ⊢C∈ℝ∧0∈ℝ→if0≤CC0∈ℝ
18 7 13 17 sylancl ⊢φ∧x∈A→if0≤CC0∈ℝ
19 18 recnd ⊢φ∧x∈A→if0≤CC0∈ℂ
20 6 renegcld ⊢φ∧x∈A→−B∈ℝ
21 ifcl ⊢−B∈ℝ∧0∈ℝ→if0≤−B−B0∈ℝ
22 20 13 21 sylancl ⊢φ∧x∈A→if0≤−B−B0∈ℝ
23 22 recnd ⊢φ∧x∈A→if0≤−B−B0∈ℂ
24 7 renegcld ⊢φ∧x∈A→−C∈ℝ
25 ifcl ⊢−C∈ℝ∧0∈ℝ→if0≤−C−C0∈ℝ
26 24 13 25 sylancl ⊢φ∧x∈A→if0≤−C−C0∈ℝ
27 26 recnd ⊢φ∧x∈A→if0≤−C−C0∈ℂ
28 16 19 23 27 addsub4d ⊢φ∧x∈A→if0≤BB0+if0≤CC0-if0≤−B−B0+if0≤−C−C0=if0≤BB0−if0≤−B−B0+if0≤CC0-if0≤−C−C0
29 6 7 readdcld ⊢φ∧x∈A→B+C∈ℝ
30 max0sub ⊢B+C∈ℝ→if0≤B+CB+C0−if0≤−B+C−B+C0=B+C
31 29 30 syl ⊢φ∧x∈A→if0≤B+CB+C0−if0≤−B+C−B+C0=B+C
32 12 28 31 3eqtr4rd ⊢φ∧x∈A→if0≤B+CB+C0−if0≤−B+C−B+C0=if0≤BB0+if0≤CC0-if0≤−B−B0+if0≤−C−C0
33 29 renegcld ⊢φ∧x∈A→−B+C∈ℝ
34 ifcl ⊢−B+C∈ℝ∧0∈ℝ→if0≤−B+C−B+C0∈ℝ
35 33 13 34 sylancl ⊢φ∧x∈A→if0≤−B+C−B+C0∈ℝ
36 35 recnd ⊢φ∧x∈A→if0≤−B+C−B+C0∈ℂ
37 15 18 readdcld ⊢φ∧x∈A→if0≤BB0+if0≤CC0∈ℝ
38 37 recnd ⊢φ∧x∈A→if0≤BB0+if0≤CC0∈ℂ
39 ifcl ⊢B+C∈ℝ∧0∈ℝ→if0≤B+CB+C0∈ℝ
40 29 13 39 sylancl ⊢φ∧x∈A→if0≤B+CB+C0∈ℝ
41 40 recnd ⊢φ∧x∈A→if0≤B+CB+C0∈ℂ
42 22 26 readdcld ⊢φ∧x∈A→if0≤−B−B0+if0≤−C−C0∈ℝ
43 42 recnd ⊢φ∧x∈A→if0≤−B−B0+if0≤−C−C0∈ℂ
44 36 38 41 43 addsubeq4d ⊢φ∧x∈A→if0≤−B+C−B+C0+if0≤BB0+if0≤CC0=if0≤B+CB+C0+if0≤−B−B0+if0≤−C−C0↔if0≤B+CB+C0−if0≤−B+C−B+C0=if0≤BB0+if0≤CC0-if0≤−B−B0+if0≤−C−C0
45 32 44 mpbird ⊢φ∧x∈A→if0≤−B+C−B+C0+if0≤BB0+if0≤CC0=if0≤B+CB+C0+if0≤−B−B0+if0≤−C−C0
46 45 itgeq2dv ⊢φ→∫Aif0≤−B+C−B+C0+if0≤BB0+if0≤CC0dx=∫Aif0≤B+CB+C0+if0≤−B−B0+if0≤−C−C0dx
47 6 2 7 4 5 ibladdnc ⊢φ→x∈A⟼B+C∈𝐿1
48 29 iblre ⊢φ→x∈A⟼B+C∈𝐿1↔x∈A⟼if0≤B+CB+C0∈𝐿1∧x∈A⟼if0≤−B+C−B+C0∈𝐿1
49 47 48 mpbid ⊢φ→x∈A⟼if0≤B+CB+C0∈𝐿1∧x∈A⟼if0≤−B+C−B+C0∈𝐿1
50 49 simprd ⊢φ→x∈A⟼if0≤−B+C−B+C0∈𝐿1
51 6 iblre ⊢φ→x∈A⟼B∈𝐿1↔x∈A⟼if0≤BB0∈𝐿1∧x∈A⟼if0≤−B−B0∈𝐿1
52 2 51 mpbid ⊢φ→x∈A⟼if0≤BB0∈𝐿1∧x∈A⟼if0≤−B−B0∈𝐿1
53 52 simpld ⊢φ→x∈A⟼if0≤BB0∈𝐿1
54 7 iblre ⊢φ→x∈A⟼C∈𝐿1↔x∈A⟼if0≤CC0∈𝐿1∧x∈A⟼if0≤−C−C0∈𝐿1
55 4 54 mpbid ⊢φ→x∈A⟼if0≤CC0∈𝐿1∧x∈A⟼if0≤−C−C0∈𝐿1
56 55 simpld ⊢φ→x∈A⟼if0≤CC0∈𝐿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⟼if0≤BB0+if0≤CC0∈MblFn
62 15 53 18 56 61 ibladdnc ⊢φ→x∈A⟼if0≤BB0+if0≤CC0∈𝐿1
63 max1 ⊢0∈ℝ∧B∈ℝ→0≤if0≤BB0
64 13 6 63 sylancr ⊢φ∧x∈A→0≤if0≤BB0
65 max1 ⊢0∈ℝ∧C∈ℝ→0≤if0≤CC0
66 13 7 65 sylancr ⊢φ∧x∈A→0≤if0≤CC0
67 15 18 64 66 addge0d ⊢φ∧x∈A→0≤if0≤BB0+if0≤CC0
68 67 iftrued ⊢φ∧x∈A→if0≤if0≤BB0+if0≤CC0if0≤BB0+if0≤CC00=if0≤BB0+if0≤CC0
69 68 oveq2d ⊢φ∧x∈A→if0≤−B+C−B+C0+if0≤if0≤BB0+if0≤CC0if0≤BB0+if0≤CC00=if0≤−B+C−B+C0+if0≤BB0+if0≤CC0
70 69 mpteq2dva ⊢φ→x∈A⟼if0≤−B+C−B+C0+if0≤if0≤BB0+if0≤CC0if0≤BB0+if0≤CC00=x∈A⟼if0≤−B+C−B+C0+if0≤BB0+if0≤CC0
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+if0≤BB0+if0≤CC0=−B+−C+if0≤BB0+if0≤CC0
76 20 recnd ⊢φ∧x∈A→−B∈ℂ
77 24 recnd ⊢φ∧x∈A→−C∈ℂ
78 76 77 16 19 add4d ⊢φ∧x∈A→−B+−C+if0≤BB0+if0≤CC0=−B+if0≤BB0+−C+if0≤CC0
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→if0≤−B−B0=−B
85 id ⊢B=0→B=0
86 82 85 breqtrrid ⊢B=0→0≤B
87 86 iftrued ⊢B=0→if0≤BB0=B
88 87 85 eqtrd ⊢B=0→if0≤BB0=0
89 81 88 oveq12d ⊢B=0→-B+if0≤BB0=0+0
90 00id ⊢0+0=0
91 89 90 eqtrdi ⊢B=0→-B+if0≤BB0=0
92 81 84 91 3eqtr4rd ⊢B=0→-B+if0≤BB0=if0≤−B−B0
93 92 adantl ⊢φ∧x∈A∧B=0→-B+if0≤BB0=if0≤−B−B0
94 ovif2 ⊢-B+if0≤BB0=if0≤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 addridd ⊢φ∧x∈A→-B+0=−B
117 116 adantr ⊢φ∧x∈A∧B≠0→-B+0=−B
118 111 115 117 ifbieq12d ⊢φ∧x∈A∧B≠0→if0≤B-B+B-B+0=if¬0≤−B0−B
119 ifnot ⊢if¬0≤−B0−B=if0≤−B−B0
120 118 119 eqtrdi ⊢φ∧x∈A∧B≠0→if0≤B-B+B-B+0=if0≤−B−B0
121 94 120 eqtrid ⊢φ∧x∈A∧B≠0→-B+if0≤BB0=if0≤−B−B0
122 93 121 pm2.61dane ⊢φ∧x∈A→-B+if0≤BB0=if0≤−B−B0
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→if0≤−C−C0=−C
127 id ⊢C=0→C=0
128 82 127 breqtrrid ⊢C=0→0≤C
129 128 iftrued ⊢C=0→if0≤CC0=C
130 129 127 eqtrd ⊢C=0→if0≤CC0=0
131 124 130 oveq12d ⊢C=0→-C+if0≤CC0=0+0
132 131 90 eqtrdi ⊢C=0→-C+if0≤CC0=0
133 124 126 132 3eqtr4rd ⊢C=0→-C+if0≤CC0=if0≤−C−C0
134 133 adantl ⊢φ∧x∈A∧C=0→-C+if0≤CC0=if0≤−C−C0
135 ovif2 ⊢-C+if0≤CC0=if0≤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 addridd ⊢φ∧x∈A→-C+0=−C
158 157 adantr ⊢φ∧x∈A∧C≠0→-C+0=−C
159 152 156 158 ifbieq12d ⊢φ∧x∈A∧C≠0→if0≤C-C+C-C+0=if¬0≤−C0−C
160 ifnot ⊢if¬0≤−C0−C=if0≤−C−C0
161 159 160 eqtrdi ⊢φ∧x∈A∧C≠0→if0≤C-C+C-C+0=if0≤−C−C0
162 135 161 eqtrid ⊢φ∧x∈A∧C≠0→-C+if0≤CC0=if0≤−C−C0
163 134 162 pm2.61dane ⊢φ∧x∈A→-C+if0≤CC0=if0≤−C−C0
164 122 163 oveq12d ⊢φ∧x∈A→−B+if0≤BB0+−C+if0≤CC0=if0≤−B−B0+if0≤−C−C0
165 75 78 164 3eqtrd ⊢φ∧x∈A→−B+C+if0≤BB0+if0≤CC0=if0≤−B−B0+if0≤−C−C0
166 165 mpteq2dva ⊢φ→x∈A⟼−B+C+if0≤BB0+if0≤CC0=x∈A⟼if0≤−B−B0+if0≤−C−C0
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⟼if0≤−B−B0+if0≤−C−C0∈MblFn
172 166 171 eqeltrd ⊢φ→x∈A⟼−B+C+if0≤BB0+if0≤CC0∈MblFn
173 71 33 61 37 172 mbfposadd ⊢φ→x∈A⟼if0≤−B+C−B+C0+if0≤if0≤BB0+if0≤CC0if0≤BB0+if0≤CC00∈MblFn
174 70 173 eqeltrrd ⊢φ→x∈A⟼if0≤−B+C−B+C0+if0≤BB0+if0≤CC0∈MblFn
175 max1 ⊢0∈ℝ∧−B+C∈ℝ→0≤if0≤−B+C−B+C0
176 13 33 175 sylancr ⊢φ∧x∈A→0≤if0≤−B+C−B+C0
177 35 50 37 62 174 35 37 176 67 itgaddnclem1 ⊢φ→∫Aif0≤−B+C−B+C0+if0≤BB0+if0≤CC0dx=∫Aif0≤−B+C−B+C0dx+∫Aif0≤BB0+if0≤CC0dx
178 49 simpld ⊢φ→x∈A⟼if0≤B+CB+C0∈𝐿1
179 52 simprd ⊢φ→x∈A⟼if0≤−B−B0∈𝐿1
180 55 simprd ⊢φ→x∈A⟼if0≤−C−C0∈𝐿1
181 22 179 26 180 171 ibladdnc ⊢φ→x∈A⟼if0≤−B−B0+if0≤−C−C0∈𝐿1
182 max1 ⊢0∈ℝ∧−B∈ℝ→0≤if0≤−B−B0
183 13 20 182 sylancr ⊢φ∧x∈A→0≤if0≤−B−B0
184 max1 ⊢0∈ℝ∧−C∈ℝ→0≤if0≤−C−C0
185 13 24 184 sylancr ⊢φ∧x∈A→0≤if0≤−C−C0
186 22 26 183 185 addge0d ⊢φ∧x∈A→0≤if0≤−B−B0+if0≤−C−C0
187 186 iftrued ⊢φ∧x∈A→if0≤if0≤−B−B0+if0≤−C−C0if0≤−B−B0+if0≤−C−C00=if0≤−B−B0+if0≤−C−C0
188 187 oveq2d ⊢φ∧x∈A→if0≤B+CB+C0+if0≤if0≤−B−B0+if0≤−C−C0if0≤−B−B0+if0≤−C−C00=if0≤B+CB+C0+if0≤−B−B0+if0≤−C−C0
189 188 mpteq2dva ⊢φ→x∈A⟼if0≤B+CB+C0+if0≤if0≤−B−B0+if0≤−C−C0if0≤−B−B0+if0≤−C−C00=x∈A⟼if0≤B+CB+C0+if0≤−B−B0+if0≤−C−C0
190 72 73 23 27 add4d ⊢φ∧x∈A→B+C+if0≤−B−B0+if0≤−C−C0=B+if0≤−B−B0+C+if0≤−C−C0
191 84 81 eqtrd ⊢B=0→if0≤−B−B0=0
192 85 191 oveq12d ⊢B=0→B+if0≤−B−B0=0+0
193 192 90 eqtrdi ⊢B=0→B+if0≤−B−B0=0
194 85 87 193 3eqtr4rd ⊢B=0→B+if0≤−B−B0=if0≤BB0
195 194 adantl ⊢φ∧x∈A∧B=0→B+if0≤−B−B0=if0≤BB0
196 ovif2 ⊢B+if0≤−B−B0=if0≤−BB+−BB+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 addridd ⊢φ∧x∈A→B+0=B
213 212 adantr ⊢φ∧x∈A∧B≠0→B+0=B
214 210 211 213 ifbieq12d ⊢φ∧x∈A∧B≠0→if0≤−BB+−BB+0=if¬0≤B0B
215 ifnot ⊢if¬0≤B0B=if0≤BB0
216 214 215 eqtrdi ⊢φ∧x∈A∧B≠0→if0≤−BB+−BB+0=if0≤BB0
217 196 216 eqtrid ⊢φ∧x∈A∧B≠0→B+if0≤−B−B0=if0≤BB0
218 195 217 pm2.61dane ⊢φ∧x∈A→B+if0≤−B−B0=if0≤BB0
219 126 124 eqtrd ⊢C=0→if0≤−C−C0=0
220 127 219 oveq12d ⊢C=0→C+if0≤−C−C0=0+0
221 220 90 eqtrdi ⊢C=0→C+if0≤−C−C0=0
222 127 129 221 3eqtr4rd ⊢C=0→C+if0≤−C−C0=if0≤CC0
223 222 adantl ⊢φ∧x∈A∧C=0→C+if0≤−C−C0=if0≤CC0
224 ovif2 ⊢C+if0≤−C−C0=if0≤−CC+−CC+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 addridd ⊢φ∧x∈A→C+0=C
241 240 adantr ⊢φ∧x∈A∧C≠0→C+0=C
242 238 239 241 ifbieq12d ⊢φ∧x∈A∧C≠0→if0≤−CC+−CC+0=if¬0≤C0C
243 ifnot ⊢if¬0≤C0C=if0≤CC0
244 242 243 eqtrdi ⊢φ∧x∈A∧C≠0→if0≤−CC+−CC+0=if0≤CC0
245 224 244 eqtrid ⊢φ∧x∈A∧C≠0→C+if0≤−C−C0=if0≤CC0
246 223 245 pm2.61dane ⊢φ∧x∈A→C+if0≤−C−C0=if0≤CC0
247 218 246 oveq12d ⊢φ∧x∈A→B+if0≤−B−B0+C+if0≤−C−C0=if0≤BB0+if0≤CC0
248 190 247 eqtrd ⊢φ∧x∈A→B+C+if0≤−B−B0+if0≤−C−C0=if0≤BB0+if0≤CC0
249 248 mpteq2dva ⊢φ→x∈A⟼B+C+if0≤−B−B0+if0≤−C−C0=x∈A⟼if0≤BB0+if0≤CC0
250 249 61 eqeltrd ⊢φ→x∈A⟼B+C+if0≤−B−B0+if0≤−C−C0∈MblFn
251 5 29 171 42 250 mbfposadd ⊢φ→x∈A⟼if0≤B+CB+C0+if0≤if0≤−B−B0+if0≤−C−C0if0≤−B−B0+if0≤−C−C00∈MblFn
252 189 251 eqeltrrd ⊢φ→x∈A⟼if0≤B+CB+C0+if0≤−B−B0+if0≤−C−C0∈MblFn
253 max1 ⊢0∈ℝ∧B+C∈ℝ→0≤if0≤B+CB+C0
254 13 29 253 sylancr ⊢φ∧x∈A→0≤if0≤B+CB+C0
255 40 178 42 181 252 40 42 254 186 itgaddnclem1 ⊢φ→∫Aif0≤B+CB+C0+if0≤−B−B0+if0≤−C−C0dx=∫Aif0≤B+CB+C0dx+∫Aif0≤−B−B0+if0≤−C−C0dx
256 46 177 255 3eqtr3d ⊢φ→∫Aif0≤−B+C−B+C0dx+∫Aif0≤BB0+if0≤CC0dx=∫Aif0≤B+CB+C0dx+∫Aif0≤−B−B0+if0≤−C−C0dx
257 35 50 itgcl ⊢φ→∫Aif0≤−B+C−B+C0dx∈ℂ
258 15 53 18 56 61 15 18 64 66 itgaddnclem1 ⊢φ→∫Aif0≤BB0+if0≤CC0dx=∫Aif0≤BB0dx+∫Aif0≤CC0dx
259 15 53 itgcl ⊢φ→∫Aif0≤BB0dx∈ℂ
260 18 56 itgcl ⊢φ→∫Aif0≤CC0dx∈ℂ
261 259 260 addcld ⊢φ→∫Aif0≤BB0dx+∫Aif0≤CC0dx∈ℂ
262 258 261 eqeltrd ⊢φ→∫Aif0≤BB0+if0≤CC0dx∈ℂ
263 40 178 itgcl ⊢φ→∫Aif0≤B+CB+C0dx∈ℂ
264 22 179 26 180 171 22 26 183 185 itgaddnclem1 ⊢φ→∫Aif0≤−B−B0+if0≤−C−C0dx=∫Aif0≤−B−B0dx+∫Aif0≤−C−C0dx
265 22 179 itgcl ⊢φ→∫Aif0≤−B−B0dx∈ℂ
266 26 180 itgcl ⊢φ→∫Aif0≤−C−C0dx∈ℂ
267 265 266 addcld ⊢φ→∫Aif0≤−B−B0dx+∫Aif0≤−C−C0dx∈ℂ
268 264 267 eqeltrd ⊢φ→∫Aif0≤−B−B0+if0≤−C−C0dx∈ℂ
269 257 262 263 268 addsubeq4d ⊢φ→∫Aif0≤−B+C−B+C0dx+∫Aif0≤BB0+if0≤CC0dx=∫Aif0≤B+CB+C0dx+∫Aif0≤−B−B0+if0≤−C−C0dx↔∫Aif0≤B+CB+C0dx−∫Aif0≤−B+C−B+C0dx=∫Aif0≤BB0+if0≤CC0dx−∫Aif0≤−B−B0+if0≤−C−C0dx
270 256 269 mpbid ⊢φ→∫Aif0≤B+CB+C0dx−∫Aif0≤−B+C−B+C0dx=∫Aif0≤BB0+if0≤CC0dx−∫Aif0≤−B−B0+if0≤−C−C0dx
271 258 264 oveq12d ⊢φ→∫Aif0≤BB0+if0≤CC0dx−∫Aif0≤−B−B0+if0≤−C−C0dx=∫Aif0≤BB0dx+∫Aif0≤CC0dx-∫Aif0≤−B−B0dx+∫Aif0≤−C−C0dx
272 259 260 265 266 addsub4d ⊢φ→∫Aif0≤BB0dx+∫Aif0≤CC0dx-∫Aif0≤−B−B0dx+∫Aif0≤−C−C0dx=∫Aif0≤BB0dx−∫Aif0≤−B−B0dx+∫Aif0≤CC0dx-∫Aif0≤−C−C0dx
273 270 271 272 3eqtrd ⊢φ→∫Aif0≤B+CB+C0dx−∫Aif0≤−B+C−B+C0dx=∫Aif0≤BB0dx−∫Aif0≤−B−B0dx+∫Aif0≤CC0dx-∫Aif0≤−C−C0dx
274 29 47 itgreval ⊢φ→∫AB+Cdx=∫Aif0≤B+CB+C0dx−∫Aif0≤−B+C−B+C0dx
275 6 2 itgreval ⊢φ→∫ABdx=∫Aif0≤BB0dx−∫Aif0≤−B−B0dx
276 7 4 itgreval ⊢φ→∫ACdx=∫Aif0≤CC0dx−∫Aif0≤−C−C0dx
277 275 276 oveq12d ⊢φ→∫ABdx+∫ACdx=∫Aif0≤BB0dx−∫Aif0≤−B−B0dx+∫Aif0≤CC0dx-∫Aif0≤−C−C0dx
278 273 274 277 3eqtr4d ⊢φ→∫AB+Cdx=∫ABdx+∫ACdx