dchrisumlem2

	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$
	dchrisumlem2.1	$⊢ φ \to U \in ℝ^{+}$
	dchrisumlem2.2	$⊢ φ \to M \leq U$
	dchrisumlem2.3	$⊢ φ \to U \leq I + 1$
	dchrisumlem2.4	$⊢ φ \to I \in ℕ$
	dchrisumlem2.5	$⊢ φ \to J \in ℤ_{\geq I}$
Assertion	dchrisumlem2	$⊢ φ \to \|seq 1 (+ F) (J) - seq 1 (+ F) (I)\| \leq 2 R ⦋ U / n ⦌ A$

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		dchrisumlem2.1	$⊢ φ \to U \in ℝ^{+}$
18		dchrisumlem2.2	$⊢ φ \to M \leq U$
19		dchrisumlem2.3	$⊢ φ \to U \leq I + 1$
20		dchrisumlem2.4	$⊢ φ \to I \in ℕ$
21		dchrisumlem2.5	$⊢ φ \to J \in ℤ_{\geq I}$
22		fzodisj	$⊢ (1 ..^I + 1) \cap (I + 1 ..^J + 1) = \emptyset$
23	22	a1i	$⊢ φ \to (1 ..^I + 1) \cap (I + 1 ..^J + 1) = \emptyset$
24	20	peano2nnd	$⊢ φ \to I + 1 \in ℕ$
25		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
26	24 25	eleqtrdi	$⊢ φ \to I + 1 \in ℤ_{\geq 1}$
27		eluzp1p1	$⊢ J \in ℤ_{\geq I} \to J + 1 \in ℤ_{\geq (I + 1)}$
28	21 27	syl	$⊢ φ \to J + 1 \in ℤ_{\geq (I + 1)}$
29		elfzuzb	$⊢ I + 1 \in (1 \dots J + 1) \leftrightarrow (I + 1 \in ℤ_{\geq 1} \land J + 1 \in ℤ_{\geq (I + 1)})$
30	26 28 29	sylanbrc	$⊢ φ \to I + 1 \in (1 \dots J + 1)$
31		fzosplit	$⊢ I + 1 \in (1 \dots J + 1) \to (1 ..^J + 1) = (1 ..^I + 1) \cup (I + 1 ..^J + 1)$
32	30 31	syl	$⊢ φ \to (1 ..^J + 1) = (1 ..^I + 1) \cup (I + 1 ..^J + 1)$
33		fzofi	$⊢ (1 ..^J + 1) \in Fin$
34	33	a1i	$⊢ φ \to (1 ..^J + 1) \in Fin$
35		elfzouz	$⊢ i \in (1 ..^J + 1) \to i \in ℤ_{\geq 1}$
36	35 25	eleqtrrdi	$⊢ i \in (1 ..^J + 1) \to i \in ℕ$
37	7	adantr	$⊢ (φ \land i \in ℕ) \to X \in D$
38		nnz	$⊢ i \in ℕ \to i \in ℤ$
39	38	adantl	$⊢ (φ \land i \in ℕ) \to i \in ℤ$
40	4 1 5 2 37 39	dchrzrhcl	$⊢ (φ \land i \in ℕ) \to X (L (i)) \in ℂ$
41	1 2 3 4 5 6 7 8 9 10 11 12 13 14	dchrisumlema	$⊢ φ \to ((i \in ℝ^{+} \to ⦋ i / n ⦌ A \in ℝ) \land (i \in [M, +∞) \to 0 \leq ⦋ i / n ⦌ A))$
42	41	simpld	$⊢ φ \to (i \in ℝ^{+} \to ⦋ i / n ⦌ A \in ℝ)$
43		nnrp	$⊢ i \in ℕ \to i \in ℝ^{+}$
44	42 43	impel	$⊢ (φ \land i \in ℕ) \to ⦋ i / n ⦌ A \in ℝ$
45	44	recnd	$⊢ (φ \land i \in ℕ) \to ⦋ i / n ⦌ A \in ℂ$
46	40 45	mulcld	$⊢ (φ \land i \in ℕ) \to X (L (i)) ⦋ i / n ⦌ A \in ℂ$
47	36 46	sylan2	$⊢ (φ \land i \in (1 ..^J + 1)) \to X (L (i)) ⦋ i / n ⦌ A \in ℂ$
48	23 32 34 47	fsumsplit	$⊢ φ \to \sum_{i \in (1 ..^J + 1)} X (L (i)) ⦋ i / n ⦌ A = \sum_{i \in (1 ..^I + 1)} X (L (i)) ⦋ i / n ⦌ A + \sum_{i \in (I + 1 ..^J + 1)} X (L (i)) ⦋ i / n ⦌ A$
49		eluzelz	$⊢ J \in ℤ_{\geq I} \to J \in ℤ$
50		fzval3	$⊢ J \in ℤ \to (1 \dots J) = (1 ..^J + 1)$
51	21 49 50	3syl	$⊢ φ \to (1 \dots J) = (1 ..^J + 1)$
52	51	sumeq1d	$⊢ φ \to \sum_{i = 1}^{J} X (L (i)) ⦋ i / n ⦌ A = \sum_{i \in (1 ..^J + 1)} X (L (i)) ⦋ i / n ⦌ A$
53	20	nnzd	$⊢ φ \to I \in ℤ$
54		fzval3	$⊢ I \in ℤ \to (1 \dots I) = (1 ..^I + 1)$
55	53 54	syl	$⊢ φ \to (1 \dots I) = (1 ..^I + 1)$
56	55	sumeq1d	$⊢ φ \to \sum_{i = 1}^{I} X (L (i)) ⦋ i / n ⦌ A = \sum_{i \in (1 ..^I + 1)} X (L (i)) ⦋ i / n ⦌ A$
57	56	oveq1d	$⊢ φ \to \sum_{i = 1}^{I} X (L (i)) ⦋ i / n ⦌ A + \sum_{i \in (I + 1 ..^J + 1)} X (L (i)) ⦋ i / n ⦌ A = \sum_{i \in (1 ..^I + 1)} X (L (i)) ⦋ i / n ⦌ A + \sum_{i \in (I + 1 ..^J + 1)} X (L (i)) ⦋ i / n ⦌ A$
58	48 52 57	3eqtr4d	$⊢ φ \to \sum_{i = 1}^{J} X (L (i)) ⦋ i / n ⦌ A = \sum_{i = 1}^{I} X (L (i)) ⦋ i / n ⦌ A + \sum_{i \in (I + 1 ..^J + 1)} X (L (i)) ⦋ i / n ⦌ A$
59		elfznn	$⊢ i \in (1 \dots J) \to i \in ℕ$
60		simpr	$⊢ (φ \land i \in ℕ) \to i \in ℕ$
61		nfcv	$⊢ \underline{Ⅎ} n i$
62		nfcv	$⊢ \underline{Ⅎ} n X (L (i))$
63		nfcv	$⊢ \underline{Ⅎ} n \times$
64		nfcsb1v	$⊢ \underline{Ⅎ} n ⦋ i / n ⦌ A$
65	62 63 64	nfov	$⊢ \underline{Ⅎ} n X (L (i)) ⦋ i / n ⦌ A$
66		2fveq3	$⊢ n = i \to X (L (n)) = X (L (i))$
67		csbeq1a	$⊢ n = i \to A = ⦋ i / n ⦌ A$
68	66 67	oveq12d	$⊢ n = i \to X (L (n)) A = X (L (i)) ⦋ i / n ⦌ A$
69	61 65 68 14	fvmptf	$⊢ (i \in ℕ \land X (L (i)) ⦋ i / n ⦌ A \in ℂ) \to F (i) = X (L (i)) ⦋ i / n ⦌ A$
70	60 46 69	syl2anc	$⊢ (φ \land i \in ℕ) \to F (i) = X (L (i)) ⦋ i / n ⦌ A$
71	59 70	sylan2	$⊢ (φ \land i \in (1 \dots J)) \to F (i) = X (L (i)) ⦋ i / n ⦌ A$
72	20 25	eleqtrdi	$⊢ φ \to I \in ℤ_{\geq 1}$
73		uztrn	$⊢ (J \in ℤ_{\geq I} \land I \in ℤ_{\geq 1}) \to J \in ℤ_{\geq 1}$
74	21 72 73	syl2anc	$⊢ φ \to J \in ℤ_{\geq 1}$
75	59 46	sylan2	$⊢ (φ \land i \in (1 \dots J)) \to X (L (i)) ⦋ i / n ⦌ A \in ℂ$
76	71 74 75	fsumser	$⊢ φ \to \sum_{i = 1}^{J} X (L (i)) ⦋ i / n ⦌ A = seq 1 (+ F) (J)$
77	58 76	eqtr3d	$⊢ φ \to \sum_{i = 1}^{I} X (L (i)) ⦋ i / n ⦌ A + \sum_{i \in (I + 1 ..^J + 1)} X (L (i)) ⦋ i / n ⦌ A = seq 1 (+ F) (J)$
78		elfznn	$⊢ i \in (1 \dots I) \to i \in ℕ$
79	78 70	sylan2	$⊢ (φ \land i \in (1 \dots I)) \to F (i) = X (L (i)) ⦋ i / n ⦌ A$
80	78 46	sylan2	$⊢ (φ \land i \in (1 \dots I)) \to X (L (i)) ⦋ i / n ⦌ A \in ℂ$
81	79 72 80	fsumser	$⊢ φ \to \sum_{i = 1}^{I} X (L (i)) ⦋ i / n ⦌ A = seq 1 (+ F) (I)$
82	77 81	oveq12d	$⊢ φ \to \sum_{i = 1}^{I} X (L (i)) ⦋ i / n ⦌ A + \sum_{i \in (I + 1 ..^J + 1)} X (L (i)) ⦋ i / n ⦌ A - \sum_{i = 1}^{I} X (L (i)) ⦋ i / n ⦌ A = seq 1 (+ F) (J) - seq 1 (+ F) (I)$
83		fzfid	$⊢ φ \to (1 \dots I) \in Fin$
84	83 80	fsumcl	$⊢ φ \to \sum_{i = 1}^{I} X (L (i)) ⦋ i / n ⦌ A \in ℂ$
85		fzofi	$⊢ (I + 1 ..^J + 1) \in Fin$
86	85	a1i	$⊢ φ \to (I + 1 ..^J + 1) \in Fin$
87		ssun2	$⊢ (I + 1 ..^J + 1) \subseteq (1 ..^I + 1) \cup (I + 1 ..^J + 1)$
88	87 32	sseqtrrid	$⊢ φ \to (I + 1 ..^J + 1) \subseteq (1 ..^J + 1)$
89	88	sselda	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to i \in (1 ..^J + 1)$
90	89 47	syldan	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to X (L (i)) ⦋ i / n ⦌ A \in ℂ$
91	86 90	fsumcl	$⊢ φ \to \sum_{i \in (I + 1 ..^J + 1)} X (L (i)) ⦋ i / n ⦌ A \in ℂ$
92	84 91	pncan2d	$⊢ φ \to \sum_{i = 1}^{I} X (L (i)) ⦋ i / n ⦌ A + \sum_{i \in (I + 1 ..^J + 1)} X (L (i)) ⦋ i / n ⦌ A - \sum_{i = 1}^{I} X (L (i)) ⦋ i / n ⦌ A = \sum_{i \in (I + 1 ..^J + 1)} X (L (i)) ⦋ i / n ⦌ A$
93	82 92	eqtr3d	$⊢ φ \to seq 1 (+ F) (J) - seq 1 (+ F) (I) = \sum_{i \in (I + 1 ..^J + 1)} X (L (i)) ⦋ i / n ⦌ A$
94	93	fveq2d	$⊢ φ \to \|seq 1 (+ F) (J) - seq 1 (+ F) (I)\| = \|\sum_{i \in (I + 1 ..^J + 1)} X (L (i)) ⦋ i / n ⦌ A\|$
95	91	abscld	$⊢ φ \to \|\sum_{i \in (I + 1 ..^J + 1)} X (L (i)) ⦋ i / n ⦌ A\| \in ℝ$
96		2re	$⊢ 2 \in ℝ$
97	96	a1i	$⊢ φ \to 2 \in ℝ$
98	97 15	remulcld	$⊢ φ \to 2 R \in ℝ$
99	44	ralrimiva	$⊢ φ \to \forall i \in ℕ ⦋ i / n ⦌ A \in ℝ$
100		csbeq1	$⊢ i = I + 1 \to ⦋ i / n ⦌ A = ⦋ (I + 1) / n ⦌ A$
101	100	eleq1d	$⊢ i = I + 1 \to (⦋ i / n ⦌ A \in ℝ \leftrightarrow ⦋ (I + 1) / n ⦌ A \in ℝ)$
102	101	rspcv	$⊢ I + 1 \in ℕ \to (\forall i \in ℕ ⦋ i / n ⦌ A \in ℝ \to ⦋ (I + 1) / n ⦌ A \in ℝ)$
103	24 99 102	sylc	$⊢ φ \to ⦋ (I + 1) / n ⦌ A \in ℝ$
104	98 103	remulcld	$⊢ φ \to 2 R ⦋ (I + 1) / n ⦌ A \in ℝ$
105	11	ralrimiva	$⊢ φ \to \forall n \in ℝ^{+} A \in ℝ$
106		nfcsb1v	$⊢ \underline{Ⅎ} n ⦋ U / n ⦌ A$
107	106	nfel1	$⊢ Ⅎ n ⦋ U / n ⦌ A \in ℝ$
108		csbeq1a	$⊢ n = U \to A = ⦋ U / n ⦌ A$
109	108	eleq1d	$⊢ n = U \to (A \in ℝ \leftrightarrow ⦋ U / n ⦌ A \in ℝ)$
110	107 109	rspc	$⊢ U \in ℝ^{+} \to (\forall n \in ℝ^{+} A \in ℝ \to ⦋ U / n ⦌ A \in ℝ)$
111	17 105 110	sylc	$⊢ φ \to ⦋ U / n ⦌ A \in ℝ$
112	98 111	remulcld	$⊢ φ \to 2 R ⦋ U / n ⦌ A \in ℝ$
113	74 25	eleqtrrdi	$⊢ φ \to J \in ℕ$
114	113	peano2nnd	$⊢ φ \to J + 1 \in ℕ$
115	114	nnrpd	$⊢ φ \to J + 1 \in ℝ^{+}$
116	1 2 3 4 5 6 7 8 9 10 11 12 13 14	dchrisumlema	$⊢ φ \to ((J + 1 \in ℝ^{+} \to ⦋ (J + 1) / n ⦌ A \in ℝ) \land (J + 1 \in [M, +∞) \to 0 \leq ⦋ (J + 1) / n ⦌ A))$
117	116	simpld	$⊢ φ \to (J + 1 \in ℝ^{+} \to ⦋ (J + 1) / n ⦌ A \in ℝ)$
118	115 117	mpd	$⊢ φ \to ⦋ (J + 1) / n ⦌ A \in ℝ$
119	118	recnd	$⊢ φ \to ⦋ (J + 1) / n ⦌ A \in ℂ$
120		fzofi	$⊢ (0 ..^J + 1) \in Fin$
121	120	a1i	$⊢ φ \to (0 ..^J + 1) \in Fin$
122		elfzoelz	$⊢ n \in (0 ..^J + 1) \to n \in ℤ$
123	7	adantr	$⊢ (φ \land n \in ℤ) \to X \in D$
124		simpr	$⊢ (φ \land n \in ℤ) \to n \in ℤ$
125	4 1 5 2 123 124	dchrzrhcl	$⊢ (φ \land n \in ℤ) \to X (L (n)) \in ℂ$
126	122 125	sylan2	$⊢ (φ \land n \in (0 ..^J + 1)) \to X (L (n)) \in ℂ$
127	121 126	fsumcl	$⊢ φ \to \sum_{n \in (0 ..^J + 1)} X (L (n)) \in ℂ$
128	119 127	mulcld	$⊢ φ \to ⦋ (J + 1) / n ⦌ A \sum_{n \in (0 ..^J + 1)} X (L (n)) \in ℂ$
129	103	recnd	$⊢ φ \to ⦋ (I + 1) / n ⦌ A \in ℂ$
130		fzofi	$⊢ (0 ..^I + 1) \in Fin$
131	130	a1i	$⊢ φ \to (0 ..^I + 1) \in Fin$
132		elfzoelz	$⊢ n \in (0 ..^I + 1) \to n \in ℤ$
133	132 125	sylan2	$⊢ (φ \land n \in (0 ..^I + 1)) \to X (L (n)) \in ℂ$
134	131 133	fsumcl	$⊢ φ \to \sum_{n \in (0 ..^I + 1)} X (L (n)) \in ℂ$
135	129 134	mulcld	$⊢ φ \to ⦋ (I + 1) / n ⦌ A \sum_{n \in (0 ..^I + 1)} X (L (n)) \in ℂ$
136	128 135	subcld	$⊢ φ \to ⦋ (J + 1) / n ⦌ A \sum_{n \in (0 ..^J + 1)} X (L (n)) - ⦋ (I + 1) / n ⦌ A \sum_{n \in (0 ..^I + 1)} X (L (n)) \in ℂ$
137	136	abscld	$⊢ φ \to \|⦋ (J + 1) / n ⦌ A \sum_{n \in (0 ..^J + 1)} X (L (n)) - ⦋ (I + 1) / n ⦌ A \sum_{n \in (0 ..^I + 1)} X (L (n))\| \in ℝ$
138	89 36	syl	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to i \in ℕ$
139		peano2nn	$⊢ i \in ℕ \to i + 1 \in ℕ$
140	139	nnrpd	$⊢ i \in ℕ \to i + 1 \in ℝ^{+}$
141		nfcsb1v	$⊢ \underline{Ⅎ} n ⦋ (i + 1) / n ⦌ A$
142	141	nfel1	$⊢ Ⅎ n ⦋ (i + 1) / n ⦌ A \in ℝ$
143		csbeq1a	$⊢ n = i + 1 \to A = ⦋ (i + 1) / n ⦌ A$
144	143	eleq1d	$⊢ n = i + 1 \to (A \in ℝ \leftrightarrow ⦋ (i + 1) / n ⦌ A \in ℝ)$
145	142 144	rspc	$⊢ i + 1 \in ℝ^{+} \to (\forall n \in ℝ^{+} A \in ℝ \to ⦋ (i + 1) / n ⦌ A \in ℝ)$
146	145	impcom	$⊢ (\forall n \in ℝ^{+} A \in ℝ \land i + 1 \in ℝ^{+}) \to ⦋ (i + 1) / n ⦌ A \in ℝ$
147	105 140 146	syl2an	$⊢ (φ \land i \in ℕ) \to ⦋ (i + 1) / n ⦌ A \in ℝ$
148	147 44	resubcld	$⊢ (φ \land i \in ℕ) \to ⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A \in ℝ$
149	148	recnd	$⊢ (φ \land i \in ℕ) \to ⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A \in ℂ$
150		fzofi	$⊢ (0 ..^i + 1) \in Fin$
151	150	a1i	$⊢ φ \to (0 ..^i + 1) \in Fin$
152		elfzoelz	$⊢ n \in (0 ..^i + 1) \to n \in ℤ$
153	152 125	sylan2	$⊢ (φ \land n \in (0 ..^i + 1)) \to X (L (n)) \in ℂ$
154	151 153	fsumcl	$⊢ φ \to \sum_{n \in (0 ..^i + 1)} X (L (n)) \in ℂ$
155	154	adantr	$⊢ (φ \land i \in ℕ) \to \sum_{n \in (0 ..^i + 1)} X (L (n)) \in ℂ$
156	149 155	mulcld	$⊢ (φ \land i \in ℕ) \to (⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A) \sum_{n \in (0 ..^i + 1)} X (L (n)) \in ℂ$
157	138 156	syldan	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to (⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A) \sum_{n \in (0 ..^i + 1)} X (L (n)) \in ℂ$
158	86 157	fsumcl	$⊢ φ \to \sum_{i \in (I + 1 ..^J + 1)} (⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A) \sum_{n \in (0 ..^i + 1)} X (L (n)) \in ℂ$
159	158	abscld	$⊢ φ \to \|\sum_{i \in (I + 1 ..^J + 1)} (⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A) \sum_{n \in (0 ..^i + 1)} X (L (n))\| \in ℝ$
160	137 159	readdcld	$⊢ φ \to \|⦋ (J + 1) / n ⦌ A \sum_{n \in (0 ..^J + 1)} X (L (n)) - ⦋ (I + 1) / n ⦌ A \sum_{n \in (0 ..^I + 1)} X (L (n))\| + \|\sum_{i \in (I + 1 ..^J + 1)} (⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A) \sum_{n \in (0 ..^i + 1)} X (L (n))\| \in ℝ$
161	40 45	mulcomd	$⊢ (φ \land i \in ℕ) \to X (L (i)) ⦋ i / n ⦌ A = ⦋ i / n ⦌ A X (L (i))$
162		nnnn0	$⊢ i \in ℕ \to i \in ℕ_{0}$
163	162	adantl	$⊢ (φ \land i \in ℕ) \to i \in ℕ_{0}$
164		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
165	163 164	eleqtrdi	$⊢ (φ \land i \in ℕ) \to i \in ℤ_{\geq 0}$
166		elfzelz	$⊢ n \in (0 \dots i) \to n \in ℤ$
167	125	adantlr	$⊢ ((φ \land i \in ℕ) \land n \in ℤ) \to X (L (n)) \in ℂ$
168	166 167	sylan2	$⊢ ((φ \land i \in ℕ) \land n \in (0 \dots i)) \to X (L (n)) \in ℂ$
169	165 168 66	fzosump1	$⊢ (φ \land i \in ℕ) \to \sum_{n \in (0 ..^i + 1)} X (L (n)) = \sum_{n \in (0 ..^i)} X (L (n)) + X (L (i))$
170	169	oveq1d	$⊢ (φ \land i \in ℕ) \to \sum_{n \in (0 ..^i + 1)} X (L (n)) - \sum_{n \in (0 ..^i)} X (L (n)) = \sum_{n \in (0 ..^i)} X (L (n)) + X (L (i)) - \sum_{n \in (0 ..^i)} X (L (n))$
171		fzofi	$⊢ (0 ..^i) \in Fin$
172	171	a1i	$⊢ (φ \land i \in ℕ) \to (0 ..^i) \in Fin$
173		elfzoelz	$⊢ n \in (0 ..^i) \to n \in ℤ$
174	173 167	sylan2	$⊢ ((φ \land i \in ℕ) \land n \in (0 ..^i)) \to X (L (n)) \in ℂ$
175	172 174	fsumcl	$⊢ (φ \land i \in ℕ) \to \sum_{n \in (0 ..^i)} X (L (n)) \in ℂ$
176	175 40	pncan2d	$⊢ (φ \land i \in ℕ) \to \sum_{n \in (0 ..^i)} X (L (n)) + X (L (i)) - \sum_{n \in (0 ..^i)} X (L (n)) = X (L (i))$
177	170 176	eqtr2d	$⊢ (φ \land i \in ℕ) \to X (L (i)) = \sum_{n \in (0 ..^i + 1)} X (L (n)) - \sum_{n \in (0 ..^i)} X (L (n))$
178	177	oveq2d	$⊢ (φ \land i \in ℕ) \to ⦋ i / n ⦌ A X (L (i)) = ⦋ i / n ⦌ A (\sum_{n \in (0 ..^i + 1)} X (L (n)) - \sum_{n \in (0 ..^i)} X (L (n)))$
179	161 178	eqtrd	$⊢ (φ \land i \in ℕ) \to X (L (i)) ⦋ i / n ⦌ A = ⦋ i / n ⦌ A (\sum_{n \in (0 ..^i + 1)} X (L (n)) - \sum_{n \in (0 ..^i)} X (L (n)))$
180	138 179	syldan	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to X (L (i)) ⦋ i / n ⦌ A = ⦋ i / n ⦌ A (\sum_{n \in (0 ..^i + 1)} X (L (n)) - \sum_{n \in (0 ..^i)} X (L (n)))$
181	180	sumeq2dv	$⊢ φ \to \sum_{i \in (I + 1 ..^J + 1)} X (L (i)) ⦋ i / n ⦌ A = \sum_{i \in (I + 1 ..^J + 1)} ⦋ i / n ⦌ A (\sum_{n \in (0 ..^i + 1)} X (L (n)) - \sum_{n \in (0 ..^i)} X (L (n)))$
182		csbeq1	$⊢ k = i \to ⦋ k / n ⦌ A = ⦋ i / n ⦌ A$
183		oveq2	$⊢ k = i \to (0 ..^k) = (0 ..^i)$
184	183	sumeq1d	$⊢ k = i \to \sum_{n \in (0 ..^k)} X (L (n)) = \sum_{n \in (0 ..^i)} X (L (n))$
185	182 184	jca	$⊢ k = i \to (⦋ k / n ⦌ A = ⦋ i / n ⦌ A \land \sum_{n \in (0 ..^k)} X (L (n)) = \sum_{n \in (0 ..^i)} X (L (n)))$
186		csbeq1	$⊢ k = i + 1 \to ⦋ k / n ⦌ A = ⦋ (i + 1) / n ⦌ A$
187		oveq2	$⊢ k = i + 1 \to (0 ..^k) = (0 ..^i + 1)$
188	187	sumeq1d	$⊢ k = i + 1 \to \sum_{n \in (0 ..^k)} X (L (n)) = \sum_{n \in (0 ..^i + 1)} X (L (n))$
189	186 188	jca	$⊢ k = i + 1 \to (⦋ k / n ⦌ A = ⦋ (i + 1) / n ⦌ A \land \sum_{n \in (0 ..^k)} X (L (n)) = \sum_{n \in (0 ..^i + 1)} X (L (n)))$
190		csbeq1	$⊢ k = I + 1 \to ⦋ k / n ⦌ A = ⦋ (I + 1) / n ⦌ A$
191		oveq2	$⊢ k = I + 1 \to (0 ..^k) = (0 ..^I + 1)$
192	191	sumeq1d	$⊢ k = I + 1 \to \sum_{n \in (0 ..^k)} X (L (n)) = \sum_{n \in (0 ..^I + 1)} X (L (n))$
193	190 192	jca	$⊢ k = I + 1 \to (⦋ k / n ⦌ A = ⦋ (I + 1) / n ⦌ A \land \sum_{n \in (0 ..^k)} X (L (n)) = \sum_{n \in (0 ..^I + 1)} X (L (n)))$
194		csbeq1	$⊢ k = J + 1 \to ⦋ k / n ⦌ A = ⦋ (J + 1) / n ⦌ A$
195		oveq2	$⊢ k = J + 1 \to (0 ..^k) = (0 ..^J + 1)$
196	195	sumeq1d	$⊢ k = J + 1 \to \sum_{n \in (0 ..^k)} X (L (n)) = \sum_{n \in (0 ..^J + 1)} X (L (n))$
197	194 196	jca	$⊢ k = J + 1 \to (⦋ k / n ⦌ A = ⦋ (J + 1) / n ⦌ A \land \sum_{n \in (0 ..^k)} X (L (n)) = \sum_{n \in (0 ..^J + 1)} X (L (n)))$
198	45	ralrimiva	$⊢ φ \to \forall i \in ℕ ⦋ i / n ⦌ A \in ℂ$
199		elfzuz	$⊢ k \in (I + 1 \dots J + 1) \to k \in ℤ_{\geq (I + 1)}$
200		eluznn	$⊢ (I + 1 \in ℕ \land k \in ℤ_{\geq (I + 1)}) \to k \in ℕ$
201	24 199 200	syl2an	$⊢ (φ \land k \in (I + 1 \dots J + 1)) \to k \in ℕ$
202		csbeq1	$⊢ i = k \to ⦋ i / n ⦌ A = ⦋ k / n ⦌ A$
203	202	eleq1d	$⊢ i = k \to (⦋ i / n ⦌ A \in ℂ \leftrightarrow ⦋ k / n ⦌ A \in ℂ)$
204	203	rspccva	$⊢ (\forall i \in ℕ ⦋ i / n ⦌ A \in ℂ \land k \in ℕ) \to ⦋ k / n ⦌ A \in ℂ$
205	198 201 204	syl2an2r	$⊢ (φ \land k \in (I + 1 \dots J + 1)) \to ⦋ k / n ⦌ A \in ℂ$
206		fzofi	$⊢ (0 ..^k) \in Fin$
207	206	a1i	$⊢ φ \to (0 ..^k) \in Fin$
208		elfzoelz	$⊢ n \in (0 ..^k) \to n \in ℤ$
209	208 125	sylan2	$⊢ (φ \land n \in (0 ..^k)) \to X (L (n)) \in ℂ$
210	207 209	fsumcl	$⊢ φ \to \sum_{n \in (0 ..^k)} X (L (n)) \in ℂ$
211	210	adantr	$⊢ (φ \land k \in (I + 1 \dots J + 1)) \to \sum_{n \in (0 ..^k)} X (L (n)) \in ℂ$
212	185 189 193 197 28 205 211	fsumparts	$⊢ φ \to \sum_{i \in (I + 1 ..^J + 1)} ⦋ i / n ⦌ A (\sum_{n \in (0 ..^i + 1)} X (L (n)) - \sum_{n \in (0 ..^i)} X (L (n))) = ⦋ (J + 1) / n ⦌ A \sum_{n \in (0 ..^J + 1)} X (L (n)) - ⦋ (I + 1) / n ⦌ A \sum_{n \in (0 ..^I + 1)} X (L (n)) - \sum_{i \in (I + 1 ..^J + 1)} (⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A) \sum_{n \in (0 ..^i + 1)} X (L (n))$
213	181 212	eqtrd	$⊢ φ \to \sum_{i \in (I + 1 ..^J + 1)} X (L (i)) ⦋ i / n ⦌ A = ⦋ (J + 1) / n ⦌ A \sum_{n \in (0 ..^J + 1)} X (L (n)) - ⦋ (I + 1) / n ⦌ A \sum_{n \in (0 ..^I + 1)} X (L (n)) - \sum_{i \in (I + 1 ..^J + 1)} (⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A) \sum_{n \in (0 ..^i + 1)} X (L (n))$
214	213	fveq2d	$⊢ φ \to \|\sum_{i \in (I + 1 ..^J + 1)} X (L (i)) ⦋ i / n ⦌ A\| = \|⦋ (J + 1) / n ⦌ A \sum_{n \in (0 ..^J + 1)} X (L (n)) - ⦋ (I + 1) / n ⦌ A \sum_{n \in (0 ..^I + 1)} X (L (n)) - \sum_{i \in (I + 1 ..^J + 1)} (⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A) \sum_{n \in (0 ..^i + 1)} X (L (n))\|$
215	136 158	abs2dif2d	$⊢ φ \to \|⦋ (J + 1) / n ⦌ A \sum_{n \in (0 ..^J + 1)} X (L (n)) - ⦋ (I + 1) / n ⦌ A \sum_{n \in (0 ..^I + 1)} X (L (n)) - \sum_{i \in (I + 1 ..^J + 1)} (⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A) \sum_{n \in (0 ..^i + 1)} X (L (n))\| \leq \|⦋ (J + 1) / n ⦌ A \sum_{n \in (0 ..^J + 1)} X (L (n)) - ⦋ (I + 1) / n ⦌ A \sum_{n \in (0 ..^I + 1)} X (L (n))\| + \|\sum_{i \in (I + 1 ..^J + 1)} (⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A) \sum_{n \in (0 ..^i + 1)} X (L (n))\|$
216	214 215	eqbrtrd	$⊢ φ \to \|\sum_{i \in (I + 1 ..^J + 1)} X (L (i)) ⦋ i / n ⦌ A\| \leq \|⦋ (J + 1) / n ⦌ A \sum_{n \in (0 ..^J + 1)} X (L (n)) - ⦋ (I + 1) / n ⦌ A \sum_{n \in (0 ..^I + 1)} X (L (n))\| + \|\sum_{i \in (I + 1 ..^J + 1)} (⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A) \sum_{n \in (0 ..^i + 1)} X (L (n))\|$
217	118 103	readdcld	$⊢ φ \to ⦋ (J + 1) / n ⦌ A + ⦋ (I + 1) / n ⦌ A \in ℝ$
218	217 15	remulcld	$⊢ φ \to (⦋ (J + 1) / n ⦌ A + ⦋ (I + 1) / n ⦌ A) R \in ℝ$
219	182 186 190 194 28 205	telfsumo	$⊢ φ \to \sum_{i \in (I + 1 ..^J + 1)} (⦋ i / n ⦌ A - ⦋ (i + 1) / n ⦌ A) = ⦋ (I + 1) / n ⦌ A - ⦋ (J + 1) / n ⦌ A$
220	138 44	syldan	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to ⦋ i / n ⦌ A \in ℝ$
221	138 147	syldan	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to ⦋ (i + 1) / n ⦌ A \in ℝ$
222	220 221	resubcld	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to ⦋ i / n ⦌ A - ⦋ (i + 1) / n ⦌ A \in ℝ$
223	86 222	fsumrecl	$⊢ φ \to \sum_{i \in (I + 1 ..^J + 1)} (⦋ i / n ⦌ A - ⦋ (i + 1) / n ⦌ A) \in ℝ$
224	219 223	eqeltrrd	$⊢ φ \to ⦋ (I + 1) / n ⦌ A - ⦋ (J + 1) / n ⦌ A \in ℝ$
225	224 15	remulcld	$⊢ φ \to (⦋ (I + 1) / n ⦌ A - ⦋ (J + 1) / n ⦌ A) R \in ℝ$
226	128	abscld	$⊢ φ \to \|⦋ (J + 1) / n ⦌ A \sum_{n \in (0 ..^J + 1)} X (L (n))\| \in ℝ$
227	135	abscld	$⊢ φ \to \|⦋ (I + 1) / n ⦌ A \sum_{n \in (0 ..^I + 1)} X (L (n))\| \in ℝ$
228	226 227	readdcld	$⊢ φ \to \|⦋ (J + 1) / n ⦌ A \sum_{n \in (0 ..^J + 1)} X (L (n))\| + \|⦋ (I + 1) / n ⦌ A \sum_{n \in (0 ..^I + 1)} X (L (n))\| \in ℝ$
229	128 135	abs2dif2d	$⊢ φ \to \|⦋ (J + 1) / n ⦌ A \sum_{n \in (0 ..^J + 1)} X (L (n)) - ⦋ (I + 1) / n ⦌ A \sum_{n \in (0 ..^I + 1)} X (L (n))\| \leq \|⦋ (J + 1) / n ⦌ A \sum_{n \in (0 ..^J + 1)} X (L (n))\| + \|⦋ (I + 1) / n ⦌ A \sum_{n \in (0 ..^I + 1)} X (L (n))\|$
230	118 15	remulcld	$⊢ φ \to ⦋ (J + 1) / n ⦌ A R \in ℝ$
231	103 15	remulcld	$⊢ φ \to ⦋ (I + 1) / n ⦌ A R \in ℝ$
232	119 127	absmuld	$⊢ φ \to \|⦋ (J + 1) / n ⦌ A \sum_{n \in (0 ..^J + 1)} X (L (n))\| = \|⦋ (J + 1) / n ⦌ A\| \|\sum_{n \in (0 ..^J + 1)} X (L (n))\|$
233		eluzelre	$⊢ i \in ℤ_{\geq M} \to i \in ℝ$
234	233	adantl	$⊢ (φ \land i \in ℤ_{\geq M}) \to i \in ℝ$
235		eluzle	$⊢ i \in ℤ_{\geq M} \to M \leq i$
236	235	adantl	$⊢ (φ \land i \in ℤ_{\geq M}) \to M \leq i$
237	10	nnred	$⊢ φ \to M \in ℝ$
238	237	adantr	$⊢ (φ \land i \in ℤ_{\geq M}) \to M \in ℝ$
239		elicopnf	$⊢ M \in ℝ \to (i \in [M, +∞) \leftrightarrow (i \in ℝ \land M \leq i))$
240	238 239	syl	$⊢ (φ \land i \in ℤ_{\geq M}) \to (i \in [M, +∞) \leftrightarrow (i \in ℝ \land M \leq i))$
241	234 236 240	mpbir2and	$⊢ (φ \land i \in ℤ_{\geq M}) \to i \in [M, +∞)$
242	241	ex	$⊢ φ \to (i \in ℤ_{\geq M} \to i \in [M, +∞))$
243	242	ssrdv	$⊢ φ \to ℤ_{\geq M} \subseteq [M, +∞)$
244	10	nnzd	$⊢ φ \to M \in ℤ$
245	53	peano2zd	$⊢ φ \to I + 1 \in ℤ$
246	17	rpred	$⊢ φ \to U \in ℝ$
247	24	nnred	$⊢ φ \to I + 1 \in ℝ$
248	237 246 247 18 19	letrd	$⊢ φ \to M \leq I + 1$
249		eluz2	$⊢ I + 1 \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land I + 1 \in ℤ \land M \leq I + 1)$
250	244 245 248 249	syl3anbrc	$⊢ φ \to I + 1 \in ℤ_{\geq M}$
251		uztrn	$⊢ (J + 1 \in ℤ_{\geq (I + 1)} \land I + 1 \in ℤ_{\geq M}) \to J + 1 \in ℤ_{\geq M}$
252	28 250 251	syl2anc	$⊢ φ \to J + 1 \in ℤ_{\geq M}$
253	243 252	sseldd	$⊢ φ \to J + 1 \in [M, +∞)$
254	116	simprd	$⊢ φ \to (J + 1 \in [M, +∞) \to 0 \leq ⦋ (J + 1) / n ⦌ A)$
255	253 254	mpd	$⊢ φ \to 0 \leq ⦋ (J + 1) / n ⦌ A$
256	118 255	absidd	$⊢ φ \to \|⦋ (J + 1) / n ⦌ A\| = ⦋ (J + 1) / n ⦌ A$
257	256	oveq1d	$⊢ φ \to \|⦋ (J + 1) / n ⦌ A\| \|\sum_{n \in (0 ..^J + 1)} X (L (n))\| = ⦋ (J + 1) / n ⦌ A \|\sum_{n \in (0 ..^J + 1)} X (L (n))\|$
258	232 257	eqtrd	$⊢ φ \to \|⦋ (J + 1) / n ⦌ A \sum_{n \in (0 ..^J + 1)} X (L (n))\| = ⦋ (J + 1) / n ⦌ A \|\sum_{n \in (0 ..^J + 1)} X (L (n))\|$
259	127	abscld	$⊢ φ \to \|\sum_{n \in (0 ..^J + 1)} X (L (n))\| \in ℝ$
260	114	nnnn0d	$⊢ φ \to J + 1 \in ℕ_{0}$
261	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	dchrisumlem1	$⊢ (φ \land J + 1 \in ℕ_{0}) \to \|\sum_{n \in (0 ..^J + 1)} X (L (n))\| \leq R$
262	260 261	mpdan	$⊢ φ \to \|\sum_{n \in (0 ..^J + 1)} X (L (n))\| \leq R$
263	259 15 118 255 262	lemul2ad	$⊢ φ \to ⦋ (J + 1) / n ⦌ A \|\sum_{n \in (0 ..^J + 1)} X (L (n))\| \leq ⦋ (J + 1) / n ⦌ A R$
264	258 263	eqbrtrd	$⊢ φ \to \|⦋ (J + 1) / n ⦌ A \sum_{n \in (0 ..^J + 1)} X (L (n))\| \leq ⦋ (J + 1) / n ⦌ A R$
265	129 134	absmuld	$⊢ φ \to \|⦋ (I + 1) / n ⦌ A \sum_{n \in (0 ..^I + 1)} X (L (n))\| = \|⦋ (I + 1) / n ⦌ A\| \|\sum_{n \in (0 ..^I + 1)} X (L (n))\|$
266	243 250	sseldd	$⊢ φ \to I + 1 \in [M, +∞)$
267	1 2 3 4 5 6 7 8 9 10 11 12 13 14	dchrisumlema	$⊢ φ \to ((I + 1 \in ℝ^{+} \to ⦋ (I + 1) / n ⦌ A \in ℝ) \land (I + 1 \in [M, +∞) \to 0 \leq ⦋ (I + 1) / n ⦌ A))$
268	267	simprd	$⊢ φ \to (I + 1 \in [M, +∞) \to 0 \leq ⦋ (I + 1) / n ⦌ A)$
269	266 268	mpd	$⊢ φ \to 0 \leq ⦋ (I + 1) / n ⦌ A$
270	103 269	absidd	$⊢ φ \to \|⦋ (I + 1) / n ⦌ A\| = ⦋ (I + 1) / n ⦌ A$
271	270	oveq1d	$⊢ φ \to \|⦋ (I + 1) / n ⦌ A\| \|\sum_{n \in (0 ..^I + 1)} X (L (n))\| = ⦋ (I + 1) / n ⦌ A \|\sum_{n \in (0 ..^I + 1)} X (L (n))\|$
272	265 271	eqtrd	$⊢ φ \to \|⦋ (I + 1) / n ⦌ A \sum_{n \in (0 ..^I + 1)} X (L (n))\| = ⦋ (I + 1) / n ⦌ A \|\sum_{n \in (0 ..^I + 1)} X (L (n))\|$
273	134	abscld	$⊢ φ \to \|\sum_{n \in (0 ..^I + 1)} X (L (n))\| \in ℝ$
274	24	nnnn0d	$⊢ φ \to I + 1 \in ℕ_{0}$
275	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	dchrisumlem1	$⊢ (φ \land I + 1 \in ℕ_{0}) \to \|\sum_{n \in (0 ..^I + 1)} X (L (n))\| \leq R$
276	274 275	mpdan	$⊢ φ \to \|\sum_{n \in (0 ..^I + 1)} X (L (n))\| \leq R$
277	273 15 103 269 276	lemul2ad	$⊢ φ \to ⦋ (I + 1) / n ⦌ A \|\sum_{n \in (0 ..^I + 1)} X (L (n))\| \leq ⦋ (I + 1) / n ⦌ A R$
278	272 277	eqbrtrd	$⊢ φ \to \|⦋ (I + 1) / n ⦌ A \sum_{n \in (0 ..^I + 1)} X (L (n))\| \leq ⦋ (I + 1) / n ⦌ A R$
279	226 227 230 231 264 278	le2addd	$⊢ φ \to \|⦋ (J + 1) / n ⦌ A \sum_{n \in (0 ..^J + 1)} X (L (n))\| + \|⦋ (I + 1) / n ⦌ A \sum_{n \in (0 ..^I + 1)} X (L (n))\| \leq ⦋ (J + 1) / n ⦌ A R + ⦋ (I + 1) / n ⦌ A R$
280	15	recnd	$⊢ φ \to R \in ℂ$
281	119 129 280	adddird	$⊢ φ \to (⦋ (J + 1) / n ⦌ A + ⦋ (I + 1) / n ⦌ A) R = ⦋ (J + 1) / n ⦌ A R + ⦋ (I + 1) / n ⦌ A R$
282	279 281	breqtrrd	$⊢ φ \to \|⦋ (J + 1) / n ⦌ A \sum_{n \in (0 ..^J + 1)} X (L (n))\| + \|⦋ (I + 1) / n ⦌ A \sum_{n \in (0 ..^I + 1)} X (L (n))\| \leq (⦋ (J + 1) / n ⦌ A + ⦋ (I + 1) / n ⦌ A) R$
283	137 228 218 229 282	letrd	$⊢ φ \to \|⦋ (J + 1) / n ⦌ A \sum_{n \in (0 ..^J + 1)} X (L (n)) - ⦋ (I + 1) / n ⦌ A \sum_{n \in (0 ..^I + 1)} X (L (n))\| \leq (⦋ (J + 1) / n ⦌ A + ⦋ (I + 1) / n ⦌ A) R$
284	157	abscld	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to \|(⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A) \sum_{n \in (0 ..^i + 1)} X (L (n))\| \in ℝ$
285	86 284	fsumrecl	$⊢ φ \to \sum_{i \in (I + 1 ..^J + 1)} \|(⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A) \sum_{n \in (0 ..^i + 1)} X (L (n))\| \in ℝ$
286	86 157	fsumabs	$⊢ φ \to \|\sum_{i \in (I + 1 ..^J + 1)} (⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A) \sum_{n \in (0 ..^i + 1)} X (L (n))\| \leq \sum_{i \in (I + 1 ..^J + 1)} \|(⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A) \sum_{n \in (0 ..^i + 1)} X (L (n))\|$
287	15	adantr	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to R \in ℝ$
288	222 287	remulcld	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to (⦋ i / n ⦌ A - ⦋ (i + 1) / n ⦌ A) R \in ℝ$
289	138 149	syldan	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to ⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A \in ℂ$
290	154	adantr	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to \sum_{n \in (0 ..^i + 1)} X (L (n)) \in ℂ$
291	289 290	absmuld	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to \|(⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A) \sum_{n \in (0 ..^i + 1)} X (L (n))\| = \|⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A\| \|\sum_{n \in (0 ..^i + 1)} X (L (n))\|$
292		elfzouz	$⊢ i \in (I + 1 ..^J + 1) \to i \in ℤ_{\geq (I + 1)}$
293		uztrn	$⊢ (i \in ℤ_{\geq (I + 1)} \land I + 1 \in ℤ_{\geq M}) \to i \in ℤ_{\geq M}$
294	292 250 293	syl2anr	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to i \in ℤ_{\geq M}$
295		eluznn	$⊢ (M \in ℕ \land i \in ℤ_{\geq M}) \to i \in ℕ$
296	10 295	sylan	$⊢ (φ \land i \in ℤ_{\geq M}) \to i \in ℕ$
297	296 140	syl	$⊢ (φ \land i \in ℤ_{\geq M}) \to i + 1 \in ℝ^{+}$
298	296	nnrpd	$⊢ (φ \land i \in ℤ_{\geq M}) \to i \in ℝ^{+}$
299	12	3expia	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+})) \to ((M \leq n \land n \leq x) \to B \leq A)$
300	299	ralrimivva	$⊢ φ \to \forall n \in ℝ^{+} \forall x \in ℝ^{+} ((M \leq n \land n \leq x) \to B \leq A)$
301	300	adantr	$⊢ (φ \land i \in ℤ_{\geq M}) \to \forall n \in ℝ^{+} \forall x \in ℝ^{+} ((M \leq n \land n \leq x) \to B \leq A)$
302		nfcv	$⊢ \underline{Ⅎ} n ℝ^{+}$
303		nfv	$⊢ Ⅎ n (M \leq i \land i \leq x)$
304		nfcv	$⊢ \underline{Ⅎ} n B$
305		nfcv	$⊢ \underline{Ⅎ} n \leq$
306	304 305 64	nfbr	$⊢ Ⅎ n B \leq ⦋ i / n ⦌ A$
307	303 306	nfim	$⊢ Ⅎ n ((M \leq i \land i \leq x) \to B \leq ⦋ i / n ⦌ A)$
308	302 307	nfralw	$⊢ Ⅎ n \forall x \in ℝ^{+} ((M \leq i \land i \leq x) \to B \leq ⦋ i / n ⦌ A)$
309		breq2	$⊢ n = i \to (M \leq n \leftrightarrow M \leq i)$
310		breq1	$⊢ n = i \to (n \leq x \leftrightarrow i \leq x)$
311	309 310	anbi12d	$⊢ n = i \to ((M \leq n \land n \leq x) \leftrightarrow (M \leq i \land i \leq x))$
312	67	breq2d	$⊢ n = i \to (B \leq A \leftrightarrow B \leq ⦋ i / n ⦌ A)$
313	311 312	imbi12d	$⊢ n = i \to (((M \leq n \land n \leq x) \to B \leq A) \leftrightarrow ((M \leq i \land i \leq x) \to B \leq ⦋ i / n ⦌ A))$
314	313	ralbidv	$⊢ n = i \to (\forall x \in ℝ^{+} ((M \leq n \land n \leq x) \to B \leq A) \leftrightarrow \forall x \in ℝ^{+} ((M \leq i \land i \leq x) \to B \leq ⦋ i / n ⦌ A))$
315	308 314	rspc	$⊢ i \in ℝ^{+} \to (\forall n \in ℝ^{+} \forall x \in ℝ^{+} ((M \leq n \land n \leq x) \to B \leq A) \to \forall x \in ℝ^{+} ((M \leq i \land i \leq x) \to B \leq ⦋ i / n ⦌ A))$
316	298 301 315	sylc	$⊢ (φ \land i \in ℤ_{\geq M}) \to \forall x \in ℝ^{+} ((M \leq i \land i \leq x) \to B \leq ⦋ i / n ⦌ A)$
317	234	lep1d	$⊢ (φ \land i \in ℤ_{\geq M}) \to i \leq i + 1$
318	236 317	jca	$⊢ (φ \land i \in ℤ_{\geq M}) \to (M \leq i \land i \leq i + 1)$
319		breq2	$⊢ x = i + 1 \to (i \leq x \leftrightarrow i \leq i + 1)$
320	319	anbi2d	$⊢ x = i + 1 \to ((M \leq i \land i \leq x) \leftrightarrow (M \leq i \land i \leq i + 1))$
321		eqvisset	$⊢ x = i + 1 \to i + 1 \in V$
322		eqtr3	$⊢ (x = i + 1 \land n = i + 1) \to x = n$
323	9	equcoms	$⊢ x = n \to A = B$
324	322 323	syl	$⊢ (x = i + 1 \land n = i + 1) \to A = B$
325	321 324	csbied	$⊢ x = i + 1 \to ⦋ (i + 1) / n ⦌ A = B$
326	325	eqcomd	$⊢ x = i + 1 \to B = ⦋ (i + 1) / n ⦌ A$
327	326	breq1d	$⊢ x = i + 1 \to (B \leq ⦋ i / n ⦌ A \leftrightarrow ⦋ (i + 1) / n ⦌ A \leq ⦋ i / n ⦌ A)$
328	320 327	imbi12d	$⊢ x = i + 1 \to (((M \leq i \land i \leq x) \to B \leq ⦋ i / n ⦌ A) \leftrightarrow ((M \leq i \land i \leq i + 1) \to ⦋ (i + 1) / n ⦌ A \leq ⦋ i / n ⦌ A))$
329	328	rspcv	$⊢ i + 1 \in ℝ^{+} \to (\forall x \in ℝ^{+} ((M \leq i \land i \leq x) \to B \leq ⦋ i / n ⦌ A) \to ((M \leq i \land i \leq i + 1) \to ⦋ (i + 1) / n ⦌ A \leq ⦋ i / n ⦌ A))$
330	297 316 318 329	syl3c	$⊢ (φ \land i \in ℤ_{\geq M}) \to ⦋ (i + 1) / n ⦌ A \leq ⦋ i / n ⦌ A$
331	294 330	syldan	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to ⦋ (i + 1) / n ⦌ A \leq ⦋ i / n ⦌ A$
332	221 220 331	abssuble0d	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to \|⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A\| = ⦋ i / n ⦌ A - ⦋ (i + 1) / n ⦌ A$
333	332	oveq1d	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to \|⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A\| \|\sum_{n \in (0 ..^i + 1)} X (L (n))\| = (⦋ i / n ⦌ A - ⦋ (i + 1) / n ⦌ A) \|\sum_{n \in (0 ..^i + 1)} X (L (n))\|$
334	291 333	eqtrd	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to \|(⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A) \sum_{n \in (0 ..^i + 1)} X (L (n))\| = (⦋ i / n ⦌ A - ⦋ (i + 1) / n ⦌ A) \|\sum_{n \in (0 ..^i + 1)} X (L (n))\|$
335	290	abscld	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to \|\sum_{n \in (0 ..^i + 1)} X (L (n))\| \in ℝ$
336	220 221	subge0d	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to (0 \leq ⦋ i / n ⦌ A - ⦋ (i + 1) / n ⦌ A \leftrightarrow ⦋ (i + 1) / n ⦌ A \leq ⦋ i / n ⦌ A)$
337	331 336	mpbird	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to 0 \leq ⦋ i / n ⦌ A - ⦋ (i + 1) / n ⦌ A$
338	138	peano2nnd	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to i + 1 \in ℕ$
339	338	nnnn0d	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to i + 1 \in ℕ_{0}$
340	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	dchrisumlem1	$⊢ (φ \land i + 1 \in ℕ_{0}) \to \|\sum_{n \in (0 ..^i + 1)} X (L (n))\| \leq R$
341	339 340	syldan	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to \|\sum_{n \in (0 ..^i + 1)} X (L (n))\| \leq R$
342	335 287 222 337 341	lemul2ad	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to (⦋ i / n ⦌ A - ⦋ (i + 1) / n ⦌ A) \|\sum_{n \in (0 ..^i + 1)} X (L (n))\| \leq (⦋ i / n ⦌ A - ⦋ (i + 1) / n ⦌ A) R$
343	334 342	eqbrtrd	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to \|(⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A) \sum_{n \in (0 ..^i + 1)} X (L (n))\| \leq (⦋ i / n ⦌ A - ⦋ (i + 1) / n ⦌ A) R$
344	86 284 288 343	fsumle	$⊢ φ \to \sum_{i \in (I + 1 ..^J + 1)} \|(⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A) \sum_{n \in (0 ..^i + 1)} X (L (n))\| \leq \sum_{i \in (I + 1 ..^J + 1)} (⦋ i / n ⦌ A - ⦋ (i + 1) / n ⦌ A) R$
345	222	recnd	$⊢ (φ \land i \in (I + 1 ..^J + 1)) \to ⦋ i / n ⦌ A - ⦋ (i + 1) / n ⦌ A \in ℂ$
346	86 280 345	fsummulc1	$⊢ φ \to \sum_{i \in (I + 1 ..^J + 1)} (⦋ i / n ⦌ A - ⦋ (i + 1) / n ⦌ A) R = \sum_{i \in (I + 1 ..^J + 1)} (⦋ i / n ⦌ A - ⦋ (i + 1) / n ⦌ A) R$
347	219	oveq1d	$⊢ φ \to \sum_{i \in (I + 1 ..^J + 1)} (⦋ i / n ⦌ A - ⦋ (i + 1) / n ⦌ A) R = (⦋ (I + 1) / n ⦌ A - ⦋ (J + 1) / n ⦌ A) R$
348	346 347	eqtr3d	$⊢ φ \to \sum_{i \in (I + 1 ..^J + 1)} (⦋ i / n ⦌ A - ⦋ (i + 1) / n ⦌ A) R = (⦋ (I + 1) / n ⦌ A - ⦋ (J + 1) / n ⦌ A) R$
349	344 348	breqtrd	$⊢ φ \to \sum_{i \in (I + 1 ..^J + 1)} \|(⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A) \sum_{n \in (0 ..^i + 1)} X (L (n))\| \leq (⦋ (I + 1) / n ⦌ A - ⦋ (J + 1) / n ⦌ A) R$
350	159 285 225 286 349	letrd	$⊢ φ \to \|\sum_{i \in (I + 1 ..^J + 1)} (⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A) \sum_{n \in (0 ..^i + 1)} X (L (n))\| \leq (⦋ (I + 1) / n ⦌ A - ⦋ (J + 1) / n ⦌ A) R$
351	137 159 218 225 283 350	le2addd	$⊢ φ \to \|⦋ (J + 1) / n ⦌ A \sum_{n \in (0 ..^J + 1)} X (L (n)) - ⦋ (I + 1) / n ⦌ A \sum_{n \in (0 ..^I + 1)} X (L (n))\| + \|\sum_{i \in (I + 1 ..^J + 1)} (⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A) \sum_{n \in (0 ..^i + 1)} X (L (n))\| \leq (⦋ (J + 1) / n ⦌ A + ⦋ (I + 1) / n ⦌ A) R + (⦋ (I + 1) / n ⦌ A - ⦋ (J + 1) / n ⦌ A) R$
352	129	2timesd	$⊢ φ \to 2 ⦋ (I + 1) / n ⦌ A = ⦋ (I + 1) / n ⦌ A + ⦋ (I + 1) / n ⦌ A$
353	129 119 129	ppncand	$⊢ φ \to ⦋ (I + 1) / n ⦌ A + ⦋ (J + 1) / n ⦌ A + (⦋ (I + 1) / n ⦌ A - ⦋ (J + 1) / n ⦌ A) = ⦋ (I + 1) / n ⦌ A + ⦋ (I + 1) / n ⦌ A$
354	129 119	addcomd	$⊢ φ \to ⦋ (I + 1) / n ⦌ A + ⦋ (J + 1) / n ⦌ A = ⦋ (J + 1) / n ⦌ A + ⦋ (I + 1) / n ⦌ A$
355	354	oveq1d	$⊢ φ \to ⦋ (I + 1) / n ⦌ A + ⦋ (J + 1) / n ⦌ A + (⦋ (I + 1) / n ⦌ A - ⦋ (J + 1) / n ⦌ A) = ⦋ (J + 1) / n ⦌ A + ⦋ (I + 1) / n ⦌ A + (⦋ (I + 1) / n ⦌ A - ⦋ (J + 1) / n ⦌ A)$
356	352 353 355	3eqtr2d	$⊢ φ \to 2 ⦋ (I + 1) / n ⦌ A = ⦋ (J + 1) / n ⦌ A + ⦋ (I + 1) / n ⦌ A + (⦋ (I + 1) / n ⦌ A - ⦋ (J + 1) / n ⦌ A)$
357	356	oveq1d	$⊢ φ \to 2 ⦋ (I + 1) / n ⦌ A R = (⦋ (J + 1) / n ⦌ A + ⦋ (I + 1) / n ⦌ A + (⦋ (I + 1) / n ⦌ A - ⦋ (J + 1) / n ⦌ A)) R$
358		2cnd	$⊢ φ \to 2 \in ℂ$
359	358 129 280	mul32d	$⊢ φ \to 2 ⦋ (I + 1) / n ⦌ A R = 2 R ⦋ (I + 1) / n ⦌ A$
360	217	recnd	$⊢ φ \to ⦋ (J + 1) / n ⦌ A + ⦋ (I + 1) / n ⦌ A \in ℂ$
361	224	recnd	$⊢ φ \to ⦋ (I + 1) / n ⦌ A - ⦋ (J + 1) / n ⦌ A \in ℂ$
362	360 361 280	adddird	$⊢ φ \to (⦋ (J + 1) / n ⦌ A + ⦋ (I + 1) / n ⦌ A + (⦋ (I + 1) / n ⦌ A - ⦋ (J + 1) / n ⦌ A)) R = (⦋ (J + 1) / n ⦌ A + ⦋ (I + 1) / n ⦌ A) R + (⦋ (I + 1) / n ⦌ A - ⦋ (J + 1) / n ⦌ A) R$
363	357 359 362	3eqtr3d	$⊢ φ \to 2 R ⦋ (I + 1) / n ⦌ A = (⦋ (J + 1) / n ⦌ A + ⦋ (I + 1) / n ⦌ A) R + (⦋ (I + 1) / n ⦌ A - ⦋ (J + 1) / n ⦌ A) R$
364	351 363	breqtrrd	$⊢ φ \to \|⦋ (J + 1) / n ⦌ A \sum_{n \in (0 ..^J + 1)} X (L (n)) - ⦋ (I + 1) / n ⦌ A \sum_{n \in (0 ..^I + 1)} X (L (n))\| + \|\sum_{i \in (I + 1 ..^J + 1)} (⦋ (i + 1) / n ⦌ A - ⦋ i / n ⦌ A) \sum_{n \in (0 ..^i + 1)} X (L (n))\| \leq 2 R ⦋ (I + 1) / n ⦌ A$
365	95 160 104 216 364	letrd	$⊢ φ \to \|\sum_{i \in (I + 1 ..^J + 1)} X (L (i)) ⦋ i / n ⦌ A\| \leq 2 R ⦋ (I + 1) / n ⦌ A$
366		2nn0	$⊢ 2 \in ℕ_{0}$
367		nn0ge0	$⊢ 2 \in ℕ_{0} \to 0 \leq 2$
368	366 367	mp1i	$⊢ φ \to 0 \leq 2$
369		0red	$⊢ φ \to 0 \in ℝ$
370	127	absge0d	$⊢ φ \to 0 \leq \|\sum_{n \in (0 ..^J + 1)} X (L (n))\|$
371	369 259 15 370 262	letrd	$⊢ φ \to 0 \leq R$
372	97 15 368 371	mulge0d	$⊢ φ \to 0 \leq 2 R$
373	24	nnrpd	$⊢ φ \to I + 1 \in ℝ^{+}$
374		nfv	$⊢ Ⅎ n (M \leq U \land U \leq x)$
375	304 305 106	nfbr	$⊢ Ⅎ n B \leq ⦋ U / n ⦌ A$
376	374 375	nfim	$⊢ Ⅎ n ((M \leq U \land U \leq x) \to B \leq ⦋ U / n ⦌ A)$
377	302 376	nfralw	$⊢ Ⅎ n \forall x \in ℝ^{+} ((M \leq U \land U \leq x) \to B \leq ⦋ U / n ⦌ A)$
378		breq2	$⊢ n = U \to (M \leq n \leftrightarrow M \leq U)$
379		breq1	$⊢ n = U \to (n \leq x \leftrightarrow U \leq x)$
380	378 379	anbi12d	$⊢ n = U \to ((M \leq n \land n \leq x) \leftrightarrow (M \leq U \land U \leq x))$
381	108	breq2d	$⊢ n = U \to (B \leq A \leftrightarrow B \leq ⦋ U / n ⦌ A)$
382	380 381	imbi12d	$⊢ n = U \to (((M \leq n \land n \leq x) \to B \leq A) \leftrightarrow ((M \leq U \land U \leq x) \to B \leq ⦋ U / n ⦌ A))$
383	382	ralbidv	$⊢ n = U \to (\forall x \in ℝ^{+} ((M \leq n \land n \leq x) \to B \leq A) \leftrightarrow \forall x \in ℝ^{+} ((M \leq U \land U \leq x) \to B \leq ⦋ U / n ⦌ A))$
384	377 383	rspc	$⊢ U \in ℝ^{+} \to (\forall n \in ℝ^{+} \forall x \in ℝ^{+} ((M \leq n \land n \leq x) \to B \leq A) \to \forall x \in ℝ^{+} ((M \leq U \land U \leq x) \to B \leq ⦋ U / n ⦌ A))$
385	17 300 384	sylc	$⊢ φ \to \forall x \in ℝ^{+} ((M \leq U \land U \leq x) \to B \leq ⦋ U / n ⦌ A)$
386	18 19	jca	$⊢ φ \to (M \leq U \land U \leq I + 1)$
387		breq2	$⊢ x = I + 1 \to (U \leq x \leftrightarrow U \leq I + 1)$
388	387	anbi2d	$⊢ x = I + 1 \to ((M \leq U \land U \leq x) \leftrightarrow (M \leq U \land U \leq I + 1))$
389		eqvisset	$⊢ x = I + 1 \to I + 1 \in V$
390		eqtr3	$⊢ (x = I + 1 \land n = I + 1) \to x = n$
391	390 323	syl	$⊢ (x = I + 1 \land n = I + 1) \to A = B$
392	389 391	csbied	$⊢ x = I + 1 \to ⦋ (I + 1) / n ⦌ A = B$
393	392	eqcomd	$⊢ x = I + 1 \to B = ⦋ (I + 1) / n ⦌ A$
394	393	breq1d	$⊢ x = I + 1 \to (B \leq ⦋ U / n ⦌ A \leftrightarrow ⦋ (I + 1) / n ⦌ A \leq ⦋ U / n ⦌ A)$
395	388 394	imbi12d	$⊢ x = I + 1 \to (((M \leq U \land U \leq x) \to B \leq ⦋ U / n ⦌ A) \leftrightarrow ((M \leq U \land U \leq I + 1) \to ⦋ (I + 1) / n ⦌ A \leq ⦋ U / n ⦌ A))$
396	395	rspcv	$⊢ I + 1 \in ℝ^{+} \to (\forall x \in ℝ^{+} ((M \leq U \land U \leq x) \to B \leq ⦋ U / n ⦌ A) \to ((M \leq U \land U \leq I + 1) \to ⦋ (I + 1) / n ⦌ A \leq ⦋ U / n ⦌ A))$
397	373 385 386 396	syl3c	$⊢ φ \to ⦋ (I + 1) / n ⦌ A \leq ⦋ U / n ⦌ A$
398	103 111 98 372 397	lemul2ad	$⊢ φ \to 2 R ⦋ (I + 1) / n ⦌ A \leq 2 R ⦋ U / n ⦌ A$
399	95 104 112 365 398	letrd	$⊢ φ \to \|\sum_{i \in (I + 1 ..^J + 1)} X (L (i)) ⦋ i / n ⦌ A\| \leq 2 R ⦋ U / n ⦌ A$
400	94 399	eqbrtrd	$⊢ φ \to \|seq 1 (+ F) (J) - seq 1 (+ F) (I)\| \leq 2 R ⦋ U / n ⦌ A$

Metamath Proof Explorer

Theorem dchrisumlem2

Proof