Metamath Proof Explorer

Theorem chtprm

Description: The Chebyshev function at a prime. (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Assertion chtprm 
|- ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( theta ` ( A + 1 ) ) = ( ( theta ` A ) + ( log ` ( A + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 peano2z 
 |-  ( A e. ZZ -> ( A + 1 ) e. ZZ )
2 1 adantr 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( A + 1 ) e. ZZ )
3 zre 
 |-  ( ( A + 1 ) e. ZZ -> ( A + 1 ) e. RR )
4 2 3 syl 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( A + 1 ) e. RR )
5 chtval 
 |-  ( ( A + 1 ) e. RR -> ( theta ` ( A + 1 ) ) = sum_ p e. ( ( 0 [,] ( A + 1 ) ) i^i Prime ) ( log ` p ) )
6 4 5 syl 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( theta ` ( A + 1 ) ) = sum_ p e. ( ( 0 [,] ( A + 1 ) ) i^i Prime ) ( log ` p ) )
7 ppisval 
 |-  ( ( A + 1 ) e. RR -> ( ( 0 [,] ( A + 1 ) ) i^i Prime ) = ( ( 2 ... ( |_ ` ( A + 1 ) ) ) i^i Prime ) )
8 4 7 syl 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( ( 0 [,] ( A + 1 ) ) i^i Prime ) = ( ( 2 ... ( |_ ` ( A + 1 ) ) ) i^i Prime ) )
9 flid 
 |-  ( ( A + 1 ) e. ZZ -> ( |_ ` ( A + 1 ) ) = ( A + 1 ) )
10 2 9 syl 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( |_ ` ( A + 1 ) ) = ( A + 1 ) )
11 10 oveq2d 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( 2 ... ( |_ ` ( A + 1 ) ) ) = ( 2 ... ( A + 1 ) ) )
12 11 ineq1d 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( ( 2 ... ( |_ ` ( A + 1 ) ) ) i^i Prime ) = ( ( 2 ... ( A + 1 ) ) i^i Prime ) )
13 8 12 eqtrd 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( ( 0 [,] ( A + 1 ) ) i^i Prime ) = ( ( 2 ... ( A + 1 ) ) i^i Prime ) )
14 13 sumeq1d 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> sum_ p e. ( ( 0 [,] ( A + 1 ) ) i^i Prime ) ( log ` p ) = sum_ p e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ( log ` p ) )
15 6 14 eqtrd 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( theta ` ( A + 1 ) ) = sum_ p e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ( log ` p ) )
16 zre 
 |-  ( A e. ZZ -> A e. RR )
17 16 adantr 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> A e. RR )
18 17 ltp1d 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> A < ( A + 1 ) )
19 17 4 ltnled 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( A < ( A + 1 ) <-> -. ( A + 1 ) <_ A ) )
20 18 19 mpbid 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> -. ( A + 1 ) <_ A )
21 elinel1 
 |-  ( ( A + 1 ) e. ( ( 2 ... A ) i^i Prime ) -> ( A + 1 ) e. ( 2 ... A ) )
22 elfzle2 
 |-  ( ( A + 1 ) e. ( 2 ... A ) -> ( A + 1 ) <_ A )
23 21 22 syl 
 |-  ( ( A + 1 ) e. ( ( 2 ... A ) i^i Prime ) -> ( A + 1 ) <_ A )
24 20 23 nsyl 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> -. ( A + 1 ) e. ( ( 2 ... A ) i^i Prime ) )
25 disjsn 
 |-  ( ( ( ( 2 ... A ) i^i Prime ) i^i { ( A + 1 ) } ) = (/) <-> -. ( A + 1 ) e. ( ( 2 ... A ) i^i Prime ) )
26 24 25 sylibr 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( ( ( 2 ... A ) i^i Prime ) i^i { ( A + 1 ) } ) = (/) )
27 2z 
 |-  2 e. ZZ
28 zcn 
 |-  ( A e. ZZ -> A e. CC )
29 28 adantr 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> A e. CC )
30 ax-1cn 
 |-  1 e. CC
31 pncan 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( ( A + 1 ) - 1 ) = A )
32 29 30 31 sylancl 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( ( A + 1 ) - 1 ) = A )
33 prmuz2 
 |-  ( ( A + 1 ) e. Prime -> ( A + 1 ) e. ( ZZ>= ` 2 ) )
34 33 adantl 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( A + 1 ) e. ( ZZ>= ` 2 ) )
35 uz2m1nn 
 |-  ( ( A + 1 ) e. ( ZZ>= ` 2 ) -> ( ( A + 1 ) - 1 ) e. NN )
36 34 35 syl 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( ( A + 1 ) - 1 ) e. NN )
37 32 36 eqeltrrd 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> A e. NN )
38 nnuz 
 |-  NN = ( ZZ>= ` 1 )
39 2m1e1 
 |-  ( 2 - 1 ) = 1
40 39 fveq2i 
 |-  ( ZZ>= ` ( 2 - 1 ) ) = ( ZZ>= ` 1 )
41 38 40 eqtr4i 
 |-  NN = ( ZZ>= ` ( 2 - 1 ) )
42 37 41 eleqtrdi 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> A e. ( ZZ>= ` ( 2 - 1 ) ) )
43 fzsuc2 
 |-  ( ( 2 e. ZZ /\ A e. ( ZZ>= ` ( 2 - 1 ) ) ) -> ( 2 ... ( A + 1 ) ) = ( ( 2 ... A ) u. { ( A + 1 ) } ) )
44 27 42 43 sylancr 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( 2 ... ( A + 1 ) ) = ( ( 2 ... A ) u. { ( A + 1 ) } ) )
45 44 ineq1d 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( ( 2 ... ( A + 1 ) ) i^i Prime ) = ( ( ( 2 ... A ) u. { ( A + 1 ) } ) i^i Prime ) )
46 indir 
 |-  ( ( ( 2 ... A ) u. { ( A + 1 ) } ) i^i Prime ) = ( ( ( 2 ... A ) i^i Prime ) u. ( { ( A + 1 ) } i^i Prime ) )
47 45 46 eqtrdi 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( ( 2 ... ( A + 1 ) ) i^i Prime ) = ( ( ( 2 ... A ) i^i Prime ) u. ( { ( A + 1 ) } i^i Prime ) ) )
48 simpr 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( A + 1 ) e. Prime )
49 48 snssd 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> { ( A + 1 ) } C_ Prime )
50 df-ss 
 |-  ( { ( A + 1 ) } C_ Prime <-> ( { ( A + 1 ) } i^i Prime ) = { ( A + 1 ) } )
51 49 50 sylib 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( { ( A + 1 ) } i^i Prime ) = { ( A + 1 ) } )
52 51 uneq2d 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( ( ( 2 ... A ) i^i Prime ) u. ( { ( A + 1 ) } i^i Prime ) ) = ( ( ( 2 ... A ) i^i Prime ) u. { ( A + 1 ) } ) )
53 47 52 eqtrd 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( ( 2 ... ( A + 1 ) ) i^i Prime ) = ( ( ( 2 ... A ) i^i Prime ) u. { ( A + 1 ) } ) )
54 fzfid 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( 2 ... ( A + 1 ) ) e. Fin )
55 inss1 
 |-  ( ( 2 ... ( A + 1 ) ) i^i Prime ) C_ ( 2 ... ( A + 1 ) )
56 ssfi 
 |-  ( ( ( 2 ... ( A + 1 ) ) e. Fin /\ ( ( 2 ... ( A + 1 ) ) i^i Prime ) C_ ( 2 ... ( A + 1 ) ) ) -> ( ( 2 ... ( A + 1 ) ) i^i Prime ) e. Fin )
57 54 55 56 sylancl 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( ( 2 ... ( A + 1 ) ) i^i Prime ) e. Fin )
58 simpr 
 |-  ( ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) /\ p e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) -> p e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) )
59 58 elin2d 
 |-  ( ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) /\ p e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) -> p e. Prime )
60 prmnn 
 |-  ( p e. Prime -> p e. NN )
61 59 60 syl 
 |-  ( ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) /\ p e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) -> p e. NN )
62 61 nnrpd 
 |-  ( ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) /\ p e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) -> p e. RR+ )
63 62 relogcld 
 |-  ( ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) /\ p e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) -> ( log ` p ) e. RR )
64 63 recnd 
 |-  ( ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) /\ p e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ) -> ( log ` p ) e. CC )
65 26 53 57 64 fsumsplit 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> sum_ p e. ( ( 2 ... ( A + 1 ) ) i^i Prime ) ( log ` p ) = ( sum_ p e. ( ( 2 ... A ) i^i Prime ) ( log ` p ) + sum_ p e. { ( A + 1 ) } ( log ` p ) ) )
66 chtval 
 |-  ( A e. RR -> ( theta ` A ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` p ) )
67 17 66 syl 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( theta ` A ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` p ) )
68 ppisval 
 |-  ( A e. RR -> ( ( 0 [,] A ) i^i Prime ) = ( ( 2 ... ( |_ ` A ) ) i^i Prime ) )
69 17 68 syl 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( ( 0 [,] A ) i^i Prime ) = ( ( 2 ... ( |_ ` A ) ) i^i Prime ) )
70 flid 
 |-  ( A e. ZZ -> ( |_ ` A ) = A )
71 70 adantr 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( |_ ` A ) = A )
72 71 oveq2d 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( 2 ... ( |_ ` A ) ) = ( 2 ... A ) )
73 72 ineq1d 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( ( 2 ... ( |_ ` A ) ) i^i Prime ) = ( ( 2 ... A ) i^i Prime ) )
74 69 73 eqtrd 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( ( 0 [,] A ) i^i Prime ) = ( ( 2 ... A ) i^i Prime ) )
75 74 sumeq1d 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` p ) = sum_ p e. ( ( 2 ... A ) i^i Prime ) ( log ` p ) )
76 67 75 eqtr2d 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> sum_ p e. ( ( 2 ... A ) i^i Prime ) ( log ` p ) = ( theta ` A ) )
77 prmnn 
 |-  ( ( A + 1 ) e. Prime -> ( A + 1 ) e. NN )
78 77 adantl 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( A + 1 ) e. NN )
79 78 nnrpd 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( A + 1 ) e. RR+ )
80 79 relogcld 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( log ` ( A + 1 ) ) e. RR )
81 80 recnd 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( log ` ( A + 1 ) ) e. CC )
82 fveq2 
 |-  ( p = ( A + 1 ) -> ( log ` p ) = ( log ` ( A + 1 ) ) )
83 82 sumsn 
 |-  ( ( ( A + 1 ) e. NN /\ ( log ` ( A + 1 ) ) e. CC ) -> sum_ p e. { ( A + 1 ) } ( log ` p ) = ( log ` ( A + 1 ) ) )
84 78 81 83 syl2anc 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> sum_ p e. { ( A + 1 ) } ( log ` p ) = ( log ` ( A + 1 ) ) )
85 76 84 oveq12d 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( sum_ p e. ( ( 2 ... A ) i^i Prime ) ( log ` p ) + sum_ p e. { ( A + 1 ) } ( log ` p ) ) = ( ( theta ` A ) + ( log ` ( A + 1 ) ) ) )
86 15 65 85 3eqtrd 
 |-  ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( theta ` ( A + 1 ) ) = ( ( theta ` A ) + ( log ` ( A + 1 ) ) ) )