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	$⊢ φ \to N \in ℕ$
	modfsummod.1	$⊢ φ \to A \in Fin$
	modfsummod.2	$⊢ φ \to \forall k \in A B \in ℤ$
Assertion	modfsummod	$⊢ φ \to \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N$

Proof

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

Metamath Proof Explorer

Theorem modfsummod

Proof