dchrisumlem1

	Ref	Expression
Hypotheses	rpvmasum.z	$⊢ Z = ℤ / N ℤ$
	rpvmasum.l	$⊢ L = ℤRHom (Z)$
	rpvmasum.a	$⊢ φ \to N \in ℕ$
	rpvmasum.g	$⊢ G = DChr (N)$
	rpvmasum.d	$⊢ D = {Base}_{G}$
	rpvmasum.1	$⊢ \underset{˙}{1} = 0_{G}$
	dchrisum.b	$⊢ φ \to X \in D$
	dchrisum.n1	$⊢ φ \to X \neq \underset{˙}{1}$
	dchrisum.2	$⊢ n = x \to A = B$
	dchrisum.3	$⊢ φ \to M \in ℕ$
	dchrisum.4	$⊢ (φ \land n \in ℝ^{+}) \to A \in ℝ$
	dchrisum.5	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (M \leq n \land n \leq x)) \to B \leq A$
	dchrisum.6	$⊢ φ \to (n \in ℝ^{+} ⟼ A) \underset{ℝ}{⇝} 0$
	dchrisum.7	$⊢ F = (n \in ℕ ⟼ X (L (n)) A)$
	dchrisum.9	$⊢ φ \to R \in ℝ$
	dchrisum.10	$⊢ φ \to \forall u \in (0 ..^N) \|\sum_{n \in (0 ..^u)} X (L (n))\| \leq R$
Assertion	dchrisumlem1	$⊢ (φ \land U \in ℕ_{0}) \to \|\sum_{n \in (0 ..^U)} X (L (n))\| \leq R$

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	$⊢ Z = ℤ / N ℤ$
2		rpvmasum.l	$⊢ L = ℤRHom (Z)$
3		rpvmasum.a	$⊢ φ \to N \in ℕ$
4		rpvmasum.g	$⊢ G = DChr (N)$
5		rpvmasum.d	$⊢ D = {Base}_{G}$
6		rpvmasum.1	$⊢ \underset{˙}{1} = 0_{G}$
7		dchrisum.b	$⊢ φ \to X \in D$
8		dchrisum.n1	$⊢ φ \to X \neq \underset{˙}{1}$
9		dchrisum.2	$⊢ n = x \to A = B$
10		dchrisum.3	$⊢ φ \to M \in ℕ$
11		dchrisum.4	$⊢ (φ \land n \in ℝ^{+}) \to A \in ℝ$
12		dchrisum.5	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (M \leq n \land n \leq x)) \to B \leq A$
13		dchrisum.6	$⊢ φ \to (n \in ℝ^{+} ⟼ A) \underset{ℝ}{⇝} 0$
14		dchrisum.7	$⊢ F = (n \in ℕ ⟼ X (L (n)) A)$
15		dchrisum.9	$⊢ φ \to R \in ℝ$
16		dchrisum.10	$⊢ φ \to \forall u \in (0 ..^N) \|\sum_{n \in (0 ..^u)} X (L (n))\| \leq R$
17		fzodisj	$⊢ (0 ..^N ⌊\frac{U}{N}⌋) \cap (N ⌊\frac{U}{N}⌋ ..^U) = \emptyset$
18	17	a1i	$⊢ (φ \land U \in ℕ_{0}) \to (0 ..^N ⌊\frac{U}{N}⌋) \cap (N ⌊\frac{U}{N}⌋ ..^U) = \emptyset$
19	3	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
20	19	adantr	$⊢ (φ \land U \in ℕ_{0}) \to N \in ℕ_{0}$
21		nn0re	$⊢ U \in ℕ_{0} \to U \in ℝ$
22	21	adantl	$⊢ (φ \land U \in ℕ_{0}) \to U \in ℝ$
23	3	adantr	$⊢ (φ \land U \in ℕ_{0}) \to N \in ℕ$
24	22 23	nndivred	$⊢ (φ \land U \in ℕ_{0}) \to \frac{U}{N} \in ℝ$
25	23	nnrpd	$⊢ (φ \land U \in ℕ_{0}) \to N \in ℝ^{+}$
26		nn0ge0	$⊢ U \in ℕ_{0} \to 0 \leq U$
27	26	adantl	$⊢ (φ \land U \in ℕ_{0}) \to 0 \leq U$
28	22 25 27	divge0d	$⊢ (φ \land U \in ℕ_{0}) \to 0 \leq \frac{U}{N}$
29		flge0nn0	$⊢ (\frac{U}{N} \in ℝ \land 0 \leq \frac{U}{N}) \to ⌊\frac{U}{N}⌋ \in ℕ_{0}$
30	24 28 29	syl2anc	$⊢ (φ \land U \in ℕ_{0}) \to ⌊\frac{U}{N}⌋ \in ℕ_{0}$
31	20 30	nn0mulcld	$⊢ (φ \land U \in ℕ_{0}) \to N ⌊\frac{U}{N}⌋ \in ℕ_{0}$
32		flle	$⊢ \frac{U}{N} \in ℝ \to ⌊\frac{U}{N}⌋ \leq \frac{U}{N}$
33	24 32	syl	$⊢ (φ \land U \in ℕ_{0}) \to ⌊\frac{U}{N}⌋ \leq \frac{U}{N}$
34		reflcl	$⊢ \frac{U}{N} \in ℝ \to ⌊\frac{U}{N}⌋ \in ℝ$
35	24 34	syl	$⊢ (φ \land U \in ℕ_{0}) \to ⌊\frac{U}{N}⌋ \in ℝ$
36	35 22 25	lemuldiv2d	$⊢ (φ \land U \in ℕ_{0}) \to (N ⌊\frac{U}{N}⌋ \leq U \leftrightarrow ⌊\frac{U}{N}⌋ \leq \frac{U}{N})$
37	33 36	mpbird	$⊢ (φ \land U \in ℕ_{0}) \to N ⌊\frac{U}{N}⌋ \leq U$
38		fznn0	$⊢ U \in ℕ_{0} \to (N ⌊\frac{U}{N}⌋ \in (0 \dots U) \leftrightarrow (N ⌊\frac{U}{N}⌋ \in ℕ_{0} \land N ⌊\frac{U}{N}⌋ \leq U))$
39	38	adantl	$⊢ (φ \land U \in ℕ_{0}) \to (N ⌊\frac{U}{N}⌋ \in (0 \dots U) \leftrightarrow (N ⌊\frac{U}{N}⌋ \in ℕ_{0} \land N ⌊\frac{U}{N}⌋ \leq U))$
40	31 37 39	mpbir2and	$⊢ (φ \land U \in ℕ_{0}) \to N ⌊\frac{U}{N}⌋ \in (0 \dots U)$
41		fzosplit	$⊢ N ⌊\frac{U}{N}⌋ \in (0 \dots U) \to (0 ..^U) = (0 ..^N ⌊\frac{U}{N}⌋) \cup (N ⌊\frac{U}{N}⌋ ..^U)$
42	40 41	syl	$⊢ (φ \land U \in ℕ_{0}) \to (0 ..^U) = (0 ..^N ⌊\frac{U}{N}⌋) \cup (N ⌊\frac{U}{N}⌋ ..^U)$
43		fzofi	$⊢ (0 ..^U) \in Fin$
44	43	a1i	$⊢ (φ \land U \in ℕ_{0}) \to (0 ..^U) \in Fin$
45	7	ad2antrr	$⊢ ((φ \land U \in ℕ_{0}) \land n \in (0 ..^U)) \to X \in D$
46		elfzoelz	$⊢ n \in (0 ..^U) \to n \in ℤ$
47	46	adantl	$⊢ ((φ \land U \in ℕ_{0}) \land n \in (0 ..^U)) \to n \in ℤ$
48	4 1 5 2 45 47	dchrzrhcl	$⊢ ((φ \land U \in ℕ_{0}) \land n \in (0 ..^U)) \to X (L (n)) \in ℂ$
49	18 42 44 48	fsumsplit	$⊢ (φ \land U \in ℕ_{0}) \to \sum_{n \in (0 ..^U)} X (L (n)) = \sum_{n \in (0 ..^N ⌊\frac{U}{N}⌋)} X (L (n)) + \sum_{n \in (N ⌊\frac{U}{N}⌋ ..^U)} X (L (n))$
50		oveq2	$⊢ k = 0 \to N k = N \cdot 0$
51	50	oveq2d	$⊢ k = 0 \to (0 ..^N k) = (0 ..^N \cdot 0)$
52	51	sumeq1d	$⊢ k = 0 \to \sum_{n \in (0 ..^N k)} X (L (n)) = \sum_{n \in (0 ..^N \cdot 0)} X (L (n))$
53	52	eqeq1d	$⊢ k = 0 \to (\sum_{n \in (0 ..^N k)} X (L (n)) = 0 \leftrightarrow \sum_{n \in (0 ..^N \cdot 0)} X (L (n)) = 0)$
54	53	imbi2d	$⊢ k = 0 \to ((φ \to \sum_{n \in (0 ..^N k)} X (L (n)) = 0) \leftrightarrow (φ \to \sum_{n \in (0 ..^N \cdot 0)} X (L (n)) = 0))$
55		oveq2	$⊢ k = m \to N k = N m$
56	55	oveq2d	$⊢ k = m \to (0 ..^N k) = (0 ..^N m)$
57	56	sumeq1d	$⊢ k = m \to \sum_{n \in (0 ..^N k)} X (L (n)) = \sum_{n \in (0 ..^N m)} X (L (n))$
58	57	eqeq1d	$⊢ k = m \to (\sum_{n \in (0 ..^N k)} X (L (n)) = 0 \leftrightarrow \sum_{n \in (0 ..^N m)} X (L (n)) = 0)$
59	58	imbi2d	$⊢ k = m \to ((φ \to \sum_{n \in (0 ..^N k)} X (L (n)) = 0) \leftrightarrow (φ \to \sum_{n \in (0 ..^N m)} X (L (n)) = 0))$
60		oveq2	$⊢ k = m + 1 \to N k = N (m + 1)$
61	60	oveq2d	$⊢ k = m + 1 \to (0 ..^N k) = (0 ..^N (m + 1))$
62	61	sumeq1d	$⊢ k = m + 1 \to \sum_{n \in (0 ..^N k)} X (L (n)) = \sum_{n \in (0 ..^N (m + 1))} X (L (n))$
63	62	eqeq1d	$⊢ k = m + 1 \to (\sum_{n \in (0 ..^N k)} X (L (n)) = 0 \leftrightarrow \sum_{n \in (0 ..^N (m + 1))} X (L (n)) = 0)$
64	63	imbi2d	$⊢ k = m + 1 \to ((φ \to \sum_{n \in (0 ..^N k)} X (L (n)) = 0) \leftrightarrow (φ \to \sum_{n \in (0 ..^N (m + 1))} X (L (n)) = 0))$
65		oveq2	$⊢ k = ⌊\frac{U}{N}⌋ \to N k = N ⌊\frac{U}{N}⌋$
66	65	oveq2d	$⊢ k = ⌊\frac{U}{N}⌋ \to (0 ..^N k) = (0 ..^N ⌊\frac{U}{N}⌋)$
67	66	sumeq1d	$⊢ k = ⌊\frac{U}{N}⌋ \to \sum_{n \in (0 ..^N k)} X (L (n)) = \sum_{n \in (0 ..^N ⌊\frac{U}{N}⌋)} X (L (n))$
68	67	eqeq1d	$⊢ k = ⌊\frac{U}{N}⌋ \to (\sum_{n \in (0 ..^N k)} X (L (n)) = 0 \leftrightarrow \sum_{n \in (0 ..^N ⌊\frac{U}{N}⌋)} X (L (n)) = 0)$
69	68	imbi2d	$⊢ k = ⌊\frac{U}{N}⌋ \to ((φ \to \sum_{n \in (0 ..^N k)} X (L (n)) = 0) \leftrightarrow (φ \to \sum_{n \in (0 ..^N ⌊\frac{U}{N}⌋)} X (L (n)) = 0))$
70	3	nncnd	$⊢ φ \to N \in ℂ$
71	70	mul01d	$⊢ φ \to N \cdot 0 = 0$
72	71	oveq2d	$⊢ φ \to (0 ..^N \cdot 0) = (0 ..^0)$
73		fzo0	$⊢ (0 ..^0) = \emptyset$
74	72 73	eqtrdi	$⊢ φ \to (0 ..^N \cdot 0) = \emptyset$
75	74	sumeq1d	$⊢ φ \to \sum_{n \in (0 ..^N \cdot 0)} X (L (n)) = \sum_{n \in \emptyset} X (L (n))$
76		sum0	$⊢ \sum_{n \in \emptyset} X (L (n)) = 0$
77	75 76	eqtrdi	$⊢ φ \to \sum_{n \in (0 ..^N \cdot 0)} X (L (n)) = 0$
78		oveq1	$⊢ \sum_{n \in (0 ..^N m)} X (L (n)) = 0 \to \sum_{n \in (0 ..^N m)} X (L (n)) + \sum_{n \in (N m ..^N (m + 1))} X (L (n)) = 0 + \sum_{n \in (N m ..^N (m + 1))} X (L (n))$
79		fzodisj	$⊢ (0 ..^N m) \cap (N m ..^N (m + 1)) = \emptyset$
80	79	a1i	$⊢ (φ \land m \in ℕ_{0}) \to (0 ..^N m) \cap (N m ..^N (m + 1)) = \emptyset$
81		nn0re	$⊢ m \in ℕ_{0} \to m \in ℝ$
82	81	adantl	$⊢ (φ \land m \in ℕ_{0}) \to m \in ℝ$
83	82	lep1d	$⊢ (φ \land m \in ℕ_{0}) \to m \leq m + 1$
84		peano2re	$⊢ m \in ℝ \to m + 1 \in ℝ$
85	82 84	syl	$⊢ (φ \land m \in ℕ_{0}) \to m + 1 \in ℝ$
86	3	adantr	$⊢ (φ \land m \in ℕ_{0}) \to N \in ℕ$
87	86	nnred	$⊢ (φ \land m \in ℕ_{0}) \to N \in ℝ$
88	86	nngt0d	$⊢ (φ \land m \in ℕ_{0}) \to 0 < N$
89		lemul2	$⊢ (m \in ℝ \land m + 1 \in ℝ \land (N \in ℝ \land 0 < N)) \to (m \leq m + 1 \leftrightarrow N m \leq N (m + 1))$
90	82 85 87 88 89	syl112anc	$⊢ (φ \land m \in ℕ_{0}) \to (m \leq m + 1 \leftrightarrow N m \leq N (m + 1))$
91	83 90	mpbid	$⊢ (φ \land m \in ℕ_{0}) \to N m \leq N (m + 1)$
92		nn0mulcl	$⊢ (N \in ℕ_{0} \land m \in ℕ_{0}) \to N m \in ℕ_{0}$
93	19 92	sylan	$⊢ (φ \land m \in ℕ_{0}) \to N m \in ℕ_{0}$
94		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
95	93 94	eleqtrdi	$⊢ (φ \land m \in ℕ_{0}) \to N m \in ℤ_{\geq 0}$
96		nn0p1nn	$⊢ m \in ℕ_{0} \to m + 1 \in ℕ$
97		nnmulcl	$⊢ (N \in ℕ \land m + 1 \in ℕ) \to N (m + 1) \in ℕ$
98	3 96 97	syl2an	$⊢ (φ \land m \in ℕ_{0}) \to N (m + 1) \in ℕ$
99	98	nnzd	$⊢ (φ \land m \in ℕ_{0}) \to N (m + 1) \in ℤ$
100		elfz5	$⊢ (N m \in ℤ_{\geq 0} \land N (m + 1) \in ℤ) \to (N m \in (0 \dots N (m + 1)) \leftrightarrow N m \leq N (m + 1))$
101	95 99 100	syl2anc	$⊢ (φ \land m \in ℕ_{0}) \to (N m \in (0 \dots N (m + 1)) \leftrightarrow N m \leq N (m + 1))$
102	91 101	mpbird	$⊢ (φ \land m \in ℕ_{0}) \to N m \in (0 \dots N (m + 1))$
103		fzosplit	$⊢ N m \in (0 \dots N (m + 1)) \to (0 ..^N (m + 1)) = (0 ..^N m) \cup (N m ..^N (m + 1))$
104	102 103	syl	$⊢ (φ \land m \in ℕ_{0}) \to (0 ..^N (m + 1)) = (0 ..^N m) \cup (N m ..^N (m + 1))$
105		fzofi	$⊢ (0 ..^N (m + 1)) \in Fin$
106	105	a1i	$⊢ (φ \land m \in ℕ_{0}) \to (0 ..^N (m + 1)) \in Fin$
107	7	ad2antrr	$⊢ ((φ \land m \in ℕ_{0}) \land n \in (0 ..^N (m + 1))) \to X \in D$
108		elfzoelz	$⊢ n \in (0 ..^N (m + 1)) \to n \in ℤ$
109	108	adantl	$⊢ ((φ \land m \in ℕ_{0}) \land n \in (0 ..^N (m + 1))) \to n \in ℤ$
110	4 1 5 2 107 109	dchrzrhcl	$⊢ ((φ \land m \in ℕ_{0}) \land n \in (0 ..^N (m + 1))) \to X (L (n)) \in ℂ$
111	80 104 106 110	fsumsplit	$⊢ (φ \land m \in ℕ_{0}) \to \sum_{n \in (0 ..^N (m + 1))} X (L (n)) = \sum_{n \in (0 ..^N m)} X (L (n)) + \sum_{n \in (N m ..^N (m + 1))} X (L (n))$
112	86	nncnd	$⊢ (φ \land m \in ℕ_{0}) \to N \in ℂ$
113	82	recnd	$⊢ (φ \land m \in ℕ_{0}) \to m \in ℂ$
114		1cnd	$⊢ (φ \land m \in ℕ_{0}) \to 1 \in ℂ$
115	112 113 114	adddid	$⊢ (φ \land m \in ℕ_{0}) \to N (m + 1) = N m + N \cdot 1$
116	112	mulridd	$⊢ (φ \land m \in ℕ_{0}) \to N \cdot 1 = N$
117	116	oveq2d	$⊢ (φ \land m \in ℕ_{0}) \to N m + N \cdot 1 = N m + N$
118	115 117	eqtrd	$⊢ (φ \land m \in ℕ_{0}) \to N (m + 1) = N m + N$
119	118	oveq2d	$⊢ (φ \land m \in ℕ_{0}) \to (N m ..^N (m + 1)) = (N m ..^N m + N)$
120	119	sumeq1d	$⊢ (φ \land m \in ℕ_{0}) \to \sum_{n \in (N m ..^N (m + 1))} X (L (n)) = \sum_{n \in (N m ..^N m + N)} X (L (n))$
121		oveq2	$⊢ k = N \to N m + k = N m + N$
122	121	oveq2d	$⊢ k = N \to (N m ..^N m + k) = (N m ..^N m + N)$
123	122	sumeq1d	$⊢ k = N \to \sum_{n \in (N m ..^N m + k)} X (L (n)) = \sum_{n \in (N m ..^N m + N)} X (L (n))$
124		oveq2	$⊢ k = N \to (0 ..^k) = (0 ..^N)$
125	124	sumeq1d	$⊢ k = N \to \sum_{n \in (0 ..^k)} X (L (n)) = \sum_{n \in (0 ..^N)} X (L (n))$
126	123 125	eqeq12d	$⊢ k = N \to (\sum_{n \in (N m ..^N m + k)} X (L (n)) = \sum_{n \in (0 ..^k)} X (L (n)) \leftrightarrow \sum_{n \in (N m ..^N m + N)} X (L (n)) = \sum_{n \in (0 ..^N)} X (L (n)))$
127	93	nn0zd	$⊢ (φ \land m \in ℕ_{0}) \to N m \in ℤ$
128	127	adantr	$⊢ ((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \to N m \in ℤ$
129		nn0z	$⊢ k \in ℕ_{0} \to k \in ℤ$
130		zaddcl	$⊢ (N m \in ℤ \land k \in ℤ) \to N m + k \in ℤ$
131	127 129 130	syl2an	$⊢ ((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \to N m + k \in ℤ$
132		peano2zm	$⊢ N m + k \in ℤ \to N m + k - 1 \in ℤ$
133	131 132	syl	$⊢ ((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \to N m + k - 1 \in ℤ$
134	7	ad3antrrr	$⊢ (((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \land n \in (N m \dots N m + k - 1)) \to X \in D$
135		elfzelz	$⊢ n \in (N m \dots N m + k - 1) \to n \in ℤ$
136	135	adantl	$⊢ (((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \land n \in (N m \dots N m + k - 1)) \to n \in ℤ$
137	4 1 5 2 134 136	dchrzrhcl	$⊢ (((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \land n \in (N m \dots N m + k - 1)) \to X (L (n)) \in ℂ$
138		2fveq3	$⊢ n = i + N m \to X (L (n)) = X (L (i + N m))$
139	128 128 133 137 138	fsumshftm	$⊢ ((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \to \sum_{n = N m}^{N m + k - 1} X (L (n)) = \sum_{i = N m - N m}^{(N m + k) - 1 - N m} X (L (i + N m))$
140		fzoval	$⊢ N m + k \in ℤ \to (N m ..^N m + k) = (N m \dots N m + k - 1)$
141	131 140	syl	$⊢ ((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \to (N m ..^N m + k) = (N m \dots N m + k - 1)$
142	141	sumeq1d	$⊢ ((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \to \sum_{n \in (N m ..^N m + k)} X (L (n)) = \sum_{n = N m}^{N m + k - 1} X (L (n))$
143	129	adantl	$⊢ ((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \to k \in ℤ$
144		fzoval	$⊢ k \in ℤ \to (0 ..^k) = (0 \dots k - 1)$
145	143 144	syl	$⊢ ((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \to (0 ..^k) = (0 \dots k - 1)$
146	128	zcnd	$⊢ ((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \to N m \in ℂ$
147	146	subidd	$⊢ ((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \to N m - N m = 0$
148	131	zcnd	$⊢ ((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \to N m + k \in ℂ$
149		1cnd	$⊢ ((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \to 1 \in ℂ$
150	148 149 146	sub32d	$⊢ ((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \to (N m + k) - 1 - N m = (N m + k) - N m - 1$
151		nn0cn	$⊢ k \in ℕ_{0} \to k \in ℂ$
152	151	adantl	$⊢ ((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \to k \in ℂ$
153	146 152	pncan2d	$⊢ ((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \to N m + k - N m = k$
154	153	oveq1d	$⊢ ((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \to (N m + k) - N m - 1 = k - 1$
155	150 154	eqtrd	$⊢ ((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \to (N m + k) - 1 - N m = k - 1$
156	147 155	oveq12d	$⊢ ((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \to (N m - N m \dots (N m + k) - 1 - N m) = (0 \dots k - 1)$
157	145 156	eqtr4d	$⊢ ((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \to (0 ..^k) = (N m - N m \dots (N m + k) - 1 - N m)$
158	157	sumeq1d	$⊢ ((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \to \sum_{i \in (0 ..^k)} X (L (i + N m)) = \sum_{i = N m - N m}^{(N m + k) - 1 - N m} X (L (i + N m))$
159	139 142 158	3eqtr4d	$⊢ ((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \to \sum_{n \in (N m ..^N m + k)} X (L (n)) = \sum_{i \in (0 ..^k)} X (L (i + N m))$
160	3	nnzd	$⊢ φ \to N \in ℤ$
161		nn0z	$⊢ m \in ℕ_{0} \to m \in ℤ$
162		dvdsmul1	$⊢ (N \in ℤ \land m \in ℤ) \to N ∥ N m$
163	160 161 162	syl2an	$⊢ (φ \land m \in ℕ_{0}) \to N ∥ N m$
164	163	ad2antrr	$⊢ (((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \land i \in (0 ..^k)) \to N ∥ N m$
165		elfzoelz	$⊢ i \in (0 ..^k) \to i \in ℤ$
166	165	adantl	$⊢ (((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \land i \in (0 ..^k)) \to i \in ℤ$
167	166	zcnd	$⊢ (((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \land i \in (0 ..^k)) \to i \in ℂ$
168	146	adantr	$⊢ (((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \land i \in (0 ..^k)) \to N m \in ℂ$
169	167 168	pncan2d	$⊢ (((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \land i \in (0 ..^k)) \to i + N m - i = N m$
170	164 169	breqtrrd	$⊢ (((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \land i \in (0 ..^k)) \to N ∥ (i + N m - i)$
171	86	nnnn0d	$⊢ (φ \land m \in ℕ_{0}) \to N \in ℕ_{0}$
172	171	ad2antrr	$⊢ (((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \land i \in (0 ..^k)) \to N \in ℕ_{0}$
173		zaddcl	$⊢ (i \in ℤ \land N m \in ℤ) \to i + N m \in ℤ$
174	165 128 173	syl2anr	$⊢ (((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \land i \in (0 ..^k)) \to i + N m \in ℤ$
175	1 2	zndvds	$⊢ (N \in ℕ_{0} \land i + N m \in ℤ \land i \in ℤ) \to (L (i + N m) = L (i) \leftrightarrow N ∥ (i + N m - i))$
176	172 174 166 175	syl3anc	$⊢ (((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \land i \in (0 ..^k)) \to (L (i + N m) = L (i) \leftrightarrow N ∥ (i + N m - i))$
177	170 176	mpbird	$⊢ (((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \land i \in (0 ..^k)) \to L (i + N m) = L (i)$
178	177	fveq2d	$⊢ (((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \land i \in (0 ..^k)) \to X (L (i + N m)) = X (L (i))$
179	178	sumeq2dv	$⊢ ((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \to \sum_{i \in (0 ..^k)} X (L (i + N m)) = \sum_{i \in (0 ..^k)} X (L (i))$
180		2fveq3	$⊢ i = n \to X (L (i)) = X (L (n))$
181	180	cbvsumv	$⊢ \sum_{i \in (0 ..^k)} X (L (i)) = \sum_{n \in (0 ..^k)} X (L (n))$
182	179 181	eqtrdi	$⊢ ((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \to \sum_{i \in (0 ..^k)} X (L (i + N m)) = \sum_{n \in (0 ..^k)} X (L (n))$
183	159 182	eqtrd	$⊢ ((φ \land m \in ℕ_{0}) \land k \in ℕ_{0}) \to \sum_{n \in (N m ..^N m + k)} X (L (n)) = \sum_{n \in (0 ..^k)} X (L (n))$
184	183	ralrimiva	$⊢ (φ \land m \in ℕ_{0}) \to \forall k \in ℕ_{0} \sum_{n \in (N m ..^N m + k)} X (L (n)) = \sum_{n \in (0 ..^k)} X (L (n))$
185	126 184 171	rspcdva	$⊢ (φ \land m \in ℕ_{0}) \to \sum_{n \in (N m ..^N m + N)} X (L (n)) = \sum_{n \in (0 ..^N)} X (L (n))$
186		fveq2	$⊢ k = L (n) \to X (k) = X (L (n))$
187	3	nnne0d	$⊢ φ \to N \neq 0$
188		ifnefalse	$⊢ N \neq 0 \to if (N = 0, ℤ, (0 ..^N)) = (0 ..^N)$
189	187 188	syl	$⊢ φ \to if (N = 0, ℤ, (0 ..^N)) = (0 ..^N)$
190		fzofi	$⊢ (0 ..^N) \in Fin$
191	189 190	eqeltrdi	$⊢ φ \to if (N = 0, ℤ, (0 ..^N)) \in Fin$
192		eqid	$⊢ {Base}_{Z} = {Base}_{Z}$
193	2	reseq1i	$⊢ {L ↾}_{if (N = 0, ℤ, (0 ..^N))} = {ℤRHom (Z) ↾}_{if (N = 0, ℤ, (0 ..^N))}$
194		eqid	$⊢ if (N = 0, ℤ, (0 ..^N)) = if (N = 0, ℤ, (0 ..^N))$
195	1 192 193 194	znf1o	$⊢ N \in ℕ_{0} \to ({L ↾}_{if (N = 0, ℤ, (0 ..^N))}) : if (N = 0, ℤ, (0 ..^N)) \underset{1-1 onto}{⟶} {Base}_{Z}$
196	19 195	syl	$⊢ φ \to ({L ↾}_{if (N = 0, ℤ, (0 ..^N))}) : if (N = 0, ℤ, (0 ..^N)) \underset{1-1 onto}{⟶} {Base}_{Z}$
197		fvres	$⊢ n \in if (N = 0, ℤ, (0 ..^N)) \to ({L ↾}_{if (N = 0, ℤ, (0 ..^N))}) (n) = L (n)$
198	197	adantl	$⊢ (φ \land n \in if (N = 0, ℤ, (0 ..^N))) \to ({L ↾}_{if (N = 0, ℤ, (0 ..^N))}) (n) = L (n)$
199	4 1 5 192 7	dchrf	$⊢ φ \to X : {Base}_{Z} ⟶ ℂ$
200	199	ffvelcdmda	$⊢ (φ \land k \in {Base}_{Z}) \to X (k) \in ℂ$
201	186 191 196 198 200	fsumf1o	$⊢ φ \to \sum_{k \in {Base}_{Z}} X (k) = \sum_{n \in if (N = 0, ℤ, (0 ..^N))} X (L (n))$
202	4 1 5 6 7 192	dchrsum	$⊢ φ \to \sum_{k \in {Base}_{Z}} X (k) = if (X = \underset{˙}{1}, ϕ (N), 0)$
203		ifnefalse	$⊢ X \neq \underset{˙}{1} \to if (X = \underset{˙}{1}, ϕ (N), 0) = 0$
204	8 203	syl	$⊢ φ \to if (X = \underset{˙}{1}, ϕ (N), 0) = 0$
205	202 204	eqtrd	$⊢ φ \to \sum_{k \in {Base}_{Z}} X (k) = 0$
206	189	sumeq1d	$⊢ φ \to \sum_{n \in if (N = 0, ℤ, (0 ..^N))} X (L (n)) = \sum_{n \in (0 ..^N)} X (L (n))$
207	201 205 206	3eqtr3rd	$⊢ φ \to \sum_{n \in (0 ..^N)} X (L (n)) = 0$
208	207	adantr	$⊢ (φ \land m \in ℕ_{0}) \to \sum_{n \in (0 ..^N)} X (L (n)) = 0$
209	120 185 208	3eqtrd	$⊢ (φ \land m \in ℕ_{0}) \to \sum_{n \in (N m ..^N (m + 1))} X (L (n)) = 0$
210	209	oveq2d	$⊢ (φ \land m \in ℕ_{0}) \to 0 + \sum_{n \in (N m ..^N (m + 1))} X (L (n)) = 0 + 0$
211		00id	$⊢ 0 + 0 = 0$
212	210 211	eqtr2di	$⊢ (φ \land m \in ℕ_{0}) \to 0 = 0 + \sum_{n \in (N m ..^N (m + 1))} X (L (n))$
213	111 212	eqeq12d	$⊢ (φ \land m \in ℕ_{0}) \to (\sum_{n \in (0 ..^N (m + 1))} X (L (n)) = 0 \leftrightarrow \sum_{n \in (0 ..^N m)} X (L (n)) + \sum_{n \in (N m ..^N (m + 1))} X (L (n)) = 0 + \sum_{n \in (N m ..^N (m + 1))} X (L (n)))$
214	78 213	imbitrrid	$⊢ (φ \land m \in ℕ_{0}) \to (\sum_{n \in (0 ..^N m)} X (L (n)) = 0 \to \sum_{n \in (0 ..^N (m + 1))} X (L (n)) = 0)$
215	214	expcom	$⊢ m \in ℕ_{0} \to (φ \to (\sum_{n \in (0 ..^N m)} X (L (n)) = 0 \to \sum_{n \in (0 ..^N (m + 1))} X (L (n)) = 0))$
216	215	a2d	$⊢ m \in ℕ_{0} \to ((φ \to \sum_{n \in (0 ..^N m)} X (L (n)) = 0) \to (φ \to \sum_{n \in (0 ..^N (m + 1))} X (L (n)) = 0))$
217	54 59 64 69 77 216	nn0ind	$⊢ ⌊\frac{U}{N}⌋ \in ℕ_{0} \to (φ \to \sum_{n \in (0 ..^N ⌊\frac{U}{N}⌋)} X (L (n)) = 0)$
218	217	impcom	$⊢ (φ \land ⌊\frac{U}{N}⌋ \in ℕ_{0}) \to \sum_{n \in (0 ..^N ⌊\frac{U}{N}⌋)} X (L (n)) = 0$
219	30 218	syldan	$⊢ (φ \land U \in ℕ_{0}) \to \sum_{n \in (0 ..^N ⌊\frac{U}{N}⌋)} X (L (n)) = 0$
220		modval	$⊢ (U \in ℝ \land N \in ℝ^{+}) \to U \mod N = U - N ⌊\frac{U}{N}⌋$
221	22 25 220	syl2anc	$⊢ (φ \land U \in ℕ_{0}) \to U \mod N = U - N ⌊\frac{U}{N}⌋$
222	221	oveq2d	$⊢ (φ \land U \in ℕ_{0}) \to N ⌊\frac{U}{N}⌋ + (U \mod N) = N ⌊\frac{U}{N}⌋ + U - N ⌊\frac{U}{N}⌋$
223	31	nn0cnd	$⊢ (φ \land U \in ℕ_{0}) \to N ⌊\frac{U}{N}⌋ \in ℂ$
224		nn0cn	$⊢ U \in ℕ_{0} \to U \in ℂ$
225	224	adantl	$⊢ (φ \land U \in ℕ_{0}) \to U \in ℂ$
226	223 225	pncan3d	$⊢ (φ \land U \in ℕ_{0}) \to N ⌊\frac{U}{N}⌋ + U - N ⌊\frac{U}{N}⌋ = U$
227	222 226	eqtr2d	$⊢ (φ \land U \in ℕ_{0}) \to U = N ⌊\frac{U}{N}⌋ + (U \mod N)$
228	227	oveq2d	$⊢ (φ \land U \in ℕ_{0}) \to (N ⌊\frac{U}{N}⌋ ..^U) = (N ⌊\frac{U}{N}⌋ ..^N ⌊\frac{U}{N}⌋ + (U \mod N))$
229	228	sumeq1d	$⊢ (φ \land U \in ℕ_{0}) \to \sum_{n \in (N ⌊\frac{U}{N}⌋ ..^U)} X (L (n)) = \sum_{n \in (N ⌊\frac{U}{N}⌋ ..^N ⌊\frac{U}{N}⌋ + (U \mod N))} X (L (n))$
230		nn0z	$⊢ U \in ℕ_{0} \to U \in ℤ$
231		zmodcl	$⊢ (U \in ℤ \land N \in ℕ) \to U \mod N \in ℕ_{0}$
232	230 3 231	syl2anr	$⊢ (φ \land U \in ℕ_{0}) \to U \mod N \in ℕ_{0}$
233	184	ralrimiva	$⊢ φ \to \forall m \in ℕ_{0} \forall k \in ℕ_{0} \sum_{n \in (N m ..^N m + k)} X (L (n)) = \sum_{n \in (0 ..^k)} X (L (n))$
234	233	adantr	$⊢ (φ \land U \in ℕ_{0}) \to \forall m \in ℕ_{0} \forall k \in ℕ_{0} \sum_{n \in (N m ..^N m + k)} X (L (n)) = \sum_{n \in (0 ..^k)} X (L (n))$
235		oveq2	$⊢ m = ⌊\frac{U}{N}⌋ \to N m = N ⌊\frac{U}{N}⌋$
236	235	oveq1d	$⊢ m = ⌊\frac{U}{N}⌋ \to N m + k = N ⌊\frac{U}{N}⌋ + k$
237	235 236	oveq12d	$⊢ m = ⌊\frac{U}{N}⌋ \to (N m ..^N m + k) = (N ⌊\frac{U}{N}⌋ ..^N ⌊\frac{U}{N}⌋ + k)$
238	237	sumeq1d	$⊢ m = ⌊\frac{U}{N}⌋ \to \sum_{n \in (N m ..^N m + k)} X (L (n)) = \sum_{n \in (N ⌊\frac{U}{N}⌋ ..^N ⌊\frac{U}{N}⌋ + k)} X (L (n))$
239	238	eqeq1d	$⊢ m = ⌊\frac{U}{N}⌋ \to (\sum_{n \in (N m ..^N m + k)} X (L (n)) = \sum_{n \in (0 ..^k)} X (L (n)) \leftrightarrow \sum_{n \in (N ⌊\frac{U}{N}⌋ ..^N ⌊\frac{U}{N}⌋ + k)} X (L (n)) = \sum_{n \in (0 ..^k)} X (L (n)))$
240		oveq2	$⊢ k = U \mod N \to N ⌊\frac{U}{N}⌋ + k = N ⌊\frac{U}{N}⌋ + (U \mod N)$
241	240	oveq2d	$⊢ k = U \mod N \to (N ⌊\frac{U}{N}⌋ ..^N ⌊\frac{U}{N}⌋ + k) = (N ⌊\frac{U}{N}⌋ ..^N ⌊\frac{U}{N}⌋ + (U \mod N))$
242	241	sumeq1d	$⊢ k = U \mod N \to \sum_{n \in (N ⌊\frac{U}{N}⌋ ..^N ⌊\frac{U}{N}⌋ + k)} X (L (n)) = \sum_{n \in (N ⌊\frac{U}{N}⌋ ..^N ⌊\frac{U}{N}⌋ + (U \mod N))} X (L (n))$
243		oveq2	$⊢ k = U \mod N \to (0 ..^k) = (0 ..^U \mod N)$
244	243	sumeq1d	$⊢ k = U \mod N \to \sum_{n \in (0 ..^k)} X (L (n)) = \sum_{n \in (0 ..^U \mod N)} X (L (n))$
245	242 244	eqeq12d	$⊢ k = U \mod N \to (\sum_{n \in (N ⌊\frac{U}{N}⌋ ..^N ⌊\frac{U}{N}⌋ + k)} X (L (n)) = \sum_{n \in (0 ..^k)} X (L (n)) \leftrightarrow \sum_{n \in (N ⌊\frac{U}{N}⌋ ..^N ⌊\frac{U}{N}⌋ + (U \mod N))} X (L (n)) = \sum_{n \in (0 ..^U \mod N)} X (L (n)))$
246	239 245	rspc2va	$⊢ ((⌊\frac{U}{N}⌋ \in ℕ_{0} \land U \mod N \in ℕ_{0}) \land \forall m \in ℕ_{0} \forall k \in ℕ_{0} \sum_{n \in (N m ..^N m + k)} X (L (n)) = \sum_{n \in (0 ..^k)} X (L (n))) \to \sum_{n \in (N ⌊\frac{U}{N}⌋ ..^N ⌊\frac{U}{N}⌋ + (U \mod N))} X (L (n)) = \sum_{n \in (0 ..^U \mod N)} X (L (n))$
247	30 232 234 246	syl21anc	$⊢ (φ \land U \in ℕ_{0}) \to \sum_{n \in (N ⌊\frac{U}{N}⌋ ..^N ⌊\frac{U}{N}⌋ + (U \mod N))} X (L (n)) = \sum_{n \in (0 ..^U \mod N)} X (L (n))$
248	229 247	eqtrd	$⊢ (φ \land U \in ℕ_{0}) \to \sum_{n \in (N ⌊\frac{U}{N}⌋ ..^U)} X (L (n)) = \sum_{n \in (0 ..^U \mod N)} X (L (n))$
249	219 248	oveq12d	$⊢ (φ \land U \in ℕ_{0}) \to \sum_{n \in (0 ..^N ⌊\frac{U}{N}⌋)} X (L (n)) + \sum_{n \in (N ⌊\frac{U}{N}⌋ ..^U)} X (L (n)) = 0 + \sum_{n \in (0 ..^U \mod N)} X (L (n))$
250		fzofi	$⊢ (0 ..^U \mod N) \in Fin$
251	250	a1i	$⊢ (φ \land U \in ℕ_{0}) \to (0 ..^U \mod N) \in Fin$
252	7	ad2antrr	$⊢ ((φ \land U \in ℕ_{0}) \land n \in (0 ..^U \mod N)) \to X \in D$
253		elfzoelz	$⊢ n \in (0 ..^U \mod N) \to n \in ℤ$
254	253	adantl	$⊢ ((φ \land U \in ℕ_{0}) \land n \in (0 ..^U \mod N)) \to n \in ℤ$
255	4 1 5 2 252 254	dchrzrhcl	$⊢ ((φ \land U \in ℕ_{0}) \land n \in (0 ..^U \mod N)) \to X (L (n)) \in ℂ$
256	251 255	fsumcl	$⊢ (φ \land U \in ℕ_{0}) \to \sum_{n \in (0 ..^U \mod N)} X (L (n)) \in ℂ$
257	256	addlidd	$⊢ (φ \land U \in ℕ_{0}) \to 0 + \sum_{n \in (0 ..^U \mod N)} X (L (n)) = \sum_{n \in (0 ..^U \mod N)} X (L (n))$
258	49 249 257	3eqtrd	$⊢ (φ \land U \in ℕ_{0}) \to \sum_{n \in (0 ..^U)} X (L (n)) = \sum_{n \in (0 ..^U \mod N)} X (L (n))$
259	258	fveq2d	$⊢ (φ \land U \in ℕ_{0}) \to \|\sum_{n \in (0 ..^U)} X (L (n))\| = \|\sum_{n \in (0 ..^U \mod N)} X (L (n))\|$
260		oveq2	$⊢ u = U \mod N \to (0 ..^u) = (0 ..^U \mod N)$
261	260	sumeq1d	$⊢ u = U \mod N \to \sum_{n \in (0 ..^u)} X (L (n)) = \sum_{n \in (0 ..^U \mod N)} X (L (n))$
262	261	fveq2d	$⊢ u = U \mod N \to \|\sum_{n \in (0 ..^u)} X (L (n))\| = \|\sum_{n \in (0 ..^U \mod N)} X (L (n))\|$
263	262	breq1d	$⊢ u = U \mod N \to (\|\sum_{n \in (0 ..^u)} X (L (n))\| \leq R \leftrightarrow \|\sum_{n \in (0 ..^U \mod N)} X (L (n))\| \leq R)$
264	16	adantr	$⊢ (φ \land U \in ℕ_{0}) \to \forall u \in (0 ..^N) \|\sum_{n \in (0 ..^u)} X (L (n))\| \leq R$
265		zmodfzo	$⊢ (U \in ℤ \land N \in ℕ) \to U \mod N \in (0 ..^N)$
266	230 3 265	syl2anr	$⊢ (φ \land U \in ℕ_{0}) \to U \mod N \in (0 ..^N)$
267	263 264 266	rspcdva	$⊢ (φ \land U \in ℕ_{0}) \to \|\sum_{n \in (0 ..^U \mod N)} X (L (n))\| \leq R$
268	259 267	eqbrtrd	$⊢ (φ \land U \in ℕ_{0}) \to \|\sum_{n \in (0 ..^U)} X (L (n))\| \leq R$

Metamath Proof Explorer

Theorem dchrisumlem1

Proof