This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑥 )