Metamath Proof Explorer

Theorem prmorcht

Description: Relate the primorial (product of the first n primes) to the Chebyshev function. (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Hypothesis prmorcht.1 
|- F = ( n e. NN |-> if ( n e. Prime , n , 1 ) )
Assertion prmorcht 
|- ( A e. NN -> ( exp ` ( theta ` A ) ) = ( seq 1 ( x. , F ) ` A ) )

Proof

Step Hyp Ref Expression
1 prmorcht.1 
 |-  F = ( n e. NN |-> if ( n e. Prime , n , 1 ) )
2 nnre 
 |-  ( A e. NN -> A e. RR )
3 chtval 
 |-  ( A e. RR -> ( theta ` A ) = sum_ k e. ( ( 0 [,] A ) i^i Prime ) ( log ` k ) )
4 2 3 syl 
 |-  ( A e. NN -> ( theta ` A ) = sum_ k e. ( ( 0 [,] A ) i^i Prime ) ( log ` k ) )
5 2eluzge1 
 |-  2 e. ( ZZ>= ` 1 )
6 ppisval2 
 |-  ( ( A e. RR /\ 2 e. ( ZZ>= ` 1 ) ) -> ( ( 0 [,] A ) i^i Prime ) = ( ( 1 ... ( |_ ` A ) ) i^i Prime ) )
7 2 5 6 sylancl 
 |-  ( A e. NN -> ( ( 0 [,] A ) i^i Prime ) = ( ( 1 ... ( |_ ` A ) ) i^i Prime ) )
8 nnz 
 |-  ( A e. NN -> A e. ZZ )
9 flid 
 |-  ( A e. ZZ -> ( |_ ` A ) = A )
10 8 9 syl 
 |-  ( A e. NN -> ( |_ ` A ) = A )
11 10 oveq2d 
 |-  ( A e. NN -> ( 1 ... ( |_ ` A ) ) = ( 1 ... A ) )
12 11 ineq1d 
 |-  ( A e. NN -> ( ( 1 ... ( |_ ` A ) ) i^i Prime ) = ( ( 1 ... A ) i^i Prime ) )
13 7 12 eqtrd 
 |-  ( A e. NN -> ( ( 0 [,] A ) i^i Prime ) = ( ( 1 ... A ) i^i Prime ) )
14 13 sumeq1d 
 |-  ( A e. NN -> sum_ k e. ( ( 0 [,] A ) i^i Prime ) ( log ` k ) = sum_ k e. ( ( 1 ... A ) i^i Prime ) ( log ` k ) )
15 inss1 
 |-  ( ( 1 ... A ) i^i Prime ) C_ ( 1 ... A )
16 elinel1 
 |-  ( k e. ( ( 1 ... A ) i^i Prime ) -> k e. ( 1 ... A ) )
17 elfznn 
 |-  ( k e. ( 1 ... A ) -> k e. NN )
18 17 adantl 
 |-  ( ( A e. NN /\ k e. ( 1 ... A ) ) -> k e. NN )
19 18 nnrpd 
 |-  ( ( A e. NN /\ k e. ( 1 ... A ) ) -> k e. RR+ )
20 19 relogcld 
 |-  ( ( A e. NN /\ k e. ( 1 ... A ) ) -> ( log ` k ) e. RR )
21 20 recnd 
 |-  ( ( A e. NN /\ k e. ( 1 ... A ) ) -> ( log ` k ) e. CC )
22 16 21 sylan2 
 |-  ( ( A e. NN /\ k e. ( ( 1 ... A ) i^i Prime ) ) -> ( log ` k ) e. CC )
23 22 ralrimiva 
 |-  ( A e. NN -> A. k e. ( ( 1 ... A ) i^i Prime ) ( log ` k ) e. CC )
24 fzfi 
 |-  ( 1 ... A ) e. Fin
25 24 olci 
 |-  ( ( 1 ... A ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... A ) e. Fin )
26 sumss2 
 |-  ( ( ( ( ( 1 ... A ) i^i Prime ) C_ ( 1 ... A ) /\ A. k e. ( ( 1 ... A ) i^i Prime ) ( log ` k ) e. CC ) /\ ( ( 1 ... A ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... A ) e. Fin ) ) -> sum_ k e. ( ( 1 ... A ) i^i Prime ) ( log ` k ) = sum_ k e. ( 1 ... A ) if ( k e. ( ( 1 ... A ) i^i Prime ) , ( log ` k ) , 0 ) )
27 25 26 mpan2 
 |-  ( ( ( ( 1 ... A ) i^i Prime ) C_ ( 1 ... A ) /\ A. k e. ( ( 1 ... A ) i^i Prime ) ( log ` k ) e. CC ) -> sum_ k e. ( ( 1 ... A ) i^i Prime ) ( log ` k ) = sum_ k e. ( 1 ... A ) if ( k e. ( ( 1 ... A ) i^i Prime ) , ( log ` k ) , 0 ) )
28 15 23 27 sylancr 
 |-  ( A e. NN -> sum_ k e. ( ( 1 ... A ) i^i Prime ) ( log ` k ) = sum_ k e. ( 1 ... A ) if ( k e. ( ( 1 ... A ) i^i Prime ) , ( log ` k ) , 0 ) )
29 14 28 eqtrd 
 |-  ( A e. NN -> sum_ k e. ( ( 0 [,] A ) i^i Prime ) ( log ` k ) = sum_ k e. ( 1 ... A ) if ( k e. ( ( 1 ... A ) i^i Prime ) , ( log ` k ) , 0 ) )
30 4 29 eqtrd 
 |-  ( A e. NN -> ( theta ` A ) = sum_ k e. ( 1 ... A ) if ( k e. ( ( 1 ... A ) i^i Prime ) , ( log ` k ) , 0 ) )
31 elin 
 |-  ( k e. ( ( 1 ... A ) i^i Prime ) <-> ( k e. ( 1 ... A ) /\ k e. Prime ) )
32 31 baibr 
 |-  ( k e. ( 1 ... A ) -> ( k e. Prime <-> k e. ( ( 1 ... A ) i^i Prime ) ) )
33 32 ifbid 
 |-  ( k e. ( 1 ... A ) -> if ( k e. Prime , ( log ` k ) , 0 ) = if ( k e. ( ( 1 ... A ) i^i Prime ) , ( log ` k ) , 0 ) )
34 33 sumeq2i 
 |-  sum_ k e. ( 1 ... A ) if ( k e. Prime , ( log ` k ) , 0 ) = sum_ k e. ( 1 ... A ) if ( k e. ( ( 1 ... A ) i^i Prime ) , ( log ` k ) , 0 )
35 30 34 eqtr4di 
 |-  ( A e. NN -> ( theta ` A ) = sum_ k e. ( 1 ... A ) if ( k e. Prime , ( log ` k ) , 0 ) )
36 eleq1w 
 |-  ( n = k -> ( n e. Prime <-> k e. Prime ) )
37 fveq2 
 |-  ( n = k -> ( log ` n ) = ( log ` k ) )
38 36 37 ifbieq1d 
 |-  ( n = k -> if ( n e. Prime , ( log ` n ) , 0 ) = if ( k e. Prime , ( log ` k ) , 0 ) )
39 eqid 
 |-  ( n e. NN |-> if ( n e. Prime , ( log ` n ) , 0 ) ) = ( n e. NN |-> if ( n e. Prime , ( log ` n ) , 0 ) )
40 fvex 
 |-  ( log ` k ) e. _V
41 0cn 
 |-  0 e. CC
42 41 elexi 
 |-  0 e. _V
43 40 42 ifex 
 |-  if ( k e. Prime , ( log ` k ) , 0 ) e. _V
44 38 39 43 fvmpt 
 |-  ( k e. NN -> ( ( n e. NN |-> if ( n e. Prime , ( log ` n ) , 0 ) ) ` k ) = if ( k e. Prime , ( log ` k ) , 0 ) )
45 18 44 syl 
 |-  ( ( A e. NN /\ k e. ( 1 ... A ) ) -> ( ( n e. NN |-> if ( n e. Prime , ( log ` n ) , 0 ) ) ` k ) = if ( k e. Prime , ( log ` k ) , 0 ) )
46 elnnuz 
 |-  ( A e. NN <-> A e. ( ZZ>= ` 1 ) )
47 46 biimpi 
 |-  ( A e. NN -> A e. ( ZZ>= ` 1 ) )
48 ifcl 
 |-  ( ( ( log ` k ) e. CC /\ 0 e. CC ) -> if ( k e. Prime , ( log ` k ) , 0 ) e. CC )
49 21 41 48 sylancl 
 |-  ( ( A e. NN /\ k e. ( 1 ... A ) ) -> if ( k e. Prime , ( log ` k ) , 0 ) e. CC )
50 45 47 49 fsumser 
 |-  ( A e. NN -> sum_ k e. ( 1 ... A ) if ( k e. Prime , ( log ` k ) , 0 ) = ( seq 1 ( + , ( n e. NN |-> if ( n e. Prime , ( log ` n ) , 0 ) ) ) ` A ) )
51 35 50 eqtrd 
 |-  ( A e. NN -> ( theta ` A ) = ( seq 1 ( + , ( n e. NN |-> if ( n e. Prime , ( log ` n ) , 0 ) ) ) ` A ) )
52 51 fveq2d 
 |-  ( A e. NN -> ( exp ` ( theta ` A ) ) = ( exp ` ( seq 1 ( + , ( n e. NN |-> if ( n e. Prime , ( log ` n ) , 0 ) ) ) ` A ) ) )
53 addcl 
 |-  ( ( k e. CC /\ p e. CC ) -> ( k + p ) e. CC )
54 53 adantl 
 |-  ( ( A e. NN /\ ( k e. CC /\ p e. CC ) ) -> ( k + p ) e. CC )
55 45 49 eqeltrd 
 |-  ( ( A e. NN /\ k e. ( 1 ... A ) ) -> ( ( n e. NN |-> if ( n e. Prime , ( log ` n ) , 0 ) ) ` k ) e. CC )
56 efadd 
 |-  ( ( k e. CC /\ p e. CC ) -> ( exp ` ( k + p ) ) = ( ( exp ` k ) x. ( exp ` p ) ) )
57 56 adantl 
 |-  ( ( A e. NN /\ ( k e. CC /\ p e. CC ) ) -> ( exp ` ( k + p ) ) = ( ( exp ` k ) x. ( exp ` p ) ) )
58 1nn 
 |-  1 e. NN
59 ifcl 
 |-  ( ( k e. NN /\ 1 e. NN ) -> if ( k e. Prime , k , 1 ) e. NN )
60 18 58 59 sylancl 
 |-  ( ( A e. NN /\ k e. ( 1 ... A ) ) -> if ( k e. Prime , k , 1 ) e. NN )
61 60 nnrpd 
 |-  ( ( A e. NN /\ k e. ( 1 ... A ) ) -> if ( k e. Prime , k , 1 ) e. RR+ )
62 61 reeflogd 
 |-  ( ( A e. NN /\ k e. ( 1 ... A ) ) -> ( exp ` ( log ` if ( k e. Prime , k , 1 ) ) ) = if ( k e. Prime , k , 1 ) )
63 fvif 
 |-  ( log ` if ( k e. Prime , k , 1 ) ) = if ( k e. Prime , ( log ` k ) , ( log ` 1 ) )
64 log1 
 |-  ( log ` 1 ) = 0
65 ifeq2 
 |-  ( ( log ` 1 ) = 0 -> if ( k e. Prime , ( log ` k ) , ( log ` 1 ) ) = if ( k e. Prime , ( log ` k ) , 0 ) )
66 64 65 ax-mp 
 |-  if ( k e. Prime , ( log ` k ) , ( log ` 1 ) ) = if ( k e. Prime , ( log ` k ) , 0 )
67 63 66 eqtri 
 |-  ( log ` if ( k e. Prime , k , 1 ) ) = if ( k e. Prime , ( log ` k ) , 0 )
68 45 67 eqtr4di 
 |-  ( ( A e. NN /\ k e. ( 1 ... A ) ) -> ( ( n e. NN |-> if ( n e. Prime , ( log ` n ) , 0 ) ) ` k ) = ( log ` if ( k e. Prime , k , 1 ) ) )
69 68 fveq2d 
 |-  ( ( A e. NN /\ k e. ( 1 ... A ) ) -> ( exp ` ( ( n e. NN |-> if ( n e. Prime , ( log ` n ) , 0 ) ) ` k ) ) = ( exp ` ( log ` if ( k e. Prime , k , 1 ) ) ) )
70 id 
 |-  ( n = k -> n = k )
71 36 70 ifbieq1d 
 |-  ( n = k -> if ( n e. Prime , n , 1 ) = if ( k e. Prime , k , 1 ) )
72 vex 
 |-  k e. _V
73 58 elexi 
 |-  1 e. _V
74 72 73 ifex 
 |-  if ( k e. Prime , k , 1 ) e. _V
75 71 1 74 fvmpt 
 |-  ( k e. NN -> ( F ` k ) = if ( k e. Prime , k , 1 ) )
76 18 75 syl 
 |-  ( ( A e. NN /\ k e. ( 1 ... A ) ) -> ( F ` k ) = if ( k e. Prime , k , 1 ) )
77 62 69 76 3eqtr4d 
 |-  ( ( A e. NN /\ k e. ( 1 ... A ) ) -> ( exp ` ( ( n e. NN |-> if ( n e. Prime , ( log ` n ) , 0 ) ) ` k ) ) = ( F ` k ) )
78 54 55 47 57 77 seqhomo 
 |-  ( A e. NN -> ( exp ` ( seq 1 ( + , ( n e. NN |-> if ( n e. Prime , ( log ` n ) , 0 ) ) ) ` A ) ) = ( seq 1 ( x. , F ) ` A ) )
79 52 78 eqtrd 
 |-  ( A e. NN -> ( exp ` ( theta ` A ) ) = ( seq 1 ( x. , F ) ` A ) )