Step | Hyp | Ref
| Expression |
1 | | itgmulc2.1 |
. . 3
⊢ (𝜑 → 𝐶 ∈ ℂ) |
2 | | itgmulc2.2 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
3 | | itgmulc2.3 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈
𝐿1) |
4 | | iblmbf 24670 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
5 | 3, 4 | syl 17 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
6 | 1, 2, 5 | mbfmulc2 24565 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn) |
7 | | ifan 4497 |
. . . . . 6
⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) = if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) |
8 | 1 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) |
9 | 5, 2 | mbfmptcl 24538 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
10 | 8, 9 | mulcld 10858 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 · 𝐵) ∈ ℂ) |
11 | 10 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (𝐶 · 𝐵) ∈ ℂ) |
12 | | ax-icn 10793 |
. . . . . . . . . . . . . 14
⊢ i ∈
ℂ |
13 | | ine0 11272 |
. . . . . . . . . . . . . 14
⊢ i ≠
0 |
14 | | elfzelz 13117 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (0...3) → 𝑘 ∈
ℤ) |
15 | 14 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → 𝑘 ∈ ℤ) |
16 | | expclz 13665 |
. . . . . . . . . . . . . 14
⊢ ((i
∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ) → (i↑𝑘) ∈
ℂ) |
17 | 12, 13, 15, 16 | mp3an12i 1467 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (i↑𝑘) ∈ ℂ) |
18 | | expne0i 13672 |
. . . . . . . . . . . . . 14
⊢ ((i
∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ) → (i↑𝑘) ≠ 0) |
19 | 12, 13, 15, 18 | mp3an12i 1467 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (i↑𝑘) ≠ 0) |
20 | 11, 17, 19 | divcld 11613 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → ((𝐶 · 𝐵) / (i↑𝑘)) ∈ ℂ) |
21 | 20 | recld 14762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ∈ ℝ) |
22 | | 0re 10840 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
23 | | ifcl 4489 |
. . . . . . . . . . 11
⊢
(((ℜ‘((𝐶
· 𝐵) / (i↑𝑘))) ∈ ℝ ∧ 0
∈ ℝ) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ ℝ) |
24 | 21, 22, 23 | sylancl 589 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ ℝ) |
25 | 24 | rexrd 10888 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈
ℝ*) |
26 | | max1 12780 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ∈ ℝ) → 0 ≤ if(0 ≤
(ℜ‘((𝐶 ·
𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) |
27 | 22, 21, 26 | sylancr 590 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤
(ℜ‘((𝐶 ·
𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) |
28 | | elxrge0 13050 |
. . . . . . . . 9
⊢ (if(0
≤ (ℜ‘((𝐶
· 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ (0[,]+∞) ↔ (if(0
≤ (ℜ‘((𝐶
· 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ ℝ* ∧ 0
≤ if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) |
29 | 25, 27, 28 | sylanbrc 586 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈
(0[,]+∞)) |
30 | | 0e0iccpnf 13052 |
. . . . . . . . 9
⊢ 0 ∈
(0[,]+∞) |
31 | 30 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,]+∞)) |
32 | 29, 31 | ifclda 4479 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ∈
(0[,]+∞)) |
33 | 32 | adantr 484 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ∈
(0[,]+∞)) |
34 | 7, 33 | eqeltrid 2842 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈
(0[,]+∞)) |
35 | 34 | fmpttd 6937 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))),
0)):ℝ⟶(0[,]+∞)) |
36 | | reex 10825 |
. . . . . . . . . . 11
⊢ ℝ
∈ V |
37 | 36 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ ∈
V) |
38 | 1 | abscld 15005 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘𝐶) ∈
ℝ) |
39 | 38 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘𝐶) ∈
ℝ) |
40 | 9 | abscld 15005 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈ ℝ) |
41 | 9 | absge0d 15013 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (abs‘𝐵)) |
42 | | elrege0 13047 |
. . . . . . . . . . . . 13
⊢
((abs‘𝐵)
∈ (0[,)+∞) ↔ ((abs‘𝐵) ∈ ℝ ∧ 0 ≤
(abs‘𝐵))) |
43 | 40, 41, 42 | sylanbrc 586 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈ (0[,)+∞)) |
44 | | 0e0icopnf 13051 |
. . . . . . . . . . . . 13
⊢ 0 ∈
(0[,)+∞) |
45 | 44 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,)+∞)) |
46 | 43, 45 | ifclda 4479 |
. . . . . . . . . . 11
⊢ (𝜑 → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ∈
(0[,)+∞)) |
47 | 46 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ∈
(0[,)+∞)) |
48 | | fconstmpt 5616 |
. . . . . . . . . . 11
⊢ (ℝ
× {(abs‘𝐶)}) =
(𝑥 ∈ ℝ ↦
(abs‘𝐶)) |
49 | 48 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ ×
{(abs‘𝐶)}) = (𝑥 ∈ ℝ ↦
(abs‘𝐶))) |
50 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))) |
51 | 37, 39, 47, 49, 50 | offval2 7493 |
. . . . . . . . 9
⊢ (𝜑 → ((ℝ ×
{(abs‘𝐶)})
∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))) = (𝑥 ∈ ℝ ↦ ((abs‘𝐶) · if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)))) |
52 | | ovif2 7314 |
. . . . . . . . . . 11
⊢
((abs‘𝐶)
· if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)) = if(𝑥 ∈ 𝐴, ((abs‘𝐶) · (abs‘𝐵)), ((abs‘𝐶) · 0)) |
53 | 8, 9 | absmuld 15023 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐶 · 𝐵)) = ((abs‘𝐶) · (abs‘𝐵))) |
54 | 53 | ifeq1da 4475 |
. . . . . . . . . . . 12
⊢ (𝜑 → if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), ((abs‘𝐶) · 0)) = if(𝑥 ∈ 𝐴, ((abs‘𝐶) · (abs‘𝐵)), ((abs‘𝐶) · 0))) |
55 | 38 | recnd 10866 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (abs‘𝐶) ∈
ℂ) |
56 | 55 | mul01d 11036 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((abs‘𝐶) · 0) =
0) |
57 | 56 | ifeq2d 4464 |
. . . . . . . . . . . 12
⊢ (𝜑 → if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), ((abs‘𝐶) · 0)) = if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)) |
58 | 54, 57 | eqtr3d 2779 |
. . . . . . . . . . 11
⊢ (𝜑 → if(𝑥 ∈ 𝐴, ((abs‘𝐶) · (abs‘𝐵)), ((abs‘𝐶) · 0)) = if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)) |
59 | 52, 58 | syl5eq 2790 |
. . . . . . . . . 10
⊢ (𝜑 → ((abs‘𝐶) · if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)) = if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)) |
60 | 59 | mpteq2dv 5156 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ ((abs‘𝐶) · if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0))) |
61 | 51, 60 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → ((ℝ ×
{(abs‘𝐶)})
∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0))) |
62 | 61 | fveq2d 6726 |
. . . . . . 7
⊢ (𝜑 →
(∫2‘((ℝ × {(abs‘𝐶)}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)))) = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)))) |
63 | 47 | fmpttd 6937 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵),
0)):ℝ⟶(0[,)+∞)) |
64 | 2, 3 | iblabs 24731 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈
𝐿1) |
65 | 40, 41 | iblpos 24695 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘𝐵), 0))) ∈
ℝ))) |
66 | 64, 65 | mpbid 235 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘𝐵), 0))) ∈
ℝ)) |
67 | 66 | simprd 499 |
. . . . . . . 8
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘𝐵), 0))) ∈
ℝ) |
68 | | abscl 14847 |
. . . . . . . . . 10
⊢ (𝐶 ∈ ℂ →
(abs‘𝐶) ∈
ℝ) |
69 | | absge0 14856 |
. . . . . . . . . 10
⊢ (𝐶 ∈ ℂ → 0 ≤
(abs‘𝐶)) |
70 | | elrege0 13047 |
. . . . . . . . . 10
⊢
((abs‘𝐶)
∈ (0[,)+∞) ↔ ((abs‘𝐶) ∈ ℝ ∧ 0 ≤
(abs‘𝐶))) |
71 | 68, 69, 70 | sylanbrc 586 |
. . . . . . . . 9
⊢ (𝐶 ∈ ℂ →
(abs‘𝐶) ∈
(0[,)+∞)) |
72 | 1, 71 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (abs‘𝐶) ∈
(0[,)+∞)) |
73 | 63, 67, 72 | itg2mulc 24650 |
. . . . . . 7
⊢ (𝜑 →
(∫2‘((ℝ × {(abs‘𝐶)}) ∘f · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)))) = ((abs‘𝐶) · (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))))) |
74 | 62, 73 | eqtr3d 2779 |
. . . . . 6
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0))) = ((abs‘𝐶) · (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))))) |
75 | 38, 67 | remulcld 10868 |
. . . . . 6
⊢ (𝜑 → ((abs‘𝐶) ·
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘𝐵), 0)))) ∈
ℝ) |
76 | 74, 75 | eqeltrd 2838 |
. . . . 5
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0))) ∈ ℝ) |
77 | 76 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0))) ∈ ℝ) |
78 | 10 | abscld 15005 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐶 · 𝐵)) ∈ ℝ) |
79 | 78 | rexrd 10888 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐶 · 𝐵)) ∈
ℝ*) |
80 | 10 | absge0d 15013 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (abs‘(𝐶 · 𝐵))) |
81 | | elxrge0 13050 |
. . . . . . . . . 10
⊢
((abs‘(𝐶
· 𝐵)) ∈
(0[,]+∞) ↔ ((abs‘(𝐶 · 𝐵)) ∈ ℝ* ∧ 0 ≤
(abs‘(𝐶 ·
𝐵)))) |
82 | 79, 80, 81 | sylanbrc 586 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐶 · 𝐵)) ∈ (0[,]+∞)) |
83 | 30 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,]+∞)) |
84 | 82, 83 | ifclda 4479 |
. . . . . . . 8
⊢ (𝜑 → if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0) ∈
(0[,]+∞)) |
85 | 84 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0) ∈
(0[,]+∞)) |
86 | 85 | fmpttd 6937 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)),
0)):ℝ⟶(0[,]+∞)) |
87 | 86 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)),
0)):ℝ⟶(0[,]+∞)) |
88 | 20 | releabsd 15020 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ≤ (abs‘((𝐶 · 𝐵) / (i↑𝑘)))) |
89 | 11, 17, 19 | absdivd 15024 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘((𝐶 · 𝐵) / (i↑𝑘))) = ((abs‘(𝐶 · 𝐵)) / (abs‘(i↑𝑘)))) |
90 | | elfznn0 13210 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (0...3) → 𝑘 ∈
ℕ0) |
91 | 90 | ad2antlr 727 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → 𝑘 ∈ ℕ0) |
92 | | absexp 14873 |
. . . . . . . . . . . . . . . . 17
⊢ ((i
∈ ℂ ∧ 𝑘
∈ ℕ0) → (abs‘(i↑𝑘)) = ((abs‘i)↑𝑘)) |
93 | 12, 91, 92 | sylancr 590 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘(i↑𝑘)) = ((abs‘i)↑𝑘)) |
94 | | absi 14855 |
. . . . . . . . . . . . . . . . . 18
⊢
(abs‘i) = 1 |
95 | 94 | oveq1i 7228 |
. . . . . . . . . . . . . . . . 17
⊢
((abs‘i)↑𝑘) = (1↑𝑘) |
96 | | 1exp 13669 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℤ →
(1↑𝑘) =
1) |
97 | 15, 96 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (1↑𝑘) = 1) |
98 | 95, 97 | syl5eq 2790 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → ((abs‘i)↑𝑘) = 1) |
99 | 93, 98 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘(i↑𝑘)) = 1) |
100 | 99 | oveq2d 7234 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → ((abs‘(𝐶 · 𝐵)) / (abs‘(i↑𝑘))) = ((abs‘(𝐶 · 𝐵)) / 1)) |
101 | 78 | recnd 10866 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐶 · 𝐵)) ∈ ℂ) |
102 | 101 | adantlr 715 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐶 · 𝐵)) ∈ ℂ) |
103 | 102 | div1d 11605 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → ((abs‘(𝐶 · 𝐵)) / 1) = (abs‘(𝐶 · 𝐵))) |
104 | 89, 100, 103 | 3eqtrd 2781 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘((𝐶 · 𝐵) / (i↑𝑘))) = (abs‘(𝐶 · 𝐵))) |
105 | 88, 104 | breqtrd 5084 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ≤ (abs‘(𝐶 · 𝐵))) |
106 | 80 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → 0 ≤ (abs‘(𝐶 · 𝐵))) |
107 | | breq1 5061 |
. . . . . . . . . . . . 13
⊢
((ℜ‘((𝐶
· 𝐵) / (i↑𝑘))) = if(0 ≤
(ℜ‘((𝐶 ·
𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) → ((ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ≤ (abs‘(𝐶 · 𝐵)) ↔ if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ (abs‘(𝐶 · 𝐵)))) |
108 | | breq1 5061 |
. . . . . . . . . . . . 13
⊢ (0 = if(0
≤ (ℜ‘((𝐶
· 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) → (0 ≤ (abs‘(𝐶 · 𝐵)) ↔ if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ (abs‘(𝐶 · 𝐵)))) |
109 | 107, 108 | ifboth 4483 |
. . . . . . . . . . . 12
⊢
(((ℜ‘((𝐶
· 𝐵) / (i↑𝑘))) ≤ (abs‘(𝐶 · 𝐵)) ∧ 0 ≤ (abs‘(𝐶 · 𝐵))) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ (abs‘(𝐶 · 𝐵))) |
110 | 105, 106,
109 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ (abs‘(𝐶 · 𝐵))) |
111 | | iftrue 4450 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) = if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) |
112 | 111 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) = if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) |
113 | | iftrue 4450 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0) = (abs‘(𝐶 · 𝐵))) |
114 | 113 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0) = (abs‘(𝐶 · 𝐵))) |
115 | 110, 112,
114 | 3brtr4d 5090 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ≤ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)) |
116 | 115 | ex 416 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ≤ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0))) |
117 | | 0le0 11936 |
. . . . . . . . . . 11
⊢ 0 ≤
0 |
118 | 117 | a1i 11 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → 0 ≤ 0) |
119 | | iffalse 4453 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) = 0) |
120 | | iffalse 4453 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0) = 0) |
121 | 118, 119,
120 | 3brtr4d 5090 |
. . . . . . . . 9
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ≤ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)) |
122 | 116, 121 | pm2.61d1 183 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ≤ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)) |
123 | 7, 122 | eqbrtrid 5093 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)) |
124 | 123 | ralrimivw 3106 |
. . . . . 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 2738 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) |
128 | | eqidd 2738 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0))) |
129 | 125, 34, 126, 127, 128 | ofrfval2 7494 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) ∘r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)) ↔ ∀𝑥 ∈ ℝ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0))) |
130 | 124, 129 | mpbird 260 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) ∘r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0))) |
131 | | itg2le 24642 |
. . . . 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 1373 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘(𝐶 · 𝐵)), 0)))) |
133 | | itg2lecl 24641 |
. . . 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 1373 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ∈ ℝ) |
135 | 134 | ralrimiva 3105 |
. 2
⊢ (𝜑 → ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ∈ ℝ) |
136 | | eqidd 2738 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) |
137 | | eqidd 2738 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) = (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))) |
138 | 136, 137,
10 | isibl2 24669 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ∈ ℝ))) |
139 | 6, 135, 138 | mpbir2and 713 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈
𝐿1) |