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