Proof of Theorem itgmulc2nclem2
Step | Hyp | Ref
| Expression |
1 | | itgmulc2nc.4 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℝ) |
2 | | max0sub 11901 |
. . . . . . 7
⊢ (𝐶 ∈ ℝ → (if(0
≤ 𝐶, 𝐶, 0) − if(0 ≤ -𝐶, -𝐶, 0)) = 𝐶) |
3 | 1, 2 | syl 17 |
. . . . . 6
⊢ (𝜑 → (if(0 ≤ 𝐶, 𝐶, 0) − if(0 ≤ -𝐶, -𝐶, 0)) = 𝐶) |
4 | 3 | oveq1d 6564 |
. . . . 5
⊢ (𝜑 → ((if(0 ≤ 𝐶, 𝐶, 0) − if(0 ≤ -𝐶, -𝐶, 0)) · 𝐵) = (𝐶 · 𝐵)) |
5 | 4 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((if(0 ≤ 𝐶, 𝐶, 0) − if(0 ≤ -𝐶, -𝐶, 0)) · 𝐵) = (𝐶 · 𝐵)) |
6 | | 0re 9919 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
7 | | ifcl 4080 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ) |
8 | 1, 6, 7 | sylancl 693 |
. . . . . . 7
⊢ (𝜑 → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ) |
9 | 8 | recnd 9947 |
. . . . . 6
⊢ (𝜑 → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℂ) |
10 | 9 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℂ) |
11 | 1 | renegcld 10336 |
. . . . . . . 8
⊢ (𝜑 → -𝐶 ∈ ℝ) |
12 | | ifcl 4080 |
. . . . . . . 8
⊢ ((-𝐶 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ -𝐶, -𝐶, 0) ∈ ℝ) |
13 | 11, 6, 12 | sylancl 693 |
. . . . . . 7
⊢ (𝜑 → if(0 ≤ -𝐶, -𝐶, 0) ∈ ℝ) |
14 | 13 | recnd 9947 |
. . . . . 6
⊢ (𝜑 → if(0 ≤ -𝐶, -𝐶, 0) ∈ ℂ) |
15 | 14 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐶, -𝐶, 0) ∈ ℂ) |
16 | | itgmulc2nc.5 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
17 | 16 | recnd 9947 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
18 | 10, 15, 17 | subdird 10366 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((if(0 ≤ 𝐶, 𝐶, 0) − if(0 ≤ -𝐶, -𝐶, 0)) · 𝐵) = ((if(0 ≤ 𝐶, 𝐶, 0) · 𝐵) − (if(0 ≤ -𝐶, -𝐶, 0) · 𝐵))) |
19 | 5, 18 | eqtr3d 2646 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 · 𝐵) = ((if(0 ≤ 𝐶, 𝐶, 0) · 𝐵) − (if(0 ≤ -𝐶, -𝐶, 0) · 𝐵))) |
20 | 19 | itgeq2dv 23354 |
. 2
⊢ (𝜑 → ∫𝐴(𝐶 · 𝐵) d𝑥 = ∫𝐴((if(0 ≤ 𝐶, 𝐶, 0) · 𝐵) − (if(0 ≤ -𝐶, -𝐶, 0) · 𝐵)) d𝑥) |
21 | | ovex 6577 |
. . . 4
⊢ (if(0
≤ 𝐶, 𝐶, 0) · 𝐵) ∈ V |
22 | 21 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐶, 𝐶, 0) · 𝐵) ∈ V) |
23 | | itgmulc2nc.3 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈
𝐿1) |
24 | | itgmulc2nc.m |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn) |
25 | | ovex 6577 |
. . . . . . . 8
⊢ (𝐶 · 𝐵) ∈ V |
26 | 25 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 · 𝐵) ∈ V) |
27 | 24, 26 | mbfdm2 23211 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ dom vol) |
28 | 8 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐶, 𝐶, 0) ∈ ℝ) |
29 | | fconstmpt 5085 |
. . . . . . 7
⊢ (𝐴 × {if(0 ≤ 𝐶, 𝐶, 0)}) = (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐶, 𝐶, 0)) |
30 | 29 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴 × {if(0 ≤ 𝐶, 𝐶, 0)}) = (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐶, 𝐶, 0))) |
31 | | eqidd 2611 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)) |
32 | 27, 28, 16, 30, 31 | offval2 6812 |
. . . . 5
⊢ (𝜑 → ((𝐴 × {if(0 ≤ 𝐶, 𝐶, 0)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ 𝐵)) = (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐶, 𝐶, 0) · 𝐵))) |
33 | | iblmbf 23340 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
34 | 23, 33 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
35 | | eqid 2610 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
36 | 17, 35 | fmptd 6292 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
37 | 34, 8, 36 | mbfmulc2re 23221 |
. . . . 5
⊢ (𝜑 → ((𝐴 × {if(0 ≤ 𝐶, 𝐶, 0)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ MblFn) |
38 | 32, 37 | eqeltrrd 2689 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐶, 𝐶, 0) · 𝐵)) ∈ MblFn) |
39 | 9, 16, 23, 38 | iblmulc2nc 32645 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐶, 𝐶, 0) · 𝐵)) ∈
𝐿1) |
40 | | ovex 6577 |
. . . 4
⊢ (if(0
≤ -𝐶, -𝐶, 0) · 𝐵) ∈ V |
41 | 40 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐶, -𝐶, 0) · 𝐵) ∈ V) |
42 | 13 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐶, -𝐶, 0) ∈ ℝ) |
43 | | fconstmpt 5085 |
. . . . . . 7
⊢ (𝐴 × {if(0 ≤ -𝐶, -𝐶, 0)}) = (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐶, -𝐶, 0)) |
44 | 43 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴 × {if(0 ≤ -𝐶, -𝐶, 0)}) = (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐶, -𝐶, 0))) |
45 | 27, 42, 16, 44, 31 | offval2 6812 |
. . . . 5
⊢ (𝜑 → ((𝐴 × {if(0 ≤ -𝐶, -𝐶, 0)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ 𝐵)) = (𝑥 ∈ 𝐴 ↦ (if(0 ≤ -𝐶, -𝐶, 0) · 𝐵))) |
46 | 34, 13, 36 | mbfmulc2re 23221 |
. . . . 5
⊢ (𝜑 → ((𝐴 × {if(0 ≤ -𝐶, -𝐶, 0)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ MblFn) |
47 | 45, 46 | eqeltrrd 2689 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ -𝐶, -𝐶, 0) · 𝐵)) ∈ MblFn) |
48 | 14, 16, 23, 47 | iblmulc2nc 32645 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ -𝐶, -𝐶, 0) · 𝐵)) ∈
𝐿1) |
49 | 19 | mpteq2dva 4672 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) = (𝑥 ∈ 𝐴 ↦ ((if(0 ≤ 𝐶, 𝐶, 0) · 𝐵) − (if(0 ≤ -𝐶, -𝐶, 0) · 𝐵)))) |
50 | 49, 24 | eqeltrrd 2689 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((if(0 ≤ 𝐶, 𝐶, 0) · 𝐵) − (if(0 ≤ -𝐶, -𝐶, 0) · 𝐵))) ∈ MblFn) |
51 | 22, 39, 41, 48, 50 | itgsubnc 32642 |
. 2
⊢ (𝜑 → ∫𝐴((if(0 ≤ 𝐶, 𝐶, 0) · 𝐵) − (if(0 ≤ -𝐶, -𝐶, 0) · 𝐵)) d𝑥 = (∫𝐴(if(0 ≤ 𝐶, 𝐶, 0) · 𝐵) d𝑥 − ∫𝐴(if(0 ≤ -𝐶, -𝐶, 0) · 𝐵) d𝑥)) |
52 | | ovex 6577 |
. . . . . . 7
⊢ (if(0
≤ 𝐶, 𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0)) ∈ V |
53 | 52 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐶, 𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0)) ∈ V) |
54 | | ifcl 4080 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ) |
55 | 16, 6, 54 | sylancl 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℝ) |
56 | 16 | iblre 23366 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ 𝐿1 ∧
(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈
𝐿1))) |
57 | 23, 56 | mpbid 221 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ 𝐿1 ∧
(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈
𝐿1)) |
58 | 57 | simpld 474 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈
𝐿1) |
59 | | eqidd 2611 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) = (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))) |
60 | 27, 28, 55, 30, 59 | offval2 6812 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 × {if(0 ≤ 𝐶, 𝐶, 0)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))) = (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐶, 𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0)))) |
61 | 16, 34 | mbfpos 23224 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn) |
62 | 55 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ 𝐵, 𝐵, 0) ∈ ℂ) |
63 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) = (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) |
64 | 62, 63 | fmptd 6292 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)):𝐴⟶ℂ) |
65 | 61, 8, 64 | mbfmulc2re 23221 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 × {if(0 ≤ 𝐶, 𝐶, 0)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))) ∈ MblFn) |
66 | 60, 65 | eqeltrrd 2689 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐶, 𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0))) ∈ MblFn) |
67 | 9, 55, 58, 66 | iblmulc2nc 32645 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐶, 𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0))) ∈
𝐿1) |
68 | | ovex 6577 |
. . . . . . 7
⊢ (if(0
≤ 𝐶, 𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0)) ∈ V |
69 | 68 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐶, 𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0)) ∈ V) |
70 | 16 | renegcld 10336 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℝ) |
71 | | ifcl 4080 |
. . . . . . . 8
⊢ ((-𝐵 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ) |
72 | 70, 6, 71 | sylancl 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℝ) |
73 | 57 | simprd 478 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈
𝐿1) |
74 | | eqidd 2611 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) = (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))) |
75 | 27, 28, 72, 30, 74 | offval2 6812 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 × {if(0 ≤ 𝐶, 𝐶, 0)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))) = (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐶, 𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0)))) |
76 | 16, 34 | mbfneg 23223 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐵) ∈ MblFn) |
77 | 70, 76 | mbfpos 23224 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ MblFn) |
78 | 72 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(0 ≤ -𝐵, -𝐵, 0) ∈ ℂ) |
79 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) = (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) |
80 | 78, 79 | fmptd 6292 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)):𝐴⟶ℂ) |
81 | 77, 8, 80 | mbfmulc2re 23221 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 × {if(0 ≤ 𝐶, 𝐶, 0)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))) ∈ MblFn) |
82 | 75, 81 | eqeltrrd 2689 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐶, 𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0))) ∈ MblFn) |
83 | 9, 72, 73, 82 | iblmulc2nc 32645 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐶, 𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0))) ∈
𝐿1) |
84 | | max0sub 11901 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ ℝ → (if(0
≤ 𝐵, 𝐵, 0) − if(0 ≤ -𝐵, -𝐵, 0)) = 𝐵) |
85 | 16, 84 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐵, 𝐵, 0) − if(0 ≤ -𝐵, -𝐵, 0)) = 𝐵) |
86 | 85 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐶, 𝐶, 0) · (if(0 ≤ 𝐵, 𝐵, 0) − if(0 ≤ -𝐵, -𝐵, 0))) = (if(0 ≤ 𝐶, 𝐶, 0) · 𝐵)) |
87 | 10, 62, 78 | subdid 10365 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐶, 𝐶, 0) · (if(0 ≤ 𝐵, 𝐵, 0) − if(0 ≤ -𝐵, -𝐵, 0))) = ((if(0 ≤ 𝐶, 𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0)) − (if(0 ≤ 𝐶, 𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0)))) |
88 | 86, 87 | eqtr3d 2646 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ 𝐶, 𝐶, 0) · 𝐵) = ((if(0 ≤ 𝐶, 𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0)) − (if(0 ≤ 𝐶, 𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0)))) |
89 | 88 | mpteq2dva 4672 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ 𝐶, 𝐶, 0) · 𝐵)) = (𝑥 ∈ 𝐴 ↦ ((if(0 ≤ 𝐶, 𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0)) − (if(0 ≤ 𝐶, 𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0))))) |
90 | 32, 89 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 × {if(0 ≤ 𝐶, 𝐶, 0)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ 𝐵)) = (𝑥 ∈ 𝐴 ↦ ((if(0 ≤ 𝐶, 𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0)) − (if(0 ≤ 𝐶, 𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0))))) |
91 | 90, 37 | eqeltrrd 2689 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((if(0 ≤ 𝐶, 𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0)) − (if(0 ≤ 𝐶, 𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0)))) ∈ MblFn) |
92 | 53, 67, 69, 83, 91 | itgsubnc 32642 |
. . . . 5
⊢ (𝜑 → ∫𝐴((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𝑥)) |
93 | 88 | itgeq2dv 23354 |
. . . . 5
⊢ (𝜑 → ∫𝐴(if(0 ≤ 𝐶, 𝐶, 0) · 𝐵) d𝑥 = ∫𝐴((if(0 ≤ 𝐶, 𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0)) − (if(0 ≤ 𝐶, 𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0))) d𝑥) |
94 | 16, 23 | itgreval 23369 |
. . . . . . 7
⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = (∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 − ∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥)) |
95 | 94 | oveq2d 6565 |
. . . . . 6
⊢ (𝜑 → (if(0 ≤ 𝐶, 𝐶, 0) · ∫𝐴𝐵 d𝑥) = (if(0 ≤ 𝐶, 𝐶, 0) · (∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 − ∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥))) |
96 | 55, 58 | itgcl 23356 |
. . . . . . 7
⊢ (𝜑 → ∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 ∈ ℂ) |
97 | 72, 73 | itgcl 23356 |
. . . . . . 7
⊢ (𝜑 → ∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥 ∈ ℂ) |
98 | 9, 96, 97 | subdid 10365 |
. . . . . 6
⊢ (𝜑 → (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𝑥))) |
99 | | max1 11890 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ 𝐶
∈ ℝ) → 0 ≤ if(0 ≤ 𝐶, 𝐶, 0)) |
100 | 6, 1, 99 | sylancr 694 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ if(0 ≤ 𝐶, 𝐶, 0)) |
101 | | max1 11890 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ 𝐵
∈ ℝ) → 0 ≤ if(0 ≤ 𝐵, 𝐵, 0)) |
102 | 6, 16, 101 | sylancr 694 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ 𝐵, 𝐵, 0)) |
103 | 9, 55, 58, 66, 8, 55, 100, 102 | itgmulc2nclem1 32646 |
. . . . . . 7
⊢ (𝜑 → (if(0 ≤ 𝐶, 𝐶, 0) · ∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥) = ∫𝐴(if(0 ≤ 𝐶, 𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0)) d𝑥) |
104 | | max1 11890 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ -𝐵
∈ ℝ) → 0 ≤ if(0 ≤ -𝐵, -𝐵, 0)) |
105 | 6, 70, 104 | sylancr 694 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤ -𝐵, -𝐵, 0)) |
106 | 9, 72, 73, 82, 8, 72, 100, 105 | itgmulc2nclem1 32646 |
. . . . . . 7
⊢ (𝜑 → (if(0 ≤ 𝐶, 𝐶, 0) · ∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥) = ∫𝐴(if(0 ≤ 𝐶, 𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0)) d𝑥) |
107 | 103, 106 | oveq12d 6567 |
. . . . . 6
⊢ (𝜑 → ((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𝑥)) |
108 | 95, 98, 107 | 3eqtrd 2648 |
. . . . 5
⊢ (𝜑 → (if(0 ≤ 𝐶, 𝐶, 0) · ∫𝐴𝐵 d𝑥) = (∫𝐴(if(0 ≤ 𝐶, 𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0)) d𝑥 − ∫𝐴(if(0 ≤ 𝐶, 𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0)) d𝑥)) |
109 | 92, 93, 108 | 3eqtr4d 2654 |
. . . 4
⊢ (𝜑 → ∫𝐴(if(0 ≤ 𝐶, 𝐶, 0) · 𝐵) d𝑥 = (if(0 ≤ 𝐶, 𝐶, 0) · ∫𝐴𝐵 d𝑥)) |
110 | | ovex 6577 |
. . . . . . 7
⊢ (if(0
≤ -𝐶, -𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0)) ∈ V |
111 | 110 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐶, -𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0)) ∈ V) |
112 | 27, 42, 55, 44, 59 | offval2 6812 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 × {if(0 ≤ -𝐶, -𝐶, 0)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))) = (𝑥 ∈ 𝐴 ↦ (if(0 ≤ -𝐶, -𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0)))) |
113 | 61, 13, 64 | mbfmulc2re 23221 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 × {if(0 ≤ -𝐶, -𝐶, 0)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0))) ∈ MblFn) |
114 | 112, 113 | eqeltrrd 2689 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ -𝐶, -𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0))) ∈ MblFn) |
115 | 14, 55, 58, 114 | iblmulc2nc 32645 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ -𝐶, -𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0))) ∈
𝐿1) |
116 | | ovex 6577 |
. . . . . . 7
⊢ (if(0
≤ -𝐶, -𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0)) ∈ V |
117 | 116 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐶, -𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0)) ∈ V) |
118 | 27, 42, 72, 44, 74 | offval2 6812 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 × {if(0 ≤ -𝐶, -𝐶, 0)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))) = (𝑥 ∈ 𝐴 ↦ (if(0 ≤ -𝐶, -𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0)))) |
119 | 77, 13, 80 | mbfmulc2re 23221 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 × {if(0 ≤ -𝐶, -𝐶, 0)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0))) ∈ MblFn) |
120 | 118, 119 | eqeltrrd 2689 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ -𝐶, -𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0))) ∈ MblFn) |
121 | 14, 72, 73, 120 | iblmulc2nc 32645 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ -𝐶, -𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0))) ∈
𝐿1) |
122 | 85 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐶, -𝐶, 0) · (if(0 ≤ 𝐵, 𝐵, 0) − if(0 ≤ -𝐵, -𝐵, 0))) = (if(0 ≤ -𝐶, -𝐶, 0) · 𝐵)) |
123 | 15, 62, 78 | subdid 10365 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐶, -𝐶, 0) · (if(0 ≤ 𝐵, 𝐵, 0) − if(0 ≤ -𝐵, -𝐵, 0))) = ((if(0 ≤ -𝐶, -𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0)) − (if(0 ≤ -𝐶, -𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0)))) |
124 | 122, 123 | eqtr3d 2646 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (if(0 ≤ -𝐶, -𝐶, 0) · 𝐵) = ((if(0 ≤ -𝐶, -𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0)) − (if(0 ≤ -𝐶, -𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0)))) |
125 | 124 | mpteq2dva 4672 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (if(0 ≤ -𝐶, -𝐶, 0) · 𝐵)) = (𝑥 ∈ 𝐴 ↦ ((if(0 ≤ -𝐶, -𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0)) − (if(0 ≤ -𝐶, -𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0))))) |
126 | 45, 125 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 × {if(0 ≤ -𝐶, -𝐶, 0)}) ∘𝑓 ·
(𝑥 ∈ 𝐴 ↦ 𝐵)) = (𝑥 ∈ 𝐴 ↦ ((if(0 ≤ -𝐶, -𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0)) − (if(0 ≤ -𝐶, -𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0))))) |
127 | 126, 46 | eqeltrrd 2689 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ((if(0 ≤ -𝐶, -𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0)) − (if(0 ≤ -𝐶, -𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0)))) ∈ MblFn) |
128 | 111, 115,
117, 121, 127 | itgsubnc 32642 |
. . . . 5
⊢ (𝜑 → ∫𝐴((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𝑥)) |
129 | 124 | itgeq2dv 23354 |
. . . . 5
⊢ (𝜑 → ∫𝐴(if(0 ≤ -𝐶, -𝐶, 0) · 𝐵) d𝑥 = ∫𝐴((if(0 ≤ -𝐶, -𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0)) − (if(0 ≤ -𝐶, -𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0))) d𝑥) |
130 | 94 | oveq2d 6565 |
. . . . . 6
⊢ (𝜑 → (if(0 ≤ -𝐶, -𝐶, 0) · ∫𝐴𝐵 d𝑥) = (if(0 ≤ -𝐶, -𝐶, 0) · (∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 − ∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥))) |
131 | 14, 96, 97 | subdid 10365 |
. . . . . 6
⊢ (𝜑 → (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𝑥))) |
132 | | max1 11890 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ -𝐶
∈ ℝ) → 0 ≤ if(0 ≤ -𝐶, -𝐶, 0)) |
133 | 6, 11, 132 | sylancr 694 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ if(0 ≤ -𝐶, -𝐶, 0)) |
134 | 14, 55, 58, 114, 13, 55, 133, 102 | itgmulc2nclem1 32646 |
. . . . . . 7
⊢ (𝜑 → (if(0 ≤ -𝐶, -𝐶, 0) · ∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥) = ∫𝐴(if(0 ≤ -𝐶, -𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0)) d𝑥) |
135 | 14, 72, 73, 120, 13, 72, 133, 105 | itgmulc2nclem1 32646 |
. . . . . . 7
⊢ (𝜑 → (if(0 ≤ -𝐶, -𝐶, 0) · ∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥) = ∫𝐴(if(0 ≤ -𝐶, -𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0)) d𝑥) |
136 | 134, 135 | oveq12d 6567 |
. . . . . 6
⊢ (𝜑 → ((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𝑥)) |
137 | 130, 131,
136 | 3eqtrd 2648 |
. . . . 5
⊢ (𝜑 → (if(0 ≤ -𝐶, -𝐶, 0) · ∫𝐴𝐵 d𝑥) = (∫𝐴(if(0 ≤ -𝐶, -𝐶, 0) · if(0 ≤ 𝐵, 𝐵, 0)) d𝑥 − ∫𝐴(if(0 ≤ -𝐶, -𝐶, 0) · if(0 ≤ -𝐵, -𝐵, 0)) d𝑥)) |
138 | 128, 129,
137 | 3eqtr4d 2654 |
. . . 4
⊢ (𝜑 → ∫𝐴(if(0 ≤ -𝐶, -𝐶, 0) · 𝐵) d𝑥 = (if(0 ≤ -𝐶, -𝐶, 0) · ∫𝐴𝐵 d𝑥)) |
139 | 109, 138 | oveq12d 6567 |
. . 3
⊢ (𝜑 → (∫𝐴(if(0 ≤ 𝐶, 𝐶, 0) · 𝐵) d𝑥 − ∫𝐴(if(0 ≤ -𝐶, -𝐶, 0) · 𝐵) d𝑥) = ((if(0 ≤ 𝐶, 𝐶, 0) · ∫𝐴𝐵 d𝑥) − (if(0 ≤ -𝐶, -𝐶, 0) · ∫𝐴𝐵 d𝑥))) |
140 | 16, 23 | itgcl 23356 |
. . . 4
⊢ (𝜑 → ∫𝐴𝐵 d𝑥 ∈ ℂ) |
141 | 9, 14, 140 | subdird 10366 |
. . 3
⊢ (𝜑 → ((if(0 ≤ 𝐶, 𝐶, 0) − if(0 ≤ -𝐶, -𝐶, 0)) · ∫𝐴𝐵 d𝑥) = ((if(0 ≤ 𝐶, 𝐶, 0) · ∫𝐴𝐵 d𝑥) − (if(0 ≤ -𝐶, -𝐶, 0) · ∫𝐴𝐵 d𝑥))) |
142 | 3 | oveq1d 6564 |
. . 3
⊢ (𝜑 → ((if(0 ≤ 𝐶, 𝐶, 0) − if(0 ≤ -𝐶, -𝐶, 0)) · ∫𝐴𝐵 d𝑥) = (𝐶 · ∫𝐴𝐵 d𝑥)) |
143 | 139, 141,
142 | 3eqtr2d 2650 |
. 2
⊢ (𝜑 → (∫𝐴(if(0 ≤ 𝐶, 𝐶, 0) · 𝐵) d𝑥 − ∫𝐴(if(0 ≤ -𝐶, -𝐶, 0) · 𝐵) d𝑥) = (𝐶 · ∫𝐴𝐵 d𝑥)) |
144 | 20, 51, 143 | 3eqtrrd 2649 |
1
⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥) |