dchrmusum2

Description: The sum of the Möbius function multiplied by a non-principal Dirichlet character, divided by n , is bounded, provided that T =/= 0 . Lemma 9.4.2 of Shapiro, p. 380. (Contributed by Mario Carneiro, 4-May-2016)

	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}$
	dchrisumn0.f	$⊢ F = (a \in ℕ ⟼ \frac{X (L (a))}{a})$
	dchrisumn0.c	$⊢ φ \to C \in [0, +∞)$
	dchrisumn0.t	$⊢ φ \to seq 1 (+ F) ⇝ T$
	dchrisumn0.1	$⊢ φ \to \forall y \in [1, +∞) \|seq 1 (+ F) (⌊y⌋) - T\| \leq \frac{C}{y}$
Assertion	dchrmusum2	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) T) \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		dchrisumn0.f	$⊢ F = (a \in ℕ ⟼ \frac{X (L (a))}{a})$
10		dchrisumn0.c	$⊢ φ \to C \in [0, +∞)$
11		dchrisumn0.t	$⊢ φ \to seq 1 (+ F) ⇝ T$
12		dchrisumn0.1	$⊢ φ \to \forall y \in [1, +∞) \|seq 1 (+ F) (⌊y⌋) - T\| \leq \frac{C}{y}$
13		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
14		ax-1cn	$⊢ 1 \in ℂ$
15		o1const	$⊢ (ℝ^{+} \subseteq ℝ \land 1 \in ℂ) \to (x \in ℝ^{+} ⟼ 1) \in 𝑂 (1)$
16	13 14 15	mp2an	$⊢ (x \in ℝ^{+} ⟼ 1) \in 𝑂 (1)$
17	16	a1i	$⊢ φ \to (x \in ℝ^{+} ⟼ 1) \in 𝑂 (1)$
18	14	a1i	$⊢ (φ \land x \in ℝ^{+}) \to 1 \in ℂ$
19		fzfid	$⊢ (φ \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \in Fin$
20	7	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to X \in D$
21		elfzelz	$⊢ d \in (1 \dots ⌊x⌋) \to d \in ℤ$
22	21	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to d \in ℤ$
23	4 1 5 2 20 22	dchrzrhcl	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to X (L (d)) \in ℂ$
24		elfznn	$⊢ d \in (1 \dots ⌊x⌋) \to d \in ℕ$
25	24	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to d \in ℕ$
26		mucl	$⊢ d \in ℕ \to μ (d) \in ℤ$
27	26	zred	$⊢ d \in ℕ \to μ (d) \in ℝ$
28		nndivre	$⊢ (μ (d) \in ℝ \land d \in ℕ) \to \frac{μ (d)}{d} \in ℝ$
29	27 28	mpancom	$⊢ d \in ℕ \to \frac{μ (d)}{d} \in ℝ$
30	25 29	syl	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{μ (d)}{d} \in ℝ$
31	30	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{μ (d)}{d} \in ℂ$
32	23 31	mulcld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to X (L (d)) (\frac{μ (d)}{d}) \in ℂ$
33	19 32	fsumcl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) \in ℂ$
34		climcl	$⊢ seq 1 (+ F) ⇝ T \to T \in ℂ$
35	11 34	syl	$⊢ φ \to T \in ℂ$
36	35	adantr	$⊢ (φ \land x \in ℝ^{+}) \to T \in ℂ$
37	33 36	mulcld	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) T \in ℂ$
38	13	a1i	$⊢ φ \to ℝ^{+} \subseteq ℝ$
39		subcl	$⊢ (1 \in ℂ \land \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) T \in ℂ) \to 1 - \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) T \in ℂ$
40	14 37 39	sylancr	$⊢ (φ \land x \in ℝ^{+}) \to 1 - \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) T \in ℂ$
41		1red	$⊢ φ \to 1 \in ℝ$
42		elrege0	$⊢ C \in [0, +∞) \leftrightarrow (C \in ℝ \land 0 \leq C)$
43	10 42	sylib	$⊢ φ \to (C \in ℝ \land 0 \leq C)$
44	43	simpld	$⊢ φ \to C \in ℝ$
45		fzfid	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (1 \dots ⌊x⌋) \in Fin$
46	32	adantlrr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to X (L (d)) (\frac{μ (d)}{d}) \in ℂ$
47		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
48		1zzd	$⊢ φ \to 1 \in ℤ$
49	7	adantr	$⊢ (φ \land m \in ℕ) \to X \in D$
50		nnz	$⊢ m \in ℕ \to m \in ℤ$
51	50	adantl	$⊢ (φ \land m \in ℕ) \to m \in ℤ$
52	4 1 5 2 49 51	dchrzrhcl	$⊢ (φ \land m \in ℕ) \to X (L (m)) \in ℂ$
53		nncn	$⊢ m \in ℕ \to m \in ℂ$
54	53	adantl	$⊢ (φ \land m \in ℕ) \to m \in ℂ$
55		nnne0	$⊢ m \in ℕ \to m \neq 0$
56	55	adantl	$⊢ (φ \land m \in ℕ) \to m \neq 0$
57	52 54 56	divcld	$⊢ (φ \land m \in ℕ) \to \frac{X (L (m))}{m} \in ℂ$
58		2fveq3	$⊢ a = m \to X (L (a)) = X (L (m))$
59		id	$⊢ a = m \to a = m$
60	58 59	oveq12d	$⊢ a = m \to \frac{X (L (a))}{a} = \frac{X (L (m))}{m}$
61	60	cbvmptv	$⊢ (a \in ℕ ⟼ \frac{X (L (a))}{a}) = (m \in ℕ ⟼ \frac{X (L (m))}{m})$
62	9 61	eqtri	$⊢ F = (m \in ℕ ⟼ \frac{X (L (m))}{m})$
63	57 62	fmptd	$⊢ φ \to F : ℕ ⟶ ℂ$
64	63	ffvelrnda	$⊢ (φ \land m \in ℕ) \to F (m) \in ℂ$
65	47 48 64	serf	$⊢ φ \to seq 1 (+ F) : ℕ ⟶ ℂ$
66	65	ad2antrr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to seq 1 (+ F) : ℕ ⟶ ℂ$
67		simprl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to x \in ℝ^{+}$
68	67	rpred	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to x \in ℝ$
69		nndivre	$⊢ (x \in ℝ \land d \in ℕ) \to \frac{x}{d} \in ℝ$
70	68 24 69	syl2an	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \frac{x}{d} \in ℝ$
71	24	adantl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to d \in ℕ$
72	71	nncnd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to d \in ℂ$
73	72	mulid2d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to 1 d = d$
74		fznnfl	$⊢ x \in ℝ \to (d \in (1 \dots ⌊x⌋) \leftrightarrow (d \in ℕ \land d \leq x))$
75	68 74	syl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (d \in (1 \dots ⌊x⌋) \leftrightarrow (d \in ℕ \land d \leq x))$
76	75	simplbda	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to d \leq x$
77	73 76	eqbrtrd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to 1 d \leq x$
78		1red	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to 1 \in ℝ$
79	68	adantr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to x \in ℝ$
80	71	nnrpd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to d \in ℝ^{+}$
81	78 79 80	lemuldivd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to (1 d \leq x \leftrightarrow 1 \leq \frac{x}{d})$
82	77 81	mpbid	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to 1 \leq \frac{x}{d}$
83		flge1nn	$⊢ (\frac{x}{d} \in ℝ \land 1 \leq \frac{x}{d}) \to ⌊\frac{x}{d}⌋ \in ℕ$
84	70 82 83	syl2anc	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to ⌊\frac{x}{d}⌋ \in ℕ$
85	66 84	ffvelrnd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to seq 1 (+ F) (⌊\frac{x}{d}⌋) \in ℂ$
86	46 85	mulcld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to X (L (d)) (\frac{μ (d)}{d}) seq 1 (+ F) (⌊\frac{x}{d}⌋) \in ℂ$
87	35	ad2antrr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to T \in ℂ$
88	46 87	mulcld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to X (L (d)) (\frac{μ (d)}{d}) T \in ℂ$
89	45 86 88	fsumsub	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{d = 1}^{⌊x⌋} (X (L (d)) (\frac{μ (d)}{d}) seq 1 (+ F) (⌊\frac{x}{d}⌋) - X (L (d)) (\frac{μ (d)}{d}) T) = \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) seq 1 (+ F) (⌊\frac{x}{d}⌋) - \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) T$
90	46 85 87	subdid	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to X (L (d)) (\frac{μ (d)}{d}) (seq 1 (+ F) (⌊\frac{x}{d}⌋) - T) = X (L (d)) (\frac{μ (d)}{d}) seq 1 (+ F) (⌊\frac{x}{d}⌋) - X (L (d)) (\frac{μ (d)}{d}) T$
91	90	sumeq2dv	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) (seq 1 (+ F) (⌊\frac{x}{d}⌋) - T) = \sum_{d = 1}^{⌊x⌋} (X (L (d)) (\frac{μ (d)}{d}) seq 1 (+ F) (⌊\frac{x}{d}⌋) - X (L (d)) (\frac{μ (d)}{d}) T)$
92	7	ad3antrrr	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to X \in D$
93	21	ad2antlr	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to d \in ℤ$
94		elfzelz	$⊢ m \in (1 \dots ⌊\frac{x}{d}⌋) \to m \in ℤ$
95	94	adantl	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to m \in ℤ$
96	4 1 5 2 92 93 95	dchrzrhmul	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to X (L (d m)) = X (L (d)) X (L (m))$
97	96	oveq1d	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to \frac{X (L (d m))}{d m} = \frac{X (L (d)) X (L (m))}{d m}$
98	23	adantlrr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to X (L (d)) \in ℂ$
99	98	adantr	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to X (L (d)) \in ℂ$
100	72	adantr	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to d \in ℂ$
101	4 1 5 2 92 95	dchrzrhcl	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to X (L (m)) \in ℂ$
102		elfznn	$⊢ m \in (1 \dots ⌊\frac{x}{d}⌋) \to m \in ℕ$
103	102	adantl	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to m \in ℕ$
104	103	nncnd	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to m \in ℂ$
105	71	nnne0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to d \neq 0$
106	105	adantr	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to d \neq 0$
107	103	nnne0d	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to m \neq 0$
108	99 100 101 104 106 107	divmuldivd	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to (\frac{X (L (d))}{d}) (\frac{X (L (m))}{m}) = \frac{X (L (d)) X (L (m))}{d m}$
109	97 108	eqtr4d	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to \frac{X (L (d m))}{d m} = (\frac{X (L (d))}{d}) (\frac{X (L (m))}{m})$
110	109	oveq2d	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to μ (d) (\frac{X (L (d m))}{d m}) = μ (d) (\frac{X (L (d))}{d}) (\frac{X (L (m))}{m})$
111	71 26	syl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to μ (d) \in ℤ$
112	111	zcnd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to μ (d) \in ℂ$
113	112	adantr	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to μ (d) \in ℂ$
114	99 100 106	divcld	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to \frac{X (L (d))}{d} \in ℂ$
115	101 104 107	divcld	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to \frac{X (L (m))}{m} \in ℂ$
116	113 114 115	mulassd	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to μ (d) (\frac{X (L (d))}{d}) (\frac{X (L (m))}{m}) = μ (d) (\frac{X (L (d))}{d}) (\frac{X (L (m))}{m})$
117	113 99 100 106	div12d	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to μ (d) (\frac{X (L (d))}{d}) = X (L (d)) (\frac{μ (d)}{d})$
118	117	oveq1d	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to μ (d) (\frac{X (L (d))}{d}) (\frac{X (L (m))}{m}) = X (L (d)) (\frac{μ (d)}{d}) (\frac{X (L (m))}{m})$
119	110 116 118	3eqtr2d	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to μ (d) (\frac{X (L (d m))}{d m}) = X (L (d)) (\frac{μ (d)}{d}) (\frac{X (L (m))}{m})$
120	119	sumeq2dv	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{d}⌋} μ (d) (\frac{X (L (d m))}{d m}) = \sum_{m = 1}^{⌊\frac{x}{d}⌋} X (L (d)) (\frac{μ (d)}{d}) (\frac{X (L (m))}{m})$
121		fzfid	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to (1 \dots ⌊\frac{x}{d}⌋) \in Fin$
122		simpll	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to φ$
123	122 102 57	syl2an	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to \frac{X (L (m))}{m} \in ℂ$
124	121 46 123	fsummulc2	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{x}{d}⌋} (\frac{X (L (m))}{m}) = \sum_{m = 1}^{⌊\frac{x}{d}⌋} X (L (d)) (\frac{μ (d)}{d}) (\frac{X (L (m))}{m})$
125		ovex	$⊢ \frac{X (L (m))}{m} \in V$
126	60 9 125	fvmpt	$⊢ m \in ℕ \to F (m) = \frac{X (L (m))}{m}$
127	103 126	syl	$⊢ (((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to F (m) = \frac{X (L (m))}{m}$
128	84 47	eleqtrdi	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to ⌊\frac{x}{d}⌋ \in ℤ_{\geq 1}$
129	127 128 123	fsumser	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{d}⌋} (\frac{X (L (m))}{m}) = seq 1 (+ F) (⌊\frac{x}{d}⌋)$
130	129	oveq2d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to X (L (d)) (\frac{μ (d)}{d}) \sum_{m = 1}^{⌊\frac{x}{d}⌋} (\frac{X (L (m))}{m}) = X (L (d)) (\frac{μ (d)}{d}) seq 1 (+ F) (⌊\frac{x}{d}⌋)$
131	120 124 130	3eqtr2rd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to X (L (d)) (\frac{μ (d)}{d}) seq 1 (+ F) (⌊\frac{x}{d}⌋) = \sum_{m = 1}^{⌊\frac{x}{d}⌋} μ (d) (\frac{X (L (d m))}{d m})$
132	131	sumeq2dv	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) seq 1 (+ F) (⌊\frac{x}{d}⌋) = \sum_{d = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{d}⌋} μ (d) (\frac{X (L (d m))}{d m})$
133		2fveq3	$⊢ n = d m \to X (L (n)) = X (L (d m))$
134		id	$⊢ n = d m \to n = d m$
135	133 134	oveq12d	$⊢ n = d m \to \frac{X (L (n))}{n} = \frac{X (L (d m))}{d m}$
136	135	oveq2d	$⊢ n = d m \to μ (d) (\frac{X (L (n))}{n}) = μ (d) (\frac{X (L (d m))}{d m})$
137		elrabi	$⊢ d \in \{y \in ℕ \| y ∥ n\} \to d \in ℕ$
138	137	ad2antll	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to d \in ℕ$
139	138 26	syl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to μ (d) \in ℤ$
140	139	zcnd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to μ (d) \in ℂ$
141	7	ad2antrr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to X \in D$
142		elfzelz	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℤ$
143	142	adantl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℤ$
144	4 1 5 2 141 143	dchrzrhcl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to X (L (n)) \in ℂ$
145		fz1ssnn	$⊢ (1 \dots ⌊x⌋) \subseteq ℕ$
146	145	a1i	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (1 \dots ⌊x⌋) \subseteq ℕ$
147	146	sselda	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
148	147	nncnd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℂ$
149	147	nnne0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to n \neq 0$
150	144 148 149	divcld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to \frac{X (L (n))}{n} \in ℂ$
151	150	adantrr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to \frac{X (L (n))}{n} \in ℂ$
152	140 151	mulcld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to μ (d) (\frac{X (L (n))}{n}) \in ℂ$
153	136 68 152	dvdsflsumcom	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{n = 1}^{⌊x⌋} \sum_{d \in \{y \in ℕ \| y ∥ n\}} μ (d) (\frac{X (L (n))}{n}) = \sum_{d = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{d}⌋} μ (d) (\frac{X (L (d m))}{d m})$
154		2fveq3	$⊢ n = 1 \to X (L (n)) = X (L (1))$
155		id	$⊢ n = 1 \to n = 1$
156	154 155	oveq12d	$⊢ n = 1 \to \frac{X (L (n))}{n} = \frac{X (L (1))}{1}$
157		simprr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 \leq x$
158		flge1nn	$⊢ (x \in ℝ \land 1 \leq x) \to ⌊x⌋ \in ℕ$
159	68 157 158	syl2anc	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to ⌊x⌋ \in ℕ$
160	159 47	eleqtrdi	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to ⌊x⌋ \in ℤ_{\geq 1}$
161		eluzfz1	$⊢ ⌊x⌋ \in ℤ_{\geq 1} \to 1 \in (1 \dots ⌊x⌋)$
162	160 161	syl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 \in (1 \dots ⌊x⌋)$
163	156 45 146 162 150	musumsum	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{n = 1}^{⌊x⌋} \sum_{d \in \{y \in ℕ \| y ∥ n\}} μ (d) (\frac{X (L (n))}{n}) = \frac{X (L (1))}{1}$
164	132 153 163	3eqtr2d	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) seq 1 (+ F) (⌊\frac{x}{d}⌋) = \frac{X (L (1))}{1}$
165	4 1 5 2 7	dchrzrh1	$⊢ φ \to X (L (1)) = 1$
166	165	adantr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to X (L (1)) = 1$
167	166	oveq1d	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{X (L (1))}{1} = \frac{1}{1}$
168		1div1e1	$⊢ \frac{1}{1} = 1$
169	167 168	eqtrdi	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{X (L (1))}{1} = 1$
170	164 169	eqtr2d	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 = \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) seq 1 (+ F) (⌊\frac{x}{d}⌋)$
171	35	adantr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to T \in ℂ$
172	45 171 46	fsummulc1	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) T = \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) T$
173	170 172	oveq12d	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 - \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) T = \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) seq 1 (+ F) (⌊\frac{x}{d}⌋) - \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) T$
174	89 91 173	3eqtr4rd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 - \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) T = \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) (seq 1 (+ F) (⌊\frac{x}{d}⌋) - T)$
175	174	fveq2d	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|1 - \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) T\| = \|\sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) (seq 1 (+ F) (⌊\frac{x}{d}⌋) - T)\|$
176	85 87	subcld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to seq 1 (+ F) (⌊\frac{x}{d}⌋) - T \in ℂ$
177	46 176	mulcld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to X (L (d)) (\frac{μ (d)}{d}) (seq 1 (+ F) (⌊\frac{x}{d}⌋) - T) \in ℂ$
178	45 177	fsumcl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) (seq 1 (+ F) (⌊\frac{x}{d}⌋) - T) \in ℂ$
179	178	abscld	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) (seq 1 (+ F) (⌊\frac{x}{d}⌋) - T)\| \in ℝ$
180	177	abscld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \|X (L (d)) (\frac{μ (d)}{d}) (seq 1 (+ F) (⌊\frac{x}{d}⌋) - T)\| \in ℝ$
181	45 180	fsumrecl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{d = 1}^{⌊x⌋} \|X (L (d)) (\frac{μ (d)}{d}) (seq 1 (+ F) (⌊\frac{x}{d}⌋) - T)\| \in ℝ$
182	44	adantr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to C \in ℝ$
183	45 177	fsumabs	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) (seq 1 (+ F) (⌊\frac{x}{d}⌋) - T)\| \leq \sum_{d = 1}^{⌊x⌋} \|X (L (d)) (\frac{μ (d)}{d}) (seq 1 (+ F) (⌊\frac{x}{d}⌋) - T)\|$
184		reflcl	$⊢ x \in ℝ \to ⌊x⌋ \in ℝ$
185	68 184	syl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to ⌊x⌋ \in ℝ$
186	185 182	remulcld	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to ⌊x⌋ C \in ℝ$
187	186 67	rerpdivcld	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{⌊x⌋ C}{x} \in ℝ$
188	182 67	rerpdivcld	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{C}{x} \in ℝ$
189	188	adantr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \frac{C}{x} \in ℝ$
190	46	abscld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \|X (L (d)) (\frac{μ (d)}{d})\| \in ℝ$
191	71	nnrecred	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \frac{1}{d} \in ℝ$
192	176	abscld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \|seq 1 (+ F) (⌊\frac{x}{d}⌋) - T\| \in ℝ$
193	80	rpred	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to d \in ℝ$
194	189 193	remulcld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to (\frac{C}{x}) d \in ℝ$
195	46	absge0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to 0 \leq \|X (L (d)) (\frac{μ (d)}{d})\|$
196	176	absge0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to 0 \leq \|seq 1 (+ F) (⌊\frac{x}{d}⌋) - T\|$
197	98	abscld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \|X (L (d))\| \in ℝ$
198	31	adantlrr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \frac{μ (d)}{d} \in ℂ$
199	198	abscld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \|\frac{μ (d)}{d}\| \in ℝ$
200	98	absge0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to 0 \leq \|X (L (d))\|$
201	198	absge0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to 0 \leq \|\frac{μ (d)}{d}\|$
202		eqid	$⊢ {Base}_{Z} = {Base}_{Z}$
203	7	ad2antrr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to X \in D$
204	3	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
205	1 202 2	znzrhfo	$⊢ N \in ℕ_{0} \to L : ℤ \underset{onto}{⟶} {Base}_{Z}$
206		fof	$⊢ L : ℤ \underset{onto}{⟶} {Base}_{Z} \to L : ℤ ⟶ {Base}_{Z}$
207	204 205 206	3syl	$⊢ φ \to L : ℤ ⟶ {Base}_{Z}$
208	207	adantr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to L : ℤ ⟶ {Base}_{Z}$
209		ffvelrn	$⊢ (L : ℤ ⟶ {Base}_{Z} \land d \in ℤ) \to L (d) \in {Base}_{Z}$
210	208 21 209	syl2an	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to L (d) \in {Base}_{Z}$
211	4 5 1 202 203 210	dchrabs2	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \|X (L (d))\| \leq 1$
212	112 72 105	absdivd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \|\frac{μ (d)}{d}\| = \frac{\|μ (d)\|}{\|d\|}$
213	80	rprege0d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to (d \in ℝ \land 0 \leq d)$
214		absid	$⊢ (d \in ℝ \land 0 \leq d) \to \|d\| = d$
215	213 214	syl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \|d\| = d$
216	215	oveq2d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \frac{\|μ (d)\|}{\|d\|} = \frac{\|μ (d)\|}{d}$
217	212 216	eqtrd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \|\frac{μ (d)}{d}\| = \frac{\|μ (d)\|}{d}$
218	112	abscld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \|μ (d)\| \in ℝ$
219		mule1	$⊢ d \in ℕ \to \|μ (d)\| \leq 1$
220	71 219	syl	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \|μ (d)\| \leq 1$
221	218 78 80 220	lediv1dd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \frac{\|μ (d)\|}{d} \leq \frac{1}{d}$
222	217 221	eqbrtrd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \|\frac{μ (d)}{d}\| \leq \frac{1}{d}$
223	197 78 199 191 200 201 211 222	lemul12ad	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \|X (L (d))\| \|\frac{μ (d)}{d}\| \leq 1 (\frac{1}{d})$
224	98 198	absmuld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \|X (L (d)) (\frac{μ (d)}{d})\| = \|X (L (d))\| \|\frac{μ (d)}{d}\|$
225	191	recnd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \frac{1}{d} \in ℂ$
226	225	mulid2d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to 1 (\frac{1}{d}) = \frac{1}{d}$
227	226	eqcomd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \frac{1}{d} = 1 (\frac{1}{d})$
228	223 224 227	3brtr4d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \|X (L (d)) (\frac{μ (d)}{d})\| \leq \frac{1}{d}$
229		2fveq3	$⊢ y = \frac{x}{d} \to seq 1 (+ F) (⌊y⌋) = seq 1 (+ F) (⌊\frac{x}{d}⌋)$
230	229	fvoveq1d	$⊢ y = \frac{x}{d} \to \|seq 1 (+ F) (⌊y⌋) - T\| = \|seq 1 (+ F) (⌊\frac{x}{d}⌋) - T\|$
231		oveq2	$⊢ y = \frac{x}{d} \to \frac{C}{y} = \frac{C}{\frac{x}{d}}$
232	230 231	breq12d	$⊢ y = \frac{x}{d} \to (\|seq 1 (+ F) (⌊y⌋) - T\| \leq \frac{C}{y} \leftrightarrow \|seq 1 (+ F) (⌊\frac{x}{d}⌋) - T\| \leq \frac{C}{\frac{x}{d}})$
233	12	ad2antrr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \forall y \in [1, +∞) \|seq 1 (+ F) (⌊y⌋) - T\| \leq \frac{C}{y}$
234		1re	$⊢ 1 \in ℝ$
235		elicopnf	$⊢ 1 \in ℝ \to (\frac{x}{d} \in [1, +∞) \leftrightarrow (\frac{x}{d} \in ℝ \land 1 \leq \frac{x}{d}))$
236	234 235	ax-mp	$⊢ \frac{x}{d} \in [1, +∞) \leftrightarrow (\frac{x}{d} \in ℝ \land 1 \leq \frac{x}{d})$
237	70 82 236	sylanbrc	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \frac{x}{d} \in [1, +∞)$
238	232 233 237	rspcdva	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \|seq 1 (+ F) (⌊\frac{x}{d}⌋) - T\| \leq \frac{C}{\frac{x}{d}}$
239	182	recnd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to C \in ℂ$
240	239	adantr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to C \in ℂ$
241		rpcnne0	$⊢ x \in ℝ^{+} \to (x \in ℂ \land x \neq 0)$
242	241	ad2antrl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (x \in ℂ \land x \neq 0)$
243	242	adantr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to (x \in ℂ \land x \neq 0)$
244		divdiv2	$⊢ (C \in ℂ \land (x \in ℂ \land x \neq 0) \land (d \in ℂ \land d \neq 0)) \to \frac{C}{\frac{x}{d}} = \frac{C d}{x}$
245	240 243 72 105 244	syl112anc	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \frac{C}{\frac{x}{d}} = \frac{C d}{x}$
246		div23	$⊢ (C \in ℂ \land d \in ℂ \land (x \in ℂ \land x \neq 0)) \to \frac{C d}{x} = (\frac{C}{x}) d$
247	240 72 243 246	syl3anc	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \frac{C d}{x} = (\frac{C}{x}) d$
248	245 247	eqtrd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \frac{C}{\frac{x}{d}} = (\frac{C}{x}) d$
249	238 248	breqtrd	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \|seq 1 (+ F) (⌊\frac{x}{d}⌋) - T\| \leq (\frac{C}{x}) d$
250	190 191 192 194 195 196 228 249	lemul12ad	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \|X (L (d)) (\frac{μ (d)}{d})\| \|seq 1 (+ F) (⌊\frac{x}{d}⌋) - T\| \leq (\frac{1}{d}) (\frac{C}{x}) d$
251	46 176	absmuld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \|X (L (d)) (\frac{μ (d)}{d}) (seq 1 (+ F) (⌊\frac{x}{d}⌋) - T)\| = \|X (L (d)) (\frac{μ (d)}{d})\| \|seq 1 (+ F) (⌊\frac{x}{d}⌋) - T\|$
252	188	recnd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{C}{x} \in ℂ$
253	252	adantr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \frac{C}{x} \in ℂ$
254	253 72 105	divcan4d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \frac{(\frac{C}{x}) d}{d} = \frac{C}{x}$
255	253 72	mulcld	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to (\frac{C}{x}) d \in ℂ$
256	255 72 105	divrec2d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \frac{(\frac{C}{x}) d}{d} = (\frac{1}{d}) (\frac{C}{x}) d$
257	254 256	eqtr3d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \frac{C}{x} = (\frac{1}{d}) (\frac{C}{x}) d$
258	250 251 257	3brtr4d	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land d \in (1 \dots ⌊x⌋)) \to \|X (L (d)) (\frac{μ (d)}{d}) (seq 1 (+ F) (⌊\frac{x}{d}⌋) - T)\| \leq \frac{C}{x}$
259	45 180 189 258	fsumle	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{d = 1}^{⌊x⌋} \|X (L (d)) (\frac{μ (d)}{d}) (seq 1 (+ F) (⌊\frac{x}{d}⌋) - T)\| \leq \sum_{d = 1}^{⌊x⌋} (\frac{C}{x})$
260	159	nnnn0d	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to ⌊x⌋ \in ℕ_{0}$
261		hashfz1	$⊢ ⌊x⌋ \in ℕ_{0} \to \|(1 \dots ⌊x⌋)\| = ⌊x⌋$
262	260 261	syl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|(1 \dots ⌊x⌋)\| = ⌊x⌋$
263	262	oveq1d	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|(1 \dots ⌊x⌋)\| (\frac{C}{x}) = ⌊x⌋ (\frac{C}{x})$
264		fsumconst	$⊢ ((1 \dots ⌊x⌋) \in Fin \land \frac{C}{x} \in ℂ) \to \sum_{d = 1}^{⌊x⌋} (\frac{C}{x}) = \|(1 \dots ⌊x⌋)\| (\frac{C}{x})$
265	45 252 264	syl2anc	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{d = 1}^{⌊x⌋} (\frac{C}{x}) = \|(1 \dots ⌊x⌋)\| (\frac{C}{x})$
266	159	nncnd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to ⌊x⌋ \in ℂ$
267		divass	$⊢ (⌊x⌋ \in ℂ \land C \in ℂ \land (x \in ℂ \land x \neq 0)) \to \frac{⌊x⌋ C}{x} = ⌊x⌋ (\frac{C}{x})$
268	266 239 242 267	syl3anc	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{⌊x⌋ C}{x} = ⌊x⌋ (\frac{C}{x})$
269	263 265 268	3eqtr4d	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{d = 1}^{⌊x⌋} (\frac{C}{x}) = \frac{⌊x⌋ C}{x}$
270	259 269	breqtrd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{d = 1}^{⌊x⌋} \|X (L (d)) (\frac{μ (d)}{d}) (seq 1 (+ F) (⌊\frac{x}{d}⌋) - T)\| \leq \frac{⌊x⌋ C}{x}$
271	43	adantr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (C \in ℝ \land 0 \leq C)$
272		flle	$⊢ x \in ℝ \to ⌊x⌋ \leq x$
273	68 272	syl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to ⌊x⌋ \leq x$
274		lemul1a	$⊢ ((⌊x⌋ \in ℝ \land x \in ℝ \land (C \in ℝ \land 0 \leq C)) \land ⌊x⌋ \leq x) \to ⌊x⌋ C \leq x C$
275	185 68 271 273 274	syl31anc	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to ⌊x⌋ C \leq x C$
276	186 182 67	ledivmuld	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (\frac{⌊x⌋ C}{x} \leq C \leftrightarrow ⌊x⌋ C \leq x C)$
277	275 276	mpbird	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{⌊x⌋ C}{x} \leq C$
278	181 187 182 270 277	letrd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{d = 1}^{⌊x⌋} \|X (L (d)) (\frac{μ (d)}{d}) (seq 1 (+ F) (⌊\frac{x}{d}⌋) - T)\| \leq C$
279	179 181 182 183 278	letrd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) (seq 1 (+ F) (⌊\frac{x}{d}⌋) - T)\| \leq C$
280	175 279	eqbrtrd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|1 - \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) T\| \leq C$
281	38 40 41 44 280	elo1d	$⊢ φ \to (x \in ℝ^{+} ⟼ 1 - \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) T) \in 𝑂 (1)$
282	18 37 281	o1dif	$⊢ φ \to ((x \in ℝ^{+} ⟼ 1) \in 𝑂 (1) \leftrightarrow (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) T) \in 𝑂 (1))$
283	17 282	mpbid	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) T) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem dchrmusum2

Proof