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

Definition df-chp 25603
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 25597 . 2 class ψ
2 vx . . 3 setvar 𝑥
3 cr 10524 . . 3 class
4 c1 10526 . . . . 5 class 1
52cv 1527 . . . . . 6 class 𝑥
6 cfl 13148 . . . . . 6 class
75, 6cfv 6348 . . . . 5 class (⌊‘𝑥)
8 cfz 12880 . . . . 5 class ...
94, 7, 8co 7145 . . . 4 class (1...(⌊‘𝑥))
10 vn . . . . . 6 setvar 𝑛
1110cv 1527 . . . . 5 class 𝑛
12 cvma 25596 . . . . 5 class Λ
1311, 12cfv 6348 . . . 4 class (Λ‘𝑛)
149, 13, 10csu 15030 . . 3 class Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛)
152, 3, 14cmpt 5137 . 2 class (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛))
161, 15wceq 1528 1 wff ψ = (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛))
Colors of variables: wff setvar class
This definition is referenced by:  chpval  25626  chpf  25627
  Copyright terms: Public domain W3C validator