Metamath Proof Explorer

Theorem fsumzcl2

Description: A finite sum with integer summands is an integer. (Contributed by Alexander van der Vekens, 31-Aug-2018)

Ref Expression
Assertion fsumzcl2 ⊢ A ∈ Fin ∧ ∀ k ∈ A B ∈ ℤ → ∑ k ∈ A B ∈ ℤ

Proof

Step Hyp Ref Expression
1 csbeq1a ⊢ k = x → B = ⦋ x / k⦌ B
2 nfcv ⊢ Ⅎ _ x B
3 nfcsb1v ⊢ Ⅎ _ k ⦋ x / k⦌ B
4 1 2 3 cbvsum ⊢ ∑ k ∈ A B = ∑ x ∈ A ⦋ x / k⦌ B
5 simpl ⊢ A ∈ Fin ∧ ∀ k ∈ A B ∈ ℤ → A ∈ Fin
6 rspcsbela ⊢ x ∈ A ∧ ∀ k ∈ A B ∈ ℤ → ⦋ x / k⦌ B ∈ ℤ
7 6 expcom ⊢ ∀ k ∈ A B ∈ ℤ → x ∈ A → ⦋ x / k⦌ B ∈ ℤ
8 7 adantl ⊢ A ∈ Fin ∧ ∀ k ∈ A B ∈ ℤ → x ∈ A → ⦋ x / k⦌ B ∈ ℤ
9 8 imp ⊢ A ∈ Fin ∧ ∀ k ∈ A B ∈ ℤ ∧ x ∈ A → ⦋ x / k⦌ B ∈ ℤ
10 5 9 fsumzcl ⊢ A ∈ Fin ∧ ∀ k ∈ A B ∈ ℤ → ∑ x ∈ A ⦋ x / k⦌ B ∈ ℤ
11 4 10 eqeltrid ⊢ A ∈ Fin ∧ ∀ k ∈ A B ∈ ℤ → ∑ k ∈ A B ∈ ℤ