Metamath Proof Explorer


Theorem chtvalz

Description: Value of the Chebyshev function for integers. (Contributed by Thierry Arnoux, 28-Dec-2021)

Ref Expression
Assertion chtvalz ( 𝑁 ∈ ℤ → ( θ ‘ 𝑁 ) = Σ 𝑛 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( log ‘ 𝑛 ) )

Proof

Step Hyp Ref Expression
1 zre ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
2 chtval ( 𝑁 ∈ ℝ → ( θ ‘ 𝑁 ) = Σ 𝑛 ∈ ( ( 0 [,] 𝑁 ) ∩ ℙ ) ( log ‘ 𝑛 ) )
3 1 2 syl ( 𝑁 ∈ ℤ → ( θ ‘ 𝑁 ) = Σ 𝑛 ∈ ( ( 0 [,] 𝑁 ) ∩ ℙ ) ( log ‘ 𝑛 ) )
4 nnz ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
5 ppisval ( 𝑁 ∈ ℝ → ( ( 0 [,] 𝑁 ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) )
6 1 5 syl ( 𝑁 ∈ ℤ → ( ( 0 [,] 𝑁 ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) )
7 flid ( 𝑁 ∈ ℤ → ( ⌊ ‘ 𝑁 ) = 𝑁 )
8 7 oveq2d ( 𝑁 ∈ ℤ → ( 2 ... ( ⌊ ‘ 𝑁 ) ) = ( 2 ... 𝑁 ) )
9 8 ineq1d ( 𝑁 ∈ ℤ → ( ( 2 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) = ( ( 2 ... 𝑁 ) ∩ ℙ ) )
10 6 9 eqtrd ( 𝑁 ∈ ℤ → ( ( 0 [,] 𝑁 ) ∩ ℙ ) = ( ( 2 ... 𝑁 ) ∩ ℙ ) )
11 4 10 syl ( 𝑁 ∈ ℕ → ( ( 0 [,] 𝑁 ) ∩ ℙ ) = ( ( 2 ... 𝑁 ) ∩ ℙ ) )
12 2nn 2 ∈ ℕ
13 nnuz ℕ = ( ℤ ‘ 1 )
14 12 13 eleqtri 2 ∈ ( ℤ ‘ 1 )
15 fzss1 ( 2 ∈ ( ℤ ‘ 1 ) → ( 2 ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
16 14 15 ax-mp ( 2 ... 𝑁 ) ⊆ ( 1 ... 𝑁 )
17 ssdif0 ( ( 2 ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) ↔ ( ( 2 ... 𝑁 ) ∖ ( 1 ... 𝑁 ) ) = ∅ )
18 16 17 mpbi ( ( 2 ... 𝑁 ) ∖ ( 1 ... 𝑁 ) ) = ∅
19 18 ineq1i ( ( ( 2 ... 𝑁 ) ∖ ( 1 ... 𝑁 ) ) ∩ ℙ ) = ( ∅ ∩ ℙ )
20 0in ( ∅ ∩ ℙ ) = ∅
21 19 20 eqtri ( ( ( 2 ... 𝑁 ) ∖ ( 1 ... 𝑁 ) ) ∩ ℙ ) = ∅
22 21 a1i ( 𝑁 ∈ ℕ → ( ( ( 2 ... 𝑁 ) ∖ ( 1 ... 𝑁 ) ) ∩ ℙ ) = ∅ )
23 13 eleq2i ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ ‘ 1 ) )
24 fzpred ( 𝑁 ∈ ( ℤ ‘ 1 ) → ( 1 ... 𝑁 ) = ( { 1 } ∪ ( ( 1 + 1 ) ... 𝑁 ) ) )
25 23 24 sylbi ( 𝑁 ∈ ℕ → ( 1 ... 𝑁 ) = ( { 1 } ∪ ( ( 1 + 1 ) ... 𝑁 ) ) )
26 25 eqcomd ( 𝑁 ∈ ℕ → ( { 1 } ∪ ( ( 1 + 1 ) ... 𝑁 ) ) = ( 1 ... 𝑁 ) )
27 1p1e2 ( 1 + 1 ) = 2
28 27 oveq1i ( ( 1 + 1 ) ... 𝑁 ) = ( 2 ... 𝑁 )
29 28 a1i ( 𝑁 ∈ ℕ → ( ( 1 + 1 ) ... 𝑁 ) = ( 2 ... 𝑁 ) )
30 26 29 difeq12d ( 𝑁 ∈ ℕ → ( ( { 1 } ∪ ( ( 1 + 1 ) ... 𝑁 ) ) ∖ ( ( 1 + 1 ) ... 𝑁 ) ) = ( ( 1 ... 𝑁 ) ∖ ( 2 ... 𝑁 ) ) )
31 difun2 ( ( { 1 } ∪ ( ( 1 + 1 ) ... 𝑁 ) ) ∖ ( ( 1 + 1 ) ... 𝑁 ) ) = ( { 1 } ∖ ( ( 1 + 1 ) ... 𝑁 ) )
32 fzpreddisj ( 𝑁 ∈ ( ℤ ‘ 1 ) → ( { 1 } ∩ ( ( 1 + 1 ) ... 𝑁 ) ) = ∅ )
33 23 32 sylbi ( 𝑁 ∈ ℕ → ( { 1 } ∩ ( ( 1 + 1 ) ... 𝑁 ) ) = ∅ )
34 disjdif2 ( ( { 1 } ∩ ( ( 1 + 1 ) ... 𝑁 ) ) = ∅ → ( { 1 } ∖ ( ( 1 + 1 ) ... 𝑁 ) ) = { 1 } )
35 33 34 syl ( 𝑁 ∈ ℕ → ( { 1 } ∖ ( ( 1 + 1 ) ... 𝑁 ) ) = { 1 } )
36 31 35 syl5eq ( 𝑁 ∈ ℕ → ( ( { 1 } ∪ ( ( 1 + 1 ) ... 𝑁 ) ) ∖ ( ( 1 + 1 ) ... 𝑁 ) ) = { 1 } )
37 30 36 eqtr3d ( 𝑁 ∈ ℕ → ( ( 1 ... 𝑁 ) ∖ ( 2 ... 𝑁 ) ) = { 1 } )
38 37 ineq1d ( 𝑁 ∈ ℕ → ( ( ( 1 ... 𝑁 ) ∖ ( 2 ... 𝑁 ) ) ∩ ℙ ) = ( { 1 } ∩ ℙ ) )
39 incom ( ℙ ∩ { 1 } ) = ( { 1 } ∩ ℙ )
40 1nprm ¬ 1 ∈ ℙ
41 disjsn ( ( ℙ ∩ { 1 } ) = ∅ ↔ ¬ 1 ∈ ℙ )
42 40 41 mpbir ( ℙ ∩ { 1 } ) = ∅
43 39 42 eqtr3i ( { 1 } ∩ ℙ ) = ∅
44 38 43 eqtrdi ( 𝑁 ∈ ℕ → ( ( ( 1 ... 𝑁 ) ∖ ( 2 ... 𝑁 ) ) ∩ ℙ ) = ∅ )
45 difininv ( ( ( ( ( 2 ... 𝑁 ) ∖ ( 1 ... 𝑁 ) ) ∩ ℙ ) = ∅ ∧ ( ( ( 1 ... 𝑁 ) ∖ ( 2 ... 𝑁 ) ) ∩ ℙ ) = ∅ ) → ( ( 2 ... 𝑁 ) ∩ ℙ ) = ( ( 1 ... 𝑁 ) ∩ ℙ ) )
46 22 44 45 syl2anc ( 𝑁 ∈ ℕ → ( ( 2 ... 𝑁 ) ∩ ℙ ) = ( ( 1 ... 𝑁 ) ∩ ℙ ) )
47 11 46 eqtrd ( 𝑁 ∈ ℕ → ( ( 0 [,] 𝑁 ) ∩ ℙ ) = ( ( 1 ... 𝑁 ) ∩ ℙ ) )
48 47 adantl ( ( 𝑁 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 0 [,] 𝑁 ) ∩ ℙ ) = ( ( 1 ... 𝑁 ) ∩ ℙ ) )
49 znnnlt1 ( 𝑁 ∈ ℤ → ( ¬ 𝑁 ∈ ℕ ↔ 𝑁 < 1 ) )
50 49 biimpa ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 ∈ ℕ ) → 𝑁 < 1 )
51 incom ( ( 0 [,] 𝑁 ) ∩ ℙ ) = ( ℙ ∩ ( 0 [,] 𝑁 ) )
52 isprm3 ( 𝑛 ∈ ℙ ↔ ( 𝑛 ∈ ( ℤ ‘ 2 ) ∧ ∀ 𝑖 ∈ ( 2 ... ( 𝑛 − 1 ) ) ¬ 𝑖𝑛 ) )
53 52 simplbi ( 𝑛 ∈ ℙ → 𝑛 ∈ ( ℤ ‘ 2 ) )
54 53 ssriv ℙ ⊆ ( ℤ ‘ 2 )
55 12 nnzi 2 ∈ ℤ
56 uzssico ( 2 ∈ ℤ → ( ℤ ‘ 2 ) ⊆ ( 2 [,) +∞ ) )
57 55 56 ax-mp ( ℤ ‘ 2 ) ⊆ ( 2 [,) +∞ )
58 54 57 sstri ℙ ⊆ ( 2 [,) +∞ )
59 incom ( ( 0 [,] 𝑁 ) ∩ ( 2 [,) +∞ ) ) = ( ( 2 [,) +∞ ) ∩ ( 0 [,] 𝑁 ) )
60 0xr 0 ∈ ℝ*
61 60 a1i ( ( 𝑁 ∈ ℤ ∧ 𝑁 < 1 ) → 0 ∈ ℝ* )
62 12 nnrei 2 ∈ ℝ
63 62 rexri 2 ∈ ℝ*
64 63 a1i ( ( 𝑁 ∈ ℤ ∧ 𝑁 < 1 ) → 2 ∈ ℝ* )
65 0le0 0 ≤ 0
66 65 a1i ( ( 𝑁 ∈ ℤ ∧ 𝑁 < 1 ) → 0 ≤ 0 )
67 1 adantr ( ( 𝑁 ∈ ℤ ∧ 𝑁 < 1 ) → 𝑁 ∈ ℝ )
68 1red ( ( 𝑁 ∈ ℤ ∧ 𝑁 < 1 ) → 1 ∈ ℝ )
69 62 a1i ( ( 𝑁 ∈ ℤ ∧ 𝑁 < 1 ) → 2 ∈ ℝ )
70 simpr ( ( 𝑁 ∈ ℤ ∧ 𝑁 < 1 ) → 𝑁 < 1 )
71 1lt2 1 < 2
72 71 a1i ( ( 𝑁 ∈ ℤ ∧ 𝑁 < 1 ) → 1 < 2 )
73 67 68 69 70 72 lttrd ( ( 𝑁 ∈ ℤ ∧ 𝑁 < 1 ) → 𝑁 < 2 )
74 iccssico ( ( ( 0 ∈ ℝ* ∧ 2 ∈ ℝ* ) ∧ ( 0 ≤ 0 ∧ 𝑁 < 2 ) ) → ( 0 [,] 𝑁 ) ⊆ ( 0 [,) 2 ) )
75 61 64 66 73 74 syl22anc ( ( 𝑁 ∈ ℤ ∧ 𝑁 < 1 ) → ( 0 [,] 𝑁 ) ⊆ ( 0 [,) 2 ) )
76 pnfxr +∞ ∈ ℝ*
77 icodisj ( ( 0 ∈ ℝ* ∧ 2 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( 0 [,) 2 ) ∩ ( 2 [,) +∞ ) ) = ∅ )
78 60 63 76 77 mp3an ( ( 0 [,) 2 ) ∩ ( 2 [,) +∞ ) ) = ∅
79 ssdisj ( ( ( 0 [,] 𝑁 ) ⊆ ( 0 [,) 2 ) ∧ ( ( 0 [,) 2 ) ∩ ( 2 [,) +∞ ) ) = ∅ ) → ( ( 0 [,] 𝑁 ) ∩ ( 2 [,) +∞ ) ) = ∅ )
80 75 78 79 sylancl ( ( 𝑁 ∈ ℤ ∧ 𝑁 < 1 ) → ( ( 0 [,] 𝑁 ) ∩ ( 2 [,) +∞ ) ) = ∅ )
81 59 80 eqtr3id ( ( 𝑁 ∈ ℤ ∧ 𝑁 < 1 ) → ( ( 2 [,) +∞ ) ∩ ( 0 [,] 𝑁 ) ) = ∅ )
82 ssdisj ( ( ℙ ⊆ ( 2 [,) +∞ ) ∧ ( ( 2 [,) +∞ ) ∩ ( 0 [,] 𝑁 ) ) = ∅ ) → ( ℙ ∩ ( 0 [,] 𝑁 ) ) = ∅ )
83 58 81 82 sylancr ( ( 𝑁 ∈ ℤ ∧ 𝑁 < 1 ) → ( ℙ ∩ ( 0 [,] 𝑁 ) ) = ∅ )
84 51 83 syl5eq ( ( 𝑁 ∈ ℤ ∧ 𝑁 < 1 ) → ( ( 0 [,] 𝑁 ) ∩ ℙ ) = ∅ )
85 1zzd ( ( 𝑁 ∈ ℤ ∧ 𝑁 < 1 ) → 1 ∈ ℤ )
86 simpl ( ( 𝑁 ∈ ℤ ∧ 𝑁 < 1 ) → 𝑁 ∈ ℤ )
87 fzn ( ( 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 < 1 ↔ ( 1 ... 𝑁 ) = ∅ ) )
88 87 biimpa ( ( ( 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 < 1 ) → ( 1 ... 𝑁 ) = ∅ )
89 85 86 70 88 syl21anc ( ( 𝑁 ∈ ℤ ∧ 𝑁 < 1 ) → ( 1 ... 𝑁 ) = ∅ )
90 89 ineq1d ( ( 𝑁 ∈ ℤ ∧ 𝑁 < 1 ) → ( ( 1 ... 𝑁 ) ∩ ℙ ) = ( ∅ ∩ ℙ ) )
91 90 20 eqtrdi ( ( 𝑁 ∈ ℤ ∧ 𝑁 < 1 ) → ( ( 1 ... 𝑁 ) ∩ ℙ ) = ∅ )
92 84 91 eqtr4d ( ( 𝑁 ∈ ℤ ∧ 𝑁 < 1 ) → ( ( 0 [,] 𝑁 ) ∩ ℙ ) = ( ( 1 ... 𝑁 ) ∩ ℙ ) )
93 50 92 syldan ( ( 𝑁 ∈ ℤ ∧ ¬ 𝑁 ∈ ℕ ) → ( ( 0 [,] 𝑁 ) ∩ ℙ ) = ( ( 1 ... 𝑁 ) ∩ ℙ ) )
94 exmidd ( 𝑁 ∈ ℤ → ( 𝑁 ∈ ℕ ∨ ¬ 𝑁 ∈ ℕ ) )
95 48 93 94 mpjaodan ( 𝑁 ∈ ℤ → ( ( 0 [,] 𝑁 ) ∩ ℙ ) = ( ( 1 ... 𝑁 ) ∩ ℙ ) )
96 95 sumeq1d ( 𝑁 ∈ ℤ → Σ 𝑛 ∈ ( ( 0 [,] 𝑁 ) ∩ ℙ ) ( log ‘ 𝑛 ) = Σ 𝑛 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( log ‘ 𝑛 ) )
97 3 96 eqtrd ( 𝑁 ∈ ℤ → ( θ ‘ 𝑁 ) = Σ 𝑛 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( log ‘ 𝑛 ) )