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 )