dchrvmasumiflem2

	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}$
	dchrvmasumif.f	$⊢ F = (a \in ℕ ⟼ \frac{X (L (a))}{a})$
	dchrvmasumif.c	$⊢ φ \to C \in [0, +∞)$
	dchrvmasumif.s	$⊢ φ \to seq 1 (+ F) ⇝ S$
	dchrvmasumif.1	$⊢ φ \to \forall y \in [1, +∞) \|seq 1 (+ F) (⌊y⌋) - S\| \leq \frac{C}{y}$
	dchrvmasumif.g	$⊢ K = (a \in ℕ ⟼ X (L (a)) (\frac{\log a}{a}))$
	dchrvmasumif.e	$⊢ φ \to E \in [0, +∞)$
	dchrvmasumif.t	$⊢ φ \to seq 1 (+ K) ⇝ T$
	dchrvmasumif.2	$⊢ φ \to \forall y \in [3, +∞) \|seq 1 (+ K) (⌊y⌋) - T\| \leq E (\frac{\log y}{y})$
Assertion	dchrvmasumiflem2	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{Λ (n)}{n}) + if (S = 0, \log x, 0)) \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		dchrvmasumif.f	$⊢ F = (a \in ℕ ⟼ \frac{X (L (a))}{a})$
10		dchrvmasumif.c	$⊢ φ \to C \in [0, +∞)$
11		dchrvmasumif.s	$⊢ φ \to seq 1 (+ F) ⇝ S$
12		dchrvmasumif.1	$⊢ φ \to \forall y \in [1, +∞) \|seq 1 (+ F) (⌊y⌋) - S\| \leq \frac{C}{y}$
13		dchrvmasumif.g	$⊢ K = (a \in ℕ ⟼ X (L (a)) (\frac{\log a}{a}))$
14		dchrvmasumif.e	$⊢ φ \to E \in [0, +∞)$
15		dchrvmasumif.t	$⊢ φ \to seq 1 (+ K) ⇝ T$
16		dchrvmasumif.2	$⊢ φ \to \forall y \in [3, +∞) \|seq 1 (+ K) (⌊y⌋) - T\| \leq E (\frac{\log y}{y})$
17		1red	$⊢ φ \to 1 \in ℝ$
18		fzfid	$⊢ (φ \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \in Fin$
19	7	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to X \in D$
20		elfzelz	$⊢ d \in (1 \dots ⌊x⌋) \to d \in ℤ$
21	20	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to d \in ℤ$
22	4 1 5 2 19 21	dchrzrhcl	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to X (L (d)) \in ℂ$
23		elfznn	$⊢ d \in (1 \dots ⌊x⌋) \to d \in ℕ$
24	23	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to d \in ℕ$
25		mucl	$⊢ d \in ℕ \to μ (d) \in ℤ$
26	24 25	syl	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to μ (d) \in ℤ$
27	26	zred	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to μ (d) \in ℝ$
28	27 24	nndivred	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{μ (d)}{d} \in ℝ$
29	28	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{μ (d)}{d} \in ℂ$
30	22 29	mulcld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to X (L (d)) (\frac{μ (d)}{d}) \in ℂ$
31	18 30	fsumcl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) \in ℂ$
32		climcl	$⊢ seq 1 (+ F) ⇝ S \to S \in ℂ$
33	11 32	syl	$⊢ φ \to S \in ℂ$
34	33	adantr	$⊢ (φ \land x \in ℝ^{+}) \to S \in ℂ$
35	31 34	mulcld	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) S \in ℂ$
36		0cnd	$⊢ (φ \land S = 0) \to 0 \in ℂ$
37		df-ne	$⊢ S \neq 0 \leftrightarrow \neg S = 0$
38		climcl	$⊢ seq 1 (+ K) ⇝ T \to T \in ℂ$
39	15 38	syl	$⊢ φ \to T \in ℂ$
40	39	adantr	$⊢ (φ \land S \neq 0) \to T \in ℂ$
41	33	adantr	$⊢ (φ \land S \neq 0) \to S \in ℂ$
42		simpr	$⊢ (φ \land S \neq 0) \to S \neq 0$
43	40 41 42	divcld	$⊢ (φ \land S \neq 0) \to \frac{T}{S} \in ℂ$
44	37 43	sylan2br	$⊢ (φ \land \neg S = 0) \to \frac{T}{S} \in ℂ$
45	36 44	ifclda	$⊢ φ \to if (S = 0, 0, \frac{T}{S}) \in ℂ$
46	45	adantr	$⊢ (φ \land x \in ℝ^{+}) \to if (S = 0, 0, \frac{T}{S}) \in ℂ$
47	1 2 3 4 5 6 7 8 9 10 11 12	dchrmusum2	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) S) \in 𝑂 (1)$
48		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
49		o1const	$⊢ (ℝ^{+} \subseteq ℝ \land if (S = 0, 0, \frac{T}{S}) \in ℂ) \to (x \in ℝ^{+} ⟼ if (S = 0, 0, \frac{T}{S})) \in 𝑂 (1)$
50	48 45 49	sylancr	$⊢ φ \to (x \in ℝ^{+} ⟼ if (S = 0, 0, \frac{T}{S})) \in 𝑂 (1)$
51	35 46 47 50	o1mul2	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) S if (S = 0, 0, \frac{T}{S})) \in 𝑂 (1)$
52		fzfid	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to (1 \dots ⌊\frac{x}{d}⌋) \in Fin$
53	19	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{d}⌋)) \to X \in D$
54		elfzelz	$⊢ k \in (1 \dots ⌊\frac{x}{d}⌋) \to k \in ℤ$
55	54	adantl	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{d}⌋)) \to k \in ℤ$
56	4 1 5 2 53 55	dchrzrhcl	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{d}⌋)) \to X (L (k)) \in ℂ$
57		simpr	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ^{+}$
58	23	nnrpd	$⊢ d \in (1 \dots ⌊x⌋) \to d \in ℝ^{+}$
59		rpdivcl	$⊢ (x \in ℝ^{+} \land d \in ℝ^{+}) \to \frac{x}{d} \in ℝ^{+}$
60	57 58 59	syl2an	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \frac{x}{d} \in ℝ^{+}$
61		elfznn	$⊢ k \in (1 \dots ⌊\frac{x}{d}⌋) \to k \in ℕ$
62	61	nnrpd	$⊢ k \in (1 \dots ⌊\frac{x}{d}⌋) \to k \in ℝ^{+}$
63		ifcl	$⊢ (\frac{x}{d} \in ℝ^{+} \land k \in ℝ^{+}) \to if (S = 0, \frac{x}{d}, k) \in ℝ^{+}$
64	60 62 63	syl2an	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{d}⌋)) \to if (S = 0, \frac{x}{d}, k) \in ℝ^{+}$
65	64	relogcld	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{d}⌋)) \to \log if (S = 0, \frac{x}{d}, k) \in ℝ$
66	61	adantl	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{d}⌋)) \to k \in ℕ$
67	65 66	nndivred	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{d}⌋)) \to \frac{\log if (S = 0, \frac{x}{d}, k)}{k} \in ℝ$
68	67	recnd	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{d}⌋)) \to \frac{\log if (S = 0, \frac{x}{d}, k)}{k} \in ℂ$
69	56 68	mulcld	$⊢ (((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \land k \in (1 \dots ⌊\frac{x}{d}⌋)) \to X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k}) \in ℂ$
70	52 69	fsumcl	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to \sum_{k = 1}^{⌊\frac{x}{d}⌋} X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k}) \in ℂ$
71	30 70	mulcld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to X (L (d)) (\frac{μ (d)}{d}) \sum_{k = 1}^{⌊\frac{x}{d}⌋} X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k}) \in ℂ$
72	18 71	fsumcl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{k = 1}^{⌊\frac{x}{d}⌋} X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k}) \in ℂ$
73	35 46	mulcld	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) S if (S = 0, 0, \frac{T}{S}) \in ℂ$
74		0cn	$⊢ 0 \in ℂ$
75	39	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to T \in ℂ$
76		ifcl	$⊢ (0 \in ℂ \land T \in ℂ) \to if (S = 0, 0, T) \in ℂ$
77	74 75 76	sylancr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to if (S = 0, 0, T) \in ℂ$
78	30 70 77	subdid	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to X (L (d)) (\frac{μ (d)}{d}) (\sum_{k = 1}^{⌊\frac{x}{d}⌋} X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k}) - if (S = 0, 0, T)) = X (L (d)) (\frac{μ (d)}{d}) \sum_{k = 1}^{⌊\frac{x}{d}⌋} X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k}) - X (L (d)) (\frac{μ (d)}{d}) if (S = 0, 0, T)$
79	78	sumeq2dv	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) (\sum_{k = 1}^{⌊\frac{x}{d}⌋} X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k}) - if (S = 0, 0, T)) = \sum_{d = 1}^{⌊x⌋} (X (L (d)) (\frac{μ (d)}{d}) \sum_{k = 1}^{⌊\frac{x}{d}⌋} X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k}) - X (L (d)) (\frac{μ (d)}{d}) if (S = 0, 0, T))$
80	30 77	mulcld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in (1 \dots ⌊x⌋)) \to X (L (d)) (\frac{μ (d)}{d}) if (S = 0, 0, T) \in ℂ$
81	18 71 80	fsumsub	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} (X (L (d)) (\frac{μ (d)}{d}) \sum_{k = 1}^{⌊\frac{x}{d}⌋} X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k}) - X (L (d)) (\frac{μ (d)}{d}) if (S = 0, 0, T)) = \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{k = 1}^{⌊\frac{x}{d}⌋} X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k}) - \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) if (S = 0, 0, T)$
82	31 34 46	mulassd	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) S if (S = 0, 0, \frac{T}{S}) = \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) S if (S = 0, 0, \frac{T}{S})$
83		ovif2	$⊢ S if (S = 0, 0, \frac{T}{S}) = if (S = 0, S \cdot 0, S (\frac{T}{S}))$
84	33	mul01d	$⊢ φ \to S \cdot 0 = 0$
85	84	ifeq1d	$⊢ φ \to if (S = 0, S \cdot 0, S (\frac{T}{S})) = if (S = 0, 0, S (\frac{T}{S}))$
86	40 41 42	divcan2d	$⊢ (φ \land S \neq 0) \to S (\frac{T}{S}) = T$
87	37 86	sylan2br	$⊢ (φ \land \neg S = 0) \to S (\frac{T}{S}) = T$
88	87	ifeq2da	$⊢ φ \to if (S = 0, 0, S (\frac{T}{S})) = if (S = 0, 0, T)$
89	85 88	eqtrd	$⊢ φ \to if (S = 0, S \cdot 0, S (\frac{T}{S})) = if (S = 0, 0, T)$
90	83 89	syl5eq	$⊢ φ \to S if (S = 0, 0, \frac{T}{S}) = if (S = 0, 0, T)$
91	90	adantr	$⊢ (φ \land x \in ℝ^{+}) \to S if (S = 0, 0, \frac{T}{S}) = if (S = 0, 0, T)$
92	91	oveq2d	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) S if (S = 0, 0, \frac{T}{S}) = \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) if (S = 0, 0, T)$
93	74 39 76	sylancr	$⊢ φ \to if (S = 0, 0, T) \in ℂ$
94	93	adantr	$⊢ (φ \land x \in ℝ^{+}) \to if (S = 0, 0, T) \in ℂ$
95	18 94 30	fsummulc1	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) if (S = 0, 0, T) = \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) if (S = 0, 0, T)$
96	82 92 95	3eqtrrd	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) if (S = 0, 0, T) = \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) S if (S = 0, 0, \frac{T}{S})$
97	96	oveq2d	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{k = 1}^{⌊\frac{x}{d}⌋} X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k}) - \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) if (S = 0, 0, T) = \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{k = 1}^{⌊\frac{x}{d}⌋} X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k}) - \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) S if (S = 0, 0, \frac{T}{S})$
98	79 81 97	3eqtrd	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) (\sum_{k = 1}^{⌊\frac{x}{d}⌋} X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k}) - if (S = 0, 0, T)) = \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{k = 1}^{⌊\frac{x}{d}⌋} X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k}) - \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) S if (S = 0, 0, \frac{T}{S})$
99	98	mpteq2dva	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) (\sum_{k = 1}^{⌊\frac{x}{d}⌋} X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k}) - if (S = 0, 0, T))) = (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{k = 1}^{⌊\frac{x}{d}⌋} X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k}) - \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) S if (S = 0, 0, \frac{T}{S}))$
100	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	dchrvmasumiflem1	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) (\sum_{k = 1}^{⌊\frac{x}{d}⌋} X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k}) - if (S = 0, 0, T))) \in 𝑂 (1)$
101	99 100	eqeltrrd	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{k = 1}^{⌊\frac{x}{d}⌋} X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k}) - \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) S if (S = 0, 0, \frac{T}{S})) \in 𝑂 (1)$
102	72 73 101	o1dif	$⊢ φ \to ((x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{k = 1}^{⌊\frac{x}{d}⌋} X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k})) \in 𝑂 (1) \leftrightarrow (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) S if (S = 0, 0, \frac{T}{S})) \in 𝑂 (1))$
103	51 102	mpbird	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{k = 1}^{⌊\frac{x}{d}⌋} X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k})) \in 𝑂 (1)$
104	7	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to X \in D$
105		elfzelz	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℤ$
106	105	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to n \in ℤ$
107	4 1 5 2 104 106	dchrzrhcl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to X (L (n)) \in ℂ$
108		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
109	108	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
110		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
111		nndivre	$⊢ (Λ (n) \in ℝ \land n \in ℕ) \to \frac{Λ (n)}{n} \in ℝ$
112	110 111	mpancom	$⊢ n \in ℕ \to \frac{Λ (n)}{n} \in ℝ$
113	109 112	syl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n)}{n} \in ℝ$
114	113	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n)}{n} \in ℂ$
115	107 114	mulcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to X (L (n)) (\frac{Λ (n)}{n}) \in ℂ$
116	18 115	fsumcl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{Λ (n)}{n}) \in ℂ$
117		relogcl	$⊢ x \in ℝ^{+} \to \log x \in ℝ$
118	117	adantl	$⊢ (φ \land x \in ℝ^{+}) \to \log x \in ℝ$
119	118	recnd	$⊢ (φ \land x \in ℝ^{+}) \to \log x \in ℂ$
120		ifcl	$⊢ (\log x \in ℂ \land 0 \in ℂ) \to if (S = 0, \log x, 0) \in ℂ$
121	119 74 120	sylancl	$⊢ (φ \land x \in ℝ^{+}) \to if (S = 0, \log x, 0) \in ℂ$
122	116 121	addcld	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{Λ (n)}{n}) + if (S = 0, \log x, 0) \in ℂ$
123	122	abscld	$⊢ (φ \land x \in ℝ^{+}) \to \|\sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{Λ (n)}{n}) + if (S = 0, \log x, 0)\| \in ℝ$
124	123	adantrr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{Λ (n)}{n}) + if (S = 0, \log x, 0)\| \in ℝ$
125	3	adantr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to N \in ℕ$
126	7	adantr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to X \in D$
127	8	adantr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to X \neq \underset{˙}{1}$
128		simprl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to x \in ℝ^{+}$
129		simprr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 \leq x$
130	1 2 125 4 5 6 126 127 128 129	dchrvmasum2if	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{Λ (n)}{n}) + if (S = 0, \log x, 0) = \sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{k = 1}^{⌊\frac{x}{d}⌋} X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k})$
131	130	fveq2d	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{Λ (n)}{n}) + if (S = 0, \log x, 0)\| = \|\sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{k = 1}^{⌊\frac{x}{d}⌋} X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k})\|$
132	124 131	eqled	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{Λ (n)}{n}) + if (S = 0, \log x, 0)\| \leq \|\sum_{d = 1}^{⌊x⌋} X (L (d)) (\frac{μ (d)}{d}) \sum_{k = 1}^{⌊\frac{x}{d}⌋} X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k})\|$
133	17 103 72 122 132	o1le	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{Λ (n)}{n}) + if (S = 0, \log x, 0)) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem dchrvmasumiflem2

Proof