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

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 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 csbeq1a 
 |-  ( k = x -> B = [_ x / k ]_ B )
2 nfcv 
 |-  F/_ x B
3 nfcsb1v 
 |-  F/_ k [_ x / k ]_ B
4 1 2 3 cbvsum 
 |-  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 )