Theorem mulog2sumlem2 27844

Description: Lemma for mulog2sum 27846. (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 11290	. 2 ⊢ (𝜑 → 1 ∈ ℝ)
2		2re 12398	. . . 4 ⊢ 2 ∈ ℝ
3		fzfid 14096	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin)
4		simpr 490	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
5		elfznn 13667	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
6	5	nnrpd 13143	. . . . . . . 8 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℝ+)
7		rpdivcl 13128	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) → (𝑥 / 𝑛) ∈ ℝ+)
8	4, 6, 7	syl2an 608	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ+)
9	8	relogcld 26933	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
10		simplr 781	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ+)
11	9, 10	rerpdivcld 13176	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℝ)
12	3, 11	fsumrecl 15880	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℝ)
13		remulcl 11266	. . . 4 ⊢ ((2 ∈ ℝ ∧ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℝ) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ ℝ)
14	2, 12, 13	sylancr 599	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ ℝ)
15		mulog2sumlem2.r	. . . . . 6 ⊢ 𝑅 = (((1 / 2) + (γ + (abs‘𝐿))) + Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚))
16		halfre 12540	. . . . . . . 8 ⊢ (1 / 2) ∈ ℝ
17		emre 27315	. . . . . . . . 9 ⊢ γ ∈ ℝ
18		mulog2sumlem.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐿)
19		rlimcl 15650	. . . . . . . . . . 11 ⊢ (𝐹 ⇝𝑟 𝐿 → 𝐿 ∈ ℂ)
20	18, 19	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ ℂ)
21	20	abscld 15586	. . . . . . . . 9 ⊢ (𝜑 → (abs‘𝐿) ∈ ℝ)
22		readdcl 11264	. . . . . . . . 9 ⊢ ((γ ∈ ℝ ∧ (abs‘𝐿) ∈ ℝ) → (γ + (abs‘𝐿)) ∈ ℝ)
23	17, 21, 22	sylancr 599	. . . . . . . 8 ⊢ (𝜑 → (γ + (abs‘𝐿)) ∈ ℝ)
24		readdcl 11264	. . . . . . . 8 ⊢ (((1 / 2) ∈ ℝ ∧ (γ + (abs‘𝐿)) ∈ ℝ) → ((1 / 2) + (γ + (abs‘𝐿))) ∈ ℝ)
25	16, 23, 24	sylancr 599	. . . . . . 7 ⊢ (𝜑 → ((1 / 2) + (γ + (abs‘𝐿))) ∈ ℝ)
26		fzfid 14096	. . . . . . . 8 ⊢ (𝜑 → (1...2) ∈ Fin)
27		epr 16356	. . . . . . . . . . 11 ⊢ e ∈ ℝ+
28		elfznn 13667	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (1...2) → 𝑚 ∈ ℕ)
29	28	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ∈ ℕ)
30	29	nnrpd 13143	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ∈ ℝ+)
31		rpdivcl 13128	. . . . . . . . . . 11 ⊢ ((e ∈ ℝ+ ∧ 𝑚 ∈ ℝ+) → (e / 𝑚) ∈ ℝ+)
32	27, 30, 31	sylancr 599	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (e / 𝑚) ∈ ℝ+)
33	32	relogcld 26933	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (log‘(e / 𝑚)) ∈ ℝ)
34	33, 29	nndivred 12373	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → ((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
35	26, 34	fsumrecl 15880	. . . . . . 7 ⊢ (𝜑 → Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
36	25, 35	readdcld 11319	. . . . . 6 ⊢ (𝜑 → (((1 / 2) + (γ + (abs‘𝐿))) + Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚)) ∈ ℝ)
37	15, 36	eqeltrid 2865	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ ℝ)
38		remulcl 11266	. . . . 5 ⊢ ((𝑅 ∈ ℝ ∧ 2 ∈ ℝ) → (𝑅 · 2) ∈ ℝ)
39	37, 2, 38	sylancl 598	. . . 4 ⊢ (𝜑 → (𝑅 · 2) ∈ ℝ)
40	39	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑅 · 2) ∈ ℝ)
41	2	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 ∈ ℝ)
42		rpssre 13109	. . . . 5 ⊢ ℝ+ ⊆ ℝ
43		2cnd 12402	. . . . 5 ⊢ (𝜑 → 2 ∈ ℂ)
44		o1const 15767	. . . . 5 ⊢ ((ℝ+ ⊆ ℝ ∧ 2 ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ 2) ∈ 𝑂(1))
45	42, 43, 44	sylancr 599	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ 2) ∈ 𝑂(1))
46		logfacrlim2 27535	. . . . 5 ⊢ (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ⇝𝑟 1
47		rlimo1 15764	. . . . 5 ⊢ ((𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ⇝𝑟 1 → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ 𝑂(1))
48	46, 47	mp1i 14	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ 𝑂(1))
49	41, 12, 45, 48	o1mul2 15772	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥))) ∈ 𝑂(1))
50	39	recnd 11318	. . . 4 ⊢ (𝜑 → (𝑅 · 2) ∈ ℂ)
51		o1const 15767	. . . 4 ⊢ ((ℝ+ ⊆ ℝ ∧ (𝑅 · 2) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ (𝑅 · 2)) ∈ 𝑂(1))
52	42, 50, 51	sylancr 599	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (𝑅 · 2)) ∈ 𝑂(1))
53	14, 40, 49, 52	o1add2 15771	. 2 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))) ∈ 𝑂(1))
54	14, 40	readdcld 11319	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ∈ ℝ)
55	5	adantl 487	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
56		mucl 27450	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (μ‘𝑛) ∈ ℤ)
57	55, 56	syl 18	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℤ)
58	57	zred 12784	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℝ)
59	58, 55	nndivred 12373	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℝ)
60	59	recnd 11318	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℂ)
61		mulog2sumlem2.t	. . . . . 6 ⊢ 𝑇 = ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿))
62	9	recnd 11318	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℂ)
63	62	sqcld 14267	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℂ)
64	63	halfcld 12572	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) / 2) ∈ ℂ)
65		remulcl 11266	. . . . . . . . . 10 ⊢ ((γ ∈ ℝ ∧ (log‘(𝑥 / 𝑛)) ∈ ℝ) → (γ · (log‘(𝑥 / 𝑛))) ∈ ℝ)
66	17, 9, 65	sylancr 599	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (γ · (log‘(𝑥 / 𝑛))) ∈ ℝ)
67	66	recnd 11318	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (γ · (log‘(𝑥 / 𝑛))) ∈ ℂ)
68	20	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝐿 ∈ ℂ)
69	67, 68	subcld 11650	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((γ · (log‘(𝑥 / 𝑛))) − 𝐿) ∈ ℂ)
70	64, 69	addcld 11309	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ∈ ℂ)
71	61, 70	eqeltrid 2865	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑇 ∈ ℂ)
72	60, 71	mulcld 11310	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · 𝑇) ∈ ℂ)
73	3, 72	fsumcl 15879	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) ∈ ℂ)
74		relogcl 26885	. . . . 5 ⊢ (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
75	74	adantl 487	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
76	75	recnd 11318	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℂ)
77	73, 76	subcld 11650	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥)) ∈ ℂ)
78	77	abscld 15586	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ∈ ℝ)
79	78	adantrr 730	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ∈ ℝ)
80	54	adantrr 730	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ∈ ℝ)
81	54	recnd 11318	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ∈ ℂ)
82	81	abscld 15586	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))) ∈ ℝ)
83	82	adantrr 730	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))) ∈ ℝ)
84	57	zcnd 12785	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℂ)
85		fzfid 14096	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
86		elfznn 13667	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) → 𝑚 ∈ ℕ)
87		nnrp 13113	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℝ+)
88		rpdivcl 13128	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 / 𝑛) ∈ ℝ+ ∧ 𝑚 ∈ ℝ+) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
89	8, 87, 88	syl2an 608	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
90	89	relogcld 26933	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
91		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℕ)
92	90, 91	nndivred 12373	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
93	92	recnd 11318	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ)
94	86, 93	sylan2 605	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ)
95	85, 94	fsumcl 15879	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ)
96	71, 95	subcld 11650	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ∈ ℂ)
97	55	nncnd 12332	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
98	55	nnne0d 12369	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0)
99	84, 96, 97, 98	div23d 12111	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = (((μ‘𝑛) / 𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
100	60, 71, 95	subdid 11753	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = ((((μ‘𝑛) / 𝑛) · 𝑇) − (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
101	99, 100	eqtrd 2796	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = ((((μ‘𝑛) / 𝑛) · 𝑇) − (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
102	101	sumeq2dv 15849	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))((((μ‘𝑛) / 𝑛) · 𝑇) − (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
103	60, 95	mulcld 11310	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ∈ ℂ)
104	3, 72, 103	fsumsub 15934	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((μ‘𝑛) / 𝑛) · 𝑇) − (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
105	102, 104	eqtrd 2796	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
106	105	adantrr 730	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
107	85, 60, 94	fsummulc2 15930	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))
108	84	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (μ‘𝑛) ∈ ℂ)
109	97, 98	jca 521	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
110	109	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
111		div23 11974	. . . . . . . . . . . . . . . . 17 ⊢ (((μ‘𝑛) ∈ ℂ ∧ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((μ‘𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) / 𝑛) = (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))
112		divass 11973	. . . . . . . . . . . . . . . . 17 ⊢ (((μ‘𝑛) ∈ ℂ ∧ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((μ‘𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) / 𝑛) = ((μ‘𝑛) · (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛)))
113	111, 112	eqtr3d 2798	. . . . . . . . . . . . . . . 16 ⊢ (((μ‘𝑛) ∈ ℂ ∧ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = ((μ‘𝑛) · (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛)))
114	108, 93, 110, 113	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = ((μ‘𝑛) · (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛)))
115	90	recnd 11318	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℂ)
116	91	nnrpd 13143	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ+)
117		rpcnne0 13120	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ ℝ+ → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0))
118	116, 117	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0))
119		divdiv1 12009	. . . . . . . . . . . . . . . . . 18 ⊢ (((log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℂ ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0) ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛) = ((log‘((𝑥 / 𝑛) / 𝑚)) / (𝑚 · 𝑛)))
120	115, 118, 110, 119	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛) = ((log‘((𝑥 / 𝑛) / 𝑚)) / (𝑚 · 𝑛)))
121		rpre 13110	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ)
122	121	adantl 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
123	122	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
124	123	recnd 11318	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℂ)
125	124	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → 𝑥 ∈ ℂ)
126		divdiv1 12009	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0) ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) → ((𝑥 / 𝑛) / 𝑚) = (𝑥 / (𝑛 · 𝑚)))
127	125, 110, 118, 126	syl3anc 1398	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((𝑥 / 𝑛) / 𝑚) = (𝑥 / (𝑛 · 𝑚)))
128	127	fveq2d 6881	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (log‘((𝑥 / 𝑛) / 𝑚)) = (log‘(𝑥 / (𝑛 · 𝑚))))
129	91	nncnd 12332	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
130	97	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → 𝑛 ∈ ℂ)
131	129, 130	mulcomd 11311	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (𝑚 · 𝑛) = (𝑛 · 𝑚))
132	128, 131	oveq12d 7430	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((log‘((𝑥 / 𝑛) / 𝑚)) / (𝑚 · 𝑛)) = ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚)))
133	120, 132	eqtrd 2796	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛) = ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚)))
134	133	oveq2d 7428	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((μ‘𝑛) · (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛)) = ((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
135	114, 134	eqtrd 2796	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = ((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
136	86, 135	sylan2 605	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = ((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
137	136	sumeq2dv 15849	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
138	107, 137	eqtrd 2796	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
139	138	sumeq2dv 15849	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
140		oveq2 7420	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑛 · 𝑚) → (𝑥 / 𝑘) = (𝑥 / (𝑛 · 𝑚)))
141	140	fveq2d 6881	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑛 · 𝑚) → (log‘(𝑥 / 𝑘)) = (log‘(𝑥 / (𝑛 · 𝑚))))
142		id 23	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑛 · 𝑚) → 𝑘 = (𝑛 · 𝑚))
143	141, 142	oveq12d 7430	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑛 · 𝑚) → ((log‘(𝑥 / 𝑘)) / 𝑘) = ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚)))
144	143	oveq2d 7428	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑛 · 𝑚) → ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) = ((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
145	4	rpred 13145	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
146		ssrab2 4028	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ ℕ
147		simprr 785	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})
148	146, 147	sselid 3929	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ ℕ)
149	148, 56	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (μ‘𝑛) ∈ ℤ)
150	149	zred 12784	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (μ‘𝑛) ∈ ℝ)
151		elfznn 13667	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (1...(⌊‘𝑥)) → 𝑘 ∈ ℕ)
152	151	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → 𝑘 ∈ ℕ)
153	152	nnrpd 13143	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → 𝑘 ∈ ℝ+)
154		rpdivcl 13128	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑘 ∈ ℝ+) → (𝑥 / 𝑘) ∈ ℝ+)
155	4, 153, 154	syl2an 608	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (𝑥 / 𝑘) ∈ ℝ+)
156	155	relogcld 26933	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (log‘(𝑥 / 𝑘)) ∈ ℝ)
157	151	ad2antrl 741	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑘 ∈ ℕ)
158	156, 157	nndivred 12373	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → ((log‘(𝑥 / 𝑘)) / 𝑘) ∈ ℝ)
159	150, 158	remulcld 11320	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) ∈ ℝ)
160	159	recnd 11318	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) ∈ ℂ)
161	144, 145, 160	dvdsflsumcom 27497	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
162	139, 161	eqtr4d 2799	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)))
163	162	adantrr 730	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)))
164		oveq2 7420	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → (𝑥 / 𝑘) = (𝑥 / 1))
165	164	fveq2d 6881	. . . . . . . . . 10 ⊢ (𝑘 = 1 → (log‘(𝑥 / 𝑘)) = (log‘(𝑥 / 1)))
166		id 23	. . . . . . . . . 10 ⊢ (𝑘 = 1 → 𝑘 = 1)
167	165, 166	oveq12d 7430	. . . . . . . . 9 ⊢ (𝑘 = 1 → ((log‘(𝑥 / 𝑘)) / 𝑘) = ((log‘(𝑥 / 1)) / 1))
168		fzfid 14096	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin)
169		fz1ssnn 13669	. . . . . . . . . 10 ⊢ (1...(⌊‘𝑥)) ⊆ ℕ
170	169	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ⊆ ℕ)
171	122	adantrr 730	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ)
172		simprr 785	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥)
173		flge1nn 13941	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ)
174	171, 172, 173	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (⌊‘𝑥) ∈ ℕ)
175		nnuz 12985	. . . . . . . . . . 11 ⊢ ℕ = (ℤ≥‘1)
176	174, 175	eleqtrdi 2871	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (⌊‘𝑥) ∈ (ℤ≥‘1))
177		eluzfz1 13644	. . . . . . . . . 10 ⊢ ((⌊‘𝑥) ∈ (ℤ≥‘1) → 1 ∈ (1...(⌊‘𝑥)))
178	176, 177	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ (1...(⌊‘𝑥)))
179	151	nnrpd 13143	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1...(⌊‘𝑥)) → 𝑘 ∈ ℝ+)
180	4, 179, 154	syl2an 608	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑘) ∈ ℝ+)
181	180	relogcld 26933	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑘)) ∈ ℝ)
182	169	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ⊆ ℕ)
183	182	sselda 3931	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → 𝑘 ∈ ℕ)
184	181, 183	nndivred 12373	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑘)) / 𝑘) ∈ ℝ)
185	184	recnd 11318	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑘)) / 𝑘) ∈ ℂ)
186	185	adantlrr 734	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑘)) / 𝑘) ∈ ℂ)
187	167, 168, 170, 178, 186	musumsum 27501	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) = ((log‘(𝑥 / 1)) / 1))
188	4	rpcnd 13147	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
189	188	div1d 12066	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 / 1) = 𝑥)
190	189	fveq2d 6881	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (log‘(𝑥 / 1)) = (log‘𝑥))
191	190	oveq1d 7427	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((log‘(𝑥 / 1)) / 1) = ((log‘𝑥) / 1))
192	76	div1d 12066	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((log‘𝑥) / 1) = (log‘𝑥))
193	191, 192	eqtrd 2796	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((log‘(𝑥 / 1)) / 1) = (log‘𝑥))
194	193	adantrr 730	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘(𝑥 / 1)) / 1) = (log‘𝑥))
195	163, 187, 194	3eqtrd 2800	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = (log‘𝑥))
196	195	oveq2d 7428	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥)))
197	106, 196	eqtrd 2796	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥)))
198	197	fveq2d 6881	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛)) = (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))))
199		ere 16235	. . . . . . . . 9 ⊢ e ∈ ℝ
200	199	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → e ∈ ℝ)
201		1re 11289	. . . . . . . . 9 ⊢ 1 ∈ ℝ
202		1lt2 12496	. . . . . . . . . 10 ⊢ 1 < 2
203		egt2lt3 16354	. . . . . . . . . . 11 ⊢ (2 < e ∧ e < 3)
204	203	simpli 489	. . . . . . . . . 10 ⊢ 2 < e
205	201, 2, 199	lttri 11417	. . . . . . . . . 10 ⊢ ((1 < 2 ∧ 2 < e) → 1 < e)
206	202, 204, 205	mp2an 705	. . . . . . . . 9 ⊢ 1 < e
207	201, 199, 206	ltleii 11414	. . . . . . . 8 ⊢ 1 ≤ e
208	200, 207	jctir 530	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (e ∈ ℝ ∧ 1 ≤ e))
209	37	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑅 ∈ ℝ)
210	16	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 / 2) ∈ ℝ)
211		1rp 13105	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ+
212		rphalfcl 13130	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℝ+ → (1 / 2) ∈ ℝ+)
213	211, 212	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (1 / 2) ∈ ℝ+
214		rpge0 13115	. . . . . . . . . . . . 13 ⊢ ((1 / 2) ∈ ℝ+ → 0 ≤ (1 / 2))
215	213, 214	mp1i 14	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ (1 / 2))
216	17	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → γ ∈ ℝ)
217		0re 11291	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ
218		emgt0 27316	. . . . . . . . . . . . . . 15 ⊢ 0 < γ
219	217, 17, 218	ltleii 11414	. . . . . . . . . . . . . 14 ⊢ 0 ≤ γ
220	219	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ γ)
221	20	absge0d 15594	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ (abs‘𝐿))
222	216, 21, 220, 221	addge0d 11873	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ (γ + (abs‘𝐿)))
223	210, 23, 215, 222	addge0d 11873	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ ((1 / 2) + (γ + (abs‘𝐿))))
224		log1 26895	. . . . . . . . . . . . . 14 ⊢ (log‘1) = 0
225	29	nncnd 12332	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ∈ ℂ)
226	225	mullidd 11308	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (1 · 𝑚) = 𝑚)
227	30	rpred 13145	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ∈ ℝ)
228	2	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 2 ∈ ℝ)
229	199	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → e ∈ ℝ)
230		elfzle2 13641	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ (1...2) → 𝑚 ≤ 2)
231	230	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ≤ 2)
232	2, 199, 204	ltleii 11414	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ≤ e
233	232	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 2 ≤ e)
234	227, 228, 229, 231, 233	letrd 11448	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ≤ e)
235	226, 234	eqbrtrd 5127	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (1 · 𝑚) ≤ e)
236		1red 11290	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 1 ∈ ℝ)
237	236, 229, 30	lemuldivd 13194	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → ((1 · 𝑚) ≤ e ↔ 1 ≤ (e / 𝑚)))
238	235, 237	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 1 ≤ (e / 𝑚))
239		logleb 26913	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℝ+ ∧ (e / 𝑚) ∈ ℝ+) → (1 ≤ (e / 𝑚) ↔ (log‘1) ≤ (log‘(e / 𝑚))))
240	211, 32, 239	sylancr 599	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (1 ≤ (e / 𝑚) ↔ (log‘1) ≤ (log‘(e / 𝑚))))
241	238, 240	mpbid 235	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (log‘1) ≤ (log‘(e / 𝑚)))
242	224, 241	eqbrtrrid 5141	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 0 ≤ (log‘(e / 𝑚)))
243	33, 30, 242	divge0d 13185	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 0 ≤ ((log‘(e / 𝑚)) / 𝑚))
244	26, 34, 243	fsumge0 15942	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚))
245	25, 35, 223, 244	addge0d 11873	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ (((1 / 2) + (γ + (abs‘𝐿))) + Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚)))
246	245, 15	breqtrrdi 5147	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝑅)
247	246	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 0 ≤ 𝑅)
248	209, 247	jca 521	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅))
249	84, 96	mulcld 11310	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℂ)
250		remulcl 11266	. . . . . . . 8 ⊢ ((2 ∈ ℝ ∧ ((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℝ) → (2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ ℝ)
251	2, 11, 250	sylancr 599	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ ℝ)
252	2	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℝ)
253		0le2 12426	. . . . . . . . 9 ⊢ 0 ≤ 2
254	253	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ 2)
255	97	mullidd 11308	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) = 𝑛)
256		fznnfl 13982	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥)))
257	122, 256	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥)))
258	257	simplbda 505	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≤ 𝑥)
259	255, 258	eqbrtrd 5127	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) ≤ 𝑥)
260		1red 11290	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
261	55	nnrpd 13143	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+)
262	260, 123, 261	lemuldivd 13194	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛)))
263	259, 262	mpbid 235	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ (𝑥 / 𝑛))
264		logleb 26913	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℝ+ ∧ (𝑥 / 𝑛) ∈ ℝ+) → (1 ≤ (𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛))))
265	211, 8, 264	sylancr 599	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 ≤ (𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛))))
266	263, 265	mpbid 235	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘1) ≤ (log‘(𝑥 / 𝑛)))
267	224, 266	eqbrtrrid 5141	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (log‘(𝑥 / 𝑛)))
268		rpregt0 13116	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
269	268	ad2antlr 740	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
270		divge0 12167	. . . . . . . . 9 ⊢ ((((log‘(𝑥 / 𝑛)) ∈ ℝ ∧ 0 ≤ (log‘(𝑥 / 𝑛))) ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → 0 ≤ ((log‘(𝑥 / 𝑛)) / 𝑥))
271	9, 267, 269, 270	syl21anc 851	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((log‘(𝑥 / 𝑛)) / 𝑥))
272	252, 11, 254, 271	mulge0d 11874	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (2 · ((log‘(𝑥 / 𝑛)) / 𝑥)))
273	249	abscld 15586	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ∈ ℝ)
274	273	adantr 486	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ∈ ℝ)
275	96	adantr 486	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ∈ ℂ)
276	275	abscld 15586	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℝ)
277	261	rpred 13145	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ)
278	251, 277	remulcld 11320	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) ∈ ℝ)
279	278	adantr 486	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) ∈ ℝ)
280	84, 96	absmuld 15604	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) = ((abs‘(μ‘𝑛)) · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))))
281	84	abscld 15586	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ∈ ℝ)
282	96	abscld 15586	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℝ)
283	96	absge0d 15594	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
284		mule1 27457	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (abs‘(μ‘𝑛)) ≤ 1)
285	55, 284	syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ≤ 1)
286	281, 260, 282, 283, 285	lemul1ad 12237	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(μ‘𝑛)) · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (1 · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))))
287	282	recnd 11318	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℂ)
288	287	mullidd 11308	. . . . . . . . . . 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 486	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
292		logdivsum.1	. . . . . . . . . 10 ⊢ 𝐹 = (𝑦 ∈ ℝ+ ↦ (Σ𝑖 ∈ (1...(⌊‘𝑦))((log‘𝑖) / 𝑖) − (((log‘𝑦)↑2) / 2)))
293	18	ad3antrrr 743	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → 𝐹 ⇝𝑟 𝐿)
294	8	adantr 486	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (𝑥 / 𝑛) ∈ ℝ+)
295		simpr 490	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → e ≤ (𝑥 / 𝑛))
296	292, 293, 294, 295	mulog2sumlem1 27843	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)))) ≤ (2 · ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))))
297	71, 95	abssubd 15603	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − 𝑇)))
298	297	adantr 486	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − 𝑇)))
299	61	oveq2i 7423	. . . . . . . . . . 11 ⊢ (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − 𝑇) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)))
300	299	fveq2i 6880	. . . . . . . . . 10 ⊢ (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − 𝑇)) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿))))
301	298, 300	eqtrdi 2812	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)))))
302		2cnd 12402	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℂ)
303	11	recnd 11318	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℂ)
304	302, 303, 97	mulassd 11313	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) = (2 · (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛)))
305		rpcnne0 13120	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ+ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
306	305	ad2antlr 740	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
307		divdiv2 12010	. . . . . . . . . . . . . 14 ⊢ (((log‘(𝑥 / 𝑛)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛)) = (((log‘(𝑥 / 𝑛)) · 𝑛) / 𝑥))
308	62, 306, 109, 307	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛)) = (((log‘(𝑥 / 𝑛)) · 𝑛) / 𝑥))
309		div23 11974	. . . . . . . . . . . . . 14 ⊢ (((log‘(𝑥 / 𝑛)) ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((log‘(𝑥 / 𝑛)) · 𝑛) / 𝑥) = (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛))
310	62, 97, 306, 309	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛)) · 𝑛) / 𝑥) = (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛))
311	308, 310	eqtrd 2796	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛)) = (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛))
312	311	oveq2d 7428	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))) = (2 · (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛)))
313	304, 312	eqtr4d 2799	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) = (2 · ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))))
314	313	adantr 486	. . . . . . . . 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 11448	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛))
317	273	adantr 486	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ∈ ℝ)
318	282	adantr 486	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℝ)
319	37	ad3antrrr 743	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 𝑅 ∈ ℝ)
320	290	adantr 486	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
321	71	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 𝑇 ∈ ℂ)
322	321	abscld 15586	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘𝑇) ∈ ℝ)
323	95	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ)
324	323	abscld 15586	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ∈ ℝ)
325	322, 324	readdcld 11319	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘𝑇) + (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℝ)
326	321, 323	abs2dif2d 15608	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ ((abs‘𝑇) + (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
327	25	ad3antrrr 743	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((1 / 2) + (γ + (abs‘𝐿))) ∈ ℝ)
328	35	ad3antrrr 743	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
329	61	fveq2i 6880	. . . . . . . . . . . 12 ⊢ (abs‘𝑇) = (abs‘((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)))
330	329, 322	eqeltrrid 2866	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ∈ ℝ)
331	64	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (((log‘(𝑥 / 𝑛))↑2) / 2) ∈ ℂ)
332	331	abscld 15586	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) ∈ ℝ)
333	69	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((γ · (log‘(𝑥 / 𝑛))) − 𝐿) ∈ ℂ)
334	333	abscld 15586	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ∈ ℝ)
335	332, 334	readdcld 11319	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) + (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ∈ ℝ)
336	331, 333	abstrid 15606	. . . . . . . . . . . . 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 743	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ + (abs‘𝐿)) ∈ ℝ)
339	9	resqcld 14248	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℝ)
340	339	rehalfcld 12574	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) / 2) ∈ ℝ)
341	9	sqge0d 14260	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((log‘(𝑥 / 𝑛))↑2))
342		2pos 12428	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 < 2
343	2, 342	pm3.2i 476	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 ∈ ℝ ∧ 0 < 2)
344	343	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 ∈ ℝ ∧ 0 < 2))
345		divge0 12167	. . . . . . . . . . . . . . . . . 18 ⊢ (((((log‘(𝑥 / 𝑛))↑2) ∈ ℝ ∧ 0 ≤ ((log‘(𝑥 / 𝑛))↑2)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ (((log‘(𝑥 / 𝑛))↑2) / 2))
346	339, 341, 344, 345	syl21anc 851	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (((log‘(𝑥 / 𝑛))↑2) / 2))
347	340, 346	absidd 15570	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) = (((log‘(𝑥 / 𝑛))↑2) / 2))
348	347	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) = (((log‘(𝑥 / 𝑛))↑2) / 2))
349	8	rpred 13145	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ)
350		ltle 11379	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ e ∈ ℝ) → ((𝑥 / 𝑛) < e → (𝑥 / 𝑛) ≤ e))
351	349, 199, 350	sylancl 598	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) < e → (𝑥 / 𝑛) ≤ e))
352	351	imp 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) ≤ e)
353	8	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) ∈ ℝ+)
354		logleb 26913	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 / 𝑛) ∈ ℝ+ ∧ e ∈ ℝ+) → ((𝑥 / 𝑛) ≤ e ↔ (log‘(𝑥 / 𝑛)) ≤ (log‘e)))
355	353, 27, 354	sylancl 598	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((𝑥 / 𝑛) ≤ e ↔ (log‘(𝑥 / 𝑛)) ≤ (log‘e)))
356	352, 355	mpbid 235	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (log‘(𝑥 / 𝑛)) ≤ (log‘e))
357		loge 26896	. . . . . . . . . . . . . . . . . . 19 ⊢ (log‘e) = 1
358	356, 357	breqtrdi 5146	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (log‘(𝑥 / 𝑛)) ≤ 1)
359		0le1 11820	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ≤ 1
360	359	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ 1)
361	9, 260, 267, 360	le2sqd 14381	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) ≤ 1 ↔ ((log‘(𝑥 / 𝑛))↑2) ≤ (1↑2)))
362	361	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((log‘(𝑥 / 𝑛)) ≤ 1 ↔ ((log‘(𝑥 / 𝑛))↑2) ≤ (1↑2)))
363	358, 362	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((log‘(𝑥 / 𝑛))↑2) ≤ (1↑2))
364		sq1 14318	. . . . . . . . . . . . . . . . 17 ⊢ (1↑2) = 1
365	363, 364	breqtrdi 5146	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((log‘(𝑥 / 𝑛))↑2) ≤ 1)
366	339	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℝ)
367		1red 11290	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 1 ∈ ℝ)
368	343	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (2 ∈ ℝ ∧ 0 < 2))
369		lediv1 12163	. . . . . . . . . . . . . . . . 17 ⊢ ((((log‘(𝑥 / 𝑛))↑2) ∈ ℝ ∧ 1 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((log‘(𝑥 / 𝑛))↑2) ≤ 1 ↔ (((log‘(𝑥 / 𝑛))↑2) / 2) ≤ (1 / 2)))
370	366, 367, 368, 369	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (((log‘(𝑥 / 𝑛))↑2) ≤ 1 ↔ (((log‘(𝑥 / 𝑛))↑2) / 2) ≤ (1 / 2)))
371	365, 370	mpbid 235	. . . . . . . . . . . . . . 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 15586	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘𝐿) ∈ ℝ)
374	66, 373	readdcld 11319	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)) ∈ ℝ)
375	374	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)) ∈ ℝ)
376	67	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ · (log‘(𝑥 / 𝑛))) ∈ ℂ)
377	20	ad3antrrr 743	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 𝐿 ∈ ℂ)
378	376, 377	abs2dif2d 15608	. . . . . . . . . . . . . . . 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 11874	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (γ · (log‘(𝑥 / 𝑛))))
382	66, 381	absidd 15570	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(γ · (log‘(𝑥 / 𝑛)))) = (γ · (log‘(𝑥 / 𝑛))))
383	382	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(γ · (log‘(𝑥 / 𝑛)))) = (γ · (log‘(𝑥 / 𝑛))))
384	383	oveq1d 7427	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘(γ · (log‘(𝑥 / 𝑛)))) + (abs‘𝐿)) = ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)))
385	378, 384	breqtrd 5131	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ≤ ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)))
386	66	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ · (log‘(𝑥 / 𝑛))) ∈ ℝ)
387	17	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → γ ∈ ℝ)
388	377	abscld 15586	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘𝐿) ∈ ℝ)
389	9	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
390	387, 218	jctir 530	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ ∈ ℝ ∧ 0 < γ))
391		lemul2 12151	. . . . . . . . . . . . . . . . . . 19 ⊢ (((log‘(𝑥 / 𝑛)) ∈ ℝ ∧ 1 ∈ ℝ ∧ (γ ∈ ℝ ∧ 0 < γ)) → ((log‘(𝑥 / 𝑛)) ≤ 1 ↔ (γ · (log‘(𝑥 / 𝑛))) ≤ (γ · 1)))
392	389, 367, 390, 391	syl3anc 1398	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((log‘(𝑥 / 𝑛)) ≤ 1 ↔ (γ · (log‘(𝑥 / 𝑛))) ≤ (γ · 1)))
393	358, 392	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ · (log‘(𝑥 / 𝑛))) ≤ (γ · 1))
394	17	recni 11304	. . . . . . . . . . . . . . . . . 18 ⊢ γ ∈ ℂ
395	394	mulridi 11294	. . . . . . . . . . . . . . . . 17 ⊢ (γ · 1) = γ
396	393, 395	breqtrdi 5146	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ · (log‘(𝑥 / 𝑛))) ≤ γ)
397	386, 387, 388, 396	leadd1dd 11911	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)) ≤ (γ + (abs‘𝐿)))
398	334, 375, 338, 385, 397	letrd 11448	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ≤ (γ + (abs‘𝐿)))
399	332, 334, 337, 338, 372, 398	le2addd 11916	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) + (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ≤ ((1 / 2) + (γ + (abs‘𝐿))))
400	330, 335, 327, 336, 399	letrd 11448	. . . . . . . . . . . 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 605	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
403	85, 402	fsumrecl 15880	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
404	403	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
405	86, 90	sylan2 605	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
406	86, 129	sylan2 605	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℂ)
407	406	mullidd 11308	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (1 · 𝑚) = 𝑚)
408		fznnfl 13982	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 / 𝑛) ∈ ℝ → (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) ↔ (𝑚 ∈ ℕ ∧ 𝑚 ≤ (𝑥 / 𝑛))))
409	349, 408	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) ↔ (𝑚 ∈ ℕ ∧ 𝑚 ≤ (𝑥 / 𝑛))))
410	409	simplbda 505	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ≤ (𝑥 / 𝑛))
411	407, 410	eqbrtrd 5127	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (1 · 𝑚) ≤ (𝑥 / 𝑛))
412		1red 11290	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 1 ∈ ℝ)
413	349	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (𝑥 / 𝑛) ∈ ℝ)
414	116	rpregt0d 13151	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (𝑚 ∈ ℝ ∧ 0 < 𝑚))
415	86, 414	sylan2 605	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (𝑚 ∈ ℝ ∧ 0 < 𝑚))
416		lemuldiv 12178	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℝ ∧ (𝑥 / 𝑛) ∈ ℝ ∧ (𝑚 ∈ ℝ ∧ 0 < 𝑚)) → ((1 · 𝑚) ≤ (𝑥 / 𝑛) ↔ 1 ≤ ((𝑥 / 𝑛) / 𝑚)))
417	412, 413, 415, 416	syl3anc 1398	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((1 · 𝑚) ≤ (𝑥 / 𝑛) ↔ 1 ≤ ((𝑥 / 𝑛) / 𝑚)))
418	411, 417	mpbid 235	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 1 ≤ ((𝑥 / 𝑛) / 𝑚))
419	86, 89	sylan2 605	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
420		logleb 26913	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ+ ∧ ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+) → (1 ≤ ((𝑥 / 𝑛) / 𝑚) ↔ (log‘1) ≤ (log‘((𝑥 / 𝑛) / 𝑚))))
421	211, 419, 420	sylancr 599	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (1 ≤ ((𝑥 / 𝑛) / 𝑚) ↔ (log‘1) ≤ (log‘((𝑥 / 𝑛) / 𝑚))))
422	418, 421	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (log‘1) ≤ (log‘((𝑥 / 𝑛) / 𝑚)))
423	224, 422	eqbrtrrid 5141	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 0 ≤ (log‘((𝑥 / 𝑛) / 𝑚)))
424		divge0 12167	. . . . . . . . . . . . . . . 16 ⊢ ((((log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ ∧ 0 ≤ (log‘((𝑥 / 𝑛) / 𝑚))) ∧ (𝑚 ∈ ℝ ∧ 0 < 𝑚)) → 0 ≤ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))
425	405, 423, 415, 424	syl21anc 851	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 0 ≤ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))
426	85, 402, 425	fsumge0 15942	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))
427	426	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 0 ≤ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))
428	404, 427	absidd 15570	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))
429		fzfid 14096	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
430	349	flcld 13918	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℤ)
431	430	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (⌊‘(𝑥 / 𝑛)) ∈ ℤ)
432		2z 12709	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℤ
433	432	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 2 ∈ ℤ)
434	349	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) ∈ ℝ)
435	199	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → e ∈ ℝ)
436		3re 12404	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 3 ∈ ℝ
437	436	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 3 ∈ ℝ)
438		simpr 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) < e)
439	203	simpri 491	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ e < 3
440	439	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → e < 3)
441	434, 435, 437, 438, 440	lttrd 11452	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) < 3)
442		3z 12710	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 3 ∈ ℤ
443		fllt 13926	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ 3 ∈ ℤ) → ((𝑥 / 𝑛) < 3 ↔ (⌊‘(𝑥 / 𝑛)) < 3))
444	434, 442, 443	sylancl 598	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((𝑥 / 𝑛) < 3 ↔ (⌊‘(𝑥 / 𝑛)) < 3))
445	441, 444	mpbid 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (⌊‘(𝑥 / 𝑛)) < 3)
446		df-3 12387	. . . . . . . . . . . . . . . . . . . 20 ⊢ 3 = (2 + 1)
447	445, 446	breqtrdi 5146	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (⌊‘(𝑥 / 𝑛)) < (2 + 1))
448		zleltp1 12728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((⌊‘(𝑥 / 𝑛)) ∈ ℤ ∧ 2 ∈ ℤ) → ((⌊‘(𝑥 / 𝑛)) ≤ 2 ↔ (⌊‘(𝑥 / 𝑛)) < (2 + 1)))
449	431, 432, 448	sylancl 598	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((⌊‘(𝑥 / 𝑛)) ≤ 2 ↔ (⌊‘(𝑥 / 𝑛)) < (2 + 1)))
450	447, 449	mpbird 260	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (⌊‘(𝑥 / 𝑛)) ≤ 2)
451		eluz2 12952	. . . . . . . . . . . . . . . . . 18 ⊢ (2 ∈ (ℤ≥‘(⌊‘(𝑥 / 𝑛))) ↔ ((⌊‘(𝑥 / 𝑛)) ∈ ℤ ∧ 2 ∈ ℤ ∧ (⌊‘(𝑥 / 𝑛)) ≤ 2))
452	431, 433, 450, 451	syl3anbrc 1362	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 2 ∈ (ℤ≥‘(⌊‘(𝑥 / 𝑛))))
453		fzss2 13678	. . . . . . . . . . . . . . . . 17 ⊢ (2 ∈ (ℤ≥‘(⌊‘(𝑥 / 𝑛))) → (1...(⌊‘(𝑥 / 𝑛))) ⊆ (1...2))
454	452, 453	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (1...(⌊‘(𝑥 / 𝑛))) ⊆ (1...2))
455	454	sselda 3931	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ (1...2))
456	34	ad5ant15 771	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
457	455, 456	syldan 603	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
458	429, 457	fsumrecl 15880	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
459	92	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ ℕ) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
460	86, 459	sylan2 605	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
461	352	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (𝑥 / 𝑛) ≤ e)
462	434	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (𝑥 / 𝑛) ∈ ℝ)
463	199	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → e ∈ ℝ)
464	30	rpregt0d 13151	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (𝑚 ∈ ℝ ∧ 0 < 𝑚))
465	464	ad5ant15 771	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (𝑚 ∈ ℝ ∧ 0 < 𝑚))
466		lediv1 12163	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ e ∈ ℝ ∧ (𝑚 ∈ ℝ ∧ 0 < 𝑚)) → ((𝑥 / 𝑛) ≤ e ↔ ((𝑥 / 𝑛) / 𝑚) ≤ (e / 𝑚)))
467	462, 463, 465, 466	syl3anc 1398	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((𝑥 / 𝑛) ≤ e ↔ ((𝑥 / 𝑛) / 𝑚) ≤ (e / 𝑚)))
468	461, 467	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((𝑥 / 𝑛) / 𝑚) ≤ (e / 𝑚))
469	89	adantlr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ ℕ) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
470	28, 469	sylan2 605	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
471	32	ad5ant15 771	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (e / 𝑚) ∈ ℝ+)
472	470, 471	logled 26937	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (((𝑥 / 𝑛) / 𝑚) ≤ (e / 𝑚) ↔ (log‘((𝑥 / 𝑛) / 𝑚)) ≤ (log‘(e / 𝑚))))
473	468, 472	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (log‘((𝑥 / 𝑛) / 𝑚)) ≤ (log‘(e / 𝑚)))
474	90	adantlr 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ ℕ) → (log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
475	28, 474	sylan2 605	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
476	33	ad5ant15 771	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (log‘(e / 𝑚)) ∈ ℝ)
477		lediv1 12163	. . . . . . . . . . . . . . . . 17 ⊢ (((log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ ∧ (log‘(e / 𝑚)) ∈ ℝ ∧ (𝑚 ∈ ℝ ∧ 0 < 𝑚)) → ((log‘((𝑥 / 𝑛) / 𝑚)) ≤ (log‘(e / 𝑚)) ↔ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ ((log‘(e / 𝑚)) / 𝑚)))
478	475, 476, 465, 477	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((log‘((𝑥 / 𝑛) / 𝑚)) ≤ (log‘(e / 𝑚)) ↔ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ ((log‘(e / 𝑚)) / 𝑚)))
479	473, 478	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ ((log‘(e / 𝑚)) / 𝑚))
480	455, 479	syldan 603	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ ((log‘(e / 𝑚)) / 𝑚))
481	429, 460, 457, 480	fsumle 15946	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘(e / 𝑚)) / 𝑚))
482		fzfid 14096	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (1...2) ∈ Fin)
483	243	ad5ant15 771	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → 0 ≤ ((log‘(e / 𝑚)) / 𝑚))
484	482, 456, 483, 454	fsumless 15943	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘(e / 𝑚)) / 𝑚) ≤ Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚))
485	404, 458, 328, 481, 484	letrd 11448	. . . . . . . . . . . 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 11916	. . . . . . . . . 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 11448	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ 𝑅)
490	317, 318, 319, 320, 489	letrd 11448	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ 𝑅)
491	4, 208, 248, 249, 251, 272, 316, 490	fsumharmonic 27321	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · ((log‘e) + 1))))
492		2cnd 12402	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 ∈ ℂ)
493	3, 492, 303	fsummulc2 15930	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((log‘(𝑥 / 𝑛)) / 𝑥)))
494		df-2 12386	. . . . . . . . . 10 ⊢ 2 = (1 + 1)
495	357	oveq1i 7422	. . . . . . . . . 10 ⊢ ((log‘e) + 1) = (1 + 1)
496	494, 495	eqtr4i 2787	. . . . . . . . 9 ⊢ 2 = ((log‘e) + 1)
497	496	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 = ((log‘e) + 1))
498	497	oveq2d 7428	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑅 · 2) = (𝑅 · ((log‘e) + 1)))
499	493, 498	oveq12d 7430	. . . . . 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 730	. . . 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 15562	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ≤ (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))))
504	503	adantrr 730	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ≤ (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))))
505	79, 80, 83, 502, 504	letrd 11448	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ≤ (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))))
506	1, 53, 54, 77, 505	o1le 15800	1 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ∈ 𝑂(1))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ≠ wne 2956  {crab 3413   ⊆ wss 3899   class class class wbr 5103   ↦ cmpt 5186  ‘cfv 6531  (class class class)co 7412  ℂcc 11179  ℝcr 11180  0cc0 11181  1c1 11182   + caddc 11184   · cmul 11186   < clt 11324   ≤ cle 11325   − cmin 11522   / cdiv 11954  ℕcn 12316  2c2 12378  3c3 12379  ℤcz 12674  ℤ_≥cuz 12946  ℝ⁺crp 13101  ...cfz 13620  ⌊cfl 13910  ↑cexp 14184  abscabs 15381   ⇝_𝑟 crli 15632  𝑂(1)co1 15633  Σcsu 15833  eceu 16208   ∥ cdvds 16402  logclog 26864  γcem 27301  μcmu 27404

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740  ax-inf2 9626  ax-cnex 11237  ax-resscn 11238  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-addrcl 11242  ax-mulcl 11243  ax-mulrcl 11244  ax-mulcom 11245  ax-addass 11246  ax-mulass 11247  ax-distr 11248  ax-i2m1 11249  ax-1ne0 11250  ax-1rid 11251  ax-rnegex 11252  ax-rrecex 11253  ax-cnre 11254  ax-pre-lttri 11255  ax-pre-lttrn 11256  ax-pre-ltadd 11257  ax-pre-mulgt0 11258  ax-pre-sup 11259  ax-addf 11260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-disj 5071  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6297  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-isom 6540  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-of 7682  df-om 7867  df-1st 7990  df-2nd 7991  df-supp 8162  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-1o 8460  df-2o 8461  df-oadd 8464  df-er 8701  df-map 8833  df-pm 8834  df-ixp 8910  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-fsupp 9338  df-fi 9387  df-sup 9418  df-inf 9419  df-oi 9488  df-dju 9963  df-card 10001  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11524  df-neg 11525  df-div 11955  df-nn 12317  df-2 12386  df-3 12387  df-4 12388  df-5 12389  df-6 12390  df-7 12391  df-8 12392  df-9 12393  df-n0 12588  df-xnn0 12661  df-z 12675  df-dec 12796  df-uz 12947  df-q 13057  df-rp 13102  df-xneg 13222  df-xadd 13223  df-xmul 13224  df-ioo 13461  df-ioc 13462  df-ico 13463  df-icc 13464  df-fz 13621  df-fzo 13769  df-fl 13912  df-mod 13990  df-seq 14125  df-exp 14185  df-fac 14398  df-bc 14427  df-hash 14455  df-shft 15200  df-cj 15246  df-re 15247  df-im 15248  df-sqrt 15382  df-abs 15383  df-limsup 15618  df-clim 15635  df-rlim 15636  df-o1 15637  df-lo1 15638  df-sum 15834  df-ef 16213  df-e 16214  df-sin 16215  df-cos 16216  df-tan 16217  df-pi 16218  df-dvds 16403  df-gcd 16645  df-prm 16827  df-pc 16995  df-struct 17305  df-sets 17322  df-slot 17340  df-ndx 17352  df-base 17368  df-ress 17389  df-plusg 17421  df-mulr 17422  df-starv 17423  df-sca 17424  df-vsca 17425  df-ip 17426  df-tset 17427  df-ple 17428  df-ds 17430  df-unif 17431  df-hom 17432  df-cco 17433  df-rest 17573  df-topn 17574  df-0g 17592  df-gsum 17593  df-topgen 17594  df-pt 17595  df-prds 17598  df-xrs 17654  df-qtop 17659  df-imas 17660  df-xps 17662  df-mre 17736  df-mrc 17737  df-acs 17739  df-mgm 18796  df-sgrp 18888  df-mnd 18904  df-submnd 18959  df-mulg 19258  df-cntz 19511  df-cmn 19976  df-psmet 21650  df-xmet 21651  df-met 21652  df-bl 21653  df-mopn 21654  df-fbas 21655  df-fg 21656  df-cnfld 21659  df-top 23192  df-topon 23209  df-topsp 23231  df-bases 23244  df-cld 23317  df-ntr 23318  df-cls 23319  df-nei 23396  df-lp 23434  df-perf 23435  df-cn 23525  df-cnp 23526  df-haus 23613  df-cmp 23685  df-tx 23861  df-hmeo 24054  df-fil 24145  df-fm 24237  df-flim 24238  df-flf 24239  df-xms 24619  df-ms 24620  df-tms 24621  df-cncf 25179  df-limc 26166  df-dv 26167  df-ulm 26686  df-log 26866  df-cxp 26867  df-atan 27177  df-em 27302  df-mu 27410

This theorem is used by:  mulog2sumlem3  27845