Step | Hyp | Ref
| Expression |
1 | | fsumcvg4.s |
. 2
⊢ 𝑆 =
(ℤ≥‘𝑀) |
2 | | fsumcvg4.m |
. 2
⊢ (𝜑 → 𝑀 ∈ ℤ) |
3 | | fsumcvg4.f |
. 2
⊢ (𝜑 → (◡𝐹 “ (ℂ ∖ {0})) ∈
Fin) |
4 | | fsumcvg4.c |
. . . . 5
⊢ (𝜑 → 𝐹:𝑆⟶ℂ) |
5 | | ffun 5961 |
. . . . 5
⊢ (𝐹:𝑆⟶ℂ → Fun 𝐹) |
6 | | difpreima 6251 |
. . . . 5
⊢ (Fun
𝐹 → (◡𝐹 “ (ℂ ∖ {0})) = ((◡𝐹 “ ℂ) ∖ (◡𝐹 “ {0}))) |
7 | 4, 5, 6 | 3syl 18 |
. . . 4
⊢ (𝜑 → (◡𝐹 “ (ℂ ∖ {0})) = ((◡𝐹 “ ℂ) ∖ (◡𝐹 “ {0}))) |
8 | | difss 3699 |
. . . 4
⊢ ((◡𝐹 “ ℂ) ∖ (◡𝐹 “ {0})) ⊆ (◡𝐹 “ ℂ) |
9 | 7, 8 | syl6eqss 3618 |
. . 3
⊢ (𝜑 → (◡𝐹 “ (ℂ ∖ {0})) ⊆
(◡𝐹 “ ℂ)) |
10 | | fimacnv 6255 |
. . . 4
⊢ (𝐹:𝑆⟶ℂ → (◡𝐹 “ ℂ) = 𝑆) |
11 | 4, 10 | syl 17 |
. . 3
⊢ (𝜑 → (◡𝐹 “ ℂ) = 𝑆) |
12 | 9, 11 | sseqtrd 3604 |
. 2
⊢ (𝜑 → (◡𝐹 “ (ℂ ∖ {0})) ⊆
𝑆) |
13 | | exmidd 431 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ∨ ¬
𝑘 ∈ (◡𝐹 “ (ℂ ∖
{0})))) |
14 | | eqid 2610 |
. . . . . . 7
⊢ (𝐹‘𝑘) = (𝐹‘𝑘) |
15 | 14 | biantru 525 |
. . . . . 6
⊢ (𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ↔
(𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ∧ (𝐹‘𝑘) = (𝐹‘𝑘))) |
16 | 15 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ↔
(𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ∧ (𝐹‘𝑘) = (𝐹‘𝑘)))) |
17 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢
(ℤ≥‘𝑀) ∈ V |
18 | 1, 17 | eqeltri 2684 |
. . . . . . . . . . . . . 14
⊢ 𝑆 ∈ V |
19 | 18 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ∈ V) |
20 | | 0nn0 11184 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℕ0 |
21 | 20 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈
ℕ0) |
22 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (ℂ
∖ {0}) = (ℂ ∖ {0}) |
23 | 22 | ffs2 28891 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ V ∧ 0 ∈
ℕ0 ∧ 𝐹:𝑆⟶ℂ) → (𝐹 supp 0) = (◡𝐹 “ (ℂ ∖
{0}))) |
24 | 19, 21, 4, 23 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 supp 0) = (◡𝐹 “ (ℂ ∖
{0}))) |
25 | | ffn 5958 |
. . . . . . . . . . . . . 14
⊢ (𝐹:𝑆⟶ℂ → 𝐹 Fn 𝑆) |
26 | 4, 25 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 Fn 𝑆) |
27 | | suppvalfn 7189 |
. . . . . . . . . . . . 13
⊢ ((𝐹 Fn 𝑆 ∧ 𝑆 ∈ V ∧ 0 ∈
ℕ0) → (𝐹 supp 0) = {𝑘 ∈ 𝑆 ∣ (𝐹‘𝑘) ≠ 0}) |
28 | 26, 19, 21, 27 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 supp 0) = {𝑘 ∈ 𝑆 ∣ (𝐹‘𝑘) ≠ 0}) |
29 | 24, 28 | eqtr3d 2646 |
. . . . . . . . . . 11
⊢ (𝜑 → (◡𝐹 “ (ℂ ∖ {0})) = {𝑘 ∈ 𝑆 ∣ (𝐹‘𝑘) ≠ 0}) |
30 | 29 | eleq2d 2673 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ↔ 𝑘 ∈ {𝑘 ∈ 𝑆 ∣ (𝐹‘𝑘) ≠ 0})) |
31 | | rabid 3095 |
. . . . . . . . . 10
⊢ (𝑘 ∈ {𝑘 ∈ 𝑆 ∣ (𝐹‘𝑘) ≠ 0} ↔ (𝑘 ∈ 𝑆 ∧ (𝐹‘𝑘) ≠ 0)) |
32 | 30, 31 | syl6bb 275 |
. . . . . . . . 9
⊢ (𝜑 → (𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ↔
(𝑘 ∈ 𝑆 ∧ (𝐹‘𝑘) ≠ 0))) |
33 | 32 | baibd 946 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ↔
(𝐹‘𝑘) ≠ 0)) |
34 | 33 | necon2bbid 2825 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → ((𝐹‘𝑘) = 0 ↔ ¬ 𝑘 ∈ (◡𝐹 “ (ℂ ∖
{0})))) |
35 | 34 | biimprd 237 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (¬ 𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) →
(𝐹‘𝑘) = 0)) |
36 | 35 | pm4.71d 664 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (¬ 𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ↔
(¬ 𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ∧ (𝐹‘𝑘) = 0))) |
37 | 16, 36 | orbi12d 742 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → ((𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ∨ ¬
𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0}))) ↔
((𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ∧ (𝐹‘𝑘) = (𝐹‘𝑘)) ∨ (¬ 𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ∧ (𝐹‘𝑘) = 0)))) |
38 | 13, 37 | mpbid 221 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → ((𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ∧ (𝐹‘𝑘) = (𝐹‘𝑘)) ∨ (¬ 𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ∧ (𝐹‘𝑘) = 0))) |
39 | | eqif 4076 |
. . 3
⊢ ((𝐹‘𝑘) = if(𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})), (𝐹‘𝑘), 0) ↔ ((𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ∧ (𝐹‘𝑘) = (𝐹‘𝑘)) ∨ (¬ 𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ∧ (𝐹‘𝑘) = 0))) |
40 | 38, 39 | sylibr 223 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝐹‘𝑘) = if(𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})), (𝐹‘𝑘), 0)) |
41 | 12 | sselda 3568 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0}))) →
𝑘 ∈ 𝑆) |
42 | 4 | ffvelrnda 6267 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝐹‘𝑘) ∈ ℂ) |
43 | 41, 42 | syldan 486 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0}))) →
(𝐹‘𝑘) ∈ ℂ) |
44 | 1, 2, 3, 12, 40, 43 | fsumcvg3 14307 |
1
⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) |