mulog2sumlem2

	Ref	Expression
Hypotheses	logdivsum.1	$⊢ F = (y \in ℝ^{+} ⟼ \sum_{i = 1}^{⌊y⌋} (\frac{\log i}{i}) - (\frac{{\log y}^{2}}{2}))$
	mulog2sumlem.1	$⊢ φ \to F \underset{ℝ}{⇝} L$
	mulog2sumlem2.t	$⊢ T = (\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L$
	mulog2sumlem2.r	$⊢ R = (\frac{1}{2}) + (γ + \|L\|) + \sum_{m = 1}^{2} (\frac{\log (\frac{e}{m})}{m})$
Assertion	mulog2sumlem2	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) T - \log x) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		logdivsum.1	$⊢ F = (y \in ℝ^{+} ⟼ \sum_{i = 1}^{⌊y⌋} (\frac{\log i}{i}) - (\frac{{\log y}^{2}}{2}))$
2		mulog2sumlem.1	$⊢ φ \to F \underset{ℝ}{⇝} L$
3		mulog2sumlem2.t	$⊢ T = (\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L$
4		mulog2sumlem2.r	$⊢ R = (\frac{1}{2}) + (γ + \|L\|) + \sum_{m = 1}^{2} (\frac{\log (\frac{e}{m})}{m})$
5		1red	$⊢ φ \to 1 \in ℝ$
6		2re	$⊢ 2 \in ℝ$
7		fzfid	$⊢ (φ \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \in Fin$
8		simpr	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ^{+}$
9		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
10	9	nnrpd	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℝ^{+}$
11		rpdivcl	$⊢ (x \in ℝ^{+} \land n \in ℝ^{+}) \to \frac{x}{n} \in ℝ^{+}$
12	8 10 11	syl2an	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ^{+}$
13	12	relogcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) \in ℝ$
14		simplr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ^{+}$
15	13 14	rerpdivcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{\log (\frac{x}{n})}{x} \in ℝ$
16	7 15	fsumrecl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x}) \in ℝ$
17		remulcl	$⊢ (2 \in ℝ \land \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x}) \in ℝ) \to 2 \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x}) \in ℝ$
18	6 16 17	sylancr	$⊢ (φ \land x \in ℝ^{+}) \to 2 \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x}) \in ℝ$
19		halfre	$⊢ \frac{1}{2} \in ℝ$
20		emre	$⊢ γ \in ℝ$
21		rlimcl	$⊢ F \underset{ℝ}{⇝} L \to L \in ℂ$
22	2 21	syl	$⊢ φ \to L \in ℂ$
23	22	abscld	$⊢ φ \to \|L\| \in ℝ$
24		readdcl	$⊢ (γ \in ℝ \land \|L\| \in ℝ) \to γ + \|L\| \in ℝ$
25	20 23 24	sylancr	$⊢ φ \to γ + \|L\| \in ℝ$
26		readdcl	$⊢ (\frac{1}{2} \in ℝ \land γ + \|L\| \in ℝ) \to (\frac{1}{2}) + γ + \|L\| \in ℝ$
27	19 25 26	sylancr	$⊢ φ \to (\frac{1}{2}) + γ + \|L\| \in ℝ$
28		fzfid	$⊢ φ \to (1 \dots 2) \in Fin$
29		epr	$⊢ e \in ℝ^{+}$
30		elfznn	$⊢ m \in (1 \dots 2) \to m \in ℕ$
31	30	adantl	$⊢ (φ \land m \in (1 \dots 2)) \to m \in ℕ$
32	31	nnrpd	$⊢ (φ \land m \in (1 \dots 2)) \to m \in ℝ^{+}$
33		rpdivcl	$⊢ (e \in ℝ^{+} \land m \in ℝ^{+}) \to \frac{e}{m} \in ℝ^{+}$
34	29 32 33	sylancr	$⊢ (φ \land m \in (1 \dots 2)) \to \frac{e}{m} \in ℝ^{+}$
35	34	relogcld	$⊢ (φ \land m \in (1 \dots 2)) \to \log (\frac{e}{m}) \in ℝ$
36	35 31	nndivred	$⊢ (φ \land m \in (1 \dots 2)) \to \frac{\log (\frac{e}{m})}{m} \in ℝ$
37	28 36	fsumrecl	$⊢ φ \to \sum_{m = 1}^{2} (\frac{\log (\frac{e}{m})}{m}) \in ℝ$
38	27 37	readdcld	$⊢ φ \to (\frac{1}{2}) + (γ + \|L\|) + \sum_{m = 1}^{2} (\frac{\log (\frac{e}{m})}{m}) \in ℝ$
39	4 38	eqeltrid	$⊢ φ \to R \in ℝ$
40		remulcl	$⊢ (R \in ℝ \land 2 \in ℝ) \to R \cdot 2 \in ℝ$
41	39 6 40	sylancl	$⊢ φ \to R \cdot 2 \in ℝ$
42	41	adantr	$⊢ (φ \land x \in ℝ^{+}) \to R \cdot 2 \in ℝ$
43	6	a1i	$⊢ (φ \land x \in ℝ^{+}) \to 2 \in ℝ$
44		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
45		2cnd	$⊢ φ \to 2 \in ℂ$
46		o1const	$⊢ (ℝ^{+} \subseteq ℝ \land 2 \in ℂ) \to (x \in ℝ^{+} ⟼ 2) \in 𝑂 (1)$
47	44 45 46	sylancr	$⊢ φ \to (x \in ℝ^{+} ⟼ 2) \in 𝑂 (1)$
48		logfacrlim2	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x})) \underset{ℝ}{⇝} 1$
49		rlimo1	$⊢ (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x})) \underset{ℝ}{⇝} 1 \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x})) \in 𝑂 (1)$
50	48 49	mp1i	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x})) \in 𝑂 (1)$
51	43 16 47 50	o1mul2	$⊢ φ \to (x \in ℝ^{+} ⟼ 2 \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x})) \in 𝑂 (1)$
52	41	recnd	$⊢ φ \to R \cdot 2 \in ℂ$
53		o1const	$⊢ (ℝ^{+} \subseteq ℝ \land R \cdot 2 \in ℂ) \to (x \in ℝ^{+} ⟼ R \cdot 2) \in 𝑂 (1)$
54	44 52 53	sylancr	$⊢ φ \to (x \in ℝ^{+} ⟼ R \cdot 2) \in 𝑂 (1)$
55	18 42 51 54	o1add2	$⊢ φ \to (x \in ℝ^{+} ⟼ 2 \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x}) + R \cdot 2) \in 𝑂 (1)$
56	18 42	readdcld	$⊢ (φ \land x \in ℝ^{+}) \to 2 \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x}) + R \cdot 2 \in ℝ$
57	9	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
58		mucl	$⊢ n \in ℕ \to μ (n) \in ℤ$
59	57 58	syl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℤ$
60	59	zred	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℝ$
61	60 57	nndivred	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{μ (n)}{n} \in ℝ$
62	61	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{μ (n)}{n} \in ℂ$
63	13	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{n}) \in ℂ$
64	63	sqcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to {\log (\frac{x}{n})}^{2} \in ℂ$
65	64	halfcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{{\log (\frac{x}{n})}^{2}}{2} \in ℂ$
66		remulcl	$⊢ (γ \in ℝ \land \log (\frac{x}{n}) \in ℝ) \to γ \log (\frac{x}{n}) \in ℝ$
67	20 13 66	sylancr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to γ \log (\frac{x}{n}) \in ℝ$
68	67	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to γ \log (\frac{x}{n}) \in ℂ$
69	22	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to L \in ℂ$
70	68 69	subcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to γ \log (\frac{x}{n}) - L \in ℂ$
71	65 70	addcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L \in ℂ$
72	3 71	eqeltrid	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to T \in ℂ$
73	62 72	mulcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) T \in ℂ$
74	7 73	fsumcl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) T \in ℂ$
75		relogcl	$⊢ x \in ℝ^{+} \to \log x \in ℝ$
76	75	adantl	$⊢ (φ \land x \in ℝ^{+}) \to \log x \in ℝ$
77	76	recnd	$⊢ (φ \land x \in ℝ^{+}) \to \log x \in ℂ$
78	74 77	subcld	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) T - \log x \in ℂ$
79	78	abscld	$⊢ (φ \land x \in ℝ^{+}) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) T - \log x\| \in ℝ$
80	79	adantrr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) T - \log x\| \in ℝ$
81	56	adantrr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to 2 \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x}) + R \cdot 2 \in ℝ$
82	56	recnd	$⊢ (φ \land x \in ℝ^{+}) \to 2 \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x}) + R \cdot 2 \in ℂ$
83	82	abscld	$⊢ (φ \land x \in ℝ^{+}) \to \|2 \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x}) + R \cdot 2\| \in ℝ$
84	83	adantrr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|2 \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x}) + R \cdot 2\| \in ℝ$
85	59	zcnd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℂ$
86		fzfid	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (1 \dots ⌊\frac{x}{n}⌋) \in Fin$
87		elfznn	$⊢ m \in (1 \dots ⌊\frac{x}{n}⌋) \to m \in ℕ$
88		nnrp	$⊢ m \in ℕ \to m \in ℝ^{+}$
89		rpdivcl	$⊢ (\frac{x}{n} \in ℝ^{+} \land m \in ℝ^{+}) \to \frac{\frac{x}{n}}{m} \in ℝ^{+}$
90	12 88 89	syl2an	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in ℕ) \to \frac{\frac{x}{n}}{m} \in ℝ^{+}$
91	90	relogcld	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in ℕ) \to \log (\frac{\frac{x}{n}}{m}) \in ℝ$
92		simpr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in ℕ) \to m \in ℕ$
93	91 92	nndivred	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in ℕ) \to \frac{\log (\frac{\frac{x}{n}}{m})}{m} \in ℝ$
94	93	recnd	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in ℕ) \to \frac{\log (\frac{\frac{x}{n}}{m})}{m} \in ℂ$
95	87 94	sylan2	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{\log (\frac{\frac{x}{n}}{m})}{m} \in ℂ$
96	86 95	fsumcl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) \in ℂ$
97	72 96	subcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) \in ℂ$
98	57	nncnd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to n \in ℂ$
99	57	nnne0d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to n \neq 0$
100	85 97 98 99	div23d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{μ (n) (T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}))}{n} = (\frac{μ (n)}{n}) (T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}))$
101	62 72 96	subdid	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) (T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})) = (\frac{μ (n)}{n}) T - (\frac{μ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})$
102	100 101	eqtrd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{μ (n) (T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}))}{n} = (\frac{μ (n)}{n}) T - (\frac{μ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})$
103	102	sumeq2dv	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n) (T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}))}{n}) = \sum_{n = 1}^{⌊x⌋} ((\frac{μ (n)}{n}) T - (\frac{μ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}))$
104	62 96	mulcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) \in ℂ$
105	7 73 104	fsumsub	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} ((\frac{μ (n)}{n}) T - (\frac{μ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})) = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) T - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})$
106	103 105	eqtrd	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n) (T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}))}{n}) = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) T - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})$
107	106	adantrr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n) (T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}))}{n}) = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) T - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})$
108	86 62 95	fsummulc2	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) = \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{μ (n)}{n}) (\frac{\log (\frac{\frac{x}{n}}{m})}{m})$
109	85	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in ℕ) \to μ (n) \in ℂ$
110	98 99	jca	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (n \in ℂ \land n \neq 0)$
111	110	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in ℕ) \to (n \in ℂ \land n \neq 0)$
112		div23	$⊢ (μ (n) \in ℂ \land \frac{\log (\frac{\frac{x}{n}}{m})}{m} \in ℂ \land (n \in ℂ \land n \neq 0)) \to \frac{μ (n) (\frac{\log (\frac{\frac{x}{n}}{m})}{m})}{n} = (\frac{μ (n)}{n}) (\frac{\log (\frac{\frac{x}{n}}{m})}{m})$
113		divass	$⊢ (μ (n) \in ℂ \land \frac{\log (\frac{\frac{x}{n}}{m})}{m} \in ℂ \land (n \in ℂ \land n \neq 0)) \to \frac{μ (n) (\frac{\log (\frac{\frac{x}{n}}{m})}{m})}{n} = μ (n) (\frac{\frac{\log (\frac{\frac{x}{n}}{m})}{m}}{n})$
114	112 113	eqtr3d	$⊢ (μ (n) \in ℂ \land \frac{\log (\frac{\frac{x}{n}}{m})}{m} \in ℂ \land (n \in ℂ \land n \neq 0)) \to (\frac{μ (n)}{n}) (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) = μ (n) (\frac{\frac{\log (\frac{\frac{x}{n}}{m})}{m}}{n})$
115	109 94 111 114	syl3anc	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in ℕ) \to (\frac{μ (n)}{n}) (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) = μ (n) (\frac{\frac{\log (\frac{\frac{x}{n}}{m})}{m}}{n})$
116	91	recnd	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in ℕ) \to \log (\frac{\frac{x}{n}}{m}) \in ℂ$
117	92	nnrpd	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in ℕ) \to m \in ℝ^{+}$
118		rpcnne0	$⊢ m \in ℝ^{+} \to (m \in ℂ \land m \neq 0)$
119	117 118	syl	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in ℕ) \to (m \in ℂ \land m \neq 0)$
120		divdiv1	$⊢ (\log (\frac{\frac{x}{n}}{m}) \in ℂ \land (m \in ℂ \land m \neq 0) \land (n \in ℂ \land n \neq 0)) \to \frac{\frac{\log (\frac{\frac{x}{n}}{m})}{m}}{n} = \frac{\log (\frac{\frac{x}{n}}{m})}{m n}$
121	116 119 111 120	syl3anc	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in ℕ) \to \frac{\frac{\log (\frac{\frac{x}{n}}{m})}{m}}{n} = \frac{\log (\frac{\frac{x}{n}}{m})}{m n}$
122		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
123	122	adantl	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ$
124	123	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to x \in ℝ$
125	124	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to x \in ℂ$
126	125	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in ℕ) \to x \in ℂ$
127		divdiv1	$⊢ (x \in ℂ \land (n \in ℂ \land n \neq 0) \land (m \in ℂ \land m \neq 0)) \to \frac{\frac{x}{n}}{m} = \frac{x}{n m}$
128	126 111 119 127	syl3anc	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in ℕ) \to \frac{\frac{x}{n}}{m} = \frac{x}{n m}$
129	128	fveq2d	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in ℕ) \to \log (\frac{\frac{x}{n}}{m}) = \log (\frac{x}{n m})$
130	92	nncnd	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in ℕ) \to m \in ℂ$
131	98	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in ℕ) \to n \in ℂ$
132	130 131	mulcomd	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in ℕ) \to m n = n m$
133	129 132	oveq12d	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in ℕ) \to \frac{\log (\frac{\frac{x}{n}}{m})}{m n} = \frac{\log (\frac{x}{n m})}{n m}$
134	121 133	eqtrd	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in ℕ) \to \frac{\frac{\log (\frac{\frac{x}{n}}{m})}{m}}{n} = \frac{\log (\frac{x}{n m})}{n m}$
135	134	oveq2d	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in ℕ) \to μ (n) (\frac{\frac{\log (\frac{\frac{x}{n}}{m})}{m}}{n}) = μ (n) (\frac{\log (\frac{x}{n m})}{n m})$
136	115 135	eqtrd	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in ℕ) \to (\frac{μ (n)}{n}) (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) = μ (n) (\frac{\log (\frac{x}{n m})}{n m})$
137	87 136	sylan2	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to (\frac{μ (n)}{n}) (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) = μ (n) (\frac{\log (\frac{x}{n m})}{n m})$
138	137	sumeq2dv	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{μ (n)}{n}) (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) = \sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) (\frac{\log (\frac{x}{n m})}{n m})$
139	108 138	eqtrd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (\frac{μ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) = \sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) (\frac{\log (\frac{x}{n m})}{n m})$
140	139	sumeq2dv	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) = \sum_{n = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) (\frac{\log (\frac{x}{n m})}{n m})$
141		oveq2	$⊢ k = n m \to \frac{x}{k} = \frac{x}{n m}$
142	141	fveq2d	$⊢ k = n m \to \log (\frac{x}{k}) = \log (\frac{x}{n m})$
143		id	$⊢ k = n m \to k = n m$
144	142 143	oveq12d	$⊢ k = n m \to \frac{\log (\frac{x}{k})}{k} = \frac{\log (\frac{x}{n m})}{n m}$
145	144	oveq2d	$⊢ k = n m \to μ (n) (\frac{\log (\frac{x}{k})}{k}) = μ (n) (\frac{\log (\frac{x}{n m})}{n m})$
146	8	rpred	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ$
147		ssrab2	$⊢ \{y \in ℕ \| y ∥ k\} \subseteq ℕ$
148		simprr	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to n \in \{y \in ℕ \| y ∥ k\}$
149	147 148	sselid	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to n \in ℕ$
150	149 58	syl	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to μ (n) \in ℤ$
151	150	zred	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to μ (n) \in ℝ$
152		elfznn	$⊢ k \in (1 \dots ⌊x⌋) \to k \in ℕ$
153	152	adantr	$⊢ (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\}) \to k \in ℕ$
154	153	nnrpd	$⊢ (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\}) \to k \in ℝ^{+}$
155		rpdivcl	$⊢ (x \in ℝ^{+} \land k \in ℝ^{+}) \to \frac{x}{k} \in ℝ^{+}$
156	8 154 155	syl2an	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to \frac{x}{k} \in ℝ^{+}$
157	156	relogcld	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to \log (\frac{x}{k}) \in ℝ$
158	152	ad2antrl	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to k \in ℕ$
159	157 158	nndivred	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to \frac{\log (\frac{x}{k})}{k} \in ℝ$
160	151 159	remulcld	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to μ (n) (\frac{\log (\frac{x}{k})}{k}) \in ℝ$
161	160	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land (k \in (1 \dots ⌊x⌋) \land n \in \{y \in ℕ \| y ∥ k\})) \to μ (n) (\frac{\log (\frac{x}{k})}{k}) \in ℂ$
162	145 146 161	dvdsflsumcom	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{k = 1}^{⌊x⌋} \sum_{n \in \{y \in ℕ \| y ∥ k\}} μ (n) (\frac{\log (\frac{x}{k})}{k}) = \sum_{n = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{n}⌋} μ (n) (\frac{\log (\frac{x}{n m})}{n m})$
163	140 162	eqtr4d	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) = \sum_{k = 1}^{⌊x⌋} \sum_{n \in \{y \in ℕ \| y ∥ k\}} μ (n) (\frac{\log (\frac{x}{k})}{k})$
164	163	adantrr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) = \sum_{k = 1}^{⌊x⌋} \sum_{n \in \{y \in ℕ \| y ∥ k\}} μ (n) (\frac{\log (\frac{x}{k})}{k})$
165		oveq2	$⊢ k = 1 \to \frac{x}{k} = \frac{x}{1}$
166	165	fveq2d	$⊢ k = 1 \to \log (\frac{x}{k}) = \log (\frac{x}{1})$
167		id	$⊢ k = 1 \to k = 1$
168	166 167	oveq12d	$⊢ k = 1 \to \frac{\log (\frac{x}{k})}{k} = \frac{\log (\frac{x}{1})}{1}$
169		fzfid	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (1 \dots ⌊x⌋) \in Fin$
170		fz1ssnn	$⊢ (1 \dots ⌊x⌋) \subseteq ℕ$
171	170	a1i	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to (1 \dots ⌊x⌋) \subseteq ℕ$
172	123	adantrr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to x \in ℝ$
173		simprr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 \leq x$
174		flge1nn	$⊢ (x \in ℝ \land 1 \leq x) \to ⌊x⌋ \in ℕ$
175	172 173 174	syl2anc	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to ⌊x⌋ \in ℕ$
176		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
177	175 176	eleqtrdi	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to ⌊x⌋ \in ℤ_{\geq 1}$
178		eluzfz1	$⊢ ⌊x⌋ \in ℤ_{\geq 1} \to 1 \in (1 \dots ⌊x⌋)$
179	177 178	syl	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 \in (1 \dots ⌊x⌋)$
180	152	nnrpd	$⊢ k \in (1 \dots ⌊x⌋) \to k \in ℝ^{+}$
181	8 180 155	syl2an	$⊢ ((φ \land x \in ℝ^{+}) \land k \in (1 \dots ⌊x⌋)) \to \frac{x}{k} \in ℝ^{+}$
182	181	relogcld	$⊢ ((φ \land x \in ℝ^{+}) \land k \in (1 \dots ⌊x⌋)) \to \log (\frac{x}{k}) \in ℝ$
183	170	a1i	$⊢ (φ \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \subseteq ℕ$
184	183	sselda	$⊢ ((φ \land x \in ℝ^{+}) \land k \in (1 \dots ⌊x⌋)) \to k \in ℕ$
185	182 184	nndivred	$⊢ ((φ \land x \in ℝ^{+}) \land k \in (1 \dots ⌊x⌋)) \to \frac{\log (\frac{x}{k})}{k} \in ℝ$
186	185	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land k \in (1 \dots ⌊x⌋)) \to \frac{\log (\frac{x}{k})}{k} \in ℂ$
187	186	adantlrr	$⊢ ((φ \land (x \in ℝ^{+} \land 1 \leq x)) \land k \in (1 \dots ⌊x⌋)) \to \frac{\log (\frac{x}{k})}{k} \in ℂ$
188	168 169 171 179 187	musumsum	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{k = 1}^{⌊x⌋} \sum_{n \in \{y \in ℕ \| y ∥ k\}} μ (n) (\frac{\log (\frac{x}{k})}{k}) = \frac{\log (\frac{x}{1})}{1}$
189	8	rpcnd	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℂ$
190	189	div1d	$⊢ (φ \land x \in ℝ^{+}) \to \frac{x}{1} = x$
191	190	fveq2d	$⊢ (φ \land x \in ℝ^{+}) \to \log (\frac{x}{1}) = \log x$
192	191	oveq1d	$⊢ (φ \land x \in ℝ^{+}) \to \frac{\log (\frac{x}{1})}{1} = \frac{\log x}{1}$
193	77	div1d	$⊢ (φ \land x \in ℝ^{+}) \to \frac{\log x}{1} = \log x$
194	192 193	eqtrd	$⊢ (φ \land x \in ℝ^{+}) \to \frac{\log (\frac{x}{1})}{1} = \log x$
195	194	adantrr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{\log (\frac{x}{1})}{1} = \log x$
196	164 188 195	3eqtrd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) = \log x$
197	196	oveq2d	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) T - \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) T - \log x$
198	107 197	eqtrd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \sum_{n = 1}^{⌊x⌋} (\frac{μ (n) (T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}))}{n}) = \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) T - \log x$
199	198	fveq2d	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{μ (n) (T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}))}{n})\| = \|\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) T - \log x\|$
200		ere	$⊢ e \in ℝ$
201	200	a1i	$⊢ (φ \land x \in ℝ^{+}) \to e \in ℝ$
202		1re	$⊢ 1 \in ℝ$
203		1lt2	$⊢ 1 < 2$
204		egt2lt3	$⊢ (2 < e \land e < 3)$
205	204	simpli	$⊢ 2 < e$
206	202 6 200	lttri	$⊢ (1 < 2 \land 2 < e) \to 1 < e$
207	203 205 206	mp2an	$⊢ 1 < e$
208	202 200 207	ltleii	$⊢ 1 \leq e$
209	201 208	jctir	$⊢ (φ \land x \in ℝ^{+}) \to (e \in ℝ \land 1 \leq e)$
210	39	adantr	$⊢ (φ \land x \in ℝ^{+}) \to R \in ℝ$
211	19	a1i	$⊢ φ \to \frac{1}{2} \in ℝ$
212		1rp	$⊢ 1 \in ℝ^{+}$
213		rphalfcl	$⊢ 1 \in ℝ^{+} \to \frac{1}{2} \in ℝ^{+}$
214	212 213	ax-mp	$⊢ \frac{1}{2} \in ℝ^{+}$
215		rpge0	$⊢ \frac{1}{2} \in ℝ^{+} \to 0 \leq \frac{1}{2}$
216	214 215	mp1i	$⊢ φ \to 0 \leq \frac{1}{2}$
217	20	a1i	$⊢ φ \to γ \in ℝ$
218		0re	$⊢ 0 \in ℝ$
219		emgt0	$⊢ 0 < γ$
220	218 20 219	ltleii	$⊢ 0 \leq γ$
221	220	a1i	$⊢ φ \to 0 \leq γ$
222	22	absge0d	$⊢ φ \to 0 \leq \|L\|$
223	217 23 221 222	addge0d	$⊢ φ \to 0 \leq γ + \|L\|$
224	211 25 216 223	addge0d	$⊢ φ \to 0 \leq (\frac{1}{2}) + γ + \|L\|$
225		log1	$⊢ \log 1 = 0$
226	31	nncnd	$⊢ (φ \land m \in (1 \dots 2)) \to m \in ℂ$
227	226	mullidd	$⊢ (φ \land m \in (1 \dots 2)) \to 1 m = m$
228	32	rpred	$⊢ (φ \land m \in (1 \dots 2)) \to m \in ℝ$
229	6	a1i	$⊢ (φ \land m \in (1 \dots 2)) \to 2 \in ℝ$
230	200	a1i	$⊢ (φ \land m \in (1 \dots 2)) \to e \in ℝ$
231		elfzle2	$⊢ m \in (1 \dots 2) \to m \leq 2$
232	231	adantl	$⊢ (φ \land m \in (1 \dots 2)) \to m \leq 2$
233	6 200 205	ltleii	$⊢ 2 \leq e$
234	233	a1i	$⊢ (φ \land m \in (1 \dots 2)) \to 2 \leq e$
235	228 229 230 232 234	letrd	$⊢ (φ \land m \in (1 \dots 2)) \to m \leq e$
236	227 235	eqbrtrd	$⊢ (φ \land m \in (1 \dots 2)) \to 1 m \leq e$
237		1red	$⊢ (φ \land m \in (1 \dots 2)) \to 1 \in ℝ$
238	237 230 32	lemuldivd	$⊢ (φ \land m \in (1 \dots 2)) \to (1 m \leq e \leftrightarrow 1 \leq \frac{e}{m})$
239	236 238	mpbid	$⊢ (φ \land m \in (1 \dots 2)) \to 1 \leq \frac{e}{m}$
240		logleb	$⊢ (1 \in ℝ^{+} \land \frac{e}{m} \in ℝ^{+}) \to (1 \leq \frac{e}{m} \leftrightarrow \log 1 \leq \log (\frac{e}{m}))$
241	212 34 240	sylancr	$⊢ (φ \land m \in (1 \dots 2)) \to (1 \leq \frac{e}{m} \leftrightarrow \log 1 \leq \log (\frac{e}{m}))$
242	239 241	mpbid	$⊢ (φ \land m \in (1 \dots 2)) \to \log 1 \leq \log (\frac{e}{m})$
243	225 242	eqbrtrrid	$⊢ (φ \land m \in (1 \dots 2)) \to 0 \leq \log (\frac{e}{m})$
244	35 32 243	divge0d	$⊢ (φ \land m \in (1 \dots 2)) \to 0 \leq \frac{\log (\frac{e}{m})}{m}$
245	28 36 244	fsumge0	$⊢ φ \to 0 \leq \sum_{m = 1}^{2} (\frac{\log (\frac{e}{m})}{m})$
246	27 37 224 245	addge0d	$⊢ φ \to 0 \leq (\frac{1}{2}) + (γ + \|L\|) + \sum_{m = 1}^{2} (\frac{\log (\frac{e}{m})}{m})$
247	246 4	breqtrrdi	$⊢ φ \to 0 \leq R$
248	247	adantr	$⊢ (φ \land x \in ℝ^{+}) \to 0 \leq R$
249	210 248	jca	$⊢ (φ \land x \in ℝ^{+}) \to (R \in ℝ \land 0 \leq R)$
250	85 97	mulcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to μ (n) (T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})) \in ℂ$
251		remulcl	$⊢ (2 \in ℝ \land \frac{\log (\frac{x}{n})}{x} \in ℝ) \to 2 (\frac{\log (\frac{x}{n})}{x}) \in ℝ$
252	6 15 251	sylancr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 2 (\frac{\log (\frac{x}{n})}{x}) \in ℝ$
253	6	a1i	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 2 \in ℝ$
254		0le2	$⊢ 0 \leq 2$
255	254	a1i	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq 2$
256	98	mullidd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 1 n = n$
257		fznnfl	$⊢ x \in ℝ \to (n \in (1 \dots ⌊x⌋) \leftrightarrow (n \in ℕ \land n \leq x))$
258	123 257	syl	$⊢ (φ \land x \in ℝ^{+}) \to (n \in (1 \dots ⌊x⌋) \leftrightarrow (n \in ℕ \land n \leq x))$
259	258	simplbda	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to n \leq x$
260	256 259	eqbrtrd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 1 n \leq x$
261		1red	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 1 \in ℝ$
262	57	nnrpd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
263	261 124 262	lemuldivd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (1 n \leq x \leftrightarrow 1 \leq \frac{x}{n})$
264	260 263	mpbid	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 1 \leq \frac{x}{n}$
265		logleb	$⊢ (1 \in ℝ^{+} \land \frac{x}{n} \in ℝ^{+}) \to (1 \leq \frac{x}{n} \leftrightarrow \log 1 \leq \log (\frac{x}{n}))$
266	212 12 265	sylancr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (1 \leq \frac{x}{n} \leftrightarrow \log 1 \leq \log (\frac{x}{n}))$
267	264 266	mpbid	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \log 1 \leq \log (\frac{x}{n})$
268	225 267	eqbrtrrid	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \log (\frac{x}{n})$
269		rpregt0	$⊢ x \in ℝ^{+} \to (x \in ℝ \land 0 < x)$
270	269	ad2antlr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (x \in ℝ \land 0 < x)$
271		divge0	$⊢ ((\log (\frac{x}{n}) \in ℝ \land 0 \leq \log (\frac{x}{n})) \land (x \in ℝ \land 0 < x)) \to 0 \leq \frac{\log (\frac{x}{n})}{x}$
272	13 268 270 271	syl21anc	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \frac{\log (\frac{x}{n})}{x}$
273	253 15 255 272	mulge0d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq 2 (\frac{\log (\frac{x}{n})}{x})$
274	250	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|μ (n) (T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}))\| \in ℝ$
275	274	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land e \leq \frac{x}{n}) \to \|μ (n) (T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}))\| \in ℝ$
276	97	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land e \leq \frac{x}{n}) \to T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) \in ℂ$
277	276	abscld	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land e \leq \frac{x}{n}) \to \|T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\| \in ℝ$
278	262	rpred	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ$
279	252 278	remulcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 2 (\frac{\log (\frac{x}{n})}{x}) n \in ℝ$
280	279	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land e \leq \frac{x}{n}) \to 2 (\frac{\log (\frac{x}{n})}{x}) n \in ℝ$
281	85 97	absmuld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|μ (n) (T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}))\| = \|μ (n)\| \|T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\|$
282	85	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|μ (n)\| \in ℝ$
283	97	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\| \in ℝ$
284	97	absge0d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \|T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\|$
285		mule1	$⊢ n \in ℕ \to \|μ (n)\| \leq 1$
286	57 285	syl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|μ (n)\| \leq 1$
287	282 261 283 284 286	lemul1ad	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|μ (n)\| \|T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\| \leq 1 \|T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\|$
288	283	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\| \in ℂ$
289	288	mullidd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 1 \|T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\| = \|T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\|$
290	287 289	breqtrd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|μ (n)\| \|T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\| \leq \|T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\|$
291	281 290	eqbrtrd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|μ (n) (T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}))\| \leq \|T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\|$
292	291	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land e \leq \frac{x}{n}) \to \|μ (n) (T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}))\| \leq \|T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\|$
293	2	ad3antrrr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land e \leq \frac{x}{n}) \to F \underset{ℝ}{⇝} L$
294	12	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land e \leq \frac{x}{n}) \to \frac{x}{n} \in ℝ^{+}$
295		simpr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land e \leq \frac{x}{n}) \to e \leq \frac{x}{n}$
296	1 293 294 295	mulog2sumlem1	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land e \leq \frac{x}{n}) \to \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) - ((\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L)\| \leq 2 (\frac{\log (\frac{x}{n})}{\frac{x}{n}})$
297	72 96	abssubd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\| = \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) - T\|$
298	297	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land e \leq \frac{x}{n}) \to \|T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\| = \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) - T\|$
299	3	oveq2i	$⊢ \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) - T = \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) - ((\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L)$
300	299	fveq2i	$⊢ \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) - T\| = \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) - ((\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L)\|$
301	298 300	eqtrdi	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land e \leq \frac{x}{n}) \to \|T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\| = \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) - ((\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L)\|$
302		2cnd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 2 \in ℂ$
303	15	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{\log (\frac{x}{n})}{x} \in ℂ$
304	302 303 98	mulassd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 2 (\frac{\log (\frac{x}{n})}{x}) n = 2 (\frac{\log (\frac{x}{n})}{x}) n$
305		rpcnne0	$⊢ x \in ℝ^{+} \to (x \in ℂ \land x \neq 0)$
306	305	ad2antlr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (x \in ℂ \land x \neq 0)$
307		divdiv2	$⊢ (\log (\frac{x}{n}) \in ℂ \land (x \in ℂ \land x \neq 0) \land (n \in ℂ \land n \neq 0)) \to \frac{\log (\frac{x}{n})}{\frac{x}{n}} = \frac{\log (\frac{x}{n}) n}{x}$
308	63 306 110 307	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{\log (\frac{x}{n})}{\frac{x}{n}} = \frac{\log (\frac{x}{n}) n}{x}$
309		div23	$⊢ (\log (\frac{x}{n}) \in ℂ \land n \in ℂ \land (x \in ℂ \land x \neq 0)) \to \frac{\log (\frac{x}{n}) n}{x} = (\frac{\log (\frac{x}{n})}{x}) n$
310	63 98 306 309	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{\log (\frac{x}{n}) n}{x} = (\frac{\log (\frac{x}{n})}{x}) n$
311	308 310	eqtrd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{\log (\frac{x}{n})}{\frac{x}{n}} = (\frac{\log (\frac{x}{n})}{x}) n$
312	311	oveq2d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 2 (\frac{\log (\frac{x}{n})}{\frac{x}{n}}) = 2 (\frac{\log (\frac{x}{n})}{x}) n$
313	304 312	eqtr4d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 2 (\frac{\log (\frac{x}{n})}{x}) n = 2 (\frac{\log (\frac{x}{n})}{\frac{x}{n}})$
314	313	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land e \leq \frac{x}{n}) \to 2 (\frac{\log (\frac{x}{n})}{x}) n = 2 (\frac{\log (\frac{x}{n})}{\frac{x}{n}})$
315	296 301 314	3brtr4d	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land e \leq \frac{x}{n}) \to \|T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\| \leq 2 (\frac{\log (\frac{x}{n})}{x}) n$
316	275 277 280 292 315	letrd	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land e \leq \frac{x}{n}) \to \|μ (n) (T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}))\| \leq 2 (\frac{\log (\frac{x}{n})}{x}) n$
317	274	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|μ (n) (T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}))\| \in ℝ$
318	283	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\| \in ℝ$
319	39	ad3antrrr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to R \in ℝ$
320	291	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|μ (n) (T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}))\| \leq \|T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\|$
321	72	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to T \in ℂ$
322	321	abscld	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|T\| \in ℝ$
323	96	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) \in ℂ$
324	323	abscld	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\| \in ℝ$
325	322 324	readdcld	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|T\| + \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\| \in ℝ$
326	321 323	abs2dif2d	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\| \leq \|T\| + \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\|$
327	27	ad3antrrr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to (\frac{1}{2}) + γ + \|L\| \in ℝ$
328	37	ad3antrrr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \sum_{m = 1}^{2} (\frac{\log (\frac{e}{m})}{m}) \in ℝ$
329	3	fveq2i	$⊢ \|T\| = \|(\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L\|$
330	329 322	eqeltrrid	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|(\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L\| \in ℝ$
331	65	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \frac{{\log (\frac{x}{n})}^{2}}{2} \in ℂ$
332	331	abscld	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|\frac{{\log (\frac{x}{n})}^{2}}{2}\| \in ℝ$
333	70	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to γ \log (\frac{x}{n}) - L \in ℂ$
334	333	abscld	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|γ \log (\frac{x}{n}) - L\| \in ℝ$
335	332 334	readdcld	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|\frac{{\log (\frac{x}{n})}^{2}}{2}\| + \|γ \log (\frac{x}{n}) - L\| \in ℝ$
336	331 333	abstrid	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|(\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L\| \leq \|\frac{{\log (\frac{x}{n})}^{2}}{2}\| + \|γ \log (\frac{x}{n}) - L\|$
337	19	a1i	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \frac{1}{2} \in ℝ$
338	25	ad3antrrr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to γ + \|L\| \in ℝ$
339	13	resqcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to {\log (\frac{x}{n})}^{2} \in ℝ$
340	339	rehalfcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{{\log (\frac{x}{n})}^{2}}{2} \in ℝ$
341	13	sqge0d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq {\log (\frac{x}{n})}^{2}$
342		2pos	$⊢ 0 < 2$
343	6 342	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
344	343	a1i	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (2 \in ℝ \land 0 < 2)$
345		divge0	$⊢ (({\log (\frac{x}{n})}^{2} \in ℝ \land 0 \leq {\log (\frac{x}{n})}^{2}) \land (2 \in ℝ \land 0 < 2)) \to 0 \leq \frac{{\log (\frac{x}{n})}^{2}}{2}$
346	339 341 344 345	syl21anc	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \frac{{\log (\frac{x}{n})}^{2}}{2}$
347	340 346	absidd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|\frac{{\log (\frac{x}{n})}^{2}}{2}\| = \frac{{\log (\frac{x}{n})}^{2}}{2}$
348	347	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|\frac{{\log (\frac{x}{n})}^{2}}{2}\| = \frac{{\log (\frac{x}{n})}^{2}}{2}$
349	12	rpred	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ$
350		ltle	$⊢ (\frac{x}{n} \in ℝ \land e \in ℝ) \to (\frac{x}{n} < e \to \frac{x}{n} \leq e)$
351	349 200 350	sylancl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (\frac{x}{n} < e \to \frac{x}{n} \leq e)$
352	351	imp	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \frac{x}{n} \leq e$
353	12	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \frac{x}{n} \in ℝ^{+}$
354		logleb	$⊢ (\frac{x}{n} \in ℝ^{+} \land e \in ℝ^{+}) \to (\frac{x}{n} \leq e \leftrightarrow \log (\frac{x}{n}) \leq \log e)$
355	353 29 354	sylancl	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to (\frac{x}{n} \leq e \leftrightarrow \log (\frac{x}{n}) \leq \log e)$
356	352 355	mpbid	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \log (\frac{x}{n}) \leq \log e$
357		loge	$⊢ \log e = 1$
358	356 357	breqtrdi	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \log (\frac{x}{n}) \leq 1$
359		0le1	$⊢ 0 \leq 1$
360	359	a1i	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq 1$
361	13 261 268 360	le2sqd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (\log (\frac{x}{n}) \leq 1 \leftrightarrow {\log (\frac{x}{n})}^{2} \leq 1^{2})$
362	361	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to (\log (\frac{x}{n}) \leq 1 \leftrightarrow {\log (\frac{x}{n})}^{2} \leq 1^{2})$
363	358 362	mpbid	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to {\log (\frac{x}{n})}^{2} \leq 1^{2}$
364		sq1	$⊢ 1^{2} = 1$
365	363 364	breqtrdi	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to {\log (\frac{x}{n})}^{2} \leq 1$
366	339	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to {\log (\frac{x}{n})}^{2} \in ℝ$
367		1red	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to 1 \in ℝ$
368	343	a1i	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to (2 \in ℝ \land 0 < 2)$
369		lediv1	$⊢ ({\log (\frac{x}{n})}^{2} \in ℝ \land 1 \in ℝ \land (2 \in ℝ \land 0 < 2)) \to ({\log (\frac{x}{n})}^{2} \leq 1 \leftrightarrow \frac{{\log (\frac{x}{n})}^{2}}{2} \leq \frac{1}{2})$
370	366 367 368 369	syl3anc	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to ({\log (\frac{x}{n})}^{2} \leq 1 \leftrightarrow \frac{{\log (\frac{x}{n})}^{2}}{2} \leq \frac{1}{2})$
371	365 370	mpbid	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \frac{{\log (\frac{x}{n})}^{2}}{2} \leq \frac{1}{2}$
372	348 371	eqbrtrd	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|\frac{{\log (\frac{x}{n})}^{2}}{2}\| \leq \frac{1}{2}$
373	69	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|L\| \in ℝ$
374	67 373	readdcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to γ \log (\frac{x}{n}) + \|L\| \in ℝ$
375	374	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to γ \log (\frac{x}{n}) + \|L\| \in ℝ$
376	68	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to γ \log (\frac{x}{n}) \in ℂ$
377	22	ad3antrrr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to L \in ℂ$
378	376 377	abs2dif2d	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|γ \log (\frac{x}{n}) - L\| \leq \|γ \log (\frac{x}{n})\| + \|L\|$
379	20	a1i	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to γ \in ℝ$
380	220	a1i	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq γ$
381	379 13 380 268	mulge0d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq γ \log (\frac{x}{n})$
382	67 381	absidd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \|γ \log (\frac{x}{n})\| = γ \log (\frac{x}{n})$
383	382	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|γ \log (\frac{x}{n})\| = γ \log (\frac{x}{n})$
384	383	oveq1d	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|γ \log (\frac{x}{n})\| + \|L\| = γ \log (\frac{x}{n}) + \|L\|$
385	378 384	breqtrd	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|γ \log (\frac{x}{n}) - L\| \leq γ \log (\frac{x}{n}) + \|L\|$
386	67	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to γ \log (\frac{x}{n}) \in ℝ$
387	20	a1i	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to γ \in ℝ$
388	377	abscld	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|L\| \in ℝ$
389	13	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \log (\frac{x}{n}) \in ℝ$
390	387 219	jctir	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to (γ \in ℝ \land 0 < γ)$
391		lemul2	$⊢ (\log (\frac{x}{n}) \in ℝ \land 1 \in ℝ \land (γ \in ℝ \land 0 < γ)) \to (\log (\frac{x}{n}) \leq 1 \leftrightarrow γ \log (\frac{x}{n}) \leq γ \cdot 1)$
392	389 367 390 391	syl3anc	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to (\log (\frac{x}{n}) \leq 1 \leftrightarrow γ \log (\frac{x}{n}) \leq γ \cdot 1)$
393	358 392	mpbid	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to γ \log (\frac{x}{n}) \leq γ \cdot 1$
394	20	recni	$⊢ γ \in ℂ$
395	394	mulridi	$⊢ γ \cdot 1 = γ$
396	393 395	breqtrdi	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to γ \log (\frac{x}{n}) \leq γ$
397	386 387 388 396	leadd1dd	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to γ \log (\frac{x}{n}) + \|L\| \leq γ + \|L\|$
398	334 375 338 385 397	letrd	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|γ \log (\frac{x}{n}) - L\| \leq γ + \|L\|$
399	332 334 337 338 372 398	le2addd	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|\frac{{\log (\frac{x}{n})}^{2}}{2}\| + \|γ \log (\frac{x}{n}) - L\| \leq (\frac{1}{2}) + γ + \|L\|$
400	330 335 327 336 399	letrd	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|(\frac{{\log (\frac{x}{n})}^{2}}{2}) + γ \log (\frac{x}{n}) - L\| \leq (\frac{1}{2}) + γ + \|L\|$
401	329 400	eqbrtrid	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|T\| \leq (\frac{1}{2}) + γ + \|L\|$
402	87 93	sylan2	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{\log (\frac{\frac{x}{n}}{m})}{m} \in ℝ$
403	86 402	fsumrecl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) \in ℝ$
404	403	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) \in ℝ$
405	87 91	sylan2	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \log (\frac{\frac{x}{n}}{m}) \in ℝ$
406	87 130	sylan2	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to m \in ℂ$
407	406	mullidd	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to 1 m = m$
408		fznnfl	$⊢ \frac{x}{n} \in ℝ \to (m \in (1 \dots ⌊\frac{x}{n}⌋) \leftrightarrow (m \in ℕ \land m \leq \frac{x}{n}))$
409	349 408	syl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to (m \in (1 \dots ⌊\frac{x}{n}⌋) \leftrightarrow (m \in ℕ \land m \leq \frac{x}{n}))$
410	409	simplbda	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to m \leq \frac{x}{n}$
411	407 410	eqbrtrd	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to 1 m \leq \frac{x}{n}$
412		1red	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to 1 \in ℝ$
413	349	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{x}{n} \in ℝ$
414	117	rpregt0d	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in ℕ) \to (m \in ℝ \land 0 < m)$
415	87 414	sylan2	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to (m \in ℝ \land 0 < m)$
416		lemuldiv	$⊢ (1 \in ℝ \land \frac{x}{n} \in ℝ \land (m \in ℝ \land 0 < m)) \to (1 m \leq \frac{x}{n} \leftrightarrow 1 \leq \frac{\frac{x}{n}}{m})$
417	412 413 415 416	syl3anc	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to (1 m \leq \frac{x}{n} \leftrightarrow 1 \leq \frac{\frac{x}{n}}{m})$
418	411 417	mpbid	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to 1 \leq \frac{\frac{x}{n}}{m}$
419	87 90	sylan2	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{\frac{x}{n}}{m} \in ℝ^{+}$
420		logleb	$⊢ (1 \in ℝ^{+} \land \frac{\frac{x}{n}}{m} \in ℝ^{+}) \to (1 \leq \frac{\frac{x}{n}}{m} \leftrightarrow \log 1 \leq \log (\frac{\frac{x}{n}}{m}))$
421	212 419 420	sylancr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to (1 \leq \frac{\frac{x}{n}}{m} \leftrightarrow \log 1 \leq \log (\frac{\frac{x}{n}}{m}))$
422	418 421	mpbid	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \log 1 \leq \log (\frac{\frac{x}{n}}{m})$
423	225 422	eqbrtrrid	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to 0 \leq \log (\frac{\frac{x}{n}}{m})$
424		divge0	$⊢ ((\log (\frac{\frac{x}{n}}{m}) \in ℝ \land 0 \leq \log (\frac{\frac{x}{n}}{m})) \land (m \in ℝ \land 0 < m)) \to 0 \leq \frac{\log (\frac{\frac{x}{n}}{m})}{m}$
425	405 423 415 424	syl21anc	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to 0 \leq \frac{\log (\frac{\frac{x}{n}}{m})}{m}$
426	86 402 425	fsumge0	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})$
427	426	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to 0 \leq \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})$
428	404 427	absidd	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\| = \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})$
429		fzfid	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to (1 \dots ⌊\frac{x}{n}⌋) \in Fin$
430	349	flcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to ⌊\frac{x}{n}⌋ \in ℤ$
431	430	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to ⌊\frac{x}{n}⌋ \in ℤ$
432		2z	$⊢ 2 \in ℤ$
433	432	a1i	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to 2 \in ℤ$
434	349	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \frac{x}{n} \in ℝ$
435	200	a1i	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to e \in ℝ$
436		3re	$⊢ 3 \in ℝ$
437	436	a1i	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to 3 \in ℝ$
438		simpr	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \frac{x}{n} < e$
439	204	simpri	$⊢ e < 3$
440	439	a1i	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to e < 3$
441	434 435 437 438 440	lttrd	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \frac{x}{n} < 3$
442		3z	$⊢ 3 \in ℤ$
443		fllt	$⊢ (\frac{x}{n} \in ℝ \land 3 \in ℤ) \to (\frac{x}{n} < 3 \leftrightarrow ⌊\frac{x}{n}⌋ < 3)$
444	434 442 443	sylancl	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to (\frac{x}{n} < 3 \leftrightarrow ⌊\frac{x}{n}⌋ < 3)$
445	441 444	mpbid	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to ⌊\frac{x}{n}⌋ < 3$
446		df-3	$⊢ 3 = 2 + 1$
447	445 446	breqtrdi	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to ⌊\frac{x}{n}⌋ < 2 + 1$
448		zleltp1	$⊢ (⌊\frac{x}{n}⌋ \in ℤ \land 2 \in ℤ) \to (⌊\frac{x}{n}⌋ \leq 2 \leftrightarrow ⌊\frac{x}{n}⌋ < 2 + 1)$
449	431 432 448	sylancl	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to (⌊\frac{x}{n}⌋ \leq 2 \leftrightarrow ⌊\frac{x}{n}⌋ < 2 + 1)$
450	447 449	mpbird	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to ⌊\frac{x}{n}⌋ \leq 2$
451		eluz2	$⊢ 2 \in ℤ_{\geq ⌊\frac{x}{n}⌋} \leftrightarrow (⌊\frac{x}{n}⌋ \in ℤ \land 2 \in ℤ \land ⌊\frac{x}{n}⌋ \leq 2)$
452	431 433 450 451	syl3anbrc	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to 2 \in ℤ_{\geq ⌊\frac{x}{n}⌋}$
453		fzss2	$⊢ 2 \in ℤ_{\geq ⌊\frac{x}{n}⌋} \to (1 \dots ⌊\frac{x}{n}⌋) \subseteq (1 \dots 2)$
454	452 453	syl	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to (1 \dots ⌊\frac{x}{n}⌋) \subseteq (1 \dots 2)$
455	454	sselda	$⊢ ((((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to m \in (1 \dots 2)$
456	36	ad5ant15	$⊢ ((((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \land m \in (1 \dots 2)) \to \frac{\log (\frac{e}{m})}{m} \in ℝ$
457	455 456	syldan	$⊢ ((((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{\log (\frac{e}{m})}{m} \in ℝ$
458	429 457	fsumrecl	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{e}{m})}{m}) \in ℝ$
459	93	adantlr	$⊢ ((((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \land m \in ℕ) \to \frac{\log (\frac{\frac{x}{n}}{m})}{m} \in ℝ$
460	87 459	sylan2	$⊢ ((((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{\log (\frac{\frac{x}{n}}{m})}{m} \in ℝ$
461	352	adantr	$⊢ ((((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \land m \in (1 \dots 2)) \to \frac{x}{n} \leq e$
462	434	adantr	$⊢ ((((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \land m \in (1 \dots 2)) \to \frac{x}{n} \in ℝ$
463	200	a1i	$⊢ ((((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \land m \in (1 \dots 2)) \to e \in ℝ$
464	32	rpregt0d	$⊢ (φ \land m \in (1 \dots 2)) \to (m \in ℝ \land 0 < m)$
465	464	ad5ant15	$⊢ ((((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \land m \in (1 \dots 2)) \to (m \in ℝ \land 0 < m)$
466		lediv1	$⊢ (\frac{x}{n} \in ℝ \land e \in ℝ \land (m \in ℝ \land 0 < m)) \to (\frac{x}{n} \leq e \leftrightarrow \frac{\frac{x}{n}}{m} \leq \frac{e}{m})$
467	462 463 465 466	syl3anc	$⊢ ((((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \land m \in (1 \dots 2)) \to (\frac{x}{n} \leq e \leftrightarrow \frac{\frac{x}{n}}{m} \leq \frac{e}{m})$
468	461 467	mpbid	$⊢ ((((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \land m \in (1 \dots 2)) \to \frac{\frac{x}{n}}{m} \leq \frac{e}{m}$
469	90	adantlr	$⊢ ((((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \land m \in ℕ) \to \frac{\frac{x}{n}}{m} \in ℝ^{+}$
470	30 469	sylan2	$⊢ ((((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \land m \in (1 \dots 2)) \to \frac{\frac{x}{n}}{m} \in ℝ^{+}$
471	34	ad5ant15	$⊢ ((((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \land m \in (1 \dots 2)) \to \frac{e}{m} \in ℝ^{+}$
472	470 471	logled	$⊢ ((((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \land m \in (1 \dots 2)) \to (\frac{\frac{x}{n}}{m} \leq \frac{e}{m} \leftrightarrow \log (\frac{\frac{x}{n}}{m}) \leq \log (\frac{e}{m}))$
473	468 472	mpbid	$⊢ ((((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \land m \in (1 \dots 2)) \to \log (\frac{\frac{x}{n}}{m}) \leq \log (\frac{e}{m})$
474	91	adantlr	$⊢ ((((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \land m \in ℕ) \to \log (\frac{\frac{x}{n}}{m}) \in ℝ$
475	30 474	sylan2	$⊢ ((((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \land m \in (1 \dots 2)) \to \log (\frac{\frac{x}{n}}{m}) \in ℝ$
476	35	ad5ant15	$⊢ ((((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \land m \in (1 \dots 2)) \to \log (\frac{e}{m}) \in ℝ$
477		lediv1	$⊢ (\log (\frac{\frac{x}{n}}{m}) \in ℝ \land \log (\frac{e}{m}) \in ℝ \land (m \in ℝ \land 0 < m)) \to (\log (\frac{\frac{x}{n}}{m}) \leq \log (\frac{e}{m}) \leftrightarrow \frac{\log (\frac{\frac{x}{n}}{m})}{m} \leq \frac{\log (\frac{e}{m})}{m})$
478	475 476 465 477	syl3anc	$⊢ ((((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \land m \in (1 \dots 2)) \to (\log (\frac{\frac{x}{n}}{m}) \leq \log (\frac{e}{m}) \leftrightarrow \frac{\log (\frac{\frac{x}{n}}{m})}{m} \leq \frac{\log (\frac{e}{m})}{m})$
479	473 478	mpbid	$⊢ ((((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \land m \in (1 \dots 2)) \to \frac{\log (\frac{\frac{x}{n}}{m})}{m} \leq \frac{\log (\frac{e}{m})}{m}$
480	455 479	syldan	$⊢ ((((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \land m \in (1 \dots ⌊\frac{x}{n}⌋)) \to \frac{\log (\frac{\frac{x}{n}}{m})}{m} \leq \frac{\log (\frac{e}{m})}{m}$
481	429 460 457 480	fsumle	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) \leq \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{e}{m})}{m})$
482		fzfid	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to (1 \dots 2) \in Fin$
483	244	ad5ant15	$⊢ ((((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \land m \in (1 \dots 2)) \to 0 \leq \frac{\log (\frac{e}{m})}{m}$
484	482 456 483 454	fsumless	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{e}{m})}{m}) \leq \sum_{m = 1}^{2} (\frac{\log (\frac{e}{m})}{m})$
485	404 458 328 481 484	letrd	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}) \leq \sum_{m = 1}^{2} (\frac{\log (\frac{e}{m})}{m})$
486	428 485	eqbrtrd	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\| \leq \sum_{m = 1}^{2} (\frac{\log (\frac{e}{m})}{m})$
487	322 324 327 328 401 486	le2addd	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|T\| + \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\| \leq (\frac{1}{2}) + (γ + \|L\|) + \sum_{m = 1}^{2} (\frac{\log (\frac{e}{m})}{m})$
488	487 4	breqtrrdi	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|T\| + \|\sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\| \leq R$
489	318 325 319 326 488	letrd	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m})\| \leq R$
490	317 318 319 320 489	letrd	$⊢ (((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \land \frac{x}{n} < e) \to \|μ (n) (T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}))\| \leq R$
491	8 209 249 250 252 273 316 490	fsumharmonic	$⊢ (φ \land x \in ℝ^{+}) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{μ (n) (T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}))}{n})\| \leq \sum_{n = 1}^{⌊x⌋} 2 (\frac{\log (\frac{x}{n})}{x}) + R (\log e + 1)$
492		2cnd	$⊢ (φ \land x \in ℝ^{+}) \to 2 \in ℂ$
493	7 492 303	fsummulc2	$⊢ (φ \land x \in ℝ^{+}) \to 2 \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x}) = \sum_{n = 1}^{⌊x⌋} 2 (\frac{\log (\frac{x}{n})}{x})$
494		df-2	$⊢ 2 = 1 + 1$
495	357	oveq1i	$⊢ \log e + 1 = 1 + 1$
496	494 495	eqtr4i	$⊢ 2 = \log e + 1$
497	496	a1i	$⊢ (φ \land x \in ℝ^{+}) \to 2 = \log e + 1$
498	497	oveq2d	$⊢ (φ \land x \in ℝ^{+}) \to R \cdot 2 = R (\log e + 1)$
499	493 498	oveq12d	$⊢ (φ \land x \in ℝ^{+}) \to 2 \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x}) + R \cdot 2 = \sum_{n = 1}^{⌊x⌋} 2 (\frac{\log (\frac{x}{n})}{x}) + R (\log e + 1)$
500	491 499	breqtrrd	$⊢ (φ \land x \in ℝ^{+}) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{μ (n) (T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}))}{n})\| \leq 2 \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x}) + R \cdot 2$
501	500	adantrr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{μ (n) (T - \sum_{m = 1}^{⌊\frac{x}{n}⌋} (\frac{\log (\frac{\frac{x}{n}}{m})}{m}))}{n})\| \leq 2 \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x}) + R \cdot 2$
502	199 501	eqbrtrrd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) T - \log x\| \leq 2 \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x}) + R \cdot 2$
503	56	leabsd	$⊢ (φ \land x \in ℝ^{+}) \to 2 \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x}) + R \cdot 2 \leq \|2 \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x}) + R \cdot 2\|$
504	503	adantrr	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to 2 \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x}) + R \cdot 2 \leq \|2 \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x}) + R \cdot 2\|$
505	80 81 84 502 504	letrd	$⊢ (φ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) T - \log x\| \leq \|2 \sum_{n = 1}^{⌊x⌋} (\frac{\log (\frac{x}{n})}{x}) + R \cdot 2\|$
506	5 55 56 78 505	o1le	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{μ (n)}{n}) T - \log x) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem mulog2sumlem2

Proof