Theorem itgmulc2lem2

Description: Lemma for itgmulc2 : real case. (Contributed by Mario Carneiro, 25-Aug-2014)

	Ref	Expression
Hypotheses	itgmulc2.1	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	itgmulc2.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
	itgmulc2.3	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
	itgmulc2.4	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	itgmulc2.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
Assertion	itgmulc2lem2	⊢ ( 𝜑 → ( 𝐶 · ∫ 𝐴 𝐵 d 𝑥 ) = ∫ 𝐴 ( 𝐶 · 𝐵 ) d 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		itgmulc2.1	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
2		itgmulc2.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
3		itgmulc2.3	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
4		itgmulc2.4	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
5		itgmulc2.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
6	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
7		max0sub	⊢ ( 𝐶 ∈ ℝ → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) − if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) = 𝐶 )
8	6 7	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) − if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) = 𝐶 )
9	8	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) − if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) · 𝐵 ) = ( 𝐶 · 𝐵 ) )
10		0re	⊢ 0 ∈ ℝ
11		ifcl	⊢ ( ( 𝐶 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℝ )
12	4 10 11	sylancl	⊢ ( 𝜑 → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℝ )
13	12	recnd	⊢ ( 𝜑 → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℂ )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℂ )
15	4	renegcld	⊢ ( 𝜑 → - 𝐶 ∈ ℝ )
16		ifcl	⊢ ( ( - 𝐶 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ∈ ℝ )
17	15 10 16	sylancl	⊢ ( 𝜑 → if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ∈ ℝ )
18	17	recnd	⊢ ( 𝜑 → if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ∈ ℂ )
19	18	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ∈ ℂ )
20	5	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
21	14 19 20	subdird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) − if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) · 𝐵 ) = ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) ) )
22	9 21	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 · 𝐵 ) = ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) ) )
23	22	itgeq2dv	⊢ ( 𝜑 → ∫ 𝐴 ( 𝐶 · 𝐵 ) d 𝑥 = ∫ 𝐴 ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) ) d 𝑥 )
24	12	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℝ )
25	24 5	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) ∈ ℝ )
26	13 2 3	iblmulc2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) ) ∈ 𝐿1 )
27	17	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ∈ ℝ )
28	27 5	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) ∈ ℝ )
29	18 2 3	iblmulc2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) ) ∈ 𝐿1 )
30	25 26 28 29	itgsub	⊢ ( 𝜑 → ∫ 𝐴 ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) ) d 𝑥 = ( ∫ 𝐴 ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) d 𝑥 − ∫ 𝐴 ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) d 𝑥 ) )
31		ifcl	⊢ ( ( 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ )
32	5 10 31	sylancl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ )
33	24 32	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ ℝ )
34	5	iblre	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ 𝐿1 ) ) )
35	3 34	mpbid	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ 𝐿1 ) )
36	35	simpld	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ 𝐿1 )
37	13 32 36	iblmulc2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ) ∈ 𝐿1 )
38	5	renegcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 ∈ ℝ )
39		ifcl	⊢ ( ( - 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ℝ )
40	38 10 39	sylancl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ℝ )
41	24 40	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ ℝ )
42	35	simprd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ 𝐿1 )
43	13 40 42	iblmulc2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) ∈ 𝐿1 )
44	33 37 41 43	itgsub	⊢ ( 𝜑 → ∫ 𝐴 ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) − ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) d 𝑥 = ( ∫ 𝐴 ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) d 𝑥 − ∫ 𝐴 ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) d 𝑥 ) )
45		max0sub	⊢ ( 𝐵 ∈ ℝ → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) − if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) = 𝐵 )
46	5 45	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) − if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) = 𝐵 )
47	46	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) − if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) = ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) )
48	32	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℂ )
49	40	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ℂ )
50	14 48 49	subdid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) − if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) = ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) − ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) )
51	47 50	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) = ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) − ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) )
52	51	itgeq2dv	⊢ ( 𝜑 → ∫ 𝐴 ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) d 𝑥 = ∫ 𝐴 ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) − ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) d 𝑥 )
53	5 3	itgreval	⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = ( ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 − ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 ) )
54	53	oveq2d	⊢ ( 𝜑 → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · ( ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 − ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 ) ) )
55	32 36	itgcl	⊢ ( 𝜑 → ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 ∈ ℂ )
56	40 42	itgcl	⊢ ( 𝜑 → ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 ∈ ℂ )
57	13 55 56	subdid	⊢ ( 𝜑 → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · ( ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 − ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 ) ) = ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 ) − ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 ) ) )
58		max1	⊢ ( ( 0 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 0 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
59	10 4 58	sylancr	⊢ ( 𝜑 → 0 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
60		max1	⊢ ( ( 0 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 0 ≤ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
61	10 5 60	sylancr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
62	13 32 36 12 32 59 61	itgmulc2lem1	⊢ ( 𝜑 → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 ) = ∫ 𝐴 ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) d 𝑥 )
63		max1	⊢ ( ( 0 ∈ ℝ ∧ - 𝐵 ∈ ℝ ) → 0 ≤ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) )
64	10 38 63	sylancr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) )
65	13 40 42 12 40 59 64	itgmulc2lem1	⊢ ( 𝜑 → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 ) = ∫ 𝐴 ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) d 𝑥 )
66	62 65	oveq12d	⊢ ( 𝜑 → ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 ) − ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 ) ) = ( ∫ 𝐴 ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) d 𝑥 − ∫ 𝐴 ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) d 𝑥 ) )
67	54 57 66	3eqtrd	⊢ ( 𝜑 → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ∫ 𝐴 ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) d 𝑥 − ∫ 𝐴 ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) d 𝑥 ) )
68	44 52 67	3eqtr4d	⊢ ( 𝜑 → ∫ 𝐴 ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) d 𝑥 = ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · ∫ 𝐴 𝐵 d 𝑥 ) )
69	27 32	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ ℝ )
70	18 32 36	iblmulc2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ) ∈ 𝐿1 )
71	27 40	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ ℝ )
72	18 40 42	iblmulc2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) ∈ 𝐿1 )
73	69 70 71 72	itgsub	⊢ ( 𝜑 → ∫ 𝐴 ( ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) d 𝑥 = ( ∫ 𝐴 ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) d 𝑥 − ∫ 𝐴 ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) d 𝑥 ) )
74	46	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) − if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) = ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) )
75	19 48 49	subdid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) − if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) = ( ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) )
76	74 75	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) = ( ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) )
77	76	itgeq2dv	⊢ ( 𝜑 → ∫ 𝐴 ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) d 𝑥 = ∫ 𝐴 ( ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) d 𝑥 )
78	53	oveq2d	⊢ ( 𝜑 → ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · ( ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 − ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 ) ) )
79	18 55 56	subdid	⊢ ( 𝜑 → ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · ( ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 − ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 ) ) = ( ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 ) ) )
80		max1	⊢ ( ( 0 ∈ ℝ ∧ - 𝐶 ∈ ℝ ) → 0 ≤ if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) )
81	10 15 80	sylancr	⊢ ( 𝜑 → 0 ≤ if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) )
82	18 32 36 17 32 81 61	itgmulc2lem1	⊢ ( 𝜑 → ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 ) = ∫ 𝐴 ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) d 𝑥 )
83	18 40 42 17 40 81 64	itgmulc2lem1	⊢ ( 𝜑 → ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 ) = ∫ 𝐴 ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) d 𝑥 )
84	82 83	oveq12d	⊢ ( 𝜑 → ( ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 ) ) = ( ∫ 𝐴 ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) d 𝑥 − ∫ 𝐴 ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) d 𝑥 ) )
85	78 79 84	3eqtrd	⊢ ( 𝜑 → ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ∫ 𝐴 ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) d 𝑥 − ∫ 𝐴 ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) d 𝑥 ) )
86	73 77 85	3eqtr4d	⊢ ( 𝜑 → ∫ 𝐴 ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) d 𝑥 = ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · ∫ 𝐴 𝐵 d 𝑥 ) )
87	68 86	oveq12d	⊢ ( 𝜑 → ( ∫ 𝐴 ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) d 𝑥 − ∫ 𝐴 ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) d 𝑥 ) = ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · ∫ 𝐴 𝐵 d 𝑥 ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · ∫ 𝐴 𝐵 d 𝑥 ) ) )
88	2 3	itgcl	⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 ∈ ℂ )
89	13 18 88	subdird	⊢ ( 𝜑 → ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) − if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · ∫ 𝐴 𝐵 d 𝑥 ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · ∫ 𝐴 𝐵 d 𝑥 ) ) )
90	4 7	syl	⊢ ( 𝜑 → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) − if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) = 𝐶 )
91	90	oveq1d	⊢ ( 𝜑 → ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) − if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( 𝐶 · ∫ 𝐴 𝐵 d 𝑥 ) )
92	87 89 91	3eqtr2d	⊢ ( 𝜑 → ( ∫ 𝐴 ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) d 𝑥 − ∫ 𝐴 ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) d 𝑥 ) = ( 𝐶 · ∫ 𝐴 𝐵 d 𝑥 ) )
93	23 30 92	3eqtrrd	⊢ ( 𝜑 → ( 𝐶 · ∫ 𝐴 𝐵 d 𝑥 ) = ∫ 𝐴 ( 𝐶 · 𝐵 ) d 𝑥 )