Theorem fsumclf

Description: Closure of a finite sum of complex numbers A ( k ) . A version of fsumcl using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	fsumclf.ph	$$⊢Ⅎk\phi$$
	fsumclf.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	fsumclf.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
Assertion	fsumclf	$$⊢\phi \to \sum _{k\in A}B\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		fsumclf.ph	$$⊢Ⅎk\phi$$
2		fsumclf.a	$$⊢\phi \to A\in \mathrm{Fin}$$
3		fsumclf.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
4		csbeq1a	$$⊢k=j\to B=⦋j/k⦌B$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}jB$$
6		nfcsb1v	$$⊢\underset{\_}{Ⅎ}k⦋j/k⦌B$$
7	4 5 6	cbvsum	$$⊢\sum _{k\in A}B=\sum _{j\in A}⦋j/k⦌B$$
8	7	a1i	$$⊢\phi \to \sum _{k\in A}B=\sum _{j\in A}⦋j/k⦌B$$
9		nfv	$$⊢Ⅎkj\in A$$
10	1 9	nfan	$$⊢Ⅎk\left(\phi \wedge j\in A\right)$$
11	6	nfel1	$$⊢Ⅎk⦋j/k⦌B\in ℂ$$
12	10 11	nfim	$$⊢Ⅎk\left(\left(\phi \wedge j\in A\right)\to ⦋j/k⦌B\in ℂ\right)$$
13		eleq1w	$$⊢k=j\to \left(k\in A\leftrightarrow j\in A\right)$$
14	13	anbi2d	$$⊢k=j\to \left(\left(\phi \wedge k\in A\right)\leftrightarrow \left(\phi \wedge j\in A\right)\right)$$
15	4	eleq1d	$$⊢k=j\to \left(B\in ℂ\leftrightarrow ⦋j/k⦌B\in ℂ\right)$$
16	14 15	imbi12d	$$⊢k=j\to \left(\left(\left(\phi \wedge k\in A\right)\to B\in ℂ\right)\leftrightarrow \left(\left(\phi \wedge j\in A\right)\to ⦋j/k⦌B\in ℂ\right)\right)$$
17	12 16 3	chvarfv	$$⊢\left(\phi \wedge j\in A\right)\to ⦋j/k⦌B\in ℂ$$
18	2 17	fsumcl	$$⊢\phi \to \sum _{j\in A}⦋j/k⦌B\in ℂ$$
19	8 18	eqeltrd	$$⊢\phi \to \sum _{k\in A}B\in ℂ$$