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