Theorem cht2

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

	Ref	Expression
Assertion	cht2	⊢ ( θ ‘ 2 ) = ( log ‘ 2 )

Proof

Step	Hyp	Ref	Expression
1		df-2	⊢ 2 = ( 1 + 1 )
2	1	fveq2i	⊢ ( θ ‘ 2 ) = ( θ ‘ ( 1 + 1 ) )
3		1z	⊢ 1 ∈ ℤ
4		2prm	⊢ 2 ∈ ℙ
5	1 4	eqeltrri	⊢ ( 1 + 1 ) ∈ ℙ
6		chtprm	⊢ ( ( 1 ∈ ℤ ∧ ( 1 + 1 ) ∈ ℙ ) → ( θ ‘ ( 1 + 1 ) ) = ( ( θ ‘ 1 ) + ( log ‘ ( 1 + 1 ) ) ) )
7	3 5 6	mp2an	⊢ ( θ ‘ ( 1 + 1 ) ) = ( ( θ ‘ 1 ) + ( log ‘ ( 1 + 1 ) ) )
8		cht1	⊢ ( θ ‘ 1 ) = 0
9	8	eqcomi	⊢ 0 = ( θ ‘ 1 )
10	1	fveq2i	⊢ ( log ‘ 2 ) = ( log ‘ ( 1 + 1 ) )
11	9 10	oveq12i	⊢ ( 0 + ( log ‘ 2 ) ) = ( ( θ ‘ 1 ) + ( log ‘ ( 1 + 1 ) ) )
12		2rp	⊢ 2 ∈ ℝ+
13		relogcl	⊢ ( 2 ∈ ℝ+ → ( log ‘ 2 ) ∈ ℝ )
14	12 13	ax-mp	⊢ ( log ‘ 2 ) ∈ ℝ
15	14	recni	⊢ ( log ‘ 2 ) ∈ ℂ
16	15	addid2i	⊢ ( 0 + ( log ‘ 2 ) ) = ( log ‘ 2 )
17	11 16	eqtr3i	⊢ ( ( θ ‘ 1 ) + ( log ‘ ( 1 + 1 ) ) ) = ( log ‘ 2 )
18	2 7 17	3eqtri	⊢ ( θ ‘ 2 ) = ( log ‘ 2 )