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