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	imbitrrdi	\|- ( 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 ) )

Metamath Proof Explorer

Theorem modfsummod

Proof