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 38014

Description: Lemma for itgaddnc 38015; cf. itgaddlem2 25801. (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 13139	. . . . . . . . . 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 13139	. . . . . . . . . 10 ⊢ (𝐶 ∈ ℝ → (if(0 ≤ 𝐶, 𝐶, 0) − if(0 ≤ -𝐶, -𝐶, 0)) = 𝐶)
6	4, 5	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐶, 𝐶, 0) − if(0 ≤ -𝐶, -𝐶, 0)) = 𝐶)
7	3, 6	oveq12d 7378	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((if(0 ≤ 𝐵, 𝐵, 0) − if(0 ≤ -𝐵, -𝐵, 0)) + (if(0 ≤ 𝐶, 𝐶, 0) − if(0 ≤ -𝐶, -𝐶, 0))) = (𝐵 + 𝐶))
8		0re 11137	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
9		ifcl 4513	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
10	1, 8, 9	sylancl 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ)
11	10	recnd 11164	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℂ)
12		ifcl 4513	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ)
13	4, 8, 12	sylancl 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ)
14	13	recnd 11164	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℂ)
15	1	renegcld 11568	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℝ)
16		ifcl 4513	. . . . . . . . . . 11 ⊢ ((-𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ)
17	15, 8, 16	sylancl 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ)
18	17	recnd 11164	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℂ)
19	4	renegcld 11568	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐶 ∈ ℝ)
20		ifcl 4513	. . . . . . . . . . 11 ⊢ ((-𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ -𝐶, -𝐶, 0) ∈ ℝ)
21	19, 8, 20	sylancl 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐶, -𝐶, 0) ∈ ℝ)
22	21	recnd 11164	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐶, -𝐶, 0) ∈ ℂ)
23	11, 14, 18, 22	addsub4d 11543	. . . . . . . 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 11165	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 + 𝐶) ∈ ℝ)
25		max0sub 13139	. . . . . . . . 9 ⊢ ((𝐵 + 𝐶) ∈ ℝ → (if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) − if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0)) = (𝐵 + 𝐶))
26	24, 25	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) − if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0)) = (𝐵 + 𝐶))
27	7, 23, 26	3eqtr4rd 2783	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) − if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0)) = ((if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) − (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0))))
28	24	renegcld 11568	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(𝐵 + 𝐶) ∈ ℝ)
29		ifcl 4513	. . . . . . . . . 10 ⊢ ((-(𝐵 + 𝐶) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0) ∈ ℝ)
30	28, 8, 29	sylancl 587	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0) ∈ ℝ)
31	30	recnd 11164	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0) ∈ ℂ)
32	10, 13	readdcld 11165	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℝ)
33	32	recnd 11164	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) ∈ ℂ)
34		ifcl 4513	. . . . . . . . . 10 ⊢ (((𝐵 + 𝐶) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) ∈ ℝ)
35	24, 8, 34	sylancl 587	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) ∈ ℝ)
36	35	recnd 11164	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) ∈ ℂ)
37	17, 21	readdcld 11165	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)) ∈ ℝ)
38	37	recnd 11164	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)) ∈ ℂ)
39	31, 33, 36, 38	addsubeq4d 11547	. . . . . . 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 257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0) + (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) + (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0))))
41	40	itgeq2dv 25759	. . . . 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 38012	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ 𝐿¹)
46	24	iblre 25771	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ 𝐿¹ ↔ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0)) ∈ 𝐿¹ ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0)) ∈ 𝐿¹)))
47	45, 46	mpbid 232	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0)) ∈ 𝐿¹ ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0)) ∈ 𝐿¹))
48	47	simprd 495	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0)) ∈ 𝐿¹)
49	1	iblre 25771	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿¹ ↔ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ 𝐿¹ ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ 𝐿¹)))
50	42, 49	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ 𝐿¹ ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ 𝐿¹))
51	50	simpld 494	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ 𝐿¹)
52	4	iblre 25771	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿¹ ↔ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐶, 𝐶, 0)) ∈ 𝐿¹ ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐶, -𝐶, 0)) ∈ 𝐿¹)))
53	43, 52	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐶, 𝐶, 0)) ∈ 𝐿¹ ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐶, -𝐶, 0)) ∈ 𝐿¹))
54	53	simpld 494	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐶, 𝐶, 0)) ∈ 𝐿¹)
55		iblmbf 25744	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿¹ → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
56	42, 55	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
57		iblmbf 25744	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿¹ → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)
58	43, 57	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)
59	56, 1, 58, 4, 44	mbfposadd 38002	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ∈ MblFn)
60	10, 51, 13, 54, 59	ibladdnc 38012	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) ∈ 𝐿¹)
61		max1 13128	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 0 ≤ if(0 ≤ 𝐵, 𝐵, 0))
62	8, 1, 61	sylancr 588	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝐵, 𝐵, 0))
63		max1 13128	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 0 ≤ if(0 ≤ 𝐶, 𝐶, 0))
64	8, 4, 63	sylancr 588	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝐶, 𝐶, 0))
65	10, 13, 62, 64	addge0d 11717	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
66	65	iftrued 4475	. . . . . . . . 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 7376	. . . . . . . 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 5179	. . . . . . 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 25627	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -(𝐵 + 𝐶)) ∈ MblFn)
70	1	recnd 11164	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)
71	4	recnd 11164	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)
72	70, 71	negdid 11509	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(𝐵 + 𝐶) = (-𝐵 + -𝐶))
73	72	oveq1d 7375	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-(𝐵 + 𝐶) + (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = ((-𝐵 + -𝐶) + (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
74	15	recnd 11164	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℂ)
75	19	recnd 11164	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐶 ∈ ℂ)
76	74, 75, 11, 14	add4d 11366	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((-𝐵 + -𝐶) + (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = ((-𝐵 + if(0 ≤ 𝐵, 𝐵, 0)) + (-𝐶 + if(0 ≤ 𝐶, 𝐶, 0))))
77		negeq 11376	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 = 0 → -𝐵 = -0)
78		neg0 11431	. . . . . . . . . . . . . . . 16 ⊢ -0 = 0
79	77, 78	eqtrdi 2788	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = 0 → -𝐵 = 0)
80		0le0 12273	. . . . . . . . . . . . . . . . 17 ⊢ 0 ≤ 0
81	80, 79	breqtrrid 5124	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 = 0 → 0 ≤ -𝐵)
82	81	iftrued 4475	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = 0 → if(0 ≤ -𝐵, -𝐵, 0) = -𝐵)
83		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 = 0 → 𝐵 = 0)
84	80, 83	breqtrrid 5124	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 = 0 → 0 ≤ 𝐵)
85	84	iftrued 4475	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 = 0 → if(0 ≤ 𝐵, 𝐵, 0) = 𝐵)
86	85, 83	eqtrd 2772	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 = 0 → if(0 ≤ 𝐵, 𝐵, 0) = 0)
87	79, 86	oveq12d 7378	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 = 0 → (-𝐵 + if(0 ≤ 𝐵, 𝐵, 0)) = (0 + 0))
88		00id 11312	. . . . . . . . . . . . . . . 16 ⊢ (0 + 0) = 0
89	87, 88	eqtrdi 2788	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = 0 → (-𝐵 + if(0 ≤ 𝐵, 𝐵, 0)) = 0)
90	79, 82, 89	3eqtr4rd 2783	. . . . . . . . . . . . . 14 ⊢ (𝐵 = 0 → (-𝐵 + if(0 ≤ 𝐵, 𝐵, 0)) = if(0 ≤ -𝐵, -𝐵, 0))
91	90	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 = 0) → (-𝐵 + if(0 ≤ 𝐵, 𝐵, 0)) = if(0 ≤ -𝐵, -𝐵, 0))
92		ovif2 7459	. . . . . . . . . . . . . 14 ⊢ (-𝐵 + if(0 ≤ 𝐵, 𝐵, 0)) = if(0 ≤ 𝐵, (-𝐵 + 𝐵), (-𝐵 + 0))
93	70	negne0bd 11489	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ≠ 0 ↔ -𝐵 ≠ 0))
94	93	biimpa 476	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → -𝐵 ≠ 0)
95	1	le0neg2d 11713	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐵 ↔ -𝐵 ≤ 0))
96		leloe 11223	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((-𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → (-𝐵 ≤ 0 ↔ (-𝐵 < 0 ∨ -𝐵 = 0)))
97	15, 8, 96	sylancl 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 ≤ 0 ↔ (-𝐵 < 0 ∨ -𝐵 = 0)))
98	95, 97	bitrd 279	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐵 ↔ (-𝐵 < 0 ∨ -𝐵 = 0)))
99		df-ne 2934	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (-𝐵 ≠ 0 ↔ ¬ -𝐵 = 0)
100		biorf 937	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ -𝐵 = 0 → (-𝐵 < 0 ↔ (-𝐵 = 0 ∨ -𝐵 < 0)))
101	99, 100	sylbi 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ (-𝐵 ≠ 0 → (-𝐵 < 0 ↔ (-𝐵 = 0 ∨ -𝐵 < 0)))
102		orcom 871	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((-𝐵 = 0 ∨ -𝐵 < 0) ↔ (-𝐵 < 0 ∨ -𝐵 = 0))
103	101, 102	bitr2di 288	. . . . . . . . . . . . . . . . . . 19 ⊢ (-𝐵 ≠ 0 → ((-𝐵 < 0 ∨ -𝐵 = 0) ↔ -𝐵 < 0))
104	98, 103	sylan9bb 509	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ -𝐵 ≠ 0) → (0 ≤ 𝐵 ↔ -𝐵 < 0))
105	94, 104	syldan 592	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (0 ≤ 𝐵 ↔ -𝐵 < 0))
106		ltnle 11216	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → (-𝐵 < 0 ↔ ¬ 0 ≤ -𝐵))
107	15, 8, 106	sylancl 587	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 < 0 ↔ ¬ 0 ≤ -𝐵))
108	107	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (-𝐵 < 0 ↔ ¬ 0 ≤ -𝐵))
109	105, 108	bitrd 279	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (0 ≤ 𝐵 ↔ ¬ 0 ≤ -𝐵))
110	74, 70	addcomd 11339	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 + 𝐵) = (𝐵 + -𝐵))
111	70	negidd 11486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 + -𝐵) = 0)
112	110, 111	eqtrd 2772	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 + 𝐵) = 0)
113	112	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (-𝐵 + 𝐵) = 0)
114	74	addridd 11337	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 + 0) = -𝐵)
115	114	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (-𝐵 + 0) = -𝐵)
116	109, 113, 115	ifbieq12d 4496	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → if(0 ≤ 𝐵, (-𝐵 + 𝐵), (-𝐵 + 0)) = if(¬ 0 ≤ -𝐵, 0, -𝐵))
117		ifnot 4520	. . . . . . . . . . . . . . 15 ⊢ if(¬ 0 ≤ -𝐵, 0, -𝐵) = if(0 ≤ -𝐵, -𝐵, 0)
118	116, 117	eqtrdi 2788	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → if(0 ≤ 𝐵, (-𝐵 + 𝐵), (-𝐵 + 0)) = if(0 ≤ -𝐵, -𝐵, 0))
119	92, 118	eqtrid 2784	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (-𝐵 + if(0 ≤ 𝐵, 𝐵, 0)) = if(0 ≤ -𝐵, -𝐵, 0))
120	91, 119	pm2.61dane 3020	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐵 + if(0 ≤ 𝐵, 𝐵, 0)) = if(0 ≤ -𝐵, -𝐵, 0))
121		negeq 11376	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 = 0 → -𝐶 = -0)
122	121, 78	eqtrdi 2788	. . . . . . . . . . . . . . 15 ⊢ (𝐶 = 0 → -𝐶 = 0)
123	80, 122	breqtrrid 5124	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 = 0 → 0 ≤ -𝐶)
124	123	iftrued 4475	. . . . . . . . . . . . . . 15 ⊢ (𝐶 = 0 → if(0 ≤ -𝐶, -𝐶, 0) = -𝐶)
125		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐶 = 0 → 𝐶 = 0)
126	80, 125	breqtrrid 5124	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 = 0 → 0 ≤ 𝐶)
127	126	iftrued 4475	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐶 = 0 → if(0 ≤ 𝐶, 𝐶, 0) = 𝐶)
128	127, 125	eqtrd 2772	. . . . . . . . . . . . . . . . 17 ⊢ (𝐶 = 0 → if(0 ≤ 𝐶, 𝐶, 0) = 0)
129	122, 128	oveq12d 7378	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 = 0 → (-𝐶 + if(0 ≤ 𝐶, 𝐶, 0)) = (0 + 0))
130	129, 88	eqtrdi 2788	. . . . . . . . . . . . . . 15 ⊢ (𝐶 = 0 → (-𝐶 + if(0 ≤ 𝐶, 𝐶, 0)) = 0)
131	122, 124, 130	3eqtr4rd 2783	. . . . . . . . . . . . . 14 ⊢ (𝐶 = 0 → (-𝐶 + if(0 ≤ 𝐶, 𝐶, 0)) = if(0 ≤ -𝐶, -𝐶, 0))
132	131	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 = 0) → (-𝐶 + if(0 ≤ 𝐶, 𝐶, 0)) = if(0 ≤ -𝐶, -𝐶, 0))
133		ovif2 7459	. . . . . . . . . . . . . 14 ⊢ (-𝐶 + if(0 ≤ 𝐶, 𝐶, 0)) = if(0 ≤ 𝐶, (-𝐶 + 𝐶), (-𝐶 + 0))
134	71	negne0bd 11489	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 ≠ 0 ↔ -𝐶 ≠ 0))
135	134	biimpa 476	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → -𝐶 ≠ 0)
136	4	le0neg2d 11713	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐶 ↔ -𝐶 ≤ 0))
137		leloe 11223	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((-𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → (-𝐶 ≤ 0 ↔ (-𝐶 < 0 ∨ -𝐶 = 0)))
138	19, 8, 137	sylancl 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐶 ≤ 0 ↔ (-𝐶 < 0 ∨ -𝐶 = 0)))
139	136, 138	bitrd 279	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ 𝐶 ↔ (-𝐶 < 0 ∨ -𝐶 = 0)))
140		df-ne 2934	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (-𝐶 ≠ 0 ↔ ¬ -𝐶 = 0)
141		biorf 937	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ -𝐶 = 0 → (-𝐶 < 0 ↔ (-𝐶 = 0 ∨ -𝐶 < 0)))
142	140, 141	sylbi 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ (-𝐶 ≠ 0 → (-𝐶 < 0 ↔ (-𝐶 = 0 ∨ -𝐶 < 0)))
143		orcom 871	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((-𝐶 = 0 ∨ -𝐶 < 0) ↔ (-𝐶 < 0 ∨ -𝐶 = 0))
144	142, 143	bitr2di 288	. . . . . . . . . . . . . . . . . . 19 ⊢ (-𝐶 ≠ 0 → ((-𝐶 < 0 ∨ -𝐶 = 0) ↔ -𝐶 < 0))
145	139, 144	sylan9bb 509	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ -𝐶 ≠ 0) → (0 ≤ 𝐶 ↔ -𝐶 < 0))
146	135, 145	syldan 592	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (0 ≤ 𝐶 ↔ -𝐶 < 0))
147		ltnle 11216	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → (-𝐶 < 0 ↔ ¬ 0 ≤ -𝐶))
148	19, 8, 147	sylancl 587	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐶 < 0 ↔ ¬ 0 ≤ -𝐶))
149	148	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (-𝐶 < 0 ↔ ¬ 0 ≤ -𝐶))
150	146, 149	bitrd 279	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (0 ≤ 𝐶 ↔ ¬ 0 ≤ -𝐶))
151	75, 71	addcomd 11339	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐶 + 𝐶) = (𝐶 + -𝐶))
152	71	negidd 11486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 + -𝐶) = 0)
153	151, 152	eqtrd 2772	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐶 + 𝐶) = 0)
154	153	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (-𝐶 + 𝐶) = 0)
155	75	addridd 11337	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐶 + 0) = -𝐶)
156	155	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (-𝐶 + 0) = -𝐶)
157	150, 154, 156	ifbieq12d 4496	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → if(0 ≤ 𝐶, (-𝐶 + 𝐶), (-𝐶 + 0)) = if(¬ 0 ≤ -𝐶, 0, -𝐶))
158		ifnot 4520	. . . . . . . . . . . . . . 15 ⊢ if(¬ 0 ≤ -𝐶, 0, -𝐶) = if(0 ≤ -𝐶, -𝐶, 0)
159	157, 158	eqtrdi 2788	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → if(0 ≤ 𝐶, (-𝐶 + 𝐶), (-𝐶 + 0)) = if(0 ≤ -𝐶, -𝐶, 0))
160	133, 159	eqtrid 2784	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (-𝐶 + if(0 ≤ 𝐶, 𝐶, 0)) = if(0 ≤ -𝐶, -𝐶, 0))
161	132, 160	pm2.61dane 3020	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-𝐶 + if(0 ≤ 𝐶, 𝐶, 0)) = if(0 ≤ -𝐶, -𝐶, 0))
162	120, 161	oveq12d 7378	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((-𝐵 + if(0 ≤ 𝐵, 𝐵, 0)) + (-𝐶 + if(0 ≤ 𝐶, 𝐶, 0))) = (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)))
163	73, 76, 162	3eqtrd 2776	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (-(𝐵 + 𝐶) + (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))) = (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)))
164	163	mpteq2dva 5179	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (-(𝐵 + 𝐶) + (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))) = (𝑥 ∈ 𝐴 ↦ (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0))))
165	1, 56	mbfneg 25627	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐵) ∈ MblFn)
166	4, 58	mbfneg 25627	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐶) ∈ MblFn)
167	72	mpteq2dva 5179	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -(𝐵 + 𝐶)) = (𝑥 ∈ 𝐴 ↦ (-𝐵 + -𝐶)))
168	167, 69	eqeltrrd 2838	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (-𝐵 + -𝐶)) ∈ MblFn)
169	165, 15, 166, 19, 168	mbfposadd 38002	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0))) ∈ MblFn)
170	164, 169	eqeltrd 2837	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (-(𝐵 + 𝐶) + (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))) ∈ MblFn)
171	69, 28, 59, 32, 170	mbfposadd 38002	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0) + if(0 ≤ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)), 0))) ∈ MblFn)
172	68, 171	eqeltrrd 2838	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0) + (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))) ∈ MblFn)
173		max1 13128	. . . . . . 7 ⊢ ((0 ∈ ℝ ∧ -(𝐵 + 𝐶) ∈ ℝ) → 0 ≤ if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0))
174	8, 28, 173	sylancr 588	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0))
175	30, 48, 32, 60, 172, 30, 32, 174, 65	itgaddnclem1 38013	. . . . 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 494	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0)) ∈ 𝐿¹)
177	50	simprd 495	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ 𝐿¹)
178	53	simprd 495	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐶, -𝐶, 0)) ∈ 𝐿¹)
179	17, 177, 21, 178, 169	ibladdnc 38012	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0))) ∈ 𝐿¹)
180		max1 13128	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ -𝐵 ∈ ℝ) → 0 ≤ if(0 ≤ -𝐵, -𝐵, 0))
181	8, 15, 180	sylancr 588	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ -𝐵, -𝐵, 0))
182		max1 13128	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ -𝐶 ∈ ℝ) → 0 ≤ if(0 ≤ -𝐶, -𝐶, 0))
183	8, 19, 182	sylancr 588	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ -𝐶, -𝐶, 0))
184	17, 21, 181, 183	addge0d 11717	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)))
185	184	iftrued 4475	. . . . . . . . 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 7376	. . . . . . . 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 5179	. . . . . . 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 11366	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐵 + 𝐶) + (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0))) = ((𝐵 + if(0 ≤ -𝐵, -𝐵, 0)) + (𝐶 + if(0 ≤ -𝐶, -𝐶, 0))))
189	82, 79	eqtrd 2772	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 = 0 → if(0 ≤ -𝐵, -𝐵, 0) = 0)
190	83, 189	oveq12d 7378	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 = 0 → (𝐵 + if(0 ≤ -𝐵, -𝐵, 0)) = (0 + 0))
191	190, 88	eqtrdi 2788	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = 0 → (𝐵 + if(0 ≤ -𝐵, -𝐵, 0)) = 0)
192	83, 85, 191	3eqtr4rd 2783	. . . . . . . . . . . . . 14 ⊢ (𝐵 = 0 → (𝐵 + if(0 ≤ -𝐵, -𝐵, 0)) = if(0 ≤ 𝐵, 𝐵, 0))
193	192	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 = 0) → (𝐵 + if(0 ≤ -𝐵, -𝐵, 0)) = if(0 ≤ 𝐵, 𝐵, 0))
194		ovif2 7459	. . . . . . . . . . . . . 14 ⊢ (𝐵 + if(0 ≤ -𝐵, -𝐵, 0)) = if(0 ≤ -𝐵, (𝐵 + -𝐵), (𝐵 + 0))
195	1	le0neg1d 11712	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ≤ 0 ↔ 0 ≤ -𝐵))
196		leloe 11223	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐵 ≤ 0 ↔ (𝐵 < 0 ∨ 𝐵 = 0)))
197	1, 8, 196	sylancl 587	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ≤ 0 ↔ (𝐵 < 0 ∨ 𝐵 = 0)))
198	195, 197	bitr3d 281	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ -𝐵 ↔ (𝐵 < 0 ∨ 𝐵 = 0)))
199		df-ne 2934	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 ≠ 0 ↔ ¬ 𝐵 = 0)
200		biorf 937	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝐵 = 0 → (𝐵 < 0 ↔ (𝐵 = 0 ∨ 𝐵 < 0)))
201	199, 200	sylbi 217	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ≠ 0 → (𝐵 < 0 ↔ (𝐵 = 0 ∨ 𝐵 < 0)))
202		orcom 871	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 = 0 ∨ 𝐵 < 0) ↔ (𝐵 < 0 ∨ 𝐵 = 0))
203	201, 202	bitr2di 288	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ≠ 0 → ((𝐵 < 0 ∨ 𝐵 = 0) ↔ 𝐵 < 0))
204	198, 203	sylan9bb 509	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (0 ≤ -𝐵 ↔ 𝐵 < 0))
205		ltnle 11216	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐵 < 0 ↔ ¬ 0 ≤ 𝐵))
206	1, 8, 205	sylancl 587	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 < 0 ↔ ¬ 0 ≤ 𝐵))
207	206	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (𝐵 < 0 ↔ ¬ 0 ≤ 𝐵))
208	204, 207	bitrd 279	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (0 ≤ -𝐵 ↔ ¬ 0 ≤ 𝐵))
209	111	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (𝐵 + -𝐵) = 0)
210	70	addridd 11337	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 + 0) = 𝐵)
211	210	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (𝐵 + 0) = 𝐵)
212	208, 209, 211	ifbieq12d 4496	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → if(0 ≤ -𝐵, (𝐵 + -𝐵), (𝐵 + 0)) = if(¬ 0 ≤ 𝐵, 0, 𝐵))
213		ifnot 4520	. . . . . . . . . . . . . . 15 ⊢ if(¬ 0 ≤ 𝐵, 0, 𝐵) = if(0 ≤ 𝐵, 𝐵, 0)
214	212, 213	eqtrdi 2788	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → if(0 ≤ -𝐵, (𝐵 + -𝐵), (𝐵 + 0)) = if(0 ≤ 𝐵, 𝐵, 0))
215	194, 214	eqtrid 2784	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ≠ 0) → (𝐵 + if(0 ≤ -𝐵, -𝐵, 0)) = if(0 ≤ 𝐵, 𝐵, 0))
216	193, 215	pm2.61dane 3020	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 + if(0 ≤ -𝐵, -𝐵, 0)) = if(0 ≤ 𝐵, 𝐵, 0))
217	124, 122	eqtrd 2772	. . . . . . . . . . . . . . . . 17 ⊢ (𝐶 = 0 → if(0 ≤ -𝐶, -𝐶, 0) = 0)
218	125, 217	oveq12d 7378	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 = 0 → (𝐶 + if(0 ≤ -𝐶, -𝐶, 0)) = (0 + 0))
219	218, 88	eqtrdi 2788	. . . . . . . . . . . . . . 15 ⊢ (𝐶 = 0 → (𝐶 + if(0 ≤ -𝐶, -𝐶, 0)) = 0)
220	125, 127, 219	3eqtr4rd 2783	. . . . . . . . . . . . . 14 ⊢ (𝐶 = 0 → (𝐶 + if(0 ≤ -𝐶, -𝐶, 0)) = if(0 ≤ 𝐶, 𝐶, 0))
221	220	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 = 0) → (𝐶 + if(0 ≤ -𝐶, -𝐶, 0)) = if(0 ≤ 𝐶, 𝐶, 0))
222		ovif2 7459	. . . . . . . . . . . . . 14 ⊢ (𝐶 + if(0 ≤ -𝐶, -𝐶, 0)) = if(0 ≤ -𝐶, (𝐶 + -𝐶), (𝐶 + 0))
223	4	le0neg1d 11712	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 ≤ 0 ↔ 0 ≤ -𝐶))
224		leloe 11223	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐶 ≤ 0 ↔ (𝐶 < 0 ∨ 𝐶 = 0)))
225	4, 8, 224	sylancl 587	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 ≤ 0 ↔ (𝐶 < 0 ∨ 𝐶 = 0)))
226	223, 225	bitr3d 281	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0 ≤ -𝐶 ↔ (𝐶 < 0 ∨ 𝐶 = 0)))
227		df-ne 2934	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐶 ≠ 0 ↔ ¬ 𝐶 = 0)
228		biorf 937	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝐶 = 0 → (𝐶 < 0 ↔ (𝐶 = 0 ∨ 𝐶 < 0)))
229	227, 228	sylbi 217	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 ≠ 0 → (𝐶 < 0 ↔ (𝐶 = 0 ∨ 𝐶 < 0)))
230		orcom 871	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 = 0 ∨ 𝐶 < 0) ↔ (𝐶 < 0 ∨ 𝐶 = 0))
231	229, 230	bitr2di 288	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐶 ≠ 0 → ((𝐶 < 0 ∨ 𝐶 = 0) ↔ 𝐶 < 0))
232	226, 231	sylan9bb 509	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (0 ≤ -𝐶 ↔ 𝐶 < 0))
233		ltnle 11216	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐶 < 0 ↔ ¬ 0 ≤ 𝐶))
234	4, 8, 233	sylancl 587	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 < 0 ↔ ¬ 0 ≤ 𝐶))
235	234	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (𝐶 < 0 ↔ ¬ 0 ≤ 𝐶))
236	232, 235	bitrd 279	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (0 ≤ -𝐶 ↔ ¬ 0 ≤ 𝐶))
237	152	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (𝐶 + -𝐶) = 0)
238	71	addridd 11337	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 + 0) = 𝐶)
239	238	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (𝐶 + 0) = 𝐶)
240	236, 237, 239	ifbieq12d 4496	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → if(0 ≤ -𝐶, (𝐶 + -𝐶), (𝐶 + 0)) = if(¬ 0 ≤ 𝐶, 0, 𝐶))
241		ifnot 4520	. . . . . . . . . . . . . . 15 ⊢ if(¬ 0 ≤ 𝐶, 0, 𝐶) = if(0 ≤ 𝐶, 𝐶, 0)
242	240, 241	eqtrdi 2788	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → if(0 ≤ -𝐶, (𝐶 + -𝐶), (𝐶 + 0)) = if(0 ≤ 𝐶, 𝐶, 0))
243	222, 242	eqtrid 2784	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≠ 0) → (𝐶 + if(0 ≤ -𝐶, -𝐶, 0)) = if(0 ≤ 𝐶, 𝐶, 0))
244	221, 243	pm2.61dane 3020	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 + if(0 ≤ -𝐶, -𝐶, 0)) = if(0 ≤ 𝐶, 𝐶, 0))
245	216, 244	oveq12d 7378	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐵 + if(0 ≤ -𝐵, -𝐵, 0)) + (𝐶 + if(0 ≤ -𝐶, -𝐶, 0))) = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
246	188, 245	eqtrd 2772	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐵 + 𝐶) + (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0))) = (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)))
247	246	mpteq2dva 5179	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((𝐵 + 𝐶) + (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)))) = (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0))))
248	247, 59	eqeltrd 2837	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((𝐵 + 𝐶) + (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)))) ∈ MblFn)
249	44, 24, 169, 37, 248	mbfposadd 38002	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) + if(0 ≤ (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)), (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)), 0))) ∈ MblFn)
250	187, 249	eqeltrrd 2838	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) + (if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)))) ∈ MblFn)
251		max1 13128	. . . . . . 7 ⊢ ((0 ∈ ℝ ∧ (𝐵 + 𝐶) ∈ ℝ) → 0 ≤ if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0))
252	8, 24, 251	sylancr 588	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0))
253	35, 176, 37, 179, 250, 35, 37, 252, 184	itgaddnclem1 38013	. . . . 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 2780	. . . 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 25761	. . . . 5 ⊢ (𝜑 → ∫𝐴if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0) d𝑥 ∈ ℂ)
256	10, 51, 13, 54, 59, 10, 13, 62, 64	itgaddnclem1 38013	. . . . . 6 ⊢ (𝜑 → ∫𝐴(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) d𝑥 = (∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 + ∫𝐴if(0 ≤ 𝐶, 𝐶, 0) d𝑥))
257	10, 51	itgcl 25761	. . . . . . 7 ⊢ (𝜑 → ∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 ∈ ℂ)
258	13, 54	itgcl 25761	. . . . . . 7 ⊢ (𝜑 → ∫𝐴if(0 ≤ 𝐶, 𝐶, 0) d𝑥 ∈ ℂ)
259	257, 258	addcld 11155	. . . . . 6 ⊢ (𝜑 → (∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 + ∫𝐴if(0 ≤ 𝐶, 𝐶, 0) d𝑥) ∈ ℂ)
260	256, 259	eqeltrd 2837	. . . . 5 ⊢ (𝜑 → ∫𝐴(if(0 ≤ 𝐵, 𝐵, 0) + if(0 ≤ 𝐶, 𝐶, 0)) d𝑥 ∈ ℂ)
261	35, 176	itgcl 25761	. . . . 5 ⊢ (𝜑 → ∫𝐴if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) d𝑥 ∈ ℂ)
262	17, 177, 21, 178, 169, 17, 21, 181, 183	itgaddnclem1 38013	. . . . . 6 ⊢ (𝜑 → ∫𝐴(if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)) d𝑥 = (∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥 + ∫𝐴if(0 ≤ -𝐶, -𝐶, 0) d𝑥))
263	17, 177	itgcl 25761	. . . . . . 7 ⊢ (𝜑 → ∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥 ∈ ℂ)
264	21, 178	itgcl 25761	. . . . . . 7 ⊢ (𝜑 → ∫𝐴if(0 ≤ -𝐶, -𝐶, 0) d𝑥 ∈ ℂ)
265	263, 264	addcld 11155	. . . . . 6 ⊢ (𝜑 → (∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥 + ∫𝐴if(0 ≤ -𝐶, -𝐶, 0) d𝑥) ∈ ℂ)
266	262, 265	eqeltrd 2837	. . . . 5 ⊢ (𝜑 → ∫𝐴(if(0 ≤ -𝐵, -𝐵, 0) + if(0 ≤ -𝐶, -𝐶, 0)) d𝑥 ∈ ℂ)
267	255, 260, 261, 266	addsubeq4d 11547	. . . 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 232	. . 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 7378	. . 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 11543	. . 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 2776	. 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 25774	. 2 ⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴if(0 ≤ (𝐵 + 𝐶), (𝐵 + 𝐶), 0) d𝑥 − ∫𝐴if(0 ≤ -(𝐵 + 𝐶), -(𝐵 + 𝐶), 0) d𝑥))
273	1, 42	itgreval 25774	. . 3 ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = (∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 − ∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥))
274	4, 43	itgreval 25774	. . 3 ⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = (∫𝐴if(0 ≤ 𝐶, 𝐶, 0) d𝑥 − ∫𝐴if(0 ≤ -𝐶, -𝐶, 0) d𝑥))
275	273, 274	oveq12d 7378	. 2 ⊢ (𝜑 → (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥) = ((∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 − ∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥) + (∫𝐴if(0 ≤ 𝐶, 𝐶, 0) d𝑥 − ∫𝐴if(0 ≤ -𝐶, -𝐶, 0) d𝑥)))
276	271, 272, 275	3eqtr4d 2782	1 ⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ifcif 4467 class class class wbr 5086 ↦ cmpt 5167 (class class class)co 7360 ℂcc 11027 ℝcr 11028 0cc0 11029 + caddc 11032 < clt 11170 ≤ cle 11171 − cmin 11368 -cneg 11369 MblFncmbf 25591 𝐿¹cibl 25594 ∫citg 25595

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5302 ax-pr 5370 ax-un 7682 ax-inf2 9553 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106 ax-pre-sup 11107 ax-addf 11108

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-disj 5054 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-se 5578 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-of 7624 df-ofr 7625 df-om 7811 df-1st 7935 df-2nd 7936 df-frecs 8224 df-wrecs 8255 df-recs 8304 df-rdg 8342 df-1o 8398 df-2o 8399 df-er 8636 df-map 8768 df-pm 8769 df-en 8887 df-dom 8888 df-sdom 8889 df-fin 8890 df-fi 9317 df-sup 9348 df-inf 9349 df-oi 9418 df-dju 9816 df-card 9854 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-nn 12166 df-2 12235 df-3 12236 df-4 12237 df-n0 12429 df-z 12516 df-uz 12780 df-q 12890 df-rp 12934 df-xneg 13054 df-xadd 13055 df-xmul 13056 df-ioo 13293 df-ico 13295 df-icc 13296 df-fz 13453 df-fzo 13600 df-fl 13742 df-mod 13820 df-seq 13955 df-exp 14015 df-hash 14284 df-cj 15052 df-re 15053 df-im 15054 df-sqrt 15188 df-abs 15189 df-clim 15441 df-sum 15640 df-rest 17376 df-topgen 17397 df-psmet 21336 df-xmet 21337 df-met 21338 df-bl 21339 df-mopn 21340 df-top 22869 df-topon 22886 df-bases 22921 df-cmp 23362 df-ovol 25441 df-vol 25442 df-mbf 25596 df-itg1 25597 df-itg2 25598 df-ibl 25599 df-itg 25600 df-0p 25647

This theorem is referenced by: itgaddnc 38015

W3C validator