Step | Hyp | Ref
| Expression |
1 | | fsumcvg4.s |
. 2
⊢ 𝑆 =
(ℤ≥‘𝑀) |
2 | | fsumcvg4.m |
. 2
⊢ (𝜑 → 𝑀 ∈ ℤ) |
3 | | fsumcvg4.f |
. 2
⊢ (𝜑 → (◡𝐹 “ (ℂ ∖ {0})) ∈
Fin) |
4 | | fsumcvg4.c |
. . . . 5
⊢ (𝜑 → 𝐹:𝑆⟶ℂ) |
5 | | ffun 6517 |
. . . . 5
⊢ (𝐹:𝑆⟶ℂ → Fun 𝐹) |
6 | | difpreima 6835 |
. . . . 5
⊢ (Fun
𝐹 → (◡𝐹 “ (ℂ ∖ {0})) = ((◡𝐹 “ ℂ) ∖ (◡𝐹 “ {0}))) |
7 | 4, 5, 6 | 3syl 18 |
. . . 4
⊢ (𝜑 → (◡𝐹 “ (ℂ ∖ {0})) = ((◡𝐹 “ ℂ) ∖ (◡𝐹 “ {0}))) |
8 | | difss 4108 |
. . . 4
⊢ ((◡𝐹 “ ℂ) ∖ (◡𝐹 “ {0})) ⊆ (◡𝐹 “ ℂ) |
9 | 7, 8 | eqsstrdi 4021 |
. . 3
⊢ (𝜑 → (◡𝐹 “ (ℂ ∖ {0})) ⊆
(◡𝐹 “ ℂ)) |
10 | | fimacnv 6839 |
. . . 4
⊢ (𝐹:𝑆⟶ℂ → (◡𝐹 “ ℂ) = 𝑆) |
11 | 4, 10 | syl 17 |
. . 3
⊢ (𝜑 → (◡𝐹 “ ℂ) = 𝑆) |
12 | 9, 11 | sseqtrd 4007 |
. 2
⊢ (𝜑 → (◡𝐹 “ (ℂ ∖ {0})) ⊆
𝑆) |
13 | | exmidd 892 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ∨ ¬
𝑘 ∈ (◡𝐹 “ (ℂ ∖
{0})))) |
14 | | eqid 2821 |
. . . . . . 7
⊢ (𝐹‘𝑘) = (𝐹‘𝑘) |
15 | 14 | biantru 532 |
. . . . . 6
⊢ (𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ↔
(𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ∧ (𝐹‘𝑘) = (𝐹‘𝑘))) |
16 | 15 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ↔
(𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ∧ (𝐹‘𝑘) = (𝐹‘𝑘)))) |
17 | 1 | fvexi 6684 |
. . . . . . . . . . . . . 14
⊢ 𝑆 ∈ V |
18 | 17 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ∈ V) |
19 | | 0nn0 11913 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℕ0 |
20 | 19 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈
ℕ0) |
21 | | eqid 2821 |
. . . . . . . . . . . . . 14
⊢ (ℂ
∖ {0}) = (ℂ ∖ {0}) |
22 | 21 | ffs2 30464 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ V ∧ 0 ∈
ℕ0 ∧ 𝐹:𝑆⟶ℂ) → (𝐹 supp 0) = (◡𝐹 “ (ℂ ∖
{0}))) |
23 | 18, 20, 4, 22 | syl3anc 1367 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 supp 0) = (◡𝐹 “ (ℂ ∖
{0}))) |
24 | 4 | ffnd 6515 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 Fn 𝑆) |
25 | | suppvalfn 7837 |
. . . . . . . . . . . . 13
⊢ ((𝐹 Fn 𝑆 ∧ 𝑆 ∈ V ∧ 0 ∈
ℕ0) → (𝐹 supp 0) = {𝑘 ∈ 𝑆 ∣ (𝐹‘𝑘) ≠ 0}) |
26 | 24, 18, 20, 25 | syl3anc 1367 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 supp 0) = {𝑘 ∈ 𝑆 ∣ (𝐹‘𝑘) ≠ 0}) |
27 | 23, 26 | eqtr3d 2858 |
. . . . . . . . . . 11
⊢ (𝜑 → (◡𝐹 “ (ℂ ∖ {0})) = {𝑘 ∈ 𝑆 ∣ (𝐹‘𝑘) ≠ 0}) |
28 | 27 | eleq2d 2898 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ↔ 𝑘 ∈ {𝑘 ∈ 𝑆 ∣ (𝐹‘𝑘) ≠ 0})) |
29 | | rabid 3378 |
. . . . . . . . . 10
⊢ (𝑘 ∈ {𝑘 ∈ 𝑆 ∣ (𝐹‘𝑘) ≠ 0} ↔ (𝑘 ∈ 𝑆 ∧ (𝐹‘𝑘) ≠ 0)) |
30 | 28, 29 | syl6bb 289 |
. . . . . . . . 9
⊢ (𝜑 → (𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ↔
(𝑘 ∈ 𝑆 ∧ (𝐹‘𝑘) ≠ 0))) |
31 | 30 | baibd 542 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ↔
(𝐹‘𝑘) ≠ 0)) |
32 | 31 | necon2bbid 3059 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → ((𝐹‘𝑘) = 0 ↔ ¬ 𝑘 ∈ (◡𝐹 “ (ℂ ∖
{0})))) |
33 | 32 | biimprd 250 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (¬ 𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) →
(𝐹‘𝑘) = 0)) |
34 | 33 | pm4.71d 564 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (¬ 𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ↔
(¬ 𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ∧ (𝐹‘𝑘) = 0))) |
35 | 16, 34 | orbi12d 915 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → ((𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ∨ ¬
𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0}))) ↔
((𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ∧ (𝐹‘𝑘) = (𝐹‘𝑘)) ∨ (¬ 𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ∧ (𝐹‘𝑘) = 0)))) |
36 | 13, 35 | mpbid 234 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → ((𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ∧ (𝐹‘𝑘) = (𝐹‘𝑘)) ∨ (¬ 𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ∧ (𝐹‘𝑘) = 0))) |
37 | | eqif 4507 |
. . 3
⊢ ((𝐹‘𝑘) = if(𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})), (𝐹‘𝑘), 0) ↔ ((𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ∧ (𝐹‘𝑘) = (𝐹‘𝑘)) ∨ (¬ 𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})) ∧ (𝐹‘𝑘) = 0))) |
38 | 36, 37 | sylibr 236 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝐹‘𝑘) = if(𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0})), (𝐹‘𝑘), 0)) |
39 | 12 | sselda 3967 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0}))) →
𝑘 ∈ 𝑆) |
40 | 4 | ffvelrnda 6851 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝐹‘𝑘) ∈ ℂ) |
41 | 39, 40 | syldan 593 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (◡𝐹 “ (ℂ ∖ {0}))) →
(𝐹‘𝑘) ∈ ℂ) |
42 | 1, 2, 3, 12, 38, 41 | fsumcvg3 15086 |
1
⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) |