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 mulid1d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( 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) )