This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 φ
fsumclf.a ⊢ φ → A ∈ Fin
fsumclf.b ⊢ φ ∧ k ∈ A → B ∈ ℂ
Assertion fsumclf ⊢ φ → ∑ k ∈ A B ∈ ℂ

Proof

Step Hyp Ref Expression
1 fsumclf.ph ⊢ Ⅎ k φ
2 fsumclf.a ⊢ φ → A ∈ Fin
3 fsumclf.b ⊢ φ ∧ k ∈ A → B ∈ ℂ
4 csbeq1a ⊢ k = j → B = ⦋ j / k⦌ B
5 nfcv ⊢ Ⅎ _ j B
6 nfcsb1v ⊢ Ⅎ _ k ⦋ j / k⦌ B
7 4 5 6 cbvsum ⊢ ∑ k ∈ A B = ∑ j ∈ A ⦋ j / k⦌ B
8 7 a1i ⊢ φ → ∑ k ∈ A B = ∑ j ∈ A ⦋ j / k⦌ B
9 nfv ⊢ Ⅎ k j ∈ A
10 1 9 nfan ⊢ Ⅎ k φ ∧ j ∈ A
11 6 nfel1 ⊢ Ⅎ k ⦋ j / k⦌ B ∈ ℂ
12 10 11 nfim ⊢ Ⅎ k φ ∧ j ∈ A → ⦋ j / k⦌ B ∈ ℂ
13 eleq1w ⊢ k = j → k ∈ A ↔ j ∈ A
14 13 anbi2d ⊢ k = j → φ ∧ k ∈ A ↔ φ ∧ j ∈ A
15 4 eleq1d ⊢ k = j → B ∈ ℂ ↔ ⦋ j / k⦌ B ∈ ℂ
16 14 15 imbi12d ⊢ k = j → φ ∧ k ∈ A → B ∈ ℂ ↔ φ ∧ j ∈ A → ⦋ j / k⦌ B ∈ ℂ
17 12 16 3 chvarfv ⊢ φ ∧ j ∈ A → ⦋ j / k⦌ B ∈ ℂ
18 2 17 fsumcl ⊢ φ → ∑ j ∈ A ⦋ j / k⦌ B ∈ ℂ
19 8 18 eqeltrd ⊢ φ → ∑ k ∈ A B ∈ ℂ