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

Metamath Proof Explorer

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 addlidi ⊢ ( 0 + ( log ‘ 2 ) ) = ( log ‘ 2 )
17 11 16 eqtr3i ⊢ ( ( θ ‘ 1 ) + ( log ‘ ( 1 + 1 ) ) ) = ( log ‘ 2 )
18 2 7 17 3eqtri ⊢ ( θ ‘ 2 ) = ( log ‘ 2 )