Proof of Theorem pserdv
Step | Hyp | Ref
| Expression |
1 | | dvfcn 23672 |
. . . . 5
⊢ (ℂ
D 𝐹):dom (ℂ D 𝐹)⟶ℂ |
2 | | ssid 3624 |
. . . . . . . . 9
⊢ ℂ
⊆ ℂ |
3 | 2 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℂ ⊆
ℂ) |
4 | | pserf.g |
. . . . . . . . . 10
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) |
5 | | pserf.f |
. . . . . . . . . 10
⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) |
6 | | pserf.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
7 | | pserf.r |
. . . . . . . . . 10
⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) |
8 | | psercn.s |
. . . . . . . . . 10
⊢ 𝑆 = (◡abs “ (0[,)𝑅)) |
9 | | psercn.m |
. . . . . . . . . 10
⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) |
10 | 4, 5, 6, 7, 8, 9 | psercn 24180 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (𝑆–cn→ℂ)) |
11 | | cncff 22696 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑆–cn→ℂ) → 𝐹:𝑆⟶ℂ) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝑆⟶ℂ) |
13 | | cnvimass 5485 |
. . . . . . . . . . 11
⊢ (◡abs “ (0[,)𝑅)) ⊆ dom abs |
14 | | absf 14077 |
. . . . . . . . . . . 12
⊢
abs:ℂ⟶ℝ |
15 | 14 | fdmi 6052 |
. . . . . . . . . . 11
⊢ dom abs =
ℂ |
16 | 13, 15 | sseqtri 3637 |
. . . . . . . . . 10
⊢ (◡abs “ (0[,)𝑅)) ⊆ ℂ |
17 | 8, 16 | eqsstri 3635 |
. . . . . . . . 9
⊢ 𝑆 ⊆
ℂ |
18 | 17 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
19 | 3, 12, 18 | dvbss 23665 |
. . . . . . 7
⊢ (𝜑 → dom (ℂ D 𝐹) ⊆ 𝑆) |
20 | 2 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ℂ ⊆
ℂ) |
21 | 12 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐹:𝑆⟶ℂ) |
22 | 17 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑆 ⊆ ℂ) |
23 | | pserdv.b |
. . . . . . . . . . . . . 14
⊢ 𝐵 = (0(ball‘(abs ∘
− ))(((abs‘𝑎) +
𝑀) / 2)) |
24 | | cnxmet 22576 |
. . . . . . . . . . . . . . . 16
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
25 | 24 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
26 | | 0cnd 10033 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 0 ∈ ℂ) |
27 | 18 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ ℂ) |
28 | 27 | abscld 14175 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) ∈ ℝ) |
29 | 4, 5, 6, 7, 8, 9 | psercnlem1 24179 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑀 ∈ ℝ+ ∧
(abs‘𝑎) < 𝑀 ∧ 𝑀 < 𝑅)) |
30 | 29 | simp1d 1073 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ∈
ℝ+) |
31 | 30 | rpred 11872 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ∈ ℝ) |
32 | 28, 31 | readdcld 10069 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((abs‘𝑎) + 𝑀) ∈ ℝ) |
33 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 0 ∈ ℝ) |
34 | 27 | absge0d 14183 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 0 ≤ (abs‘𝑎)) |
35 | 28, 30 | ltaddrpd 11905 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) < ((abs‘𝑎) + 𝑀)) |
36 | 33, 28, 32, 34, 35 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 0 < ((abs‘𝑎) + 𝑀)) |
37 | 32, 36 | elrpd 11869 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((abs‘𝑎) + 𝑀) ∈
ℝ+) |
38 | 37 | rphalfcld 11884 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (((abs‘𝑎) + 𝑀) / 2) ∈
ℝ+) |
39 | 38 | rpxrd 11873 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (((abs‘𝑎) + 𝑀) / 2) ∈
ℝ*) |
40 | | blssm 22223 |
. . . . . . . . . . . . . . 15
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ (((abs‘𝑎) +
𝑀) / 2) ∈
ℝ*) → (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2)) ⊆
ℂ) |
41 | 25, 26, 39, 40 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2)) ⊆
ℂ) |
42 | 23, 41 | syl5eqss 3649 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐵 ⊆ ℂ) |
43 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
44 | 43 | cnfldtop 22587 |
. . . . . . . . . . . . . . . 16
⊢
(TopOpen‘ℂfld) ∈ Top |
45 | 43 | cnfldtopon 22586 |
. . . . . . . . . . . . . . . . . 18
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
46 | 45 | toponunii 20721 |
. . . . . . . . . . . . . . . . 17
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
47 | 46 | restid 16094 |
. . . . . . . . . . . . . . . 16
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
48 | 44, 47 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
49 | 48 | eqcomi 2631 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
50 | 43, 49 | dvres 23675 |
. . . . . . . . . . . . 13
⊢
(((ℂ ⊆ ℂ ∧ 𝐹:𝑆⟶ℂ) ∧ (𝑆 ⊆ ℂ ∧ 𝐵 ⊆ ℂ)) → (ℂ D (𝐹 ↾ 𝐵)) = ((ℂ D 𝐹) ↾
((int‘(TopOpen‘ℂfld))‘𝐵))) |
51 | 20, 21, 22, 42, 50 | syl22anc 1327 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (ℂ D (𝐹 ↾ 𝐵)) = ((ℂ D 𝐹) ↾
((int‘(TopOpen‘ℂfld))‘𝐵))) |
52 | | resss 5422 |
. . . . . . . . . . . 12
⊢ ((ℂ
D 𝐹) ↾
((int‘(TopOpen‘ℂfld))‘𝐵)) ⊆ (ℂ D 𝐹) |
53 | 51, 52 | syl6eqss 3655 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (ℂ D (𝐹 ↾ 𝐵)) ⊆ (ℂ D 𝐹)) |
54 | | dmss 5323 |
. . . . . . . . . . 11
⊢ ((ℂ
D (𝐹 ↾ 𝐵)) ⊆ (ℂ D 𝐹) → dom (ℂ D (𝐹 ↾ 𝐵)) ⊆ dom (ℂ D 𝐹)) |
55 | 53, 54 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → dom (ℂ D (𝐹 ↾ 𝐵)) ⊆ dom (ℂ D 𝐹)) |
56 | 4, 5, 6, 7, 8, 9 | pserdvlem1 24181 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((((abs‘𝑎) + 𝑀) / 2) ∈ ℝ+ ∧
(abs‘𝑎) <
(((abs‘𝑎) + 𝑀) / 2) ∧ (((abs‘𝑎) + 𝑀) / 2) < 𝑅)) |
57 | 4, 5, 6, 7, 8, 56 | psercnlem2 24178 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 ∈ (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2)) ∧ (0(ball‘(abs
∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⊆ (◡abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))) ∧ (◡abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))) ⊆ 𝑆)) |
58 | 57 | simp1d 1073 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2))) |
59 | 58, 23 | syl6eleqr 2712 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ 𝐵) |
60 | 4, 5, 6, 7, 8, 9, 23 | pserdvlem2 24182 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (ℂ D (𝐹 ↾ 𝐵)) = (𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) |
61 | 60 | dmeqd 5326 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → dom (ℂ D (𝐹 ↾ 𝐵)) = dom (𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) |
62 | | dmmptg 5632 |
. . . . . . . . . . . . 13
⊢
(∀𝑦 ∈
𝐵 Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)) ∈ V → dom (𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) = 𝐵) |
63 | | sumex 14418 |
. . . . . . . . . . . . . 14
⊢
Σ𝑘 ∈
ℕ0 (((𝑘 +
1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)) ∈ V |
64 | 63 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝐵 → Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)) ∈ V) |
65 | 62, 64 | mprg 2926 |
. . . . . . . . . . . 12
⊢ dom
(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) = 𝐵 |
66 | 61, 65 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → dom (ℂ D (𝐹 ↾ 𝐵)) = 𝐵) |
67 | 59, 66 | eleqtrrd 2704 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ dom (ℂ D (𝐹 ↾ 𝐵))) |
68 | 55, 67 | sseldd 3604 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ dom (ℂ D 𝐹)) |
69 | 68 | ex 450 |
. . . . . . . 8
⊢ (𝜑 → (𝑎 ∈ 𝑆 → 𝑎 ∈ dom (ℂ D 𝐹))) |
70 | 69 | ssrdv 3609 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ⊆ dom (ℂ D 𝐹)) |
71 | 19, 70 | eqssd 3620 |
. . . . . 6
⊢ (𝜑 → dom (ℂ D 𝐹) = 𝑆) |
72 | 71 | feq2d 6031 |
. . . . 5
⊢ (𝜑 → ((ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ ↔ (ℂ
D 𝐹):𝑆⟶ℂ)) |
73 | 1, 72 | mpbii 223 |
. . . 4
⊢ (𝜑 → (ℂ D 𝐹):𝑆⟶ℂ) |
74 | 73 | feqmptd 6249 |
. . 3
⊢ (𝜑 → (ℂ D 𝐹) = (𝑎 ∈ 𝑆 ↦ ((ℂ D 𝐹)‘𝑎))) |
75 | | ffun 6048 |
. . . . . . 7
⊢ ((ℂ
D 𝐹):dom (ℂ D 𝐹)⟶ℂ → Fun
(ℂ D 𝐹)) |
76 | 1, 75 | mp1i 13 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → Fun (ℂ D 𝐹)) |
77 | | funssfv 6209 |
. . . . . 6
⊢ ((Fun
(ℂ D 𝐹) ∧
(ℂ D (𝐹 ↾ 𝐵)) ⊆ (ℂ D 𝐹) ∧ 𝑎 ∈ dom (ℂ D (𝐹 ↾ 𝐵))) → ((ℂ D 𝐹)‘𝑎) = ((ℂ D (𝐹 ↾ 𝐵))‘𝑎)) |
78 | 76, 53, 67, 77 | syl3anc 1326 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((ℂ D 𝐹)‘𝑎) = ((ℂ D (𝐹 ↾ 𝐵))‘𝑎)) |
79 | 60 | fveq1d 6193 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((ℂ D (𝐹 ↾ 𝐵))‘𝑎) = ((𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))‘𝑎)) |
80 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑦 = 𝑎 → (𝑦↑𝑘) = (𝑎↑𝑘)) |
81 | 80 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑦 = 𝑎 → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎↑𝑘))) |
82 | 81 | sumeq2sdv 14435 |
. . . . . . 7
⊢ (𝑦 = 𝑎 → Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)) = Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎↑𝑘))) |
83 | | eqid 2622 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) = (𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) |
84 | | sumex 14418 |
. . . . . . 7
⊢
Σ𝑘 ∈
ℕ0 (((𝑘 +
1) · (𝐴‘(𝑘 + 1))) · (𝑎↑𝑘)) ∈ V |
85 | 82, 83, 84 | fvmpt 6282 |
. . . . . 6
⊢ (𝑎 ∈ 𝐵 → ((𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))‘𝑎) = Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎↑𝑘))) |
86 | 59, 85 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))‘𝑎) = Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎↑𝑘))) |
87 | 78, 79, 86 | 3eqtrd 2660 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((ℂ D 𝐹)‘𝑎) = Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎↑𝑘))) |
88 | 87 | mpteq2dva 4744 |
. . 3
⊢ (𝜑 → (𝑎 ∈ 𝑆 ↦ ((ℂ D 𝐹)‘𝑎)) = (𝑎 ∈ 𝑆 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎↑𝑘)))) |
89 | 74, 88 | eqtrd 2656 |
. 2
⊢ (𝜑 → (ℂ D 𝐹) = (𝑎 ∈ 𝑆 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎↑𝑘)))) |
90 | | oveq1 6657 |
. . . . 5
⊢ (𝑎 = 𝑦 → (𝑎↑𝑘) = (𝑦↑𝑘)) |
91 | 90 | oveq2d 6666 |
. . . 4
⊢ (𝑎 = 𝑦 → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎↑𝑘)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) |
92 | 91 | sumeq2sdv 14435 |
. . 3
⊢ (𝑎 = 𝑦 → Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎↑𝑘)) = Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) |
93 | 92 | cbvmptv 4750 |
. 2
⊢ (𝑎 ∈ 𝑆 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎↑𝑘))) = (𝑦 ∈ 𝑆 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) |
94 | 89, 93 | syl6eq 2672 |
1
⊢ (𝜑 → (ℂ D 𝐹) = (𝑦 ∈ 𝑆 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) |