Step | Hyp | Ref
| Expression |
1 | | itgmulc2nc.m |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn) |
2 | | ifan 4134 |
. . . . . 6
⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) = if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) |
3 | | itgmulc2nc.1 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 ∈ ℂ) |
4 | 3 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) |
5 | | itgmulc2nc.3 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈
𝐿1) |
6 | | iblmbf 23534 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
8 | | itgmulc2nc.2 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
9 | 7, 8 | mbfmptcl 23404 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
10 | 4, 9 | mulcld 10060 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 · 𝐵) ∈ ℂ) |
11 | 10 | adantlr 751 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (𝐶 · 𝐵) ∈ ℂ) |
12 | | elfzelz 12342 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (0...3) → 𝑘 ∈
ℤ) |
13 | 12 | ad2antlr 763 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → 𝑘 ∈ ℤ) |
14 | | ax-icn 9995 |
. . . . . . . . . . . . . . 15
⊢ i ∈
ℂ |
15 | | ine0 10465 |
. . . . . . . . . . . . . . 15
⊢ i ≠
0 |
16 | | expclz 12885 |
. . . . . . . . . . . . . . 15
⊢ ((i
∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ) → (i↑𝑘) ∈
ℂ) |
17 | 14, 15, 16 | mp3an12 1414 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℤ →
(i↑𝑘) ∈
ℂ) |
18 | 13, 17 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (i↑𝑘) ∈ ℂ) |
19 | | expne0i 12892 |
. . . . . . . . . . . . . . 15
⊢ ((i
∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ) → (i↑𝑘) ≠ 0) |
20 | 14, 15, 19 | mp3an12 1414 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℤ →
(i↑𝑘) ≠
0) |
21 | 13, 20 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (i↑𝑘) ≠ 0) |
22 | 11, 18, 21 | divcld 10801 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → ((𝐶 · 𝐵) / (i↑𝑘)) ∈ ℂ) |
23 | 22 | recld 13934 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ∈ ℝ) |
24 | | 0re 10040 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
25 | | ifcl 4130 |
. . . . . . . . . . 11
⊢
(((ℜ‘((𝐶
· 𝐵) / (i↑𝑘))) ∈ ℝ ∧ 0
∈ ℝ) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ ℝ) |
26 | 23, 24, 25 | sylancl 694 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ ℝ) |
27 | 26 | rexrd 10089 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈
ℝ*) |
28 | | max1 12016 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ∈ ℝ) → 0 ≤ if(0 ≤
(ℜ‘((𝐶 ·
𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) |
29 | 24, 23, 28 | sylancr 695 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → 0 ≤ if(0 ≤
(ℜ‘((𝐶 ·
𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) |
30 | | elxrge0 12281 |
. . . . . . . . 9
⊢ (if(0
≤ (ℜ‘((𝐶
· 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ (0[,]+∞) ↔ (if(0
≤ (ℜ‘((𝐶
· 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈ ℝ* ∧ 0
≤ if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) |
31 | 27, 29, 30 | sylanbrc 698 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈
(0[,]+∞)) |
32 | | 0e0iccpnf 12283 |
. . . . . . . . 9
⊢ 0 ∈
(0[,]+∞) |
33 | 32 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,]+∞)) |
34 | 31, 33 | ifclda 4120 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ∈
(0[,]+∞)) |
35 | 34 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ∈
(0[,]+∞)) |
36 | 2, 35 | syl5eqel 2705 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ∈
(0[,]+∞)) |
37 | | eqid 2622 |
. . . . 5
⊢ (𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘((𝐶 ·
𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) |
38 | 36, 37 | fmptd 6385 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))),
0)):ℝ⟶(0[,]+∞)) |
39 | 9 | recld 13934 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℝ) |
40 | 39 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℂ) |
41 | 40 | abscld 14175 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℜ‘𝐵)) ∈
ℝ) |
42 | 9 | imcld 13935 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℝ) |
43 | 42 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℂ) |
44 | 43 | abscld 14175 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℑ‘𝐵)) ∈
ℝ) |
45 | 41, 44 | readdcld 10069 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))) ∈ ℝ) |
46 | 40 | absge0d 14183 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤
(abs‘(ℜ‘𝐵))) |
47 | 43 | absge0d 14183 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤
(abs‘(ℑ‘𝐵))) |
48 | 41, 44, 46, 47 | addge0d 10603 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))) |
49 | | elrege0 12278 |
. . . . . . . . . . . 12
⊢
(((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))) ∈ (0[,)+∞) ↔
(((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))) ∈ ℝ ∧ 0 ≤
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))))) |
50 | 45, 48, 49 | sylanbrc 698 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))) ∈ (0[,)+∞)) |
51 | | 0e0icopnf 12282 |
. . . . . . . . . . . 12
⊢ 0 ∈
(0[,)+∞) |
52 | 51 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,)+∞)) |
53 | 50, 52 | ifclda 4120 |
. . . . . . . . . 10
⊢ (𝜑 → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) ∈
(0[,)+∞)) |
54 | 53 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) ∈
(0[,)+∞)) |
55 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
56 | 54, 55 | fmptd 6385 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))),
0)):ℝ⟶(0[,)+∞)) |
57 | | reex 10027 |
. . . . . . . . . . . . . 14
⊢ ℝ
∈ V |
58 | 57 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℝ ∈
V) |
59 | | elrege0 12278 |
. . . . . . . . . . . . . . . 16
⊢
((abs‘(ℜ‘𝐵)) ∈ (0[,)+∞) ↔
((abs‘(ℜ‘𝐵)) ∈ ℝ ∧ 0 ≤
(abs‘(ℜ‘𝐵)))) |
60 | 41, 46, 59 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℜ‘𝐵)) ∈
(0[,)+∞)) |
61 | 60, 52 | ifclda 4120 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) ∈
(0[,)+∞)) |
62 | 61 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) ∈
(0[,)+∞)) |
63 | | elrege0 12278 |
. . . . . . . . . . . . . . . 16
⊢
((abs‘(ℑ‘𝐵)) ∈ (0[,)+∞) ↔
((abs‘(ℑ‘𝐵)) ∈ ℝ ∧ 0 ≤
(abs‘(ℑ‘𝐵)))) |
64 | 44, 47, 63 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℑ‘𝐵)) ∈
(0[,)+∞)) |
65 | 64, 52 | ifclda 4120 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0) ∈
(0[,)+∞)) |
66 | 65 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0) ∈
(0[,)+∞)) |
67 | | eqidd 2623 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) |
68 | | eqidd 2623 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))) |
69 | 58, 62, 66, 67, 68 | offval2 6914 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))) = (𝑥 ∈ ℝ ↦ (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)))) |
70 | | iftrue 4092 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) = (abs‘(ℜ‘𝐵))) |
71 | | iftrue 4092 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0) =
(abs‘(ℑ‘𝐵))) |
72 | 70, 71 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) =
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))) |
73 | | iftrue 4092 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) = ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))) |
74 | 72, 73 | eqtr4d 2659 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
75 | | 00id 10211 |
. . . . . . . . . . . . . . 15
⊢ (0 + 0) =
0 |
76 | | iffalse 4095 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) = 0) |
77 | | iffalse 4095 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0) = 0) |
78 | 76, 77 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = (0 +
0)) |
79 | | iffalse 4095 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) = 0) |
80 | 75, 78, 79 | 3eqtr4a 2682 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
81 | 74, 80 | pm2.61i 176 |
. . . . . . . . . . . . 13
⊢ (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) |
82 | 81 | mpteq2i 4741 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ ↦
(if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
83 | 69, 82 | syl6req 2673 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)))) |
84 | 83 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))) =
(∫2‘((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))))) |
85 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) |
86 | 9 | iblcn 23565 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1
∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1))) |
87 | 5, 86 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1)) |
88 | 87 | simpld 475 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈
𝐿1) |
89 | 8, 5, 85, 88, 39 | iblabsnclem 33473 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
(abs‘(ℜ‘𝐵)), 0))) ∈ ℝ)) |
90 | 89 | simpld 475 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∈ MblFn) |
91 | 62, 85 | fmptd 6385 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)),
0)):ℝ⟶(0[,)+∞)) |
92 | 89 | simprd 479 |
. . . . . . . . . . 11
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
(abs‘(ℜ‘𝐵)), 0))) ∈ ℝ) |
93 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) |
94 | 66, 93 | fmptd 6385 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)),
0)):ℝ⟶(0[,)+∞)) |
95 | 87 | simprd 479 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1) |
96 | 8, 5, 93, 95, 42 | iblabsnclem 33473 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
(abs‘(ℑ‘𝐵)), 0))) ∈ ℝ)) |
97 | 96 | simprd 479 |
. . . . . . . . . . 11
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
(abs‘(ℑ‘𝐵)), 0))) ∈ ℝ) |
98 | 90, 91, 92, 94, 97 | itg2addnc 33464 |
. . . . . . . . . 10
⊢ (𝜑 →
(∫2‘((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)))) =
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))))) |
99 | 84, 98 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))) =
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))))) |
100 | 92, 97 | readdcld 10069 |
. . . . . . . . 9
⊢ (𝜑 →
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)))) ∈
ℝ) |
101 | 99, 100 | eqeltrd 2701 |
. . . . . . . 8
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))) ∈
ℝ) |
102 | 3 | abscld 14175 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘𝐶) ∈
ℝ) |
103 | 3 | absge0d 14183 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (abs‘𝐶)) |
104 | | elrege0 12278 |
. . . . . . . . 9
⊢
((abs‘𝐶)
∈ (0[,)+∞) ↔ ((abs‘𝐶) ∈ ℝ ∧ 0 ≤
(abs‘𝐶))) |
105 | 102, 103,
104 | sylanbrc 698 |
. . . . . . . 8
⊢ (𝜑 → (abs‘𝐶) ∈
(0[,)+∞)) |
106 | 56, 101, 105 | itg2mulc 23514 |
. . . . . . 7
⊢ (𝜑 →
(∫2‘((ℝ × {(abs‘𝐶)}) ∘𝑓 ·
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)))) = ((abs‘𝐶) ·
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))))) |
107 | 102 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘𝐶) ∈
ℝ) |
108 | | fconstmpt 5163 |
. . . . . . . . . . 11
⊢ (ℝ
× {(abs‘𝐶)}) =
(𝑥 ∈ ℝ ↦
(abs‘𝐶)) |
109 | 108 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ ×
{(abs‘𝐶)}) = (𝑥 ∈ ℝ ↦
(abs‘𝐶))) |
110 | | eqidd 2623 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0))) |
111 | 58, 107, 54, 109, 110 | offval2 6914 |
. . . . . . . . 9
⊢ (𝜑 → ((ℝ ×
{(abs‘𝐶)})
∘𝑓 · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0))) = (𝑥 ∈ ℝ ↦ ((abs‘𝐶) · if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)))) |
112 | 73 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 → ((abs‘𝐶) · if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) = ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))))) |
113 | | iftrue 4092 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0) = ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))))) |
114 | 112, 113 | eqtr4d 2659 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 → ((abs‘𝐶) · if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) = if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0)) |
115 | 114 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐶) · if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) = if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0)) |
116 | 102 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (abs‘𝐶) ∈
ℂ) |
117 | 116 | mul01d 10235 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((abs‘𝐶) · 0) =
0) |
118 | 117 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → ((abs‘𝐶) · 0) = 0) |
119 | 79 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) = 0) |
120 | 119 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → ((abs‘𝐶) · if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) = ((abs‘𝐶) · 0)) |
121 | | iffalse 4095 |
. . . . . . . . . . . . 13
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0) = 0) |
122 | 121 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0) = 0) |
123 | 118, 120,
122 | 3eqtr4d 2666 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → ((abs‘𝐶) · if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) = if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0)) |
124 | 115, 123 | pm2.61dan 832 |
. . . . . . . . . 10
⊢ (𝜑 → ((abs‘𝐶) · if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) = if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0)) |
125 | 124 | mpteq2dv 4745 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ ((abs‘𝐶) · if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0))) |
126 | 111, 125 | eqtrd 2656 |
. . . . . . . 8
⊢ (𝜑 → ((ℝ ×
{(abs‘𝐶)})
∘𝑓 · (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0))) |
127 | 126 | fveq2d 6195 |
. . . . . . 7
⊢ (𝜑 →
(∫2‘((ℝ × {(abs‘𝐶)}) ∘𝑓 ·
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)))) =
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, ((abs‘𝐶) ·
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0)))) |
128 | 99 | oveq2d 6666 |
. . . . . . 7
⊢ (𝜑 → ((abs‘𝐶) ·
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)))) = ((abs‘𝐶) ·
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)))))) |
129 | 106, 127,
128 | 3eqtr3d 2664 |
. . . . . 6
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, ((abs‘𝐶) ·
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0))) = ((abs‘𝐶) ·
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)))))) |
130 | 102, 100 | remulcld 10070 |
. . . . . 6
⊢ (𝜑 → ((abs‘𝐶) ·
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))))) ∈
ℝ) |
131 | 129, 130 | eqeltrd 2701 |
. . . . 5
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, ((abs‘𝐶) ·
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0))) ∈
ℝ) |
132 | 131 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, ((abs‘𝐶) ·
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0))) ∈
ℝ) |
133 | 102 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐶) ∈ ℝ) |
134 | 133, 45 | remulcld 10070 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))) ∈ ℝ) |
135 | 134 | rexrd 10089 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))) ∈
ℝ*) |
136 | 103 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (abs‘𝐶)) |
137 | 133, 45, 136, 48 | mulge0d 10604 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ ((abs‘𝐶) ·
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))))) |
138 | | elxrge0 12281 |
. . . . . . . . 9
⊢
(((abs‘𝐶)
· ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))) ∈ (0[,]+∞)
↔ (((abs‘𝐶)
· ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))) ∈ ℝ*
∧ 0 ≤ ((abs‘𝐶)
· ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))))) |
139 | 135, 137,
138 | sylanbrc 698 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))) ∈ (0[,]+∞)) |
140 | 32 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,]+∞)) |
141 | 139, 140 | ifclda 4120 |
. . . . . . 7
⊢ (𝜑 → if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0) ∈
(0[,]+∞)) |
142 | 141 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0) ∈
(0[,]+∞)) |
143 | | eqid 2622 |
. . . . . 6
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0)) |
144 | 142, 143 | fmptd 6385 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))),
0)):ℝ⟶(0[,]+∞)) |
145 | 9 | abscld 14175 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈ ℝ) |
146 | 133, 145 | remulcld 10070 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐶) · (abs‘𝐵)) ∈ ℝ) |
147 | 146 | adantlr 751 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐶) · (abs‘𝐵)) ∈ ℝ) |
148 | 134 | adantlr 751 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))) ∈ ℝ) |
149 | 22 | releabsd 14190 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ≤ (abs‘((𝐶 · 𝐵) / (i↑𝑘)))) |
150 | 11, 18, 21 | absdivd 14194 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘((𝐶 · 𝐵) / (i↑𝑘))) = ((abs‘(𝐶 · 𝐵)) / (abs‘(i↑𝑘)))) |
151 | | elfznn0 12433 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ (0...3) → 𝑘 ∈
ℕ0) |
152 | | absexp 14044 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((i
∈ ℂ ∧ 𝑘
∈ ℕ0) → (abs‘(i↑𝑘)) = ((abs‘i)↑𝑘)) |
153 | 14, 151, 152 | sylancr 695 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (0...3) →
(abs‘(i↑𝑘)) =
((abs‘i)↑𝑘)) |
154 | | absi 14026 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(abs‘i) = 1 |
155 | 154 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((abs‘i)↑𝑘) = (1↑𝑘) |
156 | | 1exp 12889 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ℤ →
(1↑𝑘) =
1) |
157 | 12, 156 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ (0...3) →
(1↑𝑘) =
1) |
158 | 155, 157 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (0...3) →
((abs‘i)↑𝑘) =
1) |
159 | 153, 158 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (0...3) →
(abs‘(i↑𝑘)) =
1) |
160 | 159 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (0...3) →
((abs‘(𝐶 ·
𝐵)) /
(abs‘(i↑𝑘))) =
((abs‘(𝐶 ·
𝐵)) / 1)) |
161 | 160 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → ((abs‘(𝐶 · 𝐵)) / (abs‘(i↑𝑘))) = ((abs‘(𝐶 · 𝐵)) / 1)) |
162 | 10 | abscld 14175 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐶 · 𝐵)) ∈ ℝ) |
163 | 162 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐶 · 𝐵)) ∈ ℂ) |
164 | 163 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐶 · 𝐵)) ∈ ℂ) |
165 | 164 | div1d 10793 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → ((abs‘(𝐶 · 𝐵)) / 1) = (abs‘(𝐶 · 𝐵))) |
166 | 150, 161,
165 | 3eqtrd 2660 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘((𝐶 · 𝐵) / (i↑𝑘))) = (abs‘(𝐶 · 𝐵))) |
167 | 4, 9 | absmuld 14193 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐶 · 𝐵)) = ((abs‘𝐶) · (abs‘𝐵))) |
168 | 167 | adantlr 751 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐶 · 𝐵)) = ((abs‘𝐶) · (abs‘𝐵))) |
169 | 166, 168 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (abs‘((𝐶 · 𝐵) / (i↑𝑘))) = ((abs‘𝐶) · (abs‘𝐵))) |
170 | 149, 169 | breqtrd 4679 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ≤ ((abs‘𝐶) · (abs‘𝐵))) |
171 | | mulcl 10020 |
. . . . . . . . . . . . . . . . . 18
⊢ ((i
∈ ℂ ∧ (ℑ‘𝐵) ∈ ℂ) → (i ·
(ℑ‘𝐵)) ∈
ℂ) |
172 | 14, 43, 171 | sylancr 695 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (i · (ℑ‘𝐵)) ∈
ℂ) |
173 | 40, 172 | abstrid 14195 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘((ℜ‘𝐵) + (i ·
(ℑ‘𝐵)))) ≤
((abs‘(ℜ‘𝐵)) + (abs‘(i ·
(ℑ‘𝐵))))) |
174 | 9 | replimd 13937 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = ((ℜ‘𝐵) + (i · (ℑ‘𝐵)))) |
175 | 174 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) = (abs‘((ℜ‘𝐵) + (i ·
(ℑ‘𝐵))))) |
176 | | absmul 14034 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((i
∈ ℂ ∧ (ℑ‘𝐵) ∈ ℂ) → (abs‘(i
· (ℑ‘𝐵))) = ((abs‘i) ·
(abs‘(ℑ‘𝐵)))) |
177 | 14, 43, 176 | sylancr 695 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(i ·
(ℑ‘𝐵))) =
((abs‘i) · (abs‘(ℑ‘𝐵)))) |
178 | 154 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . 19
⊢
((abs‘i) · (abs‘(ℑ‘𝐵))) = (1 ·
(abs‘(ℑ‘𝐵))) |
179 | 177, 178 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(i ·
(ℑ‘𝐵))) = (1
· (abs‘(ℑ‘𝐵)))) |
180 | 44 | recnd 10068 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℑ‘𝐵)) ∈
ℂ) |
181 | 180 | mulid2d 10058 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1 ·
(abs‘(ℑ‘𝐵))) = (abs‘(ℑ‘𝐵))) |
182 | 179, 181 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℑ‘𝐵)) = (abs‘(i ·
(ℑ‘𝐵)))) |
183 | 182 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))) = ((abs‘(ℜ‘𝐵)) + (abs‘(i ·
(ℑ‘𝐵))))) |
184 | 173, 175,
183 | 3brtr4d 4685 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ≤ ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))) |
185 | 145, 45, 133, 136, 184 | lemul2ad 10964 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐶) · (abs‘𝐵)) ≤ ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))))) |
186 | 185 | adantlr 751 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → ((abs‘𝐶) · (abs‘𝐵)) ≤ ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))))) |
187 | 23, 147, 148, 170, 186 | letrd 10194 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ≤ ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))))) |
188 | 137 | adantlr 751 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → 0 ≤ ((abs‘𝐶) ·
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))))) |
189 | | breq1 4656 |
. . . . . . . . . . . . 13
⊢
((ℜ‘((𝐶
· 𝐵) / (i↑𝑘))) = if(0 ≤
(ℜ‘((𝐶 ·
𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) → ((ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) ≤ ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))) ↔ if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))))) |
190 | | breq1 4656 |
. . . . . . . . . . . . 13
⊢ (0 = if(0
≤ (ℜ‘((𝐶
· 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) → (0 ≤ ((abs‘𝐶) ·
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))) ↔ if(0 ≤
(ℜ‘((𝐶 ·
𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))))) |
191 | 189, 190 | ifboth 4124 |
. . . . . . . . . . . 12
⊢
(((ℜ‘((𝐶
· 𝐵) / (i↑𝑘))) ≤ ((abs‘𝐶) ·
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))) ∧ 0 ≤
((abs‘𝐶) ·
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))))) → if(0 ≤
(ℜ‘((𝐶 ·
𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))))) |
192 | 187, 188,
191 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))))) |
193 | | iftrue 4092 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) = if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) |
194 | 193 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) = if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) |
195 | 113 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0) = ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))))) |
196 | 192, 194,
195 | 3brtr4d 4685 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0)) |
197 | 196 | ex 450 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0))) |
198 | | 0le0 11110 |
. . . . . . . . . . 11
⊢ 0 ≤
0 |
199 | 198 | a1i 11 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → 0 ≤ 0) |
200 | | iffalse 4095 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) = 0) |
201 | 199, 200,
121 | 3brtr4d 4685 |
. . . . . . . . 9
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0)) |
202 | 197, 201 | pm2.61d1 171 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0)) |
203 | 2, 202 | syl5eqbr 4688 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0)) |
204 | 203 | ralrimivw 2967 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → ∀𝑥 ∈ ℝ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0)) |
205 | 57 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → ℝ ∈
V) |
206 | | eqidd 2623 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) |
207 | | eqidd 2623 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0))) |
208 | 205, 36, 142, 206, 207 | ofrfval2 6915 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → ((𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) ∘𝑟 ≤
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0)) ↔ ∀𝑥 ∈ ℝ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0))) |
209 | 204, 208 | mpbird 247 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) ∘𝑟 ≤
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0))) |
210 | | itg2le 23506 |
. . . . 5
⊢ (((𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘((𝐶 ·
𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)):ℝ⟶(0[,]+∞) ∧
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0)):ℝ⟶(0[,]+∞)
∧ (𝑥 ∈ ℝ
↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘((𝐶 ·
𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) ∘𝑟 ≤
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴, ((abs‘𝐶) · ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))), 0))) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, ((abs‘𝐶) ·
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0)))) |
211 | 38, 144, 209, 210 | syl3anc 1326 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, ((abs‘𝐶) ·
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0)))) |
212 | | itg2lecl 23505 |
. . . 4
⊢ (((𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘((𝐶 ·
𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)):ℝ⟶(0[,]+∞) ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, ((abs‘𝐶) ·
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0))) ∈ ℝ ∧
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, ((abs‘𝐶) ·
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))), 0)))) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ∈ ℝ) |
213 | 38, 132, 211, 212 | syl3anc 1326 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ∈ ℝ) |
214 | 213 | ralrimiva 2966 |
. 2
⊢ (𝜑 → ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ∈ ℝ) |
215 | | eqidd 2623 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) |
216 | | eqidd 2623 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))) = (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))) |
217 | 215, 216,
10 | isibl2 23533 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘((𝐶 · 𝐵) / (i↑𝑘)))), (ℜ‘((𝐶 · 𝐵) / (i↑𝑘))), 0))) ∈ ℝ))) |
218 | 1, 214, 217 | mpbir2and 957 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈
𝐿1) |