Theorem dchrvmasumlem3

Description: Lemma for dchrvmasum . (Contributed by Mario Carneiro, 3-May-2016)

	Ref	Expression
Hypotheses	rpvmasum.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
	rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	rpvmasum.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	rpvmasum.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
	rpvmasum.1	⊢ 1 = ( 0g ‘ 𝐺 )
	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	dchrvmasumlem3	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) ∈ 𝑂(1) )

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2		rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3		rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4		rpvmasum.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
5		rpvmasum.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
6		rpvmasum.1	⊢ 1 = ( 0g ‘ 𝐺 )
7		dchrisum.b	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
8		dchrisum.n1	⊢ ( 𝜑 → 𝑋 ≠ 1 )
9		dchrvmasum.f	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → 𝐹 ∈ ℂ )
10		dchrvmasum.g	⊢ ( 𝑚 = ( 𝑥 / 𝑑 ) → 𝐹 = 𝐾 )
11		dchrvmasum.c	⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
12		dchrvmasum.t	⊢ ( 𝜑 → 𝑇 ∈ ℂ )
13		dchrvmasum.1	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → ( abs ‘ ( 𝐹 − 𝑇 ) ) ≤ ( 𝐶 · ( ( log ‘ 𝑚 ) / 𝑚 ) ) )
14		dchrvmasum.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ )
15		dchrvmasum.2	⊢ ( 𝜑 → ∀ 𝑚 ∈ ( 1 [,) 3 ) ( abs ‘ ( 𝐹 − 𝑇 ) ) ≤ 𝑅 )
16		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
17	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	dchrvmasumlem2	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ) ∈ 𝑂(1) )
18		fzfid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
19	10	eleq1d	⊢ ( 𝑚 = ( 𝑥 / 𝑑 ) → ( 𝐹 ∈ ℂ ↔ 𝐾 ∈ ℂ ) )
20	9	ralrimiva	⊢ ( 𝜑 → ∀ 𝑚 ∈ ℝ+ 𝐹 ∈ ℂ )
21	20	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ∀ 𝑚 ∈ ℝ+ 𝐹 ∈ ℂ )
22		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
23		elfznn	⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑑 ∈ ℕ )
24	23	nnrpd	⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑑 ∈ ℝ+ )
25		rpdivcl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) → ( 𝑥 / 𝑑 ) ∈ ℝ+ )
26	22 24 25	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑑 ) ∈ ℝ+ )
27	19 21 26	rspcdva	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐾 ∈ ℂ )
28	12	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑇 ∈ ℂ )
29	27 28	subcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐾 − 𝑇 ) ∈ ℂ )
30	29	abscld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝐾 − 𝑇 ) ) ∈ ℝ )
31	23	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℕ )
32	30 31	nndivred	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ∈ ℝ )
33	18 32	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ∈ ℝ )
34	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑋 ∈ 𝐷 )
35		elfzelz	⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑑 ∈ ℤ )
36	35	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℤ )
37	4 1 5 2 34 36	dchrzrhcl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ∈ ℂ )
38		mucl	⊢ ( 𝑑 ∈ ℕ → ( μ ‘ 𝑑 ) ∈ ℤ )
39	31 38	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑑 ) ∈ ℤ )
40	39	zred	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑑 ) ∈ ℝ )
41	40 31	nndivred	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑑 ) / 𝑑 ) ∈ ℝ )
42	41	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑑 ) / 𝑑 ) ∈ ℂ )
43	37 42	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ∈ ℂ )
44	43 29	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ∈ ℂ )
45	18 44	fsumcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ∈ ℂ )
46	45	abscld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) ∈ ℝ )
47	33	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ∈ ℂ )
48	47	abscld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ) ∈ ℝ )
49	44	abscld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) ∈ ℝ )
50	18 49	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) ∈ ℝ )
51	18 44	fsumabs	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) ≤ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) )
52	43	abscld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ) ∈ ℝ )
53	31	nnrecred	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑑 ) ∈ ℝ )
54	29	absge0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( 𝐾 − 𝑇 ) ) )
55	37 42	absmuld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ) = ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ) · ( abs ‘ ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ) )
56	37	abscld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ) ∈ ℝ )
57		1red	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℝ )
58	42	abscld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ∈ ℝ )
59	37	absge0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ) )
60	42	absge0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( ( μ ‘ 𝑑 ) / 𝑑 ) ) )
61		eqid	⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
62	3	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
63	1 61 2	znzrhfo	⊢ ( 𝑁 ∈ ℕ0 → 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) )
64	62 63	syl	⊢ ( 𝜑 → 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) )
65		fof	⊢ ( 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
66	64 65	syl	⊢ ( 𝜑 → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
67	66	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
68	67 36	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐿 ‘ 𝑑 ) ∈ ( Base ‘ 𝑍 ) )
69	4 5 1 61 34 68	dchrabs2	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ) ≤ 1 )
70	40	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑑 ) ∈ ℂ )
71	31	nncnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℂ )
72	31	nnne0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ≠ 0 )
73	70 71 72	absdivd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( μ ‘ 𝑑 ) / 𝑑 ) ) = ( ( abs ‘ ( μ ‘ 𝑑 ) ) / ( abs ‘ 𝑑 ) ) )
74	31	nnrpd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℝ+ )
75	74	rprege0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑑 ∈ ℝ ∧ 0 ≤ 𝑑 ) )
76		absid	⊢ ( ( 𝑑 ∈ ℝ ∧ 0 ≤ 𝑑 ) → ( abs ‘ 𝑑 ) = 𝑑 )
77	75 76	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ 𝑑 ) = 𝑑 )
78	77	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( μ ‘ 𝑑 ) ) / ( abs ‘ 𝑑 ) ) = ( ( abs ‘ ( μ ‘ 𝑑 ) ) / 𝑑 ) )
79	73 78	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( μ ‘ 𝑑 ) / 𝑑 ) ) = ( ( abs ‘ ( μ ‘ 𝑑 ) ) / 𝑑 ) )
80	70	abscld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( μ ‘ 𝑑 ) ) ∈ ℝ )
81		mule1	⊢ ( 𝑑 ∈ ℕ → ( abs ‘ ( μ ‘ 𝑑 ) ) ≤ 1 )
82	31 81	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( μ ‘ 𝑑 ) ) ≤ 1 )
83	80 57 74 82	lediv1dd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( μ ‘ 𝑑 ) ) / 𝑑 ) ≤ ( 1 / 𝑑 ) )
84	79 83	eqbrtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ≤ ( 1 / 𝑑 ) )
85	56 57 58 53 59 60 69 84	lemul12ad	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ) · ( abs ‘ ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ) ≤ ( 1 · ( 1 / 𝑑 ) ) )
86	53	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑑 ) ∈ ℂ )
87	86	mullidd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 · ( 1 / 𝑑 ) ) = ( 1 / 𝑑 ) )
88	85 87	breqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ) · ( abs ‘ ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ) ≤ ( 1 / 𝑑 ) )
89	55 88	eqbrtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ) ≤ ( 1 / 𝑑 ) )
90	52 53 30 54 89	lemul1ad	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ) · ( abs ‘ ( 𝐾 − 𝑇 ) ) ) ≤ ( ( 1 / 𝑑 ) · ( abs ‘ ( 𝐾 − 𝑇 ) ) ) )
91	43 29	absmuld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) = ( ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ) · ( abs ‘ ( 𝐾 − 𝑇 ) ) ) )
92	30	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝐾 − 𝑇 ) ) ∈ ℂ )
93	92 71 72	divrec2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) = ( ( 1 / 𝑑 ) · ( abs ‘ ( 𝐾 − 𝑇 ) ) ) )
94	90 91 93	3brtr4d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) ≤ ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) )
95	18 49 32 94	fsumle	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) ≤ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) )
96	46 50 33 51 95	letrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) ≤ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) )
97	33	leabsd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ≤ ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ) )
98	46 33 48 96 97	letrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) ≤ ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ) )
99	98	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) ≤ ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ) )
100	16 17 33 45 99	o1le	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) ∈ 𝑂(1) )