Theorem cht3

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

	Ref	Expression
Assertion	cht3	⊢ ( θ ‘ 3 ) = ( log ‘ 6 )

Proof

Step	Hyp	Ref	Expression
1		df-3	⊢ 3 = ( 2 + 1 )
2	1	fveq2i	⊢ ( θ ‘ 3 ) = ( θ ‘ ( 2 + 1 ) )
3		2z	⊢ 2 ∈ ℤ
4		3prm	⊢ 3 ∈ ℙ
5	1 4	eqeltrri	⊢ ( 2 + 1 ) ∈ ℙ
6		chtprm	⊢ ( ( 2 ∈ ℤ ∧ ( 2 + 1 ) ∈ ℙ ) → ( θ ‘ ( 2 + 1 ) ) = ( ( θ ‘ 2 ) + ( log ‘ ( 2 + 1 ) ) ) )
7	3 5 6	mp2an	⊢ ( θ ‘ ( 2 + 1 ) ) = ( ( θ ‘ 2 ) + ( log ‘ ( 2 + 1 ) ) )
8		2rp	⊢ 2 ∈ ℝ+
9		3rp	⊢ 3 ∈ ℝ+
10		relogmul	⊢ ( ( 2 ∈ ℝ+ ∧ 3 ∈ ℝ+ ) → ( log ‘ ( 2 · 3 ) ) = ( ( log ‘ 2 ) + ( log ‘ 3 ) ) )
11	8 9 10	mp2an	⊢ ( log ‘ ( 2 · 3 ) ) = ( ( log ‘ 2 ) + ( log ‘ 3 ) )
12		3cn	⊢ 3 ∈ ℂ
13		2cn	⊢ 2 ∈ ℂ
14		3t2e6	⊢ ( 3 · 2 ) = 6
15	12 13 14	mulcomli	⊢ ( 2 · 3 ) = 6
16	15	fveq2i	⊢ ( log ‘ ( 2 · 3 ) ) = ( log ‘ 6 )
17		cht2	⊢ ( θ ‘ 2 ) = ( log ‘ 2 )
18	17	eqcomi	⊢ ( log ‘ 2 ) = ( θ ‘ 2 )
19	1	fveq2i	⊢ ( log ‘ 3 ) = ( log ‘ ( 2 + 1 ) )
20	18 19	oveq12i	⊢ ( ( log ‘ 2 ) + ( log ‘ 3 ) ) = ( ( θ ‘ 2 ) + ( log ‘ ( 2 + 1 ) ) )
21	11 16 20	3eqtr3ri	⊢ ( ( θ ‘ 2 ) + ( log ‘ ( 2 + 1 ) ) ) = ( log ‘ 6 )
22	2 7 21	3eqtri	⊢ ( θ ‘ 3 ) = ( log ‘ 6 )