Metamath Proof Explorer

Theorem cht2

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

Ref Expression
Assertion cht2 
|- ( theta ` 2 ) = ( log ` 2 )

Proof

Step Hyp Ref Expression
1 df-2 
 |-  2 = ( 1 + 1 )
2 1 fveq2i 
 |-  ( theta ` 2 ) = ( theta ` ( 1 + 1 ) )
3 1z 
 |-  1 e. ZZ
4 2prm 
 |-  2 e. Prime
5 1 4 eqeltrri 
 |-  ( 1 + 1 ) e. Prime
6 chtprm 
 |-  ( ( 1 e. ZZ /\ ( 1 + 1 ) e. Prime ) -> ( theta ` ( 1 + 1 ) ) = ( ( theta ` 1 ) + ( log ` ( 1 + 1 ) ) ) )
7 3 5 6 mp2an 
 |-  ( theta ` ( 1 + 1 ) ) = ( ( theta ` 1 ) + ( log ` ( 1 + 1 ) ) )
8 cht1 
 |-  ( theta ` 1 ) = 0
9 8 eqcomi 
 |-  0 = ( theta ` 1 )
10 1 fveq2i 
 |-  ( log ` 2 ) = ( log ` ( 1 + 1 ) )
11 9 10 oveq12i 
 |-  ( 0 + ( log ` 2 ) ) = ( ( theta ` 1 ) + ( log ` ( 1 + 1 ) ) )
12 2rp 
 |-  2 e. RR+
13 relogcl 
 |-  ( 2 e. RR+ -> ( log ` 2 ) e. RR )
14 12 13 ax-mp 
 |-  ( log ` 2 ) e. RR
15 14 recni 
 |-  ( log ` 2 ) e. CC
16 15 addid2i 
 |-  ( 0 + ( log ` 2 ) ) = ( log ` 2 )
17 11 16 eqtr3i 
 |-  ( ( theta ` 1 ) + ( log ` ( 1 + 1 ) ) ) = ( log ` 2 )
18 2 7 17 3eqtri 
 |-  ( theta ` 2 ) = ( log ` 2 )