dchrvmasumlem2

	Ref	Expression
Hypotheses	rpvmasum.z	$⊢ Z = ℤ / N ℤ$
	rpvmasum.l	$⊢ L = ℤRHom (Z)$
	rpvmasum.a	$⊢ φ \to N \in ℕ$
	rpvmasum.g	$⊢ G = DChr (N)$
	rpvmasum.d	$⊢ D = {Base}_{G}$
	rpvmasum.1	$⊢ \underset{˙}{1} = 0_{G}$
	dchrisum.b	$⊢ φ \to X \in D$
	dchrisum.n1	$⊢ φ \to X \neq \underset{˙}{1}$
	dchrvmasum.f	$⊢ (φ \land m \in ℝ^{+}) \to F \in ℂ$
	dchrvmasum.g	$⊢ m = \frac{x}{d} \to F = K$
	dchrvmasum.c	$⊢ φ \to C \in [0, +∞)$
	dchrvmasum.t	$⊢ φ \to T \in ℂ$
	dchrvmasum.1	$⊢ (φ \land m \in [3, +∞)) \to \|F - T\| \leq C (\frac{\log m}{m})$
	dchrvmasum.r	$⊢ φ \to R \in ℝ$
	dchrvmasum.2	$⊢ φ \to \forall m \in [1, 3) \|F - T\| \leq R$
Assertion	dchrvmasumlem2	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} (\frac{\|K - T\|}{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		rpvmasum.g	$⊢ G = DChr (N)$
5		rpvmasum.d	$⊢ D = {Base}_{G}$
6		rpvmasum.1	$⊢ \underset{˙}{1} = 0_{G}$
7		dchrisum.b	$⊢ φ \to X \in D$
8		dchrisum.n1	$⊢ φ \to X \neq \underset{˙}{1}$
9		dchrvmasum.f	$⊢ (φ \land m \in ℝ^{+}) \to F \in ℂ$
10		dchrvmasum.g	$⊢ m = \frac{x}{d} \to F = K$
11		dchrvmasum.c	$⊢ φ \to C \in [0, +∞)$
12		dchrvmasum.t	$⊢ φ \to T \in ℂ$
13		dchrvmasum.1	$⊢ (φ \land m \in [3, +∞)) \to \|F - T\| \leq C (\frac{\log m}{m})$
14		dchrvmasum.r	$⊢ φ \to R \in ℝ$
15		dchrvmasum.2	$⊢ φ \to \forall m \in [1, 3) \|F - T\| \leq R$
16		1red	$⊢ φ \to 1 \in ℝ$
17		elrege0	$⊢ C \in [0, +∞) \leftrightarrow (C \in ℝ \land 0 \leq C)$
18	11 17	sylib	$⊢ φ \to (C \in ℝ \land 0 \leq C)$
19	18	simpld	$⊢ φ \to C \in ℝ$
20	19	adantr	$⊢ (φ \land x \in ℝ^{+}) \to C \in ℝ$
21		fzfid	$⊢ (φ \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \in Fin$
22		simpr	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ^{+}$
23		elfznn	$⊢ d \in (1 \dots ⌊x⌋) \to d \in ℕ$
24	23	nnrpd	$⊢ d \in (1 \dots ⌊x⌋) \to d \in ℝ^{+}$
25		rpdivcl	$⊢ (x \in ℝ^{+} \land d \in ℝ^{+}) \to \frac{x}{d} \in ℝ^{+}$
26	22 24 25	syl2an	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{x}{d} \in ℝ^{+}$
27	26	relogcld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{d}) \in ℝ$
28	22	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to x \in ℝ^{+}$
29	27 28	rerpdivcld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{\log (\frac{x}{d})}{x} \in ℝ$
30	21 29	fsumrecl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} (\frac{\log (\frac{x}{d})}{x}) \in ℝ$
31	20 30	remulcld	$⊢ (φ \land x \in ℝ^{+}) \to C \sum_{d = 1}^{⌊x⌋} (\frac{\log (\frac{x}{d})}{x}) \in ℝ$
32		3nn	$⊢ 3 \in ℕ$
33		nnrp	$⊢ 3 \in ℕ \to 3 \in ℝ^{+}$
34		relogcl	$⊢ 3 \in ℝ^{+} \to \log 3 \in ℝ$
35	32 33 34	mp2b	$⊢ \log 3 \in ℝ$
36		1re	$⊢ 1 \in ℝ$
37	35 36	readdcli	$⊢ \log 3 + 1 \in ℝ$
38		remulcl	$⊢ (R \in ℝ \land \log 3 + 1 \in ℝ) \to R (\log 3 + 1) \in ℝ$
39	14 37 38	sylancl	$⊢ φ \to R (\log 3 + 1) \in ℝ$
40	39	adantr	$⊢ (φ \land x \in ℝ^{+}) \to R (\log 3 + 1) \in ℝ$
41		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
42	19	recnd	$⊢ φ \to C \in ℂ$
43		o1const	$⊢ (ℝ^{+} \subseteq ℝ \land C \in ℂ) \to (x \in ℝ^{+} ⟼ C) \in 𝑂 (1)$
44	41 42 43	sylancr	$⊢ φ \to (x \in ℝ^{+} ⟼ C) \in 𝑂 (1)$
45		logfacrlim2	$⊢ (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} (\frac{\log (\frac{x}{d})}{x})) \underset{ℝ}{⇝} 1$
46		rlimo1	$⊢ (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} (\frac{\log (\frac{x}{d})}{x})) \underset{ℝ}{⇝} 1 \to (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} (\frac{\log (\frac{x}{d})}{x})) \in 𝑂 (1)$
47	45 46	mp1i	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} (\frac{\log (\frac{x}{d})}{x})) \in 𝑂 (1)$
48	20 30 44 47	o1mul2	$⊢ φ \to (x \in ℝ^{+} ⟼ C \sum_{d = 1}^{⌊x⌋} (\frac{\log (\frac{x}{d})}{x})) \in 𝑂 (1)$
49	39	recnd	$⊢ φ \to R (\log 3 + 1) \in ℂ$
50		o1const	$⊢ (ℝ^{+} \subseteq ℝ \land R (\log 3 + 1) \in ℂ) \to (x \in ℝ^{+} ⟼ R (\log 3 + 1)) \in 𝑂 (1)$
51	41 49 50	sylancr	$⊢ φ \to (x \in ℝ^{+} ⟼ R (\log 3 + 1)) \in 𝑂 (1)$
52	31 40 48 51	o1add2	$⊢ φ \to (x \in ℝ^{+} ⟼ C \sum_{d = 1}^{⌊x⌋} (\frac{\log (\frac{x}{d})}{x}) + R (\log 3 + 1)) \in 𝑂 (1)$
53	31 40	readdcld	$⊢ (φ \land x \in ℝ^{+}) \to C \sum_{d = 1}^{⌊x⌋} (\frac{\log (\frac{x}{d})}{x}) + R (\log 3 + 1) \in ℝ$
54	10	eleq1d	$⊢ m = \frac{x}{d} \to (F \in ℂ \leftrightarrow K \in ℂ)$
55	9	ralrimiva	$⊢ φ \to \forall m \in ℝ^{+} F \in ℂ$
56	55	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \forall m \in ℝ^{+} F \in ℂ$
57	54 56 26	rspcdva	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to K \in ℂ$
58	12	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to T \in ℂ$
59	57 58	subcld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to K - T \in ℂ$
60	59	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|K - T\| \in ℝ$
61	23	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to d \in ℕ$
62	60 61	nndivred	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{\|K - T\|}{d} \in ℝ$
63	21 62	fsumrecl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} (\frac{\|K - T\|}{d}) \in ℝ$
64	63	recnd	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} (\frac{\|K - T\|}{d}) \in ℂ$
65	61	nnrpd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to d \in ℝ^{+}$
66	59	absge0d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to 0 \leq \|K - T\|$
67	60 65 66	divge0d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to 0 \leq \frac{\|K - T\|}{d}$
68	21 62 67	fsumge0	$⊢ (φ \land x \in ℝ^{+}) \to 0 \leq \sum_{d = 1}^{⌊x⌋} (\frac{\|K - T\|}{d})$
69	63 68	absidd	$⊢ (φ \land x \in ℝ^{+}) \to \|\sum_{d = 1}^{⌊x⌋} (\frac{\|K - T\|}{d})\| = \sum_{d = 1}^{⌊x⌋} (\frac{\|K - T\|}{d})$
70	69 63	eqeltrd	$⊢ (φ \land x \in ℝ^{+}) \to \|\sum_{d = 1}^{⌊x⌋} (\frac{\|K - T\|}{d})\| \in ℝ$
71	53	recnd	$⊢ (φ \land x \in ℝ^{+}) \to C \sum_{d = 1}^{⌊x⌋} (\frac{\log (\frac{x}{d})}{x}) + R (\log 3 + 1) \in ℂ$
72	71	abscld	$⊢ (φ \land x \in ℝ^{+}) \to \|C \sum_{d = 1}^{⌊x⌋} (\frac{\log (\frac{x}{d})}{x}) + R (\log 3 + 1)\| \in ℝ$
73		3re	$⊢ 3 \in ℝ$
74	73	a1i	$⊢ (φ \land x \in ℝ^{+}) \to 3 \in ℝ$
75		1le3	$⊢ 1 \leq 3$
76	74 75	jctir	$⊢ (φ \land x \in ℝ^{+}) \to (3 \in ℝ \land 1 \leq 3)$
77	14	adantr	$⊢ (φ \land x \in ℝ^{+}) \to R \in ℝ$
78	36	rexri	$⊢ 1 \in ℝ^{*}$
79	73	rexri	$⊢ 3 \in ℝ^{*}$
80		1lt3	$⊢ 1 < 3$
81		lbico1	$⊢ (1 \in ℝ^{} \land 3 \in ℝ^{} \land 1 < 3) \to 1 \in [1, 3)$
82	78 79 80 81	mp3an	$⊢ 1 \in [1, 3)$
83		0red	$⊢ (φ \land m \in [1, 3)) \to 0 \in ℝ$
84		elico2	$⊢ (1 \in ℝ \land 3 \in ℝ^{*}) \to (m \in [1, 3) \leftrightarrow (m \in ℝ \land 1 \leq m \land m < 3))$
85	36 79 84	mp2an	$⊢ m \in [1, 3) \leftrightarrow (m \in ℝ \land 1 \leq m \land m < 3)$
86	85	simp1bi	$⊢ m \in [1, 3) \to m \in ℝ$
87		0red	$⊢ m \in [1, 3) \to 0 \in ℝ$
88		1red	$⊢ m \in [1, 3) \to 1 \in ℝ$
89		0lt1	$⊢ 0 < 1$
90	89	a1i	$⊢ m \in [1, 3) \to 0 < 1$
91	85	simp2bi	$⊢ m \in [1, 3) \to 1 \leq m$
92	87 88 86 90 91	ltletrd	$⊢ m \in [1, 3) \to 0 < m$
93	86 92	elrpd	$⊢ m \in [1, 3) \to m \in ℝ^{+}$
94	12	adantr	$⊢ (φ \land m \in ℝ^{+}) \to T \in ℂ$
95	9 94	subcld	$⊢ (φ \land m \in ℝ^{+}) \to F - T \in ℂ$
96	95	abscld	$⊢ (φ \land m \in ℝ^{+}) \to \|F - T\| \in ℝ$
97	93 96	sylan2	$⊢ (φ \land m \in [1, 3)) \to \|F - T\| \in ℝ$
98	14	adantr	$⊢ (φ \land m \in [1, 3)) \to R \in ℝ$
99	95	absge0d	$⊢ (φ \land m \in ℝ^{+}) \to 0 \leq \|F - T\|$
100	93 99	sylan2	$⊢ (φ \land m \in [1, 3)) \to 0 \leq \|F - T\|$
101	15	r19.21bi	$⊢ (φ \land m \in [1, 3)) \to \|F - T\| \leq R$
102	83 97 98 100 101	letrd	$⊢ (φ \land m \in [1, 3)) \to 0 \leq R$
103	102	ralrimiva	$⊢ φ \to \forall m \in [1, 3) 0 \leq R$
104		biidd	$⊢ m = 1 \to (0 \leq R \leftrightarrow 0 \leq R)$
105	104	rspcv	$⊢ 1 \in [1, 3) \to (\forall m \in [1, 3) 0 \leq R \to 0 \leq R)$
106	82 103 105	mpsyl	$⊢ φ \to 0 \leq R$
107	106	adantr	$⊢ (φ \land x \in ℝ^{+}) \to 0 \leq R$
108	77 107	jca	$⊢ (φ \land x \in ℝ^{+}) \to (R \in ℝ \land 0 \leq R)$
109	60	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|K - T\| \in ℂ$
110	19	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to C \in ℝ$
111	110 29	remulcld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to C (\frac{\log (\frac{x}{d})}{x}) \in ℝ$
112	18	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (C \in ℝ \land 0 \leq C)$
113		log1	$⊢ \log 1 = 0$
114	61	nncnd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to d \in ℂ$
115	114	mulid2d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to 1 d = d$
116		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
117	116	adantl	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ$
118		fznnfl	$⊢ x \in ℝ \to (d \in (1 \dots ⌊x⌋) \leftrightarrow (d \in ℕ \land d \leq x))$
119	117 118	syl	$⊢ (φ \land x \in ℝ^{+}) \to (d \in (1 \dots ⌊x⌋) \leftrightarrow (d \in ℕ \land d \leq x))$
120	119	simplbda	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to d \leq x$
121	115 120	eqbrtrd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to 1 d \leq x$
122		1red	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to 1 \in ℝ$
123	116	ad2antlr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to x \in ℝ$
124	122 123 65	lemuldivd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (1 d \leq x \leftrightarrow 1 \leq \frac{x}{d})$
125	121 124	mpbid	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to 1 \leq \frac{x}{d}$
126		1rp	$⊢ 1 \in ℝ^{+}$
127	126	a1i	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to 1 \in ℝ^{+}$
128	127 26	logled	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (1 \leq \frac{x}{d} \leftrightarrow \log 1 \leq \log (\frac{x}{d}))$
129	125 128	mpbid	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \log 1 \leq \log (\frac{x}{d})$
130	113 129	eqbrtrrid	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to 0 \leq \log (\frac{x}{d})$
131		rpregt0	$⊢ x \in ℝ^{+} \to (x \in ℝ \land 0 < x)$
132	131	ad2antlr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (x \in ℝ \land 0 < x)$
133		divge0	$⊢ ((\log (\frac{x}{d}) \in ℝ \land 0 \leq \log (\frac{x}{d})) \land (x \in ℝ \land 0 < x)) \to 0 \leq \frac{\log (\frac{x}{d})}{x}$
134	27 130 132 133	syl21anc	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to 0 \leq \frac{\log (\frac{x}{d})}{x}$
135		mulge0	$⊢ ((C \in ℝ \land 0 \leq C) \land (\frac{\log (\frac{x}{d})}{x} \in ℝ \land 0 \leq \frac{\log (\frac{x}{d})}{x})) \to 0 \leq C (\frac{\log (\frac{x}{d})}{x})$
136	112 29 134 135	syl12anc	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to 0 \leq C (\frac{\log (\frac{x}{d})}{x})$
137		absidm	$⊢ K - T \in ℂ \to \|\|K - T\|\| = \|K - T\|$
138	59 137	syl	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \|\|K - T\|\| = \|K - T\|$
139	138	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land 3 \leq \frac{x}{d}) \to \|\|K - T\|\| = \|K - T\|$
140	10	fvoveq1d	$⊢ m = \frac{x}{d} \to \|F - T\| = \|K - T\|$
141		fveq2	$⊢ m = \frac{x}{d} \to \log m = \log (\frac{x}{d})$
142		id	$⊢ m = \frac{x}{d} \to m = \frac{x}{d}$
143	141 142	oveq12d	$⊢ m = \frac{x}{d} \to \frac{\log m}{m} = \frac{\log (\frac{x}{d})}{\frac{x}{d}}$
144	143	oveq2d	$⊢ m = \frac{x}{d} \to C (\frac{\log m}{m}) = C (\frac{\log (\frac{x}{d})}{\frac{x}{d}})$
145	140 144	breq12d	$⊢ m = \frac{x}{d} \to (\|F - T\| \leq C (\frac{\log m}{m}) \leftrightarrow \|K - T\| \leq C (\frac{\log (\frac{x}{d})}{\frac{x}{d}}))$
146	13	ralrimiva	$⊢ φ \to \forall m \in [3, +∞) \|F - T\| \leq C (\frac{\log m}{m})$
147	146	ad3antrrr	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land 3 \leq \frac{x}{d}) \to \forall m \in [3, +∞) \|F - T\| \leq C (\frac{\log m}{m})$
148		nndivre	$⊢ (x \in ℝ \land d \in ℕ) \to \frac{x}{d} \in ℝ$
149	117 23 148	syl2an	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{x}{d} \in ℝ$
150	149	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land 3 \leq \frac{x}{d}) \to \frac{x}{d} \in ℝ$
151		simpr	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land 3 \leq \frac{x}{d}) \to 3 \leq \frac{x}{d}$
152		elicopnf	$⊢ 3 \in ℝ \to (\frac{x}{d} \in [3, +∞) \leftrightarrow (\frac{x}{d} \in ℝ \land 3 \leq \frac{x}{d}))$
153	73 152	ax-mp	$⊢ \frac{x}{d} \in [3, +∞) \leftrightarrow (\frac{x}{d} \in ℝ \land 3 \leq \frac{x}{d})$
154	150 151 153	sylanbrc	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land 3 \leq \frac{x}{d}) \to \frac{x}{d} \in [3, +∞)$
155	145 147 154	rspcdva	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land 3 \leq \frac{x}{d}) \to \|K - T\| \leq C (\frac{\log (\frac{x}{d})}{\frac{x}{d}})$
156	27	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{d}) \in ℂ$
157		rpcnne0	$⊢ x \in ℝ^{+} \to (x \in ℂ \land x \neq 0)$
158	157	ad2antlr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (x \in ℂ \land x \neq 0)$
159	65	rpcnne0d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (d \in ℂ \land d \neq 0)$
160		divdiv2	$⊢ (\log (\frac{x}{d}) \in ℂ \land (x \in ℂ \land x \neq 0) \land (d \in ℂ \land d \neq 0)) \to \frac{\log (\frac{x}{d})}{\frac{x}{d}} = \frac{\log (\frac{x}{d}) d}{x}$
161	156 158 159 160	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{\log (\frac{x}{d})}{\frac{x}{d}} = \frac{\log (\frac{x}{d}) d}{x}$
162		div23	$⊢ (\log (\frac{x}{d}) \in ℂ \land d \in ℂ \land (x \in ℂ \land x \neq 0)) \to \frac{\log (\frac{x}{d}) d}{x} = (\frac{\log (\frac{x}{d})}{x}) d$
163	156 114 158 162	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{\log (\frac{x}{d}) d}{x} = (\frac{\log (\frac{x}{d})}{x}) d$
164	161 163	eqtrd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{\log (\frac{x}{d})}{\frac{x}{d}} = (\frac{\log (\frac{x}{d})}{x}) d$
165	164	oveq2d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to C (\frac{\log (\frac{x}{d})}{\frac{x}{d}}) = C (\frac{\log (\frac{x}{d})}{x}) d$
166	42	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to C \in ℂ$
167	29	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{\log (\frac{x}{d})}{x} \in ℂ$
168	166 167 114	mulassd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to C (\frac{\log (\frac{x}{d})}{x}) d = C (\frac{\log (\frac{x}{d})}{x}) d$
169	165 168	eqtr4d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to C (\frac{\log (\frac{x}{d})}{\frac{x}{d}}) = C (\frac{\log (\frac{x}{d})}{x}) d$
170	169	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land 3 \leq \frac{x}{d}) \to C (\frac{\log (\frac{x}{d})}{\frac{x}{d}}) = C (\frac{\log (\frac{x}{d})}{x}) d$
171	155 170	breqtrd	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land 3 \leq \frac{x}{d}) \to \|K - T\| \leq C (\frac{\log (\frac{x}{d})}{x}) d$
172	139 171	eqbrtrd	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land 3 \leq \frac{x}{d}) \to \|\|K - T\|\| \leq C (\frac{\log (\frac{x}{d})}{x}) d$
173	138	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land \frac{x}{d} < 3) \to \|\|K - T\|\| = \|K - T\|$
174	140	breq1d	$⊢ m = \frac{x}{d} \to (\|F - T\| \leq R \leftrightarrow \|K - T\| \leq R)$
175	15	ad3antrrr	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land \frac{x}{d} < 3) \to \forall m \in [1, 3) \|F - T\| \leq R$
176	149	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land \frac{x}{d} < 3) \to \frac{x}{d} \in ℝ$
177	125	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land \frac{x}{d} < 3) \to 1 \leq \frac{x}{d}$
178		simpr	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land \frac{x}{d} < 3) \to \frac{x}{d} < 3$
179		elico2	$⊢ (1 \in ℝ \land 3 \in ℝ^{*}) \to (\frac{x}{d} \in [1, 3) \leftrightarrow (\frac{x}{d} \in ℝ \land 1 \leq \frac{x}{d} \land \frac{x}{d} < 3))$
180	36 79 179	mp2an	$⊢ \frac{x}{d} \in [1, 3) \leftrightarrow (\frac{x}{d} \in ℝ \land 1 \leq \frac{x}{d} \land \frac{x}{d} < 3)$
181	176 177 178 180	syl3anbrc	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land \frac{x}{d} < 3) \to \frac{x}{d} \in [1, 3)$
182	174 175 181	rspcdva	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land \frac{x}{d} < 3) \to \|K - T\| \leq R$
183	173 182	eqbrtrd	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land \frac{x}{d} < 3) \to \|\|K - T\|\| \leq R$
184	22 76 108 109 111 136 172 183	fsumharmonic	$⊢ (φ \land x \in ℝ^{+}) \to \|\sum_{d = 1}^{⌊x⌋} (\frac{\|K - T\|}{d})\| \leq \sum_{d = 1}^{⌊x⌋} C (\frac{\log (\frac{x}{d})}{x}) + R (\log 3 + 1)$
185	42	adantr	$⊢ (φ \land x \in ℝ^{+}) \to C \in ℂ$
186	21 185 167	fsummulc2	$⊢ (φ \land x \in ℝ^{+}) \to C \sum_{d = 1}^{⌊x⌋} (\frac{\log (\frac{x}{d})}{x}) = \sum_{d = 1}^{⌊x⌋} C (\frac{\log (\frac{x}{d})}{x})$
187	186	oveq1d	$⊢ (φ \land x \in ℝ^{+}) \to C \sum_{d = 1}^{⌊x⌋} (\frac{\log (\frac{x}{d})}{x}) + R (\log 3 + 1) = \sum_{d = 1}^{⌊x⌋} C (\frac{\log (\frac{x}{d})}{x}) + R (\log 3 + 1)$
188	184 187	breqtrrd	$⊢ (φ \land x \in ℝ^{+}) \to \|\sum_{d = 1}^{⌊x⌋} (\frac{\|K - T\|}{d})\| \leq C \sum_{d = 1}^{⌊x⌋} (\frac{\log (\frac{x}{d})}{x}) + R (\log 3 + 1)$
189	53	leabsd	$⊢ (φ \land x \in ℝ^{+}) \to C \sum_{d = 1}^{⌊x⌋} (\frac{\log (\frac{x}{d})}{x}) + R (\log 3 + 1) \leq \|C \sum_{d = 1}^{⌊x⌋} (\frac{\log (\frac{x}{d})}{x}) + R (\log 3 + 1)\|$
190	70 53 72 188 189	letrd	$⊢ (φ \land x \in ℝ^{+}) \to \|\sum_{d = 1}^{⌊x⌋} (\frac{\|K - T\|}{d})\| \leq \|C \sum_{d = 1}^{⌊x⌋} (\frac{\log (\frac{x}{d})}{x}) + R (\log 3 + 1)\|$
191	190	adantrr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{d = 1}^{⌊x⌋} (\frac{\|K - T\|}{d})\| \leq \|C \sum_{d = 1}^{⌊x⌋} (\frac{\log (\frac{x}{d})}{x}) + R (\log 3 + 1)\|$
192	16 52 53 64 191	o1le	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} (\frac{\|K - T\|}{d})) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem dchrvmasumlem2

Proof