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 33469

Description: Lemma for itgaddnc 33470; cf. itgaddlem2 23590. (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 12027	. . . . . . . . . 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 12027	. . . . . . . . . 10 ⊢ (𝐶 ∈ ℝ → (if(0 ≤ 𝐶, 𝐶, 0) − if(0 ≤ -𝐶, -𝐶, 0)) = 𝐶)
6	4, 5	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐶, 𝐶, 0) − if(0 ≤ -𝐶, -𝐶, 0)) = 𝐶)
7	3, 6	oveq12d 6668	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((if(0 ≤ 𝐵, 𝐵, 0) − if(0 ≤ -𝐵, -𝐵, 0)) + (if(0 ≤ 𝐶, 𝐶, 0) − if(0 ≤ -𝐶, -𝐶, 0))) = (𝐵 + 𝐶))
8		0re 10040	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
9		ifcl 4130	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
10	1, 8, 9	sylancl 694	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
11	10	recnd 10068	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℂ)
12		ifcl 4130	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ)
13	4, 8, 12	sylancl 694	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ)
14	13	recnd 10068	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℂ)
15	1	renegcld 10457	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℝ)
16		ifcl 4130	. . . . . . . . . . 11 ⊢ ((-𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ)
17	15, 8, 16	sylancl 694	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ)
18	17	recnd 10068	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℂ)
19	4	renegcld 10457	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐶 ∈ ℝ)
20		ifcl 4130	. . . . . . . . . . 11 ⊢ ((-𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ -𝐶, -𝐶, 0) ∈ ℝ)
21	19, 8, 20	sylancl 694	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐶, -𝐶, 0) ∈ ℝ)
22	21	recnd 10068	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐶, -𝐶, 0) ∈ ℂ)
23	11, 14, 18, 22	addsub4d 10439	. . . . . . . 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 10069	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 + 𝐶) ∈ ℝ)
25		max0sub 12027	. . . . . . . . 9 ⊢ ((𝐵 + 𝐶) ∈ ℝ → (if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) − if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0)) = (𝐵 + 𝐶))
26	24, 25	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) − if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0)) = (𝐵 + 𝐶))
27	7, 23, 26	3eqtr4rd 2667	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) − if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0)) = ((if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) − (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0))))
28	24	renegcld 10457	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(𝐵 + 𝐶) ∈ ℝ)
29		ifcl 4130	. . . . . . . . . 10 ⊢ ((-(𝐵 + 𝐶) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0) ∈ ℝ)
30	28, 8, 29	sylancl 694	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0) ∈ ℝ)
31	30	recnd 10068	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0) ∈ ℂ)
32	10, 13	readdcld 10069	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℝ)
33	32	recnd 10068	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℂ)
34		ifcl 4130	. . . . . . . . . 10 ⊢ (((𝐵 + 𝐶) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) ∈ ℝ)
35	24, 8, 34	sylancl 694	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) ∈ ℝ)
36	35	recnd 10068	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) ∈ ℂ)
37	17, 21	readdcld 10069	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)) ∈ ℝ)
38	37	recnd 10068	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)) ∈ ℂ)
39	31, 33, 36, 38	addsubeq4d 10443	. . . . . . 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 247	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0) + (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) + (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0))))
41	40	itgeq2dv 23548	. . . . 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 33467	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ 𝐿¹)
46	24	iblre 23560	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ 𝐿¹ ↔ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0)) ∈ 𝐿¹ ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0)) ∈ 𝐿¹)))
47	45, 46	mpbid 222	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0)) ∈ 𝐿¹ ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0)) ∈ 𝐿¹))
48	47	simprd 479	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0)) ∈ 𝐿¹)
49	1	iblre 23560	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿¹ ↔ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ 𝐿¹ ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ 𝐿¹)))
50	42, 49	mpbid 222	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ 𝐿¹ ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ 𝐿¹))
51	50	simpld 475	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ 𝐿¹)
52	4	iblre 23560	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿¹ ↔ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐶, 𝐶, 0)) ∈ 𝐿¹ ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐶, -𝐶, 0)) ∈ 𝐿¹)))
53	43, 52	mpbid 222	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐶, 𝐶, 0)) ∈ 𝐿¹ ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐶, -𝐶, 0)) ∈ 𝐿¹))
54	53	simpld 475	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐶, 𝐶, 0)) ∈ 𝐿¹)
55		iblmbf 23534	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿¹ → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
56	42, 55	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
57		iblmbf 23534	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿¹ → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)
58	43, 57	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)
59	56, 1, 58, 4, 44	mbfposadd 33457	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ∈ MblFn)
60	10, 51, 13, 54, 59	ibladdnc 33467	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ∈ 𝐿¹)
61		max1 12016	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 0 ≤ if(0 ≤ 𝐵, 𝐵, 0))
62	8, 1, 61	sylancr 695	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝐵, 𝐵, 0))
63		max1 12016	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 0 ≤ if(0 ≤ 𝐶, 𝐶, 0))
64	8, 4, 63	sylancr 695	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝐶, 𝐶, 0))
65	10, 13, 62, 64	addge0d 10603	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
66	65	iftrued 4094	. . . . . . . . 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 6666	. . . . . . . 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 4744	. . . . . . 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 23417	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -(𝐵 + 𝐶)) ∈ MblFn)
70	1	recnd 10068	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)
71	4	recnd 10068	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)
72	70, 71	negdid 10405	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(𝐵 + 𝐶) = (-𝐵 + -𝐶))
73	72	oveq1d 6665	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-(𝐵 + 𝐶) + (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = ((-𝐵 + -𝐶) + (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
74	15	recnd 10068	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℂ)
75	19	recnd 10068	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐶 ∈ ℂ)
76	74, 75, 11, 14	add4d 10264	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((-𝐵 + -𝐶) + (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = ((-𝐵 + if(0 ≤ 𝐵, 𝐵, 0)) + (-𝐶 + if(0 ≤ 𝐶, 𝐶, 0))))
77		negeq 10273	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 = 0 → -𝐵 = -0)
78		neg0 10327	. . . . . . . . . . . . . . . 16 ⊢ -0 = 0
79	77, 78	syl6eq 2672	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = 0 → -𝐵 = 0)
80		0le0 11110	. . . . . . . . . . . . . . . . 17 ⊢ 0 ≤ 0
81	80, 79	syl5breqr 4691	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 = 0 → 0 ≤ -𝐵)
82	81	iftrued 4094	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = 0 → if(0 ≤ -𝐵, -𝐵, 0) = -𝐵)
83		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 = 0 → 𝐵 = 0)
84	80, 83	syl5breqr 4691	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 = 0 → 0 ≤ 𝐵)
85	84	iftrued 4094	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 = 0 → if(0 ≤ 𝐵, 𝐵, 0) = 𝐵)
86	85, 83	eqtrd 2656	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 = 0 → if(0 ≤ 𝐵, 𝐵, 0) = 0)
87	79, 86	oveq12d 6668	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 = 0 → (-𝐵 + if(0 ≤ 𝐵, 𝐵, 0)) = (0 + 0))
88		00id 10211	. . . . . . . . . . . . . . . 16 ⊢ (0 + 0) = 0
89	87, 88	syl6eq 2672	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = 0 → (-𝐵 + if(0 ≤ 𝐵, 𝐵, 0)) = 0)
90	79, 82, 89	3eqtr4rd 2667	. . . . . . . . . . . . . 14 ⊢ (𝐵 = 0 → (-𝐵 + if(0 ≤ 𝐵, 𝐵, 0)) = if(0 ≤ -𝐵, -𝐵, 0))
91	90	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 = 0) → (-𝐵 + if(0 ≤ 𝐵, 𝐵, 0)) = if(0 ≤ -𝐵, -𝐵, 0))
92		ovif2 6738	. . . . . . . . . . . . . 14 ⊢ (-𝐵 + if(0 ≤ 𝐵, 𝐵, 0)) = if(0 ≤ 𝐵, (-𝐵 + 𝐵), (-𝐵 + 0))
93	70	negne0bd 10385	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ≠ 0 ↔ -𝐵 ≠ 0))
94	93	biimpa 501	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → -𝐵 ≠ 0)
95	1	le0neg2d 10600	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐵 ↔ -𝐵 ≤ 0))
96		leloe 10124	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((-𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → (-𝐵 ≤ 0 ↔ (-𝐵 < 0 ∨ -𝐵 = 0)))
97	15, 8, 96	sylancl 694	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 ≤ 0 ↔ (-𝐵 < 0 ∨ -𝐵 = 0)))
98	95, 97	bitrd 268	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐵 ↔ (-𝐵 < 0 ∨ -𝐵 = 0)))
99		df-ne 2795	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (-𝐵 ≠ 0 ↔ ¬ -𝐵 = 0)
100		biorf 420	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ -𝐵 = 0 → (-𝐵 < 0 ↔ (-𝐵 = 0 ∨ -𝐵 < 0)))
101	99, 100	sylbi 207	. . . . . . . . . . . . . . . . . . . 20 ⊢ (-𝐵 ≠ 0 → (-𝐵 < 0 ↔ (-𝐵 = 0 ∨ -𝐵 < 0)))
102		orcom 402	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((-𝐵 = 0 ∨ -𝐵 < 0) ↔ (-𝐵 < 0 ∨ -𝐵 = 0))
103	101, 102	syl6rbb 277	. . . . . . . . . . . . . . . . . . 19 ⊢ (-𝐵 ≠ 0 → ((-𝐵 < 0 ∨ -𝐵 = 0) ↔ -𝐵 < 0))
104	98, 103	sylan9bb 736	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ -𝐵 ≠ 0) → (0 ≤ 𝐵 ↔ -𝐵 < 0))
105	94, 104	syldan 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (0 ≤ 𝐵 ↔ -𝐵 < 0))
106		ltnle 10117	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → (-𝐵 < 0 ↔ ¬ 0 ≤ -𝐵))
107	15, 8, 106	sylancl 694	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 < 0 ↔ ¬ 0 ≤ -𝐵))
108	107	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (-𝐵 < 0 ↔ ¬ 0 ≤ -𝐵))
109	105, 108	bitrd 268	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (0 ≤ 𝐵 ↔ ¬ 0 ≤ -𝐵))
110	74, 70	addcomd 10238	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 + 𝐵) = (𝐵 + -𝐵))
111	70	negidd 10382	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 + -𝐵) = 0)
112	110, 111	eqtrd 2656	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 + 𝐵) = 0)
113	112	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (-𝐵 + 𝐵) = 0)
114	74	addid1d 10236	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 + 0) = -𝐵)
115	114	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (-𝐵 + 0) = -𝐵)
116	109, 113, 115	ifbieq12d 4113	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → if(0 ≤ 𝐵, (-𝐵 + 𝐵), (-𝐵 + 0)) = if(¬ 0 ≤ -𝐵, 0, -𝐵))
117		ifnot 4133	. . . . . . . . . . . . . . 15 ⊢ if(¬ 0 ≤ -𝐵, 0, -𝐵) = if(0 ≤ -𝐵, -𝐵, 0)
118	116, 117	syl6eq 2672	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → if(0 ≤ 𝐵, (-𝐵 + 𝐵), (-𝐵 + 0)) = if(0 ≤ -𝐵, -𝐵, 0))
119	92, 118	syl5eq 2668	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (-𝐵 + if(0 ≤ 𝐵, 𝐵, 0)) = if(0 ≤ -𝐵, -𝐵, 0))
120	91, 119	pm2.61dane 2881	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 + if(0 ≤ 𝐵, 𝐵, 0)) = if(0 ≤ -𝐵, -𝐵, 0))
121		negeq 10273	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 = 0 → -𝐶 = -0)
122	121, 78	syl6eq 2672	. . . . . . . . . . . . . . 15 ⊢ (𝐶 = 0 → -𝐶 = 0)
123	80, 122	syl5breqr 4691	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 = 0 → 0 ≤ -𝐶)
124	123	iftrued 4094	. . . . . . . . . . . . . . 15 ⊢ (𝐶 = 0 → if(0 ≤ -𝐶, -𝐶, 0) = -𝐶)
125		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐶 = 0 → 𝐶 = 0)
126	80, 125	syl5breqr 4691	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 = 0 → 0 ≤ 𝐶)
127	126	iftrued 4094	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐶 = 0 → if(0 ≤ 𝐶, 𝐶, 0) = 𝐶)
128	127, 125	eqtrd 2656	. . . . . . . . . . . . . . . . 17 ⊢ (𝐶 = 0 → if(0 ≤ 𝐶, 𝐶, 0) = 0)
129	122, 128	oveq12d 6668	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 = 0 → (-𝐶 + if(0 ≤ 𝐶, 𝐶, 0)) = (0 + 0))
130	129, 88	syl6eq 2672	. . . . . . . . . . . . . . 15 ⊢ (𝐶 = 0 → (-𝐶 + if(0 ≤ 𝐶, 𝐶, 0)) = 0)
131	122, 124, 130	3eqtr4rd 2667	. . . . . . . . . . . . . 14 ⊢ (𝐶 = 0 → (-𝐶 + if(0 ≤ 𝐶, 𝐶, 0)) = if(0 ≤ -𝐶, -𝐶, 0))
132	131	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 = 0) → (-𝐶 + if(0 ≤ 𝐶, 𝐶, 0)) = if(0 ≤ -𝐶, -𝐶, 0))
133		ovif2 6738	. . . . . . . . . . . . . 14 ⊢ (-𝐶 + if(0 ≤ 𝐶, 𝐶, 0)) = if(0 ≤ 𝐶, (-𝐶 + 𝐶), (-𝐶 + 0))
134	71	negne0bd 10385	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 ≠ 0 ↔ -𝐶 ≠ 0))
135	134	biimpa 501	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → -𝐶 ≠ 0)
136	4	le0neg2d 10600	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐶 ↔ -𝐶 ≤ 0))
137		leloe 10124	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((-𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → (-𝐶 ≤ 0 ↔ (-𝐶 < 0 ∨ -𝐶 = 0)))
138	19, 8, 137	sylancl 694	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐶 ≤ 0 ↔ (-𝐶 < 0 ∨ -𝐶 = 0)))
139	136, 138	bitrd 268	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐶 ↔ (-𝐶 < 0 ∨ -𝐶 = 0)))
140		df-ne 2795	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (-𝐶 ≠ 0 ↔ ¬ -𝐶 = 0)
141		biorf 420	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ -𝐶 = 0 → (-𝐶 < 0 ↔ (-𝐶 = 0 ∨ -𝐶 < 0)))
142	140, 141	sylbi 207	. . . . . . . . . . . . . . . . . . . 20 ⊢ (-𝐶 ≠ 0 → (-𝐶 < 0 ↔ (-𝐶 = 0 ∨ -𝐶 < 0)))
143		orcom 402	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((-𝐶 = 0 ∨ -𝐶 < 0) ↔ (-𝐶 < 0 ∨ -𝐶 = 0))
144	142, 143	syl6rbb 277	. . . . . . . . . . . . . . . . . . 19 ⊢ (-𝐶 ≠ 0 → ((-𝐶 < 0 ∨ -𝐶 = 0) ↔ -𝐶 < 0))
145	139, 144	sylan9bb 736	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ -𝐶 ≠ 0) → (0 ≤ 𝐶 ↔ -𝐶 < 0))
146	135, 145	syldan 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (0 ≤ 𝐶 ↔ -𝐶 < 0))
147		ltnle 10117	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → (-𝐶 < 0 ↔ ¬ 0 ≤ -𝐶))
148	19, 8, 147	sylancl 694	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐶 < 0 ↔ ¬ 0 ≤ -𝐶))
149	148	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (-𝐶 < 0 ↔ ¬ 0 ≤ -𝐶))
150	146, 149	bitrd 268	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (0 ≤ 𝐶 ↔ ¬ 0 ≤ -𝐶))
151	75, 71	addcomd 10238	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐶 + 𝐶) = (𝐶 + -𝐶))
152	71	negidd 10382	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 + -𝐶) = 0)
153	151, 152	eqtrd 2656	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐶 + 𝐶) = 0)
154	153	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (-𝐶 + 𝐶) = 0)
155	75	addid1d 10236	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐶 + 0) = -𝐶)
156	155	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (-𝐶 + 0) = -𝐶)
157	150, 154, 156	ifbieq12d 4113	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → if(0 ≤ 𝐶, (-𝐶 + 𝐶), (-𝐶 + 0)) = if(¬ 0 ≤ -𝐶, 0, -𝐶))
158		ifnot 4133	. . . . . . . . . . . . . . 15 ⊢ if(¬ 0 ≤ -𝐶, 0, -𝐶) = if(0 ≤ -𝐶, -𝐶, 0)
159	157, 158	syl6eq 2672	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → if(0 ≤ 𝐶, (-𝐶 + 𝐶), (-𝐶 + 0)) = if(0 ≤ -𝐶, -𝐶, 0))
160	133, 159	syl5eq 2668	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (-𝐶 + if(0 ≤ 𝐶, 𝐶, 0)) = if(0 ≤ -𝐶, -𝐶, 0))
161	132, 160	pm2.61dane 2881	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐶 + if(0 ≤ 𝐶, 𝐶, 0)) = if(0 ≤ -𝐶, -𝐶, 0))
162	120, 161	oveq12d 6668	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((-𝐵 + if(0 ≤ 𝐵, 𝐵, 0)) + (-𝐶 + if(0 ≤ 𝐶, 𝐶, 0))) = (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)))
163	73, 76, 162	3eqtrd 2660	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-(𝐵 + 𝐶) + (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)))
164	163	mpteq2dva 4744	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (-(𝐵 + 𝐶) + (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))) = (𝑥 ∈ 𝐴 ↦ (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0))))
165	1, 56	mbfneg 23417	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐵) ∈ MblFn)
166	4, 58	mbfneg 23417	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐶) ∈ MblFn)
167	72	mpteq2dva 4744	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -(𝐵 + 𝐶)) = (𝑥 ∈ 𝐴 ↦ (-𝐵 + -𝐶)))
168	167, 69	eqeltrrd 2702	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (-𝐵 + -𝐶)) ∈ MblFn)
169	165, 15, 166, 19, 168	mbfposadd 33457	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0))) ∈ MblFn)
170	164, 169	eqeltrd 2701	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (-(𝐵 + 𝐶) + (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))) ∈ MblFn)
171	69, 28, 59, 32, 170	mbfposadd 33457	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0) + if(0 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) ∈ MblFn)
172	68, 171	eqeltrrd 2702	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0) + (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))) ∈ MblFn)
173		max1 12016	. . . . . . 7 ⊢ ((0 ∈ ℝ ∧ -(𝐵 + 𝐶) ∈ ℝ) → 0 ≤ if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0))
174	8, 28, 173	sylancr 695	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0))
175	30, 48, 32, 60, 172, 30, 32, 174, 65	itgaddnclem1 33468	. . . . 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 475	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0)) ∈ 𝐿¹)
177	50	simprd 479	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ 𝐿¹)
178	53	simprd 479	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐶, -𝐶, 0)) ∈ 𝐿¹)
179	17, 177, 21, 178, 169	ibladdnc 33467	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0))) ∈ 𝐿¹)
180		max1 12016	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ -𝐵 ∈ ℝ) → 0 ≤ if(0 ≤ -𝐵, -𝐵, 0))
181	8, 15, 180	sylancr 695	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ -𝐵, -𝐵, 0))
182		max1 12016	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ -𝐶 ∈ ℝ) → 0 ≤ if(0 ≤ -𝐶, -𝐶, 0))
183	8, 19, 182	sylancr 695	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ -𝐶, -𝐶, 0))
184	17, 21, 181, 183	addge0d 10603	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)))
185	184	iftrued 4094	. . . . . . . . 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 6666	. . . . . . . 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 4744	. . . . . . 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 10264	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐵 + 𝐶) + (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0))) = ((𝐵 + if(0 ≤ -𝐵, -𝐵, 0)) + (𝐶 + if(0 ≤ -𝐶, -𝐶, 0))))
189	82, 79	eqtrd 2656	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 = 0 → if(0 ≤ -𝐵, -𝐵, 0) = 0)
190	83, 189	oveq12d 6668	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 = 0 → (𝐵 + if(0 ≤ -𝐵, -𝐵, 0)) = (0 + 0))
191	190, 88	syl6eq 2672	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = 0 → (𝐵 + if(0 ≤ -𝐵, -𝐵, 0)) = 0)
192	83, 85, 191	3eqtr4rd 2667	. . . . . . . . . . . . . 14 ⊢ (𝐵 = 0 → (𝐵 + if(0 ≤ -𝐵, -𝐵, 0)) = if(0 ≤ 𝐵, 𝐵, 0))
193	192	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 = 0) → (𝐵 + if(0 ≤ -𝐵, -𝐵, 0)) = if(0 ≤ 𝐵, 𝐵, 0))
194		ovif2 6738	. . . . . . . . . . . . . 14 ⊢ (𝐵 + if(0 ≤ -𝐵, -𝐵, 0)) = if(0 ≤ -𝐵, (𝐵 + -𝐵), (𝐵 + 0))
195	1	le0neg1d 10599	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ≤ 0 ↔ 0 ≤ -𝐵))
196		leloe 10124	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐵 ≤ 0 ↔ (𝐵 < 0 ∨ 𝐵 = 0)))
197	1, 8, 196	sylancl 694	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ≤ 0 ↔ (𝐵 < 0 ∨ 𝐵 = 0)))
198	195, 197	bitr3d 270	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ -𝐵 ↔ (𝐵 < 0 ∨ 𝐵 = 0)))
199		df-ne 2795	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 ≠ 0 ↔ ¬ 𝐵 = 0)
200		biorf 420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝐵 = 0 → (𝐵 < 0 ↔ (𝐵 = 0 ∨ 𝐵 < 0)))
201	199, 200	sylbi 207	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ≠ 0 → (𝐵 < 0 ↔ (𝐵 = 0 ∨ 𝐵 < 0)))
202		orcom 402	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 = 0 ∨ 𝐵 < 0) ↔ (𝐵 < 0 ∨ 𝐵 = 0))
203	201, 202	syl6rbb 277	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ≠ 0 → ((𝐵 < 0 ∨ 𝐵 = 0) ↔ 𝐵 < 0))
204	198, 203	sylan9bb 736	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (0 ≤ -𝐵 ↔ 𝐵 < 0))
205		ltnle 10117	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐵 < 0 ↔ ¬ 0 ≤ 𝐵))
206	1, 8, 205	sylancl 694	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 < 0 ↔ ¬ 0 ≤ 𝐵))
207	206	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (𝐵 < 0 ↔ ¬ 0 ≤ 𝐵))
208	204, 207	bitrd 268	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (0 ≤ -𝐵 ↔ ¬ 0 ≤ 𝐵))
209	111	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (𝐵 + -𝐵) = 0)
210	70	addid1d 10236	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 + 0) = 𝐵)
211	210	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (𝐵 + 0) = 𝐵)
212	208, 209, 211	ifbieq12d 4113	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → if(0 ≤ -𝐵, (𝐵 + -𝐵), (𝐵 + 0)) = if(¬ 0 ≤ 𝐵, 0, 𝐵))
213		ifnot 4133	. . . . . . . . . . . . . . 15 ⊢ if(¬ 0 ≤ 𝐵, 0, 𝐵) = if(0 ≤ 𝐵, 𝐵, 0)
214	212, 213	syl6eq 2672	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → if(0 ≤ -𝐵, (𝐵 + -𝐵), (𝐵 + 0)) = if(0 ≤ 𝐵, 𝐵, 0))
215	194, 214	syl5eq 2668	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (𝐵 + if(0 ≤ -𝐵, -𝐵, 0)) = if(0 ≤ 𝐵, 𝐵, 0))
216	193, 215	pm2.61dane 2881	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 + if(0 ≤ -𝐵, -𝐵, 0)) = if(0 ≤ 𝐵, 𝐵, 0))
217	124, 122	eqtrd 2656	. . . . . . . . . . . . . . . . 17 ⊢ (𝐶 = 0 → if(0 ≤ -𝐶, -𝐶, 0) = 0)
218	125, 217	oveq12d 6668	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 = 0 → (𝐶 + if(0 ≤ -𝐶, -𝐶, 0)) = (0 + 0))
219	218, 88	syl6eq 2672	. . . . . . . . . . . . . . 15 ⊢ (𝐶 = 0 → (𝐶 + if(0 ≤ -𝐶, -𝐶, 0)) = 0)
220	125, 127, 219	3eqtr4rd 2667	. . . . . . . . . . . . . 14 ⊢ (𝐶 = 0 → (𝐶 + if(0 ≤ -𝐶, -𝐶, 0)) = if(0 ≤ 𝐶, 𝐶, 0))
221	220	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 = 0) → (𝐶 + if(0 ≤ -𝐶, -𝐶, 0)) = if(0 ≤ 𝐶, 𝐶, 0))
222		ovif2 6738	. . . . . . . . . . . . . 14 ⊢ (𝐶 + if(0 ≤ -𝐶, -𝐶, 0)) = if(0 ≤ -𝐶, (𝐶 + -𝐶), (𝐶 + 0))
223	4	le0neg1d 10599	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 ≤ 0 ↔ 0 ≤ -𝐶))
224		leloe 10124	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐶 ≤ 0 ↔ (𝐶 < 0 ∨ 𝐶 = 0)))
225	4, 8, 224	sylancl 694	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 ≤ 0 ↔ (𝐶 < 0 ∨ 𝐶 = 0)))
226	223, 225	bitr3d 270	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ -𝐶 ↔ (𝐶 < 0 ∨ 𝐶 = 0)))
227		df-ne 2795	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐶 ≠ 0 ↔ ¬ 𝐶 = 0)
228		biorf 420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝐶 = 0 → (𝐶 < 0 ↔ (𝐶 = 0 ∨ 𝐶 < 0)))
229	227, 228	sylbi 207	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 ≠ 0 → (𝐶 < 0 ↔ (𝐶 = 0 ∨ 𝐶 < 0)))
230		orcom 402	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 = 0 ∨ 𝐶 < 0) ↔ (𝐶 < 0 ∨ 𝐶 = 0))
231	229, 230	syl6rbb 277	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐶 ≠ 0 → ((𝐶 < 0 ∨ 𝐶 = 0) ↔ 𝐶 < 0))
232	226, 231	sylan9bb 736	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (0 ≤ -𝐶 ↔ 𝐶 < 0))
233		ltnle 10117	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐶 < 0 ↔ ¬ 0 ≤ 𝐶))
234	4, 8, 233	sylancl 694	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 < 0 ↔ ¬ 0 ≤ 𝐶))
235	234	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (𝐶 < 0 ↔ ¬ 0 ≤ 𝐶))
236	232, 235	bitrd 268	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (0 ≤ -𝐶 ↔ ¬ 0 ≤ 𝐶))
237	152	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (𝐶 + -𝐶) = 0)
238	71	addid1d 10236	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 + 0) = 𝐶)
239	238	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (𝐶 + 0) = 𝐶)
240	236, 237, 239	ifbieq12d 4113	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → if(0 ≤ -𝐶, (𝐶 + -𝐶), (𝐶 + 0)) = if(¬ 0 ≤ 𝐶, 0, 𝐶))
241		ifnot 4133	. . . . . . . . . . . . . . 15 ⊢ if(¬ 0 ≤ 𝐶, 0, 𝐶) = if(0 ≤ 𝐶, 𝐶, 0)
242	240, 241	syl6eq 2672	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → if(0 ≤ -𝐶, (𝐶 + -𝐶), (𝐶 + 0)) = if(0 ≤ 𝐶, 𝐶, 0))
243	222, 242	syl5eq 2668	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (𝐶 + if(0 ≤ -𝐶, -𝐶, 0)) = if(0 ≤ 𝐶, 𝐶, 0))
244	221, 243	pm2.61dane 2881	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 + if(0 ≤ -𝐶, -𝐶, 0)) = if(0 ≤ 𝐶, 𝐶, 0))
245	216, 244	oveq12d 6668	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐵 + if(0 ≤ -𝐵, -𝐵, 0)) + (𝐶 + if(0 ≤ -𝐶, -𝐶, 0))) = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
246	188, 245	eqtrd 2656	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐵 + 𝐶) + (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0))) = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
247	246	mpteq2dva 4744	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((𝐵 + 𝐶) + (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)))) = (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
248	247, 59	eqeltrd 2701	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((𝐵 + 𝐶) + (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)))) ∈ MblFn)
249	44, 24, 169, 37, 248	mbfposadd 33457	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) + if(0 ≤ (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)), (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)), 0))) ∈ MblFn)
250	187, 249	eqeltrrd 2702	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) + (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)))) ∈ MblFn)
251		max1 12016	. . . . . . 7 ⊢ ((0 ∈ ℝ ∧ (𝐵 + 𝐶) ∈ ℝ) → 0 ≤ if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0))
252	8, 24, 251	sylancr 695	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0))
253	35, 176, 37, 179, 250, 35, 37, 252, 184	itgaddnclem1 33468	. . . . 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 2664	. . . 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 23550	. . . . 5 ⊢ (𝜑 → ∫𝐴if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0) d𝑥 ∈ ℂ)
256	10, 51, 13, 54, 59, 10, 13, 62, 64	itgaddnclem1 33468	. . . . . 6 ⊢ (𝜑 → ∫𝐴(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) d𝑥 = (∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 + ∫𝐴if(0 ≤ 𝐶, 𝐶, 0) d𝑥))
257	10, 51	itgcl 23550	. . . . . . 7 ⊢ (𝜑 → ∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 ∈ ℂ)
258	13, 54	itgcl 23550	. . . . . . 7 ⊢ (𝜑 → ∫𝐴if(0 ≤ 𝐶, 𝐶, 0) d𝑥 ∈ ℂ)
259	257, 258	addcld 10059	. . . . . 6 ⊢ (𝜑 → (∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 + ∫𝐴if(0 ≤ 𝐶, 𝐶, 0) d𝑥) ∈ ℂ)
260	256, 259	eqeltrd 2701	. . . . 5 ⊢ (𝜑 → ∫𝐴(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) d𝑥 ∈ ℂ)
261	35, 176	itgcl 23550	. . . . 5 ⊢ (𝜑 → ∫𝐴if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) d𝑥 ∈ ℂ)
262	17, 177, 21, 178, 169, 17, 21, 181, 183	itgaddnclem1 33468	. . . . . 6 ⊢ (𝜑 → ∫𝐴(if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)) d𝑥 = (∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥 + ∫𝐴if(0 ≤ -𝐶, -𝐶, 0) d𝑥))
263	17, 177	itgcl 23550	. . . . . . 7 ⊢ (𝜑 → ∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥 ∈ ℂ)
264	21, 178	itgcl 23550	. . . . . . 7 ⊢ (𝜑 → ∫𝐴if(0 ≤ -𝐶, -𝐶, 0) d𝑥 ∈ ℂ)
265	263, 264	addcld 10059	. . . . . 6 ⊢ (𝜑 → (∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥 + ∫𝐴if(0 ≤ -𝐶, -𝐶, 0) d𝑥) ∈ ℂ)
266	262, 265	eqeltrd 2701	. . . . 5 ⊢ (𝜑 → ∫𝐴(if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)) d𝑥 ∈ ℂ)
267	255, 260, 261, 266	addsubeq4d 10443	. . . 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 222	. . 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 6668	. . 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 10439	. . 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 2660	. 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 23563	. 2 ⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) d𝑥 − ∫𝐴if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0) d𝑥))
273	1, 42	itgreval 23563	. . 3 ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = (∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 − ∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥))
274	4, 43	itgreval 23563	. . 3 ⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = (∫𝐴if(0 ≤ 𝐶, 𝐶, 0) d𝑥 − ∫𝐴if(0 ≤ -𝐶, -𝐶, 0) d𝑥))
275	273, 274	oveq12d 6668	. 2 ⊢ (𝜑 → (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥) = ((∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 − ∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥) + (∫𝐴if(0 ≤ 𝐶, 𝐶, 0) d𝑥 − ∫𝐴if(0 ≤ -𝐶, -𝐶, 0) d𝑥)))
276	271, 272, 275	3eqtr4d 2666	1 ⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∨ wo 383 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ifcif 4086 class class class wbr 4653 ↦ cmpt 4729 (class class class)co 6650 ℂcc 9934 ℝcr 9935 0cc0 9936 + caddc 9939 < clt 10074 ≤ cle 10075 − cmin 10266 -cneg 10267 MblFncmbf 23383 𝐿¹cibl 23386 ∫citg 23387

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-disj 4621 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-ofr 6898 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-n0 11293 df-z 11378 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-sum 14417 df-rest 16083 df-topgen 16104 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-top 20699 df-topon 20716 df-bases 20750 df-cmp 21190 df-ovol 23233 df-vol 23234 df-mbf 23388 df-itg1 23389 df-itg2 23390 df-ibl 23391 df-itg 23392 df-0p 23437

This theorem is referenced by: itgaddnc 33470

W3C validator