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 25682
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 25676 . 2 class ψ
2 vx . . 3 setvar 𝑥
3 cr 10525 . . 3 class
4 c1 10527 . . . . 5 class 1
52cv 1537 . . . . . 6 class 𝑥
6 cfl 13155 . . . . . 6 class
75, 6cfv 6334 . . . . 5 class (⌊‘𝑥)
8 cfz 12885 . . . . 5 class ...
94, 7, 8co 7140 . . . 4 class (1...(⌊‘𝑥))
10 vn . . . . . 6 setvar 𝑛
1110cv 1537 . . . . 5 class 𝑛
12 cvma 25675 . . . . 5 class Λ
1311, 12cfv 6334 . . . 4 class (Λ‘𝑛)
149, 13, 10csu 15033 . . 3 class Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛)
152, 3, 14cmpt 5122 . 2 class (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛))
161, 15wceq 1538 1 wff ψ = (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛))
Colors of variables: wff setvar class
This definition is referenced by:  chpval  25705  chpf  25706
  Copyright terms: Public domain W3C validator