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 e. ZZ -> ( theta ` N ) = sum_ n e. ( ( 1 ... N ) i^i Prime ) ( log ` n ) )

Proof

Step Hyp Ref Expression
1 zre 
 |-  ( N e. ZZ -> N e. RR )
2 chtval 
 |-  ( N e. RR -> ( theta ` N ) = sum_ n e. ( ( 0 [,] N ) i^i Prime ) ( log ` n ) )
3 1 2 syl 
 |-  ( N e. ZZ -> ( theta ` N ) = sum_ n e. ( ( 0 [,] N ) i^i Prime ) ( log ` n ) )
4 nnz 
 |-  ( N e. NN -> N e. ZZ )
5 ppisval 
 |-  ( N e. RR -> ( ( 0 [,] N ) i^i Prime ) = ( ( 2 ... ( |_ ` N ) ) i^i Prime ) )
6 1 5 syl 
 |-  ( N e. ZZ -> ( ( 0 [,] N ) i^i Prime ) = ( ( 2 ... ( |_ ` N ) ) i^i Prime ) )
7 flid 
 |-  ( N e. ZZ -> ( |_ ` N ) = N )
8 7 oveq2d 
 |-  ( N e. ZZ -> ( 2 ... ( |_ ` N ) ) = ( 2 ... N ) )
9 8 ineq1d 
 |-  ( N e. ZZ -> ( ( 2 ... ( |_ ` N ) ) i^i Prime ) = ( ( 2 ... N ) i^i Prime ) )
10 6 9 eqtrd 
 |-  ( N e. ZZ -> ( ( 0 [,] N ) i^i Prime ) = ( ( 2 ... N ) i^i Prime ) )
11 4 10 syl 
 |-  ( N e. NN -> ( ( 0 [,] N ) i^i Prime ) = ( ( 2 ... N ) i^i Prime ) )
12 2nn 
 |-  2 e. NN
13 nnuz 
 |-  NN = ( ZZ>= ` 1 )
14 12 13 eleqtri 
 |-  2 e. ( ZZ>= ` 1 )
15 fzss1 
 |-  ( 2 e. ( ZZ>= ` 1 ) -> ( 2 ... N ) C_ ( 1 ... N ) )
16 14 15 ax-mp 
 |-  ( 2 ... N ) C_ ( 1 ... N )
17 ssdif0 
 |-  ( ( 2 ... N ) C_ ( 1 ... N ) <-> ( ( 2 ... N ) \ ( 1 ... N ) ) = (/) )
18 16 17 mpbi 
 |-  ( ( 2 ... N ) \ ( 1 ... N ) ) = (/)
19 18 ineq1i 
 |-  ( ( ( 2 ... N ) \ ( 1 ... N ) ) i^i Prime ) = ( (/) i^i Prime )
20 0in 
 |-  ( (/) i^i Prime ) = (/)
21 19 20 eqtri 
 |-  ( ( ( 2 ... N ) \ ( 1 ... N ) ) i^i Prime ) = (/)
22 21 a1i 
 |-  ( N e. NN -> ( ( ( 2 ... N ) \ ( 1 ... N ) ) i^i Prime ) = (/) )
23 13 eleq2i 
 |-  ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
24 fzpred 
 |-  ( N e. ( ZZ>= ` 1 ) -> ( 1 ... N ) = ( { 1 } u. ( ( 1 + 1 ) ... N ) ) )
25 23 24 sylbi 
 |-  ( N e. NN -> ( 1 ... N ) = ( { 1 } u. ( ( 1 + 1 ) ... N ) ) )
26 25 eqcomd 
 |-  ( N e. NN -> ( { 1 } u. ( ( 1 + 1 ) ... N ) ) = ( 1 ... N ) )
27 1p1e2 
 |-  ( 1 + 1 ) = 2
28 27 oveq1i 
 |-  ( ( 1 + 1 ) ... N ) = ( 2 ... N )
29 28 a1i 
 |-  ( N e. NN -> ( ( 1 + 1 ) ... N ) = ( 2 ... N ) )
30 26 29 difeq12d 
 |-  ( N e. NN -> ( ( { 1 } u. ( ( 1 + 1 ) ... N ) ) \ ( ( 1 + 1 ) ... N ) ) = ( ( 1 ... N ) \ ( 2 ... N ) ) )
31 difun2 
 |-  ( ( { 1 } u. ( ( 1 + 1 ) ... N ) ) \ ( ( 1 + 1 ) ... N ) ) = ( { 1 } \ ( ( 1 + 1 ) ... N ) )
32 fzpreddisj 
 |-  ( N e. ( ZZ>= ` 1 ) -> ( { 1 } i^i ( ( 1 + 1 ) ... N ) ) = (/) )
33 23 32 sylbi 
 |-  ( N e. NN -> ( { 1 } i^i ( ( 1 + 1 ) ... N ) ) = (/) )
34 disjdif2 
 |-  ( ( { 1 } i^i ( ( 1 + 1 ) ... N ) ) = (/) -> ( { 1 } \ ( ( 1 + 1 ) ... N ) ) = { 1 } )
35 33 34 syl 
 |-  ( N e. NN -> ( { 1 } \ ( ( 1 + 1 ) ... N ) ) = { 1 } )
36 31 35 eqtrid 
 |-  ( N e. NN -> ( ( { 1 } u. ( ( 1 + 1 ) ... N ) ) \ ( ( 1 + 1 ) ... N ) ) = { 1 } )
37 30 36 eqtr3d 
 |-  ( N e. NN -> ( ( 1 ... N ) \ ( 2 ... N ) ) = { 1 } )
38 37 ineq1d 
 |-  ( N e. NN -> ( ( ( 1 ... N ) \ ( 2 ... N ) ) i^i Prime ) = ( { 1 } i^i Prime ) )
39 incom 
 |-  ( Prime i^i { 1 } ) = ( { 1 } i^i Prime )
40 1nprm 
 |-  -. 1 e. Prime
41 disjsn 
 |-  ( ( Prime i^i { 1 } ) = (/) <-> -. 1 e. Prime )
42 40 41 mpbir 
 |-  ( Prime i^i { 1 } ) = (/)
43 39 42 eqtr3i 
 |-  ( { 1 } i^i Prime ) = (/)
44 38 43 eqtrdi 
 |-  ( N e. NN -> ( ( ( 1 ... N ) \ ( 2 ... N ) ) i^i Prime ) = (/) )
45 difininv 
 |-  ( ( ( ( ( 2 ... N ) \ ( 1 ... N ) ) i^i Prime ) = (/) /\ ( ( ( 1 ... N ) \ ( 2 ... N ) ) i^i Prime ) = (/) ) -> ( ( 2 ... N ) i^i Prime ) = ( ( 1 ... N ) i^i Prime ) )
46 22 44 45 syl2anc 
 |-  ( N e. NN -> ( ( 2 ... N ) i^i Prime ) = ( ( 1 ... N ) i^i Prime ) )
47 11 46 eqtrd 
 |-  ( N e. NN -> ( ( 0 [,] N ) i^i Prime ) = ( ( 1 ... N ) i^i Prime ) )
48 47 adantl 
 |-  ( ( N e. ZZ /\ N e. NN ) -> ( ( 0 [,] N ) i^i Prime ) = ( ( 1 ... N ) i^i Prime ) )
49 znnnlt1 
 |-  ( N e. ZZ -> ( -. N e. NN <-> N < 1 ) )
50 49 biimpa 
 |-  ( ( N e. ZZ /\ -. N e. NN ) -> N < 1 )
51 incom 
 |-  ( ( 0 [,] N ) i^i Prime ) = ( Prime i^i ( 0 [,] N ) )
52 isprm3 
 |-  ( n e. Prime <-> ( n e. ( ZZ>= ` 2 ) /\ A. i e. ( 2 ... ( n - 1 ) ) -. i || n ) )
53 52 simplbi 
 |-  ( n e. Prime -> n e. ( ZZ>= ` 2 ) )
54 53 ssriv 
 |-  Prime C_ ( ZZ>= ` 2 )
55 12 nnzi 
 |-  2 e. ZZ
56 uzssico 
 |-  ( 2 e. ZZ -> ( ZZ>= ` 2 ) C_ ( 2 [,) +oo ) )
57 55 56 ax-mp 
 |-  ( ZZ>= ` 2 ) C_ ( 2 [,) +oo )
58 54 57 sstri 
 |-  Prime C_ ( 2 [,) +oo )
59 incom 
 |-  ( ( 0 [,] N ) i^i ( 2 [,) +oo ) ) = ( ( 2 [,) +oo ) i^i ( 0 [,] N ) )
60 0xr 
 |-  0 e. RR*
61 60 a1i 
 |-  ( ( N e. ZZ /\ N < 1 ) -> 0 e. RR* )
62 12 nnrei 
 |-  2 e. RR
63 62 rexri 
 |-  2 e. RR*
64 63 a1i 
 |-  ( ( N e. ZZ /\ N < 1 ) -> 2 e. RR* )
65 0le0 
 |-  0 <_ 0
66 65 a1i 
 |-  ( ( N e. ZZ /\ N < 1 ) -> 0 <_ 0 )
67 1 adantr 
 |-  ( ( N e. ZZ /\ N < 1 ) -> N e. RR )
68 1red 
 |-  ( ( N e. ZZ /\ N < 1 ) -> 1 e. RR )
69 62 a1i 
 |-  ( ( N e. ZZ /\ N < 1 ) -> 2 e. RR )
70 simpr 
 |-  ( ( N e. ZZ /\ N < 1 ) -> N < 1 )
71 1lt2 
 |-  1 < 2
72 71 a1i 
 |-  ( ( N e. ZZ /\ N < 1 ) -> 1 < 2 )
73 67 68 69 70 72 lttrd 
 |-  ( ( N e. ZZ /\ N < 1 ) -> N < 2 )
74 iccssico 
 |-  ( ( ( 0 e. RR* /\ 2 e. RR* ) /\ ( 0 <_ 0 /\ N < 2 ) ) -> ( 0 [,] N ) C_ ( 0 [,) 2 ) )
75 61 64 66 73 74 syl22anc 
 |-  ( ( N e. ZZ /\ N < 1 ) -> ( 0 [,] N ) C_ ( 0 [,) 2 ) )
76 pnfxr 
 |-  +oo e. RR*
77 icodisj 
 |-  ( ( 0 e. RR* /\ 2 e. RR* /\ +oo e. RR* ) -> ( ( 0 [,) 2 ) i^i ( 2 [,) +oo ) ) = (/) )
78 60 63 76 77 mp3an 
 |-  ( ( 0 [,) 2 ) i^i ( 2 [,) +oo ) ) = (/)
79 ssdisj 
 |-  ( ( ( 0 [,] N ) C_ ( 0 [,) 2 ) /\ ( ( 0 [,) 2 ) i^i ( 2 [,) +oo ) ) = (/) ) -> ( ( 0 [,] N ) i^i ( 2 [,) +oo ) ) = (/) )
80 75 78 79 sylancl 
 |-  ( ( N e. ZZ /\ N < 1 ) -> ( ( 0 [,] N ) i^i ( 2 [,) +oo ) ) = (/) )
81 59 80 eqtr3id 
 |-  ( ( N e. ZZ /\ N < 1 ) -> ( ( 2 [,) +oo ) i^i ( 0 [,] N ) ) = (/) )
82 ssdisj 
 |-  ( ( Prime C_ ( 2 [,) +oo ) /\ ( ( 2 [,) +oo ) i^i ( 0 [,] N ) ) = (/) ) -> ( Prime i^i ( 0 [,] N ) ) = (/) )
83 58 81 82 sylancr 
 |-  ( ( N e. ZZ /\ N < 1 ) -> ( Prime i^i ( 0 [,] N ) ) = (/) )
84 51 83 eqtrid 
 |-  ( ( N e. ZZ /\ N < 1 ) -> ( ( 0 [,] N ) i^i Prime ) = (/) )
85 1zzd 
 |-  ( ( N e. ZZ /\ N < 1 ) -> 1 e. ZZ )
86 simpl 
 |-  ( ( N e. ZZ /\ N < 1 ) -> N e. ZZ )
87 fzn 
 |-  ( ( 1 e. ZZ /\ N e. ZZ ) -> ( N < 1 <-> ( 1 ... N ) = (/) ) )
88 87 biimpa 
 |-  ( ( ( 1 e. ZZ /\ N e. ZZ ) /\ N < 1 ) -> ( 1 ... N ) = (/) )
89 85 86 70 88 syl21anc 
 |-  ( ( N e. ZZ /\ N < 1 ) -> ( 1 ... N ) = (/) )
90 89 ineq1d 
 |-  ( ( N e. ZZ /\ N < 1 ) -> ( ( 1 ... N ) i^i Prime ) = ( (/) i^i Prime ) )
91 90 20 eqtrdi 
 |-  ( ( N e. ZZ /\ N < 1 ) -> ( ( 1 ... N ) i^i Prime ) = (/) )
92 84 91 eqtr4d 
 |-  ( ( N e. ZZ /\ N < 1 ) -> ( ( 0 [,] N ) i^i Prime ) = ( ( 1 ... N ) i^i Prime ) )
93 50 92 syldan 
 |-  ( ( N e. ZZ /\ -. N e. NN ) -> ( ( 0 [,] N ) i^i Prime ) = ( ( 1 ... N ) i^i Prime ) )
94 exmidd 
 |-  ( N e. ZZ -> ( N e. NN \/ -. N e. NN ) )
95 48 93 94 mpjaodan 
 |-  ( N e. ZZ -> ( ( 0 [,] N ) i^i Prime ) = ( ( 1 ... N ) i^i Prime ) )
96 95 sumeq1d 
 |-  ( N e. ZZ -> sum_ n e. ( ( 0 [,] N ) i^i Prime ) ( log ` n ) = sum_ n e. ( ( 1 ... N ) i^i Prime ) ( log ` n ) )
97 3 96 eqtrd 
 |-  ( N e. ZZ -> ( theta ` N ) = sum_ n e. ( ( 1 ... N ) i^i Prime ) ( log ` n ) )