Theorem fsumreclf

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

	Ref	Expression
Hypotheses	fsumreclf.k	⊢ Ⅎ 𝑘 𝜑
	fsumreclf.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fsumreclf.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
Assertion	fsumreclf	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		fsumreclf.k	⊢ Ⅎ 𝑘 𝜑
2		fsumreclf.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
3		fsumreclf.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
4		csbeq1a	⊢ ( 𝑘 = 𝑗 → 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
5		nfcv	⊢ Ⅎ 𝑗 𝐵
6		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
7	4 5 6	cbvsum	⊢ Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
8	7	a1i	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
9		nfv	⊢ Ⅎ 𝑘 𝑗 ∈ 𝐴
10	1 9	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝐴 )
11	6	nfel1	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ
12	10 11	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ )
13		eleq1w	⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴 ) )
14	13	anbi2d	⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ) )
15	4	eleq1d	⊢ ( 𝑘 = 𝑗 → ( 𝐵 ∈ ℝ ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ ) )
16	14 15	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ ) ) )
17	12 16 3	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ )
18	2 17	fsumrecl	⊢ ( 𝜑 → Σ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ )
19	8 18	eqeltrd	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℝ )