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) )