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 38577

Description: Lemma for itgaddnc 38578; cf. itgaddlem2 26137. (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 13319	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ → (if(0 ≤ 𝐵, 𝐵, 0) − if(0 ≤ -𝐵, -𝐵, 0)) = 𝐵)
3	1, 2	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) − if(0 ≤ -𝐵, -𝐵, 0)) = 𝐵)
4		itgaddnclem.2	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)
5		max0sub 13319	. . . . . . . . . 10 ⊢ (𝐶 ∈ ℝ → (if(0 ≤ 𝐶, 𝐶, 0) − if(0 ≤ -𝐶, -𝐶, 0)) = 𝐶)
6	4, 5	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐶, 𝐶, 0) − if(0 ≤ -𝐶, -𝐶, 0)) = 𝐶)
7	3, 6	oveq12d 7436	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((if(0 ≤ 𝐵, 𝐵, 0) − if(0 ≤ -𝐵, -𝐵, 0)) + (if(0 ≤ 𝐶, 𝐶, 0) − if(0 ≤ -𝐶, -𝐶, 0))) = (𝐵 + 𝐶))
8		0re 11303	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
9		ifcl 4528	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
10	1, 8, 9	sylancl 598	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
11	10	recnd 11330	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℂ)
12		ifcl 4528	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ)
13	4, 8, 12	sylancl 598	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ)
14	13	recnd 11330	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℂ)
15	1	renegcld 11736	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℝ)
16		ifcl 4528	. . . . . . . . . . 11 ⊢ ((-𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ)
17	15, 8, 16	sylancl 598	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ)
18	17	recnd 11330	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℂ)
19	4	renegcld 11736	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐶 ∈ ℝ)
20		ifcl 4528	. . . . . . . . . . 11 ⊢ ((-𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ -𝐶, -𝐶, 0) ∈ ℝ)
21	19, 8, 20	sylancl 598	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐶, -𝐶, 0) ∈ ℝ)
22	21	recnd 11330	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐶, -𝐶, 0) ∈ ℂ)
23	11, 14, 18, 22	addsub4d 11709	. . . . . . . 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 11331	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 + 𝐶) ∈ ℝ)
25		max0sub 13319	. . . . . . . . 9 ⊢ ((𝐵 + 𝐶) ∈ ℝ → (if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) − if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0)) = (𝐵 + 𝐶))
26	24, 25	syl 18	. . . . . . . 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 11736	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(𝐵 + 𝐶) ∈ ℝ)
29		ifcl 4528	. . . . . . . . . 10 ⊢ ((-(𝐵 + 𝐶) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0) ∈ ℝ)
30	28, 8, 29	sylancl 598	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0) ∈ ℝ)
31	30	recnd 11330	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0) ∈ ℂ)
32	10, 13	readdcld 11331	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℝ)
33	32	recnd 11330	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℂ)
34		ifcl 4528	. . . . . . . . . 10 ⊢ (((𝐵 + 𝐶) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) ∈ ℝ)
35	24, 8, 34	sylancl 598	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) ∈ ℝ)
36	35	recnd 11330	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) ∈ ℂ)
37	17, 21	readdcld 11331	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)) ∈ ℝ)
38	37	recnd 11330	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)) ∈ ℂ)
39	31, 33, 36, 38	addsubeq4d 11713	. . . . . . 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 260	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0) + (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) + (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0))))
41	40	itgeq2dv 26095	. . . . 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 38575	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ 𝐿¹)
46	24	iblre 26107	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ 𝐿¹ ↔ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0)) ∈ 𝐿¹ ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0)) ∈ 𝐿¹)))
47	45, 46	mpbid 235	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0)) ∈ 𝐿¹ ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0)) ∈ 𝐿¹))
48	47	simprd 501	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0)) ∈ 𝐿¹)
49	1	iblre 26107	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿¹ ↔ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ 𝐿¹ ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ 𝐿¹)))
50	42, 49	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ 𝐿¹ ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ 𝐿¹))
51	50	simpld 500	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ 𝐿¹)
52	4	iblre 26107	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿¹ ↔ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐶, 𝐶, 0)) ∈ 𝐿¹ ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐶, -𝐶, 0)) ∈ 𝐿¹)))
53	43, 52	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐶, 𝐶, 0)) ∈ 𝐿¹ ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐶, -𝐶, 0)) ∈ 𝐿¹))
54	53	simpld 500	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐶, 𝐶, 0)) ∈ 𝐿¹)
55		iblmbf 26081	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿¹ → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
56	42, 55	syl 18	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
57		iblmbf 26081	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿¹ → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)
58	43, 57	syl 18	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)
59	56, 1, 58, 4, 44	mbfposadd 38565	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ∈ MblFn)
60	10, 51, 13, 54, 59	ibladdnc 38575	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ∈ 𝐿¹)
61		max1 13308	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 0 ≤ if(0 ≤ 𝐵, 𝐵, 0))
62	8, 1, 61	sylancr 599	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝐵, 𝐵, 0))
63		max1 13308	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 0 ≤ if(0 ≤ 𝐶, 𝐶, 0))
64	8, 4, 63	sylancr 599	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝐶, 𝐶, 0))
65	10, 13, 62, 64	addge0d 11885	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
66	65	iftrued 4490	. . . . . . . . 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 7434	. . . . . . . 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 5198	. . . . . . 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 25964	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -(𝐵 + 𝐶)) ∈ MblFn)
70	1	recnd 11330	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)
71	4	recnd 11330	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)
72	70, 71	negdid 11675	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(𝐵 + 𝐶) = (-𝐵 + -𝐶))
73	72	oveq1d 7433	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-(𝐵 + 𝐶) + (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = ((-𝐵 + -𝐶) + (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
74	15	recnd 11330	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℂ)
75	19	recnd 11330	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐶 ∈ ℂ)
76	74, 75, 11, 14	add4d 11532	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((-𝐵 + -𝐶) + (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = ((-𝐵 + if(0 ≤ 𝐵, 𝐵, 0)) + (-𝐶 + if(0 ≤ 𝐶, 𝐶, 0))))
77		negeq 11542	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 = 0 → -𝐵 = -0)
78		neg0 11597	. . . . . . . . . . . . . . . 16 ⊢ -0 = 0
79	77, 78	eqtrdi 2812	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = 0 → -𝐵 = 0)
80		0le0 12437	. . . . . . . . . . . . . . . . 17 ⊢ 0 ≤ 0
81	80, 79	breqtrrid 5143	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 = 0 → 0 ≤ -𝐵)
82	81	iftrued 4490	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = 0 → if(0 ≤ -𝐵, -𝐵, 0) = -𝐵)
83		id 23	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 = 0 → 𝐵 = 0)
84	80, 83	breqtrrid 5143	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 = 0 → 0 ≤ 𝐵)
85	84	iftrued 4490	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 = 0 → if(0 ≤ 𝐵, 𝐵, 0) = 𝐵)
86	85, 83	eqtrd 2796	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 = 0 → if(0 ≤ 𝐵, 𝐵, 0) = 0)
87	79, 86	oveq12d 7436	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 = 0 → (-𝐵 + if(0 ≤ 𝐵, 𝐵, 0)) = (0 + 0))
88		00id 11478	. . . . . . . . . . . . . . . 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 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 = 0) → (-𝐵 + if(0 ≤ 𝐵, 𝐵, 0)) = if(0 ≤ -𝐵, -𝐵, 0))
92		ovif2 7517	. . . . . . . . . . . . . 14 ⊢ (-𝐵 + if(0 ≤ 𝐵, 𝐵, 0)) = if(0 ≤ 𝐵, (-𝐵 + 𝐵), (-𝐵 + 0))
93	70	negne0bd 11655	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ≠ 0 ↔ -𝐵 ≠ 0))
94	93	biimpa 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → -𝐵 ≠ 0)
95	1	le0neg2d 11881	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐵 ↔ -𝐵 ≤ 0))
96		leloe 11389	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((-𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → (-𝐵 ≤ 0 ↔ (-𝐵 < 0 ∨ -𝐵 = 0)))
97	15, 8, 96	sylancl 598	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 ≤ 0 ↔ (-𝐵 < 0 ∨ -𝐵 = 0)))
98	95, 97	bitrd 282	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐵 ↔ (-𝐵 < 0 ∨ -𝐵 = 0)))
99		df-ne 2957	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (-𝐵 ≠ 0 ↔ ¬ -𝐵 = 0)
100		biorf 950	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ -𝐵 = 0 → (-𝐵 < 0 ↔ (-𝐵 = 0 ∨ -𝐵 < 0)))
101	99, 100	sylbi 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (-𝐵 ≠ 0 → (-𝐵 < 0 ↔ (-𝐵 = 0 ∨ -𝐵 < 0)))
102		orcom 884	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((-𝐵 = 0 ∨ -𝐵 < 0) ↔ (-𝐵 < 0 ∨ -𝐵 = 0))
103	101, 102	bitr2di 291	. . . . . . . . . . . . . . . . . . 19 ⊢ (-𝐵 ≠ 0 → ((-𝐵 < 0 ∨ -𝐵 = 0) ↔ -𝐵 < 0))
104	98, 103	sylan9bb 519	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ -𝐵 ≠ 0) → (0 ≤ 𝐵 ↔ -𝐵 < 0))
105	94, 104	syldan 603	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (0 ≤ 𝐵 ↔ -𝐵 < 0))
106		ltnle 11382	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → (-𝐵 < 0 ↔ ¬ 0 ≤ -𝐵))
107	15, 8, 106	sylancl 598	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 < 0 ↔ ¬ 0 ≤ -𝐵))
108	107	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (-𝐵 < 0 ↔ ¬ 0 ≤ -𝐵))
109	105, 108	bitrd 282	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (0 ≤ 𝐵 ↔ ¬ 0 ≤ -𝐵))
110	74, 70	addcomd 11505	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 + 𝐵) = (𝐵 + -𝐵))
111	70	negidd 11652	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 + -𝐵) = 0)
112	110, 111	eqtrd 2796	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 + 𝐵) = 0)
113	112	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (-𝐵 + 𝐵) = 0)
114	74	addridd 11503	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 + 0) = -𝐵)
115	114	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (-𝐵 + 0) = -𝐵)
116	109, 113, 115	ifbieq12d 4511	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → if(0 ≤ 𝐵, (-𝐵 + 𝐵), (-𝐵 + 0)) = if(¬ 0 ≤ -𝐵, 0, -𝐵))
117		ifnot 4535	. . . . . . . . . . . . . . 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 11542	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 = 0 → -𝐶 = -0)
122	121, 78	eqtrdi 2812	. . . . . . . . . . . . . . 15 ⊢ (𝐶 = 0 → -𝐶 = 0)
123	80, 122	breqtrrid 5143	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 = 0 → 0 ≤ -𝐶)
124	123	iftrued 4490	. . . . . . . . . . . . . . 15 ⊢ (𝐶 = 0 → if(0 ≤ -𝐶, -𝐶, 0) = -𝐶)
125		id 23	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐶 = 0 → 𝐶 = 0)
126	80, 125	breqtrrid 5143	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 = 0 → 0 ≤ 𝐶)
127	126	iftrued 4490	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐶 = 0 → if(0 ≤ 𝐶, 𝐶, 0) = 𝐶)
128	127, 125	eqtrd 2796	. . . . . . . . . . . . . . . . 17 ⊢ (𝐶 = 0 → if(0 ≤ 𝐶, 𝐶, 0) = 0)
129	122, 128	oveq12d 7436	. . . . . . . . . . . . . . . 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 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 = 0) → (-𝐶 + if(0 ≤ 𝐶, 𝐶, 0)) = if(0 ≤ -𝐶, -𝐶, 0))
133		ovif2 7517	. . . . . . . . . . . . . 14 ⊢ (-𝐶 + if(0 ≤ 𝐶, 𝐶, 0)) = if(0 ≤ 𝐶, (-𝐶 + 𝐶), (-𝐶 + 0))
134	71	negne0bd 11655	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 ≠ 0 ↔ -𝐶 ≠ 0))
135	134	biimpa 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → -𝐶 ≠ 0)
136	4	le0neg2d 11881	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐶 ↔ -𝐶 ≤ 0))
137		leloe 11389	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((-𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → (-𝐶 ≤ 0 ↔ (-𝐶 < 0 ∨ -𝐶 = 0)))
138	19, 8, 137	sylancl 598	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐶 ≤ 0 ↔ (-𝐶 < 0 ∨ -𝐶 = 0)))
139	136, 138	bitrd 282	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐶 ↔ (-𝐶 < 0 ∨ -𝐶 = 0)))
140		df-ne 2957	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (-𝐶 ≠ 0 ↔ ¬ -𝐶 = 0)
141		biorf 950	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ -𝐶 = 0 → (-𝐶 < 0 ↔ (-𝐶 = 0 ∨ -𝐶 < 0)))
142	140, 141	sylbi 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (-𝐶 ≠ 0 → (-𝐶 < 0 ↔ (-𝐶 = 0 ∨ -𝐶 < 0)))
143		orcom 884	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((-𝐶 = 0 ∨ -𝐶 < 0) ↔ (-𝐶 < 0 ∨ -𝐶 = 0))
144	142, 143	bitr2di 291	. . . . . . . . . . . . . . . . . . 19 ⊢ (-𝐶 ≠ 0 → ((-𝐶 < 0 ∨ -𝐶 = 0) ↔ -𝐶 < 0))
145	139, 144	sylan9bb 519	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ -𝐶 ≠ 0) → (0 ≤ 𝐶 ↔ -𝐶 < 0))
146	135, 145	syldan 603	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (0 ≤ 𝐶 ↔ -𝐶 < 0))
147		ltnle 11382	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → (-𝐶 < 0 ↔ ¬ 0 ≤ -𝐶))
148	19, 8, 147	sylancl 598	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐶 < 0 ↔ ¬ 0 ≤ -𝐶))
149	148	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (-𝐶 < 0 ↔ ¬ 0 ≤ -𝐶))
150	146, 149	bitrd 282	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (0 ≤ 𝐶 ↔ ¬ 0 ≤ -𝐶))
151	75, 71	addcomd 11505	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐶 + 𝐶) = (𝐶 + -𝐶))
152	71	negidd 11652	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 + -𝐶) = 0)
153	151, 152	eqtrd 2796	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐶 + 𝐶) = 0)
154	153	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (-𝐶 + 𝐶) = 0)
155	75	addridd 11503	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐶 + 0) = -𝐶)
156	155	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (-𝐶 + 0) = -𝐶)
157	150, 154, 156	ifbieq12d 4511	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → if(0 ≤ 𝐶, (-𝐶 + 𝐶), (-𝐶 + 0)) = if(¬ 0 ≤ -𝐶, 0, -𝐶))
158		ifnot 4535	. . . . . . . . . . . . . . 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 7436	. . . . . . . . . . 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 5198	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (-(𝐵 + 𝐶) + (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))) = (𝑥 ∈ 𝐴 ↦ (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0))))
165	1, 56	mbfneg 25964	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐵) ∈ MblFn)
166	4, 58	mbfneg 25964	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐶) ∈ MblFn)
167	72	mpteq2dva 5198	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -(𝐵 + 𝐶)) = (𝑥 ∈ 𝐴 ↦ (-𝐵 + -𝐶)))
168	167, 69	eqeltrrd 2862	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (-𝐵 + -𝐶)) ∈ MblFn)
169	165, 15, 166, 19, 168	mbfposadd 38565	. . . . . . . . 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 38565	. . . . . . 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 13308	. . . . . . 7 ⊢ ((0 ∈ ℝ ∧ -(𝐵 + 𝐶) ∈ ℝ) → 0 ≤ if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0))
174	8, 28, 173	sylancr 599	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0))
175	30, 48, 32, 60, 172, 30, 32, 174, 65	itgaddnclem1 38576	. . . . 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 500	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0)) ∈ 𝐿¹)
177	50	simprd 501	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ 𝐿¹)
178	53	simprd 501	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐶, -𝐶, 0)) ∈ 𝐿¹)
179	17, 177, 21, 178, 169	ibladdnc 38575	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0))) ∈ 𝐿¹)
180		max1 13308	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ -𝐵 ∈ ℝ) → 0 ≤ if(0 ≤ -𝐵, -𝐵, 0))
181	8, 15, 180	sylancr 599	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ -𝐵, -𝐵, 0))
182		max1 13308	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ -𝐶 ∈ ℝ) → 0 ≤ if(0 ≤ -𝐶, -𝐶, 0))
183	8, 19, 182	sylancr 599	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ -𝐶, -𝐶, 0))
184	17, 21, 181, 183	addge0d 11885	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)))
185	184	iftrued 4490	. . . . . . . . 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 7434	. . . . . . . 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 5198	. . . . . . 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 11532	. . . . . . . . . . 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 7436	. . . . . . . . . . . . . . . 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 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 = 0) → (𝐵 + if(0 ≤ -𝐵, -𝐵, 0)) = if(0 ≤ 𝐵, 𝐵, 0))
194		ovif2 7517	. . . . . . . . . . . . . 14 ⊢ (𝐵 + if(0 ≤ -𝐵, -𝐵, 0)) = if(0 ≤ -𝐵, (𝐵 + -𝐵), (𝐵 + 0))
195	1	le0neg1d 11880	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ≤ 0 ↔ 0 ≤ -𝐵))
196		leloe 11389	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐵 ≤ 0 ↔ (𝐵 < 0 ∨ 𝐵 = 0)))
197	1, 8, 196	sylancl 598	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ≤ 0 ↔ (𝐵 < 0 ∨ 𝐵 = 0)))
198	195, 197	bitr3d 284	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ -𝐵 ↔ (𝐵 < 0 ∨ 𝐵 = 0)))
199		df-ne 2957	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 ≠ 0 ↔ ¬ 𝐵 = 0)
200		biorf 950	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝐵 = 0 → (𝐵 < 0 ↔ (𝐵 = 0 ∨ 𝐵 < 0)))
201	199, 200	sylbi 220	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ≠ 0 → (𝐵 < 0 ↔ (𝐵 = 0 ∨ 𝐵 < 0)))
202		orcom 884	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 = 0 ∨ 𝐵 < 0) ↔ (𝐵 < 0 ∨ 𝐵 = 0))
203	201, 202	bitr2di 291	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ≠ 0 → ((𝐵 < 0 ∨ 𝐵 = 0) ↔ 𝐵 < 0))
204	198, 203	sylan9bb 519	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (0 ≤ -𝐵 ↔ 𝐵 < 0))
205		ltnle 11382	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐵 < 0 ↔ ¬ 0 ≤ 𝐵))
206	1, 8, 205	sylancl 598	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 < 0 ↔ ¬ 0 ≤ 𝐵))
207	206	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (𝐵 < 0 ↔ ¬ 0 ≤ 𝐵))
208	204, 207	bitrd 282	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (0 ≤ -𝐵 ↔ ¬ 0 ≤ 𝐵))
209	111	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (𝐵 + -𝐵) = 0)
210	70	addridd 11503	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 + 0) = 𝐵)
211	210	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (𝐵 + 0) = 𝐵)
212	208, 209, 211	ifbieq12d 4511	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → if(0 ≤ -𝐵, (𝐵 + -𝐵), (𝐵 + 0)) = if(¬ 0 ≤ 𝐵, 0, 𝐵))
213		ifnot 4535	. . . . . . . . . . . . . . 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 7436	. . . . . . . . . . . . . . . 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 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 = 0) → (𝐶 + if(0 ≤ -𝐶, -𝐶, 0)) = if(0 ≤ 𝐶, 𝐶, 0))
222		ovif2 7517	. . . . . . . . . . . . . 14 ⊢ (𝐶 + if(0 ≤ -𝐶, -𝐶, 0)) = if(0 ≤ -𝐶, (𝐶 + -𝐶), (𝐶 + 0))
223	4	le0neg1d 11880	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 ≤ 0 ↔ 0 ≤ -𝐶))
224		leloe 11389	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐶 ≤ 0 ↔ (𝐶 < 0 ∨ 𝐶 = 0)))
225	4, 8, 224	sylancl 598	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 ≤ 0 ↔ (𝐶 < 0 ∨ 𝐶 = 0)))
226	223, 225	bitr3d 284	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ -𝐶 ↔ (𝐶 < 0 ∨ 𝐶 = 0)))
227		df-ne 2957	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐶 ≠ 0 ↔ ¬ 𝐶 = 0)
228		biorf 950	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝐶 = 0 → (𝐶 < 0 ↔ (𝐶 = 0 ∨ 𝐶 < 0)))
229	227, 228	sylbi 220	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 ≠ 0 → (𝐶 < 0 ↔ (𝐶 = 0 ∨ 𝐶 < 0)))
230		orcom 884	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 = 0 ∨ 𝐶 < 0) ↔ (𝐶 < 0 ∨ 𝐶 = 0))
231	229, 230	bitr2di 291	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐶 ≠ 0 → ((𝐶 < 0 ∨ 𝐶 = 0) ↔ 𝐶 < 0))
232	226, 231	sylan9bb 519	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (0 ≤ -𝐶 ↔ 𝐶 < 0))
233		ltnle 11382	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐶 < 0 ↔ ¬ 0 ≤ 𝐶))
234	4, 8, 233	sylancl 598	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 < 0 ↔ ¬ 0 ≤ 𝐶))
235	234	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (𝐶 < 0 ↔ ¬ 0 ≤ 𝐶))
236	232, 235	bitrd 282	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (0 ≤ -𝐶 ↔ ¬ 0 ≤ 𝐶))
237	152	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (𝐶 + -𝐶) = 0)
238	71	addridd 11503	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 + 0) = 𝐶)
239	238	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (𝐶 + 0) = 𝐶)
240	236, 237, 239	ifbieq12d 4511	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → if(0 ≤ -𝐶, (𝐶 + -𝐶), (𝐶 + 0)) = if(¬ 0 ≤ 𝐶, 0, 𝐶))
241		ifnot 4535	. . . . . . . . . . . . . . 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 7436	. . . . . . . . . . 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 5198	. . . . . . . . 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 38565	. . . . . . 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 13308	. . . . . . 7 ⊢ ((0 ∈ ℝ ∧ (𝐵 + 𝐶) ∈ ℝ) → 0 ≤ if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0))
252	8, 24, 251	sylancr 599	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0))
253	35, 176, 37, 179, 250, 35, 37, 252, 184	itgaddnclem1 38576	. . . . 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 26097	. . . . 5 ⊢ (𝜑 → ∫𝐴if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0) d𝑥 ∈ ℂ)
256	10, 51, 13, 54, 59, 10, 13, 62, 64	itgaddnclem1 38576	. . . . . 6 ⊢ (𝜑 → ∫𝐴(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) d𝑥 = (∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 + ∫𝐴if(0 ≤ 𝐶, 𝐶, 0) d𝑥))
257	10, 51	itgcl 26097	. . . . . . 7 ⊢ (𝜑 → ∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 ∈ ℂ)
258	13, 54	itgcl 26097	. . . . . . 7 ⊢ (𝜑 → ∫𝐴if(0 ≤ 𝐶, 𝐶, 0) d𝑥 ∈ ℂ)
259	257, 258	addcld 11321	. . . . . 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 26097	. . . . 5 ⊢ (𝜑 → ∫𝐴if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) d𝑥 ∈ ℂ)
262	17, 177, 21, 178, 169, 17, 21, 181, 183	itgaddnclem1 38576	. . . . . 6 ⊢ (𝜑 → ∫𝐴(if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)) d𝑥 = (∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥 + ∫𝐴if(0 ≤ -𝐶, -𝐶, 0) d𝑥))
263	17, 177	itgcl 26097	. . . . . . 7 ⊢ (𝜑 → ∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥 ∈ ℂ)
264	21, 178	itgcl 26097	. . . . . . 7 ⊢ (𝜑 → ∫𝐴if(0 ≤ -𝐶, -𝐶, 0) d𝑥 ∈ ℂ)
265	263, 264	addcld 11321	. . . . . 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 11713	. . . 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 235	. . 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 7436	. . 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 11709	. . 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 26110	. 2 ⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) d𝑥 − ∫𝐴if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0) d𝑥))
273	1, 42	itgreval 26110	. . 3 ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = (∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 − ∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥))
274	4, 43	itgreval 26110	. . 3 ⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = (∫𝐴if(0 ≤ 𝐶, 𝐶, 0) d𝑥 − ∫𝐴if(0 ≤ -𝐶, -𝐶, 0) d𝑥))
275	273, 274	oveq12d 7436	. 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

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 ifcif 4482 class class class wbr 5103 ↦ cmpt 5186 (class class class)co 7418 ℂcc 11191 ℝcr 11192 0cc0 11193 + caddc 11196 < clt 11336 ≤ cle 11337 − cmin 11534 -cneg 11535 MblFncmbf 25928 𝐿¹cibl 25931 ∫citg 25932

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-inf2 9635 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269 ax-pre-mulgt0 11270 ax-pre-sup 11271 ax-addf 11272

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-disj 5071 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-of 7691 df-ofr 7692 df-om 7876 df-1st 7999 df-2nd 8000 df-frecs 8292 df-wrecs 8323 df-recs 8372 df-rdg 8411 df-1o 8469 df-2o 8470 df-er 8710 df-map 8842 df-pm 8843 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-fi 9396 df-sup 9427 df-inf 9428 df-oi 9497 df-dju 9975 df-card 10013 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-sub 11536 df-neg 11537 df-div 11967 df-nn 12329 df-2 12398 df-3 12399 df-4 12400 df-n0 12600 df-z 12687 df-uz 12959 df-q 13069 df-rp 13114 df-xneg 13234 df-xadd 13235 df-xmul 13236 df-ioo 13473 df-ico 13475 df-icc 13476 df-fz 13633 df-fzo 13782 df-fl 13925 df-mod 14003 df-seq 14138 df-exp 14198 df-hash 14468 df-cj 15259 df-re 15260 df-im 15261 df-sqrt 15395 df-abs 15396 df-clim 15648 df-sum 15847 df-rest 17586 df-topgen 17607 df-psmet 21663 df-xmet 21664 df-met 21665 df-bl 21666 df-mopn 21667 df-top 23205 df-topon 23222 df-bases 23257 df-cmp 23698 df-ovol 25778 df-vol 25779 df-mbf 25933 df-itg1 25934 df-itg2 25935 df-ibl 25936 df-itg 25937 df-0p 25984

This theorem is used by: itgaddnc 38578

W3C validator