Metamath Proof Explorer

Theorem chtf

Description: Domain and range of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Assertion chtf 
|- theta : RR --> RR

Proof

Step Hyp Ref Expression
1 df-cht 
 |-  theta = ( x e. RR |-> sum_ p e. ( ( 0 [,] x ) i^i Prime ) ( log ` p ) )
2 ppifi 
 |-  ( x e. RR -> ( ( 0 [,] x ) i^i Prime ) e. Fin )
3 simpr 
 |-  ( ( x e. RR /\ p e. ( ( 0 [,] x ) i^i Prime ) ) -> p e. ( ( 0 [,] x ) i^i Prime ) )
4 3 elin2d 
 |-  ( ( x e. RR /\ p e. ( ( 0 [,] x ) i^i Prime ) ) -> p e. Prime )
5 prmnn 
 |-  ( p e. Prime -> p e. NN )
6 4 5 syl 
 |-  ( ( x e. RR /\ p e. ( ( 0 [,] x ) i^i Prime ) ) -> p e. NN )
7 6 nnrpd 
 |-  ( ( x e. RR /\ p e. ( ( 0 [,] x ) i^i Prime ) ) -> p e. RR+ )
8 7 relogcld 
 |-  ( ( x e. RR /\ p e. ( ( 0 [,] x ) i^i Prime ) ) -> ( log ` p ) e. RR )
9 2 8 fsumrecl 
 |-  ( x e. RR -> sum_ p e. ( ( 0 [,] x ) i^i Prime ) ( log ` p ) e. RR )
10 1 9 fmpti 
 |-  theta : RR --> RR