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 27478

Description: Lemma for dchrvmasum 27505. (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 11244	. 2 ⊢ (𝜑 → 1 ∈ ℝ)
2		dchrvmasum.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))
3		elrege0 13476	. . . . . . 7 ⊢ (𝐶 ∈ (0[,)+∞) ↔ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶))
4	2, 3	sylib 218	. . . . . 6 ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶))
5	4	simpld 494	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ ℝ)
6	5	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝐶 ∈ ℝ)
7		fzfid 13996	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (1...(⌊‘𝑥)) ∈ Fin)
8		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ⁺)
9		elfznn 13575	. . . . . . . . 9 ⊢ (𝑑 ∈ (1...(⌊‘𝑥)) → 𝑑 ∈ ℕ)
10	9	nnrpd 13057	. . . . . . . 8 ⊢ (𝑑 ∈ (1...(⌊‘𝑥)) → 𝑑 ∈ ℝ⁺)
11		rpdivcl 13042	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ℝ⁺) → (𝑥 / 𝑑) ∈ ℝ⁺)
12	8, 10, 11	syl2an 596	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑑) ∈ ℝ⁺)
13	12	relogcld 26601	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑑)) ∈ ℝ)
14	8	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ⁺)
15	13, 14	rerpdivcld 13090	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑑)) / 𝑥) ∈ ℝ)
16	7, 15	fsumrecl 15752	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥) ∈ ℝ)
17	6, 16	remulcld 11273	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ∈ ℝ)
18		dchrvmasum.r	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ ℝ)
19		3nn 12327	. . . . . . 7 ⊢ 3 ∈ ℕ
20		nnrp 13028	. . . . . . 7 ⊢ (3 ∈ ℕ → 3 ∈ ℝ⁺)
21		relogcl 26553	. . . . . . 7 ⊢ (3 ∈ ℝ⁺ → (log‘3) ∈ ℝ)
22	19, 20, 21	mp2b 10	. . . . . 6 ⊢ (log‘3) ∈ ℝ
23		1re 11243	. . . . . 6 ⊢ 1 ∈ ℝ
24	22, 23	readdcli 11258	. . . . 5 ⊢ ((log‘3) + 1) ∈ ℝ
25		remulcl 11222	. . . . 5 ⊢ ((𝑅 ∈ ℝ ∧ ((log‘3) + 1) ∈ ℝ) → (𝑅 · ((log‘3) + 1)) ∈ ℝ)
26	18, 24, 25	sylancl 586	. . . 4 ⊢ (𝜑 → (𝑅 · ((log‘3) + 1)) ∈ ℝ)
27	26	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑅 · ((log‘3) + 1)) ∈ ℝ)
28		rpssre 13024	. . . . 5 ⊢ ℝ⁺ ⊆ ℝ
29	5	recnd 11271	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ ℂ)
30		o1const 15638	. . . . 5 ⊢ ((ℝ⁺ ⊆ ℝ ∧ 𝐶 ∈ ℂ) → (𝑥 ∈ ℝ⁺ ↦ 𝐶) ∈ 𝑂(1))
31	28, 29, 30	sylancr 587	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ 𝐶) ∈ 𝑂(1))
32		logfacrlim2 27206	. . . . 5 ⊢ (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ⇝_𝑟 1
33		rlimo1 15635	. . . . 5 ⊢ ((𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ⇝_𝑟 1 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ∈ 𝑂(1))
34	32, 33	mp1i 13	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ∈ 𝑂(1))
35	6, 16, 31, 34	o1mul2 15643	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥))) ∈ 𝑂(1))
36	26	recnd 11271	. . . 4 ⊢ (𝜑 → (𝑅 · ((log‘3) + 1)) ∈ ℂ)
37		o1const 15638	. . . 4 ⊢ ((ℝ⁺ ⊆ ℝ ∧ (𝑅 · ((log‘3) + 1)) ∈ ℂ) → (𝑥 ∈ ℝ⁺ ↦ (𝑅 · ((log‘3) + 1))) ∈ 𝑂(1))
38	28, 36, 37	sylancr 587	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (𝑅 · ((log‘3) + 1))) ∈ 𝑂(1))
39	17, 27, 35, 38	o1add2 15642	. 2 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1)))) ∈ 𝑂(1))
40	17, 27	readdcld 11272	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))) ∈ ℝ)
41		dchrvmasum.g	. . . . . . . . 9 ⊢ (𝑚 = (𝑥 / 𝑑) → 𝐹 = 𝐾)
42	41	eleq1d 2818	. . . . . . . 8 ⊢ (𝑚 = (𝑥 / 𝑑) → (𝐹 ∈ ℂ ↔ 𝐾 ∈ ℂ))
43		dchrvmasum.f	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → 𝐹 ∈ ℂ)
44	43	ralrimiva 3133	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑚 ∈ ℝ⁺ 𝐹 ∈ ℂ)
45	44	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ∀𝑚 ∈ ℝ⁺ 𝐹 ∈ ℂ)
46	42, 45, 12	rspcdva 3606	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝐾 ∈ ℂ)
47		dchrvmasum.t	. . . . . . . 8 ⊢ (𝜑 → 𝑇 ∈ ℂ)
48	47	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑇 ∈ ℂ)
49	46, 48	subcld 11602	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐾 − 𝑇) ∈ ℂ)
50	49	abscld 15457	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘(𝐾 − 𝑇)) ∈ ℝ)
51	9	adantl 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ∈ ℕ)
52	50, 51	nndivred 12302	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℝ)
53	7, 52	fsumrecl 15752	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℝ)
54	53	recnd 11271	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℂ)
55	51	nnrpd 13057	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ∈ ℝ⁺)
56	49	absge0d 15465	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘(𝐾 − 𝑇)))
57	50, 55, 56	divge0d 13099	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((abs‘(𝐾 − 𝑇)) / 𝑑))
58	7, 52, 57	fsumge0 15813	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 0 ≤ Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑))
59	53, 58	absidd 15443	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) = Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑))
60	59, 53	eqeltrd 2833	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ∈ ℝ)
61	40	recnd 11271	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))) ∈ ℂ)
62	61	abscld 15457	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1)))) ∈ ℝ)
63		3re 12328	. . . . . . . 8 ⊢ 3 ∈ ℝ
64	63	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 3 ∈ ℝ)
65		1le3 12460	. . . . . . 7 ⊢ 1 ≤ 3
66	64, 65	jctir 520	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (3 ∈ ℝ ∧ 1 ≤ 3))
67	18	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑅 ∈ ℝ)
68	23	rexri 11301	. . . . . . . . . 10 ⊢ 1 ∈ ℝ^*
69	63	rexri 11301	. . . . . . . . . 10 ⊢ 3 ∈ ℝ^*
70		1lt3 12421	. . . . . . . . . 10 ⊢ 1 < 3
71		lbico1 13423	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ^* ∧ 3 ∈ ℝ^* ∧ 1 < 3) → 1 ∈ (1[,)3))
72	68, 69, 70, 71	mp3an 1462	. . . . . . . . 9 ⊢ 1 ∈ (1[,)3)
73		0red 11246	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 0 ∈ ℝ)
74		elico2 13433	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℝ ∧ 3 ∈ ℝ^*) → (𝑚 ∈ (1[,)3) ↔ (𝑚 ∈ ℝ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 3)))
75	23, 69, 74	mp2an 692	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1[,)3) ↔ (𝑚 ∈ ℝ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 3))
76	75	simp1bi 1145	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (1[,)3) → 𝑚 ∈ ℝ)
77		0red 11246	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1[,)3) → 0 ∈ ℝ)
78		1red 11244	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1[,)3) → 1 ∈ ℝ)
79		0lt1 11767	. . . . . . . . . . . . . . 15 ⊢ 0 < 1
80	79	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1[,)3) → 0 < 1)
81	75	simp2bi 1146	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1[,)3) → 1 ≤ 𝑚)
82	77, 78, 76, 80, 81	ltletrd 11403	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (1[,)3) → 0 < 𝑚)
83	76, 82	elrpd 13056	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (1[,)3) → 𝑚 ∈ ℝ⁺)
84	47	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → 𝑇 ∈ ℂ)
85	43, 84	subcld 11602	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → (𝐹 − 𝑇) ∈ ℂ)
86	85	abscld 15457	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → (abs‘(𝐹 − 𝑇)) ∈ ℝ)
87	83, 86	sylan2 593	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (abs‘(𝐹 − 𝑇)) ∈ ℝ)
88	18	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 𝑅 ∈ ℝ)
89	85	absge0d 15465	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → 0 ≤ (abs‘(𝐹 − 𝑇)))
90	83, 89	sylan2 593	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 0 ≤ (abs‘(𝐹 − 𝑇)))
91		dchrvmasum.2	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑚 ∈ (1[,)3)(abs‘(𝐹 − 𝑇)) ≤ 𝑅)
92	91	r19.21bi 3237	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (abs‘(𝐹 − 𝑇)) ≤ 𝑅)
93	73, 87, 88, 90, 92	letrd 11400	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 0 ≤ 𝑅)
94	93	ralrimiva 3133	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑚 ∈ (1[,)3)0 ≤ 𝑅)
95		biidd 262	. . . . . . . . . 10 ⊢ (𝑚 = 1 → (0 ≤ 𝑅 ↔ 0 ≤ 𝑅))
96	95	rspcv 3601	. . . . . . . . 9 ⊢ (1 ∈ (1[,)3) → (∀𝑚 ∈ (1[,)3)0 ≤ 𝑅 → 0 ≤ 𝑅))
97	72, 94, 96	mpsyl 68	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ 𝑅)
98	97	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 0 ≤ 𝑅)
99	67, 98	jca 511	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅))
100	50	recnd 11271	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘(𝐾 − 𝑇)) ∈ ℂ)
101	5	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝐶 ∈ ℝ)
102	101, 15	remulcld 11273	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) ∈ ℝ)
103	4	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶))
104		log1 26563	. . . . . . . . 9 ⊢ (log‘1) = 0
105	51	nncnd 12264	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ∈ ℂ)
106	105	mullidd 11261	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (1 · 𝑑) = 𝑑)
107		rpre 13025	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
108	107	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ)
109		fznnfl 13884	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (𝑑 ∈ (1...(⌊‘𝑥)) ↔ (𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝑥)))
110	108, 109	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑑 ∈ (1...(⌊‘𝑥)) ↔ (𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝑥)))
111	110	simplbda 499	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ≤ 𝑥)
112	106, 111	eqbrtrd 5145	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (1 · 𝑑) ≤ 𝑥)
113		1red 11244	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
114	107	ad2antlr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
115	113, 114, 55	lemuldivd 13108	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((1 · 𝑑) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑑)))
116	112, 115	mpbid 232	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 1 ≤ (𝑥 / 𝑑))
117		1rp 13020	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ⁺
118	117	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ⁺)
119	118, 12	logled 26605	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (1 ≤ (𝑥 / 𝑑) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑑))))
120	116, 119	mpbid 232	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (log‘1) ≤ (log‘(𝑥 / 𝑑)))
121	104, 120	eqbrtrrid 5159	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ (log‘(𝑥 / 𝑑)))
122		rpregt0 13031	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
123	122	ad2antlr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
124		divge0 12119	. . . . . . . 8 ⊢ ((((log‘(𝑥 / 𝑑)) ∈ ℝ ∧ 0 ≤ (log‘(𝑥 / 𝑑))) ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → 0 ≤ ((log‘(𝑥 / 𝑑)) / 𝑥))
125	13, 121, 123, 124	syl21anc 837	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((log‘(𝑥 / 𝑑)) / 𝑥))
126		mulge0 11763	. . . . . . 7 ⊢ (((𝐶 ∈ ℝ ∧ 0 ≤ 𝐶) ∧ (((log‘(𝑥 / 𝑑)) / 𝑥) ∈ ℝ ∧ 0 ≤ ((log‘(𝑥 / 𝑑)) / 𝑥))) → 0 ≤ (𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)))
127	103, 15, 125, 126	syl12anc 836	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ (𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)))
128		absidm 15344	. . . . . . . . 9 ⊢ ((𝐾 − 𝑇) ∈ ℂ → (abs‘(abs‘(𝐾 − 𝑇))) = (abs‘(𝐾 − 𝑇)))
129	49, 128	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘(abs‘(𝐾 − 𝑇))) = (abs‘(𝐾 − 𝑇)))
130	129	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (abs‘(abs‘(𝐾 − 𝑇))) = (abs‘(𝐾 − 𝑇)))
131	41	fvoveq1d 7435	. . . . . . . . . 10 ⊢ (𝑚 = (𝑥 / 𝑑) → (abs‘(𝐹 − 𝑇)) = (abs‘(𝐾 − 𝑇)))
132		fveq2 6886	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑥 / 𝑑) → (log‘𝑚) = (log‘(𝑥 / 𝑑)))
133		id 22	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑥 / 𝑑) → 𝑚 = (𝑥 / 𝑑))
134	132, 133	oveq12d 7431	. . . . . . . . . . 11 ⊢ (𝑚 = (𝑥 / 𝑑) → ((log‘𝑚) / 𝑚) = ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)))
135	134	oveq2d 7429	. . . . . . . . . 10 ⊢ (𝑚 = (𝑥 / 𝑑) → (𝐶 · ((log‘𝑚) / 𝑚)) = (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))))
136	131, 135	breq12d 5136	. . . . . . . . 9 ⊢ (𝑚 = (𝑥 / 𝑑) → ((abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)) ↔ (abs‘(𝐾 − 𝑇)) ≤ (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)))))
137		dchrvmasum.1	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → (abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)))
138	137	ralrimiva 3133	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑚 ∈ (3[,)+∞)(abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)))
139	138	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → ∀𝑚 ∈ (3[,)+∞)(abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)))
140		nndivre 12289	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 𝑑 ∈ ℕ) → (𝑥 / 𝑑) ∈ ℝ)
141	108, 9, 140	syl2an 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑑) ∈ ℝ)
142	141	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (𝑥 / 𝑑) ∈ ℝ)
143		simpr 484	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → 3 ≤ (𝑥 / 𝑑))
144		elicopnf 13467	. . . . . . . . . . 11 ⊢ (3 ∈ ℝ → ((𝑥 / 𝑑) ∈ (3[,)+∞) ↔ ((𝑥 / 𝑑) ∈ ℝ ∧ 3 ≤ (𝑥 / 𝑑))))
145	63, 144	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑥 / 𝑑) ∈ (3[,)+∞) ↔ ((𝑥 / 𝑑) ∈ ℝ ∧ 3 ≤ (𝑥 / 𝑑)))
146	142, 143, 145	sylanbrc 583	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (𝑥 / 𝑑) ∈ (3[,)+∞))
147	136, 139, 146	rspcdva 3606	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (abs‘(𝐾 − 𝑇)) ≤ (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))))
148	13	recnd 11271	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑑)) ∈ ℂ)
149		rpcnne0 13035	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
150	149	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
151	55	rpcnne0d 13068	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑑 ∈ ℂ ∧ 𝑑 ≠ 0))
152		divdiv2 11961	. . . . . . . . . . . . 13 ⊢ (((log‘(𝑥 / 𝑑)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ (𝑑 ∈ ℂ ∧ 𝑑 ≠ 0)) → ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)) = (((log‘(𝑥 / 𝑑)) · 𝑑) / 𝑥))
153	148, 150, 151, 152	syl3anc 1372	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)) = (((log‘(𝑥 / 𝑑)) · 𝑑) / 𝑥))
154		div23 11923	. . . . . . . . . . . . 13 ⊢ (((log‘(𝑥 / 𝑑)) ∈ ℂ ∧ 𝑑 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((log‘(𝑥 / 𝑑)) · 𝑑) / 𝑥) = (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑))
155	148, 105, 150, 154	syl3anc 1372	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑑)) · 𝑑) / 𝑥) = (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑))
156	153, 155	eqtrd 2769	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)) = (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑))
157	156	oveq2d 7429	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))) = (𝐶 · (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑)))
158	29	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝐶 ∈ ℂ)
159	15	recnd 11271	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑑)) / 𝑥) ∈ ℂ)
160	158, 159, 105	mulassd 11266	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑) = (𝐶 · (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑)))
161	157, 160	eqtr4d 2772	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))) = ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑))
162	161	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))) = ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑))
163	147, 162	breqtrd 5149	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (abs‘(𝐾 − 𝑇)) ≤ ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑))
164	130, 163	eqbrtrd 5145	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (abs‘(abs‘(𝐾 − 𝑇))) ≤ ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑))
165	129	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (abs‘(abs‘(𝐾 − 𝑇))) = (abs‘(𝐾 − 𝑇)))
166	131	breq1d 5133	. . . . . . . 8 ⊢ (𝑚 = (𝑥 / 𝑑) → ((abs‘(𝐹 − 𝑇)) ≤ 𝑅 ↔ (abs‘(𝐾 − 𝑇)) ≤ 𝑅))
167	91	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → ∀𝑚 ∈ (1[,)3)(abs‘(𝐹 − 𝑇)) ≤ 𝑅)
168	141	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (𝑥 / 𝑑) ∈ ℝ)
169	116	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → 1 ≤ (𝑥 / 𝑑))
170		simpr 484	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (𝑥 / 𝑑) < 3)
171		elico2 13433	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ 3 ∈ ℝ^*) → ((𝑥 / 𝑑) ∈ (1[,)3) ↔ ((𝑥 / 𝑑) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑑) ∧ (𝑥 / 𝑑) < 3)))
172	23, 69, 171	mp2an 692	. . . . . . . . 9 ⊢ ((𝑥 / 𝑑) ∈ (1[,)3) ↔ ((𝑥 / 𝑑) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑑) ∧ (𝑥 / 𝑑) < 3))
173	168, 169, 170, 172	syl3anbrc 1343	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (𝑥 / 𝑑) ∈ (1[,)3))
174	166, 167, 173	rspcdva 3606	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (abs‘(𝐾 − 𝑇)) ≤ 𝑅)
175	165, 174	eqbrtrd 5145	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (abs‘(abs‘(𝐾 − 𝑇))) ≤ 𝑅)
176	8, 66, 99, 100, 102, 127, 164, 175	fsumharmonic 26991	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ≤ (Σ𝑑 ∈ (1...(⌊‘𝑥))(𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))))
177	29	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝐶 ∈ ℂ)
178	7, 177, 159	fsummulc2 15802	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) = Σ𝑑 ∈ (1...(⌊‘𝑥))(𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)))
179	178	oveq1d 7428	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))) = (Σ𝑑 ∈ (1...(⌊‘𝑥))(𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))))
180	176, 179	breqtrrd 5151	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ≤ ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))))
181	40	leabsd 15435	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))) ≤ (abs‘((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1)))))
182	60, 40, 62, 180, 181	letrd 11400	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ≤ (abs‘((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1)))))
183	182	adantrr 717	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ≤ (abs‘((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1)))))
184	1, 39, 40, 54, 183	o1le 15671	1 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ∈ 𝑂(1))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1539 ∈ wcel 2107 ≠ wne 2931 ∀wral 3050 ⊆ wss 3931 class class class wbr 5123 ↦ cmpt 5205 ‘cfv 6541 (class class class)co 7413 ℂcc 11135 ℝcr 11136 0cc0 11137 1c1 11138 + caddc 11140 · cmul 11142 +∞cpnf 11274 ℝ^*cxr 11276 < clt 11277 ≤ cle 11278 − cmin 11474 / cdiv 11902 ℕcn 12248 3c3 12304 ℝ⁺crp 13016 [,)cico 13371 ...cfz 13529 ⌊cfl 13812 abscabs 15255 ⇝_𝑟 crli 15503 𝑂(1)co1 15504 Σcsu 15704 Basecbs 17229 0_gc0g 17455 ℤRHomczrh 21472 ℤ/nℤczn 21475 logclog 26532 DChrcdchr 27212

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5259 ax-sep 5276 ax-nul 5286 ax-pow 5345 ax-pr 5412 ax-un 7737 ax-inf2 9663 ax-cnex 11193 ax-resscn 11194 ax-1cn 11195 ax-icn 11196 ax-addcl 11197 ax-addrcl 11198 ax-mulcl 11199 ax-mulrcl 11200 ax-mulcom 11201 ax-addass 11202 ax-mulass 11203 ax-distr 11204 ax-i2m1 11205 ax-1ne0 11206 ax-1rid 11207 ax-rnegex 11208 ax-rrecex 11209 ax-cnre 11210 ax-pre-lttri 11211 ax-pre-lttrn 11212 ax-pre-ltadd 11213 ax-pre-mulgt0 11214 ax-pre-sup 11215 ax-addf 11216

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3363 df-reu 3364 df-rab 3420 df-v 3465 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-uni 4888 df-int 4927 df-iun 4973 df-iin 4974 df-br 5124 df-opab 5186 df-mpt 5206 df-tr 5240 df-id 5558 df-eprel 5564 df-po 5572 df-so 5573 df-fr 5617 df-se 5618 df-we 5619 df-xp 5671 df-rel 5672 df-cnv 5673 df-co 5674 df-dm 5675 df-rn 5676 df-res 5677 df-ima 5678 df-pred 6301 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-isom 6550 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-of 7679 df-om 7870 df-1st 7996 df-2nd 7997 df-supp 8168 df-frecs 8288 df-wrecs 8319 df-recs 8393 df-rdg 8432 df-1o 8488 df-2o 8489 df-oadd 8492 df-er 8727 df-map 8850 df-pm 8851 df-ixp 8920 df-en 8968 df-dom 8969 df-sdom 8970 df-fin 8971 df-fsupp 9384 df-fi 9433 df-sup 9464 df-inf 9465 df-oi 9532 df-card 9961 df-pnf 11279 df-mnf 11280 df-xr 11281 df-ltxr 11282 df-le 11283 df-sub 11476 df-neg 11477 df-div 11903 df-nn 12249 df-2 12311 df-3 12312 df-4 12313 df-5 12314 df-6 12315 df-7 12316 df-8 12317 df-9 12318 df-n0 12510 df-xnn0 12583 df-z 12597 df-dec 12717 df-uz 12861 df-q 12973 df-rp 13017 df-xneg 13136 df-xadd 13137 df-xmul 13138 df-ioo 13373 df-ioc 13374 df-ico 13375 df-icc 13376 df-fz 13530 df-fzo 13677 df-fl 13814 df-mod 13892 df-seq 14025 df-exp 14085 df-fac 14295 df-bc 14324 df-hash 14352 df-shft 15088 df-cj 15120 df-re 15121 df-im 15122 df-sqrt 15256 df-abs 15257 df-limsup 15489 df-clim 15506 df-rlim 15507 df-o1 15508 df-lo1 15509 df-sum 15705 df-ef 16085 df-e 16086 df-sin 16087 df-cos 16088 df-tan 16089 df-pi 16090 df-dvds 16273 df-struct 17166 df-sets 17183 df-slot 17201 df-ndx 17213 df-base 17230 df-ress 17253 df-plusg 17286 df-mulr 17287 df-starv 17288 df-sca 17289 df-vsca 17290 df-ip 17291 df-tset 17292 df-ple 17293 df-ds 17295 df-unif 17296 df-hom 17297 df-cco 17298 df-rest 17438 df-topn 17439 df-0g 17457 df-gsum 17458 df-topgen 17459 df-pt 17460 df-prds 17463 df-xrs 17518 df-qtop 17523 df-imas 17524 df-xps 17526 df-mre 17600 df-mrc 17601 df-acs 17603 df-mgm 18622 df-sgrp 18701 df-mnd 18717 df-submnd 18766 df-mulg 19055 df-cntz 19304 df-cmn 19768 df-psmet 21318 df-xmet 21319 df-met 21320 df-bl 21321 df-mopn 21322 df-fbas 21323 df-fg 21324 df-cnfld 21327 df-top 22848 df-topon 22865 df-topsp 22887 df-bases 22900 df-cld 22973 df-ntr 22974 df-cls 22975 df-nei 23052 df-lp 23090 df-perf 23091 df-cn 23181 df-cnp 23182 df-haus 23269 df-cmp 23341 df-tx 23516 df-hmeo 23709 df-fil 23800 df-fm 23892 df-flim 23893 df-flf 23894 df-xms 24275 df-ms 24276 df-tms 24277 df-cncf 24840 df-limc 25837 df-dv 25838 df-ulm 26356 df-log 26534 df-cxp 26535 df-atan 26846 df-em 26972

This theorem is referenced by: dchrvmasumlem3 27479

W3C validator