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 syl5eq
 |-  ( 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 syl5eq
 |-  ( ( 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 ) )