dchrisum0lem2

	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}}$
	dchrisum0lem2.h	$⊢ H = (y \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊y⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{y})$
	dchrisum0lem2.u	$⊢ φ \to H \underset{ℝ}{⇝} U$
	dchrisum0lem2.k	$⊢ K = (a \in ℕ ⟼ \frac{X (L (a))}{a})$
	dchrisum0lem2.e	$⊢ φ \to E \in [0, +∞)$
	dchrisum0lem2.t	$⊢ φ \to seq 1 (+ K) ⇝ T$
	dchrisum0lem2.3	$⊢ φ \to \forall y \in [1, +∞) \|seq 1 (+ K) (⌊y⌋) - T\| \leq \frac{E}{y}$
Assertion	dchrisum0lem2	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} \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		dchrisum0lem2.h	$⊢ H = (y \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊y⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{y})$
14		dchrisum0lem2.u	$⊢ φ \to H \underset{ℝ}{⇝} U$
15		dchrisum0lem2.k	$⊢ K = (a \in ℕ ⟼ \frac{X (L (a))}{a})$
16		dchrisum0lem2.e	$⊢ φ \to E \in [0, +∞)$
17		dchrisum0lem2.t	$⊢ φ \to seq 1 (+ K) ⇝ T$
18		dchrisum0lem2.3	$⊢ φ \to \forall y \in [1, +∞) \|seq 1 (+ K) (⌊y⌋) - T\| \leq \frac{E}{y}$
19		2cnd	$⊢ (φ \land x \in ℝ^{+}) \to 2 \in ℂ$
20		rpcn	$⊢ x \in ℝ^{+} \to x \in ℂ$
21	20	adantl	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℂ$
22		fzfid	$⊢ (φ \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \in Fin$
23	7	ssrab3	$⊢ W \subseteq D ∖ \{\underset{˙}{1}\}$
24	23 8	sseldi	$⊢ φ \to X \in (D ∖ \{\underset{˙}{1}\})$
25	24	eldifad	$⊢ φ \to X \in D$
26	25	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to X \in D$
27		elfzelz	$⊢ m \in (1 \dots ⌊x⌋) \to m \in ℤ$
28	27	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to m \in ℤ$
29	4 1 5 2 26 28	dchrzrhcl	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to X (L (m)) \in ℂ$
30		elfznn	$⊢ m \in (1 \dots ⌊x⌋) \to m \in ℕ$
31	30	nnrpd	$⊢ m \in (1 \dots ⌊x⌋) \to m \in ℝ^{+}$
32	31	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to m \in ℝ^{+}$
33	32	rpcnd	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to m \in ℂ$
34	32	rpne0d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to m \neq 0$
35	29 33 34	divcld	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \frac{X (L (m))}{m} \in ℂ$
36	22 35	fsumcl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m}) \in ℂ$
37	21 36	mulcld	$⊢ (φ \land x \in ℝ^{+}) \to x \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m}) \in ℂ$
38		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
39		2cn	$⊢ 2 \in ℂ$
40		o1const	$⊢ (ℝ^{+} \subseteq ℝ \land 2 \in ℂ) \to (x \in ℝ^{+} ⟼ 2) \in 𝑂 (1)$
41	38 39 40	mp2an	$⊢ (x \in ℝ^{+} ⟼ 2) \in 𝑂 (1)$
42	41	a1i	$⊢ φ \to (x \in ℝ^{+} ⟼ 2) \in 𝑂 (1)$
43	38	a1i	$⊢ φ \to ℝ^{+} \subseteq ℝ$
44		1red	$⊢ φ \to 1 \in ℝ$
45		elrege0	$⊢ E \in [0, +∞) \leftrightarrow (E \in ℝ \land 0 \leq E)$
46	45	simplbi	$⊢ E \in [0, +∞) \to E \in ℝ$
47	16 46	syl	$⊢ φ \to E \in ℝ$
48	21 36	absmuld	$⊢ (φ \land x \in ℝ^{+}) \to \|x \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m})\| = \|x\| \|\sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m})\|$
49		rprege0	$⊢ x \in ℝ^{+} \to (x \in ℝ \land 0 \leq x)$
50	49	adantl	$⊢ (φ \land x \in ℝ^{+}) \to (x \in ℝ \land 0 \leq x)$
51		absid	$⊢ (x \in ℝ \land 0 \leq x) \to \|x\| = x$
52	50 51	syl	$⊢ (φ \land x \in ℝ^{+}) \to \|x\| = x$
53	52	oveq1d	$⊢ (φ \land x \in ℝ^{+}) \to \|x\| \|\sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m})\| = x \|\sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m})\|$
54	48 53	eqtrd	$⊢ (φ \land x \in ℝ^{+}) \to \|x \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m})\| = x \|\sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m})\|$
55	54	adantrr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|x \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m})\| = x \|\sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m})\|$
56	36	adantrr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m}) \in ℂ$
57	56	subid1d	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m}) - 0 = \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m})$
58	30	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to m \in ℕ$
59		2fveq3	$⊢ a = m \to X (L (a)) = X (L (m))$
60		id	$⊢ a = m \to a = m$
61	59 60	oveq12d	$⊢ a = m \to \frac{X (L (a))}{a} = \frac{X (L (m))}{m}$
62		ovex	$⊢ \frac{X (L (a))}{a} \in V$
63	61 15 62	fvmpt3i	$⊢ m \in ℕ \to K (m) = \frac{X (L (m))}{m}$
64	58 63	syl	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to K (m) = \frac{X (L (m))}{m}$
65	64	adantlrr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land m \in (1 \dots ⌊x⌋)) \to K (m) = \frac{X (L (m))}{m}$
66		rpregt0	$⊢ x \in ℝ^{+} \to (x \in ℝ \land 0 < x)$
67	66	ad2antrl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (x \in ℝ \land 0 < x)$
68	67	simpld	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to x \in ℝ$
69		simprr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 \leq x$
70		flge1nn	$⊢ (x \in ℝ \land 1 \leq x) \to ⌊x⌋ \in ℕ$
71	68 69 70	syl2anc	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to ⌊x⌋ \in ℕ$
72		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
73	71 72	eleqtrdi	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to ⌊x⌋ \in ℤ_{\geq 1}$
74	35	adantlrr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land m \in (1 \dots ⌊x⌋)) \to \frac{X (L (m))}{m} \in ℂ$
75	65 73 74	fsumser	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m}) = seq 1 (+ K) (⌊x⌋)$
76		eldifsni	$⊢ X \in (D ∖ \{\underset{˙}{1}\}) \to X \neq \underset{˙}{1}$
77	24 76	syl	$⊢ φ \to X \neq \underset{˙}{1}$
78	1 2 3 4 5 6 25 77 15 16 17 18 7	dchrvmaeq0	$⊢ φ \to (X \in W \leftrightarrow T = 0)$
79	8 78	mpbid	$⊢ φ \to T = 0$
80	79	adantr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to T = 0$
81	80	eqcomd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to 0 = T$
82	75 81	oveq12d	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m}) - 0 = seq 1 (+ K) (⌊x⌋) - T$
83	57 82	eqtr3d	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m}) = seq 1 (+ K) (⌊x⌋) - T$
84	83	fveq2d	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m})\| = \|seq 1 (+ K) (⌊x⌋) - T\|$
85		2fveq3	$⊢ y = x \to seq 1 (+ K) (⌊y⌋) = seq 1 (+ K) (⌊x⌋)$
86	85	fvoveq1d	$⊢ y = x \to \|seq 1 (+ K) (⌊y⌋) - T\| = \|seq 1 (+ K) (⌊x⌋) - T\|$
87		oveq2	$⊢ y = x \to \frac{E}{y} = \frac{E}{x}$
88	86 87	breq12d	$⊢ y = x \to (\|seq 1 (+ K) (⌊y⌋) - T\| \leq \frac{E}{y} \leftrightarrow \|seq 1 (+ K) (⌊x⌋) - T\| \leq \frac{E}{x})$
89	18	adantr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \forall y \in [1, +∞) \|seq 1 (+ K) (⌊y⌋) - T\| \leq \frac{E}{y}$
90		1re	$⊢ 1 \in ℝ$
91		elicopnf	$⊢ 1 \in ℝ \to (x \in [1, +∞) \leftrightarrow (x \in ℝ \land 1 \leq x))$
92	90 91	ax-mp	$⊢ x \in [1, +∞) \leftrightarrow (x \in ℝ \land 1 \leq x)$
93	68 69 92	sylanbrc	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to x \in [1, +∞)$
94	88 89 93	rspcdva	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|seq 1 (+ K) (⌊x⌋) - T\| \leq \frac{E}{x}$
95	84 94	eqbrtrd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m})\| \leq \frac{E}{x}$
96	56	abscld	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m})\| \in ℝ$
97	47	adantr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to E \in ℝ$
98		lemuldiv2	$⊢ (\|\sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m})\| \in ℝ \land E \in ℝ \land (x \in ℝ \land 0 < x)) \to (x \|\sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m})\| \leq E \leftrightarrow \|\sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m})\| \leq \frac{E}{x})$
99	96 97 67 98	syl3anc	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (x \|\sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m})\| \leq E \leftrightarrow \|\sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m})\| \leq \frac{E}{x})$
100	95 99	mpbird	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to x \|\sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m})\| \leq E$
101	55 100	eqbrtrd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|x \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m})\| \leq E$
102	43 37 44 47 101	elo1d	$⊢ φ \to (x \in ℝ^{+} ⟼ x \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m})) \in 𝑂 (1)$
103	19 37 42 102	o1mul2	$⊢ φ \to (x \in ℝ^{+} ⟼ 2 x \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m})) \in 𝑂 (1)$
104		fzfid	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to (1 \dots ⌊\frac{x^{2}}{m}⌋) \in Fin$
105	32	rpsqrtcld	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \sqrt{m} \in ℝ^{+}$
106	105	rpcnd	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \sqrt{m} \in ℂ$
107	105	rpne0d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \sqrt{m} \neq 0$
108	29 106 107	divcld	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \frac{X (L (m))}{\sqrt{m}} \in ℂ$
109	108	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to \frac{X (L (m))}{\sqrt{m}} \in ℂ$
110		elfznn	$⊢ d \in (1 \dots ⌊\frac{x^{2}}{m}⌋) \to d \in ℕ$
111	110	adantl	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to d \in ℕ$
112	111	nnrpd	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to d \in ℝ^{+}$
113	112	rpsqrtcld	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to \sqrt{d} \in ℝ^{+}$
114	113	rpcnd	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to \sqrt{d} \in ℂ$
115	113	rpne0d	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to \sqrt{d} \neq 0$
116	109 114 115	divcld	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to \frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}} \in ℂ$
117	104 116	fsumcl	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) \in ℂ$
118	22 117	fsumcl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) \in ℂ$
119		mulcl	$⊢ (2 \in ℂ \land x \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m}) \in ℂ) \to 2 x \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m}) \in ℂ$
120	39 37 119	sylancr	$⊢ (φ \land x \in ℝ^{+}) \to 2 x \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m}) \in ℂ$
121		2re	$⊢ 2 \in ℝ$
122		simpr	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ^{+}$
123		2z	$⊢ 2 \in ℤ$
124		rpexpcl	$⊢ (x \in ℝ^{+} \land 2 \in ℤ) \to x^{2} \in ℝ^{+}$
125	122 123 124	sylancl	$⊢ (φ \land x \in ℝ^{+}) \to x^{2} \in ℝ^{+}$
126		rpdivcl	$⊢ (x^{2} \in ℝ^{+} \land m \in ℝ^{+}) \to \frac{x^{2}}{m} \in ℝ^{+}$
127	125 31 126	syl2an	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \frac{x^{2}}{m} \in ℝ^{+}$
128	127	rpsqrtcld	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \sqrt{\frac{x^{2}}{m}} \in ℝ^{+}$
129	128	rpred	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \sqrt{\frac{x^{2}}{m}} \in ℝ$
130		remulcl	$⊢ (2 \in ℝ \land \sqrt{\frac{x^{2}}{m}} \in ℝ) \to 2 \sqrt{\frac{x^{2}}{m}} \in ℝ$
131	121 129 130	sylancr	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to 2 \sqrt{\frac{x^{2}}{m}} \in ℝ$
132	131	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to 2 \sqrt{\frac{x^{2}}{m}} \in ℂ$
133	108 132	mulcld	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to (\frac{X (L (m))}{\sqrt{m}}) 2 \sqrt{\frac{x^{2}}{m}} \in ℂ$
134	22 117 133	fsumsub	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x⌋} (\sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) - (\frac{X (L (m))}{\sqrt{m}}) 2 \sqrt{\frac{x^{2}}{m}}) = \sum_{m = 1}^{⌊x⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) - \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) 2 \sqrt{\frac{x^{2}}{m}}$
135	113	rpcnne0d	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to (\sqrt{d} \in ℂ \land \sqrt{d} \neq 0)$
136		reccl	$⊢ (\sqrt{d} \in ℂ \land \sqrt{d} \neq 0) \to \frac{1}{\sqrt{d}} \in ℂ$
137	135 136	syl	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to \frac{1}{\sqrt{d}} \in ℂ$
138	104 137	fsumcl	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{1}{\sqrt{d}}) \in ℂ$
139	108 138 132	subdid	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to (\frac{X (L (m))}{\sqrt{m}}) (\sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{\frac{x^{2}}{m}}) = (\frac{X (L (m))}{\sqrt{m}}) \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{1}{\sqrt{d}}) - (\frac{X (L (m))}{\sqrt{m}}) 2 \sqrt{\frac{x^{2}}{m}}$
140		fveq2	$⊢ y = \frac{x^{2}}{m} \to ⌊y⌋ = ⌊\frac{x^{2}}{m}⌋$
141	140	oveq2d	$⊢ y = \frac{x^{2}}{m} \to (1 \dots ⌊y⌋) = (1 \dots ⌊\frac{x^{2}}{m}⌋)$
142	141	sumeq1d	$⊢ y = \frac{x^{2}}{m} \to \sum_{d = 1}^{⌊y⌋} (\frac{1}{\sqrt{d}}) = \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{1}{\sqrt{d}})$
143		fveq2	$⊢ y = \frac{x^{2}}{m} \to \sqrt{y} = \sqrt{\frac{x^{2}}{m}}$
144	143	oveq2d	$⊢ y = \frac{x^{2}}{m} \to 2 \sqrt{y} = 2 \sqrt{\frac{x^{2}}{m}}$
145	142 144	oveq12d	$⊢ y = \frac{x^{2}}{m} \to \sum_{d = 1}^{⌊y⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{y} = \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{\frac{x^{2}}{m}}$
146		ovex	$⊢ \sum_{d = 1}^{⌊y⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{y} \in V$
147	145 13 146	fvmpt3i	$⊢ \frac{x^{2}}{m} \in ℝ^{+} \to H (\frac{x^{2}}{m}) = \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{\frac{x^{2}}{m}}$
148	127 147	syl	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to H (\frac{x^{2}}{m}) = \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{\frac{x^{2}}{m}}$
149	148	oveq2d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to (\frac{X (L (m))}{\sqrt{m}}) H (\frac{x^{2}}{m}) = (\frac{X (L (m))}{\sqrt{m}}) (\sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{1}{\sqrt{d}}) - 2 \sqrt{\frac{x^{2}}{m}})$
150	109 114 115	divrecd	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \land d \in (1 \dots ⌊\frac{x^{2}}{m}⌋)) \to \frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}} = (\frac{X (L (m))}{\sqrt{m}}) (\frac{1}{\sqrt{d}})$
151	150	sumeq2dv	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) = \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m}}) (\frac{1}{\sqrt{d}})$
152	104 108 137	fsummulc2	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to (\frac{X (L (m))}{\sqrt{m}}) \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{1}{\sqrt{d}}) = \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{X (L (m))}{\sqrt{m}}) (\frac{1}{\sqrt{d}})$
153	151 152	eqtr4d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) = (\frac{X (L (m))}{\sqrt{m}}) \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{1}{\sqrt{d}})$
154	153	oveq1d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) - (\frac{X (L (m))}{\sqrt{m}}) 2 \sqrt{\frac{x^{2}}{m}} = (\frac{X (L (m))}{\sqrt{m}}) \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{1}{\sqrt{d}}) - (\frac{X (L (m))}{\sqrt{m}}) 2 \sqrt{\frac{x^{2}}{m}}$
155	139 149 154	3eqtr4d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to (\frac{X (L (m))}{\sqrt{m}}) H (\frac{x^{2}}{m}) = \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) - (\frac{X (L (m))}{\sqrt{m}}) 2 \sqrt{\frac{x^{2}}{m}}$
156	155	sumeq2dv	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) H (\frac{x^{2}}{m}) = \sum_{m = 1}^{⌊x⌋} (\sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) - (\frac{X (L (m))}{\sqrt{m}}) 2 \sqrt{\frac{x^{2}}{m}})$
157		mulcl	$⊢ (2 \in ℂ \land x \in ℂ) \to 2 x \in ℂ$
158	39 21 157	sylancr	$⊢ (φ \land x \in ℝ^{+}) \to 2 x \in ℂ$
159	22 158 35	fsummulc2	$⊢ (φ \land x \in ℝ^{+}) \to 2 x \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m}) = \sum_{m = 1}^{⌊x⌋} 2 x (\frac{X (L (m))}{m})$
160	19 21 36	mulassd	$⊢ (φ \land x \in ℝ^{+}) \to 2 x \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m}) = 2 x \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m})$
161	158	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to 2 x \in ℂ$
162	161 108 106 107	div12d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to 2 x (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{m}}) = (\frac{X (L (m))}{\sqrt{m}}) (\frac{2 x}{\sqrt{m}})$
163	105	rpcnne0d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to (\sqrt{m} \in ℂ \land \sqrt{m} \neq 0)$
164		divdiv1	$⊢ (X (L (m)) \in ℂ \land (\sqrt{m} \in ℂ \land \sqrt{m} \neq 0) \land (\sqrt{m} \in ℂ \land \sqrt{m} \neq 0)) \to \frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{m}} = \frac{X (L (m))}{\sqrt{m} \sqrt{m}}$
165	29 163 163 164	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{m}} = \frac{X (L (m))}{\sqrt{m} \sqrt{m}}$
166	32	rprege0d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to (m \in ℝ \land 0 \leq m)$
167		remsqsqrt	$⊢ (m \in ℝ \land 0 \leq m) \to \sqrt{m} \sqrt{m} = m$
168	166 167	syl	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \sqrt{m} \sqrt{m} = m$
169	168	oveq2d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \frac{X (L (m))}{\sqrt{m} \sqrt{m}} = \frac{X (L (m))}{m}$
170	165 169	eqtr2d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \frac{X (L (m))}{m} = \frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{m}}$
171	170	oveq2d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to 2 x (\frac{X (L (m))}{m}) = 2 x (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{m}})$
172	125	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to x^{2} \in ℝ^{+}$
173	172	rprege0d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to (x^{2} \in ℝ \land 0 \leq x^{2})$
174		sqrtdiv	$⊢ ((x^{2} \in ℝ \land 0 \leq x^{2}) \land m \in ℝ^{+}) \to \sqrt{\frac{x^{2}}{m}} = \frac{\sqrt{x^{2}}}{\sqrt{m}}$
175	173 32 174	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \sqrt{\frac{x^{2}}{m}} = \frac{\sqrt{x^{2}}}{\sqrt{m}}$
176	49	ad2antlr	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to (x \in ℝ \land 0 \leq x)$
177		sqrtsq	$⊢ (x \in ℝ \land 0 \leq x) \to \sqrt{x^{2}} = x$
178	176 177	syl	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \sqrt{x^{2}} = x$
179	178	oveq1d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \frac{\sqrt{x^{2}}}{\sqrt{m}} = \frac{x}{\sqrt{m}}$
180	175 179	eqtrd	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \sqrt{\frac{x^{2}}{m}} = \frac{x}{\sqrt{m}}$
181	180	oveq2d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to 2 \sqrt{\frac{x^{2}}{m}} = 2 (\frac{x}{\sqrt{m}})$
182		2cnd	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to 2 \in ℂ$
183	21	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to x \in ℂ$
184		divass	$⊢ (2 \in ℂ \land x \in ℂ \land (\sqrt{m} \in ℂ \land \sqrt{m} \neq 0)) \to \frac{2 x}{\sqrt{m}} = 2 (\frac{x}{\sqrt{m}})$
185	182 183 163 184	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \frac{2 x}{\sqrt{m}} = 2 (\frac{x}{\sqrt{m}})$
186	181 185	eqtr4d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to 2 \sqrt{\frac{x^{2}}{m}} = \frac{2 x}{\sqrt{m}}$
187	186	oveq2d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to (\frac{X (L (m))}{\sqrt{m}}) 2 \sqrt{\frac{x^{2}}{m}} = (\frac{X (L (m))}{\sqrt{m}}) (\frac{2 x}{\sqrt{m}})$
188	162 171 187	3eqtr4d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to 2 x (\frac{X (L (m))}{m}) = (\frac{X (L (m))}{\sqrt{m}}) 2 \sqrt{\frac{x^{2}}{m}}$
189	188	sumeq2dv	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x⌋} 2 x (\frac{X (L (m))}{m}) = \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) 2 \sqrt{\frac{x^{2}}{m}}$
190	159 160 189	3eqtr3d	$⊢ (φ \land x \in ℝ^{+}) \to 2 x \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m}) = \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) 2 \sqrt{\frac{x^{2}}{m}}$
191	190	oveq2d	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) - 2 x \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m}) = \sum_{m = 1}^{⌊x⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) - \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) 2 \sqrt{\frac{x^{2}}{m}}$
192	134 156 191	3eqtr4d	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) H (\frac{x^{2}}{m}) = \sum_{m = 1}^{⌊x⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) - 2 x \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m})$
193	192	mpteq2dva	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) H (\frac{x^{2}}{m})) = (x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) - 2 x \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m}))$
194	1 2 3 4 5 6 7 8 9 10 11 12 13 14	dchrisum0lem2a	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) H (\frac{x^{2}}{m})) \in 𝑂 (1)$
195	193 194	eqeltrrd	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}}) - 2 x \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m})) \in 𝑂 (1)$
196	118 120 195	o1dif	$⊢ φ \to ((x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})) \in 𝑂 (1) \leftrightarrow (x \in ℝ^{+} ⟼ 2 x \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{m})) \in 𝑂 (1))$
197	103 196	mpbird	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} \sum_{d = 1}^{⌊\frac{x^{2}}{m}⌋} (\frac{\frac{X (L (m))}{\sqrt{m}}}{\sqrt{d}})) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem dchrisum0lem2

Proof