modfsummods

		Ref	Expression
	Assertion	modfsummods	$⊢ (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ) \to (\sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N \to \sum_{k \in A \cup \{z\}} B \mod N = \sum_{k \in A \cup \{z\}} (B \mod N) \mod N)$

Proof

Step	Hyp	Ref	Expression
1		snssi	$⊢ z \in A \to \{z\} \subseteq A$
2		ssequn1	$⊢ \{z\} \subseteq A \leftrightarrow \{z\} \cup A = A$
3		uncom	$⊢ \{z\} \cup A = A \cup \{z\}$
4	3	eqeq1i	$⊢ \{z\} \cup A = A \leftrightarrow A \cup \{z\} = A$
5		sumeq1	$⊢ A = A \cup \{z\} \to \sum_{k \in A} B = \sum_{k \in A \cup \{z\}} B$
6	5	oveq1d	$⊢ A = A \cup \{z\} \to \sum_{k \in A} B \mod N = \sum_{k \in A \cup \{z\}} B \mod N$
7		sumeq1	$⊢ A = A \cup \{z\} \to \sum_{k \in A} (B \mod N) = \sum_{k \in A \cup \{z\}} (B \mod N)$
8	7	oveq1d	$⊢ A = A \cup \{z\} \to \sum_{k \in A} (B \mod N) \mod N = \sum_{k \in A \cup \{z\}} (B \mod N) \mod N$
9	6 8	eqeq12d	$⊢ A = A \cup \{z\} \to (\sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N \leftrightarrow \sum_{k \in A \cup \{z\}} B \mod N = \sum_{k \in A \cup \{z\}} (B \mod N) \mod N)$
10	9	eqcoms	$⊢ A \cup \{z\} = A \to (\sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N \leftrightarrow \sum_{k \in A \cup \{z\}} B \mod N = \sum_{k \in A \cup \{z\}} (B \mod N) \mod N)$
11	4 10	sylbi	$⊢ \{z\} \cup A = A \to (\sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N \leftrightarrow \sum_{k \in A \cup \{z\}} B \mod N = \sum_{k \in A \cup \{z\}} (B \mod N) \mod N)$
12	11	biimpd	$⊢ \{z\} \cup A = A \to (\sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N \to \sum_{k \in A \cup \{z\}} B \mod N = \sum_{k \in A \cup \{z\}} (B \mod N) \mod N)$
13	12	a1d	$⊢ \{z\} \cup A = A \to ((A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ) \to (\sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N \to \sum_{k \in A \cup \{z\}} B \mod N = \sum_{k \in A \cup \{z\}} (B \mod N) \mod N))$
14	2 13	sylbi	$⊢ \{z\} \subseteq A \to ((A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ) \to (\sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N \to \sum_{k \in A \cup \{z\}} B \mod N = \sum_{k \in A \cup \{z\}} (B \mod N) \mod N))$
15	1 14	syl	$⊢ z \in A \to ((A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ) \to (\sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N \to \sum_{k \in A \cup \{z\}} B \mod N = \sum_{k \in A \cup \{z\}} (B \mod N) \mod N))$
16		df-nel	$⊢ z \notin A \leftrightarrow \neg z \in A$
17		simp1	$⊢ (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ) \to A \in Fin$
18	17	ad2antlr	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to A \in Fin$
19		simpl	$⊢ (z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \to z \notin A$
20	19	adantr	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to z \notin A$
21		vex	$⊢ z \in V$
22	20 21	jctil	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to (z \in V \land z \notin A)$
23		simplr3	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to \forall k \in (A \cup \{z\}) B \in ℤ$
24		fsumsplitsnun	$⊢ (A \in Fin \land (z \in V \land z \notin A) \land \forall k \in (A \cup \{z\}) B \in ℤ) \to \sum_{k \in A \cup \{z\}} B = \sum_{k \in A} B + ⦋ z / k ⦌ B$
25	18 22 23 24	syl3anc	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to \sum_{k \in A \cup \{z\}} B = \sum_{k \in A} B + ⦋ z / k ⦌ B$
26	25	oveq1d	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to \sum_{k \in A \cup \{z\}} B \mod N = (\sum_{k \in A} B + ⦋ z / k ⦌ B) \mod N$
27		ralunb	$⊢ \forall k \in (A \cup \{z\}) B \in ℤ \leftrightarrow (\forall k \in A B \in ℤ \land \forall k \in \{z\} B \in ℤ)$
28		simpl	$⊢ (\forall k \in A B \in ℤ \land \forall k \in \{z\} B \in ℤ) \to \forall k \in A B \in ℤ$
29	27 28	sylbi	$⊢ \forall k \in (A \cup \{z\}) B \in ℤ \to \forall k \in A B \in ℤ$
30		fsumzcl2	$⊢ (A \in Fin \land \forall k \in A B \in ℤ) \to \sum_{k \in A} B \in ℤ$
31	29 30	sylan2	$⊢ (A \in Fin \land \forall k \in (A \cup \{z\}) B \in ℤ) \to \sum_{k \in A} B \in ℤ$
32	31	3adant2	$⊢ (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ) \to \sum_{k \in A} B \in ℤ$
33	32	adantl	$⊢ (z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \to \sum_{k \in A} B \in ℤ$
34	33	zred	$⊢ (z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \to \sum_{k \in A} B \in ℝ$
35		modfsummodslem1	$⊢ \forall k \in (A \cup \{z\}) B \in ℤ \to ⦋ z / k ⦌ B \in ℤ$
36	35	3ad2ant3	$⊢ (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ) \to ⦋ z / k ⦌ B \in ℤ$
37	36	adantl	$⊢ (z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \to ⦋ z / k ⦌ B \in ℤ$
38	37	zred	$⊢ (z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \to ⦋ z / k ⦌ B \in ℝ$
39		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
40	39	3ad2ant2	$⊢ (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ) \to N \in ℝ^{+}$
41	40	adantl	$⊢ (z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \to N \in ℝ^{+}$
42		modaddabs	$⊢ (\sum_{k \in A} B \in ℝ \land ⦋ z / k ⦌ B \in ℝ \land N \in ℝ^{+}) \to ((\sum_{k \in A} B \mod N) + (⦋ z / k ⦌ B \mod N)) \mod N = (\sum_{k \in A} B + ⦋ z / k ⦌ B) \mod N$
43	34 38 41 42	syl3anc	$⊢ (z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \to ((\sum_{k \in A} B \mod N) + (⦋ z / k ⦌ B \mod N)) \mod N = (\sum_{k \in A} B + ⦋ z / k ⦌ B) \mod N$
44	43	eqcomd	$⊢ (z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \to (\sum_{k \in A} B + ⦋ z / k ⦌ B) \mod N = ((\sum_{k \in A} B \mod N) + (⦋ z / k ⦌ B \mod N)) \mod N$
45	44	adantr	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to (\sum_{k \in A} B + ⦋ z / k ⦌ B) \mod N = ((\sum_{k \in A} B \mod N) + (⦋ z / k ⦌ B \mod N)) \mod N$
46		simpr	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N$
47	35	zred	$⊢ \forall k \in (A \cup \{z\}) B \in ℤ \to ⦋ z / k ⦌ B \in ℝ$
48	47	3ad2ant3	$⊢ (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ) \to ⦋ z / k ⦌ B \in ℝ$
49	48	adantl	$⊢ (z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \to ⦋ z / k ⦌ B \in ℝ$
50	49 41	jca	$⊢ (z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \to (⦋ z / k ⦌ B \in ℝ \land N \in ℝ^{+})$
51	50	adantr	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to (⦋ z / k ⦌ B \in ℝ \land N \in ℝ^{+})$
52		modabs2	$⊢ (⦋ z / k ⦌ B \in ℝ \land N \in ℝ^{+}) \to (⦋ z / k ⦌ B \mod N) \mod N = ⦋ z / k ⦌ B \mod N$
53	52	eqcomd	$⊢ (⦋ z / k ⦌ B \in ℝ \land N \in ℝ^{+}) \to ⦋ z / k ⦌ B \mod N = (⦋ z / k ⦌ B \mod N) \mod N$
54	51 53	syl	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to ⦋ z / k ⦌ B \mod N = (⦋ z / k ⦌ B \mod N) \mod N$
55	46 54	oveq12d	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to (\sum_{k \in A} B \mod N) + (⦋ z / k ⦌ B \mod N) = (\sum_{k \in A} (B \mod N) \mod N) + ((⦋ z / k ⦌ B \mod N) \mod N)$
56	55	oveq1d	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to ((\sum_{k \in A} B \mod N) + (⦋ z / k ⦌ B \mod N)) \mod N = ((\sum_{k \in A} (B \mod N) \mod N) + ((⦋ z / k ⦌ B \mod N) \mod N)) \mod N$
57	45 56	eqtrd	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to (\sum_{k \in A} B + ⦋ z / k ⦌ B) \mod N = ((\sum_{k \in A} (B \mod N) \mod N) + ((⦋ z / k ⦌ B \mod N) \mod N)) \mod N$
58		zmodcl	$⊢ (B \in ℤ \land N \in ℕ) \to B \mod N \in ℕ_{0}$
59	58	nn0zd	$⊢ (B \in ℤ \land N \in ℕ) \to B \mod N \in ℤ$
60	59	expcom	$⊢ N \in ℕ \to (B \in ℤ \to B \mod N \in ℤ)$
61	60	ralimdv	$⊢ N \in ℕ \to (\forall k \in A B \in ℤ \to \forall k \in A B \mod N \in ℤ)$
62	61	com12	$⊢ \forall k \in A B \in ℤ \to (N \in ℕ \to \forall k \in A B \mod N \in ℤ)$
63	62	adantr	$⊢ (\forall k \in A B \in ℤ \land \forall k \in \{z\} B \in ℤ) \to (N \in ℕ \to \forall k \in A B \mod N \in ℤ)$
64	27 63	sylbi	$⊢ \forall k \in (A \cup \{z\}) B \in ℤ \to (N \in ℕ \to \forall k \in A B \mod N \in ℤ)$
65	64	impcom	$⊢ (N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ) \to \forall k \in A B \mod N \in ℤ$
66	65	3adant1	$⊢ (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ) \to \forall k \in A B \mod N \in ℤ$
67	17 66	jca	$⊢ (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ) \to (A \in Fin \land \forall k \in A B \mod N \in ℤ)$
68		fsumzcl2	$⊢ (A \in Fin \land \forall k \in A B \mod N \in ℤ) \to \sum_{k \in A} (B \mod N) \in ℤ$
69	68	zred	$⊢ (A \in Fin \land \forall k \in A B \mod N \in ℤ) \to \sum_{k \in A} (B \mod N) \in ℝ$
70	67 69	syl	$⊢ (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ) \to \sum_{k \in A} (B \mod N) \in ℝ$
71	70	ad2antlr	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to \sum_{k \in A} (B \mod N) \in ℝ$
72	35	anim1i	$⊢ (\forall k \in (A \cup \{z\}) B \in ℤ \land N \in ℕ) \to (⦋ z / k ⦌ B \in ℤ \land N \in ℕ)$
73	72	ancoms	$⊢ (N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ) \to (⦋ z / k ⦌ B \in ℤ \land N \in ℕ)$
74		zmodcl	$⊢ (⦋ z / k ⦌ B \in ℤ \land N \in ℕ) \to ⦋ z / k ⦌ B \mod N \in ℕ_{0}$
75	73 74	syl	$⊢ (N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ) \to ⦋ z / k ⦌ B \mod N \in ℕ_{0}$
76	75	nn0red	$⊢ (N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ) \to ⦋ z / k ⦌ B \mod N \in ℝ$
77	76	3adant1	$⊢ (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ) \to ⦋ z / k ⦌ B \mod N \in ℝ$
78	77	ad2antlr	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to ⦋ z / k ⦌ B \mod N \in ℝ$
79	40	ad2antlr	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to N \in ℝ^{+}$
80		modaddabs	$⊢ (\sum_{k \in A} (B \mod N) \in ℝ \land ⦋ z / k ⦌ B \mod N \in ℝ \land N \in ℝ^{+}) \to ((\sum_{k \in A} (B \mod N) \mod N) + ((⦋ z / k ⦌ B \mod N) \mod N)) \mod N = (\sum_{k \in A} (B \mod N) + (⦋ z / k ⦌ B \mod N)) \mod N$
81	71 78 79 80	syl3anc	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to ((\sum_{k \in A} (B \mod N) \mod N) + ((⦋ z / k ⦌ B \mod N) \mod N)) \mod N = (\sum_{k \in A} (B \mod N) + (⦋ z / k ⦌ B \mod N)) \mod N$
82	60	ralimdv	$⊢ N \in ℕ \to (\forall k \in (A \cup \{z\}) B \in ℤ \to \forall k \in (A \cup \{z\}) B \mod N \in ℤ)$
83	82	imp	$⊢ (N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ) \to \forall k \in (A \cup \{z\}) B \mod N \in ℤ$
84	83	3adant1	$⊢ (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ) \to \forall k \in (A \cup \{z\}) B \mod N \in ℤ$
85	84	ad2antlr	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to \forall k \in (A \cup \{z\}) B \mod N \in ℤ$
86		fsumsplitsnun	$⊢ (A \in Fin \land (z \in V \land z \notin A) \land \forall k \in (A \cup \{z\}) B \mod N \in ℤ) \to \sum_{k \in A \cup \{z\}} (B \mod N) = \sum_{k \in A} (B \mod N) + ⦋ z / k ⦌ (B \mod N)$
87	18 22 85 86	syl3anc	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to \sum_{k \in A \cup \{z\}} (B \mod N) = \sum_{k \in A} (B \mod N) + ⦋ z / k ⦌ (B \mod N)$
88		csbov1g	$⊢ z \in V \to ⦋ z / k ⦌ (B \mod N) = ⦋ z / k ⦌ B \mod N$
89	21 88	mp1i	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to ⦋ z / k ⦌ (B \mod N) = ⦋ z / k ⦌ B \mod N$
90	89	oveq2d	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to \sum_{k \in A} (B \mod N) + ⦋ z / k ⦌ (B \mod N) = \sum_{k \in A} (B \mod N) + (⦋ z / k ⦌ B \mod N)$
91	87 90	eqtrd	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to \sum_{k \in A \cup \{z\}} (B \mod N) = \sum_{k \in A} (B \mod N) + (⦋ z / k ⦌ B \mod N)$
92	91	eqcomd	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to \sum_{k \in A} (B \mod N) + (⦋ z / k ⦌ B \mod N) = \sum_{k \in A \cup \{z\}} (B \mod N)$
93	92	oveq1d	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to (\sum_{k \in A} (B \mod N) + (⦋ z / k ⦌ B \mod N)) \mod N = \sum_{k \in A \cup \{z\}} (B \mod N) \mod N$
94	81 93	eqtrd	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to ((\sum_{k \in A} (B \mod N) \mod N) + ((⦋ z / k ⦌ B \mod N) \mod N)) \mod N = \sum_{k \in A \cup \{z\}} (B \mod N) \mod N$
95	26 57 94	3eqtrd	$⊢ ((z \notin A \land (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ)) \land \sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N) \to \sum_{k \in A \cup \{z\}} B \mod N = \sum_{k \in A \cup \{z\}} (B \mod N) \mod N$
96	95	exp31	$⊢ z \notin A \to ((A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ) \to (\sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N \to \sum_{k \in A \cup \{z\}} B \mod N = \sum_{k \in A \cup \{z\}} (B \mod N) \mod N))$
97	16 96	sylbir	$⊢ \neg z \in A \to ((A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ) \to (\sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N \to \sum_{k \in A \cup \{z\}} B \mod N = \sum_{k \in A \cup \{z\}} (B \mod N) \mod N))$
98	15 97	pm2.61i	$⊢ (A \in Fin \land N \in ℕ \land \forall k \in (A \cup \{z\}) B \in ℤ) \to (\sum_{k \in A} B \mod N = \sum_{k \in A} (B \mod N) \mod N \to \sum_{k \in A \cup \{z\}} B \mod N = \sum_{k \in A \cup \{z\}} (B \mod N) \mod N)$

Metamath Proof Explorer

Theorem modfsummods

Proof