Step | Hyp | Ref
| Expression |
1 | | iblabs.2 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈
𝐿1) |
2 | | iblmbf 23534 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
4 | | iblabs.1 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
5 | 3, 4 | mbfmptcl 23404 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
6 | | eqidd 2623 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)) |
7 | | absf 14077 |
. . . . . 6
⊢
abs:ℂ⟶ℝ |
8 | 7 | a1i 11 |
. . . . 5
⊢ (𝜑 →
abs:ℂ⟶ℝ) |
9 | 8 | feqmptd 6249 |
. . . 4
⊢ (𝜑 → abs = (𝑦 ∈ ℂ ↦ (abs‘𝑦))) |
10 | | fveq2 6191 |
. . . 4
⊢ (𝑦 = 𝐵 → (abs‘𝑦) = (abs‘𝐵)) |
11 | 5, 6, 9, 10 | fmptco 6396 |
. . 3
⊢ (𝜑 → (abs ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) = (𝑥 ∈ 𝐴 ↦ (abs‘𝐵))) |
12 | | eqid 2622 |
. . . . 5
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
13 | 5, 12 | fmptd 6385 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
14 | | ax-resscn 9993 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
15 | | ssid 3624 |
. . . . . . 7
⊢ ℂ
⊆ ℂ |
16 | | cncfss 22702 |
. . . . . . 7
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℂ–cn→ℝ) ⊆ (ℂ–cn→ℂ)) |
17 | 14, 15, 16 | mp2an 708 |
. . . . . 6
⊢
(ℂ–cn→ℝ)
⊆ (ℂ–cn→ℂ) |
18 | | abscncf 22704 |
. . . . . 6
⊢ abs
∈ (ℂ–cn→ℝ) |
19 | 17, 18 | sselii 3600 |
. . . . 5
⊢ abs
∈ (ℂ–cn→ℂ) |
20 | 19 | a1i 11 |
. . . 4
⊢ (𝜑 → abs ∈
(ℂ–cn→ℂ)) |
21 | | cncombf 23425 |
. . . 4
⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ ∧ abs ∈
(ℂ–cn→ℂ)) →
(abs ∘ (𝑥 ∈
𝐴 ↦ 𝐵)) ∈ MblFn) |
22 | 3, 13, 20, 21 | syl3anc 1326 |
. . 3
⊢ (𝜑 → (abs ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ MblFn) |
23 | 11, 22 | eqeltrrd 2702 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ MblFn) |
24 | 5 | abscld 14175 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈ ℝ) |
25 | 24 | rexrd 10089 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈
ℝ*) |
26 | 5 | absge0d 14183 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (abs‘𝐵)) |
27 | | elxrge0 12281 |
. . . . . . 7
⊢
((abs‘𝐵)
∈ (0[,]+∞) ↔ ((abs‘𝐵) ∈ ℝ* ∧ 0 ≤
(abs‘𝐵))) |
28 | 25, 26, 27 | sylanbrc 698 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈ (0[,]+∞)) |
29 | | 0e0iccpnf 12283 |
. . . . . . 7
⊢ 0 ∈
(0[,]+∞) |
30 | 29 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,]+∞)) |
31 | 28, 30 | ifclda 4120 |
. . . . 5
⊢ (𝜑 → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ∈
(0[,]+∞)) |
32 | 31 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ∈
(0[,]+∞)) |
33 | | eqid 2622 |
. . . 4
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)) |
34 | 32, 33 | fmptd 6385 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵),
0)):ℝ⟶(0[,]+∞)) |
35 | | reex 10027 |
. . . . . . . . 9
⊢ ℝ
∈ V |
36 | 35 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ ∈
V) |
37 | 5 | recld 13934 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℝ) |
38 | 37 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℂ) |
39 | 38 | abscld 14175 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℜ‘𝐵)) ∈
ℝ) |
40 | 38 | absge0d 14183 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤
(abs‘(ℜ‘𝐵))) |
41 | | elrege0 12278 |
. . . . . . . . . . 11
⊢
((abs‘(ℜ‘𝐵)) ∈ (0[,)+∞) ↔
((abs‘(ℜ‘𝐵)) ∈ ℝ ∧ 0 ≤
(abs‘(ℜ‘𝐵)))) |
42 | 39, 40, 41 | sylanbrc 698 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℜ‘𝐵)) ∈
(0[,)+∞)) |
43 | | 0e0icopnf 12282 |
. . . . . . . . . . 11
⊢ 0 ∈
(0[,)+∞) |
44 | 43 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,)+∞)) |
45 | 42, 44 | ifclda 4120 |
. . . . . . . . 9
⊢ (𝜑 → if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) ∈
(0[,)+∞)) |
46 | 45 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) ∈
(0[,)+∞)) |
47 | 5 | imcld 13935 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℝ) |
48 | 47 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℂ) |
49 | 48 | abscld 14175 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℑ‘𝐵)) ∈
ℝ) |
50 | 48 | absge0d 14183 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤
(abs‘(ℑ‘𝐵))) |
51 | | elrege0 12278 |
. . . . . . . . . . 11
⊢
((abs‘(ℑ‘𝐵)) ∈ (0[,)+∞) ↔
((abs‘(ℑ‘𝐵)) ∈ ℝ ∧ 0 ≤
(abs‘(ℑ‘𝐵)))) |
52 | 49, 50, 51 | sylanbrc 698 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℑ‘𝐵)) ∈
(0[,)+∞)) |
53 | 52, 44 | ifclda 4120 |
. . . . . . . . 9
⊢ (𝜑 → if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0) ∈
(0[,)+∞)) |
54 | 53 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0) ∈
(0[,)+∞)) |
55 | | eqidd 2623 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) |
56 | | eqidd 2623 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))) |
57 | 36, 46, 54, 55, 56 | offval2 6914 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))) = (𝑥 ∈ ℝ ↦ (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)))) |
58 | | iftrue 4092 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) = (abs‘(ℜ‘𝐵))) |
59 | | iftrue 4092 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0) =
(abs‘(ℑ‘𝐵))) |
60 | 58, 59 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) =
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))) |
61 | | iftrue 4092 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) = ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))) |
62 | 60, 61 | eqtr4d 2659 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
63 | | 00id 10211 |
. . . . . . . . . 10
⊢ (0 + 0) =
0 |
64 | | iffalse 4095 |
. . . . . . . . . . 11
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) = 0) |
65 | | iffalse 4095 |
. . . . . . . . . . 11
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0) = 0) |
66 | 64, 65 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = (0 +
0)) |
67 | | iffalse 4095 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) = 0) |
68 | 63, 66, 67 | 3eqtr4a 2682 |
. . . . . . . . 9
⊢ (¬
𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
69 | 62, 68 | pm2.61i 176 |
. . . . . . . 8
⊢ (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) |
70 | 69 | mpteq2i 4741 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ ↦
(if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
71 | 57, 70 | syl6req 2673 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)))) |
72 | 71 | fveq2d 6195 |
. . . . 5
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))) =
(∫2‘((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))))) |
73 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) |
74 | 5 | iblcn 23565 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1
∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1))) |
75 | 1, 74 | mpbid 222 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1)) |
76 | 75 | simpld 475 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈
𝐿1) |
77 | 4, 1, 73, 76, 37 | iblabslem 23594 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
(abs‘(ℜ‘𝐵)), 0))) ∈ ℝ)) |
78 | 77 | simpld 475 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∈ MblFn) |
79 | 46, 73 | fmptd 6385 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)),
0)):ℝ⟶(0[,)+∞)) |
80 | 77 | simprd 479 |
. . . . . 6
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
(abs‘(ℜ‘𝐵)), 0))) ∈ ℝ) |
81 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) |
82 | 75 | simprd 479 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1) |
83 | 4, 1, 81, 82, 47 | iblabslem 23594 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
(abs‘(ℑ‘𝐵)), 0))) ∈ ℝ)) |
84 | 83 | simpld 475 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) ∈
MblFn) |
85 | 54, 81 | fmptd 6385 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)),
0)):ℝ⟶(0[,)+∞)) |
86 | 83 | simprd 479 |
. . . . . 6
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
(abs‘(ℑ‘𝐵)), 0))) ∈ ℝ) |
87 | 78, 79, 80, 84, 85, 86 | itg2add 23526 |
. . . . 5
⊢ (𝜑 →
(∫2‘((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)))) =
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))))) |
88 | 72, 87 | eqtrd 2656 |
. . . 4
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))) =
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))))) |
89 | 80, 86 | readdcld 10069 |
. . . 4
⊢ (𝜑 →
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)))) ∈
ℝ) |
90 | 88, 89 | eqeltrd 2701 |
. . 3
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))) ∈
ℝ) |
91 | 39, 49 | readdcld 10069 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))) ∈ ℝ) |
92 | 91 | rexrd 10089 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))) ∈
ℝ*) |
93 | 39, 49, 40, 50 | addge0d 10603 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))) |
94 | | elxrge0 12281 |
. . . . . . . 8
⊢
(((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))) ∈ (0[,]+∞) ↔
(((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))) ∈ ℝ*
∧ 0 ≤ ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))))) |
95 | 92, 93, 94 | sylanbrc 698 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))) ∈ (0[,]+∞)) |
96 | 95, 30 | ifclda 4120 |
. . . . . 6
⊢ (𝜑 → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) ∈
(0[,]+∞)) |
97 | 96 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) ∈
(0[,]+∞)) |
98 | | eqid 2622 |
. . . . 5
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
99 | 97, 98 | fmptd 6385 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))),
0)):ℝ⟶(0[,]+∞)) |
100 | | ax-icn 9995 |
. . . . . . . . . . . 12
⊢ i ∈
ℂ |
101 | | mulcl 10020 |
. . . . . . . . . . . 12
⊢ ((i
∈ ℂ ∧ (ℑ‘𝐵) ∈ ℂ) → (i ·
(ℑ‘𝐵)) ∈
ℂ) |
102 | 100, 48, 101 | sylancr 695 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (i · (ℑ‘𝐵)) ∈
ℂ) |
103 | 38, 102 | abstrid 14195 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘((ℜ‘𝐵) + (i ·
(ℑ‘𝐵)))) ≤
((abs‘(ℜ‘𝐵)) + (abs‘(i ·
(ℑ‘𝐵))))) |
104 | 5 | replimd 13937 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = ((ℜ‘𝐵) + (i · (ℑ‘𝐵)))) |
105 | 104 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) = (abs‘((ℜ‘𝐵) + (i ·
(ℑ‘𝐵))))) |
106 | | absmul 14034 |
. . . . . . . . . . . . 13
⊢ ((i
∈ ℂ ∧ (ℑ‘𝐵) ∈ ℂ) → (abs‘(i
· (ℑ‘𝐵))) = ((abs‘i) ·
(abs‘(ℑ‘𝐵)))) |
107 | 100, 48, 106 | sylancr 695 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(i ·
(ℑ‘𝐵))) =
((abs‘i) · (abs‘(ℑ‘𝐵)))) |
108 | | absi 14026 |
. . . . . . . . . . . . . 14
⊢
(abs‘i) = 1 |
109 | 108 | oveq1i 6660 |
. . . . . . . . . . . . 13
⊢
((abs‘i) · (abs‘(ℑ‘𝐵))) = (1 ·
(abs‘(ℑ‘𝐵))) |
110 | 49 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℑ‘𝐵)) ∈
ℂ) |
111 | 110 | mulid2d 10058 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1 ·
(abs‘(ℑ‘𝐵))) = (abs‘(ℑ‘𝐵))) |
112 | 109, 111 | syl5eq 2668 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘i) ·
(abs‘(ℑ‘𝐵))) = (abs‘(ℑ‘𝐵))) |
113 | 107, 112 | eqtr2d 2657 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℑ‘𝐵)) = (abs‘(i ·
(ℑ‘𝐵)))) |
114 | 113 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))) = ((abs‘(ℜ‘𝐵)) + (abs‘(i ·
(ℑ‘𝐵))))) |
115 | 103, 105,
114 | 3brtr4d 4685 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ≤ ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))) |
116 | | iftrue 4092 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) = (abs‘𝐵)) |
117 | 116 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) = (abs‘𝐵)) |
118 | 61 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) = ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))) |
119 | 115, 117,
118 | 3brtr4d 4685 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
120 | 119 | ex 450 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0))) |
121 | | 0le0 11110 |
. . . . . . . . 9
⊢ 0 ≤
0 |
122 | 121 | a1i 11 |
. . . . . . . 8
⊢ (¬
𝑥 ∈ 𝐴 → 0 ≤ 0) |
123 | | iffalse 4095 |
. . . . . . . 8
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) = 0) |
124 | 122, 123,
67 | 3brtr4d 4685 |
. . . . . . 7
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
125 | 120, 124 | pm2.61d1 171 |
. . . . . 6
⊢ (𝜑 → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
126 | 125 | ralrimivw 2967 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ℝ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
127 | | eqidd 2623 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))) |
128 | | eqidd 2623 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0))) |
129 | 36, 32, 97, 127, 128 | ofrfval2 6915 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)) ∘𝑟 ≤
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)) ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0))) |
130 | 126, 129 | mpbird 247 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)) ∘𝑟 ≤
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))) |
131 | | itg2le 23506 |
. . . 4
⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)):ℝ⟶(0[,]+∞) ∧
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))),
0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)) ∘𝑟 ≤
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘𝐵), 0))) ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)))) |
132 | 34, 99, 130, 131 | syl3anc 1326 |
. . 3
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘𝐵), 0))) ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)))) |
133 | | itg2lecl 23505 |
. . 3
⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)):ℝ⟶(0[,]+∞) ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))) ∈ ℝ ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘𝐵), 0))) ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)))) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘𝐵), 0))) ∈
ℝ) |
134 | 34, 90, 132, 133 | syl3anc 1326 |
. 2
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘𝐵), 0))) ∈
ℝ) |
135 | 24, 26 | iblpos 23559 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘𝐵), 0))) ∈
ℝ))) |
136 | 23, 134, 135 | mpbir2and 957 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈
𝐿1) |