dchrisum0lem1

	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	dchrisum0lem1	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{m = ⌊x⌋ + 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})) \in 𝑂 (1)$

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 ℝ^{+}) \to (1 \dots ⌊x⌋) \in Fin$
14		fzfid	$⊢ (φ \land x \in ℝ^{+}) \to (⌊x⌋ + 1 \dots ⌊x^{2}⌋) \in Fin$
15		fzfid	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋) \in Fin$
16		elfznn	$⊢ d \in (1 \dots ⌊x⌋) \to d \in ℕ$
17		elfzuz	$⊢ m \in (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋) \to m \in ℤ_{\geq (⌊x⌋ + 1)}$
18	16 17	anim12i	$⊢ (d \in (1 \dots ⌊x⌋) \land m \in (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋)) \to (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})$
19	18	a1i	$⊢ (φ \land x \in ℝ^{+}) \to ((d \in (1 \dots ⌊x⌋) \land m \in (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋)) \to (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)}))$
20		elfzuz	$⊢ m \in (⌊x⌋ + 1 \dots ⌊x^{2}⌋) \to m \in ℤ_{\geq (⌊x⌋ + 1)}$
21		elfznn	$⊢ d \in (1 \dots ⌊\frac{x^{2}}{m}⌋) \to d \in ℕ$
22	20 21	anim12ci	$⊢ (m \in (⌊x⌋ + 1 \dots ⌊x^{2}⌋) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})$
23	22	a1i	$⊢ (φ \land x \in ℝ^{+}) \to ((m \in (⌊x⌋ + 1 \dots ⌊x^{2}⌋) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)}))$
24		eluzelz	$⊢ m \in ℤ_{\geq (⌊x⌋ + 1)} \to m \in ℤ$
25	24	ad2antll	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to m \in ℤ$
26	25	zred	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to m \in ℝ$
27		simpr	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ^{+}$
28		2z	$⊢ 2 \in ℤ$
29		rpexpcl	$⊢ (x \in ℝ^{+} \land 2 \in ℤ) \to x^{2} \in ℝ^{+}$
30	27 28 29	sylancl	$⊢ (φ \land x \in ℝ^{+}) \to x^{2} \in ℝ^{+}$
31	30	rpred	$⊢ (φ \land x \in ℝ^{+}) \to x^{2} \in ℝ$
32	31	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to x^{2} \in ℝ$
33		simprl	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to d \in ℕ$
34	33	nnrpd	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to d \in ℝ^{+}$
35	26 32 34	lemuldivd	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to (m d \leq x^{2} \leftrightarrow m \leq \frac{x^{2}}{d})$
36	33	nnred	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to d \in ℝ$
37	27	rprege0d	$⊢ (φ \land x \in ℝ^{+}) \to (x \in ℝ \land 0 \leq x)$
38		flge0nn0	$⊢ (x \in ℝ \land 0 \leq x) \to ⌊x⌋ \in ℕ_{0}$
39		nn0p1nn	$⊢ ⌊x⌋ \in ℕ_{0} \to ⌊x⌋ + 1 \in ℕ$
40	37 38 39	3syl	$⊢ (φ \land x \in ℝ^{+}) \to ⌊x⌋ + 1 \in ℕ$
41	40	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to ⌊x⌋ + 1 \in ℕ$
42		simprr	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to m \in ℤ_{\geq (⌊x⌋ + 1)}$
43		eluznn	$⊢ (⌊x⌋ + 1 \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)}) \to m \in ℕ$
44	41 42 43	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to m \in ℕ$
45	44	nnrpd	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to m \in ℝ^{+}$
46	36 32 45	lemuldiv2d	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to (m d \leq x^{2} \leftrightarrow d \leq \frac{x^{2}}{m})$
47	35 46	bitr3d	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to (m \leq \frac{x^{2}}{d} \leftrightarrow d \leq \frac{x^{2}}{m})$
48		rpcn	$⊢ x \in ℝ^{+} \to x \in ℂ$
49	48	adantl	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℂ$
50	49	sqvald	$⊢ (φ \land x \in ℝ^{+}) \to x^{2} = x x$
51	50	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to x^{2} = x x$
52		simplr	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to x \in ℝ^{+}$
53	52	rpred	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to x \in ℝ$
54		reflcl	$⊢ x \in ℝ \to ⌊x⌋ \in ℝ$
55		peano2re	$⊢ ⌊x⌋ \in ℝ \to ⌊x⌋ + 1 \in ℝ$
56	53 54 55	3syl	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to ⌊x⌋ + 1 \in ℝ$
57		fllep1	$⊢ x \in ℝ \to x \leq ⌊x⌋ + 1$
58	53 57	syl	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to x \leq ⌊x⌋ + 1$
59		eluzle	$⊢ m \in ℤ_{\geq (⌊x⌋ + 1)} \to ⌊x⌋ + 1 \leq m$
60	59	ad2antll	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to ⌊x⌋ + 1 \leq m$
61	53 56 26 58 60	letrd	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to x \leq m$
62	53 26 52	lemul1d	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to (x \leq m \leftrightarrow x x \leq m x)$
63	61 62	mpbid	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to x x \leq m x$
64	51 63	eqbrtrd	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to x^{2} \leq m x$
65	32 53 45	ledivmuld	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to (\frac{x^{2}}{m} \leq x \leftrightarrow x^{2} \leq m x)$
66	64 65	mpbird	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to \frac{x^{2}}{m} \leq x$
67		nnre	$⊢ d \in ℕ \to d \in ℝ$
68	67	ad2antrl	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to d \in ℝ$
69	32 44	nndivred	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to \frac{x^{2}}{m} \in ℝ$
70		letr	$⊢ (d \in ℝ \land \frac{x^{2}}{m} \in ℝ \land x \in ℝ) \to ((d \leq \frac{x^{2}}{m} \land \frac{x^{2}}{m} \leq x) \to d \leq x)$
71	68 69 53 70	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to ((d \leq \frac{x^{2}}{m} \land \frac{x^{2}}{m} \leq x) \to d \leq x)$
72	66 71	mpan2d	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to (d \leq \frac{x^{2}}{m} \to d \leq x)$
73	47 72	sylbid	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to (m \leq \frac{x^{2}}{d} \to d \leq x)$
74	73	pm4.71rd	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to (m \leq \frac{x^{2}}{d} \leftrightarrow (d \leq x \land m \leq \frac{x^{2}}{d}))$
75		nnge1	$⊢ d \in ℕ \to 1 \leq d$
76	75	ad2antrl	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to 1 \leq d$
77		1re	$⊢ 1 \in ℝ$
78		0lt1	$⊢ 0 < 1$
79	77 78	pm3.2i	$⊢ (1 \in ℝ \land 0 < 1)$
80	34	rpregt0d	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to (d \in ℝ \land 0 < d)$
81	30	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to x^{2} \in ℝ^{+}$
82	81	rpregt0d	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to (x^{2} \in ℝ \land 0 < x^{2})$
83		lediv2	$⊢ ((1 \in ℝ \land 0 < 1) \land (d \in ℝ \land 0 < d) \land (x^{2} \in ℝ \land 0 < x^{2})) \to (1 \leq d \leftrightarrow \frac{x^{2}}{d} \leq \frac{x^{2}}{1})$
84	79 80 82 83	mp3an2i	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to (1 \leq d \leftrightarrow \frac{x^{2}}{d} \leq \frac{x^{2}}{1})$
85	76 84	mpbid	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to \frac{x^{2}}{d} \leq \frac{x^{2}}{1}$
86	32	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to x^{2} \in ℂ$
87	86	div1d	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to \frac{x^{2}}{1} = x^{2}$
88	85 87	breqtrd	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to \frac{x^{2}}{d} \leq x^{2}$
89		simpl	$⊢ (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)}) \to d \in ℕ$
90		nndivre	$⊢ (x^{2} \in ℝ \land d \in ℕ) \to \frac{x^{2}}{d} \in ℝ$
91	31 89 90	syl2an	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to \frac{x^{2}}{d} \in ℝ$
92		letr	$⊢ (m \in ℝ \land \frac{x^{2}}{d} \in ℝ \land x^{2} \in ℝ) \to ((m \leq \frac{x^{2}}{d} \land \frac{x^{2}}{d} \leq x^{2}) \to m \leq x^{2})$
93	26 91 32 92	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to ((m \leq \frac{x^{2}}{d} \land \frac{x^{2}}{d} \leq x^{2}) \to m \leq x^{2})$
94	88 93	mpan2d	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to (m \leq \frac{x^{2}}{d} \to m \leq x^{2})$
95	47 94	sylbird	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to (d \leq \frac{x^{2}}{m} \to m \leq x^{2})$
96	95	pm4.71rd	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to (d \leq \frac{x^{2}}{m} \leftrightarrow (m \leq x^{2} \land d \leq \frac{x^{2}}{m}))$
97	47 74 96	3bitr3d	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to ((d \leq x \land m \leq \frac{x^{2}}{d}) \leftrightarrow (m \leq x^{2} \land d \leq \frac{x^{2}}{m}))$
98		fznnfl	$⊢ x \in ℝ \to (d \in (1 \dots ⌊x⌋) \leftrightarrow (d \in ℕ \land d \leq x))$
99	98	baibd	$⊢ (x \in ℝ \land d \in ℕ) \to (d \in (1 \dots ⌊x⌋) \leftrightarrow d \leq x)$
100	53 33 99	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to (d \in (1 \dots ⌊x⌋) \leftrightarrow d \leq x)$
101	91	flcld	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to ⌊\frac{x^{2}}{d}⌋ \in ℤ$
102		elfz5	$⊢ (m \in ℤ_{\geq (⌊x⌋ + 1)} \land ⌊\frac{x^{2}}{d}⌋ \in ℤ) \to (m \in (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋) \leftrightarrow m \leq ⌊\frac{x^{2}}{d}⌋)$
103	42 101 102	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to (m \in (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋) \leftrightarrow m \leq ⌊\frac{x^{2}}{d}⌋)$
104		flge	$⊢ (\frac{x^{2}}{d} \in ℝ \land m \in ℤ) \to (m \leq \frac{x^{2}}{d} \leftrightarrow m \leq ⌊\frac{x^{2}}{d}⌋)$
105	91 25 104	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to (m \leq \frac{x^{2}}{d} \leftrightarrow m \leq ⌊\frac{x^{2}}{d}⌋)$
106	103 105	bitr4d	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to (m \in (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋) \leftrightarrow m \leq \frac{x^{2}}{d})$
107	100 106	anbi12d	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to ((d \in (1 \dots ⌊x⌋) \land m \in (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋)) \leftrightarrow (d \leq x \land m \leq \frac{x^{2}}{d}))$
108	32	flcld	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to ⌊x^{2}⌋ \in ℤ$
109		elfz5	$⊢ (m \in ℤ_{\geq (⌊x⌋ + 1)} \land ⌊x^{2}⌋ \in ℤ) \to (m \in (⌊x⌋ + 1 \dots ⌊x^{2}⌋) \leftrightarrow m \leq ⌊x^{2}⌋)$
110	42 108 109	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to (m \in (⌊x⌋ + 1 \dots ⌊x^{2}⌋) \leftrightarrow m \leq ⌊x^{2}⌋)$
111		flge	$⊢ (x^{2} \in ℝ \land m \in ℤ) \to (m \leq x^{2} \leftrightarrow m \leq ⌊x^{2}⌋)$
112	32 25 111	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to (m \leq x^{2} \leftrightarrow m \leq ⌊x^{2}⌋)$
113	110 112	bitr4d	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to (m \in (⌊x⌋ + 1 \dots ⌊x^{2}⌋) \leftrightarrow m \leq x^{2})$
114		fznnfl	$⊢ \frac{x^{2}}{m} \in ℝ \to (d \in (1 \dots ⌊\frac{x^{2}}{m}⌋) \leftrightarrow (d \in ℕ \land d \leq \frac{x^{2}}{m}))$
115	114	baibd	$⊢ (\frac{x^{2}}{m} \in ℝ \land d \in ℕ) \to (d \in (1 \dots ⌊\frac{x^{2}}{m}⌋) \leftrightarrow d \leq \frac{x^{2}}{m})$
116	69 33 115	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to (d \in (1 \dots ⌊\frac{x^{2}}{m}⌋) \leftrightarrow d \leq \frac{x^{2}}{m})$
117	113 116	anbi12d	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to ((m \in (⌊x⌋ + 1 \dots ⌊x^{2}⌋) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \leftrightarrow (m \leq x^{2} \land d \leq \frac{x^{2}}{m}))$
118	97 107 117	3bitr4d	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)})) \to ((d \in (1 \dots ⌊x⌋) \land m \in (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋)) \leftrightarrow (m \in (⌊x⌋ + 1 \dots ⌊x^{2}⌋) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)))$
119	118	ex	$⊢ (φ \land x \in ℝ^{+}) \to ((d \in ℕ \land m \in ℤ_{\geq (⌊x⌋ + 1)}) \to ((d \in (1 \dots ⌊x⌋) \land m \in (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋)) \leftrightarrow (m \in (⌊x⌋ + 1 \dots ⌊x^{2}⌋) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋))))$
120	19 23 119	pm5.21ndd	$⊢ (φ \land x \in ℝ^{+}) \to ((d \in (1 \dots ⌊x⌋) \land m \in (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋)) \leftrightarrow (m \in (⌊x⌋ + 1 \dots ⌊x^{2}⌋) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)))$
121		ssun2	$⊢ (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋) \subseteq (1 \dots ⌊x⌋) \cup (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋)$
122	40	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to ⌊x⌋ + 1 \in ℕ$
123		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
124	122 123	eleqtrdi	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to ⌊x⌋ + 1 \in ℤ_{\geq 1}$
125		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⌋})$
126	125	simprd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to ⌊\frac{x^{2}}{d}⌋ \in ℤ_{\geq ⌊x⌋}$
127		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}⌋)$
128	124 126 127	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}⌋)$
129	121 128	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}⌋)$
130	129	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}⌋)$
131	7	ssrab3	$⊢ W \subseteq D ∖ \{\underset{˙}{1}\}$
132	131 8	sselid	$⊢ φ \to X \in (D ∖ \{\underset{˙}{1}\})$
133	132	eldifad	$⊢ φ \to X \in D$
134	133	ad3antrrr	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x^{2}}{d}⌋)) \to X \in D$
135		elfzelz	$⊢ m \in (1 \dots ⌊\frac{x^{2}}{d}⌋) \to m \in ℤ$
136	135	adantl	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x^{2}}{d}⌋)) \to m \in ℤ$
137	4 1 5 2 134 136	dchrzrhcl	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x^{2}}{d}⌋)) \to X (L (m)) \in ℂ$
138		elfznn	$⊢ m \in (1 \dots ⌊\frac{x^{2}}{d}⌋) \to m \in ℕ$
139	138	adantl	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x^{2}}{d}⌋)) \to m \in ℕ$
140	139	nnrpd	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x^{2}}{d}⌋)) \to m \in ℝ^{+}$
141	140	rpsqrtcld	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x^{2}}{d}⌋)) \to \sqrt{m} \in ℝ^{+}$
142	141	rpcnd	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x^{2}}{d}⌋)) \to \sqrt{m} \in ℂ$
143	141	rpne0d	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x^{2}}{d}⌋)) \to \sqrt{m} \neq 0$
144	137 142 143	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 ℂ$
145	16	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to d \in ℕ$
146	145	nnrpd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to d \in ℝ^{+}$
147	146	rpsqrtcld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \sqrt{d} \in ℝ^{+}$
148	147	rpcnne0d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (\sqrt{d} \in ℂ \land \sqrt{d} \neq 0)$
149	148	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x^{2}}{d}⌋)) \to (\sqrt{d} \in ℂ \land \sqrt{d} \neq 0)$
150	149	simpld	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x^{2}}{d}⌋)) \to \sqrt{d} \in ℂ$
151	149	simprd	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x^{2}}{d}⌋)) \to \sqrt{d} \neq 0$
152	144 150 151	divcld	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x^{2}}{d}⌋)) \to \frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}} \in ℂ$
153	130 152	syldan	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land m \in (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋)) \to \frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}} \in ℂ$
154	153	anasss	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in (1 \dots ⌊x⌋) \land m \in (⌊x⌋ + 1 \dots ⌊\frac{x^{2}}{d}⌋))) \to \frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}} \in ℂ$
155	13 14 15 120 154	fsumcom2	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} \sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) = \sum_{m = ⌊x⌋ + 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})$
156	155	mpteq2dva	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} \sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})) = (x \in ℝ^{+} ⟼ \sum_{m = ⌊x⌋ + 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}))$
157	77	a1i	$⊢ φ \to 1 \in ℝ$
158		2cn	$⊢ 2 \in ℂ$
159	27	rpsqrtcld	$⊢ (φ \land x \in ℝ^{+}) \to \sqrt{x} \in ℝ^{+}$
160	159	rpcnd	$⊢ (φ \land x \in ℝ^{+}) \to \sqrt{x} \in ℂ$
161		mulcl	$⊢ (2 \in ℂ \land \sqrt{x} \in ℂ) \to 2 \sqrt{x} \in ℂ$
162	158 160 161	sylancr	$⊢ (φ \land x \in ℝ^{+}) \to 2 \sqrt{x} \in ℂ$
163	147	rprecred	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{1}{\sqrt{d}} \in ℝ$
164	13 163	fsumrecl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) \in ℝ$
165	164	recnd	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) \in ℂ$
166	165 162	subcld	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{x} \in ℂ$
167		2re	$⊢ 2 \in ℝ$
168		elrege0	$⊢ C \in [0, +∞) \leftrightarrow (C \in ℝ \land 0 \leq C)$
169	10 168	sylib	$⊢ φ \to (C \in ℝ \land 0 \leq C)$
170	169	simpld	$⊢ φ \to C \in ℝ$
171		remulcl	$⊢ (2 \in ℝ \land C \in ℝ) \to 2 C \in ℝ$
172	167 170 171	sylancr	$⊢ φ \to 2 C \in ℝ$
173	172	adantr	$⊢ (φ \land x \in ℝ^{+}) \to 2 C \in ℝ$
174	173 159	rerpdivcld	$⊢ (φ \land x \in ℝ^{+}) \to \frac{2 C}{\sqrt{x}} \in ℝ$
175	174	recnd	$⊢ (φ \land x \in ℝ^{+}) \to \frac{2 C}{\sqrt{x}} \in ℂ$
176	162 166 175	adddird	$⊢ (φ \land x \in ℝ^{+}) \to (2 \sqrt{x} + \sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{x}) (\frac{2 C}{\sqrt{x}}) = 2 \sqrt{x} (\frac{2 C}{\sqrt{x}}) + (\sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{x}) (\frac{2 C}{\sqrt{x}})$
177	162 165	pncan3d	$⊢ (φ \land x \in ℝ^{+}) \to 2 \sqrt{x} + \sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{x} = \sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}})$
178	177	oveq1d	$⊢ (φ \land x \in ℝ^{+}) \to (2 \sqrt{x} + \sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{x}) (\frac{2 C}{\sqrt{x}}) = \sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) (\frac{2 C}{\sqrt{x}})$
179		2cnd	$⊢ (φ \land x \in ℝ^{+}) \to 2 \in ℂ$
180	179 160 175	mulassd	$⊢ (φ \land x \in ℝ^{+}) \to 2 \sqrt{x} (\frac{2 C}{\sqrt{x}}) = 2 \sqrt{x} (\frac{2 C}{\sqrt{x}})$
181	173	recnd	$⊢ (φ \land x \in ℝ^{+}) \to 2 C \in ℂ$
182	159	rpne0d	$⊢ (φ \land x \in ℝ^{+}) \to \sqrt{x} \neq 0$
183	181 160 182	divcan2d	$⊢ (φ \land x \in ℝ^{+}) \to \sqrt{x} (\frac{2 C}{\sqrt{x}}) = 2 C$
184	183	oveq2d	$⊢ (φ \land x \in ℝ^{+}) \to 2 \sqrt{x} (\frac{2 C}{\sqrt{x}}) = 2 2 C$
185	180 184	eqtrd	$⊢ (φ \land x \in ℝ^{+}) \to 2 \sqrt{x} (\frac{2 C}{\sqrt{x}}) = 2 2 C$
186	185	oveq1d	$⊢ (φ \land x \in ℝ^{+}) \to 2 \sqrt{x} (\frac{2 C}{\sqrt{x}}) + (\sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{x}) (\frac{2 C}{\sqrt{x}}) = 2 2 C + (\sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{x}) (\frac{2 C}{\sqrt{x}})$
187	176 178 186	3eqtr3d	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) (\frac{2 C}{\sqrt{x}}) = 2 2 C + (\sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{x}) (\frac{2 C}{\sqrt{x}})$
188	187	mpteq2dva	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) (\frac{2 C}{\sqrt{x}})) = (x \in ℝ^{+} ⟼ 2 2 C + (\sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{x}) (\frac{2 C}{\sqrt{x}}))$
189		remulcl	$⊢ (2 \in ℝ \land 2 C \in ℝ) \to 2 2 C \in ℝ$
190	167 172 189	sylancr	$⊢ φ \to 2 2 C \in ℝ$
191	190	recnd	$⊢ φ \to 2 2 C \in ℂ$
192	191	adantr	$⊢ (φ \land x \in ℝ^{+}) \to 2 2 C \in ℂ$
193	166 175	mulcld	$⊢ (φ \land x \in ℝ^{+}) \to (\sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{x}) (\frac{2 C}{\sqrt{x}}) \in ℂ$
194		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
195		o1const	$⊢ (ℝ^{+} \subseteq ℝ \land 2 2 C \in ℂ) \to (x \in ℝ^{+} ⟼ 2 2 C) \in 𝑂 (1)$
196	194 191 195	sylancr	$⊢ φ \to (x \in ℝ^{+} ⟼ 2 2 C) \in 𝑂 (1)$
197		eqid	$⊢ (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{x}) = (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{x})$
198	197	divsqrsum	$⊢ (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{x}) \in dom \underset{ℝ}{⇝}$
199		rlimdmo1	$⊢ (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{x}) \in dom \underset{ℝ}{⇝} \to (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{x}) \in 𝑂 (1)$
200	198 199	mp1i	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{x}) \in 𝑂 (1)$
201	181 160 182	divrecd	$⊢ (φ \land x \in ℝ^{+}) \to \frac{2 C}{\sqrt{x}} = 2 C (\frac{1}{\sqrt{x}})$
202	201	mpteq2dva	$⊢ φ \to (x \in ℝ^{+} ⟼ \frac{2 C}{\sqrt{x}}) = (x \in ℝ^{+} ⟼ 2 C (\frac{1}{\sqrt{x}}))$
203	159	rprecred	$⊢ (φ \land x \in ℝ^{+}) \to \frac{1}{\sqrt{x}} \in ℝ$
204	172	recnd	$⊢ φ \to 2 C \in ℂ$
205		rlimconst	$⊢ (ℝ^{+} \subseteq ℝ \land 2 C \in ℂ) \to (x \in ℝ^{+} ⟼ 2 C) \underset{ℝ}{⇝} 2 C$
206	194 204 205	sylancr	$⊢ φ \to (x \in ℝ^{+} ⟼ 2 C) \underset{ℝ}{⇝} 2 C$
207		sqrtlim	$⊢ (x \in ℝ^{+} ⟼ \frac{1}{\sqrt{x}}) \underset{ℝ}{⇝} 0$
208	207	a1i	$⊢ φ \to (x \in ℝ^{+} ⟼ \frac{1}{\sqrt{x}}) \underset{ℝ}{⇝} 0$
209	173 203 206 208	rlimmul	$⊢ φ \to (x \in ℝ^{+} ⟼ 2 C (\frac{1}{\sqrt{x}})) \underset{ℝ}{⇝} 2 C \cdot 0$
210	202 209	eqbrtrd	$⊢ φ \to (x \in ℝ^{+} ⟼ \frac{2 C}{\sqrt{x}}) \underset{ℝ}{⇝} 2 C \cdot 0$
211		rlimo1	$⊢ (x \in ℝ^{+} ⟼ \frac{2 C}{\sqrt{x}}) \underset{ℝ}{⇝} 2 C \cdot 0 \to (x \in ℝ^{+} ⟼ \frac{2 C}{\sqrt{x}}) \in 𝑂 (1)$
212	210 211	syl	$⊢ φ \to (x \in ℝ^{+} ⟼ \frac{2 C}{\sqrt{x}}) \in 𝑂 (1)$
213	166 175 200 212	o1mul2	$⊢ φ \to (x \in ℝ^{+} ⟼ (\sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{x}) (\frac{2 C}{\sqrt{x}})) \in 𝑂 (1)$
214	192 193 196 213	o1add2	$⊢ φ \to (x \in ℝ^{+} ⟼ 2 2 C + (\sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{x}) (\frac{2 C}{\sqrt{x}})) \in 𝑂 (1)$
215	188 214	eqeltrd	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) (\frac{2 C}{\sqrt{x}})) \in 𝑂 (1)$
216	164 174	remulcld	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) (\frac{2 C}{\sqrt{x}}) \in ℝ$
217	15 153	fsumcl	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) \in ℂ$
218	13 217	fsumcl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} \sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) \in ℂ$
219	218	abscld	$⊢ (φ \land x \in ℝ^{+}) \to \|\sum_{d = 1}^{⌊x⌋} \sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})\| \in ℝ$
220	216	recnd	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) (\frac{2 C}{\sqrt{x}}) \in ℂ$
221	220	abscld	$⊢ (φ \land x \in ℝ^{+}) \to \|\sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) (\frac{2 C}{\sqrt{x}})\| \in ℝ$
222	217	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|\sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})\| \in ℝ$
223	13 222	fsumrecl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} \|\sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})\| \in ℝ$
224	13 217	fsumabs	$⊢ (φ \land x \in ℝ^{+}) \to \|\sum_{d = 1}^{⌊x⌋} \sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})\| \leq \sum_{d = 1}^{⌊x⌋} \|\sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})\|$
225	174	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{2 C}{\sqrt{x}} \in ℝ$
226	163 225	remulcld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (\frac{1}{\sqrt{d}}) (\frac{2 C}{\sqrt{x}}) \in ℝ$
227	130 144	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 ℂ$
228	15 227	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 ℂ$
229	228	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 ℝ$
230	1 2 3 4 5 6 7 8 9 10 11 12	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}}$
231	229 225 147 230	lediv1dd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{\|\sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{X (L (m))}{\sqrt{m}})\|}{\sqrt{d}} \leq \frac{\frac{2 C}{\sqrt{x}}}{\sqrt{d}}$
232	147	rpcnd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \sqrt{d} \in ℂ$
233	147	rpne0d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \sqrt{d} \neq 0$
234	228 232 233	absdivd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|\frac{\sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{X (L (m))}{\sqrt{m}})}{\sqrt{d}}\| = \frac{\|\sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{X (L (m))}{\sqrt{m}})\|}{\|\sqrt{d}\|}$
235	15 232 227 233	fsumdivc	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{\sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{X (L (m))}{\sqrt{m}})}{\sqrt{d}} = \sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})$
236	235	fveq2d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|\frac{\sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{X (L (m))}{\sqrt{m}})}{\sqrt{d}}\| = \|\sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})\|$
237	147	rprege0d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (\sqrt{d} \in ℝ \land 0 \leq \sqrt{d})$
238		absid	$⊢ (\sqrt{d} \in ℝ \land 0 \leq \sqrt{d}) \to \|\sqrt{d}\| = \sqrt{d}$
239	237 238	syl	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|\sqrt{d}\| = \sqrt{d}$
240	239	oveq2d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{\|\sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{X (L (m))}{\sqrt{m}})\|}{\|\sqrt{d}\|} = \frac{\|\sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{X (L (m))}{\sqrt{m}})\|}{\sqrt{d}}$
241	234 236 240	3eqtr3rd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{\|\sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{X (L (m))}{\sqrt{m}})\|}{\sqrt{d}} = \|\sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})\|$
242	175	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{2 C}{\sqrt{x}} \in ℂ$
243	242 232 233	divrec2d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{\frac{2 C}{\sqrt{x}}}{\sqrt{d}} = (\frac{1}{\sqrt{d}}) (\frac{2 C}{\sqrt{x}})$
244	231 241 243	3brtr3d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|\sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})\| \leq (\frac{1}{\sqrt{d}}) (\frac{2 C}{\sqrt{x}})$
245	13 222 226 244	fsumle	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} \|\sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})\| \leq \sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) (\frac{2 C}{\sqrt{x}})$
246	163	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{1}{\sqrt{d}} \in ℂ$
247	13 175 246	fsummulc1	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) (\frac{2 C}{\sqrt{x}}) = \sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) (\frac{2 C}{\sqrt{x}})$
248	245 247	breqtrrd	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} \|\sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})\| \leq \sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) (\frac{2 C}{\sqrt{x}})$
249	219 223 216 224 248	letrd	$⊢ (φ \land x \in ℝ^{+}) \to \|\sum_{d = 1}^{⌊x⌋} \sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})\| \leq \sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) (\frac{2 C}{\sqrt{x}})$
250	216	leabsd	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) (\frac{2 C}{\sqrt{x}}) \leq \|\sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) (\frac{2 C}{\sqrt{x}})\|$
251	219 216 221 249 250	letrd	$⊢ (φ \land x \in ℝ^{+}) \to \|\sum_{d = 1}^{⌊x⌋} \sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})\| \leq \|\sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) (\frac{2 C}{\sqrt{x}})\|$
252	251	adantrr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{d = 1}^{⌊x⌋} \sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})\| \leq \|\sum_{d = 1}^{⌊x⌋} (\frac{1}{\sqrt{d}}) (\frac{2 C}{\sqrt{x}})\|$
253	157 215 216 218 252	o1le	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} \sum_{m = ⌊x⌋ + 1}^{⌊\frac{x^{2}}{d}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})) \in 𝑂 (1)$
254	156 253	eqeltrrd	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{m = ⌊x⌋ + 1}^{⌊x^{2}⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem dchrisum0lem1

Proof