dchrisum0lem1b

	Ref	Expression
Hypotheses	rpvmasum.z	$⊢ Z = ℤ / N ℤ$
	rpvmasum.l	$⊢ L = ℤRHom (Z)$
	rpvmasum.a	$⊢ φ \to N \in ℕ$
	rpvmasum2.g	$⊢ G = DChr (N)$
	rpvmasum2.d	$⊢ D = {Base}_{G}$
	rpvmasum2.1	$⊢ \underset{˙}{1} = 0_{G}$
	rpvmasum2.w	$⊢ W = \{y \in (D ∖ \{\underset{˙}{1}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}$
	dchrisum0.b	$⊢ φ \to X \in W$
	dchrisum0lem1.f	$⊢ F = (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})$
	dchrisum0.c	$⊢ φ \to C \in [0, +∞)$
	dchrisum0.s	$⊢ φ \to seq 1 (+ F) ⇝ S$
	dchrisum0.1	$⊢ φ \to \forall y \in [1, +∞) \|seq 1 (+ F) (⌊y⌋) - S\| \leq \frac{C}{\sqrt{y}}$
Assertion	dchrisum0lem1b	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|\sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{X (L (m))}{\sqrt{m}})\| \leq \frac{2 C}{\sqrt{x}}$

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	$⊢ Z = ℤ / N ℤ$
2		rpvmasum.l	$⊢ L = ℤRHom (Z)$
3		rpvmasum.a	$⊢ φ \to N \in ℕ$
4		rpvmasum2.g	$⊢ G = DChr (N)$
5		rpvmasum2.d	$⊢ D = {Base}_{G}$
6		rpvmasum2.1	$⊢ \underset{˙}{1} = 0_{G}$
7		rpvmasum2.w	$⊢ W = \{y \in (D ∖ \{\underset{˙}{1}\}) \| \sum_{m \in ℕ} (\frac{y (L (m))}{m}) = 0\}$
8		dchrisum0.b	$⊢ φ \to X \in W$
9		dchrisum0lem1.f	$⊢ F = (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}})$
10		dchrisum0.c	$⊢ φ \to C \in [0, +∞)$
11		dchrisum0.s	$⊢ φ \to seq 1 (+ F) ⇝ S$
12		dchrisum0.1	$⊢ φ \to \forall y \in [1, +∞) \|seq 1 (+ F) (⌊y⌋) - S\| \leq \frac{C}{\sqrt{y}}$
13		fzfid	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋) \in Fin$
14		ssun2	$⊢ (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋) \subseteq (1 \dots ⌊x⌋) \cup (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋)$
15		simpr	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ^{+}$
16	15	rprege0d	$⊢ (φ \land x \in ℝ^{+}) \to (x \in ℝ \land 0 \leq x)$
17		flge0nn0	$⊢ (x \in ℝ \land 0 \leq x) \to ⌊x⌋ \in ℕ_{0}$
18	16 17	syl	$⊢ (φ \land x \in ℝ^{+}) \to ⌊x⌋ \in ℕ_{0}$
19		nn0p1nn	$⊢ ⌊x⌋ \in ℕ_{0} \to ⌊x⌋ + 1 \in ℕ$
20	18 19	syl	$⊢ (φ \land x \in ℝ^{+}) \to ⌊x⌋ + 1 \in ℕ$
21	20	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to ⌊x⌋ + 1 \in ℕ$
22		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
23	21 22	eleqtrdi	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to ⌊x⌋ + 1 \in ℤ_{\geq 1}$
24		dchrisum0lem1a	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (x \leq \frac{x^{2}}{d} \land ⌊\frac{x^{2}}{d}⌋ \in ℤ_{\geq ⌊x⌋})$
25	24	simprd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to ⌊\frac{x^{2}}{d}⌋ \in ℤ_{\geq ⌊x⌋}$
26		fzsplit2	$⊢ (⌊x⌋ + 1 \in ℤ_{\geq 1} \land ⌊\frac{x^{2}}{d}⌋ \in ℤ_{\geq ⌊x⌋}) \to (1 \dots ⌊\frac{x^{2}}{d}⌋) = (1 \dots ⌊x⌋) \cup (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋)$
27	23 25 26	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (1 \dots ⌊\frac{x^{2}}{d}⌋) = (1 \dots ⌊x⌋) \cup (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋)$
28	14 27	sseqtrrid	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋) \subseteq (1 \dots ⌊\frac{x^{2}}{d}⌋)$
29	28	sselda	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋)) \to m \in (1 \dots ⌊\frac{x^{2}}{d}⌋)$
30	7	ssrab3	$⊢ W \subseteq D ∖ \{\underset{˙}{1}\}$
31	30 8	sselid	$⊢ φ \to X \in (D ∖ \{\underset{˙}{1}\})$
32	31	eldifad	$⊢ φ \to X \in D$
33	32	ad3antrrr	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x^{2}}{d}⌋)) \to X \in D$
34		elfzelz	$⊢ m \in (1 \dots ⌊\frac{x^{2}}{d}⌋) \to m \in ℤ$
35	34	adantl	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x^{2}}{d}⌋)) \to m \in ℤ$
36	4 1 5 2 33 35	dchrzrhcl	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x^{2}}{d}⌋)) \to X (L (m)) \in ℂ$
37		elfznn	$⊢ m \in (1 \dots ⌊\frac{x^{2}}{d}⌋) \to m \in ℕ$
38	37	adantl	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x^{2}}{d}⌋)) \to m \in ℕ$
39	38	nnrpd	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x^{2}}{d}⌋)) \to m \in ℝ^{+}$
40	39	rpsqrtcld	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x^{2}}{d}⌋)) \to \sqrt{m} \in ℝ^{+}$
41	40	rpcnd	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x^{2}}{d}⌋)) \to \sqrt{m} \in ℂ$
42	40	rpne0d	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x^{2}}{d}⌋)) \to \sqrt{m} \neq 0$
43	36 41 42	divcld	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x^{2}}{d}⌋)) \to \frac{X (L (m))}{\sqrt{m}} \in ℂ$
44	29 43	syldan	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋)) \to \frac{X (L (m))}{\sqrt{m}} \in ℂ$
45	13 44	fsumcl	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{X (L (m))}{\sqrt{m}}) \in ℂ$
46	45	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|\sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{X (L (m))}{\sqrt{m}})\| \in ℝ$
47		1zzd	$⊢ φ \to 1 \in ℤ$
48	32	adantr	$⊢ (φ \land m \in ℕ) \to X \in D$
49		nnz	$⊢ m \in ℕ \to m \in ℤ$
50	49	adantl	$⊢ (φ \land m \in ℕ) \to m \in ℤ$
51	4 1 5 2 48 50	dchrzrhcl	$⊢ (φ \land m \in ℕ) \to X (L (m)) \in ℂ$
52		nnrp	$⊢ m \in ℕ \to m \in ℝ^{+}$
53	52	adantl	$⊢ (φ \land m \in ℕ) \to m \in ℝ^{+}$
54	53	rpsqrtcld	$⊢ (φ \land m \in ℕ) \to \sqrt{m} \in ℝ^{+}$
55	54	rpcnd	$⊢ (φ \land m \in ℕ) \to \sqrt{m} \in ℂ$
56	54	rpne0d	$⊢ (φ \land m \in ℕ) \to \sqrt{m} \neq 0$
57	51 55 56	divcld	$⊢ (φ \land m \in ℕ) \to \frac{X (L (m))}{\sqrt{m}} \in ℂ$
58		2fveq3	$⊢ a = m \to X (L (a)) = X (L (m))$
59		fveq2	$⊢ a = m \to \sqrt{a} = \sqrt{m}$
60	58 59	oveq12d	$⊢ a = m \to \frac{X (L (a))}{\sqrt{a}} = \frac{X (L (m))}{\sqrt{m}}$
61	60	cbvmptv	$⊢ (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}}) = (m \in ℕ ⟼ \frac{X (L (m))}{\sqrt{m}})$
62	9 61	eqtri	$⊢ F = (m \in ℕ ⟼ \frac{X (L (m))}{\sqrt{m}})$
63	57 62	fmptd	$⊢ φ \to F : ℕ ⟶ ℂ$
64	63	ffvelrnda	$⊢ (φ \land m \in ℕ) \to F (m) \in ℂ$
65	22 47 64	serf	$⊢ φ \to seq 1 (+ F) : ℕ ⟶ ℂ$
66	65	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to seq 1 (+ F) : ℕ ⟶ ℂ$
67	15	rpregt0d	$⊢ (φ \land x \in ℝ^{+}) \to (x \in ℝ \land 0 < x)$
68	67	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (x \in ℝ \land 0 < x)$
69	68	simpld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to x \in ℝ$
70		1red	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to 1 \in ℝ$
71		elfznn	$⊢ d \in (1 \dots ⌊x⌋) \to d \in ℕ$
72	71	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to d \in ℕ$
73	72	nnred	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to d \in ℝ$
74	72	nnge1d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to 1 \leq d$
75	15	rpred	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ$
76		fznnfl	$⊢ x \in ℝ \to (d \in (1 \dots ⌊x⌋) \leftrightarrow (d \in ℕ \land d \leq x))$
77	75 76	syl	$⊢ (φ \land x \in ℝ^{+}) \to (d \in (1 \dots ⌊x⌋) \leftrightarrow (d \in ℕ \land d \leq x))$
78	77	simplbda	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to d \leq x$
79	70 73 69 74 78	letrd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to 1 \leq x$
80		flge1nn	$⊢ (x \in ℝ \land 1 \leq x) \to ⌊x⌋ \in ℕ$
81	69 79 80	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to ⌊x⌋ \in ℕ$
82		eluznn	$⊢ (⌊x⌋ \in ℕ \land ⌊\frac{x^{2}}{d}⌋ \in ℤ_{\geq ⌊x⌋}) \to ⌊\frac{x^{2}}{d}⌋ \in ℕ$
83	81 25 82	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to ⌊\frac{x^{2}}{d}⌋ \in ℕ$
84	66 83	ffvelrnd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to seq 1 (+ F) (⌊\frac{x^{2}}{d}⌋) \in ℂ$
85		climcl	$⊢ seq 1 (+ F) ⇝ S \to S \in ℂ$
86	11 85	syl	$⊢ φ \to S \in ℂ$
87	86	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to S \in ℂ$
88	84 87	subcld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to seq 1 (+ F) (⌊\frac{x^{2}}{d}⌋) - S \in ℂ$
89	88	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|seq 1 (+ F) (⌊\frac{x^{2}}{d}⌋) - S\| \in ℝ$
90	66 81	ffvelrnd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to seq 1 (+ F) (⌊x⌋) \in ℂ$
91	87 90	subcld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to S - seq 1 (+ F) (⌊x⌋) \in ℂ$
92	91	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|S - seq 1 (+ F) (⌊x⌋)\| \in ℝ$
93	89 92	readdcld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|seq 1 (+ F) (⌊\frac{x^{2}}{d}⌋) - S\| + \|S - seq 1 (+ F) (⌊x⌋)\| \in ℝ$
94		2re	$⊢ 2 \in ℝ$
95		elrege0	$⊢ C \in [0, +∞) \leftrightarrow (C \in ℝ \land 0 \leq C)$
96	10 95	sylib	$⊢ φ \to (C \in ℝ \land 0 \leq C)$
97	96	simpld	$⊢ φ \to C \in ℝ$
98		remulcl	$⊢ (2 \in ℝ \land C \in ℝ) \to 2 C \in ℝ$
99	94 97 98	sylancr	$⊢ φ \to 2 C \in ℝ$
100	99	adantr	$⊢ (φ \land x \in ℝ^{+}) \to 2 C \in ℝ$
101	15	rpsqrtcld	$⊢ (φ \land x \in ℝ^{+}) \to \sqrt{x} \in ℝ^{+}$
102	100 101	rerpdivcld	$⊢ (φ \land x \in ℝ^{+}) \to \frac{2 C}{\sqrt{x}} \in ℝ$
103	102	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{2 C}{\sqrt{x}} \in ℝ$
104		ssun1	$⊢ (1 \dots ⌊x⌋) \subseteq (1 \dots ⌊x⌋) \cup (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋)$
105	104 27	sseqtrrid	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (1 \dots ⌊x⌋) \subseteq (1 \dots ⌊\frac{x^{2}}{d}⌋)$
106	105	sselda	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊x⌋)) \to m \in (1 \dots ⌊\frac{x^{2}}{d}⌋)$
107		ovex	$⊢ \frac{X (L (a))}{\sqrt{a}} \in V$
108	60 9 107	fvmpt3i	$⊢ m \in ℕ \to F (m) = \frac{X (L (m))}{\sqrt{m}}$
109	38 108	syl	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x^{2}}{d}⌋)) \to F (m) = \frac{X (L (m))}{\sqrt{m}}$
110	106 109	syldan	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊x⌋)) \to F (m) = \frac{X (L (m))}{\sqrt{m}}$
111	81 22	eleqtrdi	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to ⌊x⌋ \in ℤ_{\geq 1}$
112	106 43	syldan	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊x⌋)) \to \frac{X (L (m))}{\sqrt{m}} \in ℂ$
113	110 111 112	fsumser	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) = seq 1 (+ F) (⌊x⌋)$
114	113 90	eqeltrd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) \in ℂ$
115	114 45	pncan2d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) + \sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{X (L (m))}{\sqrt{m}}) - \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) = \sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{X (L (m))}{\sqrt{m}})$
116		reflcl	$⊢ x \in ℝ \to ⌊x⌋ \in ℝ$
117	69 116	syl	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to ⌊x⌋ \in ℝ$
118	117	ltp1d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to ⌊x⌋ < ⌊x⌋ + 1$
119		fzdisj	$⊢ ⌊x⌋ < ⌊x⌋ + 1 \to (1 \dots ⌊x⌋) \cap (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋) = \emptyset$
120	118 119	syl	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (1 \dots ⌊x⌋) \cap (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋) = \emptyset$
121		fzfid	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (1 \dots ⌊\frac{x^{2}}{d}⌋) \in Fin$
122	120 27 121 43	fsumsplit	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{X (L (m))}{\sqrt{m}}) = \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) + \sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{X (L (m))}{\sqrt{m}})$
123	83 22	eleqtrdi	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to ⌊\frac{x^{2}}{d}⌋ \in ℤ_{\geq 1}$
124	109 123 43	fsumser	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{X (L (m))}{\sqrt{m}}) = seq 1 (+ F) (⌊\frac{x^{2}}{d}⌋)$
125	122 124	eqtr3d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) + \sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{X (L (m))}{\sqrt{m}}) = seq 1 (+ F) (⌊\frac{x^{2}}{d}⌋)$
126	125 113	oveq12d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) + \sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{X (L (m))}{\sqrt{m}}) - \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) = seq 1 (+ F) (⌊\frac{x^{2}}{d}⌋) - seq 1 (+ F) (⌊x⌋)$
127	115 126	eqtr3d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{X (L (m))}{\sqrt{m}}) = seq 1 (+ F) (⌊\frac{x^{2}}{d}⌋) - seq 1 (+ F) (⌊x⌋)$
128	127	fveq2d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|\sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{X (L (m))}{\sqrt{m}})\| = \|seq 1 (+ F) (⌊\frac{x^{2}}{d}⌋) - seq 1 (+ F) (⌊x⌋)\|$
129	84 90 87	abs3difd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|seq 1 (+ F) (⌊\frac{x^{2}}{d}⌋) - seq 1 (+ F) (⌊x⌋)\| \leq \|seq 1 (+ F) (⌊\frac{x^{2}}{d}⌋) - S\| + \|S - seq 1 (+ F) (⌊x⌋)\|$
130	128 129	eqbrtrd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|\sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{X (L (m))}{\sqrt{m}})\| \leq \|seq 1 (+ F) (⌊\frac{x^{2}}{d}⌋) - S\| + \|S - seq 1 (+ F) (⌊x⌋)\|$
131	97	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to C \in ℝ$
132		simplr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to x \in ℝ^{+}$
133	132	rpsqrtcld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \sqrt{x} \in ℝ^{+}$
134	131 133	rerpdivcld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{C}{\sqrt{x}} \in ℝ$
135		2z	$⊢ 2 \in ℤ$
136		rpexpcl	$⊢ (x \in ℝ^{+} \land 2 \in ℤ) \to x^{2} \in ℝ^{+}$
137	15 135 136	sylancl	$⊢ (φ \land x \in ℝ^{+}) \to x^{2} \in ℝ^{+}$
138	137	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to x^{2} \in ℝ^{+}$
139	72	nnrpd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to d \in ℝ^{+}$
140	138 139	rpdivcld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{x^{2}}{d} \in ℝ^{+}$
141	140	rpsqrtcld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \sqrt{\frac{x^{2}}{d}} \in ℝ^{+}$
142	131 141	rerpdivcld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{C}{\sqrt{\frac{x^{2}}{d}}} \in ℝ$
143		2fveq3	$⊢ y = \frac{x^{2}}{d} \to seq 1 (+ F) (⌊y⌋) = seq 1 (+ F) (⌊\frac{x^{2}}{d}⌋)$
144	143	fvoveq1d	$⊢ y = \frac{x^{2}}{d} \to \|seq 1 (+ F) (⌊y⌋) - S\| = \|seq 1 (+ F) (⌊\frac{x^{2}}{d}⌋) - S\|$
145		fveq2	$⊢ y = \frac{x^{2}}{d} \to \sqrt{y} = \sqrt{\frac{x^{2}}{d}}$
146	145	oveq2d	$⊢ y = \frac{x^{2}}{d} \to \frac{C}{\sqrt{y}} = \frac{C}{\sqrt{\frac{x^{2}}{d}}}$
147	144 146	breq12d	$⊢ y = \frac{x^{2}}{d} \to (\|seq 1 (+ F) (⌊y⌋) - S\| \leq \frac{C}{\sqrt{y}} \leftrightarrow \|seq 1 (+ F) (⌊\frac{x^{2}}{d}⌋) - S\| \leq \frac{C}{\sqrt{\frac{x^{2}}{d}}})$
148	12	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \forall y \in [1, +∞) \|seq 1 (+ F) (⌊y⌋) - S\| \leq \frac{C}{\sqrt{y}}$
149	137	rpred	$⊢ (φ \land x \in ℝ^{+}) \to x^{2} \in ℝ$
150		nndivre	$⊢ (x^{2} \in ℝ \land d \in ℕ) \to \frac{x^{2}}{d} \in ℝ$
151	149 71 150	syl2an	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{x^{2}}{d} \in ℝ$
152	24	simpld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to x \leq \frac{x^{2}}{d}$
153	70 69 151 79 152	letrd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to 1 \leq \frac{x^{2}}{d}$
154		1re	$⊢ 1 \in ℝ$
155		elicopnf	$⊢ 1 \in ℝ \to (\frac{x^{2}}{d} \in [1, +∞) \leftrightarrow (\frac{x^{2}}{d} \in ℝ \land 1 \leq \frac{x^{2}}{d}))$
156	154 155	ax-mp	$⊢ \frac{x^{2}}{d} \in [1, +∞) \leftrightarrow (\frac{x^{2}}{d} \in ℝ \land 1 \leq \frac{x^{2}}{d})$
157	151 153 156	sylanbrc	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{x^{2}}{d} \in [1, +∞)$
158	147 148 157	rspcdva	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|seq 1 (+ F) (⌊\frac{x^{2}}{d}⌋) - S\| \leq \frac{C}{\sqrt{\frac{x^{2}}{d}}}$
159	133	rpregt0d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (\sqrt{x} \in ℝ \land 0 < \sqrt{x})$
160	141	rpregt0d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (\sqrt{\frac{x^{2}}{d}} \in ℝ \land 0 < \sqrt{\frac{x^{2}}{d}})$
161	96	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (C \in ℝ \land 0 \leq C)$
162	132	rprege0d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (x \in ℝ \land 0 \leq x)$
163	140	rprege0d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (\frac{x^{2}}{d} \in ℝ \land 0 \leq \frac{x^{2}}{d})$
164		sqrtle	$⊢ ((x \in ℝ \land 0 \leq x) \land (\frac{x^{2}}{d} \in ℝ \land 0 \leq \frac{x^{2}}{d})) \to (x \leq \frac{x^{2}}{d} \leftrightarrow \sqrt{x} \leq \sqrt{\frac{x^{2}}{d}})$
165	162 163 164	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (x \leq \frac{x^{2}}{d} \leftrightarrow \sqrt{x} \leq \sqrt{\frac{x^{2}}{d}})$
166	152 165	mpbid	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \sqrt{x} \leq \sqrt{\frac{x^{2}}{d}}$
167		lediv2a	$⊢ (((\sqrt{x} \in ℝ \land 0 < \sqrt{x}) \land (\sqrt{\frac{x^{2}}{d}} \in ℝ \land 0 < \sqrt{\frac{x^{2}}{d}}) \land (C \in ℝ \land 0 \leq C)) \land \sqrt{x} \leq \sqrt{\frac{x^{2}}{d}}) \to \frac{C}{\sqrt{\frac{x^{2}}{d}}} \leq \frac{C}{\sqrt{x}}$
168	159 160 161 166 167	syl31anc	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{C}{\sqrt{\frac{x^{2}}{d}}} \leq \frac{C}{\sqrt{x}}$
169	89 142 134 158 168	letrd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|seq 1 (+ F) (⌊\frac{x^{2}}{d}⌋) - S\| \leq \frac{C}{\sqrt{x}}$
170	87 90	abssubd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|S - seq 1 (+ F) (⌊x⌋)\| = \|seq 1 (+ F) (⌊x⌋) - S\|$
171		2fveq3	$⊢ y = x \to seq 1 (+ F) (⌊y⌋) = seq 1 (+ F) (⌊x⌋)$
172	171	fvoveq1d	$⊢ y = x \to \|seq 1 (+ F) (⌊y⌋) - S\| = \|seq 1 (+ F) (⌊x⌋) - S\|$
173		fveq2	$⊢ y = x \to \sqrt{y} = \sqrt{x}$
174	173	oveq2d	$⊢ y = x \to \frac{C}{\sqrt{y}} = \frac{C}{\sqrt{x}}$
175	172 174	breq12d	$⊢ y = x \to (\|seq 1 (+ F) (⌊y⌋) - S\| \leq \frac{C}{\sqrt{y}} \leftrightarrow \|seq 1 (+ F) (⌊x⌋) - S\| \leq \frac{C}{\sqrt{x}})$
176		elicopnf	$⊢ 1 \in ℝ \to (x \in [1, +∞) \leftrightarrow (x \in ℝ \land 1 \leq x))$
177	154 176	ax-mp	$⊢ x \in [1, +∞) \leftrightarrow (x \in ℝ \land 1 \leq x)$
178	69 79 177	sylanbrc	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to x \in [1, +∞)$
179	175 148 178	rspcdva	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|seq 1 (+ F) (⌊x⌋) - S\| \leq \frac{C}{\sqrt{x}}$
180	170 179	eqbrtrd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|S - seq 1 (+ F) (⌊x⌋)\| \leq \frac{C}{\sqrt{x}}$
181	89 92 134 134 169 180	le2addd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|seq 1 (+ F) (⌊\frac{x^{2}}{d}⌋) - S\| + \|S - seq 1 (+ F) (⌊x⌋)\| \leq (\frac{C}{\sqrt{x}}) + (\frac{C}{\sqrt{x}})$
182		2cnd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to 2 \in ℂ$
183	97	adantr	$⊢ (φ \land x \in ℝ^{+}) \to C \in ℝ$
184	183	recnd	$⊢ (φ \land x \in ℝ^{+}) \to C \in ℂ$
185	184	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to C \in ℂ$
186	101	rpcnne0d	$⊢ (φ \land x \in ℝ^{+}) \to (\sqrt{x} \in ℂ \land \sqrt{x} \neq 0)$
187	186	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (\sqrt{x} \in ℂ \land \sqrt{x} \neq 0)$
188		divass	$⊢ (2 \in ℂ \land C \in ℂ \land (\sqrt{x} \in ℂ \land \sqrt{x} \neq 0)) \to \frac{2 C}{\sqrt{x}} = 2 (\frac{C}{\sqrt{x}})$
189	182 185 187 188	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{2 C}{\sqrt{x}} = 2 (\frac{C}{\sqrt{x}})$
190	134	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{C}{\sqrt{x}} \in ℂ$
191	190	2timesd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to 2 (\frac{C}{\sqrt{x}}) = (\frac{C}{\sqrt{x}}) + (\frac{C}{\sqrt{x}})$
192	189 191	eqtrd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{2 C}{\sqrt{x}} = (\frac{C}{\sqrt{x}}) + (\frac{C}{\sqrt{x}})$
193	181 192	breqtrrd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|seq 1 (+ F) (⌊\frac{x^{2}}{d}⌋) - S\| + \|S - seq 1 (+ F) (⌊x⌋)\| \leq \frac{2 C}{\sqrt{x}}$
194	46 93 103 130 193	letrd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|\sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{X (L (m))}{\sqrt{m}})\| \leq \frac{2 C}{\sqrt{x}}$

Metamath Proof Explorer

Theorem dchrisum0lem1b

Proof