dchrisumlem3

	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	dchrisumlem3	$⊢ φ \to \exists t \exists c \in [0, +∞) (seq 1 (+ F) ⇝ t \land \forall x \in [M, +∞) \|seq 1 (+ F) (⌊x⌋) - t\| \leq c B)$

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		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
18		1zzd	$⊢ φ \to 1 \in ℤ$
19		simpr	$⊢ (φ \land i \in ℕ) \to i \in ℕ$
20	7	adantr	$⊢ (φ \land i \in ℕ) \to X \in D$
21	19	nnzd	$⊢ (φ \land i \in ℕ) \to i \in ℤ$
22	4 1 5 2 20 21	dchrzrhcl	$⊢ (φ \land i \in ℕ) \to X (L (i)) \in ℂ$
23	11	ralrimiva	$⊢ φ \to \forall n \in ℝ^{+} A \in ℝ$
24		nnrp	$⊢ i \in ℕ \to i \in ℝ^{+}$
25		nfcsb1v	$⊢ \underline{Ⅎ} n ⦋ i / n ⦌ A$
26	25	nfel1	$⊢ Ⅎ n ⦋ i / n ⦌ A \in ℝ$
27		csbeq1a	$⊢ n = i \to A = ⦋ i / n ⦌ A$
28	27	eleq1d	$⊢ n = i \to (A \in ℝ \leftrightarrow ⦋ i / n ⦌ A \in ℝ)$
29	26 28	rspc	$⊢ i \in ℝ^{+} \to (\forall n \in ℝ^{+} A \in ℝ \to ⦋ i / n ⦌ A \in ℝ)$
30	29	impcom	$⊢ (\forall n \in ℝ^{+} A \in ℝ \land i \in ℝ^{+}) \to ⦋ i / n ⦌ A \in ℝ$
31	23 24 30	syl2an	$⊢ (φ \land i \in ℕ) \to ⦋ i / n ⦌ A \in ℝ$
32	31	recnd	$⊢ (φ \land i \in ℕ) \to ⦋ i / n ⦌ A \in ℂ$
33	22 32	mulcld	$⊢ (φ \land i \in ℕ) \to X (L (i)) ⦋ i / n ⦌ A \in ℂ$
34		nfcv	$⊢ \underline{Ⅎ} n i$
35		nfcv	$⊢ \underline{Ⅎ} n X (L (i))$
36		nfcv	$⊢ \underline{Ⅎ} n \times$
37	35 36 25	nfov	$⊢ \underline{Ⅎ} n X (L (i)) ⦋ i / n ⦌ A$
38		2fveq3	$⊢ n = i \to X (L (n)) = X (L (i))$
39	38 27	oveq12d	$⊢ n = i \to X (L (n)) A = X (L (i)) ⦋ i / n ⦌ A$
40	34 37 39 14	fvmptf	$⊢ (i \in ℕ \land X (L (i)) ⦋ i / n ⦌ A \in ℂ) \to F (i) = X (L (i)) ⦋ i / n ⦌ A$
41	19 33 40	syl2anc	$⊢ (φ \land i \in ℕ) \to F (i) = X (L (i)) ⦋ i / n ⦌ A$
42	41 33	eqeltrd	$⊢ (φ \land i \in ℕ) \to F (i) \in ℂ$
43	17 18 42	serf	$⊢ φ \to seq 1 (+ F) : ℕ ⟶ ℂ$
44	43	ffvelrnda	$⊢ (φ \land k \in ℕ) \to seq 1 (+ F) (k) \in ℂ$
45	11	recnd	$⊢ (φ \land n \in ℝ^{+}) \to A \in ℂ$
46	45	ralrimiva	$⊢ φ \to \forall n \in ℝ^{+} A \in ℂ$
47	46	adantr	$⊢ (φ \land e \in ℝ^{+}) \to \forall n \in ℝ^{+} A \in ℂ$
48		id	$⊢ e \in ℝ^{+} \to e \in ℝ^{+}$
49		2re	$⊢ 2 \in ℝ$
50		remulcl	$⊢ (2 \in ℝ \land R \in ℝ) \to 2 R \in ℝ$
51	49 15 50	sylancr	$⊢ φ \to 2 R \in ℝ$
52		lbfzo0	$⊢ 0 \in (0 ..^N) \leftrightarrow N \in ℕ$
53	3 52	sylibr	$⊢ φ \to 0 \in (0 ..^N)$
54		oveq2	$⊢ u = 0 \to (0 ..^u) = (0 ..^0)$
55		fzo0	$⊢ (0 ..^0) = \emptyset$
56	54 55	eqtrdi	$⊢ u = 0 \to (0 ..^u) = \emptyset$
57	56	sumeq1d	$⊢ u = 0 \to \sum_{n \in (0 ..^u)} X (L (n)) = \sum_{n \in \emptyset} X (L (n))$
58		sum0	$⊢ \sum_{n \in \emptyset} X (L (n)) = 0$
59	57 58	eqtrdi	$⊢ u = 0 \to \sum_{n \in (0 ..^u)} X (L (n)) = 0$
60	59	abs00bd	$⊢ u = 0 \to \|\sum_{n \in (0 ..^u)} X (L (n))\| = 0$
61	60	breq1d	$⊢ u = 0 \to (\|\sum_{n \in (0 ..^u)} X (L (n))\| \leq R \leftrightarrow 0 \leq R)$
62	61	rspcv	$⊢ 0 \in (0 ..^N) \to (\forall u \in (0 ..^N) \|\sum_{n \in (0 ..^u)} X (L (n))\| \leq R \to 0 \leq R)$
63	53 16 62	sylc	$⊢ φ \to 0 \leq R$
64		0le2	$⊢ 0 \leq 2$
65		mulge0	$⊢ ((2 \in ℝ \land 0 \leq 2) \land (R \in ℝ \land 0 \leq R)) \to 0 \leq 2 R$
66	49 64 65	mpanl12	$⊢ (R \in ℝ \land 0 \leq R) \to 0 \leq 2 R$
67	15 63 66	syl2anc	$⊢ φ \to 0 \leq 2 R$
68	51 67	ge0p1rpd	$⊢ φ \to 2 R + 1 \in ℝ^{+}$
69		rpdivcl	$⊢ (e \in ℝ^{+} \land 2 R + 1 \in ℝ^{+}) \to \frac{e}{2 R + 1} \in ℝ^{+}$
70	48 68 69	syl2anr	$⊢ (φ \land e \in ℝ^{+}) \to \frac{e}{2 R + 1} \in ℝ^{+}$
71	13	adantr	$⊢ (φ \land e \in ℝ^{+}) \to (n \in ℝ^{+} ⟼ A) \underset{ℝ}{⇝} 0$
72	47 70 71	rlimi	$⊢ (φ \land e \in ℝ^{+}) \to \exists m \in ℝ \forall n \in ℝ^{+} (m \leq n \to \|A - 0\| < \frac{e}{2 R + 1})$
73		simpr	$⊢ (φ \land m \in ℝ) \to m \in ℝ$
74	10	nnred	$⊢ φ \to M \in ℝ$
75	74	adantr	$⊢ (φ \land m \in ℝ) \to M \in ℝ$
76	73 75	ifcld	$⊢ (φ \land m \in ℝ) \to if (M \leq m, m, M) \in ℝ$
77		0red	$⊢ (φ \land m \in ℝ) \to 0 \in ℝ$
78	10	nngt0d	$⊢ φ \to 0 < M$
79	78	adantr	$⊢ (φ \land m \in ℝ) \to 0 < M$
80		max1	$⊢ (M \in ℝ \land m \in ℝ) \to M \leq if (M \leq m, m, M)$
81	74 80	sylan	$⊢ (φ \land m \in ℝ) \to M \leq if (M \leq m, m, M)$
82	77 75 76 79 81	ltletrd	$⊢ (φ \land m \in ℝ) \to 0 < if (M \leq m, m, M)$
83	76 82	elrpd	$⊢ (φ \land m \in ℝ) \to if (M \leq m, m, M) \in ℝ^{+}$
84	83	adantlr	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to if (M \leq m, m, M) \in ℝ^{+}$
85		nfv	$⊢ Ⅎ n m \leq if (M \leq m, m, M)$
86		nfcv	$⊢ \underline{Ⅎ} n abs$
87		nfcsb1v	$⊢ \underline{Ⅎ} n ⦋ if (M \leq m, m, M) / n ⦌ A$
88		nfcv	$⊢ \underline{Ⅎ} n -$
89		nfcv	$⊢ \underline{Ⅎ} n 0$
90	87 88 89	nfov	$⊢ \underline{Ⅎ} n (⦋ if (M \leq m, m, M) / n ⦌ A - 0)$
91	86 90	nffv	$⊢ \underline{Ⅎ} n \|⦋ if (M \leq m, m, M) / n ⦌ A - 0\|$
92		nfcv	$⊢ \underline{Ⅎ} n <$
93		nfcv	$⊢ \underline{Ⅎ} n (\frac{e}{2 R + 1})$
94	91 92 93	nfbr	$⊢ Ⅎ n \|⦋ if (M \leq m, m, M) / n ⦌ A - 0\| < \frac{e}{2 R + 1}$
95	85 94	nfim	$⊢ Ⅎ n (m \leq if (M \leq m, m, M) \to \|⦋ if (M \leq m, m, M) / n ⦌ A - 0\| < \frac{e}{2 R + 1})$
96		breq2	$⊢ n = if (M \leq m, m, M) \to (m \leq n \leftrightarrow m \leq if (M \leq m, m, M))$
97		csbeq1a	$⊢ n = if (M \leq m, m, M) \to A = ⦋ if (M \leq m, m, M) / n ⦌ A$
98	97	fvoveq1d	$⊢ n = if (M \leq m, m, M) \to \|A - 0\| = \|⦋ if (M \leq m, m, M) / n ⦌ A - 0\|$
99	98	breq1d	$⊢ n = if (M \leq m, m, M) \to (\|A - 0\| < \frac{e}{2 R + 1} \leftrightarrow \|⦋ if (M \leq m, m, M) / n ⦌ A - 0\| < \frac{e}{2 R + 1})$
100	96 99	imbi12d	$⊢ n = if (M \leq m, m, M) \to ((m \leq n \to \|A - 0\| < \frac{e}{2 R + 1}) \leftrightarrow (m \leq if (M \leq m, m, M) \to \|⦋ if (M \leq m, m, M) / n ⦌ A - 0\| < \frac{e}{2 R + 1}))$
101	95 100	rspc	$⊢ if (M \leq m, m, M) \in ℝ^{+} \to (\forall n \in ℝ^{+} (m \leq n \to \|A - 0\| < \frac{e}{2 R + 1}) \to (m \leq if (M \leq m, m, M) \to \|⦋ if (M \leq m, m, M) / n ⦌ A - 0\| < \frac{e}{2 R + 1}))$
102	84 101	syl	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to (\forall n \in ℝ^{+} (m \leq n \to \|A - 0\| < \frac{e}{2 R + 1}) \to (m \leq if (M \leq m, m, M) \to \|⦋ if (M \leq m, m, M) / n ⦌ A - 0\| < \frac{e}{2 R + 1}))$
103	74	ad2antrr	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to M \in ℝ$
104		max2	$⊢ (M \in ℝ \land m \in ℝ) \to m \leq if (M \leq m, m, M)$
105	103 104	sylancom	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to m \leq if (M \leq m, m, M)$
106	23	ad2antrr	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to \forall n \in ℝ^{+} A \in ℝ$
107	87	nfel1	$⊢ Ⅎ n ⦋ if (M \leq m, m, M) / n ⦌ A \in ℝ$
108	97	eleq1d	$⊢ n = if (M \leq m, m, M) \to (A \in ℝ \leftrightarrow ⦋ if (M \leq m, m, M) / n ⦌ A \in ℝ)$
109	107 108	rspc	$⊢ if (M \leq m, m, M) \in ℝ^{+} \to (\forall n \in ℝ^{+} A \in ℝ \to ⦋ if (M \leq m, m, M) / n ⦌ A \in ℝ)$
110	84 106 109	sylc	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to ⦋ if (M \leq m, m, M) / n ⦌ A \in ℝ$
111	110	recnd	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to ⦋ if (M \leq m, m, M) / n ⦌ A \in ℂ$
112	111	subid1d	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to ⦋ if (M \leq m, m, M) / n ⦌ A - 0 = ⦋ if (M \leq m, m, M) / n ⦌ A$
113	112	fveq2d	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to \|⦋ if (M \leq m, m, M) / n ⦌ A - 0\| = \|⦋ if (M \leq m, m, M) / n ⦌ A\|$
114	76	adantlr	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to if (M \leq m, m, M) \in ℝ$
115	103 80	sylancom	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to M \leq if (M \leq m, m, M)$
116		elicopnf	$⊢ M \in ℝ \to (if (M \leq m, m, M) \in [M, +∞) \leftrightarrow (if (M \leq m, m, M) \in ℝ \land M \leq if (M \leq m, m, M)))$
117	103 116	syl	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to (if (M \leq m, m, M) \in [M, +∞) \leftrightarrow (if (M \leq m, m, M) \in ℝ \land M \leq if (M \leq m, m, M)))$
118	114 115 117	mpbir2and	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to if (M \leq m, m, M) \in [M, +∞)$
119	3	ad2antrr	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to N \in ℕ$
120	7	ad2antrr	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to X \in D$
121	8	ad2antrr	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to X \neq \underset{˙}{1}$
122	10	ad2antrr	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to M \in ℕ$
123	11	ad4ant14	$⊢ (((φ \land e \in ℝ^{+}) \land m \in ℝ) \land n \in ℝ^{+}) \to A \in ℝ$
124		simpll	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to φ$
125	124 12	syl3an1	$⊢ (((φ \land e \in ℝ^{+}) \land m \in ℝ) \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (M \leq n \land n \leq x)) \to B \leq A$
126	13	ad2antrr	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to (n \in ℝ^{+} ⟼ A) \underset{ℝ}{⇝} 0$
127	1 2 119 4 5 6 120 121 9 122 123 125 126 14	dchrisumlema	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to ((if (M \leq m, m, M) \in ℝ^{+} \to ⦋ if (M \leq m, m, M) / n ⦌ A \in ℝ) \land (if (M \leq m, m, M) \in [M, +∞) \to 0 \leq ⦋ if (M \leq m, m, M) / n ⦌ A))$
128	127	simprd	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to (if (M \leq m, m, M) \in [M, +∞) \to 0 \leq ⦋ if (M \leq m, m, M) / n ⦌ A)$
129	118 128	mpd	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to 0 \leq ⦋ if (M \leq m, m, M) / n ⦌ A$
130	110 129	absidd	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to \|⦋ if (M \leq m, m, M) / n ⦌ A\| = ⦋ if (M \leq m, m, M) / n ⦌ A$
131	113 130	eqtrd	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to \|⦋ if (M \leq m, m, M) / n ⦌ A - 0\| = ⦋ if (M \leq m, m, M) / n ⦌ A$
132	131	breq1d	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to (\|⦋ if (M \leq m, m, M) / n ⦌ A - 0\| < \frac{e}{2 R + 1} \leftrightarrow ⦋ if (M \leq m, m, M) / n ⦌ A < \frac{e}{2 R + 1})$
133		rpre	$⊢ e \in ℝ^{+} \to e \in ℝ$
134	133	ad2antlr	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to e \in ℝ$
135	68	ad2antrr	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to 2 R + 1 \in ℝ^{+}$
136	110 134 135	ltmuldiv2d	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to ((2 R + 1) ⦋ if (M \leq m, m, M) / n ⦌ A < e \leftrightarrow ⦋ if (M \leq m, m, M) / n ⦌ A < \frac{e}{2 R + 1})$
137	132 136	bitr4d	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to (\|⦋ if (M \leq m, m, M) / n ⦌ A - 0\| < \frac{e}{2 R + 1} \leftrightarrow (2 R + 1) ⦋ if (M \leq m, m, M) / n ⦌ A < e)$
138	51	ad2antrr	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to 2 R \in ℝ$
139	135	rpred	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to 2 R + 1 \in ℝ$
140	138	lep1d	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to 2 R \leq 2 R + 1$
141	138 139 110 129 140	lemul1ad	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to 2 R ⦋ if (M \leq m, m, M) / n ⦌ A \leq (2 R + 1) ⦋ if (M \leq m, m, M) / n ⦌ A$
142	138 110	remulcld	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to 2 R ⦋ if (M \leq m, m, M) / n ⦌ A \in ℝ$
143	139 110	remulcld	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to (2 R + 1) ⦋ if (M \leq m, m, M) / n ⦌ A \in ℝ$
144		lelttr	$⊢ (2 R ⦋ if (M \leq m, m, M) / n ⦌ A \in ℝ \land (2 R + 1) ⦋ if (M \leq m, m, M) / n ⦌ A \in ℝ \land e \in ℝ) \to ((2 R ⦋ if (M \leq m, m, M) / n ⦌ A \leq (2 R + 1) ⦋ if (M \leq m, m, M) / n ⦌ A \land (2 R + 1) ⦋ if (M \leq m, m, M) / n ⦌ A < e) \to 2 R ⦋ if (M \leq m, m, M) / n ⦌ A < e)$
145	142 143 134 144	syl3anc	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to ((2 R ⦋ if (M \leq m, m, M) / n ⦌ A \leq (2 R + 1) ⦋ if (M \leq m, m, M) / n ⦌ A \land (2 R + 1) ⦋ if (M \leq m, m, M) / n ⦌ A < e) \to 2 R ⦋ if (M \leq m, m, M) / n ⦌ A < e)$
146	141 145	mpand	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to ((2 R + 1) ⦋ if (M \leq m, m, M) / n ⦌ A < e \to 2 R ⦋ if (M \leq m, m, M) / n ⦌ A < e)$
147	137 146	sylbid	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to (\|⦋ if (M \leq m, m, M) / n ⦌ A - 0\| < \frac{e}{2 R + 1} \to 2 R ⦋ if (M \leq m, m, M) / n ⦌ A < e)$
148		1red	$⊢ (φ \land m \in ℝ) \to 1 \in ℝ$
149	10	adantr	$⊢ (φ \land m \in ℝ) \to M \in ℕ$
150	149	nnge1d	$⊢ (φ \land m \in ℝ) \to 1 \leq M$
151	148 75 76 150 81	letrd	$⊢ (φ \land m \in ℝ) \to 1 \leq if (M \leq m, m, M)$
152		flge1nn	$⊢ (if (M \leq m, m, M) \in ℝ \land 1 \leq if (M \leq m, m, M)) \to ⌊if (M \leq m, m, M)⌋ \in ℕ$
153	76 151 152	syl2anc	$⊢ (φ \land m \in ℝ) \to ⌊if (M \leq m, m, M)⌋ \in ℕ$
154	153	adantlr	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to ⌊if (M \leq m, m, M)⌋ \in ℕ$
155	3	ad2antrr	$⊢ ((φ \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to N \in ℕ$
156	7	ad2antrr	$⊢ ((φ \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to X \in D$
157	8	ad2antrr	$⊢ ((φ \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to X \neq \underset{˙}{1}$
158	10	ad2antrr	$⊢ ((φ \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to M \in ℕ$
159	11	ad4ant14	$⊢ (((φ \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \land n \in ℝ^{+}) \to A \in ℝ$
160	12	3adant1r	$⊢ ((φ \land m \in ℝ) \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (M \leq n \land n \leq x)) \to B \leq A$
161	160	3adant1r	$⊢ (((φ \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (M \leq n \land n \leq x)) \to B \leq A$
162	13	ad2antrr	$⊢ ((φ \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to (n \in ℝ^{+} ⟼ A) \underset{ℝ}{⇝} 0$
163	15	ad2antrr	$⊢ ((φ \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to R \in ℝ$
164	16	ad2antrr	$⊢ ((φ \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to \forall u \in (0 ..^N) \|\sum_{n \in (0 ..^u)} X (L (n))\| \leq R$
165	83	adantr	$⊢ ((φ \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to if (M \leq m, m, M) \in ℝ^{+}$
166	81	adantr	$⊢ ((φ \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to M \leq if (M \leq m, m, M)$
167	76	adantr	$⊢ ((φ \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to if (M \leq m, m, M) \in ℝ$
168		fllep1	$⊢ if (M \leq m, m, M) \in ℝ \to if (M \leq m, m, M) \leq ⌊if (M \leq m, m, M)⌋ + 1$
169	167 168	syl	$⊢ ((φ \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to if (M \leq m, m, M) \leq ⌊if (M \leq m, m, M)⌋ + 1$
170	153	adantr	$⊢ ((φ \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to ⌊if (M \leq m, m, M)⌋ \in ℕ$
171		simpr	$⊢ ((φ \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}$
172	1 2 155 4 5 6 156 157 9 158 159 161 162 14 163 164 165 166 169 170 171	dchrisumlem2	$⊢ ((φ \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to \|seq 1 (+ F) (k) - seq 1 (+ F) (⌊if (M \leq m, m, M)⌋)\| \leq 2 R ⦋ if (M \leq m, m, M) / n ⦌ A$
173	172	adantllr	$⊢ (((φ \land e \in ℝ^{+}) \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to \|seq 1 (+ F) (k) - seq 1 (+ F) (⌊if (M \leq m, m, M)⌋)\| \leq 2 R ⦋ if (M \leq m, m, M) / n ⦌ A$
174	43	ad3antrrr	$⊢ (((φ \land e \in ℝ^{+}) \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to seq 1 (+ F) : ℕ ⟶ ℂ$
175		eluznn	$⊢ (⌊if (M \leq m, m, M)⌋ \in ℕ \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to k \in ℕ$
176	154 175	sylan	$⊢ (((φ \land e \in ℝ^{+}) \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to k \in ℕ$
177	174 176	ffvelrnd	$⊢ (((φ \land e \in ℝ^{+}) \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to seq 1 (+ F) (k) \in ℂ$
178	154	adantr	$⊢ (((φ \land e \in ℝ^{+}) \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to ⌊if (M \leq m, m, M)⌋ \in ℕ$
179	174 178	ffvelrnd	$⊢ (((φ \land e \in ℝ^{+}) \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to seq 1 (+ F) (⌊if (M \leq m, m, M)⌋) \in ℂ$
180	177 179	subcld	$⊢ (((φ \land e \in ℝ^{+}) \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to seq 1 (+ F) (k) - seq 1 (+ F) (⌊if (M \leq m, m, M)⌋) \in ℂ$
181	180	abscld	$⊢ (((φ \land e \in ℝ^{+}) \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to \|seq 1 (+ F) (k) - seq 1 (+ F) (⌊if (M \leq m, m, M)⌋)\| \in ℝ$
182	142	adantr	$⊢ (((φ \land e \in ℝ^{+}) \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to 2 R ⦋ if (M \leq m, m, M) / n ⦌ A \in ℝ$
183	134	adantr	$⊢ (((φ \land e \in ℝ^{+}) \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to e \in ℝ$
184		lelttr	$⊢ (\|seq 1 (+ F) (k) - seq 1 (+ F) (⌊if (M \leq m, m, M)⌋)\| \in ℝ \land 2 R ⦋ if (M \leq m, m, M) / n ⦌ A \in ℝ \land e \in ℝ) \to ((\|seq 1 (+ F) (k) - seq 1 (+ F) (⌊if (M \leq m, m, M)⌋)\| \leq 2 R ⦋ if (M \leq m, m, M) / n ⦌ A \land 2 R ⦋ if (M \leq m, m, M) / n ⦌ A < e) \to \|seq 1 (+ F) (k) - seq 1 (+ F) (⌊if (M \leq m, m, M)⌋)\| < e)$
185	181 182 183 184	syl3anc	$⊢ (((φ \land e \in ℝ^{+}) \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to ((\|seq 1 (+ F) (k) - seq 1 (+ F) (⌊if (M \leq m, m, M)⌋)\| \leq 2 R ⦋ if (M \leq m, m, M) / n ⦌ A \land 2 R ⦋ if (M \leq m, m, M) / n ⦌ A < e) \to \|seq 1 (+ F) (k) - seq 1 (+ F) (⌊if (M \leq m, m, M)⌋)\| < e)$
186	173 185	mpand	$⊢ (((φ \land e \in ℝ^{+}) \land m \in ℝ) \land k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋}) \to (2 R ⦋ if (M \leq m, m, M) / n ⦌ A < e \to \|seq 1 (+ F) (k) - seq 1 (+ F) (⌊if (M \leq m, m, M)⌋)\| < e)$
187	186	ralrimdva	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to (2 R ⦋ if (M \leq m, m, M) / n ⦌ A < e \to \forall k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋} \|seq 1 (+ F) (k) - seq 1 (+ F) (⌊if (M \leq m, m, M)⌋)\| < e)$
188		fveq2	$⊢ j = ⌊if (M \leq m, m, M)⌋ \to ℤ_{\geq j} = ℤ_{\geq ⌊if (M \leq m, m, M)⌋}$
189		fveq2	$⊢ j = ⌊if (M \leq m, m, M)⌋ \to seq 1 (+ F) (j) = seq 1 (+ F) (⌊if (M \leq m, m, M)⌋)$
190	189	oveq2d	$⊢ j = ⌊if (M \leq m, m, M)⌋ \to seq 1 (+ F) (k) - seq 1 (+ F) (j) = seq 1 (+ F) (k) - seq 1 (+ F) (⌊if (M \leq m, m, M)⌋)$
191	190	fveq2d	$⊢ j = ⌊if (M \leq m, m, M)⌋ \to \|seq 1 (+ F) (k) - seq 1 (+ F) (j)\| = \|seq 1 (+ F) (k) - seq 1 (+ F) (⌊if (M \leq m, m, M)⌋)\|$
192	191	breq1d	$⊢ j = ⌊if (M \leq m, m, M)⌋ \to (\|seq 1 (+ F) (k) - seq 1 (+ F) (j)\| < e \leftrightarrow \|seq 1 (+ F) (k) - seq 1 (+ F) (⌊if (M \leq m, m, M)⌋)\| < e)$
193	188 192	raleqbidv	$⊢ j = ⌊if (M \leq m, m, M)⌋ \to (\forall k \in ℤ_{\geq j} \|seq 1 (+ F) (k) - seq 1 (+ F) (j)\| < e \leftrightarrow \forall k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋} \|seq 1 (+ F) (k) - seq 1 (+ F) (⌊if (M \leq m, m, M)⌋)\| < e)$
194	193	rspcev	$⊢ (⌊if (M \leq m, m, M)⌋ \in ℕ \land \forall k \in ℤ_{\geq ⌊if (M \leq m, m, M)⌋} \|seq 1 (+ F) (k) - seq 1 (+ F) (⌊if (M \leq m, m, M)⌋)\| < e) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} \|seq 1 (+ F) (k) - seq 1 (+ F) (j)\| < e$
195	154 187 194	syl6an	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to (2 R ⦋ if (M \leq m, m, M) / n ⦌ A < e \to \exists j \in ℕ \forall k \in ℤ_{\geq j} \|seq 1 (+ F) (k) - seq 1 (+ F) (j)\| < e)$
196	147 195	syld	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to (\|⦋ if (M \leq m, m, M) / n ⦌ A - 0\| < \frac{e}{2 R + 1} \to \exists j \in ℕ \forall k \in ℤ_{\geq j} \|seq 1 (+ F) (k) - seq 1 (+ F) (j)\| < e)$
197	105 196	embantd	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to ((m \leq if (M \leq m, m, M) \to \|⦋ if (M \leq m, m, M) / n ⦌ A - 0\| < \frac{e}{2 R + 1}) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} \|seq 1 (+ F) (k) - seq 1 (+ F) (j)\| < e)$
198	102 197	syld	$⊢ ((φ \land e \in ℝ^{+}) \land m \in ℝ) \to (\forall n \in ℝ^{+} (m \leq n \to \|A - 0\| < \frac{e}{2 R + 1}) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} \|seq 1 (+ F) (k) - seq 1 (+ F) (j)\| < e)$
199	198	rexlimdva	$⊢ (φ \land e \in ℝ^{+}) \to (\exists m \in ℝ \forall n \in ℝ^{+} (m \leq n \to \|A - 0\| < \frac{e}{2 R + 1}) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} \|seq 1 (+ F) (k) - seq 1 (+ F) (j)\| < e)$
200	72 199	mpd	$⊢ (φ \land e \in ℝ^{+}) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} \|seq 1 (+ F) (k) - seq 1 (+ F) (j)\| < e$
201	200	ralrimiva	$⊢ φ \to \forall e \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} \|seq 1 (+ F) (k) - seq 1 (+ F) (j)\| < e$
202		seqex	$⊢ seq 1 (+ F) \in V$
203	202	a1i	$⊢ φ \to seq 1 (+ F) \in V$
204	17 44 201 203	caucvg	$⊢ φ \to seq 1 (+ F) \in dom ⇝$
205	202	eldm	$⊢ seq 1 (+ F) \in dom ⇝ \leftrightarrow \exists t seq 1 (+ F) ⇝ t$
206	204 205	sylib	$⊢ φ \to \exists t seq 1 (+ F) ⇝ t$
207		simpr	$⊢ (φ \land seq 1 (+ F) ⇝ t) \to seq 1 (+ F) ⇝ t$
208		elrege0	$⊢ 2 R \in [0, +∞) \leftrightarrow (2 R \in ℝ \land 0 \leq 2 R)$
209	51 67 208	sylanbrc	$⊢ φ \to 2 R \in [0, +∞)$
210	209	adantr	$⊢ (φ \land seq 1 (+ F) ⇝ t) \to 2 R \in [0, +∞)$
211		eqid	$⊢ ℤ_{\geq ⌊m⌋} = ℤ_{\geq ⌊m⌋}$
212		pnfxr	$⊢ +∞ \in ℝ^{*}$
213		icossre	$⊢ (M \in ℝ \land +∞ \in ℝ^{*}) \to [M, +∞) \subseteq ℝ$
214	74 212 213	sylancl	$⊢ φ \to [M, +∞) \subseteq ℝ$
215	214	sselda	$⊢ (φ \land m \in [M, +∞)) \to m \in ℝ$
216	215	adantlr	$⊢ ((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \to m \in ℝ$
217	216	flcld	$⊢ ((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \to ⌊m⌋ \in ℤ$
218		simplr	$⊢ ((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \to seq 1 (+ F) ⇝ t$
219	43	ad2antrr	$⊢ ((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \to seq 1 (+ F) : ℕ ⟶ ℂ$
220		1red	$⊢ ((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \to 1 \in ℝ$
221	74	ad2antrr	$⊢ ((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \to M \in ℝ$
222	10	ad2antrr	$⊢ ((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \to M \in ℕ$
223	222	nnge1d	$⊢ ((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \to 1 \leq M$
224		elicopnf	$⊢ M \in ℝ \to (m \in [M, +∞) \leftrightarrow (m \in ℝ \land M \leq m))$
225	74 224	syl	$⊢ φ \to (m \in [M, +∞) \leftrightarrow (m \in ℝ \land M \leq m))$
226	225	simplbda	$⊢ (φ \land m \in [M, +∞)) \to M \leq m$
227	226	adantlr	$⊢ ((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \to M \leq m$
228	220 221 216 223 227	letrd	$⊢ ((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \to 1 \leq m$
229		flge1nn	$⊢ (m \in ℝ \land 1 \leq m) \to ⌊m⌋ \in ℕ$
230	216 228 229	syl2anc	$⊢ ((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \to ⌊m⌋ \in ℕ$
231	219 230	ffvelrnd	$⊢ ((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \to seq 1 (+ F) (⌊m⌋) \in ℂ$
232		nnex	$⊢ ℕ \in V$
233	232	mptex	$⊢ (k \in ℕ ⟼ seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k)) \in V$
234	233	a1i	$⊢ ((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \to (k \in ℕ ⟼ seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k)) \in V$
235	219	adantr	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to seq 1 (+ F) : ℕ ⟶ ℂ$
236		eluznn	$⊢ (⌊m⌋ \in ℕ \land i \in ℤ_{\geq ⌊m⌋}) \to i \in ℕ$
237	230 236	sylan	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to i \in ℕ$
238	235 237	ffvelrnd	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to seq 1 (+ F) (i) \in ℂ$
239		fveq2	$⊢ k = i \to seq 1 (+ F) (k) = seq 1 (+ F) (i)$
240	239	oveq2d	$⊢ k = i \to seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k) = seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (i)$
241		eqid	$⊢ (k \in ℕ ⟼ seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k)) = (k \in ℕ ⟼ seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k))$
242		ovex	$⊢ seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k) \in V$
243	240 241 242	fvmpt3i	$⊢ i \in ℕ \to (k \in ℕ ⟼ seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k)) (i) = seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (i)$
244	237 243	syl	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to (k \in ℕ ⟼ seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k)) (i) = seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (i)$
245	211 217 218 231 234 238 244	climsubc2	$⊢ ((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \to (k \in ℕ ⟼ seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k)) ⇝ (seq 1 (+ F) (⌊m⌋) - t)$
246	232	mptex	$⊢ (k \in ℕ ⟼ \|seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k)\|) \in V$
247	246	a1i	$⊢ ((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \to (k \in ℕ ⟼ \|seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k)\|) \in V$
248		fvex	$⊢ seq 1 (+ F) (⌊m⌋) \in V$
249	248	fvconst2	$⊢ i \in ℕ \to (ℕ \times \{seq 1 (+ F) (⌊m⌋)\}) (i) = seq 1 (+ F) (⌊m⌋)$
250	237 249	syl	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to (ℕ \times \{seq 1 (+ F) (⌊m⌋)\}) (i) = seq 1 (+ F) (⌊m⌋)$
251	250	oveq1d	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to (ℕ \times \{seq 1 (+ F) (⌊m⌋)\}) (i) - seq 1 (+ F) (i) = seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (i)$
252	244 251	eqtr4d	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to (k \in ℕ ⟼ seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k)) (i) = (ℕ \times \{seq 1 (+ F) (⌊m⌋)\}) (i) - seq 1 (+ F) (i)$
253	231	adantr	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to seq 1 (+ F) (⌊m⌋) \in ℂ$
254	250 253	eqeltrd	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to (ℕ \times \{seq 1 (+ F) (⌊m⌋)\}) (i) \in ℂ$
255	254 238	subcld	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to (ℕ \times \{seq 1 (+ F) (⌊m⌋)\}) (i) - seq 1 (+ F) (i) \in ℂ$
256	252 255	eqeltrd	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to (k \in ℕ ⟼ seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k)) (i) \in ℂ$
257	240	fveq2d	$⊢ k = i \to \|seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k)\| = \|seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (i)\|$
258		eqid	$⊢ (k \in ℕ ⟼ \|seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k)\|) = (k \in ℕ ⟼ \|seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k)\|)$
259		fvex	$⊢ \|seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k)\| \in V$
260	257 258 259	fvmpt3i	$⊢ i \in ℕ \to (k \in ℕ ⟼ \|seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k)\|) (i) = \|seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (i)\|$
261	237 260	syl	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to (k \in ℕ ⟼ \|seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k)\|) (i) = \|seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (i)\|$
262	244	fveq2d	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to \|(k \in ℕ ⟼ seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k)) (i)\| = \|seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (i)\|$
263	261 262	eqtr4d	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to (k \in ℕ ⟼ \|seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k)\|) (i) = \|(k \in ℕ ⟼ seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k)) (i)\|$
264	211 245 247 217 256 263	climabs	$⊢ ((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \to (k \in ℕ ⟼ \|seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k)\|) ⇝ \|seq 1 (+ F) (⌊m⌋) - t\|$
265	51	ad2antrr	$⊢ ((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \to 2 R \in ℝ$
266		0red	$⊢ (φ \land m \in [M, +∞)) \to 0 \in ℝ$
267	74	adantr	$⊢ (φ \land m \in [M, +∞)) \to M \in ℝ$
268	78	adantr	$⊢ (φ \land m \in [M, +∞)) \to 0 < M$
269	266 267 215 268 226	ltletrd	$⊢ (φ \land m \in [M, +∞)) \to 0 < m$
270	215 269	elrpd	$⊢ (φ \land m \in [M, +∞)) \to m \in ℝ^{+}$
271		nfcsb1v	$⊢ \underline{Ⅎ} n ⦋ m / n ⦌ A$
272	271	nfel1	$⊢ Ⅎ n ⦋ m / n ⦌ A \in ℝ$
273		csbeq1a	$⊢ n = m \to A = ⦋ m / n ⦌ A$
274	273	eleq1d	$⊢ n = m \to (A \in ℝ \leftrightarrow ⦋ m / n ⦌ A \in ℝ)$
275	272 274	rspc	$⊢ m \in ℝ^{+} \to (\forall n \in ℝ^{+} A \in ℝ \to ⦋ m / n ⦌ A \in ℝ)$
276	23 275	mpan9	$⊢ (φ \land m \in ℝ^{+}) \to ⦋ m / n ⦌ A \in ℝ$
277	270 276	syldan	$⊢ (φ \land m \in [M, +∞)) \to ⦋ m / n ⦌ A \in ℝ$
278	277	adantlr	$⊢ ((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \to ⦋ m / n ⦌ A \in ℝ$
279	265 278	remulcld	$⊢ ((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \to 2 R ⦋ m / n ⦌ A \in ℝ$
280	279	recnd	$⊢ ((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \to 2 R ⦋ m / n ⦌ A \in ℂ$
281		1z	$⊢ 1 \in ℤ$
282	17	eqimss2i	$⊢ ℤ_{\geq 1} \subseteq ℕ$
283	282 232	climconst2	$⊢ (2 R ⦋ m / n ⦌ A \in ℂ \land 1 \in ℤ) \to (ℕ \times \{2 R ⦋ m / n ⦌ A\}) ⇝ 2 R ⦋ m / n ⦌ A$
284	280 281 283	sylancl	$⊢ ((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \to (ℕ \times \{2 R ⦋ m / n ⦌ A\}) ⇝ 2 R ⦋ m / n ⦌ A$
285	253 238	subcld	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (i) \in ℂ$
286	285	abscld	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to \|seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (i)\| \in ℝ$
287	261 286	eqeltrd	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to (k \in ℕ ⟼ \|seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k)\|) (i) \in ℝ$
288		ovex	$⊢ 2 R ⦋ m / n ⦌ A \in V$
289	288	fvconst2	$⊢ i \in ℕ \to (ℕ \times \{2 R ⦋ m / n ⦌ A\}) (i) = 2 R ⦋ m / n ⦌ A$
290	237 289	syl	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to (ℕ \times \{2 R ⦋ m / n ⦌ A\}) (i) = 2 R ⦋ m / n ⦌ A$
291	279	adantr	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to 2 R ⦋ m / n ⦌ A \in ℝ$
292	290 291	eqeltrd	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to (ℕ \times \{2 R ⦋ m / n ⦌ A\}) (i) \in ℝ$
293		simplll	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to φ$
294	293 3	syl	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to N \in ℕ$
295	293 7	syl	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to X \in D$
296	293 8	syl	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to X \neq \underset{˙}{1}$
297	222	adantr	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to M \in ℕ$
298	293 11	sylan	$⊢ ((((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \land n \in ℝ^{+}) \to A \in ℝ$
299	293 12	syl3an1	$⊢ ((((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (M \leq n \land n \leq x)) \to B \leq A$
300	293 13	syl	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to (n \in ℝ^{+} ⟼ A) \underset{ℝ}{⇝} 0$
301	293 15	syl	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to R \in ℝ$
302	293 16	syl	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to \forall u \in (0 ..^N) \|\sum_{n \in (0 ..^u)} X (L (n))\| \leq R$
303	270	adantlr	$⊢ ((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \to m \in ℝ^{+}$
304	303	adantr	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to m \in ℝ^{+}$
305	227	adantr	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to M \leq m$
306	216	adantr	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to m \in ℝ$
307		reflcl	$⊢ m \in ℝ \to ⌊m⌋ \in ℝ$
308		peano2re	$⊢ ⌊m⌋ \in ℝ \to ⌊m⌋ + 1 \in ℝ$
309	306 307 308	3syl	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to ⌊m⌋ + 1 \in ℝ$
310		flltp1	$⊢ m \in ℝ \to m < ⌊m⌋ + 1$
311	306 310	syl	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to m < ⌊m⌋ + 1$
312	306 309 311	ltled	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to m \leq ⌊m⌋ + 1$
313	230	adantr	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to ⌊m⌋ \in ℕ$
314		simpr	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to i \in ℤ_{\geq ⌊m⌋}$
315	1 2 294 4 5 6 295 296 9 297 298 299 300 14 301 302 304 305 312 313 314	dchrisumlem2	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to \|seq 1 (+ F) (i) - seq 1 (+ F) (⌊m⌋)\| \leq 2 R ⦋ m / n ⦌ A$
316	253 238	abssubd	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to \|seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (i)\| = \|seq 1 (+ F) (i) - seq 1 (+ F) (⌊m⌋)\|$
317	261 316	eqtrd	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to (k \in ℕ ⟼ \|seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k)\|) (i) = \|seq 1 (+ F) (i) - seq 1 (+ F) (⌊m⌋)\|$
318	315 317 290	3brtr4d	$⊢ (((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \land i \in ℤ_{\geq ⌊m⌋}) \to (k \in ℕ ⟼ \|seq 1 (+ F) (⌊m⌋) - seq 1 (+ F) (k)\|) (i) \leq (ℕ \times \{2 R ⦋ m / n ⦌ A\}) (i)$
319	211 217 264 284 287 292 318	climle	$⊢ ((φ \land seq 1 (+ F) ⇝ t) \land m \in [M, +∞)) \to \|seq 1 (+ F) (⌊m⌋) - t\| \leq 2 R ⦋ m / n ⦌ A$
320	319	ralrimiva	$⊢ (φ \land seq 1 (+ F) ⇝ t) \to \forall m \in [M, +∞) \|seq 1 (+ F) (⌊m⌋) - t\| \leq 2 R ⦋ m / n ⦌ A$
321		oveq1	$⊢ c = 2 R \to c B = 2 R B$
322	321	breq2d	$⊢ c = 2 R \to (\|seq 1 (+ F) (⌊x⌋) - t\| \leq c B \leftrightarrow \|seq 1 (+ F) (⌊x⌋) - t\| \leq 2 R B)$
323	322	ralbidv	$⊢ c = 2 R \to (\forall x \in [M, +∞) \|seq 1 (+ F) (⌊x⌋) - t\| \leq c B \leftrightarrow \forall x \in [M, +∞) \|seq 1 (+ F) (⌊x⌋) - t\| \leq 2 R B)$
324		2fveq3	$⊢ m = x \to seq 1 (+ F) (⌊m⌋) = seq 1 (+ F) (⌊x⌋)$
325	324	fvoveq1d	$⊢ m = x \to \|seq 1 (+ F) (⌊m⌋) - t\| = \|seq 1 (+ F) (⌊x⌋) - t\|$
326		vex	$⊢ m \in V$
327	326	a1i	$⊢ m = x \to m \in V$
328		equequ2	$⊢ m = x \to (n = m \leftrightarrow n = x)$
329	328	biimpa	$⊢ (m = x \land n = m) \to n = x$
330	329 9	syl	$⊢ (m = x \land n = m) \to A = B$
331	327 330	csbied	$⊢ m = x \to ⦋ m / n ⦌ A = B$
332	331	oveq2d	$⊢ m = x \to 2 R ⦋ m / n ⦌ A = 2 R B$
333	325 332	breq12d	$⊢ m = x \to (\|seq 1 (+ F) (⌊m⌋) - t\| \leq 2 R ⦋ m / n ⦌ A \leftrightarrow \|seq 1 (+ F) (⌊x⌋) - t\| \leq 2 R B)$
334	333	cbvralvw	$⊢ \forall m \in [M, +∞) \|seq 1 (+ F) (⌊m⌋) - t\| \leq 2 R ⦋ m / n ⦌ A \leftrightarrow \forall x \in [M, +∞) \|seq 1 (+ F) (⌊x⌋) - t\| \leq 2 R B$
335	323 334	bitr4di	$⊢ c = 2 R \to (\forall x \in [M, +∞) \|seq 1 (+ F) (⌊x⌋) - t\| \leq c B \leftrightarrow \forall m \in [M, +∞) \|seq 1 (+ F) (⌊m⌋) - t\| \leq 2 R ⦋ m / n ⦌ A)$
336	335	rspcev	$⊢ (2 R \in [0, +∞) \land \forall m \in [M, +∞) \|seq 1 (+ F) (⌊m⌋) - t\| \leq 2 R ⦋ m / n ⦌ A) \to \exists c \in [0, +∞) \forall x \in [M, +∞) \|seq 1 (+ F) (⌊x⌋) - t\| \leq c B$
337	210 320 336	syl2anc	$⊢ (φ \land seq 1 (+ F) ⇝ t) \to \exists c \in [0, +∞) \forall x \in [M, +∞) \|seq 1 (+ F) (⌊x⌋) - t\| \leq c B$
338		r19.42v	$⊢ \exists c \in [0, +∞) (seq 1 (+ F) ⇝ t \land \forall x \in [M, +∞) \|seq 1 (+ F) (⌊x⌋) - t\| \leq c B) \leftrightarrow (seq 1 (+ F) ⇝ t \land \exists c \in [0, +∞) \forall x \in [M, +∞) \|seq 1 (+ F) (⌊x⌋) - t\| \leq c B)$
339	207 337 338	sylanbrc	$⊢ (φ \land seq 1 (+ F) ⇝ t) \to \exists c \in [0, +∞) (seq 1 (+ F) ⇝ t \land \forall x \in [M, +∞) \|seq 1 (+ F) (⌊x⌋) - t\| \leq c B)$
340	339	ex	$⊢ φ \to (seq 1 (+ F) ⇝ t \to \exists c \in [0, +∞) (seq 1 (+ F) ⇝ t \land \forall x \in [M, +∞) \|seq 1 (+ F) (⌊x⌋) - t\| \leq c B))$
341	340	eximdv	$⊢ φ \to (\exists t seq 1 (+ F) ⇝ t \to \exists t \exists c \in [0, +∞) (seq 1 (+ F) ⇝ t \land \forall x \in [M, +∞) \|seq 1 (+ F) (⌊x⌋) - t\| \leq c B))$
342	206 341	mpd	$⊢ φ \to \exists t \exists c \in [0, +∞) (seq 1 (+ F) ⇝ t \land \forall x \in [M, +∞) \|seq 1 (+ F) (⌊x⌋) - t\| \leq c B)$

Metamath Proof Explorer

Theorem dchrisumlem3

Proof