Metamath Proof Explorer

Theorem chpval2

Description: Express the second Chebyshev function directly as a sum over the primes less than A (instead of indirectly through the von Mangoldt function). (Contributed by Mario Carneiro, 8-Apr-2016)

Ref Expression
Assertion chpval2 ( 𝐴 ∈ ℝ → ( ψ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 chpval ⊢ ( 𝐴 ∈ ℝ → ( ψ ‘ 𝐴 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( Λ ‘ 𝑛 ) )
2 fveq2 ⊢ ( 𝑛 = ( 𝑝 ↑ 𝑘 ) → ( Λ ‘ 𝑛 ) = ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) )
3 id ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ )
4 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑛 ∈ ℕ )
5 4 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℕ )
6 vmacl ⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
7 5 6 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
8 7 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℂ )
9 simprr ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ( Λ ‘ 𝑛 ) = 0 )
10 2 3 8 9 fsumvma2 ⊢ ( 𝐴 ∈ ℝ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( Λ ‘ 𝑛 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) )
11 simpr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) )
12 11 elin2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℙ )
13 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) → 𝑘 ∈ ℕ )
14 vmappw ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) = ( log ‘ 𝑝 ) )
15 12 13 14 syl2an ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) = ( log ‘ 𝑝 ) )
16 15 sumeq2dv ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( log ‘ 𝑝 ) )
17 fzfid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ∈ Fin )
18 prmuz2 ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
19 eluzelre ⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) → 𝑝 ∈ ℝ )
20 eluz2gt1 ⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝑝 )
21 19 20 rplogcld ⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) → ( log ‘ 𝑝 ) ∈ ℝ+ )
22 12 18 21 3syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ+ )
23 22 rpcnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℂ )
24 fsumconst ⊢ ( ( ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ∈ Fin ∧ ( log ‘ 𝑝 ) ∈ ℂ ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( log ‘ 𝑝 ) = ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) · ( log ‘ 𝑝 ) ) )
25 17 23 24 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( log ‘ 𝑝 ) = ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) · ( log ‘ 𝑝 ) ) )
26 ppisval ⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )
27 inss1 ⊢ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ⊆ ( 2 ... ( ⌊ ‘ 𝐴 ) )
28 26 27 eqsstrdi ⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ⊆ ( 2 ... ( ⌊ ‘ 𝐴 ) ) )
29 28 sselda ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( 2 ... ( ⌊ ‘ 𝐴 ) ) )
30 elfzuz2 ⊢ ( 𝑝 ∈ ( 2 ... ( ⌊ ‘ 𝐴 ) ) → ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) )
31 29 30 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) )
32 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) ) → 𝐴 ∈ ℝ )
33 0red ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) ) → 0 ∈ ℝ )
34 2re ⊢ 2 ∈ ℝ
35 34 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) ) → 2 ∈ ℝ )
36 2pos ⊢ 0 < 2
37 36 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) ) → 0 < 2 )
38 eluzle ⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ ( ⌊ ‘ 𝐴 ) )
39 2z ⊢ 2 ∈ ℤ
40 flge ⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ℤ ) → ( 2 ≤ 𝐴 ↔ 2 ≤ ( ⌊ ‘ 𝐴 ) ) )
41 39 40 mpan2 ⊢ ( 𝐴 ∈ ℝ → ( 2 ≤ 𝐴 ↔ 2 ≤ ( ⌊ ‘ 𝐴 ) ) )
42 38 41 imbitrrid ⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ 𝐴 ) )
43 42 imp ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) ) → 2 ≤ 𝐴 )
44 33 35 32 37 43 ltletrd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) ) → 0 < 𝐴 )
45 32 44 elrpd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) ) → 𝐴 ∈ ℝ+ )
46 31 45 syldan ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝐴 ∈ ℝ+ )
47 46 relogcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝐴 ) ∈ ℝ )
48 47 22 rerpdivcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ )
49 1red ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) ) → 1 ∈ ℝ )
50 1lt2 ⊢ 1 < 2
51 50 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) ) → 1 < 2 )
52 49 35 32 51 43 ltletrd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) ) → 1 < 𝐴 )
53 31 52 syldan ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 1 < 𝐴 )
54 rplogcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( log ‘ 𝐴 ) ∈ ℝ+ )
55 53 54 syldan ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝐴 ) ∈ ℝ+ )
56 55 22 rpdivcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ+ )
57 56 rpge0d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 0 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) )
58 flge0nn0 ⊢ ( ( ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ ∧ 0 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℕ0 )
59 48 57 58 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℕ0 )
60 hashfz1 ⊢ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) = ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) )
61 59 60 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) = ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) )
62 61 oveq1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) · ( log ‘ 𝑝 ) ) = ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) · ( log ‘ 𝑝 ) ) )
63 59 nn0cnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℂ )
64 63 23 mulcomd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) · ( log ‘ 𝑝 ) ) = ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
65 25 62 64 3eqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( log ‘ 𝑝 ) = ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
66 16 65 eqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) = ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
67 66 sumeq2dv ⊢ ( 𝐴 ∈ ℝ → Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
68 1 10 67 3eqtrd ⊢ ( 𝐴 ∈ ℝ → ( ψ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )