dchrvmasumlem2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dchrvmasumlem2		Structured version Visualization version GIF version

Theorem dchrvmasumlem2 25187

Description: Lemma for dchrvmasum 25214. (Contributed by Mario Carneiro, 4-May-2016.)

**Hypotheses**
Ref	Expression
rpvmasum.z	⊢ 𝑍 = (ℤ/nℤ‘𝑁)
rpvmasum.l	⊢ 𝐿 = (ℤRHom‘𝑍)
rpvmasum.a	⊢ (𝜑 → 𝑁 ∈ ℕ)
rpvmasum.g	⊢ 𝐺 = (DChr‘𝑁)
rpvmasum.d	⊢ 𝐷 = (Base‘𝐺)
rpvmasum.1	⊢ 1 = (0_g‘𝐺)
dchrisum.b	⊢ (𝜑 → 𝑋 ∈ 𝐷)
dchrisum.n1	⊢ (𝜑 → 𝑋 ≠ 1 )
dchrvmasum.f	⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → 𝐹 ∈ ℂ)
dchrvmasum.g	⊢ (𝑚 = (𝑥 / 𝑑) → 𝐹 = 𝐾)
dchrvmasum.c	⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))
dchrvmasum.t	⊢ (𝜑 → 𝑇 ∈ ℂ)
dchrvmasum.1	⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → (abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)))
dchrvmasum.r	⊢ (𝜑 → 𝑅 ∈ ℝ)
dchrvmasum.2	⊢ (𝜑 → ∀𝑚 ∈ (1[,)3)(abs‘(𝐹 − 𝑇)) ≤ 𝑅)

**Assertion**
Ref	Expression
dchrvmasumlem2	⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ∈ 𝑂(1))

Distinct variable groups: 𝑥,𝑚, 1 𝑚,𝑑,𝑥,𝐶 𝐹,𝑑,𝑥 𝑚,𝐾 𝑚,𝑁,𝑥 𝜑,𝑑,𝑚,𝑥 𝑇,𝑑,𝑚,𝑥 𝑅,𝑑,𝑚,𝑥 𝑚,𝑍,𝑥 𝐷,𝑚,𝑥 𝐿,𝑑,𝑚,𝑥 𝑋,𝑑,𝑚,𝑥 Allowed substitution hints: 𝐷(𝑑) 1 (𝑑) 𝐹(𝑚) 𝐺(𝑥,𝑚,𝑑) 𝐾(𝑥,𝑑) 𝑁(𝑑) 𝑍(𝑑)

**Proof of Theorem dchrvmasumlem2**
Step	Hyp	Ref	Expression
1		1red 10055	. 2 ⊢ (𝜑 → 1 ∈ ℝ)
2		dchrvmasum.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))
3		elrege0 12278	. . . . . . 7 ⊢ (𝐶 ∈ (0[,)+∞) ↔ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶))
4	2, 3	sylib 208	. . . . . 6 ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶))
5	4	simpld 475	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ ℝ)
6	5	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝐶 ∈ ℝ)
7		fzfid 12772	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (1...(⌊‘𝑥)) ∈ Fin)
8		simpr 477	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ⁺)
9		elfznn 12370	. . . . . . . . 9 ⊢ (𝑑 ∈ (1...(⌊‘𝑥)) → 𝑑 ∈ ℕ)
10	9	nnrpd 11870	. . . . . . . 8 ⊢ (𝑑 ∈ (1...(⌊‘𝑥)) → 𝑑 ∈ ℝ⁺)
11		rpdivcl 11856	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ℝ⁺) → (𝑥 / 𝑑) ∈ ℝ⁺)
12	8, 10, 11	syl2an 494	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑑) ∈ ℝ⁺)
13		relogcl 24322	. . . . . . 7 ⊢ ((𝑥 / 𝑑) ∈ ℝ⁺ → (log‘(𝑥 / 𝑑)) ∈ ℝ)
14	12, 13	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑑)) ∈ ℝ)
15	8	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ⁺)
16	14, 15	rerpdivcld 11903	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑑)) / 𝑥) ∈ ℝ)
17	7, 16	fsumrecl 14465	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥) ∈ ℝ)
18	6, 17	remulcld 10070	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ∈ ℝ)
19		dchrvmasum.r	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ ℝ)
20		3nn 11186	. . . . . . 7 ⊢ 3 ∈ ℕ
21		nnrp 11842	. . . . . . 7 ⊢ (3 ∈ ℕ → 3 ∈ ℝ⁺)
22		relogcl 24322	. . . . . . 7 ⊢ (3 ∈ ℝ⁺ → (log‘3) ∈ ℝ)
23	20, 21, 22	mp2b 10	. . . . . 6 ⊢ (log‘3) ∈ ℝ
24		1re 10039	. . . . . 6 ⊢ 1 ∈ ℝ
25	23, 24	readdcli 10053	. . . . 5 ⊢ ((log‘3) + 1) ∈ ℝ
26		remulcl 10021	. . . . 5 ⊢ ((𝑅 ∈ ℝ ∧ ((log‘3) + 1) ∈ ℝ) → (𝑅 · ((log‘3) + 1)) ∈ ℝ)
27	19, 25, 26	sylancl 694	. . . 4 ⊢ (𝜑 → (𝑅 · ((log‘3) + 1)) ∈ ℝ)
28	27	adantr 481	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑅 · ((log‘3) + 1)) ∈ ℝ)
29		rpssre 11843	. . . . 5 ⊢ ℝ⁺ ⊆ ℝ
30	5	recnd 10068	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ ℂ)
31		o1const 14350	. . . . 5 ⊢ ((ℝ⁺ ⊆ ℝ ∧ 𝐶 ∈ ℂ) → (𝑥 ∈ ℝ⁺ ↦ 𝐶) ∈ 𝑂(1))
32	29, 30, 31	sylancr 695	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ 𝐶) ∈ 𝑂(1))
33		logfacrlim2 24951	. . . . 5 ⊢ (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ⇝_𝑟 1
34		rlimo1 14347	. . . . 5 ⊢ ((𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ⇝_𝑟 1 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ∈ 𝑂(1))
35	33, 34	mp1i 13	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ∈ 𝑂(1))
36	6, 17, 32, 35	o1mul2 14355	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥))) ∈ 𝑂(1))
37	27	recnd 10068	. . . 4 ⊢ (𝜑 → (𝑅 · ((log‘3) + 1)) ∈ ℂ)
38		o1const 14350	. . . 4 ⊢ ((ℝ⁺ ⊆ ℝ ∧ (𝑅 · ((log‘3) + 1)) ∈ ℂ) → (𝑥 ∈ ℝ⁺ ↦ (𝑅 · ((log‘3) + 1))) ∈ 𝑂(1))
39	29, 37, 38	sylancr 695	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (𝑅 · ((log‘3) + 1))) ∈ 𝑂(1))
40	18, 28, 36, 39	o1add2 14354	. 2 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1)))) ∈ 𝑂(1))
41	18, 28	readdcld 10069	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))) ∈ ℝ)
42		dchrvmasum.f	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → 𝐹 ∈ ℂ)
43	42	ralrimiva 2966	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑚 ∈ ℝ⁺ 𝐹 ∈ ℂ)
44	43	ad2antrr 762	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ∀𝑚 ∈ ℝ⁺ 𝐹 ∈ ℂ)
45		dchrvmasum.g	. . . . . . . . . 10 ⊢ (𝑚 = (𝑥 / 𝑑) → 𝐹 = 𝐾)
46	45	eleq1d 2686	. . . . . . . . 9 ⊢ (𝑚 = (𝑥 / 𝑑) → (𝐹 ∈ ℂ ↔ 𝐾 ∈ ℂ))
47	46	rspcv 3305	. . . . . . . 8 ⊢ ((𝑥 / 𝑑) ∈ ℝ⁺ → (∀𝑚 ∈ ℝ⁺ 𝐹 ∈ ℂ → 𝐾 ∈ ℂ))
48	12, 44, 47	sylc 65	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝐾 ∈ ℂ)
49		dchrvmasum.t	. . . . . . . 8 ⊢ (𝜑 → 𝑇 ∈ ℂ)
50	49	ad2antrr 762	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑇 ∈ ℂ)
51	48, 50	subcld 10392	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐾 − 𝑇) ∈ ℂ)
52	51	abscld 14175	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘(𝐾 − 𝑇)) ∈ ℝ)
53	9	adantl 482	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ∈ ℕ)
54	52, 53	nndivred 11069	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℝ)
55	7, 54	fsumrecl 14465	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℝ)
56	55	recnd 10068	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℂ)
57	53	nnrpd 11870	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ∈ ℝ⁺)
58	51	absge0d 14183	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘(𝐾 − 𝑇)))
59	52, 57, 58	divge0d 11912	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((abs‘(𝐾 − 𝑇)) / 𝑑))
60	7, 54, 59	fsumge0 14527	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 0 ≤ Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑))
61	55, 60	absidd 14161	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) = Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑))
62	61, 55	eqeltrd 2701	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ∈ ℝ)
63	41	recnd 10068	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))) ∈ ℂ)
64	63	abscld 14175	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1)))) ∈ ℝ)
65		3re 11094	. . . . . . . 8 ⊢ 3 ∈ ℝ
66	65	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 3 ∈ ℝ)
67		1le3 11244	. . . . . . 7 ⊢ 1 ≤ 3
68	66, 67	jctir 561	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (3 ∈ ℝ ∧ 1 ≤ 3))
69	19	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑅 ∈ ℝ)
70	24	rexri 10097	. . . . . . . . . 10 ⊢ 1 ∈ ℝ^*
71	65	rexri 10097	. . . . . . . . . 10 ⊢ 3 ∈ ℝ^*
72		1lt3 11196	. . . . . . . . . 10 ⊢ 1 < 3
73		lbico1 12228	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ^* ∧ 3 ∈ ℝ^* ∧ 1 < 3) → 1 ∈ (1[,)3))
74	70, 71, 72, 73	mp3an 1424	. . . . . . . . 9 ⊢ 1 ∈ (1[,)3)
75		0red 10041	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 0 ∈ ℝ)
76		elico2 12237	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℝ ∧ 3 ∈ ℝ^*) → (𝑚 ∈ (1[,)3) ↔ (𝑚 ∈ ℝ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 3)))
77	24, 71, 76	mp2an 708	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1[,)3) ↔ (𝑚 ∈ ℝ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 3))
78	77	simp1bi 1076	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (1[,)3) → 𝑚 ∈ ℝ)
79		0red 10041	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1[,)3) → 0 ∈ ℝ)
80		1red 10055	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1[,)3) → 1 ∈ ℝ)
81		0lt1 10550	. . . . . . . . . . . . . . 15 ⊢ 0 < 1
82	81	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1[,)3) → 0 < 1)
83	77	simp2bi 1077	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1[,)3) → 1 ≤ 𝑚)
84	79, 80, 78, 82, 83	ltletrd 10197	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (1[,)3) → 0 < 𝑚)
85	78, 84	elrpd 11869	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (1[,)3) → 𝑚 ∈ ℝ⁺)
86	49	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → 𝑇 ∈ ℂ)
87	42, 86	subcld 10392	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → (𝐹 − 𝑇) ∈ ℂ)
88	87	abscld 14175	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → (abs‘(𝐹 − 𝑇)) ∈ ℝ)
89	85, 88	sylan2 491	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (abs‘(𝐹 − 𝑇)) ∈ ℝ)
90	19	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 𝑅 ∈ ℝ)
91	87	absge0d 14183	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → 0 ≤ (abs‘(𝐹 − 𝑇)))
92	85, 91	sylan2 491	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 0 ≤ (abs‘(𝐹 − 𝑇)))
93		dchrvmasum.2	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑚 ∈ (1[,)3)(abs‘(𝐹 − 𝑇)) ≤ 𝑅)
94	93	r19.21bi 2932	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (abs‘(𝐹 − 𝑇)) ≤ 𝑅)
95	75, 89, 90, 92, 94	letrd 10194	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 0 ≤ 𝑅)
96	95	ralrimiva 2966	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑚 ∈ (1[,)3)0 ≤ 𝑅)
97		biidd 252	. . . . . . . . . 10 ⊢ (𝑚 = 1 → (0 ≤ 𝑅 ↔ 0 ≤ 𝑅))
98	97	rspcv 3305	. . . . . . . . 9 ⊢ (1 ∈ (1[,)3) → (∀𝑚 ∈ (1[,)3)0 ≤ 𝑅 → 0 ≤ 𝑅))
99	74, 96, 98	mpsyl 68	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ 𝑅)
100	99	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 0 ≤ 𝑅)
101	69, 100	jca 554	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅))
102	52	recnd 10068	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘(𝐾 − 𝑇)) ∈ ℂ)
103	5	ad2antrr 762	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝐶 ∈ ℝ)
104	103, 16	remulcld 10070	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) ∈ ℝ)
105	4	ad2antrr 762	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶))
106		log1 24332	. . . . . . . . 9 ⊢ (log‘1) = 0
107	53	nncnd 11036	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ∈ ℂ)
108	107	mulid2d 10058	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (1 · 𝑑) = 𝑑)
109		rpre 11839	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
110	109	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ)
111		fznnfl 12661	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (𝑑 ∈ (1...(⌊‘𝑥)) ↔ (𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝑥)))
112	110, 111	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑑 ∈ (1...(⌊‘𝑥)) ↔ (𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝑥)))
113	112	simplbda 654	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ≤ 𝑥)
114	108, 113	eqbrtrd 4675	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (1 · 𝑑) ≤ 𝑥)
115		1red 10055	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
116	109	ad2antlr 763	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
117	115, 116, 57	lemuldivd 11921	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((1 · 𝑑) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑑)))
118	114, 117	mpbid 222	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 1 ≤ (𝑥 / 𝑑))
119		1rp 11836	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ⁺
120	119	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ⁺)
121	120, 12	logled 24373	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (1 ≤ (𝑥 / 𝑑) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑑))))
122	118, 121	mpbid 222	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (log‘1) ≤ (log‘(𝑥 / 𝑑)))
123	106, 122	syl5eqbrr 4689	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ (log‘(𝑥 / 𝑑)))
124		rpregt0 11846	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
125	124	ad2antlr 763	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
126		divge0 10892	. . . . . . . 8 ⊢ ((((log‘(𝑥 / 𝑑)) ∈ ℝ ∧ 0 ≤ (log‘(𝑥 / 𝑑))) ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → 0 ≤ ((log‘(𝑥 / 𝑑)) / 𝑥))
127	14, 123, 125, 126	syl21anc 1325	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((log‘(𝑥 / 𝑑)) / 𝑥))
128		mulge0 10546	. . . . . . 7 ⊢ (((𝐶 ∈ ℝ ∧ 0 ≤ 𝐶) ∧ (((log‘(𝑥 / 𝑑)) / 𝑥) ∈ ℝ ∧ 0 ≤ ((log‘(𝑥 / 𝑑)) / 𝑥))) → 0 ≤ (𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)))
129	105, 16, 127, 128	syl12anc 1324	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ (𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)))
130		absidm 14063	. . . . . . . . 9 ⊢ ((𝐾 − 𝑇) ∈ ℂ → (abs‘(abs‘(𝐾 − 𝑇))) = (abs‘(𝐾 − 𝑇)))
131	51, 130	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘(abs‘(𝐾 − 𝑇))) = (abs‘(𝐾 − 𝑇)))
132	131	adantr 481	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (abs‘(abs‘(𝐾 − 𝑇))) = (abs‘(𝐾 − 𝑇)))
133		nndivre 11056	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 𝑑 ∈ ℕ) → (𝑥 / 𝑑) ∈ ℝ)
134	110, 9, 133	syl2an 494	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑑) ∈ ℝ)
135	134	adantr 481	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (𝑥 / 𝑑) ∈ ℝ)
136		simpr 477	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → 3 ≤ (𝑥 / 𝑑))
137		elicopnf 12269	. . . . . . . . . . 11 ⊢ (3 ∈ ℝ → ((𝑥 / 𝑑) ∈ (3[,)+∞) ↔ ((𝑥 / 𝑑) ∈ ℝ ∧ 3 ≤ (𝑥 / 𝑑))))
138	65, 137	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑥 / 𝑑) ∈ (3[,)+∞) ↔ ((𝑥 / 𝑑) ∈ ℝ ∧ 3 ≤ (𝑥 / 𝑑)))
139	135, 136, 138	sylanbrc 698	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (𝑥 / 𝑑) ∈ (3[,)+∞))
140		dchrvmasum.1	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → (abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)))
141	140	ralrimiva 2966	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑚 ∈ (3[,)+∞)(abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)))
142	141	ad3antrrr 766	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → ∀𝑚 ∈ (3[,)+∞)(abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)))
143	45	oveq1d 6665	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑥 / 𝑑) → (𝐹 − 𝑇) = (𝐾 − 𝑇))
144	143	fveq2d 6195	. . . . . . . . . . 11 ⊢ (𝑚 = (𝑥 / 𝑑) → (abs‘(𝐹 − 𝑇)) = (abs‘(𝐾 − 𝑇)))
145		fveq2 6191	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑥 / 𝑑) → (log‘𝑚) = (log‘(𝑥 / 𝑑)))
146		id 22	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑥 / 𝑑) → 𝑚 = (𝑥 / 𝑑))
147	145, 146	oveq12d 6668	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑥 / 𝑑) → ((log‘𝑚) / 𝑚) = ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)))
148	147	oveq2d 6666	. . . . . . . . . . 11 ⊢ (𝑚 = (𝑥 / 𝑑) → (𝐶 · ((log‘𝑚) / 𝑚)) = (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))))
149	144, 148	breq12d 4666	. . . . . . . . . 10 ⊢ (𝑚 = (𝑥 / 𝑑) → ((abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)) ↔ (abs‘(𝐾 − 𝑇)) ≤ (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)))))
150	149	rspcv 3305	. . . . . . . . 9 ⊢ ((𝑥 / 𝑑) ∈ (3[,)+∞) → (∀𝑚 ∈ (3[,)+∞)(abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)) → (abs‘(𝐾 − 𝑇)) ≤ (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)))))
151	139, 142, 150	sylc 65	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (abs‘(𝐾 − 𝑇)) ≤ (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))))
152	14	recnd 10068	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑑)) ∈ ℂ)
153		rpcnne0 11850	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
154	153	ad2antlr 763	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
155	57	rpcnne0d 11881	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑑 ∈ ℂ ∧ 𝑑 ≠ 0))
156		divdiv2 10737	. . . . . . . . . . . . 13 ⊢ (((log‘(𝑥 / 𝑑)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ (𝑑 ∈ ℂ ∧ 𝑑 ≠ 0)) → ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)) = (((log‘(𝑥 / 𝑑)) · 𝑑) / 𝑥))
157	152, 154, 155, 156	syl3anc 1326	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)) = (((log‘(𝑥 / 𝑑)) · 𝑑) / 𝑥))
158		div23 10704	. . . . . . . . . . . . 13 ⊢ (((log‘(𝑥 / 𝑑)) ∈ ℂ ∧ 𝑑 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((log‘(𝑥 / 𝑑)) · 𝑑) / 𝑥) = (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑))
159	152, 107, 154, 158	syl3anc 1326	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑑)) · 𝑑) / 𝑥) = (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑))
160	157, 159	eqtrd 2656	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)) = (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑))
161	160	oveq2d 6666	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))) = (𝐶 · (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑)))
162	30	ad2antrr 762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝐶 ∈ ℂ)
163	16	recnd 10068	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑑)) / 𝑥) ∈ ℂ)
164	162, 163, 107	mulassd 10063	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑) = (𝐶 · (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑)))
165	161, 164	eqtr4d 2659	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))) = ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑))
166	165	adantr 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))) = ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑))
167	151, 166	breqtrd 4679	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (abs‘(𝐾 − 𝑇)) ≤ ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑))
168	132, 167	eqbrtrd 4675	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (abs‘(abs‘(𝐾 − 𝑇))) ≤ ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑))
169	131	adantr 481	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (abs‘(abs‘(𝐾 − 𝑇))) = (abs‘(𝐾 − 𝑇)))
170	134	adantr 481	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (𝑥 / 𝑑) ∈ ℝ)
171	118	adantr 481	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → 1 ≤ (𝑥 / 𝑑))
172		simpr 477	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (𝑥 / 𝑑) < 3)
173		elico2 12237	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ 3 ∈ ℝ^*) → ((𝑥 / 𝑑) ∈ (1[,)3) ↔ ((𝑥 / 𝑑) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑑) ∧ (𝑥 / 𝑑) < 3)))
174	24, 71, 173	mp2an 708	. . . . . . . . 9 ⊢ ((𝑥 / 𝑑) ∈ (1[,)3) ↔ ((𝑥 / 𝑑) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑑) ∧ (𝑥 / 𝑑) < 3))
175	170, 171, 172, 174	syl3anbrc 1246	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (𝑥 / 𝑑) ∈ (1[,)3))
176	93	ad3antrrr 766	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → ∀𝑚 ∈ (1[,)3)(abs‘(𝐹 − 𝑇)) ≤ 𝑅)
177	144	breq1d 4663	. . . . . . . . 9 ⊢ (𝑚 = (𝑥 / 𝑑) → ((abs‘(𝐹 − 𝑇)) ≤ 𝑅 ↔ (abs‘(𝐾 − 𝑇)) ≤ 𝑅))
178	177	rspcv 3305	. . . . . . . 8 ⊢ ((𝑥 / 𝑑) ∈ (1[,)3) → (∀𝑚 ∈ (1[,)3)(abs‘(𝐹 − 𝑇)) ≤ 𝑅 → (abs‘(𝐾 − 𝑇)) ≤ 𝑅))
179	175, 176, 178	sylc 65	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (abs‘(𝐾 − 𝑇)) ≤ 𝑅)
180	169, 179	eqbrtrd 4675	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (abs‘(abs‘(𝐾 − 𝑇))) ≤ 𝑅)
181	8, 68, 101, 102, 104, 129, 168, 180	fsumharmonic 24738	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ≤ (Σ𝑑 ∈ (1...(⌊‘𝑥))(𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))))
182	30	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝐶 ∈ ℂ)
183	7, 182, 163	fsummulc2 14516	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) = Σ𝑑 ∈ (1...(⌊‘𝑥))(𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)))
184	183	oveq1d 6665	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))) = (Σ𝑑 ∈ (1...(⌊‘𝑥))(𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))))
185	181, 184	breqtrrd 4681	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ≤ ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))))
186	41	leabsd 14153	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))) ≤ (abs‘((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1)))))
187	62, 41, 64, 185, 186	letrd 10194	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ≤ (abs‘((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1)))))
188	187	adantrr 753	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ≤ (abs‘((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1)))))
189	1, 40, 41, 56, 188	o1le 14383	1 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ∈ 𝑂(1))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 ⊆ wss 3574 class class class wbr 4653 ↦ cmpt 4729 ‘cfv 5888 (class class class)co 6650 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 +∞cpnf 10071 ℝ^*cxr 10073 < clt 10074 ≤ cle 10075 − cmin 10266 / cdiv 10684 ℕcn 11020 3c3 11071 ℝ⁺crp 11832 [,)cico 12177 ...cfz 12326 ⌊cfl 12591 abscabs 13974 ⇝_𝑟 crli 14216 𝑂(1)co1 14217 Σcsu 14416 Basecbs 15857 0_gc0g 16100 ℤRHomczrh 19848 ℤ/nℤczn 19851 logclog 24301 DChrcdchr 24957

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ioc 12180 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861 df-fac 13061 df-bc 13090 df-hash 13118 df-shft 13807 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-limsup 14202 df-clim 14219 df-rlim 14220 df-o1 14221 df-lo1 14222 df-sum 14417 df-ef 14798 df-e 14799 df-sin 14800 df-cos 14801 df-pi 14803 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-hom 15966 df-cco 15967 df-rest 16083 df-topn 16084 df-0g 16102 df-gsum 16103 df-topgen 16104 df-pt 16105 df-prds 16108 df-xrs 16162 df-qtop 16167 df-imas 16168 df-xps 16170 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-submnd 17336 df-mulg 17541 df-cntz 17750 df-cmn 18195 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-fbas 19743 df-fg 19744 df-cnfld 19747 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cld 20823 df-ntr 20824 df-cls 20825 df-nei 20902 df-lp 20940 df-perf 20941 df-cn 21031 df-cnp 21032 df-haus 21119 df-cmp 21190 df-tx 21365 df-hmeo 21558 df-fil 21650 df-fm 21742 df-flim 21743 df-flf 21744 df-xms 22125 df-ms 22126 df-tms 22127 df-cncf 22681 df-limc 23630 df-dv 23631 df-log 24303 df-cxp 24304 df-em 24719

This theorem is referenced by: dchrvmasumlem3 25188

W3C validator