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 24738
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 24732 . 2 class ψ
2 vx . . 3 setvar 𝑥
3 cr 9886 . . 3 class
4 c1 9888 . . . . 5 class 1
52cv 1479 . . . . . 6 class 𝑥
6 cfl 12538 . . . . . 6 class
75, 6cfv 5852 . . . . 5 class (⌊‘𝑥)
8 cfz 12275 . . . . 5 class ...
94, 7, 8co 6610 . . . 4 class (1...(⌊‘𝑥))
10 vn . . . . . 6 setvar 𝑛
1110cv 1479 . . . . 5 class 𝑛
12 cvma 24731 . . . . 5 class Λ
1311, 12cfv 5852 . . . 4 class (Λ‘𝑛)
149, 13, 10csu 14357 . . 3 class Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛)
152, 3, 14cmpt 4678 . 2 class (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛))
161, 15wceq 1480 1 wff ψ = (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛))
Colors of variables: wff setvar class
This definition is referenced by:  chpval  24761  chpf  24762
  Copyright terms: Public domain W3C validator