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 e. Fin /\ A. k e. A B e. ZZ ) -> sum_ k e. A 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 B = sum_ x e. A [_ x / k ]_ B
5 simpl 
 |-  ( ( A e. Fin /\ A. k e. A B e. ZZ ) -> A e. Fin )
6 rspcsbela 
 |-  ( ( x e. A /\ A. k e. A B e. ZZ ) -> [_ x / k ]_ B e. ZZ )
7 6 expcom 
 |-  ( A. k e. A B e. ZZ -> ( x e. A -> [_ x / k ]_ B e. ZZ ) )
8 7 adantl 
 |-  ( ( A e. Fin /\ A. k e. A B e. ZZ ) -> ( x e. A -> [_ x / k ]_ B e. ZZ ) )
9 8 imp 
 |-  ( ( ( A e. Fin /\ A. k e. A B e. ZZ ) /\ x e. A ) -> [_ x / k ]_ B e. ZZ )
10 5 9 fsumzcl 
 |-  ( ( A e. Fin /\ A. k e. A B e. ZZ ) -> sum_ x e. A [_ x / k ]_ B e. ZZ )
11 4 10 eqeltrid 
 |-  ( ( A e. Fin /\ A. k e. A B e. ZZ ) -> sum_ k e. A B e. ZZ )