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

Metamath Proof Explorer

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 )