Theorem fsumreclf

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

	Ref	Expression
Hypotheses	fsumreclf.k	|- F/ k ph
	fsumreclf.a	|- ( ph -> A e. Fin )
	fsumreclf.b	|- ( ( ph /\ k e. A ) -> B e. RR )
Assertion	fsumreclf	|- ( ph -> sum_ k e. A B e. RR )

Proof

Step	Hyp	Ref	Expression
1		fsumreclf.k	|- F/ k ph
2		fsumreclf.a	|- ( ph -> A e. Fin )
3		fsumreclf.b	|- ( ( ph /\ k e. A ) -> B e. RR )
4		csbeq1a	|- ( k = j -> B = [_ j / k ]_ B )
5		nfcv	|- F/_ j B
6		nfcsb1v	|- F/_ k [_ j / k ]_ B
7	4 5 6	cbvsum	|- sum_ k e. A B = sum_ j e. A [_ j / k ]_ B
8	7	a1i	|- ( ph -> sum_ k e. A B = sum_ j e. A [_ j / k ]_ B )
9		nfv	|- F/ k j e. A
10	1 9	nfan	|- F/ k ( ph /\ j e. A )
11	6	nfel1	|- F/ k [_ j / k ]_ B e. RR
12	10 11	nfim	|- F/ k ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. RR )
13		eleq1w	|- ( k = j -> ( k e. A <-> j e. A ) )
14	13	anbi2d	|- ( k = j -> ( ( ph /\ k e. A ) <-> ( ph /\ j e. A ) ) )
15	4	eleq1d	|- ( k = j -> ( B e. RR <-> [_ j / k ]_ B e. RR ) )
16	14 15	imbi12d	|- ( k = j -> ( ( ( ph /\ k e. A ) -> B e. RR ) <-> ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. RR ) ) )
17	12 16 3	chvarfv	|- ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. RR )
18	2 17	fsumrecl	|- ( ph -> sum_ j e. A [_ j / k ]_ B e. RR )
19	8 18	eqeltrd	|- ( ph -> sum_ k e. A B e. RR )