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 27415

Description: Lemma for dchrvmasum 27442. (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 11181	. 2 ⊢ (𝜑 → 1 ∈ ℝ)
2		dchrvmasum.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))
3		elrege0 13421	. . . . . . 7 ⊢ (𝐶 ∈ (0[,)+∞) ↔ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶))
4	2, 3	sylib 218	. . . . . 6 ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶))
5	4	simpld 494	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ ℝ)
6	5	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝐶 ∈ ℝ)
7		fzfid 13944	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (1...(⌊‘𝑥)) ∈ Fin)
8		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ⁺)
9		elfznn 13520	. . . . . . . . 9 ⊢ (𝑑 ∈ (1...(⌊‘𝑥)) → 𝑑 ∈ ℕ)
10	9	nnrpd 12999	. . . . . . . 8 ⊢ (𝑑 ∈ (1...(⌊‘𝑥)) → 𝑑 ∈ ℝ⁺)
11		rpdivcl 12984	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ℝ⁺) → (𝑥 / 𝑑) ∈ ℝ⁺)
12	8, 10, 11	syl2an 596	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑑) ∈ ℝ⁺)
13	12	relogcld 26538	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑑)) ∈ ℝ)
14	8	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ⁺)
15	13, 14	rerpdivcld 13032	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑑)) / 𝑥) ∈ ℝ)
16	7, 15	fsumrecl 15706	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥) ∈ ℝ)
17	6, 16	remulcld 11210	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ∈ ℝ)
18		dchrvmasum.r	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ ℝ)
19		3nn 12266	. . . . . . 7 ⊢ 3 ∈ ℕ
20		nnrp 12969	. . . . . . 7 ⊢ (3 ∈ ℕ → 3 ∈ ℝ⁺)
21		relogcl 26490	. . . . . . 7 ⊢ (3 ∈ ℝ⁺ → (log‘3) ∈ ℝ)
22	19, 20, 21	mp2b 10	. . . . . 6 ⊢ (log‘3) ∈ ℝ
23		1re 11180	. . . . . 6 ⊢ 1 ∈ ℝ
24	22, 23	readdcli 11195	. . . . 5 ⊢ ((log‘3) + 1) ∈ ℝ
25		remulcl 11159	. . . . 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 12965	. . . . 5 ⊢ ℝ⁺ ⊆ ℝ
29	5	recnd 11208	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ ℂ)
30		o1const 15592	. . . . 5 ⊢ ((ℝ⁺ ⊆ ℝ ∧ 𝐶 ∈ ℂ) → (𝑥 ∈ ℝ⁺ ↦ 𝐶) ∈ 𝑂(1))
31	28, 29, 30	sylancr 587	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ 𝐶) ∈ 𝑂(1))
32		logfacrlim2 27143	. . . . 5 ⊢ (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ⇝_𝑟 1
33		rlimo1 15589	. . . . 5 ⊢ ((𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ⇝_𝑟 1 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ∈ 𝑂(1))
34	32, 33	mp1i 13	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ∈ 𝑂(1))
35	6, 16, 31, 34	o1mul2 15597	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥))) ∈ 𝑂(1))
36	26	recnd 11208	. . . 4 ⊢ (𝜑 → (𝑅 · ((log‘3) + 1)) ∈ ℂ)
37		o1const 15592	. . . 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 15596	. 2 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1)))) ∈ 𝑂(1))
40	17, 27	readdcld 11209	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))) ∈ ℝ)
41		dchrvmasum.g	. . . . . . . . 9 ⊢ (𝑚 = (𝑥 / 𝑑) → 𝐹 = 𝐾)
42	41	eleq1d 2814	. . . . . . . 8 ⊢ (𝑚 = (𝑥 / 𝑑) → (𝐹 ∈ ℂ ↔ 𝐾 ∈ ℂ))
43		dchrvmasum.f	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → 𝐹 ∈ ℂ)
44	43	ralrimiva 3126	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑚 ∈ ℝ⁺ 𝐹 ∈ ℂ)
45	44	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ∀𝑚 ∈ ℝ⁺ 𝐹 ∈ ℂ)
46	42, 45, 12	rspcdva 3592	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝐾 ∈ ℂ)
47		dchrvmasum.t	. . . . . . . 8 ⊢ (𝜑 → 𝑇 ∈ ℂ)
48	47	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑇 ∈ ℂ)
49	46, 48	subcld 11539	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐾 − 𝑇) ∈ ℂ)
50	49	abscld 15411	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘(𝐾 − 𝑇)) ∈ ℝ)
51	9	adantl 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ∈ ℕ)
52	50, 51	nndivred 12241	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℝ)
53	7, 52	fsumrecl 15706	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℝ)
54	53	recnd 11208	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℂ)
55	51	nnrpd 12999	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ∈ ℝ⁺)
56	49	absge0d 15419	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘(𝐾 − 𝑇)))
57	50, 55, 56	divge0d 13041	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((abs‘(𝐾 − 𝑇)) / 𝑑))
58	7, 52, 57	fsumge0 15767	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 0 ≤ Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑))
59	53, 58	absidd 15395	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) = Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑))
60	59, 53	eqeltrd 2829	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ∈ ℝ)
61	40	recnd 11208	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))) ∈ ℂ)
62	61	abscld 15411	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1)))) ∈ ℝ)
63		3re 12267	. . . . . . . 8 ⊢ 3 ∈ ℝ
64	63	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 3 ∈ ℝ)
65		1le3 12399	. . . . . . 7 ⊢ 1 ≤ 3
66	64, 65	jctir 520	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (3 ∈ ℝ ∧ 1 ≤ 3))
67	18	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑅 ∈ ℝ)
68	23	rexri 11238	. . . . . . . . . 10 ⊢ 1 ∈ ℝ^*
69	63	rexri 11238	. . . . . . . . . 10 ⊢ 3 ∈ ℝ^*
70		1lt3 12360	. . . . . . . . . 10 ⊢ 1 < 3
71		lbico1 13367	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ^* ∧ 3 ∈ ℝ^* ∧ 1 < 3) → 1 ∈ (1[,)3))
72	68, 69, 70, 71	mp3an 1463	. . . . . . . . 9 ⊢ 1 ∈ (1[,)3)
73		0red 11183	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 0 ∈ ℝ)
74		elico2 13377	. . . . . . . . . . . . . . 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 11183	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1[,)3) → 0 ∈ ℝ)
78		1red 11181	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1[,)3) → 1 ∈ ℝ)
79		0lt1 11706	. . . . . . . . . . . . . . 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 11340	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (1[,)3) → 0 < 𝑚)
83	76, 82	elrpd 12998	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (1[,)3) → 𝑚 ∈ ℝ⁺)
84	47	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → 𝑇 ∈ ℂ)
85	43, 84	subcld 11539	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → (𝐹 − 𝑇) ∈ ℂ)
86	85	abscld 15411	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → (abs‘(𝐹 − 𝑇)) ∈ ℝ)
87	83, 86	sylan2 593	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (abs‘(𝐹 − 𝑇)) ∈ ℝ)
88	18	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 𝑅 ∈ ℝ)
89	85	absge0d 15419	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → 0 ≤ (abs‘(𝐹 − 𝑇)))
90	83, 89	sylan2 593	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 0 ≤ (abs‘(𝐹 − 𝑇)))
91		dchrvmasum.2	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑚 ∈ (1[,)3)(abs‘(𝐹 − 𝑇)) ≤ 𝑅)
92	91	r19.21bi 3230	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (abs‘(𝐹 − 𝑇)) ≤ 𝑅)
93	73, 87, 88, 90, 92	letrd 11337	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 0 ≤ 𝑅)
94	93	ralrimiva 3126	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑚 ∈ (1[,)3)0 ≤ 𝑅)
95		biidd 262	. . . . . . . . . 10 ⊢ (𝑚 = 1 → (0 ≤ 𝑅 ↔ 0 ≤ 𝑅))
96	95	rspcv 3587	. . . . . . . . 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 11208	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘(𝐾 − 𝑇)) ∈ ℂ)
101	5	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝐶 ∈ ℝ)
102	101, 15	remulcld 11210	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) ∈ ℝ)
103	4	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶))
104		log1 26500	. . . . . . . . 9 ⊢ (log‘1) = 0
105	51	nncnd 12203	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ∈ ℂ)
106	105	mullidd 11198	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (1 · 𝑑) = 𝑑)
107		rpre 12966	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
108	107	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ)
109		fznnfl 13830	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (𝑑 ∈ (1...(⌊‘𝑥)) ↔ (𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝑥)))
110	108, 109	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑑 ∈ (1...(⌊‘𝑥)) ↔ (𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝑥)))
111	110	simplbda 499	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ≤ 𝑥)
112	106, 111	eqbrtrd 5131	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (1 · 𝑑) ≤ 𝑥)
113		1red 11181	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
114	107	ad2antlr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
115	113, 114, 55	lemuldivd 13050	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((1 · 𝑑) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑑)))
116	112, 115	mpbid 232	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 1 ≤ (𝑥 / 𝑑))
117		1rp 12961	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ⁺
118	117	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ⁺)
119	118, 12	logled 26542	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (1 ≤ (𝑥 / 𝑑) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑑))))
120	116, 119	mpbid 232	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (log‘1) ≤ (log‘(𝑥 / 𝑑)))
121	104, 120	eqbrtrrid 5145	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ (log‘(𝑥 / 𝑑)))
122		rpregt0 12972	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
123	122	ad2antlr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
124		divge0 12058	. . . . . . . 8 ⊢ ((((log‘(𝑥 / 𝑑)) ∈ ℝ ∧ 0 ≤ (log‘(𝑥 / 𝑑))) ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → 0 ≤ ((log‘(𝑥 / 𝑑)) / 𝑥))
125	13, 121, 123, 124	syl21anc 837	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((log‘(𝑥 / 𝑑)) / 𝑥))
126		mulge0 11702	. . . . . . 7 ⊢ (((𝐶 ∈ ℝ ∧ 0 ≤ 𝐶) ∧ (((log‘(𝑥 / 𝑑)) / 𝑥) ∈ ℝ ∧ 0 ≤ ((log‘(𝑥 / 𝑑)) / 𝑥))) → 0 ≤ (𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)))
127	103, 15, 125, 126	syl12anc 836	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ (𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)))
128		absidm 15296	. . . . . . . . 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 7411	. . . . . . . . . 10 ⊢ (𝑚 = (𝑥 / 𝑑) → (abs‘(𝐹 − 𝑇)) = (abs‘(𝐾 − 𝑇)))
132		fveq2 6860	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑥 / 𝑑) → (log‘𝑚) = (log‘(𝑥 / 𝑑)))
133		id 22	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑥 / 𝑑) → 𝑚 = (𝑥 / 𝑑))
134	132, 133	oveq12d 7407	. . . . . . . . . . 11 ⊢ (𝑚 = (𝑥 / 𝑑) → ((log‘𝑚) / 𝑚) = ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)))
135	134	oveq2d 7405	. . . . . . . . . 10 ⊢ (𝑚 = (𝑥 / 𝑑) → (𝐶 · ((log‘𝑚) / 𝑚)) = (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))))
136	131, 135	breq12d 5122	. . . . . . . . 9 ⊢ (𝑚 = (𝑥 / 𝑑) → ((abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)) ↔ (abs‘(𝐾 − 𝑇)) ≤ (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)))))
137		dchrvmasum.1	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → (abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)))
138	137	ralrimiva 3126	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑚 ∈ (3[,)+∞)(abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)))
139	138	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → ∀𝑚 ∈ (3[,)+∞)(abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)))
140		nndivre 12228	. . . . . . . . . . . 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 13412	. . . . . . . . . . 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 3592	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (abs‘(𝐾 − 𝑇)) ≤ (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))))
148	13	recnd 11208	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑑)) ∈ ℂ)
149		rpcnne0 12976	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
150	149	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
151	55	rpcnne0d 13010	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑑 ∈ ℂ ∧ 𝑑 ≠ 0))
152		divdiv2 11900	. . . . . . . . . . . . 13 ⊢ (((log‘(𝑥 / 𝑑)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ (𝑑 ∈ ℂ ∧ 𝑑 ≠ 0)) → ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)) = (((log‘(𝑥 / 𝑑)) · 𝑑) / 𝑥))
153	148, 150, 151, 152	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)) = (((log‘(𝑥 / 𝑑)) · 𝑑) / 𝑥))
154		div23 11862	. . . . . . . . . . . . 13 ⊢ (((log‘(𝑥 / 𝑑)) ∈ ℂ ∧ 𝑑 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((log‘(𝑥 / 𝑑)) · 𝑑) / 𝑥) = (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑))
155	148, 105, 150, 154	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑑)) · 𝑑) / 𝑥) = (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑))
156	153, 155	eqtrd 2765	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)) = (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑))
157	156	oveq2d 7405	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))) = (𝐶 · (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑)))
158	29	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝐶 ∈ ℂ)
159	15	recnd 11208	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑑)) / 𝑥) ∈ ℂ)
160	158, 159, 105	mulassd 11203	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑) = (𝐶 · (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑)))
161	157, 160	eqtr4d 2768	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))) = ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑))
162	161	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))) = ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑))
163	147, 162	breqtrd 5135	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (abs‘(𝐾 − 𝑇)) ≤ ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑))
164	130, 163	eqbrtrd 5131	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (abs‘(abs‘(𝐾 − 𝑇))) ≤ ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑))
165	129	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (abs‘(abs‘(𝐾 − 𝑇))) = (abs‘(𝐾 − 𝑇)))
166	131	breq1d 5119	. . . . . . . 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 13377	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ 3 ∈ ℝ^*) → ((𝑥 / 𝑑) ∈ (1[,)3) ↔ ((𝑥 / 𝑑) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑑) ∧ (𝑥 / 𝑑) < 3)))
172	23, 69, 171	mp2an 692	. . . . . . . . 9 ⊢ ((𝑥 / 𝑑) ∈ (1[,)3) ↔ ((𝑥 / 𝑑) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑑) ∧ (𝑥 / 𝑑) < 3))
173	168, 169, 170, 172	syl3anbrc 1344	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (𝑥 / 𝑑) ∈ (1[,)3))
174	166, 167, 173	rspcdva 3592	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (abs‘(𝐾 − 𝑇)) ≤ 𝑅)
175	165, 174	eqbrtrd 5131	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (abs‘(abs‘(𝐾 − 𝑇))) ≤ 𝑅)
176	8, 66, 99, 100, 102, 127, 164, 175	fsumharmonic 26928	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ≤ (Σ𝑑 ∈ (1...(⌊‘𝑥))(𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))))
177	29	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝐶 ∈ ℂ)
178	7, 177, 159	fsummulc2 15756	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) = Σ𝑑 ∈ (1...(⌊‘𝑥))(𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)))
179	178	oveq1d 7404	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))) = (Σ𝑑 ∈ (1...(⌊‘𝑥))(𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))))
180	176, 179	breqtrrd 5137	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ≤ ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))))
181	40	leabsd 15387	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))) ≤ (abs‘((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1)))))
182	60, 40, 62, 180, 181	letrd 11337	. . 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 15625	1 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ∈ 𝑂(1))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2926 ∀wral 3045 ⊆ wss 3916 class class class wbr 5109 ↦ cmpt 5190 ‘cfv 6513 (class class class)co 7389 ℂcc 11072 ℝcr 11073 0cc0 11074 1c1 11075 + caddc 11077 · cmul 11079 +∞cpnf 11211 ℝ^*cxr 11213 < clt 11214 ≤ cle 11215 − cmin 11411 / cdiv 11841 ℕcn 12187 3c3 12243 ℝ⁺crp 12957 [,)cico 13314 ...cfz 13474 ⌊cfl 13758 abscabs 15206 ⇝_𝑟 crli 15457 𝑂(1)co1 15458 Σcsu 15658 Basecbs 17185 0_gc0g 17408 ℤRHomczrh 21415 ℤ/nℤczn 21418 logclog 26469 DChrcdchr 27149

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-rep 5236 ax-sep 5253 ax-nul 5263 ax-pow 5322 ax-pr 5389 ax-un 7713 ax-inf2 9600 ax-cnex 11130 ax-resscn 11131 ax-1cn 11132 ax-icn 11133 ax-addcl 11134 ax-addrcl 11135 ax-mulcl 11136 ax-mulrcl 11137 ax-mulcom 11138 ax-addass 11139 ax-mulass 11140 ax-distr 11141 ax-i2m1 11142 ax-1ne0 11143 ax-1rid 11144 ax-rnegex 11145 ax-rrecex 11146 ax-cnre 11147 ax-pre-lttri 11148 ax-pre-lttrn 11149 ax-pre-ltadd 11150 ax-pre-mulgt0 11151 ax-pre-sup 11152 ax-addf 11153

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3356 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3756 df-csb 3865 df-dif 3919 df-un 3921 df-in 3923 df-ss 3933 df-pss 3936 df-nul 4299 df-if 4491 df-pw 4567 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4874 df-int 4913 df-iun 4959 df-iin 4960 df-br 5110 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5535 df-eprel 5540 df-po 5548 df-so 5549 df-fr 5593 df-se 5594 df-we 5595 df-xp 5646 df-rel 5647 df-cnv 5648 df-co 5649 df-dm 5650 df-rn 5651 df-res 5652 df-ima 5653 df-pred 6276 df-ord 6337 df-on 6338 df-lim 6339 df-suc 6340 df-iota 6466 df-fun 6515 df-fn 6516 df-f 6517 df-f1 6518 df-fo 6519 df-f1o 6520 df-fv 6521 df-isom 6522 df-riota 7346 df-ov 7392 df-oprab 7393 df-mpo 7394 df-of 7655 df-om 7845 df-1st 7970 df-2nd 7971 df-supp 8142 df-frecs 8262 df-wrecs 8293 df-recs 8342 df-rdg 8380 df-1o 8436 df-2o 8437 df-oadd 8440 df-er 8673 df-map 8803 df-pm 8804 df-ixp 8873 df-en 8921 df-dom 8922 df-sdom 8923 df-fin 8924 df-fsupp 9319 df-fi 9368 df-sup 9399 df-inf 9400 df-oi 9469 df-card 9898 df-pnf 11216 df-mnf 11217 df-xr 11218 df-ltxr 11219 df-le 11220 df-sub 11413 df-neg 11414 df-div 11842 df-nn 12188 df-2 12250 df-3 12251 df-4 12252 df-5 12253 df-6 12254 df-7 12255 df-8 12256 df-9 12257 df-n0 12449 df-xnn0 12522 df-z 12536 df-dec 12656 df-uz 12800 df-q 12914 df-rp 12958 df-xneg 13078 df-xadd 13079 df-xmul 13080 df-ioo 13316 df-ioc 13317 df-ico 13318 df-icc 13319 df-fz 13475 df-fzo 13622 df-fl 13760 df-mod 13838 df-seq 13973 df-exp 14033 df-fac 14245 df-bc 14274 df-hash 14302 df-shft 15039 df-cj 15071 df-re 15072 df-im 15073 df-sqrt 15207 df-abs 15208 df-limsup 15443 df-clim 15460 df-rlim 15461 df-o1 15462 df-lo1 15463 df-sum 15659 df-ef 16039 df-e 16040 df-sin 16041 df-cos 16042 df-tan 16043 df-pi 16044 df-dvds 16229 df-struct 17123 df-sets 17140 df-slot 17158 df-ndx 17170 df-base 17186 df-ress 17207 df-plusg 17239 df-mulr 17240 df-starv 17241 df-sca 17242 df-vsca 17243 df-ip 17244 df-tset 17245 df-ple 17246 df-ds 17248 df-unif 17249 df-hom 17250 df-cco 17251 df-rest 17391 df-topn 17392 df-0g 17410 df-gsum 17411 df-topgen 17412 df-pt 17413 df-prds 17416 df-xrs 17471 df-qtop 17476 df-imas 17477 df-xps 17479 df-mre 17553 df-mrc 17554 df-acs 17556 df-mgm 18573 df-sgrp 18652 df-mnd 18668 df-submnd 18717 df-mulg 19006 df-cntz 19255 df-cmn 19718 df-psmet 21262 df-xmet 21263 df-met 21264 df-bl 21265 df-mopn 21266 df-fbas 21267 df-fg 21268 df-cnfld 21271 df-top 22787 df-topon 22804 df-topsp 22826 df-bases 22839 df-cld 22912 df-ntr 22913 df-cls 22914 df-nei 22991 df-lp 23029 df-perf 23030 df-cn 23120 df-cnp 23121 df-haus 23208 df-cmp 23280 df-tx 23455 df-hmeo 23648 df-fil 23739 df-fm 23831 df-flim 23832 df-flf 23833 df-xms 24214 df-ms 24215 df-tms 24216 df-cncf 24777 df-limc 25773 df-dv 25774 df-ulm 26292 df-log 26471 df-cxp 26472 df-atan 26783 df-em 26909

This theorem is referenced by: dchrvmasumlem3 27416

W3C validator