| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | itgmulc2.1 | . . 3
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 2 |  | itgmulc2.2 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) | 
| 3 |  | itgmulc2.3 | . . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈
𝐿1) | 
| 4 |  | iblmbf 25803 | . . . 4
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) | 
| 5 | 3, 4 | syl 17 | . . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) | 
| 6 | 1, 2, 5 | mbfmulc2 25699 | . 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn) | 
| 7 |  | ifan 4578 | . . . . . 6
⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) = if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) | 
| 8 | 1 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) | 
| 9 | 5, 2 | mbfmptcl 25672 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) | 
| 10 | 8, 9 | mulcld 11282 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 · 𝐵) ∈ ℂ) | 
| 11 | 10 | adantlr 715 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (𝐶 · 𝐵) ∈ ℂ) | 
| 12 |  | ax-icn 11215 | . . . . . . . . . . . . . 14
⊢ i ∈
ℂ | 
| 13 |  | ine0 11699 | . . . . . . . . . . . . . 14
⊢ i ≠
0 | 
| 14 |  | elfzelz 13565 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (0...3) → 𝑘 ∈
ℤ) | 
| 15 | 14 | ad2antlr 727 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → 𝑘 ∈ ℤ) | 
| 16 |  | expclz 14126 | . . . . . . . . . . . . . 14
⊢ ((i
∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ) → (i↑𝑘) ∈
ℂ) | 
| 17 | 12, 13, 15, 16 | mp3an12i 1466 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (i↑𝑘) ∈ ℂ) | 
| 18 |  | expne0i 14136 | . . . . . . . . . . . . . 14
⊢ ((i
∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ) → (i↑𝑘) ≠ 0) | 
| 19 | 12, 13, 15, 18 | mp3an12i 1466 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (i↑𝑘) ≠ 0) | 
| 20 | 11, 17, 19 | divcld 12044 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → ((𝐶 · 𝐵) / (i↑𝑘)) ∈ ℂ) | 
| 21 | 20 | recld 15234 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ∈ ℝ) | 
| 22 |  | 0re 11264 | . . . . . . . . . . 11
⊢ 0 ∈
ℝ | 
| 23 |  | ifcl 4570 | . . . . . . . . . . 11
⊢
(((ℜ‘((𝐶
· 𝐵) / (i↑𝑘))) ∈ ℝ ∧ 0
∈ ℝ) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ ℝ) | 
| 24 | 21, 22, 23 | sylancl 586 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ ℝ) | 
| 25 | 24 | rexrd 11312 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈
ℝ*) | 
| 26 |  | max1 13228 | . . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ∈ ℝ) → 0 ≤ if(0 ≤
(ℜ‘((𝐶 ·
𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) | 
| 27 | 22, 21, 26 | sylancr 587 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤
(ℜ‘((𝐶 ·
𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) | 
| 28 |  | elxrge0 13498 | . . . . . . . . 9
⊢ (if(0
≤ (ℜ‘((𝐶
· 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ (0[,]+∞) ↔ (if(0
≤ (ℜ‘((𝐶
· 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ ℝ* ∧ 0
≤ if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) | 
| 29 | 25, 27, 28 | sylanbrc 583 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈
(0[,]+∞)) | 
| 30 |  | 0e0iccpnf 13500 | . . . . . . . . 9
⊢ 0 ∈
(0[,]+∞) | 
| 31 | 30 | a1i 11 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,]+∞)) | 
| 32 | 29, 31 | ifclda 4560 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ∈
(0[,]+∞)) | 
| 33 | 32 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ∈
(0[,]+∞)) | 
| 34 | 7, 33 | eqeltrid 2844 | . . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈
(0[,]+∞)) | 
| 35 | 34 | fmpttd 7134 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))),
0)):ℝ⟶(0[,]+∞)) | 
| 36 |  | reex 11247 | . . . . . . . . . . 11
⊢ ℝ
∈ V | 
| 37 | 36 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → ℝ ∈
V) | 
| 38 | 1 | abscld 15476 | . . . . . . . . . . 11
⊢ (𝜑 → (abs‘𝐶) ∈
ℝ) | 
| 39 | 38 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘𝐶) ∈
ℝ) | 
| 40 | 9 | abscld 15476 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈ ℝ) | 
| 41 | 9 | absge0d 15484 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (abs‘𝐵)) | 
| 42 |  | elrege0 13495 | . . . . . . . . . . . . 13
⊢
((abs‘𝐵)
∈ (0[,)+∞) ↔ ((abs‘𝐵) ∈ ℝ ∧ 0 ≤
(abs‘𝐵))) | 
| 43 | 40, 41, 42 | sylanbrc 583 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈ (0[,)+∞)) | 
| 44 |  | 0e0icopnf 13499 | . . . . . . . . . . . . 13
⊢ 0 ∈
(0[,)+∞) | 
| 45 | 44 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,)+∞)) | 
| 46 | 43, 45 | ifclda 4560 | . . . . . . . . . . 11
⊢ (𝜑 → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ∈
(0[,)+∞)) | 
| 47 | 46 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ∈
(0[,)+∞)) | 
| 48 |  | fconstmpt 5746 | . . . . . . . . . . 11
⊢ (ℝ
× {(abs‘𝐶)}) =
(𝑥 ∈ ℝ ↦
(abs‘𝐶)) | 
| 49 | 48 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → (ℝ ×
{(abs‘𝐶)}) = (𝑥 ∈ ℝ ↦
(abs‘𝐶))) | 
| 50 |  | eqidd 2737 | . . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))) | 
| 51 | 37, 39, 47, 49, 50 | offval2 7718 | . . . . . . . . 9
⊢ (𝜑 → ((ℝ ×
{(abs‘𝐶)})
∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))) = (𝑥 ∈ ℝ ↦ ((abs‘𝐶) · if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)))) | 
| 52 |  | ovif2 7533 | . . . . . . . . . . 11
⊢
((abs‘𝐶)
· if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)) = if(𝑥 ∈ 𝐴, ((abs‘𝐶) · (abs‘𝐵)), ((abs‘𝐶) · 0)) | 
| 53 | 8, 9 | absmuld 15494 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐶 · 𝐵)) = ((abs‘𝐶) · (abs‘𝐵))) | 
| 54 | 53 | ifeq1da 4556 | . . . . . . . . . . . 12
⊢ (𝜑 → if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), ((abs‘𝐶) · 0)) = if(𝑥 ∈ 𝐴, ((abs‘𝐶) · (abs‘𝐵)), ((abs‘𝐶) · 0))) | 
| 55 | 38 | recnd 11290 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (abs‘𝐶) ∈
ℂ) | 
| 56 | 55 | mul01d 11461 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((abs‘𝐶) · 0) =
0) | 
| 57 | 56 | ifeq2d 4545 | . . . . . . . . . . . 12
⊢ (𝜑 → if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), ((abs‘𝐶) · 0)) = if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)) | 
| 58 | 54, 57 | eqtr3d 2778 | . . . . . . . . . . 11
⊢ (𝜑 → if(𝑥 ∈ 𝐴, ((abs‘𝐶) · (abs‘𝐵)), ((abs‘𝐶) · 0)) = if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)) | 
| 59 | 52, 58 | eqtrid 2788 | . . . . . . . . . 10
⊢ (𝜑 → ((abs‘𝐶) · if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)) = if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)) | 
| 60 | 59 | mpteq2dv 5243 | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ ((abs‘𝐶) · if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0))) | 
| 61 | 51, 60 | eqtrd 2776 | . . . . . . . 8
⊢ (𝜑 → ((ℝ ×
{(abs‘𝐶)})
∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0))) | 
| 62 | 61 | fveq2d 6909 | . . . . . . 7
⊢ (𝜑 →
(∫2‘((ℝ × {(abs‘𝐶)}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)))) = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)))) | 
| 63 | 47 | fmpttd 7134 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵),
0)):ℝ⟶(0[,)+∞)) | 
| 64 | 2, 3 | iblabs 25865 | . . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈
𝐿1) | 
| 65 | 40, 41 | iblpos 25829 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘𝐵), 0))) ∈
ℝ))) | 
| 66 | 64, 65 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘𝐵), 0))) ∈
ℝ)) | 
| 67 | 66 | simprd 495 | . . . . . . . 8
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘𝐵), 0))) ∈
ℝ) | 
| 68 |  | abscl 15318 | . . . . . . . . . 10
⊢ (𝐶 ∈ ℂ →
(abs‘𝐶) ∈
ℝ) | 
| 69 |  | absge0 15327 | . . . . . . . . . 10
⊢ (𝐶 ∈ ℂ → 0 ≤
(abs‘𝐶)) | 
| 70 |  | elrege0 13495 | . . . . . . . . . 10
⊢
((abs‘𝐶)
∈ (0[,)+∞) ↔ ((abs‘𝐶) ∈ ℝ ∧ 0 ≤
(abs‘𝐶))) | 
| 71 | 68, 69, 70 | sylanbrc 583 | . . . . . . . . 9
⊢ (𝐶 ∈ ℂ →
(abs‘𝐶) ∈
(0[,)+∞)) | 
| 72 | 1, 71 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (abs‘𝐶) ∈
(0[,)+∞)) | 
| 73 | 63, 67, 72 | itg2mulc 25783 | . . . . . . 7
⊢ (𝜑 →
(∫2‘((ℝ × {(abs‘𝐶)}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)))) = ((abs‘𝐶) · (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))))) | 
| 74 | 62, 73 | eqtr3d 2778 | . . . . . 6
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0))) = ((abs‘𝐶) · (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))))) | 
| 75 | 38, 67 | remulcld 11292 | . . . . . 6
⊢ (𝜑 → ((abs‘𝐶) ·
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘𝐵), 0)))) ∈
ℝ) | 
| 76 | 74, 75 | eqeltrd 2840 | . . . . 5
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0))) ∈ ℝ) | 
| 77 | 76 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0))) ∈ ℝ) | 
| 78 | 10 | abscld 15476 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐶 · 𝐵)) ∈ ℝ) | 
| 79 | 78 | rexrd 11312 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐶 · 𝐵)) ∈
ℝ*) | 
| 80 | 10 | absge0d 15484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (abs‘(𝐶 · 𝐵))) | 
| 81 |  | elxrge0 13498 | . . . . . . . . . 10
⊢
((abs‘(𝐶
· 𝐵)) ∈
(0[,]+∞) ↔ ((abs‘(𝐶 · 𝐵)) ∈ ℝ* ∧ 0 ≤
(abs‘(𝐶 ·
𝐵)))) | 
| 82 | 79, 80, 81 | sylanbrc 583 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐶 · 𝐵)) ∈ (0[,]+∞)) | 
| 83 | 30 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,]+∞)) | 
| 84 | 82, 83 | ifclda 4560 | . . . . . . . 8
⊢ (𝜑 → if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0) ∈
(0[,]+∞)) | 
| 85 | 84 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0) ∈
(0[,]+∞)) | 
| 86 | 85 | fmpttd 7134 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)),
0)):ℝ⟶(0[,]+∞)) | 
| 87 | 86 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)),
0)):ℝ⟶(0[,]+∞)) | 
| 88 | 20 | releabsd 15491 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ≤ (abs‘((𝐶 · 𝐵) / (i↑𝑘)))) | 
| 89 | 11, 17, 19 | absdivd 15495 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘((𝐶 · 𝐵) / (i↑𝑘))) = ((abs‘(𝐶 · 𝐵)) / (abs‘(i↑𝑘)))) | 
| 90 |  | elfznn0 13661 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (0...3) → 𝑘 ∈
ℕ0) | 
| 91 | 90 | ad2antlr 727 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → 𝑘 ∈ ℕ0) | 
| 92 |  | absexp 15344 | . . . . . . . . . . . . . . . . 17
⊢ ((i
∈ ℂ ∧ 𝑘
∈ ℕ0) → (abs‘(i↑𝑘)) = ((abs‘i)↑𝑘)) | 
| 93 | 12, 91, 92 | sylancr 587 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘(i↑𝑘)) = ((abs‘i)↑𝑘)) | 
| 94 |  | absi 15326 | . . . . . . . . . . . . . . . . . 18
⊢
(abs‘i) = 1 | 
| 95 | 94 | oveq1i 7442 | . . . . . . . . . . . . . . . . 17
⊢
((abs‘i)↑𝑘) = (1↑𝑘) | 
| 96 |  | 1exp 14133 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℤ →
(1↑𝑘) =
1) | 
| 97 | 15, 96 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (1↑𝑘) = 1) | 
| 98 | 95, 97 | eqtrid 2788 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → ((abs‘i)↑𝑘) = 1) | 
| 99 | 93, 98 | eqtrd 2776 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘(i↑𝑘)) = 1) | 
| 100 | 99 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → ((abs‘(𝐶 · 𝐵)) / (abs‘(i↑𝑘))) = ((abs‘(𝐶 · 𝐵)) / 1)) | 
| 101 | 78 | recnd 11290 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐶 · 𝐵)) ∈ ℂ) | 
| 102 | 101 | adantlr 715 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐶 · 𝐵)) ∈ ℂ) | 
| 103 | 102 | div1d 12036 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → ((abs‘(𝐶 · 𝐵)) / 1) = (abs‘(𝐶 · 𝐵))) | 
| 104 | 89, 100, 103 | 3eqtrd 2780 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘((𝐶 · 𝐵) / (i↑𝑘))) = (abs‘(𝐶 · 𝐵))) | 
| 105 | 88, 104 | breqtrd 5168 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ≤ (abs‘(𝐶 · 𝐵))) | 
| 106 | 80 | adantlr 715 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → 0 ≤ (abs‘(𝐶 · 𝐵))) | 
| 107 |  | breq1 5145 | . . . . . . . . . . . . 13
⊢
((ℜ‘((𝐶
· 𝐵) / (i↑𝑘))) = if(0 ≤
(ℜ‘((𝐶 ·
𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) → ((ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ≤ (abs‘(𝐶 · 𝐵)) ↔ if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ (abs‘(𝐶 · 𝐵)))) | 
| 108 |  | breq1 5145 | . . . . . . . . . . . . 13
⊢ (0 = if(0
≤ (ℜ‘((𝐶
· 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) → (0 ≤ (abs‘(𝐶 · 𝐵)) ↔ if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ (abs‘(𝐶 · 𝐵)))) | 
| 109 | 107, 108 | ifboth 4564 | . . . . . . . . . . . 12
⊢
(((ℜ‘((𝐶
· 𝐵) / (i↑𝑘))) ≤ (abs‘(𝐶 · 𝐵)) ∧ 0 ≤ (abs‘(𝐶 · 𝐵))) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ (abs‘(𝐶 · 𝐵))) | 
| 110 | 105, 106,
109 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ (abs‘(𝐶 · 𝐵))) | 
| 111 |  | iftrue 4530 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) = if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) | 
| 112 | 111 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) = if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) | 
| 113 |  | iftrue 4530 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0) = (abs‘(𝐶 · 𝐵))) | 
| 114 | 113 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0) = (abs‘(𝐶 · 𝐵))) | 
| 115 | 110, 112,
114 | 3brtr4d 5174 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ≤ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)) | 
| 116 | 115 | ex 412 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ≤ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0))) | 
| 117 |  | 0le0 12368 | . . . . . . . . . . 11
⊢ 0 ≤
0 | 
| 118 | 117 | a1i 11 | . . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → 0 ≤ 0) | 
| 119 |  | iffalse 4533 | . . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) = 0) | 
| 120 |  | iffalse 4533 | . . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0) = 0) | 
| 121 | 118, 119,
120 | 3brtr4d 5174 | . . . . . . . . 9
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ≤ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)) | 
| 122 | 116, 121 | pm2.61d1 180 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ≤ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)) | 
| 123 | 7, 122 | eqbrtrid 5177 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)) | 
| 124 | 123 | ralrimivw 3149 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → ∀𝑥 ∈ ℝ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)) | 
| 125 | 36 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → ℝ ∈
V) | 
| 126 | 85 | adantlr 715 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0) ∈
(0[,]+∞)) | 
| 127 |  | eqidd 2737 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) | 
| 128 |  | eqidd 2737 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0))) | 
| 129 | 125, 34, 126, 127, 128 | ofrfval2 7719 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) ∘r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)) ↔ ∀𝑥 ∈ ℝ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0))) | 
| 130 | 124, 129 | mpbird 257 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) ∘r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0))) | 
| 131 |  | itg2le 25775 | . . . . 5
⊢ (((𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘((𝐶 ·
𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)):ℝ⟶(0[,]+∞) ∧
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)):ℝ⟶(0[,]+∞) ∧
(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘((𝐶 ·
𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) ∘r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0))) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)))) | 
| 132 | 35, 87, 130, 131 | syl3anc 1372 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)))) | 
| 133 |  | itg2lecl 25774 | . . . 4
⊢ (((𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘((𝐶 ·
𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)):ℝ⟶(0[,]+∞) ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0))) ∈ ℝ ∧
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)))) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ∈ ℝ) | 
| 134 | 35, 77, 132, 133 | syl3anc 1372 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ∈ ℝ) | 
| 135 | 134 | ralrimiva 3145 | . 2
⊢ (𝜑 → ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ∈ ℝ) | 
| 136 |  | eqidd 2737 | . . 3
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) | 
| 137 |  | eqidd 2737 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) = (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))) | 
| 138 | 136, 137,
10 | isibl2 25802 | . 2
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ∈ ℝ))) | 
| 139 | 6, 135, 138 | mpbir2and 713 | 1
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈
𝐿1) |