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 3cn 
 |-  3 e. CC
13 2cn 
 |-  2 e. CC
14 3t2e6 
 |-  ( 3 x. 2 ) = 6
15 12 13 14 mulcomli 
 |-  ( 2 x. 3 ) = 6
16 15 fveq2i 
 |-  ( log ` ( 2 x. 3 ) ) = ( log ` 6 )
17 cht2 
 |-  ( theta ` 2 ) = ( log ` 2 )
18 17 eqcomi 
 |-  ( log ` 2 ) = ( theta ` 2 )
19 1 fveq2i 
 |-  ( log ` 3 ) = ( log ` ( 2 + 1 ) )
20 18 19 oveq12i 
 |-  ( ( log ` 2 ) + ( log ` 3 ) ) = ( ( theta ` 2 ) + ( log ` ( 2 + 1 ) ) )
21 11 16 20 3eqtr3ri 
 |-  ( ( theta ` 2 ) + ( log ` ( 2 + 1 ) ) ) = ( log ` 6 )
22 2 7 21 3eqtri 
 |-  ( theta ` 3 ) = ( log ` 6 )