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 26068

Description: Lemma for dchrvmasum 26095. (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 10636	. 2 ⊢ (𝜑 → 1 ∈ ℝ)
2		dchrvmasum.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))
3		elrege0 12836	. . . . . . 7 ⊢ (𝐶 ∈ (0[,)+∞) ↔ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶))
4	2, 3	sylib 220	. . . . . 6 ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶))
5	4	simpld 497	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ ℝ)
6	5	adantr 483	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝐶 ∈ ℝ)
7		fzfid 13335	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (1...(⌊‘𝑥)) ∈ Fin)
8		simpr 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ⁺)
9		elfznn 12930	. . . . . . . . 9 ⊢ (𝑑 ∈ (1...(⌊‘𝑥)) → 𝑑 ∈ ℕ)
10	9	nnrpd 12423	. . . . . . . 8 ⊢ (𝑑 ∈ (1...(⌊‘𝑥)) → 𝑑 ∈ ℝ⁺)
11		rpdivcl 12408	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ℝ⁺) → (𝑥 / 𝑑) ∈ ℝ⁺)
12	8, 10, 11	syl2an 597	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑑) ∈ ℝ⁺)
13	12	relogcld 25200	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑑)) ∈ ℝ)
14	8	adantr 483	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ⁺)
15	13, 14	rerpdivcld 12456	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑑)) / 𝑥) ∈ ℝ)
16	7, 15	fsumrecl 15085	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥) ∈ ℝ)
17	6, 16	remulcld 10665	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ∈ ℝ)
18		dchrvmasum.r	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ ℝ)
19		3nn 11710	. . . . . . 7 ⊢ 3 ∈ ℕ
20		nnrp 12394	. . . . . . 7 ⊢ (3 ∈ ℕ → 3 ∈ ℝ⁺)
21		relogcl 25153	. . . . . . 7 ⊢ (3 ∈ ℝ⁺ → (log‘3) ∈ ℝ)
22	19, 20, 21	mp2b 10	. . . . . 6 ⊢ (log‘3) ∈ ℝ
23		1re 10635	. . . . . 6 ⊢ 1 ∈ ℝ
24	22, 23	readdcli 10650	. . . . 5 ⊢ ((log‘3) + 1) ∈ ℝ
25		remulcl 10616	. . . . 5 ⊢ ((𝑅 ∈ ℝ ∧ ((log‘3) + 1) ∈ ℝ) → (𝑅 · ((log‘3) + 1)) ∈ ℝ)
26	18, 24, 25	sylancl 588	. . . 4 ⊢ (𝜑 → (𝑅 · ((log‘3) + 1)) ∈ ℝ)
27	26	adantr 483	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑅 · ((log‘3) + 1)) ∈ ℝ)
28		rpssre 12390	. . . . 5 ⊢ ℝ⁺ ⊆ ℝ
29	5	recnd 10663	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ ℂ)
30		o1const 14970	. . . . 5 ⊢ ((ℝ⁺ ⊆ ℝ ∧ 𝐶 ∈ ℂ) → (𝑥 ∈ ℝ⁺ ↦ 𝐶) ∈ 𝑂(1))
31	28, 29, 30	sylancr 589	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ 𝐶) ∈ 𝑂(1))
32		logfacrlim2 25796	. . . . 5 ⊢ (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ⇝_𝑟 1
33		rlimo1 14967	. . . . 5 ⊢ ((𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ⇝_𝑟 1 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ∈ 𝑂(1))
34	32, 33	mp1i 13	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ∈ 𝑂(1))
35	6, 16, 31, 34	o1mul2 14975	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥))) ∈ 𝑂(1))
36	26	recnd 10663	. . . 4 ⊢ (𝜑 → (𝑅 · ((log‘3) + 1)) ∈ ℂ)
37		o1const 14970	. . . 4 ⊢ ((ℝ⁺ ⊆ ℝ ∧ (𝑅 · ((log‘3) + 1)) ∈ ℂ) → (𝑥 ∈ ℝ⁺ ↦ (𝑅 · ((log‘3) + 1))) ∈ 𝑂(1))
38	28, 36, 37	sylancr 589	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (𝑅 · ((log‘3) + 1))) ∈ 𝑂(1))
39	17, 27, 35, 38	o1add2 14974	. 2 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1)))) ∈ 𝑂(1))
40	17, 27	readdcld 10664	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))) ∈ ℝ)
41		dchrvmasum.g	. . . . . . . . 9 ⊢ (𝑚 = (𝑥 / 𝑑) → 𝐹 = 𝐾)
42	41	eleq1d 2897	. . . . . . . 8 ⊢ (𝑚 = (𝑥 / 𝑑) → (𝐹 ∈ ℂ ↔ 𝐾 ∈ ℂ))
43		dchrvmasum.f	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → 𝐹 ∈ ℂ)
44	43	ralrimiva 3182	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑚 ∈ ℝ⁺ 𝐹 ∈ ℂ)
45	44	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ∀𝑚 ∈ ℝ⁺ 𝐹 ∈ ℂ)
46	42, 45, 12	rspcdva 3624	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝐾 ∈ ℂ)
47		dchrvmasum.t	. . . . . . . 8 ⊢ (𝜑 → 𝑇 ∈ ℂ)
48	47	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑇 ∈ ℂ)
49	46, 48	subcld 10991	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐾 − 𝑇) ∈ ℂ)
50	49	abscld 14790	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘(𝐾 − 𝑇)) ∈ ℝ)
51	9	adantl 484	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ∈ ℕ)
52	50, 51	nndivred 11685	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℝ)
53	7, 52	fsumrecl 15085	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℝ)
54	53	recnd 10663	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℂ)
55	51	nnrpd 12423	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ∈ ℝ⁺)
56	49	absge0d 14798	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘(𝐾 − 𝑇)))
57	50, 55, 56	divge0d 12465	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((abs‘(𝐾 − 𝑇)) / 𝑑))
58	7, 52, 57	fsumge0 15144	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 0 ≤ Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑))
59	53, 58	absidd 14776	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) = Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑))
60	59, 53	eqeltrd 2913	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ∈ ℝ)
61	40	recnd 10663	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))) ∈ ℂ)
62	61	abscld 14790	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1)))) ∈ ℝ)
63		3re 11711	. . . . . . . 8 ⊢ 3 ∈ ℝ
64	63	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 3 ∈ ℝ)
65		1le3 11843	. . . . . . 7 ⊢ 1 ≤ 3
66	64, 65	jctir 523	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (3 ∈ ℝ ∧ 1 ≤ 3))
67	18	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑅 ∈ ℝ)
68	23	rexri 10693	. . . . . . . . . 10 ⊢ 1 ∈ ℝ^*
69	63	rexri 10693	. . . . . . . . . 10 ⊢ 3 ∈ ℝ^*
70		1lt3 11804	. . . . . . . . . 10 ⊢ 1 < 3
71		lbico1 12785	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ^* ∧ 3 ∈ ℝ^* ∧ 1 < 3) → 1 ∈ (1[,)3))
72	68, 69, 70, 71	mp3an 1457	. . . . . . . . 9 ⊢ 1 ∈ (1[,)3)
73		0red 10638	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 0 ∈ ℝ)
74		elico2 12794	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℝ ∧ 3 ∈ ℝ^*) → (𝑚 ∈ (1[,)3) ↔ (𝑚 ∈ ℝ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 3)))
75	23, 69, 74	mp2an 690	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1[,)3) ↔ (𝑚 ∈ ℝ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 3))
76	75	simp1bi 1141	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (1[,)3) → 𝑚 ∈ ℝ)
77		0red 10638	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1[,)3) → 0 ∈ ℝ)
78		1red 10636	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1[,)3) → 1 ∈ ℝ)
79		0lt1 11156	. . . . . . . . . . . . . . 15 ⊢ 0 < 1
80	79	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1[,)3) → 0 < 1)
81	75	simp2bi 1142	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1[,)3) → 1 ≤ 𝑚)
82	77, 78, 76, 80, 81	ltletrd 10794	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (1[,)3) → 0 < 𝑚)
83	76, 82	elrpd 12422	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (1[,)3) → 𝑚 ∈ ℝ⁺)
84	47	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → 𝑇 ∈ ℂ)
85	43, 84	subcld 10991	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → (𝐹 − 𝑇) ∈ ℂ)
86	85	abscld 14790	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → (abs‘(𝐹 − 𝑇)) ∈ ℝ)
87	83, 86	sylan2 594	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (abs‘(𝐹 − 𝑇)) ∈ ℝ)
88	18	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 𝑅 ∈ ℝ)
89	85	absge0d 14798	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → 0 ≤ (abs‘(𝐹 − 𝑇)))
90	83, 89	sylan2 594	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 0 ≤ (abs‘(𝐹 − 𝑇)))
91		dchrvmasum.2	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑚 ∈ (1[,)3)(abs‘(𝐹 − 𝑇)) ≤ 𝑅)
92	91	r19.21bi 3208	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (abs‘(𝐹 − 𝑇)) ≤ 𝑅)
93	73, 87, 88, 90, 92	letrd 10791	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 0 ≤ 𝑅)
94	93	ralrimiva 3182	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑚 ∈ (1[,)3)0 ≤ 𝑅)
95		biidd 264	. . . . . . . . . 10 ⊢ (𝑚 = 1 → (0 ≤ 𝑅 ↔ 0 ≤ 𝑅))
96	95	rspcv 3617	. . . . . . . . 9 ⊢ (1 ∈ (1[,)3) → (∀𝑚 ∈ (1[,)3)0 ≤ 𝑅 → 0 ≤ 𝑅))
97	72, 94, 96	mpsyl 68	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ 𝑅)
98	97	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 0 ≤ 𝑅)
99	67, 98	jca 514	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅))
100	50	recnd 10663	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘(𝐾 − 𝑇)) ∈ ℂ)
101	5	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝐶 ∈ ℝ)
102	101, 15	remulcld 10665	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) ∈ ℝ)
103	4	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶))
104		log1 25163	. . . . . . . . 9 ⊢ (log‘1) = 0
105	51	nncnd 11648	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ∈ ℂ)
106	105	mulid2d 10653	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (1 · 𝑑) = 𝑑)
107		rpre 12391	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
108	107	adantl 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ)
109		fznnfl 13224	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (𝑑 ∈ (1...(⌊‘𝑥)) ↔ (𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝑥)))
110	108, 109	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑑 ∈ (1...(⌊‘𝑥)) ↔ (𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝑥)))
111	110	simplbda 502	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ≤ 𝑥)
112	106, 111	eqbrtrd 5080	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (1 · 𝑑) ≤ 𝑥)
113		1red 10636	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
114	107	ad2antlr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
115	113, 114, 55	lemuldivd 12474	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((1 · 𝑑) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑑)))
116	112, 115	mpbid 234	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 1 ≤ (𝑥 / 𝑑))
117		1rp 12387	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ⁺
118	117	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ⁺)
119	118, 12	logled 25204	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (1 ≤ (𝑥 / 𝑑) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑑))))
120	116, 119	mpbid 234	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (log‘1) ≤ (log‘(𝑥 / 𝑑)))
121	104, 120	eqbrtrrid 5094	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ (log‘(𝑥 / 𝑑)))
122		rpregt0 12397	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
123	122	ad2antlr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
124		divge0 11503	. . . . . . . 8 ⊢ ((((log‘(𝑥 / 𝑑)) ∈ ℝ ∧ 0 ≤ (log‘(𝑥 / 𝑑))) ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → 0 ≤ ((log‘(𝑥 / 𝑑)) / 𝑥))
125	13, 121, 123, 124	syl21anc 835	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((log‘(𝑥 / 𝑑)) / 𝑥))
126		mulge0 11152	. . . . . . 7 ⊢ (((𝐶 ∈ ℝ ∧ 0 ≤ 𝐶) ∧ (((log‘(𝑥 / 𝑑)) / 𝑥) ∈ ℝ ∧ 0 ≤ ((log‘(𝑥 / 𝑑)) / 𝑥))) → 0 ≤ (𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)))
127	103, 15, 125, 126	syl12anc 834	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ (𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)))
128		absidm 14677	. . . . . . . . 9 ⊢ ((𝐾 − 𝑇) ∈ ℂ → (abs‘(abs‘(𝐾 − 𝑇))) = (abs‘(𝐾 − 𝑇)))
129	49, 128	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘(abs‘(𝐾 − 𝑇))) = (abs‘(𝐾 − 𝑇)))
130	129	adantr 483	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (abs‘(abs‘(𝐾 − 𝑇))) = (abs‘(𝐾 − 𝑇)))
131	41	fvoveq1d 7172	. . . . . . . . . 10 ⊢ (𝑚 = (𝑥 / 𝑑) → (abs‘(𝐹 − 𝑇)) = (abs‘(𝐾 − 𝑇)))
132		fveq2 6664	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑥 / 𝑑) → (log‘𝑚) = (log‘(𝑥 / 𝑑)))
133		id 22	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑥 / 𝑑) → 𝑚 = (𝑥 / 𝑑))
134	132, 133	oveq12d 7168	. . . . . . . . . . 11 ⊢ (𝑚 = (𝑥 / 𝑑) → ((log‘𝑚) / 𝑚) = ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)))
135	134	oveq2d 7166	. . . . . . . . . 10 ⊢ (𝑚 = (𝑥 / 𝑑) → (𝐶 · ((log‘𝑚) / 𝑚)) = (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))))
136	131, 135	breq12d 5071	. . . . . . . . 9 ⊢ (𝑚 = (𝑥 / 𝑑) → ((abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)) ↔ (abs‘(𝐾 − 𝑇)) ≤ (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)))))
137		dchrvmasum.1	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → (abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)))
138	137	ralrimiva 3182	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑚 ∈ (3[,)+∞)(abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)))
139	138	ad3antrrr 728	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → ∀𝑚 ∈ (3[,)+∞)(abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)))
140		nndivre 11672	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 𝑑 ∈ ℕ) → (𝑥 / 𝑑) ∈ ℝ)
141	108, 9, 140	syl2an 597	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑑) ∈ ℝ)
142	141	adantr 483	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (𝑥 / 𝑑) ∈ ℝ)
143		simpr 487	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → 3 ≤ (𝑥 / 𝑑))
144		elicopnf 12827	. . . . . . . . . . 11 ⊢ (3 ∈ ℝ → ((𝑥 / 𝑑) ∈ (3[,)+∞) ↔ ((𝑥 / 𝑑) ∈ ℝ ∧ 3 ≤ (𝑥 / 𝑑))))
145	63, 144	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑥 / 𝑑) ∈ (3[,)+∞) ↔ ((𝑥 / 𝑑) ∈ ℝ ∧ 3 ≤ (𝑥 / 𝑑)))
146	142, 143, 145	sylanbrc 585	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (𝑥 / 𝑑) ∈ (3[,)+∞))
147	136, 139, 146	rspcdva 3624	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (abs‘(𝐾 − 𝑇)) ≤ (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))))
148	13	recnd 10663	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑑)) ∈ ℂ)
149		rpcnne0 12401	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
150	149	ad2antlr 725	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
151	55	rpcnne0d 12434	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑑 ∈ ℂ ∧ 𝑑 ≠ 0))
152		divdiv2 11346	. . . . . . . . . . . . 13 ⊢ (((log‘(𝑥 / 𝑑)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ (𝑑 ∈ ℂ ∧ 𝑑 ≠ 0)) → ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)) = (((log‘(𝑥 / 𝑑)) · 𝑑) / 𝑥))
153	148, 150, 151, 152	syl3anc 1367	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)) = (((log‘(𝑥 / 𝑑)) · 𝑑) / 𝑥))
154		div23 11311	. . . . . . . . . . . . 13 ⊢ (((log‘(𝑥 / 𝑑)) ∈ ℂ ∧ 𝑑 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((log‘(𝑥 / 𝑑)) · 𝑑) / 𝑥) = (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑))
155	148, 105, 150, 154	syl3anc 1367	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑑)) · 𝑑) / 𝑥) = (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑))
156	153, 155	eqtrd 2856	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)) = (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑))
157	156	oveq2d 7166	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))) = (𝐶 · (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑)))
158	29	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝐶 ∈ ℂ)
159	15	recnd 10663	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑑)) / 𝑥) ∈ ℂ)
160	158, 159, 105	mulassd 10658	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑) = (𝐶 · (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑)))
161	157, 160	eqtr4d 2859	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))) = ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑))
162	161	adantr 483	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))) = ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑))
163	147, 162	breqtrd 5084	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (abs‘(𝐾 − 𝑇)) ≤ ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑))
164	130, 163	eqbrtrd 5080	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (abs‘(abs‘(𝐾 − 𝑇))) ≤ ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑))
165	129	adantr 483	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (abs‘(abs‘(𝐾 − 𝑇))) = (abs‘(𝐾 − 𝑇)))
166	131	breq1d 5068	. . . . . . . 8 ⊢ (𝑚 = (𝑥 / 𝑑) → ((abs‘(𝐹 − 𝑇)) ≤ 𝑅 ↔ (abs‘(𝐾 − 𝑇)) ≤ 𝑅))
167	91	ad3antrrr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → ∀𝑚 ∈ (1[,)3)(abs‘(𝐹 − 𝑇)) ≤ 𝑅)
168	141	adantr 483	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (𝑥 / 𝑑) ∈ ℝ)
169	116	adantr 483	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → 1 ≤ (𝑥 / 𝑑))
170		simpr 487	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (𝑥 / 𝑑) < 3)
171		elico2 12794	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ 3 ∈ ℝ^*) → ((𝑥 / 𝑑) ∈ (1[,)3) ↔ ((𝑥 / 𝑑) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑑) ∧ (𝑥 / 𝑑) < 3)))
172	23, 69, 171	mp2an 690	. . . . . . . . 9 ⊢ ((𝑥 / 𝑑) ∈ (1[,)3) ↔ ((𝑥 / 𝑑) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑑) ∧ (𝑥 / 𝑑) < 3))
173	168, 169, 170, 172	syl3anbrc 1339	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (𝑥 / 𝑑) ∈ (1[,)3))
174	166, 167, 173	rspcdva 3624	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (abs‘(𝐾 − 𝑇)) ≤ 𝑅)
175	165, 174	eqbrtrd 5080	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (abs‘(abs‘(𝐾 − 𝑇))) ≤ 𝑅)
176	8, 66, 99, 100, 102, 127, 164, 175	fsumharmonic 25583	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ≤ (Σ𝑑 ∈ (1...(⌊‘𝑥))(𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))))
177	29	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝐶 ∈ ℂ)
178	7, 177, 159	fsummulc2 15133	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) = Σ𝑑 ∈ (1...(⌊‘𝑥))(𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)))
179	178	oveq1d 7165	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))) = (Σ𝑑 ∈ (1...(⌊‘𝑥))(𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))))
180	176, 179	breqtrrd 5086	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ≤ ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))))
181	40	leabsd 14768	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))) ≤ (abs‘((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1)))))
182	60, 40, 62, 180, 181	letrd 10791	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ≤ (abs‘((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1)))))
183	182	adantrr 715	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ≤ (abs‘((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1)))))
184	1, 39, 40, 54, 183	o1le 15003	1 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ∈ 𝑂(1))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 ≠ wne 3016 ∀wral 3138 ⊆ wss 3935 class class class wbr 5058 ↦ cmpt 5138 ‘cfv 6349 (class class class)co 7150 ℂcc 10529 ℝcr 10530 0cc0 10531 1c1 10532 + caddc 10534 · cmul 10536 +∞cpnf 10666 ℝ^*cxr 10668 < clt 10669 ≤ cle 10670 − cmin 10864 / cdiv 11291 ℕcn 11632 3c3 11687 ℝ⁺crp 12383 [,)cico 12734 ...cfz 12886 ⌊cfl 13154 abscabs 14587 ⇝_𝑟 crli 14836 𝑂(1)co1 14837 Σcsu 15036 Basecbs 16477 0_gc0g 16707 ℤRHomczrh 20641 ℤ/nℤczn 20644 logclog 25132 DChrcdchr 25802

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-rep 5182 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7455 ax-inf2 9098 ax-cnex 10587 ax-resscn 10588 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-addrcl 10592 ax-mulcl 10593 ax-mulrcl 10594 ax-mulcom 10595 ax-addass 10596 ax-mulass 10597 ax-distr 10598 ax-i2m1 10599 ax-1ne0 10600 ax-1rid 10601 ax-rnegex 10602 ax-rrecex 10603 ax-cnre 10604 ax-pre-lttri 10605 ax-pre-lttrn 10606 ax-pre-ltadd 10607 ax-pre-mulgt0 10608 ax-pre-sup 10609 ax-addf 10610 ax-mulf 10611

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-fal 1546 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4561 df-pr 4563 df-tp 4565 df-op 4567 df-uni 4832 df-int 4869 df-iun 4913 df-iin 4914 df-br 5059 df-opab 5121 df-mpt 5139 df-tr 5165 df-id 5454 df-eprel 5459 df-po 5468 df-so 5469 df-fr 5508 df-se 5509 df-we 5510 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-pred 6142 df-ord 6188 df-on 6189 df-lim 6190 df-suc 6191 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-fv 6357 df-isom 6358 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-of 7403 df-om 7575 df-1st 7683 df-2nd 7684 df-supp 7825 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-1o 8096 df-2o 8097 df-oadd 8100 df-er 8283 df-map 8402 df-pm 8403 df-ixp 8456 df-en 8504 df-dom 8505 df-sdom 8506 df-fin 8507 df-fsupp 8828 df-fi 8869 df-sup 8900 df-inf 8901 df-oi 8968 df-card 9362 df-pnf 10671 df-mnf 10672 df-xr 10673 df-ltxr 10674 df-le 10675 df-sub 10866 df-neg 10867 df-div 11292 df-nn 11633 df-2 11694 df-3 11695 df-4 11696 df-5 11697 df-6 11698 df-7 11699 df-8 11700 df-9 11701 df-n0 11892 df-xnn0 11962 df-z 11976 df-dec 12093 df-uz 12238 df-q 12343 df-rp 12384 df-xneg 12501 df-xadd 12502 df-xmul 12503 df-ioo 12736 df-ioc 12737 df-ico 12738 df-icc 12739 df-fz 12887 df-fzo 13028 df-fl 13156 df-mod 13232 df-seq 13364 df-exp 13424 df-fac 13628 df-bc 13657 df-hash 13685 df-shft 14420 df-cj 14452 df-re 14453 df-im 14454 df-sqrt 14588 df-abs 14589 df-limsup 14822 df-clim 14839 df-rlim 14840 df-o1 14841 df-lo1 14842 df-sum 15037 df-ef 15415 df-e 15416 df-sin 15417 df-cos 15418 df-tan 15419 df-pi 15420 df-dvds 15602 df-struct 16479 df-ndx 16480 df-slot 16481 df-base 16483 df-sets 16484 df-ress 16485 df-plusg 16572 df-mulr 16573 df-starv 16574 df-sca 16575 df-vsca 16576 df-ip 16577 df-tset 16578 df-ple 16579 df-ds 16581 df-unif 16582 df-hom 16583 df-cco 16584 df-rest 16690 df-topn 16691 df-0g 16709 df-gsum 16710 df-topgen 16711 df-pt 16712 df-prds 16715 df-xrs 16769 df-qtop 16774 df-imas 16775 df-xps 16777 df-mre 16851 df-mrc 16852 df-acs 16854 df-mgm 17846 df-sgrp 17895 df-mnd 17906 df-submnd 17951 df-mulg 18219 df-cntz 18441 df-cmn 18902 df-psmet 20531 df-xmet 20532 df-met 20533 df-bl 20534 df-mopn 20535 df-fbas 20536 df-fg 20537 df-cnfld 20540 df-top 21496 df-topon 21513 df-topsp 21535 df-bases 21548 df-cld 21621 df-ntr 21622 df-cls 21623 df-nei 21700 df-lp 21738 df-perf 21739 df-cn 21829 df-cnp 21830 df-haus 21917 df-cmp 21989 df-tx 22164 df-hmeo 22357 df-fil 22448 df-fm 22540 df-flim 22541 df-flf 22542 df-xms 22924 df-ms 22925 df-tms 22926 df-cncf 23480 df-limc 24458 df-dv 24459 df-ulm 24959 df-log 25134 df-cxp 25135 df-atan 25439 df-em 25564

This theorem is referenced by: dchrvmasumlem3 26069

W3C validator