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