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 φ N
modfsummod.1 φ A Fin
modfsummod.2 φ k A B
Assertion modfsummod φ k A B mod N = k A B mod N mod N

Proof

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