This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rpvmasum

Description: The sum of the von Mangoldt function over those integers n == A (mod N ) is asymptotic to log x / phi ( x ) + O(1) . Equation 9.4.3 of Shapiro, p. 375. (Contributed by Mario Carneiro, 2-May-2016) (Proof shortened by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
rpvmasum.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
rpvmasum.b ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
rpvmasum.t ⊢ 𝑇 = ( ◡ 𝐿 “ { 𝐴 } )
Assertion rpvmasum ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )

Proof

Step Hyp Ref Expression
1 rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2 rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3 rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 rpvmasum.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
5 rpvmasum.b ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
6 rpvmasum.t ⊢ 𝑇 = ( ◡ 𝐿 “ { 𝐴 } )
7 3 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) → 𝑁 ∈ ℕ )
8 eqid ⊢ ( DChr ‘ 𝑁 ) = ( DChr ‘ 𝑁 )
9 eqid ⊢ ( Base ‘ ( DChr ‘ 𝑁 ) ) = ( Base ‘ ( DChr ‘ 𝑁 ) )
10 eqid ⊢ ( 0g ‘ ( DChr ‘ 𝑁 ) ) = ( 0g ‘ ( DChr ‘ 𝑁 ) )
11 2fveq3 ⊢ ( 𝑚 = 𝑛 → ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) = ( 𝑦 ‘ ( 𝐿 ‘ 𝑛 ) ) )
12 id ⊢ ( 𝑚 = 𝑛 → 𝑚 = 𝑛 )
13 11 12 oveq12d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) )
14 13 cbvsumv ⊢ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = Σ 𝑛 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 )
15 14 eqeq1i ⊢ ( Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 ↔ Σ 𝑛 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) = 0 )
16 15 rabbii ⊢ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } = { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑛 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) = 0 }
17 simpr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) → 𝑓 ∈ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } )
18 1 2 7 8 9 10 16 17 dchrisum0 ⊢ ¬ ( 𝜑 ∧ 𝑓 ∈ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } )
19 18 imnani ⊢ ( 𝜑 → ¬ 𝑓 ∈ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } )
20 19 eq0rdv ⊢ ( 𝜑 → { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } = ∅ )
21 20 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) = ( ♯ ‘ ∅ ) )
22 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
23 21 22 eqtrdi ⊢ ( 𝜑 → ( ♯ ‘ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) = 0 )
24 23 oveq2d ⊢ ( 𝜑 → ( 1 − ( ♯ ‘ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) ) = ( 1 − 0 ) )
25 1m0e1 ⊢ ( 1 − 0 ) = 1
26 24 25 eqtrdi ⊢ ( 𝜑 → ( 1 − ( ♯ ‘ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) ) = 1 )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 − ( ♯ ‘ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) ) = 1 )
28 27 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) ) ) = ( ( log ‘ 𝑥 ) · 1 ) )
29 relogcl ⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℝ )
30 29 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℝ )
31 30 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℂ )
32 31 mulridd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · 1 ) = ( log ‘ 𝑥 ) )
33 28 32 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) ) ) = ( log ‘ 𝑥 ) )
34 33 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) ) ) ) = ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) )
35 34 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) ) )
36 eqid ⊢ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } = { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 }
37 18 pm2.21i ⊢ ( ( 𝜑 ∧ 𝑓 ∈ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) → 𝐴 = ( 1r ‘ 𝑍 ) )
38 1 2 3 8 9 10 36 4 5 6 37 rpvmasum2 ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ { 𝑦 ∈ ( ( Base ‘ ( DChr ‘ 𝑁 ) ) ∖ { ( 0g ‘ ( DChr ‘ 𝑁 ) ) } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 } ) ) ) ) ) ∈ 𝑂(1) )
39 35 38 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )