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 eqtrid ⊢ φ ∧ 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 eqtrid ⊢ φ ∧ 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 eqtrid ⊢ φ ∧ 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 eqtrid ⊢ φ ∧ 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