# 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 ${⊢}\left({A}\in \mathrm{Fin}\wedge \forall {k}\in \left({A}\cup \left\{{Z}\right\}\right)\phantom{\rule{.4em}{0ex}}{B}\in ℤ\right)\to \sum _{{k}\in {A}\cup \left\{{Z}\right\}}{B}\in ℤ$

### Proof

Step Hyp Ref Expression
1 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
2 nfcsb1v
3 csbeq1a
4 1 2 3 cbvsumi
5 snfi ${⊢}\left\{{Z}\right\}\in \mathrm{Fin}$
6 5 a1i ${⊢}\left({A}\in \mathrm{Fin}\wedge \forall {k}\in \left({A}\cup \left\{{Z}\right\}\right)\phantom{\rule{.4em}{0ex}}{B}\in ℤ\right)\to \left\{{Z}\right\}\in \mathrm{Fin}$
7 unfi ${⊢}\left({A}\in \mathrm{Fin}\wedge \left\{{Z}\right\}\in \mathrm{Fin}\right)\to {A}\cup \left\{{Z}\right\}\in \mathrm{Fin}$
8 6 7 syldan ${⊢}\left({A}\in \mathrm{Fin}\wedge \forall {k}\in \left({A}\cup \left\{{Z}\right\}\right)\phantom{\rule{.4em}{0ex}}{B}\in ℤ\right)\to {A}\cup \left\{{Z}\right\}\in \mathrm{Fin}$
9 rspcsbela
10 9 expcom
14 4 13 eqeltrid ${⊢}\left({A}\in \mathrm{Fin}\wedge \forall {k}\in \left({A}\cup \left\{{Z}\right\}\right)\phantom{\rule{.4em}{0ex}}{B}\in ℤ\right)\to \sum _{{k}\in {A}\cup \left\{{Z}\right\}}{B}\in ℤ$