Metamath Proof Explorer


Theorem chtvalz

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

Ref Expression
Assertion chtvalz N θ N = n 1 N log n

Proof

Step Hyp Ref Expression
1 zre N N
2 chtval N θ N = n 0 N log n
3 1 2 syl N θ N = n 0 N log n
4 nnz N N
5 ppisval N 0 N = 2 N
6 1 5 syl N 0 N = 2 N
7 flid N N = N
8 7 oveq2d N 2 N = 2 N
9 8 ineq1d N 2 N = 2 N
10 6 9 eqtrd N 0 N = 2 N
11 4 10 syl N 0 N = 2 N
12 2nn 2
13 nnuz = 1
14 12 13 eleqtri 2 1
15 fzss1 2 1 2 N 1 N
16 14 15 ax-mp 2 N 1 N
17 ssdif0 2 N 1 N 2 N 1 N =
18 16 17 mpbi 2 N 1 N =
19 18 ineq1i 2 N 1 N =
20 0in =
21 19 20 eqtri 2 N 1 N =
22 21 a1i N 2 N 1 N =
23 13 eleq2i N N 1
24 fzpred N 1 1 N = 1 1 + 1 N
25 23 24 sylbi N 1 N = 1 1 + 1 N
26 25 eqcomd N 1 1 + 1 N = 1 N
27 1p1e2 1 + 1 = 2
28 27 oveq1i 1 + 1 N = 2 N
29 28 a1i N 1 + 1 N = 2 N
30 26 29 difeq12d N 1 1 + 1 N 1 + 1 N = 1 N 2 N
31 difun2 1 1 + 1 N 1 + 1 N = 1 1 + 1 N
32 fzpreddisj N 1 1 1 + 1 N =
33 23 32 sylbi N 1 1 + 1 N =
34 disjdif2 1 1 + 1 N = 1 1 + 1 N = 1
35 33 34 syl N 1 1 + 1 N = 1
36 31 35 syl5eq N 1 1 + 1 N 1 + 1 N = 1
37 30 36 eqtr3d N 1 N 2 N = 1
38 37 ineq1d N 1 N 2 N = 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 N 1 N 2 N =
45 difininv 2 N 1 N = 1 N 2 N = 2 N = 1 N
46 22 44 45 syl2anc N 2 N = 1 N
47 11 46 eqtrd N 0 N = 1 N
48 47 adantl N N 0 N = 1 N
49 znnnlt1 N ¬ N N < 1
50 49 biimpa N ¬ N N < 1
51 incom 0 N = 0 N
52 isprm3 n n 2 i 2 n 1 ¬ i n
53 52 simplbi n n 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 N 2 +∞ = 2 +∞ 0 N
60 0xr 0 *
61 60 a1i N N < 1 0 *
62 12 nnrei 2
63 62 rexri 2 *
64 63 a1i N N < 1 2 *
65 0le0 0 0
66 65 a1i N N < 1 0 0
67 1 adantr N N < 1 N
68 1red N N < 1 1
69 62 a1i N N < 1 2
70 simpr N N < 1 N < 1
71 1lt2 1 < 2
72 71 a1i N N < 1 1 < 2
73 67 68 69 70 72 lttrd N N < 1 N < 2
74 iccssico 0 * 2 * 0 0 N < 2 0 N 0 2
75 61 64 66 73 74 syl22anc N N < 1 0 N 0 2
76 pnfxr +∞ *
77 icodisj 0 * 2 * +∞ * 0 2 2 +∞ =
78 60 63 76 77 mp3an 0 2 2 +∞ =
79 ssdisj 0 N 0 2 0 2 2 +∞ = 0 N 2 +∞ =
80 75 78 79 sylancl N N < 1 0 N 2 +∞ =
81 59 80 eqtr3id N N < 1 2 +∞ 0 N =
82 ssdisj 2 +∞ 2 +∞ 0 N = 0 N =
83 58 81 82 sylancr N N < 1 0 N =
84 51 83 syl5eq N N < 1 0 N =
85 1zzd N N < 1 1
86 simpl N N < 1 N
87 fzn 1 N N < 1 1 N =
88 87 biimpa 1 N N < 1 1 N =
89 85 86 70 88 syl21anc N N < 1 1 N =
90 89 ineq1d N N < 1 1 N =
91 90 20 eqtrdi N N < 1 1 N =
92 84 91 eqtr4d N N < 1 0 N = 1 N
93 50 92 syldan N ¬ N 0 N = 1 N
94 exmidd N N ¬ N
95 48 93 94 mpjaodan N 0 N = 1 N
96 95 sumeq1d N n 0 N log n = n 1 N log n
97 3 96 eqtrd N θ N = n 1 N log n