Metamath Proof Explorer

Theorem itgmulc2lem2

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

Ref Expression
Hypotheses itgmulc2.1 ⊢ φ → C ∈ ℂ
itgmulc2.2 ⊢ φ ∧ x ∈ A → B ∈ V
itgmulc2.3 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
itgmulc2.4 ⊢ φ → C ∈ ℝ
itgmulc2.5 ⊢ φ ∧ x ∈ A → B ∈ ℝ
Assertion itgmulc2lem2 ⊢ φ → C ⁢ ∫ A B dx = ∫ A C ⁢ B dx

Proof

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