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 ⊢ Z = ℤ/Nℤ
rpvmasum.l ⊢ L = ℤRHom ⁡ Z
rpvmasum.a ⊢ φ → N ∈ ℕ
rpvmasum.u ⊢ U = Unit ⁡ Z
rpvmasum.b ⊢ φ → A ∈ U
rpvmasum.t ⊢ T = L -1 A
Assertion rpvmasum ⊢ φ → x ∈ ℝ + ⟼ ϕ ⁡ N ⁢ ∑ n ∈ 1 … x ∩ T Λ ⁡ n n − log ⁡ x ∈ 𝑂⁡1

Proof

Step Hyp Ref Expression
1 rpvmasum.z ⊢ Z = ℤ/Nℤ
2 rpvmasum.l ⊢ L = ℤRHom ⁡ Z
3 rpvmasum.a ⊢ φ → N ∈ ℕ
4 rpvmasum.u ⊢ U = Unit ⁡ Z
5 rpvmasum.b ⊢ φ → A ∈ U
6 rpvmasum.t ⊢ T = L -1 A
7 3 adantr ⊢ φ ∧ f ∈ y ∈ Base DChr ⁡ N ∖ 0 DChr ⁡ N | ∑ m ∈ ℕ y ⁡ L ⁡ m m = 0 → N ∈ ℕ
8 eqid ⊢ DChr ⁡ N = DChr ⁡ N
9 eqid ⊢ Base DChr ⁡ N = Base DChr ⁡ N
10 eqid ⊢ 0 DChr ⁡ N = 0 DChr ⁡ N
11 2fveq3 ⊢ m = n → y ⁡ L ⁡ m = y ⁡ L ⁡ n
12 id ⊢ m = n → m = n
13 11 12 oveq12d ⊢ m = n → y ⁡ L ⁡ m m = y ⁡ L ⁡ n n
14 13 cbvsumv ⊢ ∑ m ∈ ℕ y ⁡ L ⁡ m m = ∑ n ∈ ℕ y ⁡ L ⁡ n n
15 14 eqeq1i ⊢ ∑ m ∈ ℕ y ⁡ L ⁡ m m = 0 ↔ ∑ n ∈ ℕ y ⁡ L ⁡ n n = 0
16 15 rabbii ⊢ y ∈ Base DChr ⁡ N ∖ 0 DChr ⁡ N | ∑ m ∈ ℕ y ⁡ L ⁡ m m = 0 = y ∈ Base DChr ⁡ N ∖ 0 DChr ⁡ N | ∑ n ∈ ℕ y ⁡ L ⁡ n n = 0
17 simpr ⊢ φ ∧ f ∈ y ∈ Base DChr ⁡ N ∖ 0 DChr ⁡ N | ∑ m ∈ ℕ y ⁡ L ⁡ m m = 0 → f ∈ y ∈ Base DChr ⁡ N ∖ 0 DChr ⁡ N | ∑ m ∈ ℕ y ⁡ L ⁡ m m = 0
18 1 2 7 8 9 10 16 17 dchrisum0 ⊢ ¬ φ ∧ f ∈ y ∈ Base DChr ⁡ N ∖ 0 DChr ⁡ N | ∑ m ∈ ℕ y ⁡ L ⁡ m m = 0
19 18 imnani ⊢ φ → ¬ f ∈ y ∈ Base DChr ⁡ N ∖ 0 DChr ⁡ N | ∑ m ∈ ℕ y ⁡ L ⁡ m m = 0
20 19 eq0rdv ⊢ φ → y ∈ Base DChr ⁡ N ∖ 0 DChr ⁡ N | ∑ m ∈ ℕ y ⁡ L ⁡ m m = 0 = ∅
21 20 fveq2d ⊢ φ → y ∈ Base DChr ⁡ N ∖ 0 DChr ⁡ N | ∑ m ∈ ℕ y ⁡ L ⁡ m m = 0 = ∅
22 hash0 ⊢ ∅ = 0
23 21 22 eqtrdi ⊢ φ → y ∈ Base DChr ⁡ N ∖ 0 DChr ⁡ N | ∑ m ∈ ℕ y ⁡ L ⁡ m m = 0 = 0
24 23 oveq2d ⊢ φ → 1 − y ∈ Base DChr ⁡ N ∖ 0 DChr ⁡ N | ∑ m ∈ ℕ y ⁡ L ⁡ m m = 0 = 1 − 0
25 1m0e1 ⊢ 1 − 0 = 1
26 24 25 eqtrdi ⊢ φ → 1 − y ∈ Base DChr ⁡ N ∖ 0 DChr ⁡ N | ∑ m ∈ ℕ y ⁡ L ⁡ m m = 0 = 1
27 26 adantr ⊢ φ ∧ x ∈ ℝ + → 1 − y ∈ Base DChr ⁡ N ∖ 0 DChr ⁡ N | ∑ m ∈ ℕ y ⁡ L ⁡ m m = 0 = 1
28 27 oveq2d ⊢ φ ∧ x ∈ ℝ + → log ⁡ x ⁢ 1 − y ∈ Base DChr ⁡ N ∖ 0 DChr ⁡ N | ∑ m ∈ ℕ y ⁡ L ⁡ m m = 0 = log ⁡ x ⋅ 1
29 relogcl ⊢ x ∈ ℝ + → log ⁡ x ∈ ℝ
30 29 adantl ⊢ φ ∧ x ∈ ℝ + → log ⁡ x ∈ ℝ
31 30 recnd ⊢ φ ∧ x ∈ ℝ + → log ⁡ x ∈ ℂ
32 31 mulid1d ⊢ φ ∧ x ∈ ℝ + → log ⁡ x ⋅ 1 = log ⁡ x
33 28 32 eqtrd ⊢ φ ∧ x ∈ ℝ + → log ⁡ x ⁢ 1 − y ∈ Base DChr ⁡ N ∖ 0 DChr ⁡ N | ∑ m ∈ ℕ y ⁡ L ⁡ m m = 0 = log ⁡ x
34 33 oveq2d ⊢ φ ∧ x ∈ ℝ + → ϕ ⁡ N ⁢ ∑ n ∈ 1 … x ∩ T Λ ⁡ n n − log ⁡ x ⁢ 1 − y ∈ Base DChr ⁡ N ∖ 0 DChr ⁡ N | ∑ m ∈ ℕ y ⁡ L ⁡ m m = 0 = ϕ ⁡ N ⁢ ∑ n ∈ 1 … x ∩ T Λ ⁡ n n − log ⁡ x
35 34 mpteq2dva ⊢ φ → x ∈ ℝ + ⟼ ϕ ⁡ N ⁢ ∑ n ∈ 1 … x ∩ T Λ ⁡ n n − log ⁡ x ⁢ 1 − y ∈ Base DChr ⁡ N ∖ 0 DChr ⁡ N | ∑ m ∈ ℕ y ⁡ L ⁡ m m = 0 = x ∈ ℝ + ⟼ ϕ ⁡ N ⁢ ∑ n ∈ 1 … x ∩ T Λ ⁡ n n − log ⁡ x
36 eqid ⊢ y ∈ Base DChr ⁡ N ∖ 0 DChr ⁡ N | ∑ m ∈ ℕ y ⁡ L ⁡ m m = 0 = y ∈ Base DChr ⁡ N ∖ 0 DChr ⁡ N | ∑ m ∈ ℕ y ⁡ L ⁡ m m = 0
37 18 pm2.21i ⊢ φ ∧ f ∈ y ∈ Base DChr ⁡ N ∖ 0 DChr ⁡ N | ∑ m ∈ ℕ y ⁡ L ⁡ m m = 0 → A = 1 Z
38 1 2 3 8 9 10 36 4 5 6 37 rpvmasum2 ⊢ φ → x ∈ ℝ + ⟼ ϕ ⁡ N ⁢ ∑ n ∈ 1 … x ∩ T Λ ⁡ n n − log ⁡ x ⁢ 1 − y ∈ Base DChr ⁡ N ∖ 0 DChr ⁡ N | ∑ m ∈ ℕ y ⁡ L ⁡ m m = 0 ∈ 𝑂⁡1
39 35 38 eqeltrrd ⊢ φ → x ∈ ℝ + ⟼ ϕ ⁡ N ⁢ ∑ n ∈ 1 … x ∩ T Λ ⁡ n n − log ⁡ x ∈ 𝑂⁡1