Theorem fsumcvg4

Description: A serie with finite support is a finite sum, and therefore converges. (Contributed by Thierry Arnoux, 6-Sep-2017) (Revised by Thierry Arnoux, 1-Sep-2019)

	Ref	Expression
Hypotheses	fsumcvg4.s	$$⊢S={\mathbb{Z}}_{\ge M}$$
	fsumcvg4.m	$$⊢\phi \to M\in \mathbb{Z}$$
	fsumcvg4.c	$$⊢\phi \to F:S⟶ℂ$$
	fsumcvg4.f	$$⊢\phi \to F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\in \mathrm{Fin}$$
Assertion	fsumcvg4	$$⊢\phi \to seqM\left(+,F\right)\in \mathrm{dom}⇝$$

Proof

Step	Hyp	Ref	Expression
1		fsumcvg4.s	$$⊢S={\mathbb{Z}}_{\ge M}$$
2		fsumcvg4.m	$$⊢\phi \to M\in \mathbb{Z}$$
3		fsumcvg4.c	$$⊢\phi \to F:S⟶ℂ$$
4		fsumcvg4.f	$$⊢\phi \to F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\in \mathrm{Fin}$$
5		ffun	$$⊢F:S⟶ℂ\to \mathrm{Fun}F$$
6		difpreima	$$⊢\mathrm{Fun}F\to F^{-1}\left[ℂ\setminus \left\{0\right\}\right]=F^{-1}\left[ℂ\right]\setminus F^{-1}\left[\left\{0\right\}\right]$$
7	3 5 6	3syl	$$⊢\phi \to F^{-1}\left[ℂ\setminus \left\{0\right\}\right]=F^{-1}\left[ℂ\right]\setminus F^{-1}\left[\left\{0\right\}\right]$$
8		difss	$$⊢F^{-1}\left[ℂ\right]\setminus F^{-1}\left[\left\{0\right\}\right]\subseteq F^{-1}\left[ℂ\right]$$
9	7 8	eqsstrdi	$$⊢\phi \to F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\subseteq F^{-1}\left[ℂ\right]$$
10		fimacnv	$$⊢F:S⟶ℂ\to F^{-1}\left[ℂ\right]=S$$
11	3 10	syl	$$⊢\phi \to F^{-1}\left[ℂ\right]=S$$
12	9 11	sseqtrd	$$⊢\phi \to F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\subseteq S$$
13		exmidd	$$⊢\left(\phi \wedge k\in S\right)\to \left(k\in F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\vee \neg k\in F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\right)$$
14		eqid	$$⊢F\left(k\right)=F\left(k\right)$$
15	14	biantru	$$⊢k\in F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\leftrightarrow \left(k\in F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\wedge F\left(k\right)=F\left(k\right)\right)$$
16	15	a1i	$$⊢\left(\phi \wedge k\in S\right)\to \left(k\in F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\leftrightarrow \left(k\in F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\wedge F\left(k\right)=F\left(k\right)\right)\right)$$
17	1	fvexi	$$⊢S\in \mathrm{V}$$
18	17	a1i	$$⊢\phi \to S\in \mathrm{V}$$
19		0nn0	$$⊢0\in {\mathbb{N}}_0$$
20	19	a1i	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
21		eqid	$$⊢ℂ\setminus \left\{0\right\}=ℂ\setminus \left\{0\right\}$$
22	21	ffs2	$$⊢\left(S\in \mathrm{V}\wedge 0\in {\mathbb{N}}_0\wedge F:S⟶ℂ\right)\to F\mathrm{supp}0=F^{-1}\left[ℂ\setminus \left\{0\right\}\right]$$
23	18 20 3 22	syl3anc	$$⊢\phi \to F\mathrm{supp}0=F^{-1}\left[ℂ\setminus \left\{0\right\}\right]$$
24	3	ffnd	$$⊢\phi \to FFnS$$
25		suppvalfn	$$⊢\left(FFnS\wedge S\in \mathrm{V}\wedge 0\in {\mathbb{N}}_0\right)\to F\mathrm{supp}0=\left\{k\in S|F\left(k\right)\ne 0\right\}$$
26	24 18 20 25	syl3anc	$$⊢\phi \to F\mathrm{supp}0=\left\{k\in S|F\left(k\right)\ne 0\right\}$$
27	23 26	eqtr3d	$$⊢\phi \to F^{-1}\left[ℂ\setminus \left\{0\right\}\right]=\left\{k\in S|F\left(k\right)\ne 0\right\}$$
28	27	eleq2d	$$⊢\phi \to \left(k\in F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\leftrightarrow k\in \left\{k\in S|F\left(k\right)\ne 0\right\}\right)$$
29		rabid	$$⊢k\in \left\{k\in S|F\left(k\right)\ne 0\right\}\leftrightarrow \left(k\in S\wedge F\left(k\right)\ne 0\right)$$
30	28 29	bitrdi	$$⊢\phi \to \left(k\in F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\leftrightarrow \left(k\in S\wedge F\left(k\right)\ne 0\right)\right)$$
31	30	baibd	$$⊢\left(\phi \wedge k\in S\right)\to \left(k\in F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\leftrightarrow F\left(k\right)\ne 0\right)$$
32	31	necon2bbid	$$⊢\left(\phi \wedge k\in S\right)\to \left(F\left(k\right)=0\leftrightarrow \neg k\in F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\right)$$
33	32	biimprd	$$⊢\left(\phi \wedge k\in S\right)\to \left(\neg k\in F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to F\left(k\right)=0\right)$$
34	33	pm4.71d	$$⊢\left(\phi \wedge k\in S\right)\to \left(\neg k\in F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\leftrightarrow \left(\neg k\in F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\wedge F\left(k\right)=0\right)\right)$$
35	16 34	orbi12d	$$⊢\left(\phi \wedge k\in S\right)\to \left(\left(k\in F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\vee \neg k\in F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\right)\leftrightarrow \left(\left(k\in F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\wedge F\left(k\right)=F\left(k\right)\right)\vee \left(\neg k\in F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\wedge F\left(k\right)=0\right)\right)\right)$$
36	13 35	mpbid	$$⊢\left(\phi \wedge k\in S\right)\to \left(\left(k\in F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\wedge F\left(k\right)=F\left(k\right)\right)\vee \left(\neg k\in F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\wedge F\left(k\right)=0\right)\right)$$
37		eqif	$$⊢F\left(k\right)=if\left(k\in F^{-1}\left[ℂ\setminus \left\{0\right\}\right],F\left(k\right),0\right)\leftrightarrow \left(\left(k\in F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\wedge F\left(k\right)=F\left(k\right)\right)\vee \left(\neg k\in F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\wedge F\left(k\right)=0\right)\right)$$
38	36 37	sylibr	$$⊢\left(\phi \wedge k\in S\right)\to F\left(k\right)=if\left(k\in F^{-1}\left[ℂ\setminus \left\{0\right\}\right],F\left(k\right),0\right)$$
39	12	sselda	$$⊢\left(\phi \wedge k\in F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\right)\to k\in S$$
40	3	ffvelrnda	$$⊢\left(\phi \wedge k\in S\right)\to F\left(k\right)\in ℂ$$
41	39 40	syldan	$$⊢\left(\phi \wedge k\in F^{-1}\left[ℂ\setminus \left\{0\right\}\right]\right)\to F\left(k\right)\in ℂ$$
42	1 2 4 12 38 41	fsumcvg3	$$⊢\phi \to seqM\left(+,F\right)\in \mathrm{dom}⇝$$