Theorem mulog2sumlem2 26883

Description: Lemma for mulog2sum 26885. (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 11156	. 2 ⊢ (𝜑 → 1 ∈ ℝ)
2		2re 12227	. . . 4 ⊢ 2 ∈ ℝ
3		fzfid 13878	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin)
4		simpr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
5		elfznn 13470	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
6	5	nnrpd 12955	. . . . . . . 8 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℝ+)
7		rpdivcl 12940	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) → (𝑥 / 𝑛) ∈ ℝ+)
8	4, 6, 7	syl2an 596	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ+)
9	8	relogcld 25978	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
10		simplr 767	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ+)
11	9, 10	rerpdivcld 12988	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℝ)
12	3, 11	fsumrecl 15619	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℝ)
13		remulcl 11136	. . . 4 ⊢ ((2 ∈ ℝ ∧ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℝ) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ ℝ)
14	2, 12, 13	sylancr 587	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ ℝ)
15		mulog2sumlem2.r	. . . . . 6 ⊢ 𝑅 = (((1 / 2) + (γ + (abs‘𝐿))) + Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚))
16		halfre 12367	. . . . . . . 8 ⊢ (1 / 2) ∈ ℝ
17		emre 26355	. . . . . . . . 9 ⊢ γ ∈ ℝ
18		mulog2sumlem.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐿)
19		rlimcl 15385	. . . . . . . . . . 11 ⊢ (𝐹 ⇝𝑟 𝐿 → 𝐿 ∈ ℂ)
20	18, 19	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ ℂ)
21	20	abscld 15321	. . . . . . . . 9 ⊢ (𝜑 → (abs‘𝐿) ∈ ℝ)
22		readdcl 11134	. . . . . . . . 9 ⊢ ((γ ∈ ℝ ∧ (abs‘𝐿) ∈ ℝ) → (γ + (abs‘𝐿)) ∈ ℝ)
23	17, 21, 22	sylancr 587	. . . . . . . 8 ⊢ (𝜑 → (γ + (abs‘𝐿)) ∈ ℝ)
24		readdcl 11134	. . . . . . . 8 ⊢ (((1 / 2) ∈ ℝ ∧ (γ + (abs‘𝐿)) ∈ ℝ) → ((1 / 2) + (γ + (abs‘𝐿))) ∈ ℝ)
25	16, 23, 24	sylancr 587	. . . . . . 7 ⊢ (𝜑 → ((1 / 2) + (γ + (abs‘𝐿))) ∈ ℝ)
26		fzfid 13878	. . . . . . . 8 ⊢ (𝜑 → (1...2) ∈ Fin)
27		epr 16090	. . . . . . . . . . 11 ⊢ e ∈ ℝ+
28		elfznn 13470	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (1...2) → 𝑚 ∈ ℕ)
29	28	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ∈ ℕ)
30	29	nnrpd 12955	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ∈ ℝ+)
31		rpdivcl 12940	. . . . . . . . . . 11 ⊢ ((e ∈ ℝ+ ∧ 𝑚 ∈ ℝ+) → (e / 𝑚) ∈ ℝ+)
32	27, 30, 31	sylancr 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (e / 𝑚) ∈ ℝ+)
33	32	relogcld 25978	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (log‘(e / 𝑚)) ∈ ℝ)
34	33, 29	nndivred 12207	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → ((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
35	26, 34	fsumrecl 15619	. . . . . . 7 ⊢ (𝜑 → Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
36	25, 35	readdcld 11184	. . . . . 6 ⊢ (𝜑 → (((1 / 2) + (γ + (abs‘𝐿))) + Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚)) ∈ ℝ)
37	15, 36	eqeltrid 2842	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ ℝ)
38		remulcl 11136	. . . . 5 ⊢ ((𝑅 ∈ ℝ ∧ 2 ∈ ℝ) → (𝑅 · 2) ∈ ℝ)
39	37, 2, 38	sylancl 586	. . . 4 ⊢ (𝜑 → (𝑅 · 2) ∈ ℝ)
40	39	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑅 · 2) ∈ ℝ)
41	2	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 ∈ ℝ)
42		rpssre 12922	. . . . 5 ⊢ ℝ+ ⊆ ℝ
43		2cnd 12231	. . . . 5 ⊢ (𝜑 → 2 ∈ ℂ)
44		o1const 15502	. . . . 5 ⊢ ((ℝ+ ⊆ ℝ ∧ 2 ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ 2) ∈ 𝑂(1))
45	42, 43, 44	sylancr 587	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ 2) ∈ 𝑂(1))
46		logfacrlim2 26574	. . . . 5 ⊢ (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ⇝𝑟 1
47		rlimo1 15499	. . . . 5 ⊢ ((𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ⇝𝑟 1 → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ 𝑂(1))
48	46, 47	mp1i 13	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ 𝑂(1))
49	41, 12, 45, 48	o1mul2 15507	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥))) ∈ 𝑂(1))
50	39	recnd 11183	. . . 4 ⊢ (𝜑 → (𝑅 · 2) ∈ ℂ)
51		o1const 15502	. . . 4 ⊢ ((ℝ+ ⊆ ℝ ∧ (𝑅 · 2) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ (𝑅 · 2)) ∈ 𝑂(1))
52	42, 50, 51	sylancr 587	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (𝑅 · 2)) ∈ 𝑂(1))
53	14, 40, 49, 52	o1add2 15506	. 2 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))) ∈ 𝑂(1))
54	14, 40	readdcld 11184	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ∈ ℝ)
55	5	adantl 482	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
56		mucl 26490	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (μ‘𝑛) ∈ ℤ)
57	55, 56	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℤ)
58	57	zred 12607	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℝ)
59	58, 55	nndivred 12207	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℝ)
60	59	recnd 11183	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℂ)
61		mulog2sumlem2.t	. . . . . 6 ⊢ 𝑇 = ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿))
62	9	recnd 11183	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℂ)
63	62	sqcld 14049	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℂ)
64	63	halfcld 12398	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) / 2) ∈ ℂ)
65		remulcl 11136	. . . . . . . . . 10 ⊢ ((γ ∈ ℝ ∧ (log‘(𝑥 / 𝑛)) ∈ ℝ) → (γ · (log‘(𝑥 / 𝑛))) ∈ ℝ)
66	17, 9, 65	sylancr 587	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (γ · (log‘(𝑥 / 𝑛))) ∈ ℝ)
67	66	recnd 11183	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (γ · (log‘(𝑥 / 𝑛))) ∈ ℂ)
68	20	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝐿 ∈ ℂ)
69	67, 68	subcld 11512	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((γ · (log‘(𝑥 / 𝑛))) − 𝐿) ∈ ℂ)
70	64, 69	addcld 11174	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ∈ ℂ)
71	61, 70	eqeltrid 2842	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑇 ∈ ℂ)
72	60, 71	mulcld 11175	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · 𝑇) ∈ ℂ)
73	3, 72	fsumcl 15618	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) ∈ ℂ)
74		relogcl 25931	. . . . 5 ⊢ (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
75	74	adantl 482	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
76	75	recnd 11183	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℂ)
77	73, 76	subcld 11512	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥)) ∈ ℂ)
78	77	abscld 15321	. . . 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 11183	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ∈ ℂ)
82	81	abscld 15321	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))) ∈ ℝ)
83	82	adantrr 715	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))) ∈ ℝ)
84	57	zcnd 12608	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℂ)
85		fzfid 13878	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
86		elfznn 13470	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) → 𝑚 ∈ ℕ)
87		nnrp 12926	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℝ+)
88		rpdivcl 12940	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 / 𝑛) ∈ ℝ+ ∧ 𝑚 ∈ ℝ+) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
89	8, 87, 88	syl2an 596	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
90	89	relogcld 25978	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
91		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℕ)
92	90, 91	nndivred 12207	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
93	92	recnd 11183	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ)
94	86, 93	sylan2 593	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ)
95	85, 94	fsumcl 15618	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ)
96	71, 95	subcld 11512	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ∈ ℂ)
97	55	nncnd 12169	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
98	55	nnne0d 12203	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0)
99	84, 96, 97, 98	div23d 11968	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = (((μ‘𝑛) / 𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
100	60, 71, 95	subdid 11611	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = ((((μ‘𝑛) / 𝑛) · 𝑇) − (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
101	99, 100	eqtrd 2776	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = ((((μ‘𝑛) / 𝑛) · 𝑇) − (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
102	101	sumeq2dv 15588	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))((((μ‘𝑛) / 𝑛) · 𝑇) − (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
103	60, 95	mulcld 11175	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ∈ ℂ)
104	3, 72, 103	fsumsub 15673	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((μ‘𝑛) / 𝑛) · 𝑇) − (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
105	102, 104	eqtrd 2776	. . . . . . 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 15669	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))
108	84	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (μ‘𝑛) ∈ ℂ)
109	97, 98	jca 512	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
110	109	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
111		div23 11832	. . . . . . . . . . . . . . . . 17 ⊢ (((μ‘𝑛) ∈ ℂ ∧ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((μ‘𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) / 𝑛) = (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))
112		divass 11831	. . . . . . . . . . . . . . . . 17 ⊢ (((μ‘𝑛) ∈ ℂ ∧ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((μ‘𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) / 𝑛) = ((μ‘𝑛) · (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛)))
113	111, 112	eqtr3d 2778	. . . . . . . . . . . . . . . 16 ⊢ (((μ‘𝑛) ∈ ℂ ∧ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = ((μ‘𝑛) · (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛)))
114	108, 93, 110, 113	syl3anc 1371	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = ((μ‘𝑛) · (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛)))
115	90	recnd 11183	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℂ)
116	91	nnrpd 12955	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ+)
117		rpcnne0 12933	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ ℝ+ → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0))
118	116, 117	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0))
119		divdiv1 11866	. . . . . . . . . . . . . . . . . 18 ⊢ (((log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℂ ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0) ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛) = ((log‘((𝑥 / 𝑛) / 𝑚)) / (𝑚 · 𝑛)))
120	115, 118, 110, 119	syl3anc 1371	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛) = ((log‘((𝑥 / 𝑛) / 𝑚)) / (𝑚 · 𝑛)))
121		rpre 12923	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ)
122	121	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
123	122	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
124	123	recnd 11183	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℂ)
125	124	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → 𝑥 ∈ ℂ)
126		divdiv1 11866	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0) ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) → ((𝑥 / 𝑛) / 𝑚) = (𝑥 / (𝑛 · 𝑚)))
127	125, 110, 118, 126	syl3anc 1371	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((𝑥 / 𝑛) / 𝑚) = (𝑥 / (𝑛 · 𝑚)))
128	127	fveq2d 6846	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (log‘((𝑥 / 𝑛) / 𝑚)) = (log‘(𝑥 / (𝑛 · 𝑚))))
129	91	nncnd 12169	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
130	97	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → 𝑛 ∈ ℂ)
131	129, 130	mulcomd 11176	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (𝑚 · 𝑛) = (𝑛 · 𝑚))
132	128, 131	oveq12d 7375	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((log‘((𝑥 / 𝑛) / 𝑚)) / (𝑚 · 𝑛)) = ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚)))
133	120, 132	eqtrd 2776	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛) = ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚)))
134	133	oveq2d 7373	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((μ‘𝑛) · (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛)) = ((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
135	114, 134	eqtrd 2776	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = ((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
136	86, 135	sylan2 593	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = ((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
137	136	sumeq2dv 15588	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
138	107, 137	eqtrd 2776	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
139	138	sumeq2dv 15588	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
140		oveq2 7365	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑛 · 𝑚) → (𝑥 / 𝑘) = (𝑥 / (𝑛 · 𝑚)))
141	140	fveq2d 6846	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑛 · 𝑚) → (log‘(𝑥 / 𝑘)) = (log‘(𝑥 / (𝑛 · 𝑚))))
142		id 22	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑛 · 𝑚) → 𝑘 = (𝑛 · 𝑚))
143	141, 142	oveq12d 7375	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑛 · 𝑚) → ((log‘(𝑥 / 𝑘)) / 𝑘) = ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚)))
144	143	oveq2d 7373	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑛 · 𝑚) → ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) = ((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
145	4	rpred 12957	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
146		ssrab2 4037	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ ℕ
147		simprr 771	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})
148	146, 147	sselid 3942	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ ℕ)
149	148, 56	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (μ‘𝑛) ∈ ℤ)
150	149	zred 12607	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (μ‘𝑛) ∈ ℝ)
151		elfznn 13470	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (1...(⌊‘𝑥)) → 𝑘 ∈ ℕ)
152	151	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → 𝑘 ∈ ℕ)
153	152	nnrpd 12955	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → 𝑘 ∈ ℝ+)
154		rpdivcl 12940	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑘 ∈ ℝ+) → (𝑥 / 𝑘) ∈ ℝ+)
155	4, 153, 154	syl2an 596	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (𝑥 / 𝑘) ∈ ℝ+)
156	155	relogcld 25978	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (log‘(𝑥 / 𝑘)) ∈ ℝ)
157	151	ad2antrl 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑘 ∈ ℕ)
158	156, 157	nndivred 12207	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → ((log‘(𝑥 / 𝑘)) / 𝑘) ∈ ℝ)
159	150, 158	remulcld 11185	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) ∈ ℝ)
160	159	recnd 11183	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) ∈ ℂ)
161	144, 145, 160	dvdsflsumcom 26537	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
162	139, 161	eqtr4d 2779	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)))
163	162	adantrr 715	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)))
164		oveq2 7365	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → (𝑥 / 𝑘) = (𝑥 / 1))
165	164	fveq2d 6846	. . . . . . . . . 10 ⊢ (𝑘 = 1 → (log‘(𝑥 / 𝑘)) = (log‘(𝑥 / 1)))
166		id 22	. . . . . . . . . 10 ⊢ (𝑘 = 1 → 𝑘 = 1)
167	165, 166	oveq12d 7375	. . . . . . . . 9 ⊢ (𝑘 = 1 → ((log‘(𝑥 / 𝑘)) / 𝑘) = ((log‘(𝑥 / 1)) / 1))
168		fzfid 13878	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin)
169		fz1ssnn 13472	. . . . . . . . . 10 ⊢ (1...(⌊‘𝑥)) ⊆ ℕ
170	169	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ⊆ ℕ)
171	122	adantrr 715	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ)
172		simprr 771	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥)
173		flge1nn 13726	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ)
174	171, 172, 173	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (⌊‘𝑥) ∈ ℕ)
175		nnuz 12806	. . . . . . . . . . 11 ⊢ ℕ = (ℤ≥‘1)
176	174, 175	eleqtrdi 2848	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (⌊‘𝑥) ∈ (ℤ≥‘1))
177		eluzfz1 13448	. . . . . . . . . 10 ⊢ ((⌊‘𝑥) ∈ (ℤ≥‘1) → 1 ∈ (1...(⌊‘𝑥)))
178	176, 177	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ (1...(⌊‘𝑥)))
179	151	nnrpd 12955	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1...(⌊‘𝑥)) → 𝑘 ∈ ℝ+)
180	4, 179, 154	syl2an 596	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑘) ∈ ℝ+)
181	180	relogcld 25978	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑘)) ∈ ℝ)
182	169	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ⊆ ℕ)
183	182	sselda 3944	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → 𝑘 ∈ ℕ)
184	181, 183	nndivred 12207	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑘)) / 𝑘) ∈ ℝ)
185	184	recnd 11183	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑘)) / 𝑘) ∈ ℂ)
186	185	adantlrr 719	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑘)) / 𝑘) ∈ ℂ)
187	167, 168, 170, 178, 186	musumsum 26541	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) = ((log‘(𝑥 / 1)) / 1))
188	4	rpcnd 12959	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
189	188	div1d 11923	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 / 1) = 𝑥)
190	189	fveq2d 6846	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (log‘(𝑥 / 1)) = (log‘𝑥))
191	190	oveq1d 7372	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((log‘(𝑥 / 1)) / 1) = ((log‘𝑥) / 1))
192	76	div1d 11923	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((log‘𝑥) / 1) = (log‘𝑥))
193	191, 192	eqtrd 2776	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((log‘(𝑥 / 1)) / 1) = (log‘𝑥))
194	193	adantrr 715	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘(𝑥 / 1)) / 1) = (log‘𝑥))
195	163, 187, 194	3eqtrd 2780	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = (log‘𝑥))
196	195	oveq2d 7373	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥)))
197	106, 196	eqtrd 2776	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥)))
198	197	fveq2d 6846	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛)) = (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))))
199		ere 15971	. . . . . . . . 9 ⊢ e ∈ ℝ
200	199	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → e ∈ ℝ)
201		1re 11155	. . . . . . . . 9 ⊢ 1 ∈ ℝ
202		1lt2 12324	. . . . . . . . . 10 ⊢ 1 < 2
203		egt2lt3 16088	. . . . . . . . . . 11 ⊢ (2 < e ∧ e < 3)
204	203	simpli 484	. . . . . . . . . 10 ⊢ 2 < e
205	201, 2, 199	lttri 11281	. . . . . . . . . 10 ⊢ ((1 < 2 ∧ 2 < e) → 1 < e)
206	202, 204, 205	mp2an 690	. . . . . . . . 9 ⊢ 1 < e
207	201, 199, 206	ltleii 11278	. . . . . . . 8 ⊢ 1 ≤ e
208	200, 207	jctir 521	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (e ∈ ℝ ∧ 1 ≤ e))
209	37	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑅 ∈ ℝ)
210	16	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 / 2) ∈ ℝ)
211		1rp 12919	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ+
212		rphalfcl 12942	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℝ+ → (1 / 2) ∈ ℝ+)
213	211, 212	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (1 / 2) ∈ ℝ+
214		rpge0 12928	. . . . . . . . . . . . 13 ⊢ ((1 / 2) ∈ ℝ+ → 0 ≤ (1 / 2))
215	213, 214	mp1i 13	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ (1 / 2))
216	17	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → γ ∈ ℝ)
217		0re 11157	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ
218		emgt0 26356	. . . . . . . . . . . . . . 15 ⊢ 0 < γ
219	217, 17, 218	ltleii 11278	. . . . . . . . . . . . . 14 ⊢ 0 ≤ γ
220	219	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ γ)
221	20	absge0d 15329	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ (abs‘𝐿))
222	216, 21, 220, 221	addge0d 11731	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ (γ + (abs‘𝐿)))
223	210, 23, 215, 222	addge0d 11731	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ ((1 / 2) + (γ + (abs‘𝐿))))
224		log1 25941	. . . . . . . . . . . . . 14 ⊢ (log‘1) = 0
225	29	nncnd 12169	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ∈ ℂ)
226	225	mulid2d 11173	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (1 · 𝑚) = 𝑚)
227	30	rpred 12957	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ∈ ℝ)
228	2	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 2 ∈ ℝ)
229	199	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → e ∈ ℝ)
230		elfzle2 13445	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ (1...2) → 𝑚 ≤ 2)
231	230	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ≤ 2)
232	2, 199, 204	ltleii 11278	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ≤ e
233	232	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 2 ≤ e)
234	227, 228, 229, 231, 233	letrd 11312	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ≤ e)
235	226, 234	eqbrtrd 5127	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (1 · 𝑚) ≤ e)
236		1red 11156	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 1 ∈ ℝ)
237	236, 229, 30	lemuldivd 13006	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → ((1 · 𝑚) ≤ e ↔ 1 ≤ (e / 𝑚)))
238	235, 237	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 1 ≤ (e / 𝑚))
239		logleb 25958	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℝ+ ∧ (e / 𝑚) ∈ ℝ+) → (1 ≤ (e / 𝑚) ↔ (log‘1) ≤ (log‘(e / 𝑚))))
240	211, 32, 239	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (1 ≤ (e / 𝑚) ↔ (log‘1) ≤ (log‘(e / 𝑚))))
241	238, 240	mpbid 231	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (log‘1) ≤ (log‘(e / 𝑚)))
242	224, 241	eqbrtrrid 5141	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 0 ≤ (log‘(e / 𝑚)))
243	33, 30, 242	divge0d 12997	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 0 ≤ ((log‘(e / 𝑚)) / 𝑚))
244	26, 34, 243	fsumge0 15680	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚))
245	25, 35, 223, 244	addge0d 11731	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ (((1 / 2) + (γ + (abs‘𝐿))) + Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚)))
246	245, 15	breqtrrdi 5147	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝑅)
247	246	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 0 ≤ 𝑅)
248	209, 247	jca 512	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅))
249	84, 96	mulcld 11175	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℂ)
250		remulcl 11136	. . . . . . . 8 ⊢ ((2 ∈ ℝ ∧ ((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℝ) → (2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ ℝ)
251	2, 11, 250	sylancr 587	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ ℝ)
252	2	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℝ)
253		0le2 12255	. . . . . . . . 9 ⊢ 0 ≤ 2
254	253	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ 2)
255	97	mulid2d 11173	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) = 𝑛)
256		fznnfl 13767	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥)))
257	122, 256	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥)))
258	257	simplbda 500	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≤ 𝑥)
259	255, 258	eqbrtrd 5127	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) ≤ 𝑥)
260		1red 11156	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
261	55	nnrpd 12955	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+)
262	260, 123, 261	lemuldivd 13006	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛)))
263	259, 262	mpbid 231	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ (𝑥 / 𝑛))
264		logleb 25958	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℝ+ ∧ (𝑥 / 𝑛) ∈ ℝ+) → (1 ≤ (𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛))))
265	211, 8, 264	sylancr 587	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 ≤ (𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛))))
266	263, 265	mpbid 231	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘1) ≤ (log‘(𝑥 / 𝑛)))
267	224, 266	eqbrtrrid 5141	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (log‘(𝑥 / 𝑛)))
268		rpregt0 12929	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
269	268	ad2antlr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
270		divge0 12024	. . . . . . . . 9 ⊢ ((((log‘(𝑥 / 𝑛)) ∈ ℝ ∧ 0 ≤ (log‘(𝑥 / 𝑛))) ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → 0 ≤ ((log‘(𝑥 / 𝑛)) / 𝑥))
271	9, 267, 269, 270	syl21anc 836	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((log‘(𝑥 / 𝑛)) / 𝑥))
272	252, 11, 254, 271	mulge0d 11732	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (2 · ((log‘(𝑥 / 𝑛)) / 𝑥)))
273	249	abscld 15321	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ∈ ℝ)
274	273	adantr 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ∈ ℝ)
275	96	adantr 481	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ∈ ℂ)
276	275	abscld 15321	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℝ)
277	261	rpred 12957	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ)
278	251, 277	remulcld 11185	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) ∈ ℝ)
279	278	adantr 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) ∈ ℝ)
280	84, 96	absmuld 15339	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) = ((abs‘(μ‘𝑛)) · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))))
281	84	abscld 15321	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ∈ ℝ)
282	96	abscld 15321	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℝ)
283	96	absge0d 15329	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
284		mule1 26497	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (abs‘(μ‘𝑛)) ≤ 1)
285	55, 284	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ≤ 1)
286	281, 260, 282, 283, 285	lemul1ad 12094	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(μ‘𝑛)) · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (1 · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))))
287	282	recnd 11183	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℂ)
288	287	mulid2d 11173	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) = (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
289	286, 288	breqtrd 5131	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(μ‘𝑛)) · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
290	280, 289	eqbrtrd 5127	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
291	290	adantr 481	. . . . . . . 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 481	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (𝑥 / 𝑛) ∈ ℝ+)
295		simpr 485	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → e ≤ (𝑥 / 𝑛))
296	292, 293, 294, 295	mulog2sumlem1 26882	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)))) ≤ (2 · ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))))
297	71, 95	abssubd 15338	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − 𝑇)))
298	297	adantr 481	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − 𝑇)))
299	61	oveq2i 7368	. . . . . . . . . . 11 ⊢ (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − 𝑇) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)))
300	299	fveq2i 6845	. . . . . . . . . 10 ⊢ (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − 𝑇)) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿))))
301	298, 300	eqtrdi 2792	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)))))
302		2cnd 12231	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℂ)
303	11	recnd 11183	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℂ)
304	302, 303, 97	mulassd 11178	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) = (2 · (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛)))
305		rpcnne0 12933	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ+ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
306	305	ad2antlr 725	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
307		divdiv2 11867	. . . . . . . . . . . . . 14 ⊢ (((log‘(𝑥 / 𝑛)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛)) = (((log‘(𝑥 / 𝑛)) · 𝑛) / 𝑥))
308	62, 306, 109, 307	syl3anc 1371	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛)) = (((log‘(𝑥 / 𝑛)) · 𝑛) / 𝑥))
309		div23 11832	. . . . . . . . . . . . . 14 ⊢ (((log‘(𝑥 / 𝑛)) ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((log‘(𝑥 / 𝑛)) · 𝑛) / 𝑥) = (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛))
310	62, 97, 306, 309	syl3anc 1371	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛)) · 𝑛) / 𝑥) = (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛))
311	308, 310	eqtrd 2776	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛)) = (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛))
312	311	oveq2d 7373	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))) = (2 · (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛)))
313	304, 312	eqtr4d 2779	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) = (2 · ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))))
314	313	adantr 481	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) = (2 · ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))))
315	296, 301, 314	3brtr4d 5137	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛))
316	274, 276, 279, 291, 315	letrd 11312	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛))
317	273	adantr 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ∈ ℝ)
318	282	adantr 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℝ)
319	37	ad3antrrr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 𝑅 ∈ ℝ)
320	290	adantr 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
321	71	adantr 481	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 𝑇 ∈ ℂ)
322	321	abscld 15321	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘𝑇) ∈ ℝ)
323	95	adantr 481	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ)
324	323	abscld 15321	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ∈ ℝ)
325	322, 324	readdcld 11184	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘𝑇) + (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℝ)
326	321, 323	abs2dif2d 15343	. . . . . . . . 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 6845	. . . . . . . . . . . 12 ⊢ (abs‘𝑇) = (abs‘((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)))
330	329, 322	eqeltrrid 2843	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ∈ ℝ)
331	64	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (((log‘(𝑥 / 𝑛))↑2) / 2) ∈ ℂ)
332	331	abscld 15321	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) ∈ ℝ)
333	69	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((γ · (log‘(𝑥 / 𝑛))) − 𝐿) ∈ ℂ)
334	333	abscld 15321	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ∈ ℝ)
335	332, 334	readdcld 11184	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) + (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ∈ ℝ)
336	331, 333	abstrid 15341	. . . . . . . . . . . . 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 14030	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℝ)
340	339	rehalfcld 12400	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) / 2) ∈ ℝ)
341	9	sqge0d 14042	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((log‘(𝑥 / 𝑛))↑2))
342		2pos 12256	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 < 2
343	2, 342	pm3.2i 471	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 ∈ ℝ ∧ 0 < 2)
344	343	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 ∈ ℝ ∧ 0 < 2))
345		divge0 12024	. . . . . . . . . . . . . . . . . 18 ⊢ (((((log‘(𝑥 / 𝑛))↑2) ∈ ℝ ∧ 0 ≤ ((log‘(𝑥 / 𝑛))↑2)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ (((log‘(𝑥 / 𝑛))↑2) / 2))
346	339, 341, 344, 345	syl21anc 836	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (((log‘(𝑥 / 𝑛))↑2) / 2))
347	340, 346	absidd 15307	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) = (((log‘(𝑥 / 𝑛))↑2) / 2))
348	347	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) = (((log‘(𝑥 / 𝑛))↑2) / 2))
349	8	rpred 12957	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ)
350		ltle 11243	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ e ∈ ℝ) → ((𝑥 / 𝑛) < e → (𝑥 / 𝑛) ≤ e))
351	349, 199, 350	sylancl 586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) < e → (𝑥 / 𝑛) ≤ e))
352	351	imp 407	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) ≤ e)
353	8	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) ∈ ℝ+)
354		logleb 25958	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 / 𝑛) ∈ ℝ+ ∧ e ∈ ℝ+) → ((𝑥 / 𝑛) ≤ e ↔ (log‘(𝑥 / 𝑛)) ≤ (log‘e)))
355	353, 27, 354	sylancl 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((𝑥 / 𝑛) ≤ e ↔ (log‘(𝑥 / 𝑛)) ≤ (log‘e)))
356	352, 355	mpbid 231	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (log‘(𝑥 / 𝑛)) ≤ (log‘e))
357		loge 25942	. . . . . . . . . . . . . . . . . . 19 ⊢ (log‘e) = 1
358	356, 357	breqtrdi 5146	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (log‘(𝑥 / 𝑛)) ≤ 1)
359		0le1 11678	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ≤ 1
360	359	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ 1)
361	9, 260, 267, 360	le2sqd 14160	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) ≤ 1 ↔ ((log‘(𝑥 / 𝑛))↑2) ≤ (1↑2)))
362	361	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((log‘(𝑥 / 𝑛)) ≤ 1 ↔ ((log‘(𝑥 / 𝑛))↑2) ≤ (1↑2)))
363	358, 362	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((log‘(𝑥 / 𝑛))↑2) ≤ (1↑2))
364		sq1 14099	. . . . . . . . . . . . . . . . 17 ⊢ (1↑2) = 1
365	363, 364	breqtrdi 5146	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((log‘(𝑥 / 𝑛))↑2) ≤ 1)
366	339	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℝ)
367		1red 11156	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 1 ∈ ℝ)
368	343	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (2 ∈ ℝ ∧ 0 < 2))
369		lediv1 12020	. . . . . . . . . . . . . . . . 17 ⊢ ((((log‘(𝑥 / 𝑛))↑2) ∈ ℝ ∧ 1 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((log‘(𝑥 / 𝑛))↑2) ≤ 1 ↔ (((log‘(𝑥 / 𝑛))↑2) / 2) ≤ (1 / 2)))
370	366, 367, 368, 369	syl3anc 1371	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (((log‘(𝑥 / 𝑛))↑2) ≤ 1 ↔ (((log‘(𝑥 / 𝑛))↑2) / 2) ≤ (1 / 2)))
371	365, 370	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (((log‘(𝑥 / 𝑛))↑2) / 2) ≤ (1 / 2))
372	348, 371	eqbrtrd 5127	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) ≤ (1 / 2))
373	68	abscld 15321	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘𝐿) ∈ ℝ)
374	66, 373	readdcld 11184	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)) ∈ ℝ)
375	374	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)) ∈ ℝ)
376	67	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ · (log‘(𝑥 / 𝑛))) ∈ ℂ)
377	20	ad3antrrr 728	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 𝐿 ∈ ℂ)
378	376, 377	abs2dif2d 15343	. . . . . . . . . . . . . . . 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 11732	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (γ · (log‘(𝑥 / 𝑛))))
382	66, 381	absidd 15307	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(γ · (log‘(𝑥 / 𝑛)))) = (γ · (log‘(𝑥 / 𝑛))))
383	382	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(γ · (log‘(𝑥 / 𝑛)))) = (γ · (log‘(𝑥 / 𝑛))))
384	383	oveq1d 7372	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘(γ · (log‘(𝑥 / 𝑛)))) + (abs‘𝐿)) = ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)))
385	378, 384	breqtrd 5131	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ≤ ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)))
386	66	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ · (log‘(𝑥 / 𝑛))) ∈ ℝ)
387	17	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → γ ∈ ℝ)
388	377	abscld 15321	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘𝐿) ∈ ℝ)
389	9	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
390	387, 218	jctir 521	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ ∈ ℝ ∧ 0 < γ))
391		lemul2 12008	. . . . . . . . . . . . . . . . . . 19 ⊢ (((log‘(𝑥 / 𝑛)) ∈ ℝ ∧ 1 ∈ ℝ ∧ (γ ∈ ℝ ∧ 0 < γ)) → ((log‘(𝑥 / 𝑛)) ≤ 1 ↔ (γ · (log‘(𝑥 / 𝑛))) ≤ (γ · 1)))
392	389, 367, 390, 391	syl3anc 1371	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((log‘(𝑥 / 𝑛)) ≤ 1 ↔ (γ · (log‘(𝑥 / 𝑛))) ≤ (γ · 1)))
393	358, 392	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ · (log‘(𝑥 / 𝑛))) ≤ (γ · 1))
394	17	recni 11169	. . . . . . . . . . . . . . . . . 18 ⊢ γ ∈ ℂ
395	394	mulid1i 11159	. . . . . . . . . . . . . . . . 17 ⊢ (γ · 1) = γ
396	393, 395	breqtrdi 5146	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ · (log‘(𝑥 / 𝑛))) ≤ γ)
397	386, 387, 388, 396	leadd1dd 11769	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)) ≤ (γ + (abs‘𝐿)))
398	334, 375, 338, 385, 397	letrd 11312	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ≤ (γ + (abs‘𝐿)))
399	332, 334, 337, 338, 372, 398	le2addd 11774	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) + (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ≤ ((1 / 2) + (γ + (abs‘𝐿))))
400	330, 335, 327, 336, 399	letrd 11312	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ≤ ((1 / 2) + (γ + (abs‘𝐿))))
401	329, 400	eqbrtrid 5140	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘𝑇) ≤ ((1 / 2) + (γ + (abs‘𝐿))))
402	86, 92	sylan2 593	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
403	85, 402	fsumrecl 15619	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
404	403	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
405	86, 90	sylan2 593	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
406	86, 129	sylan2 593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℂ)
407	406	mulid2d 11173	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (1 · 𝑚) = 𝑚)
408		fznnfl 13767	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 / 𝑛) ∈ ℝ → (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) ↔ (𝑚 ∈ ℕ ∧ 𝑚 ≤ (𝑥 / 𝑛))))
409	349, 408	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) ↔ (𝑚 ∈ ℕ ∧ 𝑚 ≤ (𝑥 / 𝑛))))
410	409	simplbda 500	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ≤ (𝑥 / 𝑛))
411	407, 410	eqbrtrd 5127	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (1 · 𝑚) ≤ (𝑥 / 𝑛))
412		1red 11156	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 1 ∈ ℝ)
413	349	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (𝑥 / 𝑛) ∈ ℝ)
414	116	rpregt0d 12963	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (𝑚 ∈ ℝ ∧ 0 < 𝑚))
415	86, 414	sylan2 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (𝑚 ∈ ℝ ∧ 0 < 𝑚))
416		lemuldiv 12035	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℝ ∧ (𝑥 / 𝑛) ∈ ℝ ∧ (𝑚 ∈ ℝ ∧ 0 < 𝑚)) → ((1 · 𝑚) ≤ (𝑥 / 𝑛) ↔ 1 ≤ ((𝑥 / 𝑛) / 𝑚)))
417	412, 413, 415, 416	syl3anc 1371	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((1 · 𝑚) ≤ (𝑥 / 𝑛) ↔ 1 ≤ ((𝑥 / 𝑛) / 𝑚)))
418	411, 417	mpbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 1 ≤ ((𝑥 / 𝑛) / 𝑚))
419	86, 89	sylan2 593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
420		logleb 25958	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ+ ∧ ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+) → (1 ≤ ((𝑥 / 𝑛) / 𝑚) ↔ (log‘1) ≤ (log‘((𝑥 / 𝑛) / 𝑚))))
421	211, 419, 420	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (1 ≤ ((𝑥 / 𝑛) / 𝑚) ↔ (log‘1) ≤ (log‘((𝑥 / 𝑛) / 𝑚))))
422	418, 421	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (log‘1) ≤ (log‘((𝑥 / 𝑛) / 𝑚)))
423	224, 422	eqbrtrrid 5141	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 0 ≤ (log‘((𝑥 / 𝑛) / 𝑚)))
424		divge0 12024	. . . . . . . . . . . . . . . 16 ⊢ ((((log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ ∧ 0 ≤ (log‘((𝑥 / 𝑛) / 𝑚))) ∧ (𝑚 ∈ ℝ ∧ 0 < 𝑚)) → 0 ≤ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))
425	405, 423, 415, 424	syl21anc 836	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 0 ≤ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))
426	85, 402, 425	fsumge0 15680	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))
427	426	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 0 ≤ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))
428	404, 427	absidd 15307	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))
429		fzfid 13878	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
430	349	flcld 13703	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℤ)
431	430	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (⌊‘(𝑥 / 𝑛)) ∈ ℤ)
432		2z 12535	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℤ
433	432	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 2 ∈ ℤ)
434	349	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) ∈ ℝ)
435	199	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → e ∈ ℝ)
436		3re 12233	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 3 ∈ ℝ
437	436	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 3 ∈ ℝ)
438		simpr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) < e)
439	203	simpri 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ e < 3
440	439	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → e < 3)
441	434, 435, 437, 438, 440	lttrd 11316	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) < 3)
442		3z 12536	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 3 ∈ ℤ
443		fllt 13711	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ 3 ∈ ℤ) → ((𝑥 / 𝑛) < 3 ↔ (⌊‘(𝑥 / 𝑛)) < 3))
444	434, 442, 443	sylancl 586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((𝑥 / 𝑛) < 3 ↔ (⌊‘(𝑥 / 𝑛)) < 3))
445	441, 444	mpbid 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (⌊‘(𝑥 / 𝑛)) < 3)
446		df-3 12217	. . . . . . . . . . . . . . . . . . . 20 ⊢ 3 = (2 + 1)
447	445, 446	breqtrdi 5146	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (⌊‘(𝑥 / 𝑛)) < (2 + 1))
448		zleltp1 12554	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((⌊‘(𝑥 / 𝑛)) ∈ ℤ ∧ 2 ∈ ℤ) → ((⌊‘(𝑥 / 𝑛)) ≤ 2 ↔ (⌊‘(𝑥 / 𝑛)) < (2 + 1)))
449	431, 432, 448	sylancl 586	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((⌊‘(𝑥 / 𝑛)) ≤ 2 ↔ (⌊‘(𝑥 / 𝑛)) < (2 + 1)))
450	447, 449	mpbird 256	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (⌊‘(𝑥 / 𝑛)) ≤ 2)
451		eluz2 12769	. . . . . . . . . . . . . . . . . 18 ⊢ (2 ∈ (ℤ≥‘(⌊‘(𝑥 / 𝑛))) ↔ ((⌊‘(𝑥 / 𝑛)) ∈ ℤ ∧ 2 ∈ ℤ ∧ (⌊‘(𝑥 / 𝑛)) ≤ 2))
452	431, 433, 450, 451	syl3anbrc 1343	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 2 ∈ (ℤ≥‘(⌊‘(𝑥 / 𝑛))))
453		fzss2 13481	. . . . . . . . . . . . . . . . 17 ⊢ (2 ∈ (ℤ≥‘(⌊‘(𝑥 / 𝑛))) → (1...(⌊‘(𝑥 / 𝑛))) ⊆ (1...2))
454	452, 453	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (1...(⌊‘(𝑥 / 𝑛))) ⊆ (1...2))
455	454	sselda 3944	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ (1...2))
456	34	ad5ant15 757	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
457	455, 456	syldan 591	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
458	429, 457	fsumrecl 15619	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
459	92	adantlr 713	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ ℕ) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
460	86, 459	sylan2 593	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
461	352	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (𝑥 / 𝑛) ≤ e)
462	434	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (𝑥 / 𝑛) ∈ ℝ)
463	199	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → e ∈ ℝ)
464	30	rpregt0d 12963	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (𝑚 ∈ ℝ ∧ 0 < 𝑚))
465	464	ad5ant15 757	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (𝑚 ∈ ℝ ∧ 0 < 𝑚))
466		lediv1 12020	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ e ∈ ℝ ∧ (𝑚 ∈ ℝ ∧ 0 < 𝑚)) → ((𝑥 / 𝑛) ≤ e ↔ ((𝑥 / 𝑛) / 𝑚) ≤ (e / 𝑚)))
467	462, 463, 465, 466	syl3anc 1371	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((𝑥 / 𝑛) ≤ e ↔ ((𝑥 / 𝑛) / 𝑚) ≤ (e / 𝑚)))
468	461, 467	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((𝑥 / 𝑛) / 𝑚) ≤ (e / 𝑚))
469	89	adantlr 713	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ ℕ) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
470	28, 469	sylan2 593	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
471	32	ad5ant15 757	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (e / 𝑚) ∈ ℝ+)
472	470, 471	logled 25982	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (((𝑥 / 𝑛) / 𝑚) ≤ (e / 𝑚) ↔ (log‘((𝑥 / 𝑛) / 𝑚)) ≤ (log‘(e / 𝑚))))
473	468, 472	mpbid 231	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (log‘((𝑥 / 𝑛) / 𝑚)) ≤ (log‘(e / 𝑚)))
474	90	adantlr 713	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ ℕ) → (log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
475	28, 474	sylan2 593	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
476	33	ad5ant15 757	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (log‘(e / 𝑚)) ∈ ℝ)
477		lediv1 12020	. . . . . . . . . . . . . . . . 17 ⊢ (((log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ ∧ (log‘(e / 𝑚)) ∈ ℝ ∧ (𝑚 ∈ ℝ ∧ 0 < 𝑚)) → ((log‘((𝑥 / 𝑛) / 𝑚)) ≤ (log‘(e / 𝑚)) ↔ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ ((log‘(e / 𝑚)) / 𝑚)))
478	475, 476, 465, 477	syl3anc 1371	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((log‘((𝑥 / 𝑛) / 𝑚)) ≤ (log‘(e / 𝑚)) ↔ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ ((log‘(e / 𝑚)) / 𝑚)))
479	473, 478	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ ((log‘(e / 𝑚)) / 𝑚))
480	455, 479	syldan 591	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ ((log‘(e / 𝑚)) / 𝑚))
481	429, 460, 457, 480	fsumle 15684	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘(e / 𝑚)) / 𝑚))
482		fzfid 13878	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (1...2) ∈ Fin)
483	243	ad5ant15 757	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → 0 ≤ ((log‘(e / 𝑚)) / 𝑚))
484	482, 456, 483, 454	fsumless 15681	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘(e / 𝑚)) / 𝑚) ≤ Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚))
485	404, 458, 328, 481, 484	letrd 11312	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚))
486	428, 485	eqbrtrd 5127	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ≤ Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚))
487	322, 324, 327, 328, 401, 486	le2addd 11774	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘𝑇) + (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ (((1 / 2) + (γ + (abs‘𝐿))) + Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚)))
488	487, 15	breqtrrdi 5147	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘𝑇) + (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ 𝑅)
489	318, 325, 319, 326, 488	letrd 11312	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ 𝑅)
490	317, 318, 319, 320, 489	letrd 11312	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ 𝑅)
491	4, 208, 248, 249, 251, 272, 316, 490	fsumharmonic 26361	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · ((log‘e) + 1))))
492		2cnd 12231	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 ∈ ℂ)
493	3, 492, 303	fsummulc2 15669	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((log‘(𝑥 / 𝑛)) / 𝑥)))
494		df-2 12216	. . . . . . . . . 10 ⊢ 2 = (1 + 1)
495	357	oveq1i 7367	. . . . . . . . . 10 ⊢ ((log‘e) + 1) = (1 + 1)
496	494, 495	eqtr4i 2767	. . . . . . . . 9 ⊢ 2 = ((log‘e) + 1)
497	496	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 = ((log‘e) + 1))
498	497	oveq2d 7373	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑅 · 2) = (𝑅 · ((log‘e) + 1)))
499	493, 498	oveq12d 7375	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · ((log‘e) + 1))))
500	491, 499	breqtrrd 5133	. . . . 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 5129	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ≤ ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)))
503	54	leabsd 15299	. . . 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 11312	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ≤ (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))))
506	1, 53, 54, 77, 505	o1le 15537	1 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ∈ 𝑂(1))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2943  {crab 3407   ⊆ wss 3910   class class class wbr 5105   ↦ cmpt 5188  ‘cfv 6496  (class class class)co 7357  ℂcc 11049  ℝcr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056   < clt 11189   ≤ cle 11190   − cmin 11385   / cdiv 11812  ℕcn 12153  2c2 12208  3c3 12209  ℤcz 12499  ℤ_≥cuz 12763  ℝ⁺crp 12915  ...cfz 13424  ⌊cfl 13695  ↑cexp 13967  abscabs 15119   ⇝_𝑟 crli 15367  𝑂(1)co1 15368  Σcsu 15570  eceu 15945   ∥ cdvds 16136  logclog 25910  γcem 26341  μcmu 26444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-addf 11130  ax-mulf 11131

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-disj 5071  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-oadd 8416  df-er 8648  df-map 8767  df-pm 8768  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-fi 9347  df-sup 9378  df-inf 9379  df-oi 9446  df-dju 9837  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-xnn0 12486  df-z 12500  df-dec 12619  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ioo 13268  df-ioc 13269  df-ico 13270  df-icc 13271  df-fz 13425  df-fzo 13568  df-fl 13697  df-mod 13775  df-seq 13907  df-exp 13968  df-fac 14174  df-bc 14203  df-hash 14231  df-shft 14952  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-limsup 15353  df-clim 15370  df-rlim 15371  df-o1 15372  df-lo1 15373  df-sum 15571  df-ef 15950  df-e 15951  df-sin 15952  df-cos 15953  df-tan 15954  df-pi 15955  df-dvds 16137  df-gcd 16375  df-prm 16548  df-pc 16709  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-hom 17157  df-cco 17158  df-rest 17304  df-topn 17305  df-0g 17323  df-gsum 17324  df-topgen 17325  df-pt 17326  df-prds 17329  df-xrs 17384  df-qtop 17389  df-imas 17390  df-xps 17392  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-submnd 18602  df-mulg 18873  df-cntz 19097  df-cmn 19564  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-fbas 20793  df-fg 20794  df-cnfld 20797  df-top 22243  df-topon 22260  df-topsp 22282  df-bases 22296  df-cld 22370  df-ntr 22371  df-cls 22372  df-nei 22449  df-lp 22487  df-perf 22488  df-cn 22578  df-cnp 22579  df-haus 22666  df-cmp 22738  df-tx 22913  df-hmeo 23106  df-fil 23197  df-fm 23289  df-flim 23290  df-flf 23291  df-xms 23673  df-ms 23674  df-tms 23675  df-cncf 24241  df-limc 25230  df-dv 25231  df-ulm 25736  df-log 25912  df-cxp 25913  df-atan 26217  df-em 26342  df-mu 26450

This theorem is referenced by:  mulog2sumlem3  26884