Theorem fsumreclf

Description: Closure of a finite sum of reals. (Contributed by Glauco Siliprandi, 21-Nov-2020)

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

Proof

Step	Hyp	Ref	Expression
1		fsumreclf.k	$$⊢Ⅎk\phi$$
2		fsumreclf.a	$$⊢\phi \to A\in \mathrm{Fin}$$
3		fsumreclf.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℝ$$
4		csbeq1a	$$⊢k=j\to B=⦋j/k⦌B$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}jA$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}kA$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}jB$$
8		nfcsb1v	$$⊢\underset{\_}{Ⅎ}k⦋j/k⦌B$$
9	4 5 6 7 8	cbvsum	$$⊢\sum _{k\in A}B=\sum _{j\in A}⦋j/k⦌B$$
10	9	a1i	$$⊢\phi \to \sum _{k\in A}B=\sum _{j\in A}⦋j/k⦌B$$
11		nfv	$$⊢Ⅎkj\in A$$
12	1 11	nfan	$$⊢Ⅎk\left(\phi \wedge j\in A\right)$$
13	8	nfel1	$$⊢Ⅎk⦋j/k⦌B\in ℝ$$
14	12 13	nfim	$$⊢Ⅎk\left(\left(\phi \wedge j\in A\right)\to ⦋j/k⦌B\in ℝ\right)$$
15		eleq1w	$$⊢k=j\to \left(k\in A\leftrightarrow j\in A\right)$$
16	15	anbi2d	$$⊢k=j\to \left(\left(\phi \wedge k\in A\right)\leftrightarrow \left(\phi \wedge j\in A\right)\right)$$
17	4	eleq1d	$$⊢k=j\to \left(B\in ℝ\leftrightarrow ⦋j/k⦌B\in ℝ\right)$$
18	16 17	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)$$
19	14 18 3	chvarfv	$$⊢\left(\phi \wedge j\in A\right)\to ⦋j/k⦌B\in ℝ$$
20	2 19	fsumrecl	$$⊢\phi \to \sum _{j\in A}⦋j/k⦌B\in ℝ$$
21	10 20	eqeltrd	$$⊢\phi \to \sum _{k\in A}B\in ℝ$$