itgaddnclem2 - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > itgaddnclem2		Structured version Visualization version GIF version

Theorem itgaddnclem2 38138

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

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

**Assertion**
Ref	Expression
itgaddnclem2	⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥))

Distinct variable groups: 𝑥,𝐴 𝑥,𝑉 𝜑,𝑥 Allowed substitution hints: 𝐵(𝑥) 𝐶(𝑥)

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

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∨ wo 858 = wceq 1559 ∈ wcel 2141 ≠ wne 2956 ifcif 4477 class class class wbr 5097 ↦ cmpt 5178 (class class class)co 7390 ℂcc 11064 ℝcr 11065 0cc0 11066 + caddc 11069 < clt 11209 ≤ cle 11210 − cmin 11407 -cneg 11408 MblFncmbf 25663 𝐿¹cibl 25666 ∫citg 25667

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5224 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7712 ax-inf2 9589 ax-cnex 11122 ax-resscn 11123 ax-1cn 11124 ax-icn 11125 ax-addcl 11126 ax-addrcl 11127 ax-mulcl 11128 ax-mulrcl 11129 ax-mulcom 11130 ax-addass 11131 ax-mulass 11132 ax-distr 11133 ax-i2m1 11134 ax-1ne0 11135 ax-1rid 11136 ax-rnegex 11137 ax-rrecex 11138 ax-cnre 11139 ax-pre-lttri 11140 ax-pre-lttrn 11141 ax-pre-ltadd 11142 ax-pre-mulgt0 11143 ax-pre-sup 11144 ax-addf 11145

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-int 4903 df-iun 4948 df-disj 5065 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-se 5597 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6282 df-ord 6343 df-on 6344 df-lim 6345 df-suc 6346 df-iota 6471 df-fun 6517 df-fn 6518 df-f 6519 df-f1 6520 df-fo 6521 df-f1o 6522 df-fv 6523 df-isom 6524 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-of 7654 df-ofr 7655 df-om 7841 df-1st 7964 df-2nd 7965 df-frecs 8255 df-wrecs 8286 df-recs 8335 df-rdg 8374 df-1o 8430 df-2o 8431 df-er 8671 df-map 8803 df-pm 8804 df-en 8921 df-dom 8922 df-sdom 8923 df-fin 8924 df-fi 9350 df-sup 9381 df-inf 9382 df-oi 9451 df-dju 9852 df-card 9890 df-pnf 11211 df-mnf 11212 df-xr 11213 df-ltxr 11214 df-le 11215 df-sub 11409 df-neg 11410 df-div 11838 df-nn 12204 df-2 12273 df-3 12274 df-4 12275 df-n0 12475 df-z 12562 df-uz 12833 df-q 12943 df-rp 12987 df-xneg 13107 df-xadd 13108 df-xmul 13109 df-ioo 13346 df-ico 13348 df-icc 13349 df-fz 13506 df-fzo 13653 df-fl 13795 df-mod 13873 df-seq 14008 df-exp 14068 df-hash 14337 df-cj 15116 df-re 15117 df-im 15118 df-sqrt 15252 df-abs 15253 df-clim 15505 df-sum 15704 df-rest 17441 df-topgen 17462 df-psmet 21403 df-xmet 21404 df-met 21405 df-bl 21406 df-mopn 21407 df-top 22941 df-topon 22958 df-bases 22993 df-cmp 23434 df-ovol 25513 df-vol 25514 df-mbf 25668 df-itg1 25669 df-itg2 25670 df-ibl 25671 df-itg 25672 df-0p 25719

This theorem is referenced by: itgaddnc 38139

W3C validator