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