Proof of Theorem iblabsnc
Step | Hyp | Ref
| Expression |
1 | | iblabsnc.m |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ MblFn) |
2 | | iblabsnc.2 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈
𝐿1) |
3 | | iblmbf 24932 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
4 | 2, 3 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn) |
5 | | iblabsnc.1 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
6 | 4, 5 | mbfmptcl 24800 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
7 | 6 | abscld 15148 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈ ℝ) |
8 | 7 | rexrd 11025 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈
ℝ*) |
9 | 6 | absge0d 15156 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (abs‘𝐵)) |
10 | | elxrge0 13189 |
. . . . . . 7
⊢
((abs‘𝐵)
∈ (0[,]+∞) ↔ ((abs‘𝐵) ∈ ℝ* ∧ 0 ≤
(abs‘𝐵))) |
11 | 8, 9, 10 | sylanbrc 583 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈ (0[,]+∞)) |
12 | | 0e0iccpnf 13191 |
. . . . . . 7
⊢ 0 ∈
(0[,]+∞) |
13 | 12 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,]+∞)) |
14 | 11, 13 | ifclda 4494 |
. . . . 5
⊢ (𝜑 → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ∈
(0[,]+∞)) |
15 | 14 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ∈
(0[,]+∞)) |
16 | 15 | fmpttd 6989 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵),
0)):ℝ⟶(0[,]+∞)) |
17 | | reex 10962 |
. . . . . . . . 9
⊢ ℝ
∈ V |
18 | 17 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ ∈
V) |
19 | 6 | recld 14905 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℝ) |
20 | 19 | recnd 11003 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘𝐵) ∈ ℂ) |
21 | 20 | abscld 15148 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℜ‘𝐵)) ∈
ℝ) |
22 | 20 | absge0d 15156 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤
(abs‘(ℜ‘𝐵))) |
23 | | elrege0 13186 |
. . . . . . . . . . 11
⊢
((abs‘(ℜ‘𝐵)) ∈ (0[,)+∞) ↔
((abs‘(ℜ‘𝐵)) ∈ ℝ ∧ 0 ≤
(abs‘(ℜ‘𝐵)))) |
24 | 21, 22, 23 | sylanbrc 583 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℜ‘𝐵)) ∈
(0[,)+∞)) |
25 | | 0e0icopnf 13190 |
. . . . . . . . . . 11
⊢ 0 ∈
(0[,)+∞) |
26 | 25 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐴) → 0 ∈
(0[,)+∞)) |
27 | 24, 26 | ifclda 4494 |
. . . . . . . . 9
⊢ (𝜑 → if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) ∈
(0[,)+∞)) |
28 | 27 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) ∈
(0[,)+∞)) |
29 | 6 | imcld 14906 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℝ) |
30 | 29 | recnd 11003 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℑ‘𝐵) ∈ ℂ) |
31 | 30 | abscld 15148 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℑ‘𝐵)) ∈
ℝ) |
32 | 30 | absge0d 15156 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤
(abs‘(ℑ‘𝐵))) |
33 | | elrege0 13186 |
. . . . . . . . . . 11
⊢
((abs‘(ℑ‘𝐵)) ∈ (0[,)+∞) ↔
((abs‘(ℑ‘𝐵)) ∈ ℝ ∧ 0 ≤
(abs‘(ℑ‘𝐵)))) |
34 | 31, 32, 33 | sylanbrc 583 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℑ‘𝐵)) ∈
(0[,)+∞)) |
35 | 34, 26 | ifclda 4494 |
. . . . . . . . 9
⊢ (𝜑 → if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0) ∈
(0[,)+∞)) |
36 | 35 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0) ∈
(0[,)+∞)) |
37 | | eqidd 2739 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) |
38 | | eqidd 2739 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))) |
39 | 18, 28, 36, 37, 38 | offval2 7553 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∘f + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))) = (𝑥 ∈ ℝ ↦ (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)))) |
40 | | iftrue 4465 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) = (abs‘(ℜ‘𝐵))) |
41 | | iftrue 4465 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0) =
(abs‘(ℑ‘𝐵))) |
42 | 40, 41 | oveq12d 7293 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) =
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))) |
43 | | iftrue 4465 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) = ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))) |
44 | 42, 43 | eqtr4d 2781 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
45 | | 00id 11150 |
. . . . . . . . . 10
⊢ (0 + 0) =
0 |
46 | | iffalse 4468 |
. . . . . . . . . . 11
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) = 0) |
47 | | iffalse 4468 |
. . . . . . . . . . 11
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0) = 0) |
48 | 46, 47 | oveq12d 7293 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = (0 +
0)) |
49 | | iffalse 4468 |
. . . . . . . . . 10
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) = 0) |
50 | 45, 48, 49 | 3eqtr4a 2804 |
. . . . . . . . 9
⊢ (¬
𝑥 ∈ 𝐴 → (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
51 | 44, 50 | pm2.61i 182 |
. . . . . . . 8
⊢ (if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) |
52 | 51 | mpteq2i 5179 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ ↦
(if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0) + if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
53 | 39, 52 | eqtr2di 2795 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∘f + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)))) |
54 | 53 | fveq2d 6778 |
. . . . 5
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))) =
(∫2‘((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∘f + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))))) |
55 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) |
56 | 6 | iblcn 24963 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1
∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1))) |
57 | 2, 56 | mpbid 231 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1)) |
58 | 57 | simpld 495 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈
𝐿1) |
59 | 5, 2, 55, 58, 19 | iblabsnclem 35840 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
(abs‘(ℜ‘𝐵)), 0))) ∈ ℝ)) |
60 | 59 | simpld 495 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∈ MblFn) |
61 | 28 | fmpttd 6989 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)),
0)):ℝ⟶(0[,)+∞)) |
62 | 59 | simprd 496 |
. . . . . 6
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
(abs‘(ℜ‘𝐵)), 0))) ∈ ℝ) |
63 | 36 | fmpttd 6989 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)),
0)):ℝ⟶(0[,)+∞)) |
64 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) |
65 | 57 | simprd 496 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈
𝐿1) |
66 | 5, 2, 64, 65, 29 | iblabsnclem 35840 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
(abs‘(ℑ‘𝐵)), 0))) ∈ ℝ)) |
67 | 66 | simprd 496 |
. . . . . 6
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
(abs‘(ℑ‘𝐵)), 0))) ∈ ℝ) |
68 | 60, 61, 62, 63, 67 | itg2addnc 35831 |
. . . . 5
⊢ (𝜑 →
(∫2‘((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0)) ∘f + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)))) =
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))))) |
69 | 54, 68 | eqtrd 2778 |
. . . 4
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))) =
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0))))) |
70 | 62, 67 | readdcld 11004 |
. . . 4
⊢ (𝜑 →
((∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℜ‘𝐵)), 0))) + (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(ℑ‘𝐵)), 0)))) ∈
ℝ) |
71 | 69, 70 | eqeltrd 2839 |
. . 3
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))) ∈
ℝ) |
72 | 21, 31 | readdcld 11004 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))) ∈ ℝ) |
73 | 72 | rexrd 11025 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))) ∈
ℝ*) |
74 | 21, 31, 22, 32 | addge0d 11551 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵)))) |
75 | | elxrge0 13189 |
. . . . . . . 8
⊢
(((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))) ∈ (0[,]+∞) ↔
(((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))) ∈ ℝ*
∧ 0 ≤ ((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))))) |
76 | 73, 74, 75 | sylanbrc 583 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))) ∈ (0[,]+∞)) |
77 | 76, 13 | ifclda 4494 |
. . . . . 6
⊢ (𝜑 → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) ∈
(0[,]+∞)) |
78 | 77 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) ∈
(0[,]+∞)) |
79 | 78 | fmpttd 6989 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))),
0)):ℝ⟶(0[,]+∞)) |
80 | | ax-icn 10930 |
. . . . . . . . . . 11
⊢ i ∈
ℂ |
81 | | mulcl 10955 |
. . . . . . . . . . 11
⊢ ((i
∈ ℂ ∧ (ℑ‘𝐵) ∈ ℂ) → (i ·
(ℑ‘𝐵)) ∈
ℂ) |
82 | 80, 30, 81 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (i · (ℑ‘𝐵)) ∈
ℂ) |
83 | 20, 82 | abstrid 15168 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘((ℜ‘𝐵) + (i ·
(ℑ‘𝐵)))) ≤
((abs‘(ℜ‘𝐵)) + (abs‘(i ·
(ℑ‘𝐵))))) |
84 | | iftrue 4465 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) = (abs‘𝐵)) |
85 | 84 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) = (abs‘𝐵)) |
86 | 6 | replimd 14908 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = ((ℜ‘𝐵) + (i · (ℑ‘𝐵)))) |
87 | 86 | fveq2d 6778 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) = (abs‘((ℜ‘𝐵) + (i ·
(ℑ‘𝐵))))) |
88 | 85, 87 | eqtrd 2778 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) = (abs‘((ℜ‘𝐵) + (i ·
(ℑ‘𝐵))))) |
89 | 43 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) = ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵)))) |
90 | | absmul 15006 |
. . . . . . . . . . . . 13
⊢ ((i
∈ ℂ ∧ (ℑ‘𝐵) ∈ ℂ) → (abs‘(i
· (ℑ‘𝐵))) = ((abs‘i) ·
(abs‘(ℑ‘𝐵)))) |
91 | 80, 30, 90 | sylancr 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(i ·
(ℑ‘𝐵))) =
((abs‘i) · (abs‘(ℑ‘𝐵)))) |
92 | | absi 14998 |
. . . . . . . . . . . . . 14
⊢
(abs‘i) = 1 |
93 | 92 | oveq1i 7285 |
. . . . . . . . . . . . 13
⊢
((abs‘i) · (abs‘(ℑ‘𝐵))) = (1 ·
(abs‘(ℑ‘𝐵))) |
94 | 31 | recnd 11003 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℑ‘𝐵)) ∈
ℂ) |
95 | 94 | mulid2d 10993 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1 ·
(abs‘(ℑ‘𝐵))) = (abs‘(ℑ‘𝐵))) |
96 | 93, 95 | eqtrid 2790 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘i) ·
(abs‘(ℑ‘𝐵))) = (abs‘(ℑ‘𝐵))) |
97 | 91, 96 | eqtr2d 2779 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(ℑ‘𝐵)) = (abs‘(i ·
(ℑ‘𝐵)))) |
98 | 97 | oveq2d 7291 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))) = ((abs‘(ℜ‘𝐵)) + (abs‘(i ·
(ℑ‘𝐵))))) |
99 | 89, 98 | eqtrd 2778 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0) = ((abs‘(ℜ‘𝐵)) + (abs‘(i ·
(ℑ‘𝐵))))) |
100 | 83, 88, 99 | 3brtr4d 5106 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
101 | 100 | ex 413 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0))) |
102 | | 0le0 12074 |
. . . . . . . . 9
⊢ 0 ≤
0 |
103 | 102 | a1i 11 |
. . . . . . . 8
⊢ (¬
𝑥 ∈ 𝐴 → 0 ≤ 0) |
104 | | iffalse 4468 |
. . . . . . . 8
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) = 0) |
105 | 103, 104,
49 | 3brtr4d 5106 |
. . . . . . 7
⊢ (¬
𝑥 ∈ 𝐴 → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
106 | 101, 105 | pm2.61d1 180 |
. . . . . 6
⊢ (𝜑 → if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
107 | 106 | ralrimivw 3104 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ℝ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) |
108 | | eqidd 2739 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0))) |
109 | | eqidd 2739 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0))) |
110 | 18, 15, 78, 108, 109 | ofrfval2 7554 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)) ∘r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0)) ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0) ≤ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0))) |
111 | 107, 110 | mpbird 256 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)) ∘r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0))) |
112 | | itg2le 24904 |
. . . 4
⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)):ℝ⟶(0[,]+∞) ∧
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))),
0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)) ∘r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, ((abs‘(ℜ‘𝐵)) +
(abs‘(ℑ‘𝐵))), 0))) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘𝐵), 0))) ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)))) |
113 | 16, 79, 111, 112 | syl3anc 1370 |
. . 3
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘𝐵), 0))) ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)))) |
114 | | itg2lecl 24903 |
. . 3
⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘𝐵), 0)):ℝ⟶(0[,]+∞) ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0))) ∈ ℝ ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘𝐵), 0))) ≤
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴,
((abs‘(ℜ‘𝐵)) + (abs‘(ℑ‘𝐵))), 0)))) →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘𝐵), 0))) ∈
ℝ) |
115 | 16, 71, 113, 114 | syl3anc 1370 |
. 2
⊢ (𝜑 →
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘𝐵), 0))) ∈
ℝ) |
116 | 7, 9 | iblpos 24957 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ MblFn ∧
(∫2‘(𝑥
∈ ℝ ↦ if(𝑥
∈ 𝐴, (abs‘𝐵), 0))) ∈
ℝ))) |
117 | 1, 115, 116 | mpbir2and 710 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈
𝐿1) |