Metamath Proof Explorer

Theorem fsummsnunz

Description: A finite sum all of whose summands are integers is itself an integer (case where the summation set is the union of a finite set and a singleton). (Contributed by Alexander van der Vekens, 1-Sep-2018) (Revised by AV, 17-Dec-2021)

Ref Expression
Assertion fsummsnunz ⊢ A ∈ Fin ∧ ∀ k ∈ A ∪ Z B ∈ ℤ → ∑ k ∈ A ∪ Z B ∈ ℤ

Proof

Step Hyp Ref Expression
1 nfcv ⊢ Ⅎ _ x B
2 nfcsb1v ⊢ Ⅎ _ k ⦋ x / k⦌ B
3 csbeq1a ⊢ k = x → B = ⦋ x / k⦌ B
4 1 2 3 cbvsumi ⊢ ∑ k ∈ A ∪ Z B = ∑ x ∈ A ∪ Z ⦋ x / k⦌ B
5 snfi ⊢ Z ∈ Fin
6 5 a1i ⊢ A ∈ Fin ∧ ∀ k ∈ A ∪ Z B ∈ ℤ → Z ∈ Fin
7 unfi ⊢ A ∈ Fin ∧ Z ∈ Fin → A ∪ Z ∈ Fin
8 6 7 syldan ⊢ A ∈ Fin ∧ ∀ k ∈ A ∪ Z B ∈ ℤ → A ∪ Z ∈ Fin
9 rspcsbela ⊢ x ∈ A ∪ Z ∧ ∀ k ∈ A ∪ Z B ∈ ℤ → ⦋ x / k⦌ B ∈ ℤ
10 9 expcom ⊢ ∀ k ∈ A ∪ Z B ∈ ℤ → x ∈ A ∪ Z → ⦋ x / k⦌ B ∈ ℤ
11 10 adantl ⊢ A ∈ Fin ∧ ∀ k ∈ A ∪ Z B ∈ ℤ → x ∈ A ∪ Z → ⦋ x / k⦌ B ∈ ℤ
12 11 imp ⊢ A ∈ Fin ∧ ∀ k ∈ A ∪ Z B ∈ ℤ ∧ x ∈ A ∪ Z → ⦋ x / k⦌ B ∈ ℤ
13 8 12 fsumzcl ⊢ A ∈ Fin ∧ ∀ k ∈ A ∪ Z B ∈ ℤ → ∑ x ∈ A ∪ Z ⦋ x / k⦌ B ∈ ℤ
14 4 13 eqeltrid ⊢ A ∈ Fin ∧ ∀ k ∈ A ∪ Z B ∈ ℤ → ∑ k ∈ A ∪ Z B ∈ ℤ