Metamath Proof Explorer

Theorem modfsummod

Description: A finite sum modulo a positive integer equals the finite sum of their summands modulo the positive integer, modulo the positive integer. (Contributed by Alexander van der Vekens, 1-Sep-2018)

Ref Expression
Hypotheses modfsummod.n 
|- ( ph -> N e. NN )
modfsummod.1 
|- ( ph -> A e. Fin )
modfsummod.2 
|- ( ph -> A. k e. A B e. ZZ )
Assertion modfsummod 
|- ( ph -> ( sum_ k e. A B mod N ) = ( sum_ k e. A ( B mod N ) mod N ) )

Proof

Step Hyp Ref Expression
1 modfsummod.n 
 |-  ( ph -> N e. NN )
2 modfsummod.1 
 |-  ( ph -> A e. Fin )
3 modfsummod.2 
 |-  ( ph -> A. k e. A B e. ZZ )
4 raleq 
 |-  ( x = (/) -> ( A. k e. x B e. ZZ <-> A. k e. (/) B e. ZZ ) )
5 4 anbi1d 
 |-  ( x = (/) -> ( ( A. k e. x B e. ZZ /\ N e. NN ) <-> ( A. k e. (/) B e. ZZ /\ N e. NN ) ) )
6 sumeq1 
 |-  ( x = (/) -> sum_ k e. x B = sum_ k e. (/) B )
7 6 oveq1d 
 |-  ( x = (/) -> ( sum_ k e. x B mod N ) = ( sum_ k e. (/) B mod N ) )
8 sumeq1 
 |-  ( x = (/) -> sum_ k e. x ( B mod N ) = sum_ k e. (/) ( B mod N ) )
9 8 oveq1d 
 |-  ( x = (/) -> ( sum_ k e. x ( B mod N ) mod N ) = ( sum_ k e. (/) ( B mod N ) mod N ) )
10 7 9 eqeq12d 
 |-  ( x = (/) -> ( ( sum_ k e. x B mod N ) = ( sum_ k e. x ( B mod N ) mod N ) <-> ( sum_ k e. (/) B mod N ) = ( sum_ k e. (/) ( B mod N ) mod N ) ) )
11 5 10 imbi12d 
 |-  ( x = (/) -> ( ( ( A. k e. x B e. ZZ /\ N e. NN ) -> ( sum_ k e. x B mod N ) = ( sum_ k e. x ( B mod N ) mod N ) ) <-> ( ( A. k e. (/) B e. ZZ /\ N e. NN ) -> ( sum_ k e. (/) B mod N ) = ( sum_ k e. (/) ( B mod N ) mod N ) ) ) )
12 raleq 
 |-  ( x = y -> ( A. k e. x B e. ZZ <-> A. k e. y B e. ZZ ) )
13 12 anbi1d 
 |-  ( x = y -> ( ( A. k e. x B e. ZZ /\ N e. NN ) <-> ( A. k e. y B e. ZZ /\ N e. NN ) ) )
14 sumeq1 
 |-  ( x = y -> sum_ k e. x B = sum_ k e. y B )
15 14 oveq1d 
 |-  ( x = y -> ( sum_ k e. x B mod N ) = ( sum_ k e. y B mod N ) )
16 sumeq1 
 |-  ( x = y -> sum_ k e. x ( B mod N ) = sum_ k e. y ( B mod N ) )
17 16 oveq1d 
 |-  ( x = y -> ( sum_ k e. x ( B mod N ) mod N ) = ( sum_ k e. y ( B mod N ) mod N ) )
18 15 17 eqeq12d 
 |-  ( x = y -> ( ( sum_ k e. x B mod N ) = ( sum_ k e. x ( B mod N ) mod N ) <-> ( sum_ k e. y B mod N ) = ( sum_ k e. y ( B mod N ) mod N ) ) )
19 13 18 imbi12d 
 |-  ( x = y -> ( ( ( A. k e. x B e. ZZ /\ N e. NN ) -> ( sum_ k e. x B mod N ) = ( sum_ k e. x ( B mod N ) mod N ) ) <-> ( ( A. k e. y B e. ZZ /\ N e. NN ) -> ( sum_ k e. y B mod N ) = ( sum_ k e. y ( B mod N ) mod N ) ) ) )
20 raleq 
 |-  ( x = ( y u. { z } ) -> ( A. k e. x B e. ZZ <-> A. k e. ( y u. { z } ) B e. ZZ ) )
21 20 anbi1d 
 |-  ( x = ( y u. { z } ) -> ( ( A. k e. x B e. ZZ /\ N e. NN ) <-> ( A. k e. ( y u. { z } ) B e. ZZ /\ N e. NN ) ) )
22 sumeq1 
 |-  ( x = ( y u. { z } ) -> sum_ k e. x B = sum_ k e. ( y u. { z } ) B )
23 22 oveq1d 
 |-  ( x = ( y u. { z } ) -> ( sum_ k e. x B mod N ) = ( sum_ k e. ( y u. { z } ) B mod N ) )
24 sumeq1 
 |-  ( x = ( y u. { z } ) -> sum_ k e. x ( B mod N ) = sum_ k e. ( y u. { z } ) ( B mod N ) )
25 24 oveq1d 
 |-  ( x = ( y u. { z } ) -> ( sum_ k e. x ( B mod N ) mod N ) = ( sum_ k e. ( y u. { z } ) ( B mod N ) mod N ) )
26 23 25 eqeq12d 
 |-  ( x = ( y u. { z } ) -> ( ( sum_ k e. x B mod N ) = ( sum_ k e. x ( B mod N ) mod N ) <-> ( sum_ k e. ( y u. { z } ) B mod N ) = ( sum_ k e. ( y u. { z } ) ( B mod N ) mod N ) ) )
27 21 26 imbi12d 
 |-  ( x = ( y u. { z } ) -> ( ( ( A. k e. x B e. ZZ /\ N e. NN ) -> ( sum_ k e. x B mod N ) = ( sum_ k e. x ( B mod N ) mod N ) ) <-> ( ( A. k e. ( y u. { z } ) B e. ZZ /\ N e. NN ) -> ( sum_ k e. ( y u. { z } ) B mod N ) = ( sum_ k e. ( y u. { z } ) ( B mod N ) mod N ) ) ) )
28 raleq 
 |-  ( x = A -> ( A. k e. x B e. ZZ <-> A. k e. A B e. ZZ ) )
29 28 anbi1d 
 |-  ( x = A -> ( ( A. k e. x B e. ZZ /\ N e. NN ) <-> ( A. k e. A B e. ZZ /\ N e. NN ) ) )
30 sumeq1 
 |-  ( x = A -> sum_ k e. x B = sum_ k e. A B )
31 30 oveq1d 
 |-  ( x = A -> ( sum_ k e. x B mod N ) = ( sum_ k e. A B mod N ) )
32 sumeq1 
 |-  ( x = A -> sum_ k e. x ( B mod N ) = sum_ k e. A ( B mod N ) )
33 32 oveq1d 
 |-  ( x = A -> ( sum_ k e. x ( B mod N ) mod N ) = ( sum_ k e. A ( B mod N ) mod N ) )
34 31 33 eqeq12d 
 |-  ( x = A -> ( ( sum_ k e. x B mod N ) = ( sum_ k e. x ( B mod N ) mod N ) <-> ( sum_ k e. A B mod N ) = ( sum_ k e. A ( B mod N ) mod N ) ) )
35 29 34 imbi12d 
 |-  ( x = A -> ( ( ( A. k e. x B e. ZZ /\ N e. NN ) -> ( sum_ k e. x B mod N ) = ( sum_ k e. x ( B mod N ) mod N ) ) <-> ( ( A. k e. A B e. ZZ /\ N e. NN ) -> ( sum_ k e. A B mod N ) = ( sum_ k e. A ( B mod N ) mod N ) ) ) )
36 sum0 
 |-  sum_ k e. (/) B = 0
37 36 oveq1i 
 |-  ( sum_ k e. (/) B mod N ) = ( 0 mod N )
38 sum0 
 |-  sum_ k e. (/) ( B mod N ) = 0
39 38 a1i 
 |-  ( N e. NN -> sum_ k e. (/) ( B mod N ) = 0 )
40 39 oveq1d 
 |-  ( N e. NN -> ( sum_ k e. (/) ( B mod N ) mod N ) = ( 0 mod N ) )
41 37 40 eqtr4id 
 |-  ( N e. NN -> ( sum_ k e. (/) B mod N ) = ( sum_ k e. (/) ( B mod N ) mod N ) )
42 41 adantl 
 |-  ( ( A. k e. (/) B e. ZZ /\ N e. NN ) -> ( sum_ k e. (/) B mod N ) = ( sum_ k e. (/) ( B mod N ) mod N ) )
43 simpll 
 |-  ( ( ( y e. Fin /\ ( A. k e. y B e. ZZ /\ N e. NN ) ) /\ A. k e. { z } B e. ZZ ) -> y e. Fin )
44 simplrr 
 |-  ( ( ( y e. Fin /\ ( A. k e. y B e. ZZ /\ N e. NN ) ) /\ A. k e. { z } B e. ZZ ) -> N e. NN )
45 ralun 
 |-  ( ( A. k e. y B e. ZZ /\ A. k e. { z } B e. ZZ ) -> A. k e. ( y u. { z } ) B e. ZZ )
46 45 ex 
 |-  ( A. k e. y B e. ZZ -> ( A. k e. { z } B e. ZZ -> A. k e. ( y u. { z } ) B e. ZZ ) )
47 46 ad2antrl 
 |-  ( ( y e. Fin /\ ( A. k e. y B e. ZZ /\ N e. NN ) ) -> ( A. k e. { z } B e. ZZ -> A. k e. ( y u. { z } ) B e. ZZ ) )
48 47 imp 
 |-  ( ( ( y e. Fin /\ ( A. k e. y B e. ZZ /\ N e. NN ) ) /\ A. k e. { z } B e. ZZ ) -> A. k e. ( y u. { z } ) B e. ZZ )
49 modfsummods 
 |-  ( ( y e. Fin /\ N e. NN /\ A. k e. ( y u. { z } ) B e. ZZ ) -> ( ( sum_ k e. y B mod N ) = ( sum_ k e. y ( B mod N ) mod N ) -> ( sum_ k e. ( y u. { z } ) B mod N ) = ( sum_ k e. ( y u. { z } ) ( B mod N ) mod N ) ) )
50 43 44 48 49 syl3anc 
 |-  ( ( ( y e. Fin /\ ( A. k e. y B e. ZZ /\ N e. NN ) ) /\ A. k e. { z } B e. ZZ ) -> ( ( sum_ k e. y B mod N ) = ( sum_ k e. y ( B mod N ) mod N ) -> ( sum_ k e. ( y u. { z } ) B mod N ) = ( sum_ k e. ( y u. { z } ) ( B mod N ) mod N ) ) )
51 50 ex 
 |-  ( ( y e. Fin /\ ( A. k e. y B e. ZZ /\ N e. NN ) ) -> ( A. k e. { z } B e. ZZ -> ( ( sum_ k e. y B mod N ) = ( sum_ k e. y ( B mod N ) mod N ) -> ( sum_ k e. ( y u. { z } ) B mod N ) = ( sum_ k e. ( y u. { z } ) ( B mod N ) mod N ) ) ) )
52 51 com23 
 |-  ( ( y e. Fin /\ ( A. k e. y B e. ZZ /\ N e. NN ) ) -> ( ( sum_ k e. y B mod N ) = ( sum_ k e. y ( B mod N ) mod N ) -> ( A. k e. { z } B e. ZZ -> ( sum_ k e. ( y u. { z } ) B mod N ) = ( sum_ k e. ( y u. { z } ) ( B mod N ) mod N ) ) ) )
53 52 ex 
 |-  ( y e. Fin -> ( ( A. k e. y B e. ZZ /\ N e. NN ) -> ( ( sum_ k e. y B mod N ) = ( sum_ k e. y ( B mod N ) mod N ) -> ( A. k e. { z } B e. ZZ -> ( sum_ k e. ( y u. { z } ) B mod N ) = ( sum_ k e. ( y u. { z } ) ( B mod N ) mod N ) ) ) ) )
54 53 a2d 
 |-  ( y e. Fin -> ( ( ( A. k e. y B e. ZZ /\ N e. NN ) -> ( sum_ k e. y B mod N ) = ( sum_ k e. y ( B mod N ) mod N ) ) -> ( ( A. k e. y B e. ZZ /\ N e. NN ) -> ( A. k e. { z } B e. ZZ -> ( sum_ k e. ( y u. { z } ) B mod N ) = ( sum_ k e. ( y u. { z } ) ( B mod N ) mod N ) ) ) ) )
55 ralunb 
 |-  ( A. k e. ( y u. { z } ) B e. ZZ <-> ( A. k e. y B e. ZZ /\ A. k e. { z } B e. ZZ ) )
56 55 anbi1i 
 |-  ( ( A. k e. ( y u. { z } ) B e. ZZ /\ N e. NN ) <-> ( ( A. k e. y B e. ZZ /\ A. k e. { z } B e. ZZ ) /\ N e. NN ) )
57 56 imbi1i 
 |-  ( ( ( A. k e. ( y u. { z } ) B e. ZZ /\ N e. NN ) -> ( sum_ k e. ( y u. { z } ) B mod N ) = ( sum_ k e. ( y u. { z } ) ( B mod N ) mod N ) ) <-> ( ( ( A. k e. y B e. ZZ /\ A. k e. { z } B e. ZZ ) /\ N e. NN ) -> ( sum_ k e. ( y u. { z } ) B mod N ) = ( sum_ k e. ( y u. { z } ) ( B mod N ) mod N ) ) )
58 an32 
 |-  ( ( ( A. k e. y B e. ZZ /\ A. k e. { z } B e. ZZ ) /\ N e. NN ) <-> ( ( A. k e. y B e. ZZ /\ N e. NN ) /\ A. k e. { z } B e. ZZ ) )
59 58 imbi1i 
 |-  ( ( ( ( A. k e. y B e. ZZ /\ A. k e. { z } B e. ZZ ) /\ N e. NN ) -> ( sum_ k e. ( y u. { z } ) B mod N ) = ( sum_ k e. ( y u. { z } ) ( B mod N ) mod N ) ) <-> ( ( ( A. k e. y B e. ZZ /\ N e. NN ) /\ A. k e. { z } B e. ZZ ) -> ( sum_ k e. ( y u. { z } ) B mod N ) = ( sum_ k e. ( y u. { z } ) ( B mod N ) mod N ) ) )
60 impexp 
 |-  ( ( ( ( A. k e. y B e. ZZ /\ N e. NN ) /\ A. k e. { z } B e. ZZ ) -> ( sum_ k e. ( y u. { z } ) B mod N ) = ( sum_ k e. ( y u. { z } ) ( B mod N ) mod N ) ) <-> ( ( A. k e. y B e. ZZ /\ N e. NN ) -> ( A. k e. { z } B e. ZZ -> ( sum_ k e. ( y u. { z } ) B mod N ) = ( sum_ k e. ( y u. { z } ) ( B mod N ) mod N ) ) ) )
61 57 59 60 3bitri 
 |-  ( ( ( A. k e. ( y u. { z } ) B e. ZZ /\ N e. NN ) -> ( sum_ k e. ( y u. { z } ) B mod N ) = ( sum_ k e. ( y u. { z } ) ( B mod N ) mod N ) ) <-> ( ( A. k e. y B e. ZZ /\ N e. NN ) -> ( A. k e. { z } B e. ZZ -> ( sum_ k e. ( y u. { z } ) B mod N ) = ( sum_ k e. ( y u. { z } ) ( B mod N ) mod N ) ) ) )
62 54 61 syl6ibr 
 |-  ( y e. Fin -> ( ( ( A. k e. y B e. ZZ /\ N e. NN ) -> ( sum_ k e. y B mod N ) = ( sum_ k e. y ( B mod N ) mod N ) ) -> ( ( A. k e. ( y u. { z } ) B e. ZZ /\ N e. NN ) -> ( sum_ k e. ( y u. { z } ) B mod N ) = ( sum_ k e. ( y u. { z } ) ( B mod N ) mod N ) ) ) )
63 11 19 27 35 42 62 findcard2 
 |-  ( A e. Fin -> ( ( A. k e. A B e. ZZ /\ N e. NN ) -> ( sum_ k e. A B mod N ) = ( sum_ k e. A ( B mod N ) mod N ) ) )
64 2 63 syl 
 |-  ( ph -> ( ( A. k e. A B e. ZZ /\ N e. NN ) -> ( sum_ k e. A B mod N ) = ( sum_ k e. A ( B mod N ) mod N ) ) )
65 3 1 64 mp2and 
 |-  ( ph -> ( sum_ k e. A B mod N ) = ( sum_ k e. A ( B mod N ) mod N ) )