Metamath Proof Explorer

Theorem cht3

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

Ref Expression
Assertion cht3 
|- ( theta ` 3 ) = ( log ` 6 )

Proof

Step Hyp Ref Expression
1 df-3 
 |-  3 = ( 2 + 1 )
2 1 fveq2i 
 |-  ( theta ` 3 ) = ( theta ` ( 2 + 1 ) )
3 2z 
 |-  2 e. ZZ
4 3prm 
 |-  3 e. Prime
5 1 4 eqeltrri 
 |-  ( 2 + 1 ) e. Prime
6 chtprm 
 |-  ( ( 2 e. ZZ /\ ( 2 + 1 ) e. Prime ) -> ( theta ` ( 2 + 1 ) ) = ( ( theta ` 2 ) + ( log ` ( 2 + 1 ) ) ) )
7 3 5 6 mp2an 
 |-  ( theta ` ( 2 + 1 ) ) = ( ( theta ` 2 ) + ( log ` ( 2 + 1 ) ) )
8 2rp 
 |-  2 e. RR+
9 3rp 
 |-  3 e. RR+
10 relogmul 
 |-  ( ( 2 e. RR+ /\ 3 e. RR+ ) -> ( log ` ( 2 x. 3 ) ) = ( ( log ` 2 ) + ( log ` 3 ) ) )
11 8 9 10 mp2an 
 |-  ( log ` ( 2 x. 3 ) ) = ( ( log ` 2 ) + ( log ` 3 ) )
12 2t3e6 
 |-  ( 2 x. 3 ) = 6
13 12 fveq2i 
 |-  ( log ` ( 2 x. 3 ) ) = ( log ` 6 )
14 cht2 
 |-  ( theta ` 2 ) = ( log ` 2 )
15 14 eqcomi 
 |-  ( log ` 2 ) = ( theta ` 2 )
16 1 fveq2i 
 |-  ( log ` 3 ) = ( log ` ( 2 + 1 ) )
17 15 16 oveq12i 
 |-  ( ( log ` 2 ) + ( log ` 3 ) ) = ( ( theta ` 2 ) + ( log ` ( 2 + 1 ) ) )
18 11 13 17 3eqtr3ri 
 |-  ( ( theta ` 2 ) + ( log ` ( 2 + 1 ) ) ) = ( log ` 6 )
19 2 7 18 3eqtri 
 |-  ( theta ` 3 ) = ( log ` 6 )