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 if n n 1
Assertion prmorcht A e θ A = seq 1 × F A

Proof

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