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