Metamath Proof Explorer

Theorem chpval2

Description: Express the second Chebyshev function directly as a sum over the primes less than A (instead of indirectly through the von Mangoldt function). (Contributed by Mario Carneiro, 8-Apr-2016)

Ref Expression
Assertion chpval2 
|- ( A e. RR -> ( psi ` A ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( ( log ` p ) x. ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) )

Proof

Step Hyp Ref Expression
1 chpval 
 |-  ( A e. RR -> ( psi ` A ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( Lam ` n ) )
2 fveq2 
 |-  ( n = ( p ^ k ) -> ( Lam ` n ) = ( Lam ` ( p ^ k ) ) )
3 id 
 |-  ( A e. RR -> A e. RR )
4 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` A ) ) -> n e. NN )
5 4 adantl 
 |-  ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. NN )
6 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
7 5 6 syl 
 |-  ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( Lam ` n ) e. RR )
8 7 recnd 
 |-  ( ( A e. RR /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( Lam ` n ) e. CC )
9 simprr 
 |-  ( ( A e. RR /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ ( Lam ` n ) = 0 ) ) -> ( Lam ` n ) = 0 )
10 2 3 8 9 fsumvma2 
 |-  ( A e. RR -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( Lam ` n ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( Lam ` ( p ^ k ) ) )
11 simpr 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. ( ( 0 [,] A ) i^i Prime ) )
12 11 elin2d 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. Prime )
13 elfznn 
 |-  ( k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) -> k e. NN )
14 vmappw 
 |-  ( ( p e. Prime /\ k e. NN ) -> ( Lam ` ( p ^ k ) ) = ( log ` p ) )
15 12 13 14 syl2an 
 |-  ( ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) -> ( Lam ` ( p ^ k ) ) = ( log ` p ) )
16 15 sumeq2dv 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( Lam ` ( p ^ k ) ) = sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( log ` p ) )
17 fzfid 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) e. Fin )
18 prmuz2 
 |-  ( p e. Prime -> p e. ( ZZ>= ` 2 ) )
19 eluzelre 
 |-  ( p e. ( ZZ>= ` 2 ) -> p e. RR )
20 eluz2gt1 
 |-  ( p e. ( ZZ>= ` 2 ) -> 1 < p )
21 19 20 rplogcld 
 |-  ( p e. ( ZZ>= ` 2 ) -> ( log ` p ) e. RR+ )
22 12 18 21 3syl 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( log ` p ) e. RR+ )
23 22 rpcnd 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( log ` p ) e. CC )
24 fsumconst 
 |-  ( ( ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) e. Fin /\ ( log ` p ) e. CC ) -> sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( log ` p ) = ( ( # ` ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) x. ( log ` p ) ) )
25 17 23 24 syl2anc 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( log ` p ) = ( ( # ` ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) x. ( log ` p ) ) )
26 ppisval 
 |-  ( A e. RR -> ( ( 0 [,] A ) i^i Prime ) = ( ( 2 ... ( |_ ` A ) ) i^i Prime ) )
27 inss1 
 |-  ( ( 2 ... ( |_ ` A ) ) i^i Prime ) C_ ( 2 ... ( |_ ` A ) )
28 26 27 eqsstrdi 
 |-  ( A e. RR -> ( ( 0 [,] A ) i^i Prime ) C_ ( 2 ... ( |_ ` A ) ) )
29 28 sselda 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. ( 2 ... ( |_ ` A ) ) )
30 elfzuz2 
 |-  ( p e. ( 2 ... ( |_ ` A ) ) -> ( |_ ` A ) e. ( ZZ>= ` 2 ) )
31 29 30 syl 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( |_ ` A ) e. ( ZZ>= ` 2 ) )
32 simpl 
 |-  ( ( A e. RR /\ ( |_ ` A ) e. ( ZZ>= ` 2 ) ) -> A e. RR )
33 0red 
 |-  ( ( A e. RR /\ ( |_ ` A ) e. ( ZZ>= ` 2 ) ) -> 0 e. RR )
34 2re 
 |-  2 e. RR
35 34 a1i 
 |-  ( ( A e. RR /\ ( |_ ` A ) e. ( ZZ>= ` 2 ) ) -> 2 e. RR )
36 2pos 
 |-  0 < 2
37 36 a1i 
 |-  ( ( A e. RR /\ ( |_ ` A ) e. ( ZZ>= ` 2 ) ) -> 0 < 2 )
38 eluzle 
 |-  ( ( |_ ` A ) e. ( ZZ>= ` 2 ) -> 2 <_ ( |_ ` A ) )
39 2z 
 |-  2 e. ZZ
40 flge 
 |-  ( ( A e. RR /\ 2 e. ZZ ) -> ( 2 <_ A <-> 2 <_ ( |_ ` A ) ) )
41 39 40 mpan2 
 |-  ( A e. RR -> ( 2 <_ A <-> 2 <_ ( |_ ` A ) ) )
42 38 41 imbitrrid 
 |-  ( A e. RR -> ( ( |_ ` A ) e. ( ZZ>= ` 2 ) -> 2 <_ A ) )
43 42 imp 
 |-  ( ( A e. RR /\ ( |_ ` A ) e. ( ZZ>= ` 2 ) ) -> 2 <_ A )
44 33 35 32 37 43 ltletrd 
 |-  ( ( A e. RR /\ ( |_ ` A ) e. ( ZZ>= ` 2 ) ) -> 0 < A )
45 32 44 elrpd 
 |-  ( ( A e. RR /\ ( |_ ` A ) e. ( ZZ>= ` 2 ) ) -> A e. RR+ )
46 31 45 syldan 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> A e. RR+ )
47 46 relogcld 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( log ` A ) e. RR )
48 47 22 rerpdivcld 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( log ` A ) / ( log ` p ) ) e. RR )
49 1red 
 |-  ( ( A e. RR /\ ( |_ ` A ) e. ( ZZ>= ` 2 ) ) -> 1 e. RR )
50 1lt2 
 |-  1 < 2
51 50 a1i 
 |-  ( ( A e. RR /\ ( |_ ` A ) e. ( ZZ>= ` 2 ) ) -> 1 < 2 )
52 49 35 32 51 43 ltletrd 
 |-  ( ( A e. RR /\ ( |_ ` A ) e. ( ZZ>= ` 2 ) ) -> 1 < A )
53 31 52 syldan 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> 1 < A )
54 rplogcl 
 |-  ( ( A e. RR /\ 1 < A ) -> ( log ` A ) e. RR+ )
55 53 54 syldan 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( log ` A ) e. RR+ )
56 55 22 rpdivcld 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( log ` A ) / ( log ` p ) ) e. RR+ )
57 56 rpge0d 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> 0 <_ ( ( log ` A ) / ( log ` p ) ) )
58 flge0nn0 
 |-  ( ( ( ( log ` A ) / ( log ` p ) ) e. RR /\ 0 <_ ( ( log ` A ) / ( log ` p ) ) ) -> ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) e. NN0 )
59 48 57 58 syl2anc 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) e. NN0 )
60 hashfz1 
 |-  ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) e. NN0 -> ( # ` ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) = ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) )
61 59 60 syl 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( # ` ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) = ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) )
62 61 oveq1d 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( # ` ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) x. ( log ` p ) ) = ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) x. ( log ` p ) ) )
63 59 nn0cnd 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) e. CC )
64 63 23 mulcomd 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) x. ( log ` p ) ) = ( ( log ` p ) x. ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) )
65 25 62 64 3eqtrd 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( log ` p ) = ( ( log ` p ) x. ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) )
66 16 65 eqtrd 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( Lam ` ( p ^ k ) ) = ( ( log ` p ) x. ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) )
67 66 sumeq2dv 
 |-  ( A e. RR -> sum_ p e. ( ( 0 [,] A ) i^i Prime ) sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( Lam ` ( p ^ k ) ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( ( log ` p ) x. ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) )
68 1 10 67 3eqtrd 
 |-  ( A e. RR -> ( psi ` A ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( ( log ` p ) x. ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) )