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