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 24625
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 24619 . 2 class ψ
2 vx . . 3 setvar 𝑥
3 cr 9814 . . 3 class
4 c1 9816 . . . . 5 class 1
52cv 1474 . . . . . 6 class 𝑥
6 cfl 12453 . . . . . 6 class
75, 6cfv 5804 . . . . 5 class (⌊‘𝑥)
8 cfz 12197 . . . . 5 class ...
94, 7, 8co 6549 . . . 4 class (1...(⌊‘𝑥))
10 vn . . . . . 6 setvar 𝑛
1110cv 1474 . . . . 5 class 𝑛
12 cvma 24618 . . . . 5 class Λ
1311, 12cfv 5804 . . . 4 class (Λ‘𝑛)
149, 13, 10csu 14264 . . 3 class Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛)
152, 3, 14cmpt 4643 . 2 class (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛))
161, 15wceq 1475 1 wff ψ = (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛))
Colors of variables: wff setvar class
This definition is referenced by:  chpval  24648  chpf  24649
  Copyright terms: Public domain W3C validator