dchrvmasumiflem1

	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	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)$

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		fzfid	$⊢ (φ \land m \in ℝ^{+}) \to (1 \dots ⌊m⌋) \in Fin$
18		simpl	$⊢ (φ \land m \in ℝ^{+}) \to φ$
19		elfznn	$⊢ k \in (1 \dots ⌊m⌋) \to k \in ℕ$
20	7	adantr	$⊢ (φ \land k \in ℕ) \to X \in D$
21		nnz	$⊢ k \in ℕ \to k \in ℤ$
22	21	adantl	$⊢ (φ \land k \in ℕ) \to k \in ℤ$
23	4 1 5 2 20 22	dchrzrhcl	$⊢ (φ \land k \in ℕ) \to X (L (k)) \in ℂ$
24	18 19 23	syl2an	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots ⌊m⌋)) \to X (L (k)) \in ℂ$
25		simpr	$⊢ (φ \land m \in ℝ^{+}) \to m \in ℝ^{+}$
26	19	nnrpd	$⊢ k \in (1 \dots ⌊m⌋) \to k \in ℝ^{+}$
27		ifcl	$⊢ (m \in ℝ^{+} \land k \in ℝ^{+}) \to if (S = 0, m, k) \in ℝ^{+}$
28	25 26 27	syl2an	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots ⌊m⌋)) \to if (S = 0, m, k) \in ℝ^{+}$
29	28	relogcld	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots ⌊m⌋)) \to \log if (S = 0, m, k) \in ℝ$
30	19	adantl	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots ⌊m⌋)) \to k \in ℕ$
31	29 30	nndivred	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots ⌊m⌋)) \to \frac{\log if (S = 0, m, k)}{k} \in ℝ$
32	31	recnd	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots ⌊m⌋)) \to \frac{\log if (S = 0, m, k)}{k} \in ℂ$
33	24 32	mulcld	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots ⌊m⌋)) \to X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) \in ℂ$
34	17 33	fsumcl	$⊢ (φ \land m \in ℝ^{+}) \to \sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) \in ℂ$
35		fveq2	$⊢ m = \frac{x}{d} \to ⌊m⌋ = ⌊\frac{x}{d}⌋$
36	35	oveq2d	$⊢ m = \frac{x}{d} \to (1 \dots ⌊m⌋) = (1 \dots ⌊\frac{x}{d}⌋)$
37		ifeq1	$⊢ m = \frac{x}{d} \to if (S = 0, m, k) = if (S = 0, \frac{x}{d}, k)$
38	37	fveq2d	$⊢ m = \frac{x}{d} \to \log if (S = 0, m, k) = \log if (S = 0, \frac{x}{d}, k)$
39	38	oveq1d	$⊢ m = \frac{x}{d} \to \frac{\log if (S = 0, m, k)}{k} = \frac{\log if (S = 0, \frac{x}{d}, k)}{k}$
40	39	oveq2d	$⊢ m = \frac{x}{d} \to X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) = X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k})$
41	40	adantr	$⊢ (m = \frac{x}{d} \land k \in (1 \dots ⌊\frac{x}{d}⌋)) \to X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) = X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k})$
42	36 41	sumeq12rdv	$⊢ m = \frac{x}{d} \to \sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) = \sum_{k = 1}^{⌊\frac{x}{d}⌋} X (L (k)) (\frac{\log if (S = 0, \frac{x}{d}, k)}{k})$
43	10 14	ifcld	$⊢ φ \to if (S = 0, C, E) \in [0, +∞)$
44		0cn	$⊢ 0 \in ℂ$
45		climcl	$⊢ seq 1 (+ K) ⇝ T \to T \in ℂ$
46	15 45	syl	$⊢ φ \to T \in ℂ$
47		ifcl	$⊢ (0 \in ℂ \land T \in ℂ) \to if (S = 0, 0, T) \in ℂ$
48	44 46 47	sylancr	$⊢ φ \to if (S = 0, 0, T) \in ℂ$
49		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
50		1zzd	$⊢ φ \to 1 \in ℤ$
51		nncn	$⊢ k \in ℕ \to k \in ℂ$
52	51	adantl	$⊢ (φ \land k \in ℕ) \to k \in ℂ$
53		nnne0	$⊢ k \in ℕ \to k \neq 0$
54	53	adantl	$⊢ (φ \land k \in ℕ) \to k \neq 0$
55	23 52 54	divcld	$⊢ (φ \land k \in ℕ) \to \frac{X (L (k))}{k} \in ℂ$
56		2fveq3	$⊢ a = k \to X (L (a)) = X (L (k))$
57		id	$⊢ a = k \to a = k$
58	56 57	oveq12d	$⊢ a = k \to \frac{X (L (a))}{a} = \frac{X (L (k))}{k}$
59	58	cbvmptv	$⊢ (a \in ℕ ⟼ \frac{X (L (a))}{a}) = (k \in ℕ ⟼ \frac{X (L (k))}{k})$
60	9 59	eqtri	$⊢ F = (k \in ℕ ⟼ \frac{X (L (k))}{k})$
61	55 60	fmptd	$⊢ φ \to F : ℕ ⟶ ℂ$
62		ffvelrn	$⊢ (F : ℕ ⟶ ℂ \land k \in ℕ) \to F (k) \in ℂ$
63	61 62	sylan	$⊢ (φ \land k \in ℕ) \to F (k) \in ℂ$
64	49 50 63	serf	$⊢ φ \to seq 1 (+ F) : ℕ ⟶ ℂ$
65	64	ad2antrr	$⊢ ((φ \land m \in [3, +∞)) \land S = 0) \to seq 1 (+ F) : ℕ ⟶ ℂ$
66		3re	$⊢ 3 \in ℝ$
67		elicopnf	$⊢ 3 \in ℝ \to (m \in [3, +∞) \leftrightarrow (m \in ℝ \land 3 \leq m))$
68	66 67	mp1i	$⊢ φ \to (m \in [3, +∞) \leftrightarrow (m \in ℝ \land 3 \leq m))$
69	68	simprbda	$⊢ (φ \land m \in [3, +∞)) \to m \in ℝ$
70		1red	$⊢ (φ \land m \in [3, +∞)) \to 1 \in ℝ$
71	66	a1i	$⊢ (φ \land m \in [3, +∞)) \to 3 \in ℝ$
72		1le3	$⊢ 1 \leq 3$
73	72	a1i	$⊢ (φ \land m \in [3, +∞)) \to 1 \leq 3$
74	68	simplbda	$⊢ (φ \land m \in [3, +∞)) \to 3 \leq m$
75	70 71 69 73 74	letrd	$⊢ (φ \land m \in [3, +∞)) \to 1 \leq m$
76		flge1nn	$⊢ (m \in ℝ \land 1 \leq m) \to ⌊m⌋ \in ℕ$
77	69 75 76	syl2anc	$⊢ (φ \land m \in [3, +∞)) \to ⌊m⌋ \in ℕ$
78	77	adantr	$⊢ ((φ \land m \in [3, +∞)) \land S = 0) \to ⌊m⌋ \in ℕ$
79	65 78	ffvelrnd	$⊢ ((φ \land m \in [3, +∞)) \land S = 0) \to seq 1 (+ F) (⌊m⌋) \in ℂ$
80	79	abscld	$⊢ ((φ \land m \in [3, +∞)) \land S = 0) \to \|seq 1 (+ F) (⌊m⌋)\| \in ℝ$
81		simpl	$⊢ (φ \land m \in [3, +∞)) \to φ$
82		0red	$⊢ (φ \land m \in [3, +∞)) \to 0 \in ℝ$
83		3pos	$⊢ 0 < 3$
84	83	a1i	$⊢ (φ \land m \in [3, +∞)) \to 0 < 3$
85	82 71 69 84 74	ltletrd	$⊢ (φ \land m \in [3, +∞)) \to 0 < m$
86	69 85	elrpd	$⊢ (φ \land m \in [3, +∞)) \to m \in ℝ^{+}$
87	81 86	jca	$⊢ (φ \land m \in [3, +∞)) \to (φ \land m \in ℝ^{+})$
88		elrege0	$⊢ C \in [0, +∞) \leftrightarrow (C \in ℝ \land 0 \leq C)$
89	88	simplbi	$⊢ C \in [0, +∞) \to C \in ℝ$
90	10 89	syl	$⊢ φ \to C \in ℝ$
91		rerpdivcl	$⊢ (C \in ℝ \land m \in ℝ^{+}) \to \frac{C}{m} \in ℝ$
92	90 91	sylan	$⊢ (φ \land m \in ℝ^{+}) \to \frac{C}{m} \in ℝ$
93	87 92	syl	$⊢ (φ \land m \in [3, +∞)) \to \frac{C}{m} \in ℝ$
94	93	adantr	$⊢ ((φ \land m \in [3, +∞)) \land S = 0) \to \frac{C}{m} \in ℝ$
95	86	relogcld	$⊢ (φ \land m \in [3, +∞)) \to \log m \in ℝ$
96	69 75	logge0d	$⊢ (φ \land m \in [3, +∞)) \to 0 \leq \log m$
97	95 96	jca	$⊢ (φ \land m \in [3, +∞)) \to (\log m \in ℝ \land 0 \leq \log m)$
98	97	adantr	$⊢ ((φ \land m \in [3, +∞)) \land S = 0) \to (\log m \in ℝ \land 0 \leq \log m)$
99		oveq2	$⊢ S = 0 \to seq 1 (+ F) (⌊m⌋) - S = seq 1 (+ F) (⌊m⌋) - 0$
100	64	adantr	$⊢ (φ \land m \in [3, +∞)) \to seq 1 (+ F) : ℕ ⟶ ℂ$
101	100 77	ffvelrnd	$⊢ (φ \land m \in [3, +∞)) \to seq 1 (+ F) (⌊m⌋) \in ℂ$
102	101	subid1d	$⊢ (φ \land m \in [3, +∞)) \to seq 1 (+ F) (⌊m⌋) - 0 = seq 1 (+ F) (⌊m⌋)$
103	99 102	sylan9eqr	$⊢ ((φ \land m \in [3, +∞)) \land S = 0) \to seq 1 (+ F) (⌊m⌋) - S = seq 1 (+ F) (⌊m⌋)$
104	103	fveq2d	$⊢ ((φ \land m \in [3, +∞)) \land S = 0) \to \|seq 1 (+ F) (⌊m⌋) - S\| = \|seq 1 (+ F) (⌊m⌋)\|$
105		2fveq3	$⊢ y = m \to seq 1 (+ F) (⌊y⌋) = seq 1 (+ F) (⌊m⌋)$
106	105	fvoveq1d	$⊢ y = m \to \|seq 1 (+ F) (⌊y⌋) - S\| = \|seq 1 (+ F) (⌊m⌋) - S\|$
107		oveq2	$⊢ y = m \to \frac{C}{y} = \frac{C}{m}$
108	106 107	breq12d	$⊢ y = m \to (\|seq 1 (+ F) (⌊y⌋) - S\| \leq \frac{C}{y} \leftrightarrow \|seq 1 (+ F) (⌊m⌋) - S\| \leq \frac{C}{m})$
109	12	adantr	$⊢ (φ \land m \in [3, +∞)) \to \forall y \in [1, +∞) \|seq 1 (+ F) (⌊y⌋) - S\| \leq \frac{C}{y}$
110		1re	$⊢ 1 \in ℝ$
111		elicopnf	$⊢ 1 \in ℝ \to (m \in [1, +∞) \leftrightarrow (m \in ℝ \land 1 \leq m))$
112	110 111	ax-mp	$⊢ m \in [1, +∞) \leftrightarrow (m \in ℝ \land 1 \leq m)$
113	69 75 112	sylanbrc	$⊢ (φ \land m \in [3, +∞)) \to m \in [1, +∞)$
114	108 109 113	rspcdva	$⊢ (φ \land m \in [3, +∞)) \to \|seq 1 (+ F) (⌊m⌋) - S\| \leq \frac{C}{m}$
115	114	adantr	$⊢ ((φ \land m \in [3, +∞)) \land S = 0) \to \|seq 1 (+ F) (⌊m⌋) - S\| \leq \frac{C}{m}$
116	104 115	eqbrtrrd	$⊢ ((φ \land m \in [3, +∞)) \land S = 0) \to \|seq 1 (+ F) (⌊m⌋)\| \leq \frac{C}{m}$
117		lemul2a	$⊢ ((\|seq 1 (+ F) (⌊m⌋)\| \in ℝ \land \frac{C}{m} \in ℝ \land (\log m \in ℝ \land 0 \leq \log m)) \land \|seq 1 (+ F) (⌊m⌋)\| \leq \frac{C}{m}) \to \log m \|seq 1 (+ F) (⌊m⌋)\| \leq \log m (\frac{C}{m})$
118	80 94 98 116 117	syl31anc	$⊢ ((φ \land m \in [3, +∞)) \land S = 0) \to \log m \|seq 1 (+ F) (⌊m⌋)\| \leq \log m (\frac{C}{m})$
119		iftrue	$⊢ S = 0 \to if (S = 0, m, k) = m$
120	119	fveq2d	$⊢ S = 0 \to \log if (S = 0, m, k) = \log m$
121	120	oveq1d	$⊢ S = 0 \to \frac{\log if (S = 0, m, k)}{k} = \frac{\log m}{k}$
122	121	ad2antlr	$⊢ (((φ \land m \in ℝ^{+}) \land S = 0) \land k \in (1 \dots ⌊m⌋)) \to \frac{\log if (S = 0, m, k)}{k} = \frac{\log m}{k}$
123	122	oveq2d	$⊢ (((φ \land m \in ℝ^{+}) \land S = 0) \land k \in (1 \dots ⌊m⌋)) \to X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) = X (L (k)) (\frac{\log m}{k})$
124	24	adantlr	$⊢ (((φ \land m \in ℝ^{+}) \land S = 0) \land k \in (1 \dots ⌊m⌋)) \to X (L (k)) \in ℂ$
125		relogcl	$⊢ m \in ℝ^{+} \to \log m \in ℝ$
126	125	adantl	$⊢ (φ \land m \in ℝ^{+}) \to \log m \in ℝ$
127	126	recnd	$⊢ (φ \land m \in ℝ^{+}) \to \log m \in ℂ$
128	127	ad2antrr	$⊢ (((φ \land m \in ℝ^{+}) \land S = 0) \land k \in (1 \dots ⌊m⌋)) \to \log m \in ℂ$
129	19	adantl	$⊢ (((φ \land m \in ℝ^{+}) \land S = 0) \land k \in (1 \dots ⌊m⌋)) \to k \in ℕ$
130	129	nncnd	$⊢ (((φ \land m \in ℝ^{+}) \land S = 0) \land k \in (1 \dots ⌊m⌋)) \to k \in ℂ$
131	129	nnne0d	$⊢ (((φ \land m \in ℝ^{+}) \land S = 0) \land k \in (1 \dots ⌊m⌋)) \to k \neq 0$
132	124 128 130 131	div12d	$⊢ (((φ \land m \in ℝ^{+}) \land S = 0) \land k \in (1 \dots ⌊m⌋)) \to X (L (k)) (\frac{\log m}{k}) = \log m (\frac{X (L (k))}{k})$
133	123 132	eqtrd	$⊢ (((φ \land m \in ℝ^{+}) \land S = 0) \land k \in (1 \dots ⌊m⌋)) \to X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) = \log m (\frac{X (L (k))}{k})$
134	133	sumeq2dv	$⊢ ((φ \land m \in ℝ^{+}) \land S = 0) \to \sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) = \sum_{k = 1}^{⌊m⌋} \log m (\frac{X (L (k))}{k})$
135		iftrue	$⊢ S = 0 \to if (S = 0, 0, T) = 0$
136	135	oveq2d	$⊢ S = 0 \to \sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) - if (S = 0, 0, T) = \sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) - 0$
137	34	subid1d	$⊢ (φ \land m \in ℝ^{+}) \to \sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) - 0 = \sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k})$
138	136 137	sylan9eqr	$⊢ ((φ \land m \in ℝ^{+}) \land S = 0) \to \sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) - if (S = 0, 0, T) = \sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k})$
139		ovex	$⊢ \frac{X (L (k))}{k} \in V$
140	58 9 139	fvmpt	$⊢ k \in ℕ \to F (k) = \frac{X (L (k))}{k}$
141	30 140	syl	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots ⌊m⌋)) \to F (k) = \frac{X (L (k))}{k}$
142	61	adantr	$⊢ (φ \land m \in ℝ^{+}) \to F : ℕ ⟶ ℂ$
143	142 19 62	syl2an	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots ⌊m⌋)) \to F (k) \in ℂ$
144	141 143	eqeltrrd	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots ⌊m⌋)) \to \frac{X (L (k))}{k} \in ℂ$
145	17 127 144	fsummulc2	$⊢ (φ \land m \in ℝ^{+}) \to \log m \sum_{k = 1}^{⌊m⌋} (\frac{X (L (k))}{k}) = \sum_{k = 1}^{⌊m⌋} \log m (\frac{X (L (k))}{k})$
146	145	adantr	$⊢ ((φ \land m \in ℝ^{+}) \land S = 0) \to \log m \sum_{k = 1}^{⌊m⌋} (\frac{X (L (k))}{k}) = \sum_{k = 1}^{⌊m⌋} \log m (\frac{X (L (k))}{k})$
147	134 138 146	3eqtr4d	$⊢ ((φ \land m \in ℝ^{+}) \land S = 0) \to \sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) - if (S = 0, 0, T) = \log m \sum_{k = 1}^{⌊m⌋} (\frac{X (L (k))}{k})$
148	87 147	sylan	$⊢ ((φ \land m \in [3, +∞)) \land S = 0) \to \sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) - if (S = 0, 0, T) = \log m \sum_{k = 1}^{⌊m⌋} (\frac{X (L (k))}{k})$
149	87 141	sylan	$⊢ ((φ \land m \in [3, +∞)) \land k \in (1 \dots ⌊m⌋)) \to F (k) = \frac{X (L (k))}{k}$
150	77 49	eleqtrdi	$⊢ (φ \land m \in [3, +∞)) \to ⌊m⌋ \in ℤ_{\geq 1}$
151	81 19 55	syl2an	$⊢ ((φ \land m \in [3, +∞)) \land k \in (1 \dots ⌊m⌋)) \to \frac{X (L (k))}{k} \in ℂ$
152	149 150 151	fsumser	$⊢ (φ \land m \in [3, +∞)) \to \sum_{k = 1}^{⌊m⌋} (\frac{X (L (k))}{k}) = seq 1 (+ F) (⌊m⌋)$
153	152	adantr	$⊢ ((φ \land m \in [3, +∞)) \land S = 0) \to \sum_{k = 1}^{⌊m⌋} (\frac{X (L (k))}{k}) = seq 1 (+ F) (⌊m⌋)$
154	153	oveq2d	$⊢ ((φ \land m \in [3, +∞)) \land S = 0) \to \log m \sum_{k = 1}^{⌊m⌋} (\frac{X (L (k))}{k}) = \log m seq 1 (+ F) (⌊m⌋)$
155	148 154	eqtrd	$⊢ ((φ \land m \in [3, +∞)) \land S = 0) \to \sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) - if (S = 0, 0, T) = \log m seq 1 (+ F) (⌊m⌋)$
156	155	fveq2d	$⊢ ((φ \land m \in [3, +∞)) \land S = 0) \to \|\sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) - if (S = 0, 0, T)\| = \|\log m seq 1 (+ F) (⌊m⌋)\|$
157	125	ad2antlr	$⊢ ((φ \land m \in ℝ^{+}) \land S = 0) \to \log m \in ℝ$
158	157	recnd	$⊢ ((φ \land m \in ℝ^{+}) \land S = 0) \to \log m \in ℂ$
159	87 158	sylan	$⊢ ((φ \land m \in [3, +∞)) \land S = 0) \to \log m \in ℂ$
160	159 79	absmuld	$⊢ ((φ \land m \in [3, +∞)) \land S = 0) \to \|\log m seq 1 (+ F) (⌊m⌋)\| = \|\log m\| \|seq 1 (+ F) (⌊m⌋)\|$
161	95 96	absidd	$⊢ (φ \land m \in [3, +∞)) \to \|\log m\| = \log m$
162	161	oveq1d	$⊢ (φ \land m \in [3, +∞)) \to \|\log m\| \|seq 1 (+ F) (⌊m⌋)\| = \log m \|seq 1 (+ F) (⌊m⌋)\|$
163	162	adantr	$⊢ ((φ \land m \in [3, +∞)) \land S = 0) \to \|\log m\| \|seq 1 (+ F) (⌊m⌋)\| = \log m \|seq 1 (+ F) (⌊m⌋)\|$
164	156 160 163	3eqtrd	$⊢ ((φ \land m \in [3, +∞)) \land S = 0) \to \|\sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) - if (S = 0, 0, T)\| = \log m \|seq 1 (+ F) (⌊m⌋)\|$
165		iftrue	$⊢ S = 0 \to if (S = 0, C, E) = C$
166	165	adantl	$⊢ ((φ \land m \in ℝ^{+}) \land S = 0) \to if (S = 0, C, E) = C$
167	166	oveq1d	$⊢ ((φ \land m \in ℝ^{+}) \land S = 0) \to if (S = 0, C, E) (\frac{\log m}{m}) = C (\frac{\log m}{m})$
168	90	recnd	$⊢ φ \to C \in ℂ$
169	168	ad2antrr	$⊢ ((φ \land m \in ℝ^{+}) \land S = 0) \to C \in ℂ$
170		rpcnne0	$⊢ m \in ℝ^{+} \to (m \in ℂ \land m \neq 0)$
171	170	ad2antlr	$⊢ ((φ \land m \in ℝ^{+}) \land S = 0) \to (m \in ℂ \land m \neq 0)$
172		div12	$⊢ (C \in ℂ \land \log m \in ℂ \land (m \in ℂ \land m \neq 0)) \to C (\frac{\log m}{m}) = \log m (\frac{C}{m})$
173	169 158 171 172	syl3anc	$⊢ ((φ \land m \in ℝ^{+}) \land S = 0) \to C (\frac{\log m}{m}) = \log m (\frac{C}{m})$
174	167 173	eqtrd	$⊢ ((φ \land m \in ℝ^{+}) \land S = 0) \to if (S = 0, C, E) (\frac{\log m}{m}) = \log m (\frac{C}{m})$
175	87 174	sylan	$⊢ ((φ \land m \in [3, +∞)) \land S = 0) \to if (S = 0, C, E) (\frac{\log m}{m}) = \log m (\frac{C}{m})$
176	118 164 175	3brtr4d	$⊢ ((φ \land m \in [3, +∞)) \land S = 0) \to \|\sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) - if (S = 0, 0, T)\| \leq if (S = 0, C, E) (\frac{\log m}{m})$
177		2fveq3	$⊢ y = m \to seq 1 (+ K) (⌊y⌋) = seq 1 (+ K) (⌊m⌋)$
178	177	fvoveq1d	$⊢ y = m \to \|seq 1 (+ K) (⌊y⌋) - T\| = \|seq 1 (+ K) (⌊m⌋) - T\|$
179		fveq2	$⊢ y = m \to \log y = \log m$
180		id	$⊢ y = m \to y = m$
181	179 180	oveq12d	$⊢ y = m \to \frac{\log y}{y} = \frac{\log m}{m}$
182	181	oveq2d	$⊢ y = m \to E (\frac{\log y}{y}) = E (\frac{\log m}{m})$
183	178 182	breq12d	$⊢ y = m \to (\|seq 1 (+ K) (⌊y⌋) - T\| \leq E (\frac{\log y}{y}) \leftrightarrow \|seq 1 (+ K) (⌊m⌋) - T\| \leq E (\frac{\log m}{m}))$
184	183	rspccva	$⊢ (\forall y \in [3, +∞) \|seq 1 (+ K) (⌊y⌋) - T\| \leq E (\frac{\log y}{y}) \land m \in [3, +∞)) \to \|seq 1 (+ K) (⌊m⌋) - T\| \leq E (\frac{\log m}{m})$
185	16 184	sylan	$⊢ (φ \land m \in [3, +∞)) \to \|seq 1 (+ K) (⌊m⌋) - T\| \leq E (\frac{\log m}{m})$
186	185	adantr	$⊢ ((φ \land m \in [3, +∞)) \land S \neq 0) \to \|seq 1 (+ K) (⌊m⌋) - T\| \leq E (\frac{\log m}{m})$
187		fveq2	$⊢ a = k \to \log a = \log k$
188	187 57	oveq12d	$⊢ a = k \to \frac{\log a}{a} = \frac{\log k}{k}$
189	56 188	oveq12d	$⊢ a = k \to X (L (a)) (\frac{\log a}{a}) = X (L (k)) (\frac{\log k}{k})$
190		ovex	$⊢ X (L (k)) (\frac{\log k}{k}) \in V$
191	189 13 190	fvmpt	$⊢ k \in ℕ \to K (k) = X (L (k)) (\frac{\log k}{k})$
192	19 191	syl	$⊢ k \in (1 \dots ⌊m⌋) \to K (k) = X (L (k)) (\frac{\log k}{k})$
193		ifnefalse	$⊢ S \neq 0 \to if (S = 0, m, k) = k$
194	193	fveq2d	$⊢ S \neq 0 \to \log if (S = 0, m, k) = \log k$
195	194	oveq1d	$⊢ S \neq 0 \to \frac{\log if (S = 0, m, k)}{k} = \frac{\log k}{k}$
196	195	oveq2d	$⊢ S \neq 0 \to X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) = X (L (k)) (\frac{\log k}{k})$
197	196	adantl	$⊢ ((φ \land m \in [3, +∞)) \land S \neq 0) \to X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) = X (L (k)) (\frac{\log k}{k})$
198	197	eqcomd	$⊢ ((φ \land m \in [3, +∞)) \land S \neq 0) \to X (L (k)) (\frac{\log k}{k}) = X (L (k)) (\frac{\log if (S = 0, m, k)}{k})$
199	192 198	sylan9eqr	$⊢ (((φ \land m \in [3, +∞)) \land S \neq 0) \land k \in (1 \dots ⌊m⌋)) \to K (k) = X (L (k)) (\frac{\log if (S = 0, m, k)}{k})$
200	150	adantr	$⊢ ((φ \land m \in [3, +∞)) \land S \neq 0) \to ⌊m⌋ \in ℤ_{\geq 1}$
201		nnrp	$⊢ k \in ℕ \to k \in ℝ^{+}$
202	201	adantl	$⊢ (φ \land k \in ℕ) \to k \in ℝ^{+}$
203	202	relogcld	$⊢ (φ \land k \in ℕ) \to \log k \in ℝ$
204	203	recnd	$⊢ (φ \land k \in ℕ) \to \log k \in ℂ$
205	204 52 54	divcld	$⊢ (φ \land k \in ℕ) \to \frac{\log k}{k} \in ℂ$
206	23 205	mulcld	$⊢ (φ \land k \in ℕ) \to X (L (k)) (\frac{\log k}{k}) \in ℂ$
207	189	cbvmptv	$⊢ (a \in ℕ ⟼ X (L (a)) (\frac{\log a}{a})) = (k \in ℕ ⟼ X (L (k)) (\frac{\log k}{k}))$
208	13 207	eqtri	$⊢ K = (k \in ℕ ⟼ X (L (k)) (\frac{\log k}{k}))$
209	206 208	fmptd	$⊢ φ \to K : ℕ ⟶ ℂ$
210	209	ad2antrr	$⊢ ((φ \land m \in [3, +∞)) \land S \neq 0) \to K : ℕ ⟶ ℂ$
211		ffvelrn	$⊢ (K : ℕ ⟶ ℂ \land k \in ℕ) \to K (k) \in ℂ$
212	210 19 211	syl2an	$⊢ (((φ \land m \in [3, +∞)) \land S \neq 0) \land k \in (1 \dots ⌊m⌋)) \to K (k) \in ℂ$
213	199 212	eqeltrrd	$⊢ (((φ \land m \in [3, +∞)) \land S \neq 0) \land k \in (1 \dots ⌊m⌋)) \to X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) \in ℂ$
214	199 200 213	fsumser	$⊢ ((φ \land m \in [3, +∞)) \land S \neq 0) \to \sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) = seq 1 (+ K) (⌊m⌋)$
215		ifnefalse	$⊢ S \neq 0 \to if (S = 0, 0, T) = T$
216	215	adantl	$⊢ ((φ \land m \in [3, +∞)) \land S \neq 0) \to if (S = 0, 0, T) = T$
217	214 216	oveq12d	$⊢ ((φ \land m \in [3, +∞)) \land S \neq 0) \to \sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) - if (S = 0, 0, T) = seq 1 (+ K) (⌊m⌋) - T$
218	217	fveq2d	$⊢ ((φ \land m \in [3, +∞)) \land S \neq 0) \to \|\sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) - if (S = 0, 0, T)\| = \|seq 1 (+ K) (⌊m⌋) - T\|$
219		ifnefalse	$⊢ S \neq 0 \to if (S = 0, C, E) = E$
220	219	adantl	$⊢ ((φ \land m \in [3, +∞)) \land S \neq 0) \to if (S = 0, C, E) = E$
221	220	oveq1d	$⊢ ((φ \land m \in [3, +∞)) \land S \neq 0) \to if (S = 0, C, E) (\frac{\log m}{m}) = E (\frac{\log m}{m})$
222	186 218 221	3brtr4d	$⊢ ((φ \land m \in [3, +∞)) \land S \neq 0) \to \|\sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) - if (S = 0, 0, T)\| \leq if (S = 0, C, E) (\frac{\log m}{m})$
223	176 222	pm2.61dane	$⊢ (φ \land m \in [3, +∞)) \to \|\sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) - if (S = 0, 0, T)\| \leq if (S = 0, C, E) (\frac{\log m}{m})$
224		fzfid	$⊢ φ \to (1 \dots 2) \in Fin$
225	7	adantr	$⊢ (φ \land k \in (1 \dots 2)) \to X \in D$
226		elfzelz	$⊢ k \in (1 \dots 2) \to k \in ℤ$
227	226	adantl	$⊢ (φ \land k \in (1 \dots 2)) \to k \in ℤ$
228	4 1 5 2 225 227	dchrzrhcl	$⊢ (φ \land k \in (1 \dots 2)) \to X (L (k)) \in ℂ$
229	228	abscld	$⊢ (φ \land k \in (1 \dots 2)) \to \|X (L (k))\| \in ℝ$
230		3rp	$⊢ 3 \in ℝ^{+}$
231		relogcl	$⊢ 3 \in ℝ^{+} \to \log 3 \in ℝ$
232	230 231	ax-mp	$⊢ \log 3 \in ℝ$
233		elfznn	$⊢ k \in (1 \dots 2) \to k \in ℕ$
234	233	adantl	$⊢ (φ \land k \in (1 \dots 2)) \to k \in ℕ$
235		nndivre	$⊢ (\log 3 \in ℝ \land k \in ℕ) \to \frac{\log 3}{k} \in ℝ$
236	232 234 235	sylancr	$⊢ (φ \land k \in (1 \dots 2)) \to \frac{\log 3}{k} \in ℝ$
237	229 236	remulcld	$⊢ (φ \land k \in (1 \dots 2)) \to \|X (L (k))\| (\frac{\log 3}{k}) \in ℝ$
238	224 237	fsumrecl	$⊢ φ \to \sum_{k = 1}^{2} \|X (L (k))\| (\frac{\log 3}{k}) \in ℝ$
239	48	abscld	$⊢ φ \to \|if (S = 0, 0, T)\| \in ℝ$
240	238 239	readdcld	$⊢ φ \to \sum_{k = 1}^{2} \|X (L (k))\| (\frac{\log 3}{k}) + \|if (S = 0, 0, T)\| \in ℝ$
241		simpl	$⊢ (φ \land m \in [1, 3)) \to φ$
242	66	rexri	$⊢ 3 \in ℝ^{*}$
243		elico2	$⊢ (1 \in ℝ \land 3 \in ℝ^{*}) \to (m \in [1, 3) \leftrightarrow (m \in ℝ \land 1 \leq m \land m < 3))$
244	110 242 243	mp2an	$⊢ m \in [1, 3) \leftrightarrow (m \in ℝ \land 1 \leq m \land m < 3)$
245	244	simp1bi	$⊢ m \in [1, 3) \to m \in ℝ$
246	245	adantl	$⊢ (φ \land m \in [1, 3)) \to m \in ℝ$
247		0red	$⊢ (φ \land m \in [1, 3)) \to 0 \in ℝ$
248		1red	$⊢ (φ \land m \in [1, 3)) \to 1 \in ℝ$
249		0lt1	$⊢ 0 < 1$
250	249	a1i	$⊢ (φ \land m \in [1, 3)) \to 0 < 1$
251	244	simp2bi	$⊢ m \in [1, 3) \to 1 \leq m$
252	251	adantl	$⊢ (φ \land m \in [1, 3)) \to 1 \leq m$
253	247 248 246 250 252	ltletrd	$⊢ (φ \land m \in [1, 3)) \to 0 < m$
254	246 253	elrpd	$⊢ (φ \land m \in [1, 3)) \to m \in ℝ^{+}$
255	241 254	jca	$⊢ (φ \land m \in [1, 3)) \to (φ \land m \in ℝ^{+})$
256	48	adantr	$⊢ (φ \land m \in ℝ^{+}) \to if (S = 0, 0, T) \in ℂ$
257	34 256	subcld	$⊢ (φ \land m \in ℝ^{+}) \to \sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) - if (S = 0, 0, T) \in ℂ$
258	255 257	syl	$⊢ (φ \land m \in [1, 3)) \to \sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) - if (S = 0, 0, T) \in ℂ$
259	258	abscld	$⊢ (φ \land m \in [1, 3)) \to \|\sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) - if (S = 0, 0, T)\| \in ℝ$
260	255 34	syl	$⊢ (φ \land m \in [1, 3)) \to \sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) \in ℂ$
261	260	abscld	$⊢ (φ \land m \in [1, 3)) \to \|\sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| \in ℝ$
262	239	adantr	$⊢ (φ \land m \in [1, 3)) \to \|if (S = 0, 0, T)\| \in ℝ$
263	261 262	readdcld	$⊢ (φ \land m \in [1, 3)) \to \|\sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| + \|if (S = 0, 0, T)\| \in ℝ$
264	238	adantr	$⊢ (φ \land m \in [1, 3)) \to \sum_{k = 1}^{2} \|X (L (k))\| (\frac{\log 3}{k}) \in ℝ$
265	264 262	readdcld	$⊢ (φ \land m \in [1, 3)) \to \sum_{k = 1}^{2} \|X (L (k))\| (\frac{\log 3}{k}) + \|if (S = 0, 0, T)\| \in ℝ$
266	34 256	abs2dif2d	$⊢ (φ \land m \in ℝ^{+}) \to \|\sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) - if (S = 0, 0, T)\| \leq \|\sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| + \|if (S = 0, 0, T)\|$
267	255 266	syl	$⊢ (φ \land m \in [1, 3)) \to \|\sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) - if (S = 0, 0, T)\| \leq \|\sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| + \|if (S = 0, 0, T)\|$
268	33	abscld	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots ⌊m⌋)) \to \|X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| \in ℝ$
269	17 268	fsumrecl	$⊢ (φ \land m \in ℝ^{+}) \to \sum_{k = 1}^{⌊m⌋} \|X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| \in ℝ$
270	255 269	syl	$⊢ (φ \land m \in [1, 3)) \to \sum_{k = 1}^{⌊m⌋} \|X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| \in ℝ$
271	17 33	fsumabs	$⊢ (φ \land m \in ℝ^{+}) \to \|\sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| \leq \sum_{k = 1}^{⌊m⌋} \|X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\|$
272	255 271	syl	$⊢ (φ \land m \in [1, 3)) \to \|\sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| \leq \sum_{k = 1}^{⌊m⌋} \|X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\|$
273		fzfid	$⊢ (φ \land m \in ℝ^{+}) \to (1 \dots 2) \in Fin$
274	228	adantlr	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to X (L (k)) \in ℂ$
275	25	adantr	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to m \in ℝ^{+}$
276	233	adantl	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to k \in ℕ$
277	276	nnrpd	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to k \in ℝ^{+}$
278	275 277	ifcld	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to if (S = 0, m, k) \in ℝ^{+}$
279	278	relogcld	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to \log if (S = 0, m, k) \in ℝ$
280	279 276	nndivred	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to \frac{\log if (S = 0, m, k)}{k} \in ℝ$
281	280	recnd	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to \frac{\log if (S = 0, m, k)}{k} \in ℂ$
282	274 281	mulcld	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) \in ℂ$
283	282	abscld	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to \|X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| \in ℝ$
284	273 283	fsumrecl	$⊢ (φ \land m \in ℝ^{+}) \to \sum_{k = 1}^{2} \|X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| \in ℝ$
285	255 284	syl	$⊢ (φ \land m \in [1, 3)) \to \sum_{k = 1}^{2} \|X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| \in ℝ$
286		fzfid	$⊢ (φ \land m \in [1, 3)) \to (1 \dots 2) \in Fin$
287	255 282	sylan	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) \in ℂ$
288	287	abscld	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to \|X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| \in ℝ$
289	287	absge0d	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to 0 \leq \|X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\|$
290	246	flcld	$⊢ (φ \land m \in [1, 3)) \to ⌊m⌋ \in ℤ$
291		2z	$⊢ 2 \in ℤ$
292	291	a1i	$⊢ (φ \land m \in [1, 3)) \to 2 \in ℤ$
293	244	simp3bi	$⊢ m \in [1, 3) \to m < 3$
294	293	adantl	$⊢ (φ \land m \in [1, 3)) \to m < 3$
295		3z	$⊢ 3 \in ℤ$
296		fllt	$⊢ (m \in ℝ \land 3 \in ℤ) \to (m < 3 \leftrightarrow ⌊m⌋ < 3)$
297	246 295 296	sylancl	$⊢ (φ \land m \in [1, 3)) \to (m < 3 \leftrightarrow ⌊m⌋ < 3)$
298	294 297	mpbid	$⊢ (φ \land m \in [1, 3)) \to ⌊m⌋ < 3$
299		df-3	$⊢ 3 = 2 + 1$
300	298 299	breqtrdi	$⊢ (φ \land m \in [1, 3)) \to ⌊m⌋ < 2 + 1$
301		rpre	$⊢ m \in ℝ^{+} \to m \in ℝ$
302	301	adantl	$⊢ (φ \land m \in ℝ^{+}) \to m \in ℝ$
303	302	flcld	$⊢ (φ \land m \in ℝ^{+}) \to ⌊m⌋ \in ℤ$
304		zleltp1	$⊢ (⌊m⌋ \in ℤ \land 2 \in ℤ) \to (⌊m⌋ \leq 2 \leftrightarrow ⌊m⌋ < 2 + 1)$
305	303 291 304	sylancl	$⊢ (φ \land m \in ℝ^{+}) \to (⌊m⌋ \leq 2 \leftrightarrow ⌊m⌋ < 2 + 1)$
306	255 305	syl	$⊢ (φ \land m \in [1, 3)) \to (⌊m⌋ \leq 2 \leftrightarrow ⌊m⌋ < 2 + 1)$
307	300 306	mpbird	$⊢ (φ \land m \in [1, 3)) \to ⌊m⌋ \leq 2$
308		eluz2	$⊢ 2 \in ℤ_{\geq ⌊m⌋} \leftrightarrow (⌊m⌋ \in ℤ \land 2 \in ℤ \land ⌊m⌋ \leq 2)$
309	290 292 307 308	syl3anbrc	$⊢ (φ \land m \in [1, 3)) \to 2 \in ℤ_{\geq ⌊m⌋}$
310		fzss2	$⊢ 2 \in ℤ_{\geq ⌊m⌋} \to (1 \dots ⌊m⌋) \subseteq (1 \dots 2)$
311	309 310	syl	$⊢ (φ \land m \in [1, 3)) \to (1 \dots ⌊m⌋) \subseteq (1 \dots 2)$
312	286 288 289 311	fsumless	$⊢ (φ \land m \in [1, 3)) \to \sum_{k = 1}^{⌊m⌋} \|X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| \leq \sum_{k = 1}^{2} \|X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\|$
313	237	adantlr	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to \|X (L (k))\| (\frac{\log 3}{k}) \in ℝ$
314	274 281	absmuld	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to \|X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| = \|X (L (k))\| \|\frac{\log if (S = 0, m, k)}{k}\|$
315	255 314	sylan	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to \|X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| = \|X (L (k))\| \|\frac{\log if (S = 0, m, k)}{k}\|$
316	255 280	sylan	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to \frac{\log if (S = 0, m, k)}{k} \in ℝ$
317	255 279	sylan	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to \log if (S = 0, m, k) \in ℝ$
318		log1	$⊢ \log 1 = 0$
319		elfzle1	$⊢ k \in (1 \dots 2) \to 1 \leq k$
320		breq2	$⊢ m = if (S = 0, m, k) \to (1 \leq m \leftrightarrow 1 \leq if (S = 0, m, k))$
321		breq2	$⊢ k = if (S = 0, m, k) \to (1 \leq k \leftrightarrow 1 \leq if (S = 0, m, k))$
322	320 321	ifboth	$⊢ (1 \leq m \land 1 \leq k) \to 1 \leq if (S = 0, m, k)$
323	252 319 322	syl2an	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to 1 \leq if (S = 0, m, k)$
324		1rp	$⊢ 1 \in ℝ^{+}$
325		logleb	$⊢ (1 \in ℝ^{+} \land if (S = 0, m, k) \in ℝ^{+}) \to (1 \leq if (S = 0, m, k) \leftrightarrow \log 1 \leq \log if (S = 0, m, k))$
326	324 278 325	sylancr	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to (1 \leq if (S = 0, m, k) \leftrightarrow \log 1 \leq \log if (S = 0, m, k))$
327	255 326	sylan	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to (1 \leq if (S = 0, m, k) \leftrightarrow \log 1 \leq \log if (S = 0, m, k))$
328	323 327	mpbid	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to \log 1 \leq \log if (S = 0, m, k)$
329	318 328	eqbrtrrid	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to 0 \leq \log if (S = 0, m, k)$
330	277	rpregt0d	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to (k \in ℝ \land 0 < k)$
331	255 330	sylan	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to (k \in ℝ \land 0 < k)$
332		divge0	$⊢ ((\log if (S = 0, m, k) \in ℝ \land 0 \leq \log if (S = 0, m, k)) \land (k \in ℝ \land 0 < k)) \to 0 \leq \frac{\log if (S = 0, m, k)}{k}$
333	317 329 331 332	syl21anc	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to 0 \leq \frac{\log if (S = 0, m, k)}{k}$
334	316 333	absidd	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to \|\frac{\log if (S = 0, m, k)}{k}\| = \frac{\log if (S = 0, m, k)}{k}$
335	334 316	eqeltrd	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to \|\frac{\log if (S = 0, m, k)}{k}\| \in ℝ$
336	236	adantlr	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to \frac{\log 3}{k} \in ℝ$
337	229	adantlr	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to \|X (L (k))\| \in ℝ$
338	274	absge0d	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to 0 \leq \|X (L (k))\|$
339	337 338	jca	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to (\|X (L (k))\| \in ℝ \land 0 \leq \|X (L (k))\|)$
340	255 339	sylan	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to (\|X (L (k))\| \in ℝ \land 0 \leq \|X (L (k))\|)$
341	293	ad2antlr	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to m < 3$
342	276	nnred	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to k \in ℝ$
343		2re	$⊢ 2 \in ℝ$
344	343	a1i	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to 2 \in ℝ$
345	66	a1i	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to 3 \in ℝ$
346		elfzle2	$⊢ k \in (1 \dots 2) \to k \leq 2$
347	346	adantl	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to k \leq 2$
348		2lt3	$⊢ 2 < 3$
349	348	a1i	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to 2 < 3$
350	342 344 345 347 349	lelttrd	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to k < 3$
351	255 350	sylan	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to k < 3$
352		breq1	$⊢ m = if (S = 0, m, k) \to (m < 3 \leftrightarrow if (S = 0, m, k) < 3)$
353		breq1	$⊢ k = if (S = 0, m, k) \to (k < 3 \leftrightarrow if (S = 0, m, k) < 3)$
354	352 353	ifboth	$⊢ (m < 3 \land k < 3) \to if (S = 0, m, k) < 3$
355	341 351 354	syl2anc	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to if (S = 0, m, k) < 3$
356	278	rpred	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to if (S = 0, m, k) \in ℝ$
357		ltle	$⊢ (if (S = 0, m, k) \in ℝ \land 3 \in ℝ) \to (if (S = 0, m, k) < 3 \to if (S = 0, m, k) \leq 3)$
358	356 66 357	sylancl	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to (if (S = 0, m, k) < 3 \to if (S = 0, m, k) \leq 3)$
359	255 358	sylan	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to (if (S = 0, m, k) < 3 \to if (S = 0, m, k) \leq 3)$
360	355 359	mpd	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to if (S = 0, m, k) \leq 3$
361		logleb	$⊢ (if (S = 0, m, k) \in ℝ^{+} \land 3 \in ℝ^{+}) \to (if (S = 0, m, k) \leq 3 \leftrightarrow \log if (S = 0, m, k) \leq \log 3)$
362	278 230 361	sylancl	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to (if (S = 0, m, k) \leq 3 \leftrightarrow \log if (S = 0, m, k) \leq \log 3)$
363	255 362	sylan	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to (if (S = 0, m, k) \leq 3 \leftrightarrow \log if (S = 0, m, k) \leq \log 3)$
364	360 363	mpbid	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to \log if (S = 0, m, k) \leq \log 3$
365	232	a1i	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to \log 3 \in ℝ$
366	279 365 277	lediv1d	$⊢ ((φ \land m \in ℝ^{+}) \land k \in (1 \dots 2)) \to (\log if (S = 0, m, k) \leq \log 3 \leftrightarrow \frac{\log if (S = 0, m, k)}{k} \leq \frac{\log 3}{k})$
367	255 366	sylan	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to (\log if (S = 0, m, k) \leq \log 3 \leftrightarrow \frac{\log if (S = 0, m, k)}{k} \leq \frac{\log 3}{k})$
368	364 367	mpbid	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to \frac{\log if (S = 0, m, k)}{k} \leq \frac{\log 3}{k}$
369	334 368	eqbrtrd	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to \|\frac{\log if (S = 0, m, k)}{k}\| \leq \frac{\log 3}{k}$
370		lemul2a	$⊢ ((\|\frac{\log if (S = 0, m, k)}{k}\| \in ℝ \land \frac{\log 3}{k} \in ℝ \land (\|X (L (k))\| \in ℝ \land 0 \leq \|X (L (k))\|)) \land \|\frac{\log if (S = 0, m, k)}{k}\| \leq \frac{\log 3}{k}) \to \|X (L (k))\| \|\frac{\log if (S = 0, m, k)}{k}\| \leq \|X (L (k))\| (\frac{\log 3}{k})$
371	335 336 340 369 370	syl31anc	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to \|X (L (k))\| \|\frac{\log if (S = 0, m, k)}{k}\| \leq \|X (L (k))\| (\frac{\log 3}{k})$
372	315 371	eqbrtrd	$⊢ ((φ \land m \in [1, 3)) \land k \in (1 \dots 2)) \to \|X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| \leq \|X (L (k))\| (\frac{\log 3}{k})$
373	286 288 313 372	fsumle	$⊢ (φ \land m \in [1, 3)) \to \sum_{k = 1}^{2} \|X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| \leq \sum_{k = 1}^{2} \|X (L (k))\| (\frac{\log 3}{k})$
374	270 285 264 312 373	letrd	$⊢ (φ \land m \in [1, 3)) \to \sum_{k = 1}^{⌊m⌋} \|X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| \leq \sum_{k = 1}^{2} \|X (L (k))\| (\frac{\log 3}{k})$
375	261 270 264 272 374	letrd	$⊢ (φ \land m \in [1, 3)) \to \|\sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| \leq \sum_{k = 1}^{2} \|X (L (k))\| (\frac{\log 3}{k})$
376	34	abscld	$⊢ (φ \land m \in ℝ^{+}) \to \|\sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| \in ℝ$
377	238	adantr	$⊢ (φ \land m \in ℝ^{+}) \to \sum_{k = 1}^{2} \|X (L (k))\| (\frac{\log 3}{k}) \in ℝ$
378	256	abscld	$⊢ (φ \land m \in ℝ^{+}) \to \|if (S = 0, 0, T)\| \in ℝ$
379	376 377 378	leadd1d	$⊢ (φ \land m \in ℝ^{+}) \to (\|\sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| \leq \sum_{k = 1}^{2} \|X (L (k))\| (\frac{\log 3}{k}) \leftrightarrow \|\sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| + \|if (S = 0, 0, T)\| \leq \sum_{k = 1}^{2} \|X (L (k))\| (\frac{\log 3}{k}) + \|if (S = 0, 0, T)\|)$
380	255 379	syl	$⊢ (φ \land m \in [1, 3)) \to (\|\sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| \leq \sum_{k = 1}^{2} \|X (L (k))\| (\frac{\log 3}{k}) \leftrightarrow \|\sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| + \|if (S = 0, 0, T)\| \leq \sum_{k = 1}^{2} \|X (L (k))\| (\frac{\log 3}{k}) + \|if (S = 0, 0, T)\|)$
381	375 380	mpbid	$⊢ (φ \land m \in [1, 3)) \to \|\sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k})\| + \|if (S = 0, 0, T)\| \leq \sum_{k = 1}^{2} \|X (L (k))\| (\frac{\log 3}{k}) + \|if (S = 0, 0, T)\|$
382	259 263 265 267 381	letrd	$⊢ (φ \land m \in [1, 3)) \to \|\sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) - if (S = 0, 0, T)\| \leq \sum_{k = 1}^{2} \|X (L (k))\| (\frac{\log 3}{k}) + \|if (S = 0, 0, T)\|$
383	382	ralrimiva	$⊢ φ \to \forall m \in [1, 3) \|\sum_{k = 1}^{⌊m⌋} X (L (k)) (\frac{\log if (S = 0, m, k)}{k}) - if (S = 0, 0, T)\| \leq \sum_{k = 1}^{2} \|X (L (k))\| (\frac{\log 3}{k}) + \|if (S = 0, 0, T)\|$
384	1 2 3 4 5 6 7 8 34 42 43 48 223 240 383	dchrvmasumlem3	$⊢ φ \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)$

Metamath Proof Explorer

Theorem dchrvmasumiflem1

Proof