Metamath Proof Explorer

Theorem chtfl

Description: The Chebyshev function does not change off the integers. (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Assertion chtfl ( 𝐴 ∈ ℝ → ( θ ‘ ( ⌊ ‘ 𝐴 ) ) = ( θ ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 flidm ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ ( ⌊ ‘ 𝐴 ) ) = ( ⌊ ‘ 𝐴 ) )
2 1 oveq2d ⊢ ( 𝐴 ∈ ℝ → ( 2 ... ( ⌊ ‘ ( ⌊ ‘ 𝐴 ) ) ) = ( 2 ... ( ⌊ ‘ 𝐴 ) ) )
3 2 ineq1d ⊢ ( 𝐴 ∈ ℝ → ( ( 2 ... ( ⌊ ‘ ( ⌊ ‘ 𝐴 ) ) ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )
4 reflcl ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
5 ppisval ⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℝ → ( ( 0 [,] ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ ( ⌊ ‘ 𝐴 ) ) ) ∩ ℙ ) )
6 4 5 syl ⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ ( ⌊ ‘ 𝐴 ) ) ) ∩ ℙ ) )
7 ppisval ⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )
8 3 6 7 3eqtr4d ⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) = ( ( 0 [,] 𝐴 ) ∩ ℙ ) )
9 8 sumeq1d ⊢ ( 𝐴 ∈ ℝ → Σ 𝑝 ∈ ( ( 0 [,] ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
10 chtval ⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℝ → ( θ ‘ ( ⌊ ‘ 𝐴 ) ) = Σ 𝑝 ∈ ( ( 0 [,] ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
11 4 10 syl ⊢ ( 𝐴 ∈ ℝ → ( θ ‘ ( ⌊ ‘ 𝐴 ) ) = Σ 𝑝 ∈ ( ( 0 [,] ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
12 chtval ⊢ ( 𝐴 ∈ ℝ → ( θ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
13 9 11 12 3eqtr4d ⊢ ( 𝐴 ∈ ℝ → ( θ ‘ ( ⌊ ‘ 𝐴 ) ) = ( θ ‘ 𝐴 ) )