Metamath Proof Explorer

Theorem fsummmodsnunz

Description: A finite sum of summands modulo a positive number with an additional summand is an integer. (Contributed by Alexander van der Vekens, 1-Sep-2018)

Ref Expression
Assertion fsummmodsnunz 
|- ( ( A e. Fin /\ N e. NN /\ A. k e. ( A u. { z } ) B e. ZZ ) -> sum_ k e. ( A u. { z } ) ( B mod N ) e. ZZ )

Proof

Step Hyp Ref Expression
1 csbeq1a 
 |-  ( k = x -> ( B mod N ) = [_ x / k ]_ ( B mod N ) )
2 nfcv 
 |-  F/_ x ( B mod N )
3 nfcsb1v 
 |-  F/_ k [_ x / k ]_ ( B mod N )
4 1 2 3 cbvsum 
 |-  sum_ k e. ( A u. { z } ) ( B mod N ) = sum_ x e. ( A u. { z } ) [_ x / k ]_ ( B mod N )
5 snfi 
 |-  { z } e. Fin
6 unfi 
 |-  ( ( A e. Fin /\ { z } e. Fin ) -> ( A u. { z } ) e. Fin )
7 5 6 mpan2 
 |-  ( A e. Fin -> ( A u. { z } ) e. Fin )
8 7 3ad2ant1 
 |-  ( ( A e. Fin /\ N e. NN /\ 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 3ad2ant3 
 |-  ( ( A e. Fin /\ N e. NN /\ 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 /\ N e. NN /\ A. k e. ( A u. { z } ) B e. ZZ ) /\ x e. ( A u. { z } ) ) -> [_ x / k ]_ B e. ZZ )
13 vex 
 |-  x e. _V
14 csbov1g 
 |-  ( x e. _V -> [_ x / k ]_ ( B mod N ) = ( [_ x / k ]_ B mod N ) )
15 13 14 ax-mp 
 |-  [_ x / k ]_ ( B mod N ) = ( [_ x / k ]_ B mod N )
16 simpr 
 |-  ( ( N e. NN /\ [_ x / k ]_ B e. ZZ ) -> [_ x / k ]_ B e. ZZ )
17 simpl 
 |-  ( ( N e. NN /\ [_ x / k ]_ B e. ZZ ) -> N e. NN )
18 16 17 zmodcld 
 |-  ( ( N e. NN /\ [_ x / k ]_ B e. ZZ ) -> ( [_ x / k ]_ B mod N ) e. NN0 )
19 18 nn0zd 
 |-  ( ( N e. NN /\ [_ x / k ]_ B e. ZZ ) -> ( [_ x / k ]_ B mod N ) e. ZZ )
20 15 19 eqeltrid 
 |-  ( ( N e. NN /\ [_ x / k ]_ B e. ZZ ) -> [_ x / k ]_ ( B mod N ) e. ZZ )
21 20 ex 
 |-  ( N e. NN -> ( [_ x / k ]_ B e. ZZ -> [_ x / k ]_ ( B mod N ) e. ZZ ) )
22 21 3ad2ant2 
 |-  ( ( A e. Fin /\ N e. NN /\ A. k e. ( A u. { z } ) B e. ZZ ) -> ( [_ x / k ]_ B e. ZZ -> [_ x / k ]_ ( B mod N ) e. ZZ ) )
23 22 adantr 
 |-  ( ( ( A e. Fin /\ N e. NN /\ A. k e. ( A u. { z } ) B e. ZZ ) /\ x e. ( A u. { z } ) ) -> ( [_ x / k ]_ B e. ZZ -> [_ x / k ]_ ( B mod N ) e. ZZ ) )
24 12 23 mpd 
 |-  ( ( ( A e. Fin /\ N e. NN /\ A. k e. ( A u. { z } ) B e. ZZ ) /\ x e. ( A u. { z } ) ) -> [_ x / k ]_ ( B mod N ) e. ZZ )
25 8 24 fsumzcl 
 |-  ( ( A e. Fin /\ N e. NN /\ A. k e. ( A u. { z } ) B e. ZZ ) -> sum_ x e. ( A u. { z } ) [_ x / k ]_ ( B mod N ) e. ZZ )
26 4 25 eqeltrid 
 |-  ( ( A e. Fin /\ N e. NN /\ A. k e. ( A u. { z } ) B e. ZZ ) -> sum_ k e. ( A u. { z } ) ( B mod N ) e. ZZ )