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	⊢ Ⅎ 𝑘 𝜑
	fsumclf.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fsumclf.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
Assertion	fsumclf	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℂ )

Proof

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