This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cht1

Description: The Chebyshev function at 1 . (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Assertion cht1 ( θ ‘ 1 ) = 0

Proof

Step Hyp Ref Expression
1 1re ⊢ 1 ∈ ℝ
2 chtval ⊢ ( 1 ∈ ℝ → ( θ ‘ 1 ) = Σ 𝑝 ∈ ( ( 0 [,] 1 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
3 1 2 ax-mp ⊢ ( θ ‘ 1 ) = Σ 𝑝 ∈ ( ( 0 [,] 1 ) ∩ ℙ ) ( log ‘ 𝑝 )
4 ppisval ⊢ ( 1 ∈ ℝ → ( ( 0 [,] 1 ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ 1 ) ) ∩ ℙ ) )
5 1 4 ax-mp ⊢ ( ( 0 [,] 1 ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ 1 ) ) ∩ ℙ )
6 1z ⊢ 1 ∈ ℤ
7 flid ⊢ ( 1 ∈ ℤ → ( ⌊ ‘ 1 ) = 1 )
8 6 7 ax-mp ⊢ ( ⌊ ‘ 1 ) = 1
9 8 oveq2i ⊢ ( 2 ... ( ⌊ ‘ 1 ) ) = ( 2 ... 1 )
10 1lt2 ⊢ 1 < 2
11 2z ⊢ 2 ∈ ℤ
12 fzn ⊢ ( ( 2 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 1 < 2 ↔ ( 2 ... 1 ) = ∅ ) )
13 11 6 12 mp2an ⊢ ( 1 < 2 ↔ ( 2 ... 1 ) = ∅ )
14 10 13 mpbi ⊢ ( 2 ... 1 ) = ∅
15 9 14 eqtri ⊢ ( 2 ... ( ⌊ ‘ 1 ) ) = ∅
16 15 ineq1i ⊢ ( ( 2 ... ( ⌊ ‘ 1 ) ) ∩ ℙ ) = ( ∅ ∩ ℙ )
17 0in ⊢ ( ∅ ∩ ℙ ) = ∅
18 5 16 17 3eqtri ⊢ ( ( 0 [,] 1 ) ∩ ℙ ) = ∅
19 18 sumeq1i ⊢ Σ 𝑝 ∈ ( ( 0 [,] 1 ) ∩ ℙ ) ( log ‘ 𝑝 ) = Σ 𝑝 ∈ ∅ ( log ‘ 𝑝 )
20 sum0 ⊢ Σ 𝑝 ∈ ∅ ( log ‘ 𝑝 ) = 0
21 3 19 20 3eqtri ⊢ ( θ ‘ 1 ) = 0