dchrmusumlem

Description: The sum of the Möbius function multiplied by a non-principal Dirichlet character, divided by n , is bounded. Equation 9.4.16 of Shapiro, p. 379. (Contributed by Mario Carneiro, 12-May-2016)

	Ref	Expression
Hypotheses	rpvmasum.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
	rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	dchrmusum.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	dchrmusum.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
	dchrmusum.1	⊢ 1 = ( 0_g ‘ 𝐺 )
	dchrmusum.b	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
	dchrmusum.n1	⊢ ( 𝜑 → 𝑋 ≠ 1 )
	dchrmusum.f	⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) )
	dchrmusum.c	⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
	dchrmusum.t	⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ 𝑇 )
	dchrmusum.2	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) ≤ ( 𝐶 / 𝑦 ) )
Assertion	dchrmusumlem	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ⁺ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ) ∈ 𝑂(1) )

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2		rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3		rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4		dchrmusum.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
5		dchrmusum.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
6		dchrmusum.1	⊢ 1 = ( 0_g ‘ 𝐺 )
7		dchrmusum.b	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
8		dchrmusum.n1	⊢ ( 𝜑 → 𝑋 ≠ 1 )
9		dchrmusum.f	⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) )
10		dchrmusum.c	⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
11		dchrmusum.t	⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ 𝑇 )
12		dchrmusum.2	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) ≤ ( 𝐶 / 𝑦 ) )
13		fzfid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
14	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑋 ∈ 𝐷 )
15		elfzelz	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℤ )
16	15	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℤ )
17	4 1 5 2 14 16	dchrzrhcl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
18		elfznn	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
19	18	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
20		mucl	⊢ ( 𝑛 ∈ ℕ → ( μ ‘ 𝑛 ) ∈ ℤ )
21	19 20	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℤ )
22	21	zred	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℝ )
23	22 19	nndivred	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
24	23	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
25	17 24	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
26	13 25	fsumcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
27		climcl	⊢ ( seq 1 ( + , 𝐹 ) ⇝ 𝑇 → 𝑇 ∈ ℂ )
28	11 27	syl	⊢ ( 𝜑 → 𝑇 ∈ ℂ )
29	28	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → 𝑇 ∈ ℂ )
30	26 29	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · 𝑇 ) ∈ ℂ )
31	1 2 3 4 5 6 7 8 9 10 11 12	dchrisumn0	⊢ ( 𝜑 → 𝑇 ≠ 0 )
32	31	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → 𝑇 ≠ 0 )
33	30 29 32	divrecd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · 𝑇 ) / 𝑇 ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · 𝑇 ) · ( 1 / 𝑇 ) ) )
34	26 29 32	divcan4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · 𝑇 ) / 𝑇 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) )
35	33 34	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · 𝑇 ) · ( 1 / 𝑇 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) )
36	35	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ⁺ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · 𝑇 ) · ( 1 / 𝑇 ) ) ) = ( 𝑥 ∈ ℝ⁺ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ) )
37	28 31	reccld	⊢ ( 𝜑 → ( 1 / 𝑇 ) ∈ ℂ )
38	37	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → ( 1 / 𝑇 ) ∈ ℂ )
39	1 2 3 4 5 6 7 8 9 10 11 12	dchrmusum2	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ⁺ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · 𝑇 ) ) ∈ 𝑂(1) )
40		rpssre	⊢ ℝ⁺ ⊆ ℝ
41		o1const	⊢ ( ( ℝ⁺ ⊆ ℝ ∧ ( 1 / 𝑇 ) ∈ ℂ ) → ( 𝑥 ∈ ℝ⁺ ↦ ( 1 / 𝑇 ) ) ∈ 𝑂(1) )
42	40 37 41	sylancr	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ⁺ ↦ ( 1 / 𝑇 ) ) ∈ 𝑂(1) )
43	30 38 39 42	o1mul2	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ⁺ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · 𝑇 ) · ( 1 / 𝑇 ) ) ) ∈ 𝑂(1) )
44	36 43	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ⁺ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ) ∈ 𝑂(1) )

Metamath Proof Explorer

Theorem dchrmusumlem

Proof