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 e. Fin /\ A. k e. ( A u. { Z } ) B e. ZZ ) -> sum_ k e. ( A u. { Z } ) B e. ZZ )

Proof

Step	Hyp	Ref	Expression
1		nfcv	|- F/_ x B
2		nfcsb1v	|- F/_ k [_ x / k ]_ B
3		csbeq1a	|- ( k = x -> B = [_ x / k ]_ B )
4	1 2 3	cbvsumi	|- sum_ k e. ( A u. { Z } ) B = sum_ x e. ( A u. { Z } ) [_ x / k ]_ B
5		snfi	|- { Z } e. Fin
6	5	a1i	|- ( ( A e. Fin /\ A. k e. ( A u. { Z } ) B e. ZZ ) -> { Z } e. Fin )
7		unfi	|- ( ( A e. Fin /\ { Z } e. Fin ) -> ( A u. { Z } ) e. Fin )
8	6 7	syldan	|- ( ( A e. Fin /\ A. k e. ( A u. { Z } ) B e. ZZ ) -> ( A u. { Z } ) e. Fin )
9		rspcsbela	|- ( ( x e. ( A u. { Z } ) /\ A. k e. ( A u. { Z } ) B e. ZZ ) -> [_ x / k ]_ B e. ZZ )
10	9	expcom	|- ( A. k e. ( A u. { Z } ) B e. ZZ -> ( x e. ( A u. { Z } ) -> [_ x / k ]_ B e. ZZ ) )
11	10	adantl	|- ( ( A e. Fin /\ A. k e. ( A u. { Z } ) B e. ZZ ) -> ( x e. ( A u. { Z } ) -> [_ x / k ]_ B e. ZZ ) )
12	11	imp	|- ( ( ( A e. Fin /\ A. k e. ( A u. { Z } ) B e. ZZ ) /\ x e. ( A u. { Z } ) ) -> [_ x / k ]_ B e. ZZ )
13	8 12	fsumzcl	|- ( ( A e. Fin /\ A. k e. ( A u. { Z } ) B e. ZZ ) -> sum_ x e. ( A u. { Z } ) [_ x / k ]_ B e. ZZ )
14	4 13	eqeltrid	|- ( ( A e. Fin /\ A. k e. ( A u. { Z } ) B e. ZZ ) -> sum_ k e. ( A u. { Z } ) B e. ZZ )