Theorem mulog2sumlem2

Description: Lemma for mulog2sum . (Contributed by Mario Carneiro, 19-May-2016)

	Ref	Expression
Hypotheses	logdivsum.1	⊢ 𝐹 = ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑖 ) / 𝑖 ) − ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) )
	mulog2sumlem.1	⊢ ( 𝜑 → 𝐹 ⇝𝑟 𝐿 )
	mulog2sumlem2.t	⊢ 𝑇 = ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ ( 𝑥 / 𝑛 ) ) ) − 𝐿 ) )
	mulog2sumlem2.r	⊢ 𝑅 = ( ( ( 1 / 2 ) + ( γ + ( abs ‘ 𝐿 ) ) ) + Σ 𝑚 ∈ ( 1 ... 2 ) ( ( log ‘ ( e / 𝑚 ) ) / 𝑚 ) )
Assertion	mulog2sumlem2	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · 𝑇 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )

Proof

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