Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-chp Structured version   Visualization version   GIF version

Definition df-chp 25045
 Description: Define the second Chebyshev function, which adds up the logarithms of the primes corresponding to the prime powers less than 𝑥, see definition in [ApostolNT] p. 75. (Contributed by Mario Carneiro, 7-Apr-2016.)
Assertion
Ref Expression
df-chp ψ = (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛))
Distinct variable group:   𝑥,𝑛

Detailed syntax breakdown of Definition df-chp
StepHypRef Expression
1 cchp 25039 . 2 class ψ
2 vx . . 3 setvar 𝑥
3 cr 10136 . . 3 class
4 c1 10138 . . . . 5 class 1
52cv 1629 . . . . . 6 class 𝑥
6 cfl 12798 . . . . . 6 class
75, 6cfv 6031 . . . . 5 class (⌊‘𝑥)
8 cfz 12532 . . . . 5 class ...
94, 7, 8co 6792 . . . 4 class (1...(⌊‘𝑥))
10 vn . . . . . 6 setvar 𝑛
1110cv 1629 . . . . 5 class 𝑛
12 cvma 25038 . . . . 5 class Λ
1311, 12cfv 6031 . . . 4 class (Λ‘𝑛)
149, 13, 10csu 14623 . . 3 class Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛)
152, 3, 14cmpt 4861 . 2 class (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛))
161, 15wceq 1630 1 wff ψ = (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛))
 Colors of variables: wff setvar class This definition is referenced by:  chpval  25068  chpf  25069
 Copyright terms: Public domain W3C validator