Proof of Theorem iblabsnc
Step | Hyp | Ref
| Expression |
1 | | iblabsnc.m |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ MblFn) |
2 | | iblabsnc.2 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈
𝐿1) |
3 | | iblmbf 23340 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
4 | 2, 3 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
5 | | iblabsnc.1 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
6 | 4, 5 | mbfmptcl 23210 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
7 | 6 | abscld 14023 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈ ℝ) |
8 | 7 | rexrd 9968 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈
ℝ*) |
9 | 6 | absge0d 14031 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (abs‘𝐵)) |
10 | | elxrge0 12152 |
. . . . . . 7
⊢
((abs‘𝐵)
∈ (0[,]+∞) ↔ ((abs‘𝐵) ∈ ℝ* ∧ 0 ≤
(abs‘𝐵))) |
11 | 8, 9, 10 | sylanbrc 695 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈ (0[,]+∞)) |
12 | | 0e0iccpnf 12154 |
. . . . . . 7
⊢ 0 ∈
(0[,]+∞) |
13 | 12 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,]+∞)) |
14 | 11, 13 | ifclda 4070 |
. . . . 5
⊢ (𝜑 → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ∈
(0[,]+∞)) |
15 | 14 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ∈
(0[,]+∞)) |
16 | | eqid 2610 |
. . . 4
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)) |
17 | 15, 16 | fmptd 6292 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵),
0)):ℝ⟶(0[,]+∞)) |
18 | | reex 9906 |
. . . . . . . . 9
⊢ ℝ
∈ V |
19 | 18 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ ∈
V) |
20 | 6 | recld 13782 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℝ) |
21 | 20 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℂ) |
22 | 21 | abscld 14023 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℜ‘𝐵)) ∈
ℝ) |
23 | 21 | absge0d 14031 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤
(abs‘(ℜ‘𝐵))) |
24 | | elrege0 12149 |
. . . . . . . . . . 11
⊢
((abs‘(ℜ‘𝐵)) ∈ (0[,)+∞) ↔
((abs‘(ℜ‘𝐵)) ∈ ℝ ∧ 0 ≤
(abs‘(ℜ‘𝐵)))) |
25 | 22, 23, 24 | sylanbrc 695 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℜ‘𝐵)) ∈
(0[,)+∞)) |
26 | | 0e0icopnf 12153 |
. . . . . . . . . . 11
⊢ 0 ∈
(0[,)+∞) |
27 | 26 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,)+∞)) |
28 | 25, 27 | ifclda 4070 |
. . . . . . . . 9
⊢ (𝜑 → if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) ∈
(0[,)+∞)) |
29 | 28 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) ∈
(0[,)+∞)) |
30 | 6 | imcld 13783 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℝ) |
31 | 30 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℂ) |
32 | 31 | abscld 14023 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℑ‘𝐵)) ∈
ℝ) |
33 | 31 | absge0d 14031 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤
(abs‘(ℑ‘𝐵))) |
34 | | elrege0 12149 |
. . . . . . . . . . 11
⊢
((abs‘(ℑ‘𝐵)) ∈ (0[,)+∞) ↔
((abs‘(ℑ‘𝐵)) ∈ ℝ ∧ 0 ≤
(abs‘(ℑ‘𝐵)))) |
35 | 32, 33, 34 | sylanbrc 695 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℑ‘𝐵)) ∈
(0[,)+∞)) |
36 | 35, 27 | ifclda 4070 |
. . . . . . . . 9
⊢ (𝜑 → if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0) ∈
(0[,)+∞)) |
37 | 36 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0) ∈
(0[,)+∞)) |
38 | | eqidd 2611 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) |
39 | | eqidd 2611 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))) |
40 | 19, 29, 37, 38, 39 | offval2 6812 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))) = (𝑥 ∈ ℝ ↦ (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)))) |
41 | | iftrue 4042 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) = (abs‘(ℜ‘𝐵))) |
42 | | iftrue 4042 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0) =
(abs‘(ℑ‘𝐵))) |
43 | 41, 42 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) =
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))) |
44 | | iftrue 4042 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) = ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))) |
45 | 43, 44 | eqtr4d 2647 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
46 | | 00id 10090 |
. . . . . . . . . 10
⊢ (0 + 0) =
0 |
47 | | iffalse 4045 |
. . . . . . . . . . 11
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) = 0) |
48 | | iffalse 4045 |
. . . . . . . . . . 11
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0) = 0) |
49 | 47, 48 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = (0 +
0)) |
50 | | iffalse 4045 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) = 0) |
51 | 46, 49, 50 | 3eqtr4a 2670 |
. . . . . . . . 9
⊢ (¬
𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
52 | 45, 51 | pm2.61i 175 |
. . . . . . . 8
⊢ (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) |
53 | 52 | mpteq2i 4669 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ ↦
(if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
54 | 40, 53 | syl6req 2661 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)))) |
55 | 54 | fveq2d 6107 |
. . . . 5
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))) =
(∫2‘((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))))) |
56 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) |
57 | 6 | iblcn 23371 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1
∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1))) |
58 | 2, 57 | mpbid 221 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1)) |
59 | 58 | simpld 474 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈
𝐿1) |
60 | 5, 2, 56, 59, 20 | iblabsnclem 32643 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
(abs‘(ℜ‘𝐵)), 0))) ∈ ℝ)) |
61 | 60 | simpld 474 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∈ MblFn) |
62 | 29, 56 | fmptd 6292 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)),
0)):ℝ⟶(0[,)+∞)) |
63 | 60 | simprd 478 |
. . . . . 6
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
(abs‘(ℜ‘𝐵)), 0))) ∈ ℝ) |
64 | | eqid 2610 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) |
65 | 37, 64 | fmptd 6292 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)),
0)):ℝ⟶(0[,)+∞)) |
66 | 58 | simprd 478 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1) |
67 | 5, 2, 64, 66, 30 | iblabsnclem 32643 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
(abs‘(ℑ‘𝐵)), 0))) ∈ ℝ)) |
68 | 67 | simprd 478 |
. . . . . 6
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
(abs‘(ℑ‘𝐵)), 0))) ∈ ℝ) |
69 | 61, 62, 63, 65, 68 | itg2addnc 32634 |
. . . . 5
⊢ (𝜑 →
(∫2‘((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)))) =
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))))) |
70 | 55, 69 | eqtrd 2644 |
. . . 4
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))) =
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))))) |
71 | 63, 68 | readdcld 9948 |
. . . 4
⊢ (𝜑 →
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)))) ∈
ℝ) |
72 | 70, 71 | eqeltrd 2688 |
. . 3
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))) ∈
ℝ) |
73 | 22, 32 | readdcld 9948 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))) ∈ ℝ) |
74 | 73 | rexrd 9968 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))) ∈
ℝ*) |
75 | 22, 32, 23, 33 | addge0d 10482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))) |
76 | | elxrge0 12152 |
. . . . . . . 8
⊢
(((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))) ∈ (0[,]+∞) ↔
(((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))) ∈ ℝ*
∧ 0 ≤ ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))))) |
77 | 74, 75, 76 | sylanbrc 695 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))) ∈ (0[,]+∞)) |
78 | 77, 13 | ifclda 4070 |
. . . . . 6
⊢ (𝜑 → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) ∈
(0[,]+∞)) |
79 | 78 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) ∈
(0[,]+∞)) |
80 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
81 | 79, 80 | fmptd 6292 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))),
0)):ℝ⟶(0[,]+∞)) |
82 | | ax-icn 9874 |
. . . . . . . . . . 11
⊢ i ∈
ℂ |
83 | | mulcl 9899 |
. . . . . . . . . . 11
⊢ ((i
∈ ℂ ∧ (ℑ‘𝐵) ∈ ℂ) → (i ·
(ℑ‘𝐵)) ∈
ℂ) |
84 | 82, 31, 83 | sylancr 694 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (i · (ℑ‘𝐵)) ∈
ℂ) |
85 | 21, 84 | abstrid 14043 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘((ℜ‘𝐵) + (i ·
(ℑ‘𝐵)))) ≤
((abs‘(ℜ‘𝐵)) + (abs‘(i ·
(ℑ‘𝐵))))) |
86 | | iftrue 4042 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) = (abs‘𝐵)) |
87 | 86 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) = (abs‘𝐵)) |
88 | 6 | replimd 13785 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = ((ℜ‘𝐵) + (i · (ℑ‘𝐵)))) |
89 | 88 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) = (abs‘((ℜ‘𝐵) + (i ·
(ℑ‘𝐵))))) |
90 | 87, 89 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) = (abs‘((ℜ‘𝐵) + (i ·
(ℑ‘𝐵))))) |
91 | 44 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) = ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))) |
92 | | absmul 13882 |
. . . . . . . . . . . . 13
⊢ ((i
∈ ℂ ∧ (ℑ‘𝐵) ∈ ℂ) → (abs‘(i
· (ℑ‘𝐵))) = ((abs‘i) ·
(abs‘(ℑ‘𝐵)))) |
93 | 82, 31, 92 | sylancr 694 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(i ·
(ℑ‘𝐵))) =
((abs‘i) · (abs‘(ℑ‘𝐵)))) |
94 | | absi 13874 |
. . . . . . . . . . . . . 14
⊢
(abs‘i) = 1 |
95 | 94 | oveq1i 6559 |
. . . . . . . . . . . . 13
⊢
((abs‘i) · (abs‘(ℑ‘𝐵))) = (1 ·
(abs‘(ℑ‘𝐵))) |
96 | 32 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℑ‘𝐵)) ∈
ℂ) |
97 | 96 | mulid2d 9937 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1 ·
(abs‘(ℑ‘𝐵))) = (abs‘(ℑ‘𝐵))) |
98 | 95, 97 | syl5eq 2656 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘i) ·
(abs‘(ℑ‘𝐵))) = (abs‘(ℑ‘𝐵))) |
99 | 93, 98 | eqtr2d 2645 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℑ‘𝐵)) = (abs‘(i ·
(ℑ‘𝐵)))) |
100 | 99 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))) = ((abs‘(ℜ‘𝐵)) + (abs‘(i ·
(ℑ‘𝐵))))) |
101 | 91, 100 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) = ((abs‘(ℜ‘𝐵)) + (abs‘(i ·
(ℑ‘𝐵))))) |
102 | 85, 90, 101 | 3brtr4d 4615 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
103 | 102 | ex 449 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0))) |
104 | | 0le0 10987 |
. . . . . . . . 9
⊢ 0 ≤
0 |
105 | 104 | a1i 11 |
. . . . . . . 8
⊢ (¬
𝑥 ∈ 𝐴 → 0 ≤ 0) |
106 | | iffalse 4045 |
. . . . . . . 8
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) = 0) |
107 | 105, 106,
50 | 3brtr4d 4615 |
. . . . . . 7
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
108 | 103, 107 | pm2.61d1 170 |
. . . . . 6
⊢ (𝜑 → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
109 | 108 | ralrimivw 2950 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ℝ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
110 | | eqidd 2611 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))) |
111 | | eqidd 2611 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0))) |
112 | 19, 15, 79, 110, 111 | ofrfval2 6813 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)) ∘𝑟 ≤
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)) ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0))) |
113 | 109, 112 | mpbird 246 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)) ∘𝑟 ≤
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))) |
114 | | itg2le 23312 |
. . . 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)))) |
115 | 17, 81, 113, 114 | syl3anc 1318 |
. . 3
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘𝐵), 0))) ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)))) |
116 | | itg2lecl 23311 |
. . 3
⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)):ℝ⟶(0[,]+∞) ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))) ∈ ℝ ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘𝐵), 0))) ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)))) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘𝐵), 0))) ∈
ℝ) |
117 | 17, 72, 115, 116 | syl3anc 1318 |
. 2
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘𝐵), 0))) ∈
ℝ) |
118 | 7, 9 | iblpos 23365 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘𝐵), 0))) ∈
ℝ))) |
119 | 1, 117, 118 | mpbir2and 959 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈
𝐿1) |