Metamath Proof Explorer

Theorem itgmulc2nclem2

Description: Lemma for itgmulc2nc ; cf. itgmulc2lem2 . (Contributed by Brendan Leahy, 19-Nov-2017)

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

Proof

Step Hyp Ref Expression
1 itgmulc2nc.1 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
2 itgmulc2nc.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
3 itgmulc2nc.3 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
4 itgmulc2nc.m ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ MblFn )
5 itgmulc2nc.4 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
6 itgmulc2nc.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
7 max0sub ⊢ ( 𝐶 ∈ ℝ → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) − if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) = 𝐶 )
8 5 7 syl ⊢ ( 𝜑 → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) − if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) = 𝐶 )
9 8 oveq1d ⊢ ( 𝜑 → ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) − if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) · 𝐵 ) = ( 𝐶 · 𝐵 ) )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) − if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) · 𝐵 ) = ( 𝐶 · 𝐵 ) )
11 0re ⊢ 0 ∈ ℝ
12 ifcl ⊢ ( ( 𝐶 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℝ )
13 5 11 12 sylancl ⊢ ( 𝜑 → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℝ )
14 13 recnd ⊢ ( 𝜑 → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℂ )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℂ )
16 5 renegcld ⊢ ( 𝜑 → - 𝐶 ∈ ℝ )
17 ifcl ⊢ ( ( - 𝐶 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ∈ ℝ )
18 16 11 17 sylancl ⊢ ( 𝜑 → if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ∈ ℝ )
19 18 recnd ⊢ ( 𝜑 → if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ∈ ℂ )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ∈ ℂ )
21 6 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
22 15 20 21 subdird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) − if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) · 𝐵 ) = ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) ) )
23 10 22 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 · 𝐵 ) = ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) ) )
24 23 itgeq2dv ⊢ ( 𝜑 → ∫ 𝐴 ( 𝐶 · 𝐵 ) d 𝑥 = ∫ 𝐴 ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) ) d 𝑥 )
25 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) ∈ V )
26 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 · 𝐵 ) ∈ V )
27 4 26 mbfdm2 ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
28 13 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ∈ ℝ )
29 fconstmpt ⊢ ( 𝐴 × { if ( 0 ≤ 𝐶 , 𝐶 , 0 ) } ) = ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
30 29 a1i ⊢ ( 𝜑 → ( 𝐴 × { if ( 0 ≤ 𝐶 , 𝐶 , 0 ) } ) = ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) ) )
31 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
32 27 28 6 30 31 offval2 ⊢ ( 𝜑 → ( ( 𝐴 × { if ( 0 ≤ 𝐶 , 𝐶 , 0 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) ) )
33 iblmbf ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
34 3 33 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
35 21 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
36 34 13 35 mbfmulc2re ⊢ ( 𝜑 → ( ( 𝐴 × { if ( 0 ≤ 𝐶 , 𝐶 , 0 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ MblFn )
37 32 36 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) ) ∈ MblFn )
38 14 6 3 37 iblmulc2nc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) ) ∈ 𝐿1 )
39 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) ∈ V )
40 18 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ∈ ℝ )
41 fconstmpt ⊢ ( 𝐴 × { if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) } ) = ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) )
42 41 a1i ⊢ ( 𝜑 → ( 𝐴 × { if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) } ) = ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) )
43 27 40 6 42 31 offval2 ⊢ ( 𝜑 → ( ( 𝐴 × { if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) ) )
44 34 18 35 mbfmulc2re ⊢ ( 𝜑 → ( ( 𝐴 × { if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ MblFn )
45 43 44 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) ) ∈ MblFn )
46 19 6 3 45 iblmulc2nc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) ) ∈ 𝐿1 )
47 23 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) ) ) )
48 47 4 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) ) ) ∈ MblFn )
49 25 38 39 46 48 itgsubnc ⊢ ( 𝜑 → ∫ 𝐴 ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) ) d 𝑥 = ( ∫ 𝐴 ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) d 𝑥 − ∫ 𝐴 ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) d 𝑥 ) )
50 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ V )
51 ifcl ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ )
52 6 11 51 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℝ )
53 6 iblre ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ 𝐿1 ) ) )
54 3 53 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ 𝐿1 ) )
55 54 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ 𝐿1 )
56 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) )
57 27 28 52 30 56 offval2 ⊢ ( 𝜑 → ( ( 𝐴 × { if ( 0 ≤ 𝐶 , 𝐶 , 0 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ) )
58 6 34 mbfpos ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ MblFn )
59 52 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ∈ ℂ )
60 59 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) : 𝐴 ⟶ ℂ )
61 58 13 60 mbfmulc2re ⊢ ( 𝜑 → ( ( 𝐴 × { if ( 0 ≤ 𝐶 , 𝐶 , 0 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ) ∈ MblFn )
62 57 61 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ) ∈ MblFn )
63 14 52 55 62 iblmulc2nc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ) ∈ 𝐿1 )
64 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ V )
65 6 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 ∈ ℝ )
66 ifcl ⊢ ( ( - 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ℝ )
67 65 11 66 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ℝ )
68 54 simprd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ 𝐿1 )
69 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) )
70 27 28 67 30 69 offval2 ⊢ ( 𝜑 → ( ( 𝐴 × { if ( 0 ≤ 𝐶 , 𝐶 , 0 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) )
71 6 34 mbfneg ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ∈ MblFn )
72 65 71 mbfpos ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ MblFn )
73 67 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ∈ ℂ )
74 73 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) : 𝐴 ⟶ ℂ )
75 72 13 74 mbfmulc2re ⊢ ( 𝜑 → ( ( 𝐴 × { if ( 0 ≤ 𝐶 , 𝐶 , 0 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) ∈ MblFn )
76 70 75 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) ∈ MblFn )
77 14 67 68 76 iblmulc2nc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) ∈ 𝐿1 )
78 max0sub ⊢ ( 𝐵 ∈ ℝ → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) − if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) = 𝐵 )
79 6 78 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) − if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) = 𝐵 )
80 79 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) − if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) = ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) )
81 15 59 73 subdid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) − if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) = ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) − ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) )
82 80 81 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) = ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) − ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) )
83 82 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) − ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) ) )
84 32 83 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 × { if ( 0 ≤ 𝐶 , 𝐶 , 0 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) − ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) ) )
85 84 36 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) − ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) ) ∈ MblFn )
86 50 63 64 77 85 itgsubnc ⊢ ( 𝜑 → ∫ 𝐴 ( ( 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 𝑥 ) )
87 82 itgeq2dv ⊢ ( 𝜑 → ∫ 𝐴 ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) d 𝑥 = ∫ 𝐴 ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) − ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) d 𝑥 )
88 6 3 itgreval ⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = ( ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 − ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 ) )
89 88 oveq2d ⊢ ( 𝜑 → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · ( ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 − ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 ) ) )
90 52 55 itgcl ⊢ ( 𝜑 → ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 ∈ ℂ )
91 67 68 itgcl ⊢ ( 𝜑 → ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 ∈ ℂ )
92 14 90 91 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 𝑥 ) ) )
93 max1 ⊢ ( ( 0 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 0 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
94 11 5 93 sylancr ⊢ ( 𝜑 → 0 ≤ if ( 0 ≤ 𝐶 , 𝐶 , 0 ) )
95 max1 ⊢ ( ( 0 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 0 ≤ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
96 11 6 95 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) )
97 14 52 55 62 13 52 94 96 itgmulc2nclem1 ⊢ ( 𝜑 → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 ) = ∫ 𝐴 ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) d 𝑥 )
98 max1 ⊢ ( ( 0 ∈ ℝ ∧ - 𝐵 ∈ ℝ ) → 0 ≤ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) )
99 11 65 98 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) )
100 14 67 68 76 13 67 94 99 itgmulc2nclem1 ⊢ ( 𝜑 → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 ) = ∫ 𝐴 ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) d 𝑥 )
101 97 100 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 𝑥 ) )
102 89 92 101 3eqtrd ⊢ ( 𝜑 → ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ∫ 𝐴 ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) d 𝑥 − ∫ 𝐴 ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) d 𝑥 ) )
103 86 87 102 3eqtr4d ⊢ ( 𝜑 → ∫ 𝐴 ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) d 𝑥 = ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · ∫ 𝐴 𝐵 d 𝑥 ) )
104 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ∈ V )
105 27 40 52 42 56 offval2 ⊢ ( 𝜑 → ( ( 𝐴 × { if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ) )
106 58 18 60 mbfmulc2re ⊢ ( 𝜑 → ( ( 𝐴 × { if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ) ∈ MblFn )
107 105 106 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ) ∈ MblFn )
108 19 52 55 107 iblmulc2nc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) ) ∈ 𝐿1 )
109 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ∈ V )
110 27 40 67 42 69 offval2 ⊢ ( 𝜑 → ( ( 𝐴 × { if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) )
111 72 18 74 mbfmulc2re ⊢ ( 𝜑 → ( ( 𝐴 × { if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) ∈ MblFn )
112 110 111 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) ∈ MblFn )
113 19 67 68 112 iblmulc2nc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) ∈ 𝐿1 )
114 79 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) − if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) = ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) )
115 20 59 73 subdid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · ( if ( 0 ≤ 𝐵 , 𝐵 , 0 ) − if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) = ( ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) )
116 114 115 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) = ( ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) )
117 116 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) ) )
118 43 117 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 × { if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) ) )
119 118 44 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) ) ∈ MblFn )
120 104 108 109 113 119 itgsubnc ⊢ ( 𝜑 → ∫ 𝐴 ( ( 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 𝑥 ) )
121 116 itgeq2dv ⊢ ( 𝜑 → ∫ 𝐴 ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) d 𝑥 = ∫ 𝐴 ( ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) ) d 𝑥 )
122 88 oveq2d ⊢ ( 𝜑 → ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · ( ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 − ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 ) ) )
123 19 90 91 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 𝑥 ) ) )
124 max1 ⊢ ( ( 0 ∈ ℝ ∧ - 𝐶 ∈ ℝ ) → 0 ≤ if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) )
125 11 16 124 sylancr ⊢ ( 𝜑 → 0 ≤ if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) )
126 19 52 55 107 18 52 125 96 itgmulc2nclem1 ⊢ ( 𝜑 → ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · ∫ 𝐴 if ( 0 ≤ 𝐵 , 𝐵 , 0 ) d 𝑥 ) = ∫ 𝐴 ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) d 𝑥 )
127 19 67 68 112 18 67 125 99 itgmulc2nclem1 ⊢ ( 𝜑 → ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · ∫ 𝐴 if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) d 𝑥 ) = ∫ 𝐴 ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) d 𝑥 )
128 126 127 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 𝑥 ) )
129 122 123 128 3eqtrd ⊢ ( 𝜑 → ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ∫ 𝐴 ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ 𝐵 , 𝐵 , 0 ) ) d 𝑥 − ∫ 𝐴 ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · if ( 0 ≤ - 𝐵 , - 𝐵 , 0 ) ) d 𝑥 ) )
130 120 121 129 3eqtr4d ⊢ ( 𝜑 → ∫ 𝐴 ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) d 𝑥 = ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · ∫ 𝐴 𝐵 d 𝑥 ) )
131 103 130 oveq12d ⊢ ( 𝜑 → ( ∫ 𝐴 ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) d 𝑥 − ∫ 𝐴 ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) d 𝑥 ) = ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · ∫ 𝐴 𝐵 d 𝑥 ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · ∫ 𝐴 𝐵 d 𝑥 ) ) )
132 6 3 itgcl ⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 ∈ ℂ )
133 14 19 132 subdird ⊢ ( 𝜑 → ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) − if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · ∫ 𝐴 𝐵 d 𝑥 ) − ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · ∫ 𝐴 𝐵 d 𝑥 ) ) )
134 8 oveq1d ⊢ ( 𝜑 → ( ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) − if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( 𝐶 · ∫ 𝐴 𝐵 d 𝑥 ) )
135 131 133 134 3eqtr2d ⊢ ( 𝜑 → ( ∫ 𝐴 ( if ( 0 ≤ 𝐶 , 𝐶 , 0 ) · 𝐵 ) d 𝑥 − ∫ 𝐴 ( if ( 0 ≤ - 𝐶 , - 𝐶 , 0 ) · 𝐵 ) d 𝑥 ) = ( 𝐶 · ∫ 𝐴 𝐵 d 𝑥 ) )
136 24 49 135 3eqtrrd ⊢ ( 𝜑 → ( 𝐶 · ∫ 𝐴 𝐵 d 𝑥 ) = ∫ 𝐴 ( 𝐶 · 𝐵 ) d 𝑥 )