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 27449

Description: Lemma for dchrvmasum 27476. (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 11134	. 2 ⊢ (𝜑 → 1 ∈ ℝ)
2		dchrvmasum.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))
3		elrege0 13396	. . . . . . 7 ⊢ (𝐶 ∈ (0[,)+∞) ↔ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶))
4	2, 3	sylib 218	. . . . . 6 ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶))
5	4	simpld 494	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ ℝ)
6	5	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝐶 ∈ ℝ)
7		fzfid 13924	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (1...(⌊‘𝑥)) ∈ Fin)
8		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ⁺)
9		elfznn 13496	. . . . . . . . 9 ⊢ (𝑑 ∈ (1...(⌊‘𝑥)) → 𝑑 ∈ ℕ)
10	9	nnrpd 12973	. . . . . . . 8 ⊢ (𝑑 ∈ (1...(⌊‘𝑥)) → 𝑑 ∈ ℝ⁺)
11		rpdivcl 12958	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ℝ⁺) → (𝑥 / 𝑑) ∈ ℝ⁺)
12	8, 10, 11	syl2an 597	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑑) ∈ ℝ⁺)
13	12	relogcld 26575	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑑)) ∈ ℝ)
14	8	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ⁺)
15	13, 14	rerpdivcld 13006	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑑)) / 𝑥) ∈ ℝ)
16	7, 15	fsumrecl 15685	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥) ∈ ℝ)
17	6, 16	remulcld 11164	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ∈ ℝ)
18		dchrvmasum.r	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ ℝ)
19		3nn 12249	. . . . . . 7 ⊢ 3 ∈ ℕ
20		nnrp 12943	. . . . . . 7 ⊢ (3 ∈ ℕ → 3 ∈ ℝ⁺)
21		relogcl 26527	. . . . . . 7 ⊢ (3 ∈ ℝ⁺ → (log‘3) ∈ ℝ)
22	19, 20, 21	mp2b 10	. . . . . 6 ⊢ (log‘3) ∈ ℝ
23		1re 11133	. . . . . 6 ⊢ 1 ∈ ℝ
24	22, 23	readdcli 11149	. . . . 5 ⊢ ((log‘3) + 1) ∈ ℝ
25		remulcl 11112	. . . . 5 ⊢ ((𝑅 ∈ ℝ ∧ ((log‘3) + 1) ∈ ℝ) → (𝑅 · ((log‘3) + 1)) ∈ ℝ)
26	18, 24, 25	sylancl 587	. . . 4 ⊢ (𝜑 → (𝑅 · ((log‘3) + 1)) ∈ ℝ)
27	26	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑅 · ((log‘3) + 1)) ∈ ℝ)
28		rpssre 12939	. . . . 5 ⊢ ℝ⁺ ⊆ ℝ
29	5	recnd 11162	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ ℂ)
30		o1const 15571	. . . . 5 ⊢ ((ℝ⁺ ⊆ ℝ ∧ 𝐶 ∈ ℂ) → (𝑥 ∈ ℝ⁺ ↦ 𝐶) ∈ 𝑂(1))
31	28, 29, 30	sylancr 588	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ 𝐶) ∈ 𝑂(1))
32		logfacrlim2 27177	. . . . 5 ⊢ (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ⇝_𝑟 1
33		rlimo1 15568	. . . . 5 ⊢ ((𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ⇝_𝑟 1 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ∈ 𝑂(1))
34	32, 33	mp1i 13	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ∈ 𝑂(1))
35	6, 16, 31, 34	o1mul2 15576	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥))) ∈ 𝑂(1))
36	26	recnd 11162	. . . 4 ⊢ (𝜑 → (𝑅 · ((log‘3) + 1)) ∈ ℂ)
37		o1const 15571	. . . 4 ⊢ ((ℝ⁺ ⊆ ℝ ∧ (𝑅 · ((log‘3) + 1)) ∈ ℂ) → (𝑥 ∈ ℝ⁺ ↦ (𝑅 · ((log‘3) + 1))) ∈ 𝑂(1))
38	28, 36, 37	sylancr 588	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (𝑅 · ((log‘3) + 1))) ∈ 𝑂(1))
39	17, 27, 35, 38	o1add2 15575	. 2 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1)))) ∈ 𝑂(1))
40	17, 27	readdcld 11163	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))) ∈ ℝ)
41		dchrvmasum.g	. . . . . . . . 9 ⊢ (𝑚 = (𝑥 / 𝑑) → 𝐹 = 𝐾)
42	41	eleq1d 2820	. . . . . . . 8 ⊢ (𝑚 = (𝑥 / 𝑑) → (𝐹 ∈ ℂ ↔ 𝐾 ∈ ℂ))
43		dchrvmasum.f	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → 𝐹 ∈ ℂ)
44	43	ralrimiva 3127	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑚 ∈ ℝ⁺ 𝐹 ∈ ℂ)
45	44	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ∀𝑚 ∈ ℝ⁺ 𝐹 ∈ ℂ)
46	42, 45, 12	rspcdva 3563	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝐾 ∈ ℂ)
47		dchrvmasum.t	. . . . . . . 8 ⊢ (𝜑 → 𝑇 ∈ ℂ)
48	47	ad2antrr 727	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑇 ∈ ℂ)
49	46, 48	subcld 11494	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐾 − 𝑇) ∈ ℂ)
50	49	abscld 15390	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘(𝐾 − 𝑇)) ∈ ℝ)
51	9	adantl 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ∈ ℕ)
52	50, 51	nndivred 12220	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℝ)
53	7, 52	fsumrecl 15685	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℝ)
54	53	recnd 11162	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℂ)
55	51	nnrpd 12973	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ∈ ℝ⁺)
56	49	absge0d 15398	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘(𝐾 − 𝑇)))
57	50, 55, 56	divge0d 13015	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((abs‘(𝐾 − 𝑇)) / 𝑑))
58	7, 52, 57	fsumge0 15747	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 0 ≤ Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑))
59	53, 58	absidd 15374	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) = Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑))
60	59, 53	eqeltrd 2835	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ∈ ℝ)
61	40	recnd 11162	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))) ∈ ℂ)
62	61	abscld 15390	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1)))) ∈ ℝ)
63		3re 12250	. . . . . . . 8 ⊢ 3 ∈ ℝ
64	63	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 3 ∈ ℝ)
65		1le3 12377	. . . . . . 7 ⊢ 1 ≤ 3
66	64, 65	jctir 520	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (3 ∈ ℝ ∧ 1 ≤ 3))
67	18	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑅 ∈ ℝ)
68	23	rexri 11192	. . . . . . . . . 10 ⊢ 1 ∈ ℝ^*
69	63	rexri 11192	. . . . . . . . . 10 ⊢ 3 ∈ ℝ^*
70		1lt3 12338	. . . . . . . . . 10 ⊢ 1 < 3
71		lbico1 13342	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ^* ∧ 3 ∈ ℝ^* ∧ 1 < 3) → 1 ∈ (1[,)3))
72	68, 69, 70, 71	mp3an 1464	. . . . . . . . 9 ⊢ 1 ∈ (1[,)3)
73		0red 11136	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 0 ∈ ℝ)
74		elico2 13352	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℝ ∧ 3 ∈ ℝ^*) → (𝑚 ∈ (1[,)3) ↔ (𝑚 ∈ ℝ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 3)))
75	23, 69, 74	mp2an 693	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1[,)3) ↔ (𝑚 ∈ ℝ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 3))
76	75	simp1bi 1146	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (1[,)3) → 𝑚 ∈ ℝ)
77		0red 11136	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1[,)3) → 0 ∈ ℝ)
78		1red 11134	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1[,)3) → 1 ∈ ℝ)
79		0lt1 11661	. . . . . . . . . . . . . . 15 ⊢ 0 < 1
80	79	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1[,)3) → 0 < 1)
81	75	simp2bi 1147	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1[,)3) → 1 ≤ 𝑚)
82	77, 78, 76, 80, 81	ltletrd 11295	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (1[,)3) → 0 < 𝑚)
83	76, 82	elrpd 12972	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (1[,)3) → 𝑚 ∈ ℝ⁺)
84	47	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → 𝑇 ∈ ℂ)
85	43, 84	subcld 11494	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → (𝐹 − 𝑇) ∈ ℂ)
86	85	abscld 15390	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → (abs‘(𝐹 − 𝑇)) ∈ ℝ)
87	83, 86	sylan2 594	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (abs‘(𝐹 − 𝑇)) ∈ ℝ)
88	18	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 𝑅 ∈ ℝ)
89	85	absge0d 15398	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → 0 ≤ (abs‘(𝐹 − 𝑇)))
90	83, 89	sylan2 594	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 0 ≤ (abs‘(𝐹 − 𝑇)))
91		dchrvmasum.2	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑚 ∈ (1[,)3)(abs‘(𝐹 − 𝑇)) ≤ 𝑅)
92	91	r19.21bi 3227	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (abs‘(𝐹 − 𝑇)) ≤ 𝑅)
93	73, 87, 88, 90, 92	letrd 11292	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 0 ≤ 𝑅)
94	93	ralrimiva 3127	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑚 ∈ (1[,)3)0 ≤ 𝑅)
95		biidd 262	. . . . . . . . . 10 ⊢ (𝑚 = 1 → (0 ≤ 𝑅 ↔ 0 ≤ 𝑅))
96	95	rspcv 3558	. . . . . . . . 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 11162	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘(𝐾 − 𝑇)) ∈ ℂ)
101	5	ad2antrr 727	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝐶 ∈ ℝ)
102	101, 15	remulcld 11164	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) ∈ ℝ)
103	4	ad2antrr 727	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶))
104		log1 26537	. . . . . . . . 9 ⊢ (log‘1) = 0
105	51	nncnd 12179	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ∈ ℂ)
106	105	mullidd 11152	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (1 · 𝑑) = 𝑑)
107		rpre 12940	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
108	107	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ)
109		fznnfl 13810	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (𝑑 ∈ (1...(⌊‘𝑥)) ↔ (𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝑥)))
110	108, 109	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑑 ∈ (1...(⌊‘𝑥)) ↔ (𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝑥)))
111	110	simplbda 499	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ≤ 𝑥)
112	106, 111	eqbrtrd 5096	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (1 · 𝑑) ≤ 𝑥)
113		1red 11134	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
114	107	ad2antlr 728	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
115	113, 114, 55	lemuldivd 13024	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((1 · 𝑑) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑑)))
116	112, 115	mpbid 232	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 1 ≤ (𝑥 / 𝑑))
117		1rp 12935	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ⁺
118	117	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ⁺)
119	118, 12	logled 26579	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (1 ≤ (𝑥 / 𝑑) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑑))))
120	116, 119	mpbid 232	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (log‘1) ≤ (log‘(𝑥 / 𝑑)))
121	104, 120	eqbrtrrid 5110	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ (log‘(𝑥 / 𝑑)))
122		rpregt0 12946	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
123	122	ad2antlr 728	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
124		divge0 12014	. . . . . . . 8 ⊢ ((((log‘(𝑥 / 𝑑)) ∈ ℝ ∧ 0 ≤ (log‘(𝑥 / 𝑑))) ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → 0 ≤ ((log‘(𝑥 / 𝑑)) / 𝑥))
125	13, 121, 123, 124	syl21anc 838	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((log‘(𝑥 / 𝑑)) / 𝑥))
126		mulge0 11657	. . . . . . 7 ⊢ (((𝐶 ∈ ℝ ∧ 0 ≤ 𝐶) ∧ (((log‘(𝑥 / 𝑑)) / 𝑥) ∈ ℝ ∧ 0 ≤ ((log‘(𝑥 / 𝑑)) / 𝑥))) → 0 ≤ (𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)))
127	103, 15, 125, 126	syl12anc 837	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ (𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)))
128		absidm 15275	. . . . . . . . 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 7378	. . . . . . . . . 10 ⊢ (𝑚 = (𝑥 / 𝑑) → (abs‘(𝐹 − 𝑇)) = (abs‘(𝐾 − 𝑇)))
132		fveq2 6829	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑥 / 𝑑) → (log‘𝑚) = (log‘(𝑥 / 𝑑)))
133		id 22	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑥 / 𝑑) → 𝑚 = (𝑥 / 𝑑))
134	132, 133	oveq12d 7374	. . . . . . . . . . 11 ⊢ (𝑚 = (𝑥 / 𝑑) → ((log‘𝑚) / 𝑚) = ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)))
135	134	oveq2d 7372	. . . . . . . . . 10 ⊢ (𝑚 = (𝑥 / 𝑑) → (𝐶 · ((log‘𝑚) / 𝑚)) = (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))))
136	131, 135	breq12d 5087	. . . . . . . . 9 ⊢ (𝑚 = (𝑥 / 𝑑) → ((abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)) ↔ (abs‘(𝐾 − 𝑇)) ≤ (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)))))
137		dchrvmasum.1	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → (abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)))
138	137	ralrimiva 3127	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑚 ∈ (3[,)+∞)(abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)))
139	138	ad3antrrr 731	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → ∀𝑚 ∈ (3[,)+∞)(abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)))
140		nndivre 12207	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 𝑑 ∈ ℕ) → (𝑥 / 𝑑) ∈ ℝ)
141	108, 9, 140	syl2an 597	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑑) ∈ ℝ)
142	141	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (𝑥 / 𝑑) ∈ ℝ)
143		simpr 484	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → 3 ≤ (𝑥 / 𝑑))
144		elicopnf 13387	. . . . . . . . . . 11 ⊢ (3 ∈ ℝ → ((𝑥 / 𝑑) ∈ (3[,)+∞) ↔ ((𝑥 / 𝑑) ∈ ℝ ∧ 3 ≤ (𝑥 / 𝑑))))
145	63, 144	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑥 / 𝑑) ∈ (3[,)+∞) ↔ ((𝑥 / 𝑑) ∈ ℝ ∧ 3 ≤ (𝑥 / 𝑑)))
146	142, 143, 145	sylanbrc 584	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (𝑥 / 𝑑) ∈ (3[,)+∞))
147	136, 139, 146	rspcdva 3563	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (abs‘(𝐾 − 𝑇)) ≤ (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))))
148	13	recnd 11162	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑑)) ∈ ℂ)
149		rpcnne0 12950	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
150	149	ad2antlr 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
151	55	rpcnne0d 12984	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑑 ∈ ℂ ∧ 𝑑 ≠ 0))
152		divdiv2 11856	. . . . . . . . . . . . 13 ⊢ (((log‘(𝑥 / 𝑑)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ (𝑑 ∈ ℂ ∧ 𝑑 ≠ 0)) → ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)) = (((log‘(𝑥 / 𝑑)) · 𝑑) / 𝑥))
153	148, 150, 151, 152	syl3anc 1374	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)) = (((log‘(𝑥 / 𝑑)) · 𝑑) / 𝑥))
154		div23 11817	. . . . . . . . . . . . 13 ⊢ (((log‘(𝑥 / 𝑑)) ∈ ℂ ∧ 𝑑 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((log‘(𝑥 / 𝑑)) · 𝑑) / 𝑥) = (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑))
155	148, 105, 150, 154	syl3anc 1374	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑑)) · 𝑑) / 𝑥) = (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑))
156	153, 155	eqtrd 2770	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)) = (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑))
157	156	oveq2d 7372	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))) = (𝐶 · (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑)))
158	29	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝐶 ∈ ℂ)
159	15	recnd 11162	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑑)) / 𝑥) ∈ ℂ)
160	158, 159, 105	mulassd 11157	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑) = (𝐶 · (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑)))
161	157, 160	eqtr4d 2773	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))) = ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑))
162	161	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))) = ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑))
163	147, 162	breqtrd 5100	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (abs‘(𝐾 − 𝑇)) ≤ ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑))
164	130, 163	eqbrtrd 5096	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 3 ≤ (𝑥 / 𝑑)) → (abs‘(abs‘(𝐾 − 𝑇))) ≤ ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑))
165	129	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (abs‘(abs‘(𝐾 − 𝑇))) = (abs‘(𝐾 − 𝑇)))
166	131	breq1d 5084	. . . . . . . 8 ⊢ (𝑚 = (𝑥 / 𝑑) → ((abs‘(𝐹 − 𝑇)) ≤ 𝑅 ↔ (abs‘(𝐾 − 𝑇)) ≤ 𝑅))
167	91	ad3antrrr 731	. . . . . . . 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 13352	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ 3 ∈ ℝ^*) → ((𝑥 / 𝑑) ∈ (1[,)3) ↔ ((𝑥 / 𝑑) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑑) ∧ (𝑥 / 𝑑) < 3)))
172	23, 69, 171	mp2an 693	. . . . . . . . 9 ⊢ ((𝑥 / 𝑑) ∈ (1[,)3) ↔ ((𝑥 / 𝑑) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑑) ∧ (𝑥 / 𝑑) < 3))
173	168, 169, 170, 172	syl3anbrc 1345	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (𝑥 / 𝑑) ∈ (1[,)3))
174	166, 167, 173	rspcdva 3563	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (abs‘(𝐾 − 𝑇)) ≤ 𝑅)
175	165, 174	eqbrtrd 5096	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑑) < 3) → (abs‘(abs‘(𝐾 − 𝑇))) ≤ 𝑅)
176	8, 66, 99, 100, 102, 127, 164, 175	fsumharmonic 26963	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ≤ (Σ𝑑 ∈ (1...(⌊‘𝑥))(𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))))
177	29	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝐶 ∈ ℂ)
178	7, 177, 159	fsummulc2 15735	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) = Σ𝑑 ∈ (1...(⌊‘𝑥))(𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)))
179	178	oveq1d 7371	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))) = (Σ𝑑 ∈ (1...(⌊‘𝑥))(𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))))
180	176, 179	breqtrrd 5102	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ≤ ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))))
181	40	leabsd 15366	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))) ≤ (abs‘((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1)))))
182	60, 40, 62, 180, 181	letrd 11292	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ≤ (abs‘((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1)))))
183	182	adantrr 718	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ≤ (abs‘((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1)))))
184	1, 39, 40, 54, 183	o1le 15604	1 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ∈ 𝑂(1))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2930 ∀wral 3049 ⊆ wss 3885 class class class wbr 5074 ↦ cmpt 5155 ‘cfv 6487 (class class class)co 7356 ℂcc 11025 ℝcr 11026 0cc0 11027 1c1 11028 + caddc 11030 · cmul 11032 +∞cpnf 11165 ℝ^*cxr 11167 < clt 11168 ≤ cle 11169 − cmin 11366 / cdiv 11796 ℕcn 12163 3c3 12226 ℝ⁺crp 12931 [,)cico 13289 ...cfz 13450 ⌊cfl 13738 abscabs 15185 ⇝_𝑟 crli 15436 𝑂(1)co1 15437 Σcsu 15637 Basecbs 17168 0_gc0g 17391 ℤRHomczrh 21468 ℤ/nℤczn 21471 logclog 26506 DChrcdchr 27183

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2184 ax-ext 2707 ax-rep 5201 ax-sep 5220 ax-nul 5230 ax-pow 5296 ax-pr 5364 ax-un 7678 ax-inf2 9551 ax-cnex 11083 ax-resscn 11084 ax-1cn 11085 ax-icn 11086 ax-addcl 11087 ax-addrcl 11088 ax-mulcl 11089 ax-mulrcl 11090 ax-mulcom 11091 ax-addass 11092 ax-mulass 11093 ax-distr 11094 ax-i2m1 11095 ax-1ne0 11096 ax-1rid 11097 ax-rnegex 11098 ax-rrecex 11099 ax-cnre 11100 ax-pre-lttri 11101 ax-pre-lttrn 11102 ax-pre-ltadd 11103 ax-pre-mulgt0 11104 ax-pre-sup 11105 ax-addf 11106

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2538 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2810 df-nfc 2884 df-ne 2931 df-nel 3035 df-ral 3050 df-rex 3060 df-rmo 3340 df-reu 3341 df-rab 3388 df-v 3429 df-sbc 3726 df-csb 3834 df-dif 3888 df-un 3890 df-in 3892 df-ss 3902 df-pss 3905 df-nul 4264 df-if 4457 df-pw 4533 df-sn 4558 df-pr 4560 df-tp 4562 df-op 4564 df-uni 4841 df-int 4880 df-iun 4925 df-iin 4926 df-br 5075 df-opab 5137 df-mpt 5156 df-tr 5182 df-id 5515 df-eprel 5520 df-po 5528 df-so 5529 df-fr 5573 df-se 5574 df-we 5575 df-xp 5626 df-rel 5627 df-cnv 5628 df-co 5629 df-dm 5630 df-rn 5631 df-res 5632 df-ima 5633 df-pred 6254 df-ord 6315 df-on 6316 df-lim 6317 df-suc 6318 df-iota 6443 df-fun 6489 df-fn 6490 df-f 6491 df-f1 6492 df-fo 6493 df-f1o 6494 df-fv 6495 df-isom 6496 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-of 7620 df-om 7807 df-1st 7931 df-2nd 7932 df-supp 8100 df-frecs 8220 df-wrecs 8251 df-recs 8300 df-rdg 8338 df-1o 8394 df-2o 8395 df-oadd 8398 df-er 8632 df-map 8764 df-pm 8765 df-ixp 8835 df-en 8883 df-dom 8884 df-sdom 8885 df-fin 8886 df-fsupp 9264 df-fi 9313 df-sup 9344 df-inf 9345 df-oi 9414 df-card 9852 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-div 11797 df-nn 12164 df-2 12233 df-3 12234 df-4 12235 df-5 12236 df-6 12237 df-7 12238 df-8 12239 df-9 12240 df-n0 12427 df-xnn0 12500 df-z 12514 df-dec 12634 df-uz 12778 df-q 12888 df-rp 12932 df-xneg 13052 df-xadd 13053 df-xmul 13054 df-ioo 13291 df-ioc 13292 df-ico 13293 df-icc 13294 df-fz 13451 df-fzo 13598 df-fl 13740 df-mod 13818 df-seq 13953 df-exp 14013 df-fac 14225 df-bc 14254 df-hash 14282 df-shft 15018 df-cj 15050 df-re 15051 df-im 15052 df-sqrt 15186 df-abs 15187 df-limsup 15422 df-clim 15439 df-rlim 15440 df-o1 15441 df-lo1 15442 df-sum 15638 df-ef 16021 df-e 16022 df-sin 16023 df-cos 16024 df-tan 16025 df-pi 16026 df-dvds 16211 df-struct 17106 df-sets 17123 df-slot 17141 df-ndx 17153 df-base 17169 df-ress 17190 df-plusg 17222 df-mulr 17223 df-starv 17224 df-sca 17225 df-vsca 17226 df-ip 17227 df-tset 17228 df-ple 17229 df-ds 17231 df-unif 17232 df-hom 17233 df-cco 17234 df-rest 17374 df-topn 17375 df-0g 17393 df-gsum 17394 df-topgen 17395 df-pt 17396 df-prds 17399 df-xrs 17455 df-qtop 17460 df-imas 17461 df-xps 17463 df-mre 17537 df-mrc 17538 df-acs 17540 df-mgm 18597 df-sgrp 18676 df-mnd 18692 df-submnd 18741 df-mulg 19033 df-cntz 19281 df-cmn 19746 df-psmet 21333 df-xmet 21334 df-met 21335 df-bl 21336 df-mopn 21337 df-fbas 21338 df-fg 21339 df-cnfld 21342 df-top 22847 df-topon 22864 df-topsp 22886 df-bases 22899 df-cld 22972 df-ntr 22973 df-cls 22974 df-nei 23051 df-lp 23089 df-perf 23090 df-cn 23180 df-cnp 23181 df-haus 23268 df-cmp 23340 df-tx 23515 df-hmeo 23708 df-fil 23799 df-fm 23891 df-flim 23892 df-flf 23893 df-xms 24273 df-ms 24274 df-tms 24275 df-cncf 24833 df-limc 25821 df-dv 25822 df-ulm 26330 df-log 26508 df-cxp 26509 df-atan 26819 df-em 26944

This theorem is referenced by: dchrvmasumlem3 27450

W3C validator