Theorem mulog2sumlem2 26114

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

Hypotheses

Ref	Expression
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

Ref	Expression
mulog2sumlem2	⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ∈ 𝑂(1))

Distinct variable groups:   𝑖,𝑚,𝑛,𝑥,𝑦   𝑥,𝐹   𝑛,𝐿,𝑥   𝜑,𝑚,𝑛,𝑥   𝑅,𝑛,𝑥

Allowed substitution hints:   𝜑(𝑦,𝑖)   𝑅(𝑦,𝑖,𝑚)   𝑇(𝑥,𝑦,𝑖,𝑚,𝑛)   𝐹(𝑦,𝑖,𝑚,𝑛)   𝐿(𝑦,𝑖,𝑚)

Proof of Theorem mulog2sumlem2

Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		1red 10645	. 2 ⊢ (𝜑 → 1 ∈ ℝ)
2		2re 11714	. . . 4 ⊢ 2 ∈ ℝ
3		fzfid 13344	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin)
4		simpr 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
5		elfznn 12939	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
6	5	nnrpd 12432	. . . . . . . 8 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℝ+)
7		rpdivcl 12417	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) → (𝑥 / 𝑛) ∈ ℝ+)
8	4, 6, 7	syl2an 597	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ+)
9	8	relogcld 25209	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
10		simplr 767	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ+)
11	9, 10	rerpdivcld 12465	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℝ)
12	3, 11	fsumrecl 15094	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℝ)
13		remulcl 10625	. . . 4 ⊢ ((2 ∈ ℝ ∧ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℝ) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ ℝ)
14	2, 12, 13	sylancr 589	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ ℝ)
15		mulog2sumlem2.r	. . . . . 6 ⊢ 𝑅 = (((1 / 2) + (γ + (abs‘𝐿))) + Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚))
16		halfre 11854	. . . . . . . 8 ⊢ (1 / 2) ∈ ℝ
17		emre 25586	. . . . . . . . 9 ⊢ γ ∈ ℝ
18		mulog2sumlem.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐿)
19		rlimcl 14863	. . . . . . . . . . 11 ⊢ (𝐹 ⇝𝑟 𝐿 → 𝐿 ∈ ℂ)
20	18, 19	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ ℂ)
21	20	abscld 14799	. . . . . . . . 9 ⊢ (𝜑 → (abs‘𝐿) ∈ ℝ)
22		readdcl 10623	. . . . . . . . 9 ⊢ ((γ ∈ ℝ ∧ (abs‘𝐿) ∈ ℝ) → (γ + (abs‘𝐿)) ∈ ℝ)
23	17, 21, 22	sylancr 589	. . . . . . . 8 ⊢ (𝜑 → (γ + (abs‘𝐿)) ∈ ℝ)
24		readdcl 10623	. . . . . . . 8 ⊢ (((1 / 2) ∈ ℝ ∧ (γ + (abs‘𝐿)) ∈ ℝ) → ((1 / 2) + (γ + (abs‘𝐿))) ∈ ℝ)
25	16, 23, 24	sylancr 589	. . . . . . 7 ⊢ (𝜑 → ((1 / 2) + (γ + (abs‘𝐿))) ∈ ℝ)
26		fzfid 13344	. . . . . . . 8 ⊢ (𝜑 → (1...2) ∈ Fin)
27		epr 15564	. . . . . . . . . . 11 ⊢ e ∈ ℝ+
28		elfznn 12939	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (1...2) → 𝑚 ∈ ℕ)
29	28	adantl 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ∈ ℕ)
30	29	nnrpd 12432	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ∈ ℝ+)
31		rpdivcl 12417	. . . . . . . . . . 11 ⊢ ((e ∈ ℝ+ ∧ 𝑚 ∈ ℝ+) → (e / 𝑚) ∈ ℝ+)
32	27, 30, 31	sylancr 589	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (e / 𝑚) ∈ ℝ+)
33	32	relogcld 25209	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (log‘(e / 𝑚)) ∈ ℝ)
34	33, 29	nndivred 11694	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → ((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
35	26, 34	fsumrecl 15094	. . . . . . 7 ⊢ (𝜑 → Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
36	25, 35	readdcld 10673	. . . . . 6 ⊢ (𝜑 → (((1 / 2) + (γ + (abs‘𝐿))) + Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚)) ∈ ℝ)
37	15, 36	eqeltrid 2920	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ ℝ)
38		remulcl 10625	. . . . 5 ⊢ ((𝑅 ∈ ℝ ∧ 2 ∈ ℝ) → (𝑅 · 2) ∈ ℝ)
39	37, 2, 38	sylancl 588	. . . 4 ⊢ (𝜑 → (𝑅 · 2) ∈ ℝ)
40	39	adantr 483	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑅 · 2) ∈ ℝ)
41	2	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 ∈ ℝ)
42		rpssre 12399	. . . . 5 ⊢ ℝ+ ⊆ ℝ
43		2cnd 11718	. . . . 5 ⊢ (𝜑 → 2 ∈ ℂ)
44		o1const 14979	. . . . 5 ⊢ ((ℝ+ ⊆ ℝ ∧ 2 ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ 2) ∈ 𝑂(1))
45	42, 43, 44	sylancr 589	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ 2) ∈ 𝑂(1))
46		logfacrlim2 25805	. . . . 5 ⊢ (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ⇝𝑟 1
47		rlimo1 14976	. . . . 5 ⊢ ((𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ⇝𝑟 1 → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ 𝑂(1))
48	46, 47	mp1i 13	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ 𝑂(1))
49	41, 12, 45, 48	o1mul2 14984	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥))) ∈ 𝑂(1))
50	39	recnd 10672	. . . 4 ⊢ (𝜑 → (𝑅 · 2) ∈ ℂ)
51		o1const 14979	. . . 4 ⊢ ((ℝ+ ⊆ ℝ ∧ (𝑅 · 2) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ (𝑅 · 2)) ∈ 𝑂(1))
52	42, 50, 51	sylancr 589	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (𝑅 · 2)) ∈ 𝑂(1))
53	14, 40, 49, 52	o1add2 14983	. 2 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))) ∈ 𝑂(1))
54	14, 40	readdcld 10673	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ∈ ℝ)
55	5	adantl 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
56		mucl 25721	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (μ‘𝑛) ∈ ℤ)
57	55, 56	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℤ)
58	57	zred 12090	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℝ)
59	58, 55	nndivred 11694	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℝ)
60	59	recnd 10672	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℂ)
61		mulog2sumlem2.t	. . . . . 6 ⊢ 𝑇 = ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿))
62	9	recnd 10672	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℂ)
63	62	sqcld 13511	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℂ)
64	63	halfcld 11885	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) / 2) ∈ ℂ)
65		remulcl 10625	. . . . . . . . . 10 ⊢ ((γ ∈ ℝ ∧ (log‘(𝑥 / 𝑛)) ∈ ℝ) → (γ · (log‘(𝑥 / 𝑛))) ∈ ℝ)
66	17, 9, 65	sylancr 589	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (γ · (log‘(𝑥 / 𝑛))) ∈ ℝ)
67	66	recnd 10672	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (γ · (log‘(𝑥 / 𝑛))) ∈ ℂ)
68	20	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝐿 ∈ ℂ)
69	67, 68	subcld 11000	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((γ · (log‘(𝑥 / 𝑛))) − 𝐿) ∈ ℂ)
70	64, 69	addcld 10663	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ∈ ℂ)
71	61, 70	eqeltrid 2920	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑇 ∈ ℂ)
72	60, 71	mulcld 10664	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · 𝑇) ∈ ℂ)
73	3, 72	fsumcl 15093	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) ∈ ℂ)
74		relogcl 25162	. . . . 5 ⊢ (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
75	74	adantl 484	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
76	75	recnd 10672	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℂ)
77	73, 76	subcld 11000	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥)) ∈ ℂ)
78	77	abscld 14799	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ∈ ℝ)
79	78	adantrr 715	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ∈ ℝ)
80	54	adantrr 715	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ∈ ℝ)
81	54	recnd 10672	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ∈ ℂ)
82	81	abscld 14799	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))) ∈ ℝ)
83	82	adantrr 715	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))) ∈ ℝ)
84	57	zcnd 12091	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℂ)
85		fzfid 13344	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
86		elfznn 12939	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) → 𝑚 ∈ ℕ)
87		nnrp 12403	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℝ+)
88		rpdivcl 12417	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 / 𝑛) ∈ ℝ+ ∧ 𝑚 ∈ ℝ+) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
89	8, 87, 88	syl2an 597	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
90	89	relogcld 25209	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
91		simpr 487	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℕ)
92	90, 91	nndivred 11694	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
93	92	recnd 10672	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ)
94	86, 93	sylan2 594	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ)
95	85, 94	fsumcl 15093	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ)
96	71, 95	subcld 11000	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ∈ ℂ)
97	55	nncnd 11657	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
98	55	nnne0d 11690	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0)
99	84, 96, 97, 98	div23d 11456	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = (((μ‘𝑛) / 𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
100	60, 71, 95	subdid 11099	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = ((((μ‘𝑛) / 𝑛) · 𝑇) − (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
101	99, 100	eqtrd 2859	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = ((((μ‘𝑛) / 𝑛) · 𝑇) − (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
102	101	sumeq2dv 15063	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))((((μ‘𝑛) / 𝑛) · 𝑇) − (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
103	60, 95	mulcld 10664	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ∈ ℂ)
104	3, 72, 103	fsumsub 15146	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((μ‘𝑛) / 𝑛) · 𝑇) − (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
105	102, 104	eqtrd 2859	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
106	105	adantrr 715	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
107	85, 60, 94	fsummulc2 15142	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))
108	84	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (μ‘𝑛) ∈ ℂ)
109	97, 98	jca 514	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
110	109	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
111		div23 11320	. . . . . . . . . . . . . . . . 17 ⊢ (((μ‘𝑛) ∈ ℂ ∧ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((μ‘𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) / 𝑛) = (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))
112		divass 11319	. . . . . . . . . . . . . . . . 17 ⊢ (((μ‘𝑛) ∈ ℂ ∧ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((μ‘𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) / 𝑛) = ((μ‘𝑛) · (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛)))
113	111, 112	eqtr3d 2861	. . . . . . . . . . . . . . . 16 ⊢ (((μ‘𝑛) ∈ ℂ ∧ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = ((μ‘𝑛) · (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛)))
114	108, 93, 110, 113	syl3anc 1367	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = ((μ‘𝑛) · (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛)))
115	90	recnd 10672	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℂ)
116	91	nnrpd 12432	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ+)
117		rpcnne0 12410	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ ℝ+ → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0))
118	116, 117	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0))
119		divdiv1 11354	. . . . . . . . . . . . . . . . . 18 ⊢ (((log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℂ ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0) ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛) = ((log‘((𝑥 / 𝑛) / 𝑚)) / (𝑚 · 𝑛)))
120	115, 118, 110, 119	syl3anc 1367	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛) = ((log‘((𝑥 / 𝑛) / 𝑚)) / (𝑚 · 𝑛)))
121		rpre 12400	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ)
122	121	adantl 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
123	122	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
124	123	recnd 10672	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℂ)
125	124	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → 𝑥 ∈ ℂ)
126		divdiv1 11354	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0) ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) → ((𝑥 / 𝑛) / 𝑚) = (𝑥 / (𝑛 · 𝑚)))
127	125, 110, 118, 126	syl3anc 1367	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((𝑥 / 𝑛) / 𝑚) = (𝑥 / (𝑛 · 𝑚)))
128	127	fveq2d 6677	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (log‘((𝑥 / 𝑛) / 𝑚)) = (log‘(𝑥 / (𝑛 · 𝑚))))
129	91	nncnd 11657	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
130	97	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → 𝑛 ∈ ℂ)
131	129, 130	mulcomd 10665	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (𝑚 · 𝑛) = (𝑛 · 𝑚))
132	128, 131	oveq12d 7177	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((log‘((𝑥 / 𝑛) / 𝑚)) / (𝑚 · 𝑛)) = ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚)))
133	120, 132	eqtrd 2859	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛) = ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚)))
134	133	oveq2d 7175	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((μ‘𝑛) · (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛)) = ((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
135	114, 134	eqtrd 2859	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = ((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
136	86, 135	sylan2 594	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = ((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
137	136	sumeq2dv 15063	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
138	107, 137	eqtrd 2859	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
139	138	sumeq2dv 15063	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
140		oveq2 7167	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑛 · 𝑚) → (𝑥 / 𝑘) = (𝑥 / (𝑛 · 𝑚)))
141	140	fveq2d 6677	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑛 · 𝑚) → (log‘(𝑥 / 𝑘)) = (log‘(𝑥 / (𝑛 · 𝑚))))
142		id 22	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑛 · 𝑚) → 𝑘 = (𝑛 · 𝑚))
143	141, 142	oveq12d 7177	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑛 · 𝑚) → ((log‘(𝑥 / 𝑘)) / 𝑘) = ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚)))
144	143	oveq2d 7175	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑛 · 𝑚) → ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) = ((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
145	4	rpred 12434	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
146		ssrab2 4059	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ ℕ
147		simprr 771	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})
148	146, 147	sseldi 3968	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ ℕ)
149	148, 56	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (μ‘𝑛) ∈ ℤ)
150	149	zred 12090	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (μ‘𝑛) ∈ ℝ)
151		elfznn 12939	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (1...(⌊‘𝑥)) → 𝑘 ∈ ℕ)
152	151	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → 𝑘 ∈ ℕ)
153	152	nnrpd 12432	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → 𝑘 ∈ ℝ+)
154		rpdivcl 12417	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑘 ∈ ℝ+) → (𝑥 / 𝑘) ∈ ℝ+)
155	4, 153, 154	syl2an 597	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (𝑥 / 𝑘) ∈ ℝ+)
156	155	relogcld 25209	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (log‘(𝑥 / 𝑘)) ∈ ℝ)
157	151	ad2antrl 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑘 ∈ ℕ)
158	156, 157	nndivred 11694	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → ((log‘(𝑥 / 𝑘)) / 𝑘) ∈ ℝ)
159	150, 158	remulcld 10674	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) ∈ ℝ)
160	159	recnd 10672	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) ∈ ℂ)
161	144, 145, 160	dvdsflsumcom 25768	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
162	139, 161	eqtr4d 2862	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)))
163	162	adantrr 715	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)))
164		oveq2 7167	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → (𝑥 / 𝑘) = (𝑥 / 1))
165	164	fveq2d 6677	. . . . . . . . . 10 ⊢ (𝑘 = 1 → (log‘(𝑥 / 𝑘)) = (log‘(𝑥 / 1)))
166		id 22	. . . . . . . . . 10 ⊢ (𝑘 = 1 → 𝑘 = 1)
167	165, 166	oveq12d 7177	. . . . . . . . 9 ⊢ (𝑘 = 1 → ((log‘(𝑥 / 𝑘)) / 𝑘) = ((log‘(𝑥 / 1)) / 1))
168		fzfid 13344	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin)
169		fz1ssnn 12941	. . . . . . . . . 10 ⊢ (1...(⌊‘𝑥)) ⊆ ℕ
170	169	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ⊆ ℕ)
171	122	adantrr 715	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ)
172		simprr 771	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥)
173		flge1nn 13194	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ)
174	171, 172, 173	syl2anc 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (⌊‘𝑥) ∈ ℕ)
175		nnuz 12284	. . . . . . . . . . 11 ⊢ ℕ = (ℤ≥‘1)
176	174, 175	eleqtrdi 2926	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (⌊‘𝑥) ∈ (ℤ≥‘1))
177		eluzfz1 12917	. . . . . . . . . 10 ⊢ ((⌊‘𝑥) ∈ (ℤ≥‘1) → 1 ∈ (1...(⌊‘𝑥)))
178	176, 177	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ (1...(⌊‘𝑥)))
179	151	nnrpd 12432	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1...(⌊‘𝑥)) → 𝑘 ∈ ℝ+)
180	4, 179, 154	syl2an 597	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑘) ∈ ℝ+)
181	180	relogcld 25209	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑘)) ∈ ℝ)
182	169	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ⊆ ℕ)
183	182	sselda 3970	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → 𝑘 ∈ ℕ)
184	181, 183	nndivred 11694	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑘)) / 𝑘) ∈ ℝ)
185	184	recnd 10672	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑘)) / 𝑘) ∈ ℂ)
186	185	adantlrr 719	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑘)) / 𝑘) ∈ ℂ)
187	167, 168, 170, 178, 186	musumsum 25772	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) = ((log‘(𝑥 / 1)) / 1))
188	4	rpcnd 12436	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
189	188	div1d 11411	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 / 1) = 𝑥)
190	189	fveq2d 6677	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (log‘(𝑥 / 1)) = (log‘𝑥))
191	190	oveq1d 7174	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((log‘(𝑥 / 1)) / 1) = ((log‘𝑥) / 1))
192	76	div1d 11411	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((log‘𝑥) / 1) = (log‘𝑥))
193	191, 192	eqtrd 2859	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((log‘(𝑥 / 1)) / 1) = (log‘𝑥))
194	193	adantrr 715	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘(𝑥 / 1)) / 1) = (log‘𝑥))
195	163, 187, 194	3eqtrd 2863	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = (log‘𝑥))
196	195	oveq2d 7175	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥)))
197	106, 196	eqtrd 2859	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥)))
198	197	fveq2d 6677	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛)) = (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))))
199		ere 15445	. . . . . . . . 9 ⊢ e ∈ ℝ
200	199	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → e ∈ ℝ)
201		1re 10644	. . . . . . . . 9 ⊢ 1 ∈ ℝ
202		1lt2 11811	. . . . . . . . . 10 ⊢ 1 < 2
203		egt2lt3 15562	. . . . . . . . . . 11 ⊢ (2 < e ∧ e < 3)
204	203	simpli 486	. . . . . . . . . 10 ⊢ 2 < e
205	201, 2, 199	lttri 10769	. . . . . . . . . 10 ⊢ ((1 < 2 ∧ 2 < e) → 1 < e)
206	202, 204, 205	mp2an 690	. . . . . . . . 9 ⊢ 1 < e
207	201, 199, 206	ltleii 10766	. . . . . . . 8 ⊢ 1 ≤ e
208	200, 207	jctir 523	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (e ∈ ℝ ∧ 1 ≤ e))
209	37	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑅 ∈ ℝ)
210	16	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 / 2) ∈ ℝ)
211		1rp 12396	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ+
212		rphalfcl 12419	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℝ+ → (1 / 2) ∈ ℝ+)
213	211, 212	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (1 / 2) ∈ ℝ+
214		rpge0 12405	. . . . . . . . . . . . 13 ⊢ ((1 / 2) ∈ ℝ+ → 0 ≤ (1 / 2))
215	213, 214	mp1i 13	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ (1 / 2))
216	17	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → γ ∈ ℝ)
217		0re 10646	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ
218		emgt0 25587	. . . . . . . . . . . . . . 15 ⊢ 0 < γ
219	217, 17, 218	ltleii 10766	. . . . . . . . . . . . . 14 ⊢ 0 ≤ γ
220	219	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ γ)
221	20	absge0d 14807	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ (abs‘𝐿))
222	216, 21, 220, 221	addge0d 11219	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ (γ + (abs‘𝐿)))
223	210, 23, 215, 222	addge0d 11219	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ ((1 / 2) + (γ + (abs‘𝐿))))
224		log1 25172	. . . . . . . . . . . . . 14 ⊢ (log‘1) = 0
225	29	nncnd 11657	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ∈ ℂ)
226	225	mulid2d 10662	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (1 · 𝑚) = 𝑚)
227	30	rpred 12434	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ∈ ℝ)
228	2	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 2 ∈ ℝ)
229	199	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → e ∈ ℝ)
230		elfzle2 12914	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ (1...2) → 𝑚 ≤ 2)
231	230	adantl 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ≤ 2)
232	2, 199, 204	ltleii 10766	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ≤ e
233	232	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 2 ≤ e)
234	227, 228, 229, 231, 233	letrd 10800	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ≤ e)
235	226, 234	eqbrtrd 5091	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (1 · 𝑚) ≤ e)
236		1red 10645	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 1 ∈ ℝ)
237	236, 229, 30	lemuldivd 12483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → ((1 · 𝑚) ≤ e ↔ 1 ≤ (e / 𝑚)))
238	235, 237	mpbid 234	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 1 ≤ (e / 𝑚))
239		logleb 25189	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℝ+ ∧ (e / 𝑚) ∈ ℝ+) → (1 ≤ (e / 𝑚) ↔ (log‘1) ≤ (log‘(e / 𝑚))))
240	211, 32, 239	sylancr 589	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (1 ≤ (e / 𝑚) ↔ (log‘1) ≤ (log‘(e / 𝑚))))
241	238, 240	mpbid 234	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (log‘1) ≤ (log‘(e / 𝑚)))
242	224, 241	eqbrtrrid 5105	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 0 ≤ (log‘(e / 𝑚)))
243	33, 30, 242	divge0d 12474	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 0 ≤ ((log‘(e / 𝑚)) / 𝑚))
244	26, 34, 243	fsumge0 15153	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚))
245	25, 35, 223, 244	addge0d 11219	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ (((1 / 2) + (γ + (abs‘𝐿))) + Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚)))
246	245, 15	breqtrrdi 5111	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝑅)
247	246	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 0 ≤ 𝑅)
248	209, 247	jca 514	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅))
249	84, 96	mulcld 10664	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℂ)
250		remulcl 10625	. . . . . . . 8 ⊢ ((2 ∈ ℝ ∧ ((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℝ) → (2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ ℝ)
251	2, 11, 250	sylancr 589	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ ℝ)
252	2	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℝ)
253		0le2 11742	. . . . . . . . 9 ⊢ 0 ≤ 2
254	253	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ 2)
255	97	mulid2d 10662	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) = 𝑛)
256		fznnfl 13233	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥)))
257	122, 256	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥)))
258	257	simplbda 502	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≤ 𝑥)
259	255, 258	eqbrtrd 5091	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) ≤ 𝑥)
260		1red 10645	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
261	55	nnrpd 12432	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+)
262	260, 123, 261	lemuldivd 12483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛)))
263	259, 262	mpbid 234	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ (𝑥 / 𝑛))
264		logleb 25189	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℝ+ ∧ (𝑥 / 𝑛) ∈ ℝ+) → (1 ≤ (𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛))))
265	211, 8, 264	sylancr 589	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 ≤ (𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛))))
266	263, 265	mpbid 234	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘1) ≤ (log‘(𝑥 / 𝑛)))
267	224, 266	eqbrtrrid 5105	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (log‘(𝑥 / 𝑛)))
268		rpregt0 12406	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
269	268	ad2antlr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
270		divge0 11512	. . . . . . . . 9 ⊢ ((((log‘(𝑥 / 𝑛)) ∈ ℝ ∧ 0 ≤ (log‘(𝑥 / 𝑛))) ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → 0 ≤ ((log‘(𝑥 / 𝑛)) / 𝑥))
271	9, 267, 269, 270	syl21anc 835	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((log‘(𝑥 / 𝑛)) / 𝑥))
272	252, 11, 254, 271	mulge0d 11220	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (2 · ((log‘(𝑥 / 𝑛)) / 𝑥)))
273	249	abscld 14799	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ∈ ℝ)
274	273	adantr 483	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ∈ ℝ)
275	96	adantr 483	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ∈ ℂ)
276	275	abscld 14799	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℝ)
277	261	rpred 12434	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ)
278	251, 277	remulcld 10674	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) ∈ ℝ)
279	278	adantr 483	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) ∈ ℝ)
280	84, 96	absmuld 14817	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) = ((abs‘(μ‘𝑛)) · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))))
281	84	abscld 14799	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ∈ ℝ)
282	96	abscld 14799	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℝ)
283	96	absge0d 14807	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
284		mule1 25728	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (abs‘(μ‘𝑛)) ≤ 1)
285	55, 284	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ≤ 1)
286	281, 260, 282, 283, 285	lemul1ad 11582	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(μ‘𝑛)) · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (1 · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))))
287	282	recnd 10672	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℂ)
288	287	mulid2d 10662	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) = (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
289	286, 288	breqtrd 5095	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(μ‘𝑛)) · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
290	280, 289	eqbrtrd 5091	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
291	290	adantr 483	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
292		logdivsum.1	. . . . . . . . . 10 ⊢ 𝐹 = (𝑦 ∈ ℝ+ ↦ (Σ𝑖 ∈ (1...(⌊‘𝑦))((log‘𝑖) / 𝑖) − (((log‘𝑦)↑2) / 2)))
293	18	ad3antrrr 728	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → 𝐹 ⇝𝑟 𝐿)
294	8	adantr 483	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (𝑥 / 𝑛) ∈ ℝ+)
295		simpr 487	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → e ≤ (𝑥 / 𝑛))
296	292, 293, 294, 295	mulog2sumlem1 26113	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)))) ≤ (2 · ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))))
297	71, 95	abssubd 14816	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − 𝑇)))
298	297	adantr 483	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − 𝑇)))
299	61	oveq2i 7170	. . . . . . . . . . 11 ⊢ (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − 𝑇) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)))
300	299	fveq2i 6676	. . . . . . . . . 10 ⊢ (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − 𝑇)) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿))))
301	298, 300	syl6eq 2875	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)))))
302		2cnd 11718	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℂ)
303	11	recnd 10672	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℂ)
304	302, 303, 97	mulassd 10667	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) = (2 · (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛)))
305		rpcnne0 12410	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ+ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
306	305	ad2antlr 725	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
307		divdiv2 11355	. . . . . . . . . . . . . 14 ⊢ (((log‘(𝑥 / 𝑛)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛)) = (((log‘(𝑥 / 𝑛)) · 𝑛) / 𝑥))
308	62, 306, 109, 307	syl3anc 1367	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛)) = (((log‘(𝑥 / 𝑛)) · 𝑛) / 𝑥))
309		div23 11320	. . . . . . . . . . . . . 14 ⊢ (((log‘(𝑥 / 𝑛)) ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((log‘(𝑥 / 𝑛)) · 𝑛) / 𝑥) = (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛))
310	62, 97, 306, 309	syl3anc 1367	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛)) · 𝑛) / 𝑥) = (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛))
311	308, 310	eqtrd 2859	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛)) = (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛))
312	311	oveq2d 7175	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))) = (2 · (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛)))
313	304, 312	eqtr4d 2862	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) = (2 · ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))))
314	313	adantr 483	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) = (2 · ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))))
315	296, 301, 314	3brtr4d 5101	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛))
316	274, 276, 279, 291, 315	letrd 10800	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛))
317	273	adantr 483	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ∈ ℝ)
318	282	adantr 483	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℝ)
319	37	ad3antrrr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 𝑅 ∈ ℝ)
320	290	adantr 483	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
321	71	adantr 483	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 𝑇 ∈ ℂ)
322	321	abscld 14799	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘𝑇) ∈ ℝ)
323	95	adantr 483	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ)
324	323	abscld 14799	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ∈ ℝ)
325	322, 324	readdcld 10673	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘𝑇) + (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℝ)
326	321, 323	abs2dif2d 14821	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ ((abs‘𝑇) + (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
327	25	ad3antrrr 728	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((1 / 2) + (γ + (abs‘𝐿))) ∈ ℝ)
328	35	ad3antrrr 728	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
329	61	fveq2i 6676	. . . . . . . . . . . 12 ⊢ (abs‘𝑇) = (abs‘((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)))
330	329, 322	eqeltrrid 2921	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ∈ ℝ)
331	64	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (((log‘(𝑥 / 𝑛))↑2) / 2) ∈ ℂ)
332	331	abscld 14799	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) ∈ ℝ)
333	69	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((γ · (log‘(𝑥 / 𝑛))) − 𝐿) ∈ ℂ)
334	333	abscld 14799	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ∈ ℝ)
335	332, 334	readdcld 10673	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) + (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ∈ ℝ)
336	331, 333	abstrid 14819	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ≤ ((abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) + (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿))))
337	16	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (1 / 2) ∈ ℝ)
338	23	ad3antrrr 728	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ + (abs‘𝐿)) ∈ ℝ)
339	9	resqcld 13614	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℝ)
340	339	rehalfcld 11887	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) / 2) ∈ ℝ)
341	9	sqge0d 13615	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((log‘(𝑥 / 𝑛))↑2))
342		2pos 11743	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 < 2
343	2, 342	pm3.2i 473	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 ∈ ℝ ∧ 0 < 2)
344	343	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 ∈ ℝ ∧ 0 < 2))
345		divge0 11512	. . . . . . . . . . . . . . . . . 18 ⊢ (((((log‘(𝑥 / 𝑛))↑2) ∈ ℝ ∧ 0 ≤ ((log‘(𝑥 / 𝑛))↑2)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ (((log‘(𝑥 / 𝑛))↑2) / 2))
346	339, 341, 344, 345	syl21anc 835	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (((log‘(𝑥 / 𝑛))↑2) / 2))
347	340, 346	absidd 14785	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) = (((log‘(𝑥 / 𝑛))↑2) / 2))
348	347	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) = (((log‘(𝑥 / 𝑛))↑2) / 2))
349	8	rpred 12434	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ)
350		ltle 10732	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ e ∈ ℝ) → ((𝑥 / 𝑛) < e → (𝑥 / 𝑛) ≤ e))
351	349, 199, 350	sylancl 588	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) < e → (𝑥 / 𝑛) ≤ e))
352	351	imp 409	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) ≤ e)
353	8	adantr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) ∈ ℝ+)
354		logleb 25189	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 / 𝑛) ∈ ℝ+ ∧ e ∈ ℝ+) → ((𝑥 / 𝑛) ≤ e ↔ (log‘(𝑥 / 𝑛)) ≤ (log‘e)))
355	353, 27, 354	sylancl 588	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((𝑥 / 𝑛) ≤ e ↔ (log‘(𝑥 / 𝑛)) ≤ (log‘e)))
356	352, 355	mpbid 234	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (log‘(𝑥 / 𝑛)) ≤ (log‘e))
357		loge 25173	. . . . . . . . . . . . . . . . . . 19 ⊢ (log‘e) = 1
358	356, 357	breqtrdi 5110	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (log‘(𝑥 / 𝑛)) ≤ 1)
359		0le1 11166	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ≤ 1
360	359	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ 1)
361	9, 260, 267, 360	le2sqd 13623	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) ≤ 1 ↔ ((log‘(𝑥 / 𝑛))↑2) ≤ (1↑2)))
362	361	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((log‘(𝑥 / 𝑛)) ≤ 1 ↔ ((log‘(𝑥 / 𝑛))↑2) ≤ (1↑2)))
363	358, 362	mpbid 234	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((log‘(𝑥 / 𝑛))↑2) ≤ (1↑2))
364		sq1 13561	. . . . . . . . . . . . . . . . 17 ⊢ (1↑2) = 1
365	363, 364	breqtrdi 5110	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((log‘(𝑥 / 𝑛))↑2) ≤ 1)
366	339	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℝ)
367		1red 10645	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 1 ∈ ℝ)
368	343	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (2 ∈ ℝ ∧ 0 < 2))
369		lediv1 11508	. . . . . . . . . . . . . . . . 17 ⊢ ((((log‘(𝑥 / 𝑛))↑2) ∈ ℝ ∧ 1 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((log‘(𝑥 / 𝑛))↑2) ≤ 1 ↔ (((log‘(𝑥 / 𝑛))↑2) / 2) ≤ (1 / 2)))
370	366, 367, 368, 369	syl3anc 1367	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (((log‘(𝑥 / 𝑛))↑2) ≤ 1 ↔ (((log‘(𝑥 / 𝑛))↑2) / 2) ≤ (1 / 2)))
371	365, 370	mpbid 234	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (((log‘(𝑥 / 𝑛))↑2) / 2) ≤ (1 / 2))
372	348, 371	eqbrtrd 5091	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) ≤ (1 / 2))
373	68	abscld 14799	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘𝐿) ∈ ℝ)
374	66, 373	readdcld 10673	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)) ∈ ℝ)
375	374	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)) ∈ ℝ)
376	67	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ · (log‘(𝑥 / 𝑛))) ∈ ℂ)
377	20	ad3antrrr 728	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 𝐿 ∈ ℂ)
378	376, 377	abs2dif2d 14821	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ≤ ((abs‘(γ · (log‘(𝑥 / 𝑛)))) + (abs‘𝐿)))
379	17	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → γ ∈ ℝ)
380	219	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ γ)
381	379, 9, 380, 267	mulge0d 11220	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (γ · (log‘(𝑥 / 𝑛))))
382	66, 381	absidd 14785	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(γ · (log‘(𝑥 / 𝑛)))) = (γ · (log‘(𝑥 / 𝑛))))
383	382	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(γ · (log‘(𝑥 / 𝑛)))) = (γ · (log‘(𝑥 / 𝑛))))
384	383	oveq1d 7174	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘(γ · (log‘(𝑥 / 𝑛)))) + (abs‘𝐿)) = ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)))
385	378, 384	breqtrd 5095	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ≤ ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)))
386	66	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ · (log‘(𝑥 / 𝑛))) ∈ ℝ)
387	17	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → γ ∈ ℝ)
388	377	abscld 14799	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘𝐿) ∈ ℝ)
389	9	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
390	387, 218	jctir 523	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ ∈ ℝ ∧ 0 < γ))
391		lemul2 11496	. . . . . . . . . . . . . . . . . . 19 ⊢ (((log‘(𝑥 / 𝑛)) ∈ ℝ ∧ 1 ∈ ℝ ∧ (γ ∈ ℝ ∧ 0 < γ)) → ((log‘(𝑥 / 𝑛)) ≤ 1 ↔ (γ · (log‘(𝑥 / 𝑛))) ≤ (γ · 1)))
392	389, 367, 390, 391	syl3anc 1367	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((log‘(𝑥 / 𝑛)) ≤ 1 ↔ (γ · (log‘(𝑥 / 𝑛))) ≤ (γ · 1)))
393	358, 392	mpbid 234	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ · (log‘(𝑥 / 𝑛))) ≤ (γ · 1))
394	17	recni 10658	. . . . . . . . . . . . . . . . . 18 ⊢ γ ∈ ℂ
395	394	mulid1i 10648	. . . . . . . . . . . . . . . . 17 ⊢ (γ · 1) = γ
396	393, 395	breqtrdi 5110	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ · (log‘(𝑥 / 𝑛))) ≤ γ)
397	386, 387, 388, 396	leadd1dd 11257	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)) ≤ (γ + (abs‘𝐿)))
398	334, 375, 338, 385, 397	letrd 10800	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ≤ (γ + (abs‘𝐿)))
399	332, 334, 337, 338, 372, 398	le2addd 11262	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) + (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ≤ ((1 / 2) + (γ + (abs‘𝐿))))
400	330, 335, 327, 336, 399	letrd 10800	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ≤ ((1 / 2) + (γ + (abs‘𝐿))))
401	329, 400	eqbrtrid 5104	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘𝑇) ≤ ((1 / 2) + (γ + (abs‘𝐿))))
402	86, 92	sylan2 594	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
403	85, 402	fsumrecl 15094	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
404	403	adantr 483	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
405	86, 90	sylan2 594	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
406	86, 129	sylan2 594	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℂ)
407	406	mulid2d 10662	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (1 · 𝑚) = 𝑚)
408		fznnfl 13233	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 / 𝑛) ∈ ℝ → (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) ↔ (𝑚 ∈ ℕ ∧ 𝑚 ≤ (𝑥 / 𝑛))))
409	349, 408	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) ↔ (𝑚 ∈ ℕ ∧ 𝑚 ≤ (𝑥 / 𝑛))))
410	409	simplbda 502	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ≤ (𝑥 / 𝑛))
411	407, 410	eqbrtrd 5091	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (1 · 𝑚) ≤ (𝑥 / 𝑛))
412		1red 10645	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 1 ∈ ℝ)
413	349	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (𝑥 / 𝑛) ∈ ℝ)
414	116	rpregt0d 12440	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (𝑚 ∈ ℝ ∧ 0 < 𝑚))
415	86, 414	sylan2 594	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (𝑚 ∈ ℝ ∧ 0 < 𝑚))
416		lemuldiv 11523	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℝ ∧ (𝑥 / 𝑛) ∈ ℝ ∧ (𝑚 ∈ ℝ ∧ 0 < 𝑚)) → ((1 · 𝑚) ≤ (𝑥 / 𝑛) ↔ 1 ≤ ((𝑥 / 𝑛) / 𝑚)))
417	412, 413, 415, 416	syl3anc 1367	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((1 · 𝑚) ≤ (𝑥 / 𝑛) ↔ 1 ≤ ((𝑥 / 𝑛) / 𝑚)))
418	411, 417	mpbid 234	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 1 ≤ ((𝑥 / 𝑛) / 𝑚))
419	86, 89	sylan2 594	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
420		logleb 25189	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ+ ∧ ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+) → (1 ≤ ((𝑥 / 𝑛) / 𝑚) ↔ (log‘1) ≤ (log‘((𝑥 / 𝑛) / 𝑚))))
421	211, 419, 420	sylancr 589	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (1 ≤ ((𝑥 / 𝑛) / 𝑚) ↔ (log‘1) ≤ (log‘((𝑥 / 𝑛) / 𝑚))))
422	418, 421	mpbid 234	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (log‘1) ≤ (log‘((𝑥 / 𝑛) / 𝑚)))
423	224, 422	eqbrtrrid 5105	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 0 ≤ (log‘((𝑥 / 𝑛) / 𝑚)))
424		divge0 11512	. . . . . . . . . . . . . . . 16 ⊢ ((((log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ ∧ 0 ≤ (log‘((𝑥 / 𝑛) / 𝑚))) ∧ (𝑚 ∈ ℝ ∧ 0 < 𝑚)) → 0 ≤ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))
425	405, 423, 415, 424	syl21anc 835	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 0 ≤ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))
426	85, 402, 425	fsumge0 15153	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))
427	426	adantr 483	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 0 ≤ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))
428	404, 427	absidd 14785	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))
429		fzfid 13344	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
430	349	flcld 13171	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℤ)
431	430	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (⌊‘(𝑥 / 𝑛)) ∈ ℤ)
432		2z 12017	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℤ
433	432	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 2 ∈ ℤ)
434	349	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) ∈ ℝ)
435	199	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → e ∈ ℝ)
436		3re 11720	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 3 ∈ ℝ
437	436	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 3 ∈ ℝ)
438		simpr 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) < e)
439	203	simpri 488	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ e < 3
440	439	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → e < 3)
441	434, 435, 437, 438, 440	lttrd 10804	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) < 3)
442		3z 12018	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 3 ∈ ℤ
443		fllt 13179	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ 3 ∈ ℤ) → ((𝑥 / 𝑛) < 3 ↔ (⌊‘(𝑥 / 𝑛)) < 3))
444	434, 442, 443	sylancl 588	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((𝑥 / 𝑛) < 3 ↔ (⌊‘(𝑥 / 𝑛)) < 3))
445	441, 444	mpbid 234	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (⌊‘(𝑥 / 𝑛)) < 3)
446		df-3 11704	. . . . . . . . . . . . . . . . . . . 20 ⊢ 3 = (2 + 1)
447	445, 446	breqtrdi 5110	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (⌊‘(𝑥 / 𝑛)) < (2 + 1))
448		zleltp1 12036	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((⌊‘(𝑥 / 𝑛)) ∈ ℤ ∧ 2 ∈ ℤ) → ((⌊‘(𝑥 / 𝑛)) ≤ 2 ↔ (⌊‘(𝑥 / 𝑛)) < (2 + 1)))
449	431, 432, 448	sylancl 588	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((⌊‘(𝑥 / 𝑛)) ≤ 2 ↔ (⌊‘(𝑥 / 𝑛)) < (2 + 1)))
450	447, 449	mpbird 259	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (⌊‘(𝑥 / 𝑛)) ≤ 2)
451		eluz2 12252	. . . . . . . . . . . . . . . . . 18 ⊢ (2 ∈ (ℤ≥‘(⌊‘(𝑥 / 𝑛))) ↔ ((⌊‘(𝑥 / 𝑛)) ∈ ℤ ∧ 2 ∈ ℤ ∧ (⌊‘(𝑥 / 𝑛)) ≤ 2))
452	431, 433, 450, 451	syl3anbrc 1339	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 2 ∈ (ℤ≥‘(⌊‘(𝑥 / 𝑛))))
453		fzss2 12950	. . . . . . . . . . . . . . . . 17 ⊢ (2 ∈ (ℤ≥‘(⌊‘(𝑥 / 𝑛))) → (1...(⌊‘(𝑥 / 𝑛))) ⊆ (1...2))
454	452, 453	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (1...(⌊‘(𝑥 / 𝑛))) ⊆ (1...2))
455	454	sselda 3970	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ (1...2))
456	34	ad5ant15 757	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
457	455, 456	syldan 593	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
458	429, 457	fsumrecl 15094	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
459	92	adantlr 713	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ ℕ) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
460	86, 459	sylan2 594	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
461	352	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (𝑥 / 𝑛) ≤ e)
462	434	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (𝑥 / 𝑛) ∈ ℝ)
463	199	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → e ∈ ℝ)
464	30	rpregt0d 12440	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (𝑚 ∈ ℝ ∧ 0 < 𝑚))
465	464	ad5ant15 757	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (𝑚 ∈ ℝ ∧ 0 < 𝑚))
466		lediv1 11508	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ e ∈ ℝ ∧ (𝑚 ∈ ℝ ∧ 0 < 𝑚)) → ((𝑥 / 𝑛) ≤ e ↔ ((𝑥 / 𝑛) / 𝑚) ≤ (e / 𝑚)))
467	462, 463, 465, 466	syl3anc 1367	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((𝑥 / 𝑛) ≤ e ↔ ((𝑥 / 𝑛) / 𝑚) ≤ (e / 𝑚)))
468	461, 467	mpbid 234	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((𝑥 / 𝑛) / 𝑚) ≤ (e / 𝑚))
469	89	adantlr 713	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ ℕ) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
470	28, 469	sylan2 594	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
471	32	ad5ant15 757	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (e / 𝑚) ∈ ℝ+)
472	470, 471	logled 25213	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (((𝑥 / 𝑛) / 𝑚) ≤ (e / 𝑚) ↔ (log‘((𝑥 / 𝑛) / 𝑚)) ≤ (log‘(e / 𝑚))))
473	468, 472	mpbid 234	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (log‘((𝑥 / 𝑛) / 𝑚)) ≤ (log‘(e / 𝑚)))
474	90	adantlr 713	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ ℕ) → (log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
475	28, 474	sylan2 594	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
476	33	ad5ant15 757	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (log‘(e / 𝑚)) ∈ ℝ)
477		lediv1 11508	. . . . . . . . . . . . . . . . 17 ⊢ (((log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ ∧ (log‘(e / 𝑚)) ∈ ℝ ∧ (𝑚 ∈ ℝ ∧ 0 < 𝑚)) → ((log‘((𝑥 / 𝑛) / 𝑚)) ≤ (log‘(e / 𝑚)) ↔ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ ((log‘(e / 𝑚)) / 𝑚)))
478	475, 476, 465, 477	syl3anc 1367	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((log‘((𝑥 / 𝑛) / 𝑚)) ≤ (log‘(e / 𝑚)) ↔ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ ((log‘(e / 𝑚)) / 𝑚)))
479	473, 478	mpbid 234	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ ((log‘(e / 𝑚)) / 𝑚))
480	455, 479	syldan 593	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ ((log‘(e / 𝑚)) / 𝑚))
481	429, 460, 457, 480	fsumle 15157	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘(e / 𝑚)) / 𝑚))
482		fzfid 13344	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (1...2) ∈ Fin)
483	243	ad5ant15 757	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → 0 ≤ ((log‘(e / 𝑚)) / 𝑚))
484	482, 456, 483, 454	fsumless 15154	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘(e / 𝑚)) / 𝑚) ≤ Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚))
485	404, 458, 328, 481, 484	letrd 10800	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚))
486	428, 485	eqbrtrd 5091	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ≤ Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚))
487	322, 324, 327, 328, 401, 486	le2addd 11262	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘𝑇) + (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ (((1 / 2) + (γ + (abs‘𝐿))) + Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚)))
488	487, 15	breqtrrdi 5111	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘𝑇) + (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ 𝑅)
489	318, 325, 319, 326, 488	letrd 10800	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ 𝑅)
490	317, 318, 319, 320, 489	letrd 10800	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ 𝑅)
491	4, 208, 248, 249, 251, 272, 316, 490	fsumharmonic 25592	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · ((log‘e) + 1))))
492		2cnd 11718	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 ∈ ℂ)
493	3, 492, 303	fsummulc2 15142	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((log‘(𝑥 / 𝑛)) / 𝑥)))
494		df-2 11703	. . . . . . . . . 10 ⊢ 2 = (1 + 1)
495	357	oveq1i 7169	. . . . . . . . . 10 ⊢ ((log‘e) + 1) = (1 + 1)
496	494, 495	eqtr4i 2850	. . . . . . . . 9 ⊢ 2 = ((log‘e) + 1)
497	496	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 = ((log‘e) + 1))
498	497	oveq2d 7175	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑅 · 2) = (𝑅 · ((log‘e) + 1)))
499	493, 498	oveq12d 7177	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · ((log‘e) + 1))))
500	491, 499	breqtrrd 5097	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛)) ≤ ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)))
501	500	adantrr 715	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛)) ≤ ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)))
502	198, 501	eqbrtrrd 5093	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ≤ ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)))
503	54	leabsd 14777	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ≤ (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))))
504	503	adantrr 715	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ≤ (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))))
505	79, 80, 83, 502, 504	letrd 10800	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ≤ (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))))
506	1, 53, 54, 77, 505	o1le 15012	1 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ∈ 𝑂(1))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1536   ∈ wcel 2113   ≠ wne 3019  {crab 3145   ⊆ wss 3939   class class class wbr 5069   ↦ cmpt 5149  ‘cfv 6358  (class class class)co 7159  ℂcc 10538  ℝcr 10539  0cc0 10540  1c1 10541   + caddc 10543   · cmul 10545   < clt 10678   ≤ cle 10679   − cmin 10873   / cdiv 11300  ℕcn 11641  2c2 11695  3c3 11696  ℤcz 11984  ℤ_≥cuz 12246  ℝ⁺crp 12392  ...cfz 12895  ⌊cfl 13163  ↑cexp 13432  abscabs 14596   ⇝_𝑟 crli 14845  𝑂(1)co1 14846  Σcsu 15045  eceu 15419   ∥ cdvds 15610  logclog 25141  γcem 25572  μcmu 25675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-rep 5193  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464  ax-inf2 9107  ax-cnex 10596  ax-resscn 10597  ax-1cn 10598  ax-icn 10599  ax-addcl 10600  ax-addrcl 10601  ax-mulcl 10602  ax-mulrcl 10603  ax-mulcom 10604  ax-addass 10605  ax-mulass 10606  ax-distr 10607  ax-i2m1 10608  ax-1ne0 10609  ax-1rid 10610  ax-rnegex 10611  ax-rrecex 10612  ax-cnre 10613  ax-pre-lttri 10614  ax-pre-lttrn 10615  ax-pre-ltadd 10616  ax-pre-mulgt0 10617  ax-pre-sup 10618  ax-addf 10619  ax-mulf 10620

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1539  df-fal 1549  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-nel 3127  df-ral 3146  df-rex 3147  df-reu 3148  df-rmo 3149  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-tp 4575  df-op 4577  df-uni 4842  df-int 4880  df-iun 4924  df-iin 4925  df-disj 5035  df-br 5070  df-opab 5132  df-mpt 5150  df-tr 5176  df-id 5463  df-eprel 5468  df-po 5477  df-so 5478  df-fr 5517  df-se 5518  df-we 5519  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-pred 6151  df-ord 6197  df-on 6198  df-lim 6199  df-suc 6200  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-isom 6367  df-riota 7117  df-ov 7162  df-oprab 7163  df-mpo 7164  df-of 7412  df-om 7584  df-1st 7692  df-2nd 7693  df-supp 7834  df-wrecs 7950  df-recs 8011  df-rdg 8049  df-1o 8105  df-2o 8106  df-oadd 8109  df-er 8292  df-map 8411  df-pm 8412  df-ixp 8465  df-en 8513  df-dom 8514  df-sdom 8515  df-fin 8516  df-fsupp 8837  df-fi 8878  df-sup 8909  df-inf 8910  df-oi 8977  df-dju 9333  df-card 9371  df-pnf 10680  df-mnf 10681  df-xr 10682  df-ltxr 10683  df-le 10684  df-sub 10875  df-neg 10876  df-div 11301  df-nn 11642  df-2 11703  df-3 11704  df-4 11705  df-5 11706  df-6 11707  df-7 11708  df-8 11709  df-9 11710  df-n0 11901  df-xnn0 11971  df-z 11985  df-dec 12102  df-uz 12247  df-q 12352  df-rp 12393  df-xneg 12510  df-xadd 12511  df-xmul 12512  df-ioo 12745  df-ioc 12746  df-ico 12747  df-icc 12748  df-fz 12896  df-fzo 13037  df-fl 13165  df-mod 13241  df-seq 13373  df-exp 13433  df-fac 13637  df-bc 13666  df-hash 13694  df-shft 14429  df-cj 14461  df-re 14462  df-im 14463  df-sqrt 14597  df-abs 14598  df-limsup 14831  df-clim 14848  df-rlim 14849  df-o1 14850  df-lo1 14851  df-sum 15046  df-ef 15424  df-e 15425  df-sin 15426  df-cos 15427  df-tan 15428  df-pi 15429  df-dvds 15611  df-gcd 15847  df-prm 16019  df-pc 16177  df-struct 16488  df-ndx 16489  df-slot 16490  df-base 16492  df-sets 16493  df-ress 16494  df-plusg 16581  df-mulr 16582  df-starv 16583  df-sca 16584  df-vsca 16585  df-ip 16586  df-tset 16587  df-ple 16588  df-ds 16590  df-unif 16591  df-hom 16592  df-cco 16593  df-rest 16699  df-topn 16700  df-0g 16718  df-gsum 16719  df-topgen 16720  df-pt 16721  df-prds 16724  df-xrs 16778  df-qtop 16783  df-imas 16784  df-xps 16786  df-mre 16860  df-mrc 16861  df-acs 16863  df-mgm 17855  df-sgrp 17904  df-mnd 17915  df-submnd 17960  df-mulg 18228  df-cntz 18450  df-cmn 18911  df-psmet 20540  df-xmet 20541  df-met 20542  df-bl 20543  df-mopn 20544  df-fbas 20545  df-fg 20546  df-cnfld 20549  df-top 21505  df-topon 21522  df-topsp 21544  df-bases 21557  df-cld 21630  df-ntr 21631  df-cls 21632  df-nei 21709  df-lp 21747  df-perf 21748  df-cn 21838  df-cnp 21839  df-haus 21926  df-cmp 21998  df-tx 22173  df-hmeo 22366  df-fil 22457  df-fm 22549  df-flim 22550  df-flf 22551  df-xms 22933  df-ms 22934  df-tms 22935  df-cncf 23489  df-limc 24467  df-dv 24468  df-ulm 24968  df-log 25143  df-cxp 25144  df-atan 25448  df-em 25573  df-mu 25681

This theorem is referenced by:  mulog2sumlem3  26115