dchrvmasumlem3 - Metamath Proof Explorer

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

Theorem dchrvmasumlem3 26069

Description: Lemma for dchrvmasum 26095. (Contributed by Mario Carneiro, 3-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
dchrvmasumlem3	⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ∈ 𝑂(1))

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

**Proof of Theorem dchrvmasumlem3**
Step	Hyp	Ref	Expression
1		1red 10636	. 2 ⊢ (𝜑 → 1 ∈ ℝ)
2		rpvmasum.z	. . 3 ⊢ 𝑍 = (ℤ/nℤ‘𝑁)
3		rpvmasum.l	. . 3 ⊢ 𝐿 = (ℤRHom‘𝑍)
4		rpvmasum.a	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ)
5		rpvmasum.g	. . 3 ⊢ 𝐺 = (DChr‘𝑁)
6		rpvmasum.d	. . 3 ⊢ 𝐷 = (Base‘𝐺)
7		rpvmasum.1	. . 3 ⊢ 1 = (0_g‘𝐺)
8		dchrisum.b	. . 3 ⊢ (𝜑 → 𝑋 ∈ 𝐷)
9		dchrisum.n1	. . 3 ⊢ (𝜑 → 𝑋 ≠ 1 )
10		dchrvmasum.f	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ⁺) → 𝐹 ∈ ℂ)
11		dchrvmasum.g	. . 3 ⊢ (𝑚 = (𝑥 / 𝑑) → 𝐹 = 𝐾)
12		dchrvmasum.c	. . 3 ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))
13		dchrvmasum.t	. . 3 ⊢ (𝜑 → 𝑇 ∈ ℂ)
14		dchrvmasum.1	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → (abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)))
15		dchrvmasum.r	. . 3 ⊢ (𝜑 → 𝑅 ∈ ℝ)
16		dchrvmasum.2	. . 3 ⊢ (𝜑 → ∀𝑚 ∈ (1[,)3)(abs‘(𝐹 − 𝑇)) ≤ 𝑅)
17	2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16	dchrvmasumlem2 26068	. 2 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ∈ 𝑂(1))
18		fzfid 13335	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (1...(⌊‘𝑥)) ∈ Fin)
19	11	eleq1d 2897	. . . . . . 7 ⊢ (𝑚 = (𝑥 / 𝑑) → (𝐹 ∈ ℂ ↔ 𝐾 ∈ ℂ))
20	10	ralrimiva 3182	. . . . . . . 8 ⊢ (𝜑 → ∀𝑚 ∈ ℝ⁺ 𝐹 ∈ ℂ)
21	20	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ∀𝑚 ∈ ℝ⁺ 𝐹 ∈ ℂ)
22		simpr 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ⁺)
23		elfznn 12930	. . . . . . . . 9 ⊢ (𝑑 ∈ (1...(⌊‘𝑥)) → 𝑑 ∈ ℕ)
24	23	nnrpd 12423	. . . . . . . 8 ⊢ (𝑑 ∈ (1...(⌊‘𝑥)) → 𝑑 ∈ ℝ⁺)
25		rpdivcl 12408	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑑 ∈ ℝ⁺) → (𝑥 / 𝑑) ∈ ℝ⁺)
26	22, 24, 25	syl2an 597	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑑) ∈ ℝ⁺)
27	19, 21, 26	rspcdva 3625	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝐾 ∈ ℂ)
28	13	ad2antrr 724	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑇 ∈ ℂ)
29	27, 28	subcld 10991	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐾 − 𝑇) ∈ ℂ)
30	29	abscld 14790	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘(𝐾 − 𝑇)) ∈ ℝ)
31	23	adantl 484	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ∈ ℕ)
32	30, 31	nndivred 11685	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℝ)
33	18, 32	fsumrecl 15085	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℝ)
34	8	ad2antrr 724	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑋 ∈ 𝐷)
35		elfzelz 12902	. . . . . . 7 ⊢ (𝑑 ∈ (1...(⌊‘𝑥)) → 𝑑 ∈ ℤ)
36	35	adantl 484	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ∈ ℤ)
37	5, 2, 6, 3, 34, 36	dchrzrhcl 25815	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑋‘(𝐿‘𝑑)) ∈ ℂ)
38		mucl 25712	. . . . . . . . 9 ⊢ (𝑑 ∈ ℕ → (μ‘𝑑) ∈ ℤ)
39	31, 38	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (μ‘𝑑) ∈ ℤ)
40	39	zred 12081	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (μ‘𝑑) ∈ ℝ)
41	40, 31	nndivred 11685	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑑) / 𝑑) ∈ ℝ)
42	41	recnd 10663	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑑) / 𝑑) ∈ ℂ)
43	37, 42	mulcld 10655	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) ∈ ℂ)
44	43, 29	mulcld 10655	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇)) ∈ ℂ)
45	18, 44	fsumcl 15084	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇)) ∈ ℂ)
46	45	abscld 14790	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ∈ ℝ)
47	33	recnd 10663	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℂ)
48	47	abscld 14790	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ∈ ℝ)
49	44	abscld 14790	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ∈ ℝ)
50	18, 49	fsumrecl 15085	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ∈ ℝ)
51	18, 44	fsumabs 15150	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ≤ Σ𝑑 ∈ (1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))))
52	43	abscld 14790	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑))) ∈ ℝ)
53	31	nnrecred 11682	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (1 / 𝑑) ∈ ℝ)
54	29	absge0d 14798	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘(𝐾 − 𝑇)))
55	37, 42	absmuld 14808	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑))) = ((abs‘(𝑋‘(𝐿‘𝑑))) · (abs‘((μ‘𝑑) / 𝑑))))
56	37	abscld 14790	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑋‘(𝐿‘𝑑))) ∈ ℝ)
57		1red 10636	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
58	42	abscld 14790	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑑) / 𝑑)) ∈ ℝ)
59	37	absge0d 14798	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘(𝑋‘(𝐿‘𝑑))))
60	42	absge0d 14798	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘((μ‘𝑑) / 𝑑)))
61		eqid 2821	. . . . . . . . . . . 12 ⊢ (Base‘𝑍) = (Base‘𝑍)
62	4	nnnn0d 11949	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
63	2, 61, 3	znzrhfo 20688	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ₀ → 𝐿:ℤ–onto→(Base‘𝑍))
64	62, 63	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐿:ℤ–onto→(Base‘𝑍))
65		fof 6585	. . . . . . . . . . . . . . 15 ⊢ (𝐿:ℤ–onto→(Base‘𝑍) → 𝐿:ℤ⟶(Base‘𝑍))
66	64, 65	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑍))
67	66	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝐿:ℤ⟶(Base‘𝑍))
68	67, 36	ffvelrnd 6847	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝐿‘𝑑) ∈ (Base‘𝑍))
69	5, 6, 2, 61, 34, 68	dchrabs2 25832	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑋‘(𝐿‘𝑑))) ≤ 1)
70	40	recnd 10663	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (μ‘𝑑) ∈ ℂ)
71	31	nncnd 11648	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ∈ ℂ)
72	31	nnne0d 11681	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ≠ 0)
73	70, 71, 72	absdivd 14809	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑑) / 𝑑)) = ((abs‘(μ‘𝑑)) / (abs‘𝑑)))
74	31	nnrpd 12423	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ∈ ℝ⁺)
75	74	rprege0d 12432	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑑 ∈ ℝ ∧ 0 ≤ 𝑑))
76		absid 14650	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ ℝ ∧ 0 ≤ 𝑑) → (abs‘𝑑) = 𝑑)
77	75, 76	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘𝑑) = 𝑑)
78	77	oveq2d 7166	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((abs‘(μ‘𝑑)) / (abs‘𝑑)) = ((abs‘(μ‘𝑑)) / 𝑑))
79	73, 78	eqtrd 2856	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑑) / 𝑑)) = ((abs‘(μ‘𝑑)) / 𝑑))
80	70	abscld 14790	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑑)) ∈ ℝ)
81		mule1 25719	. . . . . . . . . . . . . 14 ⊢ (𝑑 ∈ ℕ → (abs‘(μ‘𝑑)) ≤ 1)
82	31, 81	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑑)) ≤ 1)
83	80, 57, 74, 82	lediv1dd 12483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((abs‘(μ‘𝑑)) / 𝑑) ≤ (1 / 𝑑))
84	79, 83	eqbrtrd 5081	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑑) / 𝑑)) ≤ (1 / 𝑑))
85	56, 57, 58, 53, 59, 60, 69, 84	lemul12ad 11576	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑋‘(𝐿‘𝑑))) · (abs‘((μ‘𝑑) / 𝑑))) ≤ (1 · (1 / 𝑑)))
86	53	recnd 10663	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (1 / 𝑑) ∈ ℂ)
87	86	mulid2d 10653	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (1 · (1 / 𝑑)) = (1 / 𝑑))
88	85, 87	breqtrd 5085	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑋‘(𝐿‘𝑑))) · (abs‘((μ‘𝑑) / 𝑑))) ≤ (1 / 𝑑))
89	55, 88	eqbrtrd 5081	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑))) ≤ (1 / 𝑑))
90	52, 53, 30, 54, 89	lemul1ad 11573	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((abs‘((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑))) · (abs‘(𝐾 − 𝑇))) ≤ ((1 / 𝑑) · (abs‘(𝐾 − 𝑇))))
91	43, 29	absmuld 14808	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) = ((abs‘((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑))) · (abs‘(𝐾 − 𝑇))))
92	30	recnd 10663	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘(𝐾 − 𝑇)) ∈ ℂ)
93	92, 71, 72	divrec2d 11414	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝐾 − 𝑇)) / 𝑑) = ((1 / 𝑑) · (abs‘(𝐾 − 𝑇))))
94	90, 91, 93	3brtr4d 5091	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ≤ ((abs‘(𝐾 − 𝑇)) / 𝑑))
95	18, 49, 32, 94	fsumle 15148	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ≤ Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑))
96	46, 50, 33, 51, 95	letrd 10791	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ≤ Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑))
97	33	leabsd 14768	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑) ≤ (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)))
98	46, 33, 48, 96, 97	letrd 10791	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ≤ (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)))
99	98	adantrr 715	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ≤ (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)))
100	1, 17, 33, 45, 99	o1le 15003	1 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ∈ 𝑂(1))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 398 = wceq 1533 ∈ wcel 2110 ≠ wne 3016 ∀wral 3138 class class class wbr 5059 ↦ cmpt 5139 ⟶wf 6346 –onto→wfo 6348 ‘cfv 6350 (class class class)co 7150 ℂcc 10529 ℝcr 10530 0cc0 10531 1c1 10532 · cmul 10536 +∞cpnf 10666 ≤ cle 10670 − cmin 10864 / cdiv 11291 ℕcn 11632 3c3 11687 ℕ₀cn0 11891 ℤcz 11975 ℝ⁺crp 12383 [,)cico 12734 ...cfz 12886 ⌊cfl 13154 abscabs 14587 𝑂(1)co1 14837 Σcsu 15036 Basecbs 16477 0_gc0g 16707 ℤRHomczrh 20641 ℤ/nℤczn 20644 logclog 25132 μcmu 25666 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 2156 ax-12 2172 ax-ext 2793 ax-rep 5183 ax-sep 5196 ax-nul 5203 ax-pow 5259 ax-pr 5322 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 3497 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4562 df-pr 4564 df-tp 4566 df-op 4568 df-uni 4833 df-int 4870 df-iun 4914 df-iin 4915 df-disj 5025 df-br 5060 df-opab 5122 df-mpt 5140 df-tr 5166 df-id 5455 df-eprel 5460 df-po 5469 df-so 5470 df-fr 5509 df-se 5510 df-we 5511 df-xp 5556 df-rel 5557 df-cnv 5558 df-co 5559 df-dm 5560 df-rn 5561 df-res 5562 df-ima 5563 df-pred 6143 df-ord 6189 df-on 6190 df-lim 6191 df-suc 6192 df-iota 6309 df-fun 6352 df-fn 6353 df-f 6354 df-f1 6355 df-fo 6356 df-f1o 6357 df-fv 6358 df-isom 6359 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-tpos 7886 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-1o 8096 df-2o 8097 df-oadd 8100 df-omul 8101 df-er 8283 df-ec 8285 df-qs 8289 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-acn 9365 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-prm 16010 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-qus 16776 df-xps 16777 df-mre 16851 df-mrc 16852 df-acs 16854 df-mgm 17846 df-sgrp 17895 df-mnd 17906 df-mhm 17950 df-submnd 17951 df-grp 18100 df-minusg 18101 df-sbg 18102 df-mulg 18219 df-subg 18270 df-nsg 18271 df-eqg 18272 df-ghm 18350 df-cntz 18441 df-od 18650 df-cmn 18902 df-abl 18903 df-mgp 19234 df-ur 19246 df-ring 19293 df-cring 19294 df-oppr 19367 df-dvdsr 19385 df-unit 19386 df-invr 19416 df-dvr 19427 df-rnghom 19461 df-drng 19498 df-subrg 19527 df-lmod 19630 df-lss 19698 df-lsp 19738 df-sra 19938 df-rgmod 19939 df-lidl 19940 df-rsp 19941 df-2idl 19999 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-zring 20612 df-zrh 20645 df-zn 20648 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 df-mu 25672 df-dchr 25803

This theorem is referenced by: dchrvmasumiflem1 26071

W3C validator