Theorem mulog2sumlem2 27384

Description: Lemma for mulog2sum 27386. (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 11212	. 2 ⊢ (𝜑 → 1 ∈ ℝ)
2		2re 12283	. . . 4 ⊢ 2 ∈ ℝ
3		fzfid 13935	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin)
4		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
5		elfznn 13527	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
6	5	nnrpd 13011	. . . . . . . 8 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℝ+)
7		rpdivcl 12996	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+) → (𝑥 / 𝑛) ∈ ℝ+)
8	4, 6, 7	syl2an 595	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ+)
9	8	relogcld 26473	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
10		simplr 766	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ+)
11	9, 10	rerpdivcld 13044	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℝ)
12	3, 11	fsumrecl 15677	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℝ)
13		remulcl 11191	. . . 4 ⊢ ((2 ∈ ℝ ∧ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℝ) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ ℝ)
14	2, 12, 13	sylancr 586	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ ℝ)
15		mulog2sumlem2.r	. . . . . 6 ⊢ 𝑅 = (((1 / 2) + (γ + (abs‘𝐿))) + Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚))
16		halfre 12423	. . . . . . . 8 ⊢ (1 / 2) ∈ ℝ
17		emre 26854	. . . . . . . . 9 ⊢ γ ∈ ℝ
18		mulog2sumlem.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐿)
19		rlimcl 15444	. . . . . . . . . . 11 ⊢ (𝐹 ⇝𝑟 𝐿 → 𝐿 ∈ ℂ)
20	18, 19	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ ℂ)
21	20	abscld 15380	. . . . . . . . 9 ⊢ (𝜑 → (abs‘𝐿) ∈ ℝ)
22		readdcl 11189	. . . . . . . . 9 ⊢ ((γ ∈ ℝ ∧ (abs‘𝐿) ∈ ℝ) → (γ + (abs‘𝐿)) ∈ ℝ)
23	17, 21, 22	sylancr 586	. . . . . . . 8 ⊢ (𝜑 → (γ + (abs‘𝐿)) ∈ ℝ)
24		readdcl 11189	. . . . . . . 8 ⊢ (((1 / 2) ∈ ℝ ∧ (γ + (abs‘𝐿)) ∈ ℝ) → ((1 / 2) + (γ + (abs‘𝐿))) ∈ ℝ)
25	16, 23, 24	sylancr 586	. . . . . . 7 ⊢ (𝜑 → ((1 / 2) + (γ + (abs‘𝐿))) ∈ ℝ)
26		fzfid 13935	. . . . . . . 8 ⊢ (𝜑 → (1...2) ∈ Fin)
27		epr 16148	. . . . . . . . . . 11 ⊢ e ∈ ℝ+
28		elfznn 13527	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (1...2) → 𝑚 ∈ ℕ)
29	28	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ∈ ℕ)
30	29	nnrpd 13011	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ∈ ℝ+)
31		rpdivcl 12996	. . . . . . . . . . 11 ⊢ ((e ∈ ℝ+ ∧ 𝑚 ∈ ℝ+) → (e / 𝑚) ∈ ℝ+)
32	27, 30, 31	sylancr 586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (e / 𝑚) ∈ ℝ+)
33	32	relogcld 26473	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (log‘(e / 𝑚)) ∈ ℝ)
34	33, 29	nndivred 12263	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → ((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
35	26, 34	fsumrecl 15677	. . . . . . 7 ⊢ (𝜑 → Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
36	25, 35	readdcld 11240	. . . . . 6 ⊢ (𝜑 → (((1 / 2) + (γ + (abs‘𝐿))) + Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚)) ∈ ℝ)
37	15, 36	eqeltrid 2829	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ ℝ)
38		remulcl 11191	. . . . 5 ⊢ ((𝑅 ∈ ℝ ∧ 2 ∈ ℝ) → (𝑅 · 2) ∈ ℝ)
39	37, 2, 38	sylancl 585	. . . 4 ⊢ (𝜑 → (𝑅 · 2) ∈ ℝ)
40	39	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑅 · 2) ∈ ℝ)
41	2	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 ∈ ℝ)
42		rpssre 12978	. . . . 5 ⊢ ℝ+ ⊆ ℝ
43		2cnd 12287	. . . . 5 ⊢ (𝜑 → 2 ∈ ℂ)
44		o1const 15561	. . . . 5 ⊢ ((ℝ+ ⊆ ℝ ∧ 2 ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ 2) ∈ 𝑂(1))
45	42, 43, 44	sylancr 586	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ 2) ∈ 𝑂(1))
46		logfacrlim2 27075	. . . . 5 ⊢ (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ⇝𝑟 1
47		rlimo1 15558	. . . . 5 ⊢ ((𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ⇝𝑟 1 → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ 𝑂(1))
48	46, 47	mp1i 13	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ 𝑂(1))
49	41, 12, 45, 48	o1mul2 15566	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥))) ∈ 𝑂(1))
50	39	recnd 11239	. . . 4 ⊢ (𝜑 → (𝑅 · 2) ∈ ℂ)
51		o1const 15561	. . . 4 ⊢ ((ℝ+ ⊆ ℝ ∧ (𝑅 · 2) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ (𝑅 · 2)) ∈ 𝑂(1))
52	42, 50, 51	sylancr 586	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (𝑅 · 2)) ∈ 𝑂(1))
53	14, 40, 49, 52	o1add2 15565	. 2 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))) ∈ 𝑂(1))
54	14, 40	readdcld 11240	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ∈ ℝ)
55	5	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
56		mucl 26989	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (μ‘𝑛) ∈ ℤ)
57	55, 56	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℤ)
58	57	zred 12663	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℝ)
59	58, 55	nndivred 12263	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℝ)
60	59	recnd 11239	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℂ)
61		mulog2sumlem2.t	. . . . . 6 ⊢ 𝑇 = ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿))
62	9	recnd 11239	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℂ)
63	62	sqcld 14106	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℂ)
64	63	halfcld 12454	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) / 2) ∈ ℂ)
65		remulcl 11191	. . . . . . . . . 10 ⊢ ((γ ∈ ℝ ∧ (log‘(𝑥 / 𝑛)) ∈ ℝ) → (γ · (log‘(𝑥 / 𝑛))) ∈ ℝ)
66	17, 9, 65	sylancr 586	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (γ · (log‘(𝑥 / 𝑛))) ∈ ℝ)
67	66	recnd 11239	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (γ · (log‘(𝑥 / 𝑛))) ∈ ℂ)
68	20	ad2antrr 723	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝐿 ∈ ℂ)
69	67, 68	subcld 11568	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((γ · (log‘(𝑥 / 𝑛))) − 𝐿) ∈ ℂ)
70	64, 69	addcld 11230	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ∈ ℂ)
71	61, 70	eqeltrid 2829	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑇 ∈ ℂ)
72	60, 71	mulcld 11231	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · 𝑇) ∈ ℂ)
73	3, 72	fsumcl 15676	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) ∈ ℂ)
74		relogcl 26426	. . . . 5 ⊢ (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
75	74	adantl 481	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
76	75	recnd 11239	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℂ)
77	73, 76	subcld 11568	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥)) ∈ ℂ)
78	77	abscld 15380	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ∈ ℝ)
79	78	adantrr 714	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ∈ ℝ)
80	54	adantrr 714	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ∈ ℝ)
81	54	recnd 11239	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ∈ ℂ)
82	81	abscld 15380	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))) ∈ ℝ)
83	82	adantrr 714	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))) ∈ ℝ)
84	57	zcnd 12664	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℂ)
85		fzfid 13935	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
86		elfznn 13527	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) → 𝑚 ∈ ℕ)
87		nnrp 12982	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℝ+)
88		rpdivcl 12996	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 / 𝑛) ∈ ℝ+ ∧ 𝑚 ∈ ℝ+) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
89	8, 87, 88	syl2an 595	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
90	89	relogcld 26473	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
91		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℕ)
92	90, 91	nndivred 12263	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
93	92	recnd 11239	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ)
94	86, 93	sylan2 592	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ)
95	85, 94	fsumcl 15676	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ)
96	71, 95	subcld 11568	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ∈ ℂ)
97	55	nncnd 12225	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
98	55	nnne0d 12259	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0)
99	84, 96, 97, 98	div23d 12024	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = (((μ‘𝑛) / 𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
100	60, 71, 95	subdid 11667	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = ((((μ‘𝑛) / 𝑛) · 𝑇) − (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
101	99, 100	eqtrd 2764	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = ((((μ‘𝑛) / 𝑛) · 𝑇) − (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
102	101	sumeq2dv 15646	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))((((μ‘𝑛) / 𝑛) · 𝑇) − (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
103	60, 95	mulcld 11231	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ∈ ℂ)
104	3, 72, 103	fsumsub 15731	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((μ‘𝑛) / 𝑛) · 𝑇) − (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
105	102, 104	eqtrd 2764	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
106	105	adantrr 714	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
107	85, 60, 94	fsummulc2 15727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))
108	84	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (μ‘𝑛) ∈ ℂ)
109	97, 98	jca 511	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
110	109	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
111		div23 11888	. . . . . . . . . . . . . . . . 17 ⊢ (((μ‘𝑛) ∈ ℂ ∧ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((μ‘𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) / 𝑛) = (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))
112		divass 11887	. . . . . . . . . . . . . . . . 17 ⊢ (((μ‘𝑛) ∈ ℂ ∧ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((μ‘𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) / 𝑛) = ((μ‘𝑛) · (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛)))
113	111, 112	eqtr3d 2766	. . . . . . . . . . . . . . . 16 ⊢ (((μ‘𝑛) ∈ ℂ ∧ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = ((μ‘𝑛) · (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛)))
114	108, 93, 110, 113	syl3anc 1368	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = ((μ‘𝑛) · (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛)))
115	90	recnd 11239	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℂ)
116	91	nnrpd 13011	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ+)
117		rpcnne0 12989	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ ℝ+ → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0))
118	116, 117	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0))
119		divdiv1 11922	. . . . . . . . . . . . . . . . . 18 ⊢ (((log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℂ ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0) ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛) = ((log‘((𝑥 / 𝑛) / 𝑚)) / (𝑚 · 𝑛)))
120	115, 118, 110, 119	syl3anc 1368	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛) = ((log‘((𝑥 / 𝑛) / 𝑚)) / (𝑚 · 𝑛)))
121		rpre 12979	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ)
122	121	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
123	122	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
124	123	recnd 11239	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℂ)
125	124	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → 𝑥 ∈ ℂ)
126		divdiv1 11922	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0) ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) → ((𝑥 / 𝑛) / 𝑚) = (𝑥 / (𝑛 · 𝑚)))
127	125, 110, 118, 126	syl3anc 1368	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((𝑥 / 𝑛) / 𝑚) = (𝑥 / (𝑛 · 𝑚)))
128	127	fveq2d 6885	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (log‘((𝑥 / 𝑛) / 𝑚)) = (log‘(𝑥 / (𝑛 · 𝑚))))
129	91	nncnd 12225	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
130	97	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → 𝑛 ∈ ℂ)
131	129, 130	mulcomd 11232	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (𝑚 · 𝑛) = (𝑛 · 𝑚))
132	128, 131	oveq12d 7419	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((log‘((𝑥 / 𝑛) / 𝑚)) / (𝑚 · 𝑛)) = ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚)))
133	120, 132	eqtrd 2764	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛) = ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚)))
134	133	oveq2d 7417	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((μ‘𝑛) · (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛)) = ((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
135	114, 134	eqtrd 2764	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = ((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
136	86, 135	sylan2 592	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = ((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
137	136	sumeq2dv 15646	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
138	107, 137	eqtrd 2764	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
139	138	sumeq2dv 15646	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
140		oveq2 7409	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑛 · 𝑚) → (𝑥 / 𝑘) = (𝑥 / (𝑛 · 𝑚)))
141	140	fveq2d 6885	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑛 · 𝑚) → (log‘(𝑥 / 𝑘)) = (log‘(𝑥 / (𝑛 · 𝑚))))
142		id 22	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑛 · 𝑚) → 𝑘 = (𝑛 · 𝑚))
143	141, 142	oveq12d 7419	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑛 · 𝑚) → ((log‘(𝑥 / 𝑘)) / 𝑘) = ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚)))
144	143	oveq2d 7417	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑛 · 𝑚) → ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) = ((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
145	4	rpred 13013	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
146		ssrab2 4069	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ ℕ
147		simprr 770	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})
148	146, 147	sselid 3972	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ ℕ)
149	148, 56	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (μ‘𝑛) ∈ ℤ)
150	149	zred 12663	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (μ‘𝑛) ∈ ℝ)
151		elfznn 13527	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (1...(⌊‘𝑥)) → 𝑘 ∈ ℕ)
152	151	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → 𝑘 ∈ ℕ)
153	152	nnrpd 13011	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → 𝑘 ∈ ℝ+)
154		rpdivcl 12996	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑘 ∈ ℝ+) → (𝑥 / 𝑘) ∈ ℝ+)
155	4, 153, 154	syl2an 595	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (𝑥 / 𝑘) ∈ ℝ+)
156	155	relogcld 26473	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (log‘(𝑥 / 𝑘)) ∈ ℝ)
157	151	ad2antrl 725	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑘 ∈ ℕ)
158	156, 157	nndivred 12263	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → ((log‘(𝑥 / 𝑘)) / 𝑘) ∈ ℝ)
159	150, 158	remulcld 11241	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) ∈ ℝ)
160	159	recnd 11239	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) ∈ ℂ)
161	144, 145, 160	dvdsflsumcom 27036	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
162	139, 161	eqtr4d 2767	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)))
163	162	adantrr 714	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)))
164		oveq2 7409	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → (𝑥 / 𝑘) = (𝑥 / 1))
165	164	fveq2d 6885	. . . . . . . . . 10 ⊢ (𝑘 = 1 → (log‘(𝑥 / 𝑘)) = (log‘(𝑥 / 1)))
166		id 22	. . . . . . . . . 10 ⊢ (𝑘 = 1 → 𝑘 = 1)
167	165, 166	oveq12d 7419	. . . . . . . . 9 ⊢ (𝑘 = 1 → ((log‘(𝑥 / 𝑘)) / 𝑘) = ((log‘(𝑥 / 1)) / 1))
168		fzfid 13935	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin)
169		fz1ssnn 13529	. . . . . . . . . 10 ⊢ (1...(⌊‘𝑥)) ⊆ ℕ
170	169	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ⊆ ℕ)
171	122	adantrr 714	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ)
172		simprr 770	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥)
173		flge1nn 13783	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ)
174	171, 172, 173	syl2anc 583	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (⌊‘𝑥) ∈ ℕ)
175		nnuz 12862	. . . . . . . . . . 11 ⊢ ℕ = (ℤ≥‘1)
176	174, 175	eleqtrdi 2835	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (⌊‘𝑥) ∈ (ℤ≥‘1))
177		eluzfz1 13505	. . . . . . . . . 10 ⊢ ((⌊‘𝑥) ∈ (ℤ≥‘1) → 1 ∈ (1...(⌊‘𝑥)))
178	176, 177	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ (1...(⌊‘𝑥)))
179	151	nnrpd 13011	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1...(⌊‘𝑥)) → 𝑘 ∈ ℝ+)
180	4, 179, 154	syl2an 595	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑘) ∈ ℝ+)
181	180	relogcld 26473	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑘)) ∈ ℝ)
182	169	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ⊆ ℕ)
183	182	sselda 3974	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → 𝑘 ∈ ℕ)
184	181, 183	nndivred 12263	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑘)) / 𝑘) ∈ ℝ)
185	184	recnd 11239	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑘)) / 𝑘) ∈ ℂ)
186	185	adantlrr 718	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑘)) / 𝑘) ∈ ℂ)
187	167, 168, 170, 178, 186	musumsum 27040	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) = ((log‘(𝑥 / 1)) / 1))
188	4	rpcnd 13015	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
189	188	div1d 11979	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 / 1) = 𝑥)
190	189	fveq2d 6885	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (log‘(𝑥 / 1)) = (log‘𝑥))
191	190	oveq1d 7416	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((log‘(𝑥 / 1)) / 1) = ((log‘𝑥) / 1))
192	76	div1d 11979	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((log‘𝑥) / 1) = (log‘𝑥))
193	191, 192	eqtrd 2764	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((log‘(𝑥 / 1)) / 1) = (log‘𝑥))
194	193	adantrr 714	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘(𝑥 / 1)) / 1) = (log‘𝑥))
195	163, 187, 194	3eqtrd 2768	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = (log‘𝑥))
196	195	oveq2d 7417	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥)))
197	106, 196	eqtrd 2764	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥)))
198	197	fveq2d 6885	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛)) = (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))))
199		ere 16029	. . . . . . . . 9 ⊢ e ∈ ℝ
200	199	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → e ∈ ℝ)
201		1re 11211	. . . . . . . . 9 ⊢ 1 ∈ ℝ
202		1lt2 12380	. . . . . . . . . 10 ⊢ 1 < 2
203		egt2lt3 16146	. . . . . . . . . . 11 ⊢ (2 < e ∧ e < 3)
204	203	simpli 483	. . . . . . . . . 10 ⊢ 2 < e
205	201, 2, 199	lttri 11337	. . . . . . . . . 10 ⊢ ((1 < 2 ∧ 2 < e) → 1 < e)
206	202, 204, 205	mp2an 689	. . . . . . . . 9 ⊢ 1 < e
207	201, 199, 206	ltleii 11334	. . . . . . . 8 ⊢ 1 ≤ e
208	200, 207	jctir 520	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (e ∈ ℝ ∧ 1 ≤ e))
209	37	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑅 ∈ ℝ)
210	16	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 / 2) ∈ ℝ)
211		1rp 12975	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ+
212		rphalfcl 12998	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℝ+ → (1 / 2) ∈ ℝ+)
213	211, 212	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (1 / 2) ∈ ℝ+
214		rpge0 12984	. . . . . . . . . . . . 13 ⊢ ((1 / 2) ∈ ℝ+ → 0 ≤ (1 / 2))
215	213, 214	mp1i 13	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ (1 / 2))
216	17	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → γ ∈ ℝ)
217		0re 11213	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ
218		emgt0 26855	. . . . . . . . . . . . . . 15 ⊢ 0 < γ
219	217, 17, 218	ltleii 11334	. . . . . . . . . . . . . 14 ⊢ 0 ≤ γ
220	219	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ γ)
221	20	absge0d 15388	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ (abs‘𝐿))
222	216, 21, 220, 221	addge0d 11787	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ (γ + (abs‘𝐿)))
223	210, 23, 215, 222	addge0d 11787	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ ((1 / 2) + (γ + (abs‘𝐿))))
224		log1 26436	. . . . . . . . . . . . . 14 ⊢ (log‘1) = 0
225	29	nncnd 12225	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ∈ ℂ)
226	225	mullidd 11229	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (1 · 𝑚) = 𝑚)
227	30	rpred 13013	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ∈ ℝ)
228	2	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 2 ∈ ℝ)
229	199	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → e ∈ ℝ)
230		elfzle2 13502	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 ∈ (1...2) → 𝑚 ≤ 2)
231	230	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ≤ 2)
232	2, 199, 204	ltleii 11334	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ≤ e
233	232	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 2 ≤ e)
234	227, 228, 229, 231, 233	letrd 11368	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ≤ e)
235	226, 234	eqbrtrd 5160	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (1 · 𝑚) ≤ e)
236		1red 11212	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 1 ∈ ℝ)
237	236, 229, 30	lemuldivd 13062	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → ((1 · 𝑚) ≤ e ↔ 1 ≤ (e / 𝑚)))
238	235, 237	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 1 ≤ (e / 𝑚))
239		logleb 26453	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℝ+ ∧ (e / 𝑚) ∈ ℝ+) → (1 ≤ (e / 𝑚) ↔ (log‘1) ≤ (log‘(e / 𝑚))))
240	211, 32, 239	sylancr 586	. . . . . . . . . . . . . . 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 5174	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 0 ≤ (log‘(e / 𝑚)))
243	33, 30, 242	divge0d 13053	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 0 ≤ ((log‘(e / 𝑚)) / 𝑚))
244	26, 34, 243	fsumge0 15738	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚))
245	25, 35, 223, 244	addge0d 11787	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ (((1 / 2) + (γ + (abs‘𝐿))) + Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚)))
246	245, 15	breqtrrdi 5180	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝑅)
247	246	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 0 ≤ 𝑅)
248	209, 247	jca 511	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅))
249	84, 96	mulcld 11231	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℂ)
250		remulcl 11191	. . . . . . . 8 ⊢ ((2 ∈ ℝ ∧ ((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℝ) → (2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ ℝ)
251	2, 11, 250	sylancr 586	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ ℝ)
252	2	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℝ)
253		0le2 12311	. . . . . . . . 9 ⊢ 0 ≤ 2
254	253	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ 2)
255	97	mullidd 11229	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) = 𝑛)
256		fznnfl 13824	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥)))
257	122, 256	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥)))
258	257	simplbda 499	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≤ 𝑥)
259	255, 258	eqbrtrd 5160	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) ≤ 𝑥)
260		1red 11212	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
261	55	nnrpd 13011	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+)
262	260, 123, 261	lemuldivd 13062	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛)))
263	259, 262	mpbid 231	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ (𝑥 / 𝑛))
264		logleb 26453	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℝ+ ∧ (𝑥 / 𝑛) ∈ ℝ+) → (1 ≤ (𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛))))
265	211, 8, 264	sylancr 586	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 ≤ (𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛))))
266	263, 265	mpbid 231	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘1) ≤ (log‘(𝑥 / 𝑛)))
267	224, 266	eqbrtrrid 5174	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (log‘(𝑥 / 𝑛)))
268		rpregt0 12985	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
269	268	ad2antlr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
270		divge0 12080	. . . . . . . . 9 ⊢ ((((log‘(𝑥 / 𝑛)) ∈ ℝ ∧ 0 ≤ (log‘(𝑥 / 𝑛))) ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → 0 ≤ ((log‘(𝑥 / 𝑛)) / 𝑥))
271	9, 267, 269, 270	syl21anc 835	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((log‘(𝑥 / 𝑛)) / 𝑥))
272	252, 11, 254, 271	mulge0d 11788	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (2 · ((log‘(𝑥 / 𝑛)) / 𝑥)))
273	249	abscld 15380	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ∈ ℝ)
274	273	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ∈ ℝ)
275	96	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ∈ ℂ)
276	275	abscld 15380	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℝ)
277	261	rpred 13013	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ)
278	251, 277	remulcld 11241	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) ∈ ℝ)
279	278	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) ∈ ℝ)
280	84, 96	absmuld 15398	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) = ((abs‘(μ‘𝑛)) · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))))
281	84	abscld 15380	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ∈ ℝ)
282	96	abscld 15380	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℝ)
283	96	absge0d 15388	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
284		mule1 26996	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (abs‘(μ‘𝑛)) ≤ 1)
285	55, 284	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ≤ 1)
286	281, 260, 282, 283, 285	lemul1ad 12150	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(μ‘𝑛)) · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (1 · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))))
287	282	recnd 11239	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℂ)
288	287	mullidd 11229	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) = (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
289	286, 288	breqtrd 5164	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(μ‘𝑛)) · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
290	280, 289	eqbrtrd 5160	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
291	290	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
292		logdivsum.1	. . . . . . . . . 10 ⊢ 𝐹 = (𝑦 ∈ ℝ+ ↦ (Σ𝑖 ∈ (1...(⌊‘𝑦))((log‘𝑖) / 𝑖) − (((log‘𝑦)↑2) / 2)))
293	18	ad3antrrr 727	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → 𝐹 ⇝𝑟 𝐿)
294	8	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (𝑥 / 𝑛) ∈ ℝ+)
295		simpr 484	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → e ≤ (𝑥 / 𝑛))
296	292, 293, 294, 295	mulog2sumlem1 27383	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)))) ≤ (2 · ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))))
297	71, 95	abssubd 15397	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − 𝑇)))
298	297	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − 𝑇)))
299	61	oveq2i 7412	. . . . . . . . . . 11 ⊢ (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − 𝑇) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)))
300	299	fveq2i 6884	. . . . . . . . . 10 ⊢ (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − 𝑇)) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿))))
301	298, 300	eqtrdi 2780	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)))))
302		2cnd 12287	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℂ)
303	11	recnd 11239	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℂ)
304	302, 303, 97	mulassd 11234	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) = (2 · (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛)))
305		rpcnne0 12989	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ+ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
306	305	ad2antlr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
307		divdiv2 11923	. . . . . . . . . . . . . 14 ⊢ (((log‘(𝑥 / 𝑛)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛)) = (((log‘(𝑥 / 𝑛)) · 𝑛) / 𝑥))
308	62, 306, 109, 307	syl3anc 1368	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛)) = (((log‘(𝑥 / 𝑛)) · 𝑛) / 𝑥))
309		div23 11888	. . . . . . . . . . . . . 14 ⊢ (((log‘(𝑥 / 𝑛)) ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((log‘(𝑥 / 𝑛)) · 𝑛) / 𝑥) = (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛))
310	62, 97, 306, 309	syl3anc 1368	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛)) · 𝑛) / 𝑥) = (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛))
311	308, 310	eqtrd 2764	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛)) = (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛))
312	311	oveq2d 7417	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))) = (2 · (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛)))
313	304, 312	eqtr4d 2767	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) = (2 · ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))))
314	313	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) = (2 · ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))))
315	296, 301, 314	3brtr4d 5170	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛))
316	274, 276, 279, 291, 315	letrd 11368	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛))
317	273	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ∈ ℝ)
318	282	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℝ)
319	37	ad3antrrr 727	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 𝑅 ∈ ℝ)
320	290	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
321	71	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 𝑇 ∈ ℂ)
322	321	abscld 15380	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘𝑇) ∈ ℝ)
323	95	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ)
324	323	abscld 15380	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ∈ ℝ)
325	322, 324	readdcld 11240	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘𝑇) + (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℝ)
326	321, 323	abs2dif2d 15402	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ ((abs‘𝑇) + (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
327	25	ad3antrrr 727	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((1 / 2) + (γ + (abs‘𝐿))) ∈ ℝ)
328	35	ad3antrrr 727	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
329	61	fveq2i 6884	. . . . . . . . . . . 12 ⊢ (abs‘𝑇) = (abs‘((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)))
330	329, 322	eqeltrrid 2830	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ∈ ℝ)
331	64	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (((log‘(𝑥 / 𝑛))↑2) / 2) ∈ ℂ)
332	331	abscld 15380	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) ∈ ℝ)
333	69	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((γ · (log‘(𝑥 / 𝑛))) − 𝐿) ∈ ℂ)
334	333	abscld 15380	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ∈ ℝ)
335	332, 334	readdcld 11240	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) + (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ∈ ℝ)
336	331, 333	abstrid 15400	. . . . . . . . . . . . 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 727	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ + (abs‘𝐿)) ∈ ℝ)
339	9	resqcld 14087	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℝ)
340	339	rehalfcld 12456	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) / 2) ∈ ℝ)
341	9	sqge0d 14099	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((log‘(𝑥 / 𝑛))↑2))
342		2pos 12312	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 < 2
343	2, 342	pm3.2i 470	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 ∈ ℝ ∧ 0 < 2)
344	343	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 ∈ ℝ ∧ 0 < 2))
345		divge0 12080	. . . . . . . . . . . . . . . . . 18 ⊢ (((((log‘(𝑥 / 𝑛))↑2) ∈ ℝ ∧ 0 ≤ ((log‘(𝑥 / 𝑛))↑2)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ (((log‘(𝑥 / 𝑛))↑2) / 2))
346	339, 341, 344, 345	syl21anc 835	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (((log‘(𝑥 / 𝑛))↑2) / 2))
347	340, 346	absidd 15366	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) = (((log‘(𝑥 / 𝑛))↑2) / 2))
348	347	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) = (((log‘(𝑥 / 𝑛))↑2) / 2))
349	8	rpred 13013	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ)
350		ltle 11299	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ e ∈ ℝ) → ((𝑥 / 𝑛) < e → (𝑥 / 𝑛) ≤ e))
351	349, 199, 350	sylancl 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) < e → (𝑥 / 𝑛) ≤ e))
352	351	imp 406	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) ≤ e)
353	8	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) ∈ ℝ+)
354		logleb 26453	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥 / 𝑛) ∈ ℝ+ ∧ e ∈ ℝ+) → ((𝑥 / 𝑛) ≤ e ↔ (log‘(𝑥 / 𝑛)) ≤ (log‘e)))
355	353, 27, 354	sylancl 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((𝑥 / 𝑛) ≤ e ↔ (log‘(𝑥 / 𝑛)) ≤ (log‘e)))
356	352, 355	mpbid 231	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (log‘(𝑥 / 𝑛)) ≤ (log‘e))
357		loge 26437	. . . . . . . . . . . . . . . . . . 19 ⊢ (log‘e) = 1
358	356, 357	breqtrdi 5179	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (log‘(𝑥 / 𝑛)) ≤ 1)
359		0le1 11734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ≤ 1
360	359	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ 1)
361	9, 260, 267, 360	le2sqd 14217	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) ≤ 1 ↔ ((log‘(𝑥 / 𝑛))↑2) ≤ (1↑2)))
362	361	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((log‘(𝑥 / 𝑛)) ≤ 1 ↔ ((log‘(𝑥 / 𝑛))↑2) ≤ (1↑2)))
363	358, 362	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((log‘(𝑥 / 𝑛))↑2) ≤ (1↑2))
364		sq1 14156	. . . . . . . . . . . . . . . . 17 ⊢ (1↑2) = 1
365	363, 364	breqtrdi 5179	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((log‘(𝑥 / 𝑛))↑2) ≤ 1)
366	339	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℝ)
367		1red 11212	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 1 ∈ ℝ)
368	343	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (2 ∈ ℝ ∧ 0 < 2))
369		lediv1 12076	. . . . . . . . . . . . . . . . 17 ⊢ ((((log‘(𝑥 / 𝑛))↑2) ∈ ℝ ∧ 1 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((log‘(𝑥 / 𝑛))↑2) ≤ 1 ↔ (((log‘(𝑥 / 𝑛))↑2) / 2) ≤ (1 / 2)))
370	366, 367, 368, 369	syl3anc 1368	. . . . . . . . . . . . . . . 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 5160	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) ≤ (1 / 2))
373	68	abscld 15380	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘𝐿) ∈ ℝ)
374	66, 373	readdcld 11240	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)) ∈ ℝ)
375	374	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)) ∈ ℝ)
376	67	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ · (log‘(𝑥 / 𝑛))) ∈ ℂ)
377	20	ad3antrrr 727	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 𝐿 ∈ ℂ)
378	376, 377	abs2dif2d 15402	. . . . . . . . . . . . . . . 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 11788	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (γ · (log‘(𝑥 / 𝑛))))
382	66, 381	absidd 15366	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(γ · (log‘(𝑥 / 𝑛)))) = (γ · (log‘(𝑥 / 𝑛))))
383	382	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(γ · (log‘(𝑥 / 𝑛)))) = (γ · (log‘(𝑥 / 𝑛))))
384	383	oveq1d 7416	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘(γ · (log‘(𝑥 / 𝑛)))) + (abs‘𝐿)) = ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)))
385	378, 384	breqtrd 5164	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ≤ ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)))
386	66	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ · (log‘(𝑥 / 𝑛))) ∈ ℝ)
387	17	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → γ ∈ ℝ)
388	377	abscld 15380	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘𝐿) ∈ ℝ)
389	9	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
390	387, 218	jctir 520	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ ∈ ℝ ∧ 0 < γ))
391		lemul2 12064	. . . . . . . . . . . . . . . . . . 19 ⊢ (((log‘(𝑥 / 𝑛)) ∈ ℝ ∧ 1 ∈ ℝ ∧ (γ ∈ ℝ ∧ 0 < γ)) → ((log‘(𝑥 / 𝑛)) ≤ 1 ↔ (γ · (log‘(𝑥 / 𝑛))) ≤ (γ · 1)))
392	389, 367, 390, 391	syl3anc 1368	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((log‘(𝑥 / 𝑛)) ≤ 1 ↔ (γ · (log‘(𝑥 / 𝑛))) ≤ (γ · 1)))
393	358, 392	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ · (log‘(𝑥 / 𝑛))) ≤ (γ · 1))
394	17	recni 11225	. . . . . . . . . . . . . . . . . 18 ⊢ γ ∈ ℂ
395	394	mulridi 11215	. . . . . . . . . . . . . . . . 17 ⊢ (γ · 1) = γ
396	393, 395	breqtrdi 5179	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ · (log‘(𝑥 / 𝑛))) ≤ γ)
397	386, 387, 388, 396	leadd1dd 11825	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)) ≤ (γ + (abs‘𝐿)))
398	334, 375, 338, 385, 397	letrd 11368	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ≤ (γ + (abs‘𝐿)))
399	332, 334, 337, 338, 372, 398	le2addd 11830	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) + (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ≤ ((1 / 2) + (γ + (abs‘𝐿))))
400	330, 335, 327, 336, 399	letrd 11368	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ≤ ((1 / 2) + (γ + (abs‘𝐿))))
401	329, 400	eqbrtrid 5173	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘𝑇) ≤ ((1 / 2) + (γ + (abs‘𝐿))))
402	86, 92	sylan2 592	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
403	85, 402	fsumrecl 15677	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
404	403	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
405	86, 90	sylan2 592	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
406	86, 129	sylan2 592	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℂ)
407	406	mullidd 11229	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (1 · 𝑚) = 𝑚)
408		fznnfl 13824	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 / 𝑛) ∈ ℝ → (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) ↔ (𝑚 ∈ ℕ ∧ 𝑚 ≤ (𝑥 / 𝑛))))
409	349, 408	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) ↔ (𝑚 ∈ ℕ ∧ 𝑚 ≤ (𝑥 / 𝑛))))
410	409	simplbda 499	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ≤ (𝑥 / 𝑛))
411	407, 410	eqbrtrd 5160	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (1 · 𝑚) ≤ (𝑥 / 𝑛))
412		1red 11212	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 1 ∈ ℝ)
413	349	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (𝑥 / 𝑛) ∈ ℝ)
414	116	rpregt0d 13019	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (𝑚 ∈ ℝ ∧ 0 < 𝑚))
415	86, 414	sylan2 592	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (𝑚 ∈ ℝ ∧ 0 < 𝑚))
416		lemuldiv 12091	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℝ ∧ (𝑥 / 𝑛) ∈ ℝ ∧ (𝑚 ∈ ℝ ∧ 0 < 𝑚)) → ((1 · 𝑚) ≤ (𝑥 / 𝑛) ↔ 1 ≤ ((𝑥 / 𝑛) / 𝑚)))
417	412, 413, 415, 416	syl3anc 1368	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((1 · 𝑚) ≤ (𝑥 / 𝑛) ↔ 1 ≤ ((𝑥 / 𝑛) / 𝑚)))
418	411, 417	mpbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 1 ≤ ((𝑥 / 𝑛) / 𝑚))
419	86, 89	sylan2 592	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
420		logleb 26453	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ+ ∧ ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+) → (1 ≤ ((𝑥 / 𝑛) / 𝑚) ↔ (log‘1) ≤ (log‘((𝑥 / 𝑛) / 𝑚))))
421	211, 419, 420	sylancr 586	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (1 ≤ ((𝑥 / 𝑛) / 𝑚) ↔ (log‘1) ≤ (log‘((𝑥 / 𝑛) / 𝑚))))
422	418, 421	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (log‘1) ≤ (log‘((𝑥 / 𝑛) / 𝑚)))
423	224, 422	eqbrtrrid 5174	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 0 ≤ (log‘((𝑥 / 𝑛) / 𝑚)))
424		divge0 12080	. . . . . . . . . . . . . . . 16 ⊢ ((((log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ ∧ 0 ≤ (log‘((𝑥 / 𝑛) / 𝑚))) ∧ (𝑚 ∈ ℝ ∧ 0 < 𝑚)) → 0 ≤ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))
425	405, 423, 415, 424	syl21anc 835	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 0 ≤ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))
426	85, 402, 425	fsumge0 15738	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))
427	426	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 0 ≤ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))
428	404, 427	absidd 15366	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))
429		fzfid 13935	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
430	349	flcld 13760	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℤ)
431	430	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (⌊‘(𝑥 / 𝑛)) ∈ ℤ)
432		2z 12591	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℤ
433	432	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 2 ∈ ℤ)
434	349	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) ∈ ℝ)
435	199	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → e ∈ ℝ)
436		3re 12289	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 3 ∈ ℝ
437	436	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 3 ∈ ℝ)
438		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) < e)
439	203	simpri 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ e < 3
440	439	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → e < 3)
441	434, 435, 437, 438, 440	lttrd 11372	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) < 3)
442		3z 12592	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 3 ∈ ℤ
443		fllt 13768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ 3 ∈ ℤ) → ((𝑥 / 𝑛) < 3 ↔ (⌊‘(𝑥 / 𝑛)) < 3))
444	434, 442, 443	sylancl 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((𝑥 / 𝑛) < 3 ↔ (⌊‘(𝑥 / 𝑛)) < 3))
445	441, 444	mpbid 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (⌊‘(𝑥 / 𝑛)) < 3)
446		df-3 12273	. . . . . . . . . . . . . . . . . . . 20 ⊢ 3 = (2 + 1)
447	445, 446	breqtrdi 5179	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (⌊‘(𝑥 / 𝑛)) < (2 + 1))
448		zleltp1 12610	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((⌊‘(𝑥 / 𝑛)) ∈ ℤ ∧ 2 ∈ ℤ) → ((⌊‘(𝑥 / 𝑛)) ≤ 2 ↔ (⌊‘(𝑥 / 𝑛)) < (2 + 1)))
449	431, 432, 448	sylancl 585	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((⌊‘(𝑥 / 𝑛)) ≤ 2 ↔ (⌊‘(𝑥 / 𝑛)) < (2 + 1)))
450	447, 449	mpbird 257	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (⌊‘(𝑥 / 𝑛)) ≤ 2)
451		eluz2 12825	. . . . . . . . . . . . . . . . . 18 ⊢ (2 ∈ (ℤ≥‘(⌊‘(𝑥 / 𝑛))) ↔ ((⌊‘(𝑥 / 𝑛)) ∈ ℤ ∧ 2 ∈ ℤ ∧ (⌊‘(𝑥 / 𝑛)) ≤ 2))
452	431, 433, 450, 451	syl3anbrc 1340	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 2 ∈ (ℤ≥‘(⌊‘(𝑥 / 𝑛))))
453		fzss2 13538	. . . . . . . . . . . . . . . . 17 ⊢ (2 ∈ (ℤ≥‘(⌊‘(𝑥 / 𝑛))) → (1...(⌊‘(𝑥 / 𝑛))) ⊆ (1...2))
454	452, 453	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (1...(⌊‘(𝑥 / 𝑛))) ⊆ (1...2))
455	454	sselda 3974	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ (1...2))
456	34	ad5ant15 756	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
457	455, 456	syldan 590	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
458	429, 457	fsumrecl 15677	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
459	92	adantlr 712	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ ℕ) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
460	86, 459	sylan2 592	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
461	352	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (𝑥 / 𝑛) ≤ e)
462	434	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (𝑥 / 𝑛) ∈ ℝ)
463	199	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → e ∈ ℝ)
464	30	rpregt0d 13019	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (𝑚 ∈ ℝ ∧ 0 < 𝑚))
465	464	ad5ant15 756	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (𝑚 ∈ ℝ ∧ 0 < 𝑚))
466		lediv1 12076	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ e ∈ ℝ ∧ (𝑚 ∈ ℝ ∧ 0 < 𝑚)) → ((𝑥 / 𝑛) ≤ e ↔ ((𝑥 / 𝑛) / 𝑚) ≤ (e / 𝑚)))
467	462, 463, 465, 466	syl3anc 1368	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((𝑥 / 𝑛) ≤ e ↔ ((𝑥 / 𝑛) / 𝑚) ≤ (e / 𝑚)))
468	461, 467	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((𝑥 / 𝑛) / 𝑚) ≤ (e / 𝑚))
469	89	adantlr 712	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ ℕ) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
470	28, 469	sylan2 592	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
471	32	ad5ant15 756	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (e / 𝑚) ∈ ℝ+)
472	470, 471	logled 26477	. . . . . . . . . . . . . . . . 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 712	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ ℕ) → (log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
475	28, 474	sylan2 592	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
476	33	ad5ant15 756	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (log‘(e / 𝑚)) ∈ ℝ)
477		lediv1 12076	. . . . . . . . . . . . . . . . 17 ⊢ (((log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ ∧ (log‘(e / 𝑚)) ∈ ℝ ∧ (𝑚 ∈ ℝ ∧ 0 < 𝑚)) → ((log‘((𝑥 / 𝑛) / 𝑚)) ≤ (log‘(e / 𝑚)) ↔ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ ((log‘(e / 𝑚)) / 𝑚)))
478	475, 476, 465, 477	syl3anc 1368	. . . . . . . . . . . . . . . 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 590	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ ((log‘(e / 𝑚)) / 𝑚))
481	429, 460, 457, 480	fsumle 15742	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘(e / 𝑚)) / 𝑚))
482		fzfid 13935	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (1...2) ∈ Fin)
483	243	ad5ant15 756	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → 0 ≤ ((log‘(e / 𝑚)) / 𝑚))
484	482, 456, 483, 454	fsumless 15739	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘(e / 𝑚)) / 𝑚) ≤ Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚))
485	404, 458, 328, 481, 484	letrd 11368	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚))
486	428, 485	eqbrtrd 5160	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ≤ Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚))
487	322, 324, 327, 328, 401, 486	le2addd 11830	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘𝑇) + (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ (((1 / 2) + (γ + (abs‘𝐿))) + Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚)))
488	487, 15	breqtrrdi 5180	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘𝑇) + (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ 𝑅)
489	318, 325, 319, 326, 488	letrd 11368	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ 𝑅)
490	317, 318, 319, 320, 489	letrd 11368	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ 𝑅)
491	4, 208, 248, 249, 251, 272, 316, 490	fsumharmonic 26860	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · ((log‘e) + 1))))
492		2cnd 12287	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 ∈ ℂ)
493	3, 492, 303	fsummulc2 15727	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((log‘(𝑥 / 𝑛)) / 𝑥)))
494		df-2 12272	. . . . . . . . . 10 ⊢ 2 = (1 + 1)
495	357	oveq1i 7411	. . . . . . . . . 10 ⊢ ((log‘e) + 1) = (1 + 1)
496	494, 495	eqtr4i 2755	. . . . . . . . 9 ⊢ 2 = ((log‘e) + 1)
497	496	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 = ((log‘e) + 1))
498	497	oveq2d 7417	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑅 · 2) = (𝑅 · ((log‘e) + 1)))
499	493, 498	oveq12d 7419	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · ((log‘e) + 1))))
500	491, 499	breqtrrd 5166	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛)) ≤ ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)))
501	500	adantrr 714	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛)) ≤ ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)))
502	198, 501	eqbrtrrd 5162	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ≤ ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)))
503	54	leabsd 15358	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ≤ (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))))
504	503	adantrr 714	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ≤ (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))))
505	79, 80, 83, 502, 504	letrd 11368	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ≤ (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))))
506	1, 53, 54, 77, 505	o1le 15596	1 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ∈ 𝑂(1))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   ≠ wne 2932  {crab 3424   ⊆ wss 3940   class class class wbr 5138   ↦ cmpt 5221  ‘cfv 6533  (class class class)co 7401  ℂcc 11104  ℝcr 11105  0cc0 11106  1c1 11107   + caddc 11109   · cmul 11111   < clt 11245   ≤ cle 11246   − cmin 11441   / cdiv 11868  ℕcn 12209  2c2 12264  3c3 12265  ℤcz 12555  ℤ_≥cuz 12819  ℝ⁺crp 12971  ...cfz 13481  ⌊cfl 13752  ↑cexp 14024  abscabs 15178   ⇝_𝑟 crli 15426  𝑂(1)co1 15427  Σcsu 15629  eceu 16003   ∥ cdvds 16194  logclog 26405  γcem 26840  μcmu 26943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-iin 4990  df-disj 5104  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-om 7849  df-1st 7968  df-2nd 7969  df-supp 8141  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-oadd 8465  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-dju 9892  df-card 9930  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-xnn0 12542  df-z 12556  df-dec 12675  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ioo 13325  df-ioc 13326  df-ico 13327  df-icc 13328  df-fz 13482  df-fzo 13625  df-fl 13754  df-mod 13832  df-seq 13964  df-exp 14025  df-fac 14231  df-bc 14260  df-hash 14288  df-shft 15011  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-limsup 15412  df-clim 15429  df-rlim 15430  df-o1 15431  df-lo1 15432  df-sum 15630  df-ef 16008  df-e 16009  df-sin 16010  df-cos 16011  df-tan 16012  df-pi 16013  df-dvds 16195  df-gcd 16433  df-prm 16606  df-pc 16769  df-struct 17079  df-sets 17096  df-slot 17114  df-ndx 17126  df-base 17144  df-ress 17173  df-plusg 17209  df-mulr 17210  df-starv 17211  df-sca 17212  df-vsca 17213  df-ip 17214  df-tset 17215  df-ple 17216  df-ds 17218  df-unif 17219  df-hom 17220  df-cco 17221  df-rest 17367  df-topn 17368  df-0g 17386  df-gsum 17387  df-topgen 17388  df-pt 17389  df-prds 17392  df-xrs 17447  df-qtop 17452  df-imas 17453  df-xps 17455  df-mre 17529  df-mrc 17530  df-acs 17532  df-mgm 18563  df-sgrp 18642  df-mnd 18658  df-submnd 18704  df-mulg 18986  df-cntz 19223  df-cmn 19692  df-psmet 21220  df-xmet 21221  df-met 21222  df-bl 21223  df-mopn 21224  df-fbas 21225  df-fg 21226  df-cnfld 21229  df-top 22718  df-topon 22735  df-topsp 22757  df-bases 22771  df-cld 22845  df-ntr 22846  df-cls 22847  df-nei 22924  df-lp 22962  df-perf 22963  df-cn 23053  df-cnp 23054  df-haus 23141  df-cmp 23213  df-tx 23388  df-hmeo 23581  df-fil 23672  df-fm 23764  df-flim 23765  df-flf 23766  df-xms 24148  df-ms 24149  df-tms 24150  df-cncf 24720  df-limc 25717  df-dv 25718  df-ulm 26230  df-log 26407  df-cxp 26408  df-atan 26715  df-em 26841  df-mu 26949

This theorem is referenced by:  mulog2sumlem3  27385