Metamath Proof Explorer


Theorem dchrvmasum

Description: The sum of the von Mangoldt function multiplied by a non-principal Dirichlet character, divided by n , is bounded. Equation 9.4.8 of Shapiro, p. 376. (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 = ( 0g𝐺 )
dchrmusum.b ( 𝜑𝑋𝐷 )
dchrmusum.n1 ( 𝜑𝑋1 )
Assertion dchrvmasum ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 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 = ( 0g𝐺 )
7 dchrmusum.b ( 𝜑𝑋𝐷 )
8 dchrmusum.n1 ( 𝜑𝑋1 )
9 eqid ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) )
10 1 2 3 4 5 6 7 8 9 dchrmusumlema ( 𝜑 → ∃ 𝑡𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) )
11 3 adantr ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑁 ∈ ℕ )
12 7 adantr ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑋𝐷 )
13 8 adantr ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑋1 )
14 simprl ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑐 ∈ ( 0 [,) +∞ ) )
15 simprrl ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 )
16 simprrr ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) )
17 1 2 11 4 5 6 12 13 9 14 15 16 dchrvmasumlem ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ∈ 𝑂(1) )
18 17 rexlimdvaa ( 𝜑 → ( ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ∈ 𝑂(1) ) )
19 18 exlimdv ( 𝜑 → ( ∃ 𝑡𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ∈ 𝑂(1) ) )
20 10 19 mpd ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ∈ 𝑂(1) )