dchrisum0lem2a

	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$
Assertion	dchrisum0lem2a	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) H (\frac{x^{2}}{m})) \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		fzfid	$⊢ (φ \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \in Fin$
16		simpl	$⊢ (φ \land x \in ℝ^{+}) \to φ$
17		elfznn	$⊢ m \in (1 \dots ⌊x⌋) \to m \in ℕ$
18	7	ssrab3	$⊢ W \subseteq D ∖ \{\underset{˙}{1}\}$
19	18 8	sselid	$⊢ φ \to X \in (D ∖ \{\underset{˙}{1}\})$
20	19	eldifad	$⊢ φ \to X \in D$
21	20	adantr	$⊢ (φ \land m \in ℕ) \to X \in D$
22		nnz	$⊢ m \in ℕ \to m \in ℤ$
23	22	adantl	$⊢ (φ \land m \in ℕ) \to m \in ℤ$
24	4 1 5 2 21 23	dchrzrhcl	$⊢ (φ \land m \in ℕ) \to X (L (m)) \in ℂ$
25		nnrp	$⊢ m \in ℕ \to m \in ℝ^{+}$
26	25	adantl	$⊢ (φ \land m \in ℕ) \to m \in ℝ^{+}$
27	26	rpsqrtcld	$⊢ (φ \land m \in ℕ) \to \sqrt{m} \in ℝ^{+}$
28	27	rpcnd	$⊢ (φ \land m \in ℕ) \to \sqrt{m} \in ℂ$
29	27	rpne0d	$⊢ (φ \land m \in ℕ) \to \sqrt{m} \neq 0$
30	24 28 29	divcld	$⊢ (φ \land m \in ℕ) \to \frac{X (L (m))}{\sqrt{m}} \in ℂ$
31	16 17 30	syl2an	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \frac{X (L (m))}{\sqrt{m}} \in ℂ$
32	15 31	fsumcl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) \in ℂ$
33		rlimcl	$⊢ H \underset{ℝ}{⇝} U \to U \in ℂ$
34	14 33	syl	$⊢ φ \to U \in ℂ$
35	34	adantr	$⊢ (φ \land x \in ℝ^{+}) \to U \in ℂ$
36		0xr	$⊢ 0 \in ℝ^{*}$
37		0lt1	$⊢ 0 < 1$
38		df-ioo	$⊢ (.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z < y)\})$
39		df-ico	$⊢ [.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\})$
40		xrltletr	$⊢ (0 \in ℝ^{} \land 1 \in ℝ^{} \land w \in ℝ^{*}) \to ((0 < 1 \land 1 \leq w) \to 0 < w)$
41	38 39 40	ixxss1	$⊢ (0 \in ℝ^{*} \land 0 < 1) \to [1, +∞) \subseteq (0, +∞)$
42	36 37 41	mp2an	$⊢ [1, +∞) \subseteq (0, +∞)$
43		ioorp	$⊢ (0, +∞) = ℝ^{+}$
44	42 43	sseqtri	$⊢ [1, +∞) \subseteq ℝ^{+}$
45		resmpt	$⊢ [1, +∞) \subseteq ℝ^{+} \to {(x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}})) ↾}_{[1, +∞)} = (x \in [1, +∞) ⟼ \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}))$
46	44 45	ax-mp	$⊢ {(x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}})) ↾}_{[1, +∞)} = (x \in [1, +∞) ⟼ \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}))$
47	44	sseli	$⊢ x \in [1, +∞) \to x \in ℝ^{+}$
48	17	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to m \in ℕ$
49		2fveq3	$⊢ a = m \to X (L (a)) = X (L (m))$
50		fveq2	$⊢ a = m \to \sqrt{a} = \sqrt{m}$
51	49 50	oveq12d	$⊢ a = m \to \frac{X (L (a))}{\sqrt{a}} = \frac{X (L (m))}{\sqrt{m}}$
52		ovex	$⊢ \frac{X (L (a))}{\sqrt{a}} \in V$
53	51 9 52	fvmpt3i	$⊢ m \in ℕ \to F (m) = \frac{X (L (m))}{\sqrt{m}}$
54	48 53	syl	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to F (m) = \frac{X (L (m))}{\sqrt{m}}$
55	47 54	sylanl2	$⊢ ((φ \land x \in [1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to F (m) = \frac{X (L (m))}{\sqrt{m}}$
56		1re	$⊢ 1 \in ℝ$
57		elicopnf	$⊢ 1 \in ℝ \to (x \in [1, +∞) \leftrightarrow (x \in ℝ \land 1 \leq x))$
58	56 57	ax-mp	$⊢ x \in [1, +∞) \leftrightarrow (x \in ℝ \land 1 \leq x)$
59		flge1nn	$⊢ (x \in ℝ \land 1 \leq x) \to ⌊x⌋ \in ℕ$
60	58 59	sylbi	$⊢ x \in [1, +∞) \to ⌊x⌋ \in ℕ$
61	60	adantl	$⊢ (φ \land x \in [1, +∞)) \to ⌊x⌋ \in ℕ$
62		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
63	61 62	eleqtrdi	$⊢ (φ \land x \in [1, +∞)) \to ⌊x⌋ \in ℤ_{\geq 1}$
64	47 31	sylanl2	$⊢ ((φ \land x \in [1, +∞)) \land m \in (1 \dots ⌊x⌋)) \to \frac{X (L (m))}{\sqrt{m}} \in ℂ$
65	55 63 64	fsumser	$⊢ (φ \land x \in [1, +∞)) \to \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) = seq 1 (+ F) (⌊x⌋)$
66	65	mpteq2dva	$⊢ φ \to (x \in [1, +∞) ⟼ \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}})) = (x \in [1, +∞) ⟼ seq 1 (+ F) (⌊x⌋))$
67	46 66	eqtrid	$⊢ φ \to {(x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}})) ↾}_{[1, +∞)} = (x \in [1, +∞) ⟼ seq 1 (+ F) (⌊x⌋))$
68		fveq2	$⊢ m = ⌊x⌋ \to seq 1 (+ F) (m) = seq 1 (+ F) (⌊x⌋)$
69		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
70	69	a1i	$⊢ φ \to ℝ^{+} \subseteq ℝ$
71	44 70	sstrid	$⊢ φ \to [1, +∞) \subseteq ℝ$
72		1zzd	$⊢ φ \to 1 \in ℤ$
73	51	cbvmptv	$⊢ (a \in ℕ ⟼ \frac{X (L (a))}{\sqrt{a}}) = (m \in ℕ ⟼ \frac{X (L (m))}{\sqrt{m}})$
74	9 73	eqtri	$⊢ F = (m \in ℕ ⟼ \frac{X (L (m))}{\sqrt{m}})$
75	30 74	fmptd	$⊢ φ \to F : ℕ ⟶ ℂ$
76	75	ffvelrnda	$⊢ (φ \land m \in ℕ) \to F (m) \in ℂ$
77	62 72 76	serf	$⊢ φ \to seq 1 (+ F) : ℕ ⟶ ℂ$
78	77	feqmptd	$⊢ φ \to seq 1 (+ F) = (m \in ℕ ⟼ seq 1 (+ F) (m))$
79	78 11	eqbrtrrd	$⊢ φ \to (m \in ℕ ⟼ seq 1 (+ F) (m)) ⇝ S$
80	77	ffvelrnda	$⊢ (φ \land m \in ℕ) \to seq 1 (+ F) (m) \in ℂ$
81	58	simprbi	$⊢ x \in [1, +∞) \to 1 \leq x$
82	81	adantl	$⊢ (φ \land x \in [1, +∞)) \to 1 \leq x$
83	62 68 71 72 79 80 82	climrlim2	$⊢ φ \to (x \in [1, +∞) ⟼ seq 1 (+ F) (⌊x⌋)) \underset{ℝ}{⇝} S$
84		rlimo1	$⊢ (x \in [1, +∞) ⟼ seq 1 (+ F) (⌊x⌋)) \underset{ℝ}{⇝} S \to (x \in [1, +∞) ⟼ seq 1 (+ F) (⌊x⌋)) \in 𝑂 (1)$
85	83 84	syl	$⊢ φ \to (x \in [1, +∞) ⟼ seq 1 (+ F) (⌊x⌋)) \in 𝑂 (1)$
86	67 85	eqeltrd	$⊢ φ \to {(x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}})) ↾}_{[1, +∞)} \in 𝑂 (1)$
87	32	fmpttd	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}})) : ℝ^{+} ⟶ ℂ$
88		1red	$⊢ φ \to 1 \in ℝ$
89	87 70 88	o1resb	$⊢ φ \to ((x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}})) \in 𝑂 (1) \leftrightarrow {(x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}})) ↾}_{[1, +∞)} \in 𝑂 (1))$
90	86 89	mpbird	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}})) \in 𝑂 (1)$
91		o1const	$⊢ (ℝ^{+} \subseteq ℝ \land U \in ℂ) \to (x \in ℝ^{+} ⟼ U) \in 𝑂 (1)$
92	69 34 91	sylancr	$⊢ φ \to (x \in ℝ^{+} ⟼ U) \in 𝑂 (1)$
93	32 35 90 92	o1mul2	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) U) \in 𝑂 (1)$
94		simpr	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ^{+}$
95		2z	$⊢ 2 \in ℤ$
96		rpexpcl	$⊢ (x \in ℝ^{+} \land 2 \in ℤ) \to x^{2} \in ℝ^{+}$
97	94 95 96	sylancl	$⊢ (φ \land x \in ℝ^{+}) \to x^{2} \in ℝ^{+}$
98	17	nnrpd	$⊢ m \in (1 \dots ⌊x⌋) \to m \in ℝ^{+}$
99		rpdivcl	$⊢ (x^{2} \in ℝ^{+} \land m \in ℝ^{+}) \to \frac{x^{2}}{m} \in ℝ^{+}$
100	97 98 99	syl2an	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \frac{x^{2}}{m} \in ℝ^{+}$
101	13	divsqrsumf	$⊢ H : ℝ^{+} ⟶ ℝ$
102	101	ffvelrni	$⊢ \frac{x^{2}}{m} \in ℝ^{+} \to H (\frac{x^{2}}{m}) \in ℝ$
103	100 102	syl	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to H (\frac{x^{2}}{m}) \in ℝ$
104	103	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to H (\frac{x^{2}}{m}) \in ℂ$
105	31 104	mulcld	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to (\frac{X (L (m))}{\sqrt{m}}) H (\frac{x^{2}}{m}) \in ℂ$
106	15 105	fsumcl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) H (\frac{x^{2}}{m}) \in ℂ$
107	32 35	mulcld	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) U \in ℂ$
108	14	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to H \underset{ℝ}{⇝} U$
109	108 33	syl	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to U \in ℂ$
110	31 109	mulcld	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to (\frac{X (L (m))}{\sqrt{m}}) U \in ℂ$
111	15 105 110	fsumsub	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x⌋} ((\frac{X (L (m))}{\sqrt{m}}) H (\frac{x^{2}}{m}) - (\frac{X (L (m))}{\sqrt{m}}) U) = \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) H (\frac{x^{2}}{m}) - \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) U$
112	31 104 109	subdid	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to (\frac{X (L (m))}{\sqrt{m}}) (H (\frac{x^{2}}{m}) - U) = (\frac{X (L (m))}{\sqrt{m}}) H (\frac{x^{2}}{m}) - (\frac{X (L (m))}{\sqrt{m}}) U$
113	112	sumeq2dv	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) (H (\frac{x^{2}}{m}) - U) = \sum_{m = 1}^{⌊x⌋} ((\frac{X (L (m))}{\sqrt{m}}) H (\frac{x^{2}}{m}) - (\frac{X (L (m))}{\sqrt{m}}) U)$
114	15 35 31	fsummulc1	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) U = \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) U$
115	114	oveq2d	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) H (\frac{x^{2}}{m}) - \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) U = \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) H (\frac{x^{2}}{m}) - \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) U$
116	111 113 115	3eqtr4d	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) (H (\frac{x^{2}}{m}) - U) = \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) H (\frac{x^{2}}{m}) - \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) U$
117	116	mpteq2dva	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) (H (\frac{x^{2}}{m}) - U)) = (x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) H (\frac{x^{2}}{m}) - \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) U)$
118	104 109	subcld	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to H (\frac{x^{2}}{m}) - U \in ℂ$
119	31 118	mulcld	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to (\frac{X (L (m))}{\sqrt{m}}) (H (\frac{x^{2}}{m}) - U) \in ℂ$
120	15 119	fsumcl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) (H (\frac{x^{2}}{m}) - U) \in ℂ$
121	120	abscld	$⊢ (φ \land x \in ℝ^{+}) \to \|\sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) (H (\frac{x^{2}}{m}) - U)\| \in ℝ$
122	119	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \|(\frac{X (L (m))}{\sqrt{m}}) (H (\frac{x^{2}}{m}) - U)\| \in ℝ$
123	15 122	fsumrecl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x⌋} \|(\frac{X (L (m))}{\sqrt{m}}) (H (\frac{x^{2}}{m}) - U)\| \in ℝ$
124		1red	$⊢ (φ \land x \in ℝ^{+}) \to 1 \in ℝ$
125	15 119	fsumabs	$⊢ (φ \land x \in ℝ^{+}) \to \|\sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) (H (\frac{x^{2}}{m}) - U)\| \leq \sum_{m = 1}^{⌊x⌋} \|(\frac{X (L (m))}{\sqrt{m}}) (H (\frac{x^{2}}{m}) - U)\|$
126		rprege0	$⊢ x \in ℝ^{+} \to (x \in ℝ \land 0 \leq x)$
127	126	adantl	$⊢ (φ \land x \in ℝ^{+}) \to (x \in ℝ \land 0 \leq x)$
128	127	simpld	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ$
129		reflcl	$⊢ x \in ℝ \to ⌊x⌋ \in ℝ$
130	128 129	syl	$⊢ (φ \land x \in ℝ^{+}) \to ⌊x⌋ \in ℝ$
131	130 94	rerpdivcld	$⊢ (φ \land x \in ℝ^{+}) \to \frac{⌊x⌋}{x} \in ℝ$
132		simplr	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to x \in ℝ^{+}$
133	132	rprecred	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \frac{1}{x} \in ℝ$
134	31	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \|\frac{X (L (m))}{\sqrt{m}}\| \in ℝ$
135	98	rpsqrtcld	$⊢ m \in (1 \dots ⌊x⌋) \to \sqrt{m} \in ℝ^{+}$
136	135	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \sqrt{m} \in ℝ^{+}$
137	136	rprecred	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \frac{1}{\sqrt{m}} \in ℝ$
138	118	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \|H (\frac{x^{2}}{m}) - U\| \in ℝ$
139	136 132	rpdivcld	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \frac{\sqrt{m}}{x} \in ℝ^{+}$
140	69 139	sselid	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \frac{\sqrt{m}}{x} \in ℝ$
141	31	absge0d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to 0 \leq \|\frac{X (L (m))}{\sqrt{m}}\|$
142	118	absge0d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to 0 \leq \|H (\frac{x^{2}}{m}) - U\|$
143	16 17 24	syl2an	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to X (L (m)) \in ℂ$
144	136	rpcnd	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \sqrt{m} \in ℂ$
145	136	rpne0d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \sqrt{m} \neq 0$
146	143 144 145	absdivd	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \|\frac{X (L (m))}{\sqrt{m}}\| = \frac{\|X (L (m))\|}{\|\sqrt{m}\|}$
147	136	rprege0d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to (\sqrt{m} \in ℝ \land 0 \leq \sqrt{m})$
148		absid	$⊢ (\sqrt{m} \in ℝ \land 0 \leq \sqrt{m}) \to \|\sqrt{m}\| = \sqrt{m}$
149	147 148	syl	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \|\sqrt{m}\| = \sqrt{m}$
150	149	oveq2d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \frac{\|X (L (m))\|}{\|\sqrt{m}\|} = \frac{\|X (L (m))\|}{\sqrt{m}}$
151	146 150	eqtrd	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \|\frac{X (L (m))}{\sqrt{m}}\| = \frac{\|X (L (m))\|}{\sqrt{m}}$
152	143	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \|X (L (m))\| \in ℝ$
153		1red	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to 1 \in ℝ$
154		eqid	$⊢ {Base}_{Z} = {Base}_{Z}$
155	20	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to X \in D$
156	3	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
157	1 154 2	znzrhfo	$⊢ N \in ℕ_{0} \to L : ℤ \underset{onto}{⟶} {Base}_{Z}$
158		fof	$⊢ L : ℤ \underset{onto}{⟶} {Base}_{Z} \to L : ℤ ⟶ {Base}_{Z}$
159	156 157 158	3syl	$⊢ φ \to L : ℤ ⟶ {Base}_{Z}$
160	159	adantr	$⊢ (φ \land x \in ℝ^{+}) \to L : ℤ ⟶ {Base}_{Z}$
161		elfzelz	$⊢ m \in (1 \dots ⌊x⌋) \to m \in ℤ$
162		ffvelrn	$⊢ (L : ℤ ⟶ {Base}_{Z} \land m \in ℤ) \to L (m) \in {Base}_{Z}$
163	160 161 162	syl2an	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to L (m) \in {Base}_{Z}$
164	4 5 1 154 155 163	dchrabs2	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \|X (L (m))\| \leq 1$
165	152 153 136 164	lediv1dd	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \frac{\|X (L (m))\|}{\sqrt{m}} \leq \frac{1}{\sqrt{m}}$
166	151 165	eqbrtrd	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \|\frac{X (L (m))}{\sqrt{m}}\| \leq \frac{1}{\sqrt{m}}$
167	13 108	divsqrtsum2	$⊢ (((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \land \frac{x^{2}}{m} \in ℝ^{+}) \to \|H (\frac{x^{2}}{m}) - U\| \leq \frac{1}{\sqrt{\frac{x^{2}}{m}}}$
168	100 167	mpdan	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \|H (\frac{x^{2}}{m}) - U\| \leq \frac{1}{\sqrt{\frac{x^{2}}{m}}}$
169	97	rprege0d	$⊢ (φ \land x \in ℝ^{+}) \to (x^{2} \in ℝ \land 0 \leq x^{2})$
170		sqrtdiv	$⊢ ((x^{2} \in ℝ \land 0 \leq x^{2}) \land m \in ℝ^{+}) \to \sqrt{\frac{x^{2}}{m}} = \frac{\sqrt{x^{2}}}{\sqrt{m}}$
171	169 98 170	syl2an	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \sqrt{\frac{x^{2}}{m}} = \frac{\sqrt{x^{2}}}{\sqrt{m}}$
172	126	ad2antlr	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to (x \in ℝ \land 0 \leq x)$
173		sqrtsq	$⊢ (x \in ℝ \land 0 \leq x) \to \sqrt{x^{2}} = x$
174	172 173	syl	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \sqrt{x^{2}} = x$
175	174	oveq1d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \frac{\sqrt{x^{2}}}{\sqrt{m}} = \frac{x}{\sqrt{m}}$
176	171 175	eqtrd	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \sqrt{\frac{x^{2}}{m}} = \frac{x}{\sqrt{m}}$
177	176	oveq2d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \frac{1}{\sqrt{\frac{x^{2}}{m}}} = \frac{1}{\frac{x}{\sqrt{m}}}$
178		rpcnne0	$⊢ x \in ℝ^{+} \to (x \in ℂ \land x \neq 0)$
179	178	ad2antlr	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to (x \in ℂ \land x \neq 0)$
180	136	rpcnne0d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to (\sqrt{m} \in ℂ \land \sqrt{m} \neq 0)$
181		recdiv	$⊢ ((x \in ℂ \land x \neq 0) \land (\sqrt{m} \in ℂ \land \sqrt{m} \neq 0)) \to \frac{1}{\frac{x}{\sqrt{m}}} = \frac{\sqrt{m}}{x}$
182	179 180 181	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \frac{1}{\frac{x}{\sqrt{m}}} = \frac{\sqrt{m}}{x}$
183	177 182	eqtrd	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \frac{1}{\sqrt{\frac{x^{2}}{m}}} = \frac{\sqrt{m}}{x}$
184	168 183	breqtrd	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \|H (\frac{x^{2}}{m}) - U\| \leq \frac{\sqrt{m}}{x}$
185	134 137 138 140 141 142 166 184	lemul12ad	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \|\frac{X (L (m))}{\sqrt{m}}\| \|H (\frac{x^{2}}{m}) - U\| \leq (\frac{1}{\sqrt{m}}) (\frac{\sqrt{m}}{x})$
186	31 118	absmuld	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \|(\frac{X (L (m))}{\sqrt{m}}) (H (\frac{x^{2}}{m}) - U)\| = \|\frac{X (L (m))}{\sqrt{m}}\| \|H (\frac{x^{2}}{m}) - U\|$
187		1cnd	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to 1 \in ℂ$
188		dmdcan	$⊢ ((\sqrt{m} \in ℂ \land \sqrt{m} \neq 0) \land (x \in ℂ \land x \neq 0) \land 1 \in ℂ) \to (\frac{\sqrt{m}}{x}) (\frac{1}{\sqrt{m}}) = \frac{1}{x}$
189	180 179 187 188	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to (\frac{\sqrt{m}}{x}) (\frac{1}{\sqrt{m}}) = \frac{1}{x}$
190	139	rpcnd	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \frac{\sqrt{m}}{x} \in ℂ$
191		reccl	$⊢ (\sqrt{m} \in ℂ \land \sqrt{m} \neq 0) \to \frac{1}{\sqrt{m}} \in ℂ$
192	180 191	syl	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \frac{1}{\sqrt{m}} \in ℂ$
193	190 192	mulcomd	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to (\frac{\sqrt{m}}{x}) (\frac{1}{\sqrt{m}}) = (\frac{1}{\sqrt{m}}) (\frac{\sqrt{m}}{x})$
194	189 193	eqtr3d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \frac{1}{x} = (\frac{1}{\sqrt{m}}) (\frac{\sqrt{m}}{x})$
195	185 186 194	3brtr4d	$⊢ ((φ \land x \in ℝ^{+}) \land m \in (1 \dots ⌊x⌋)) \to \|(\frac{X (L (m))}{\sqrt{m}}) (H (\frac{x^{2}}{m}) - U)\| \leq \frac{1}{x}$
196	15 122 133 195	fsumle	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x⌋} \|(\frac{X (L (m))}{\sqrt{m}}) (H (\frac{x^{2}}{m}) - U)\| \leq \sum_{m = 1}^{⌊x⌋} (\frac{1}{x})$
197		flge0nn0	$⊢ (x \in ℝ \land 0 \leq x) \to ⌊x⌋ \in ℕ_{0}$
198		hashfz1	$⊢ ⌊x⌋ \in ℕ_{0} \to \|(1 \dots ⌊x⌋)\| = ⌊x⌋$
199	127 197 198	3syl	$⊢ (φ \land x \in ℝ^{+}) \to \|(1 \dots ⌊x⌋)\| = ⌊x⌋$
200	199	oveq1d	$⊢ (φ \land x \in ℝ^{+}) \to \|(1 \dots ⌊x⌋)\| (\frac{1}{x}) = ⌊x⌋ (\frac{1}{x})$
201	94	rpreccld	$⊢ (φ \land x \in ℝ^{+}) \to \frac{1}{x} \in ℝ^{+}$
202	201	rpcnd	$⊢ (φ \land x \in ℝ^{+}) \to \frac{1}{x} \in ℂ$
203		fsumconst	$⊢ ((1 \dots ⌊x⌋) \in Fin \land \frac{1}{x} \in ℂ) \to \sum_{m = 1}^{⌊x⌋} (\frac{1}{x}) = \|(1 \dots ⌊x⌋)\| (\frac{1}{x})$
204	15 202 203	syl2anc	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x⌋} (\frac{1}{x}) = \|(1 \dots ⌊x⌋)\| (\frac{1}{x})$
205	130	recnd	$⊢ (φ \land x \in ℝ^{+}) \to ⌊x⌋ \in ℂ$
206	178	adantl	$⊢ (φ \land x \in ℝ^{+}) \to (x \in ℂ \land x \neq 0)$
207	206	simpld	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℂ$
208	206	simprd	$⊢ (φ \land x \in ℝ^{+}) \to x \neq 0$
209	205 207 208	divrecd	$⊢ (φ \land x \in ℝ^{+}) \to \frac{⌊x⌋}{x} = ⌊x⌋ (\frac{1}{x})$
210	200 204 209	3eqtr4d	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x⌋} (\frac{1}{x}) = \frac{⌊x⌋}{x}$
211	196 210	breqtrd	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x⌋} \|(\frac{X (L (m))}{\sqrt{m}}) (H (\frac{x^{2}}{m}) - U)\| \leq \frac{⌊x⌋}{x}$
212		flle	$⊢ x \in ℝ \to ⌊x⌋ \leq x$
213	128 212	syl	$⊢ (φ \land x \in ℝ^{+}) \to ⌊x⌋ \leq x$
214	128	recnd	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℂ$
215	214	mulid1d	$⊢ (φ \land x \in ℝ^{+}) \to x \cdot 1 = x$
216	213 215	breqtrrd	$⊢ (φ \land x \in ℝ^{+}) \to ⌊x⌋ \leq x \cdot 1$
217		rpregt0	$⊢ x \in ℝ^{+} \to (x \in ℝ \land 0 < x)$
218	217	adantl	$⊢ (φ \land x \in ℝ^{+}) \to (x \in ℝ \land 0 < x)$
219		ledivmul	$⊢ (⌊x⌋ \in ℝ \land 1 \in ℝ \land (x \in ℝ \land 0 < x)) \to (\frac{⌊x⌋}{x} \leq 1 \leftrightarrow ⌊x⌋ \leq x \cdot 1)$
220	130 124 218 219	syl3anc	$⊢ (φ \land x \in ℝ^{+}) \to (\frac{⌊x⌋}{x} \leq 1 \leftrightarrow ⌊x⌋ \leq x \cdot 1)$
221	216 220	mpbird	$⊢ (φ \land x \in ℝ^{+}) \to \frac{⌊x⌋}{x} \leq 1$
222	123 131 124 211 221	letrd	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{m = 1}^{⌊x⌋} \|(\frac{X (L (m))}{\sqrt{m}}) (H (\frac{x^{2}}{m}) - U)\| \leq 1$
223	121 123 124 125 222	letrd	$⊢ (φ \land x \in ℝ^{+}) \to \|\sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) (H (\frac{x^{2}}{m}) - U)\| \leq 1$
224	223	adantrr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) (H (\frac{x^{2}}{m}) - U)\| \leq 1$
225	70 120 88 88 224	elo1d	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) (H (\frac{x^{2}}{m}) - U)) \in 𝑂 (1)$
226	117 225	eqeltrrd	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) H (\frac{x^{2}}{m}) - \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) U) \in 𝑂 (1)$
227	106 107 226	o1dif	$⊢ φ \to ((x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) H (\frac{x^{2}}{m})) \in 𝑂 (1) \leftrightarrow (x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) U) \in 𝑂 (1))$
228	93 227	mpbird	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{m = 1}^{⌊x⌋} (\frac{X (L (m))}{\sqrt{m}}) H (\frac{x^{2}}{m})) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem dchrisum0lem2a

Proof