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 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) )
Assertion prmorcht ( 𝐴 ∈ ℕ → ( exp ‘ ( θ ‘ 𝐴 ) ) = ( seq 1 ( · , 𝐹 ) ‘ 𝐴 ) )

Proof

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