Metamath Proof Explorer

Theorem chtge0

Description: The Chebyshev function is always positive. (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Assertion chtge0 
|- ( A e. RR -> 0 <_ ( theta ` A ) )

Proof

Step Hyp Ref Expression
1 ppifi 
 |-  ( A e. RR -> ( ( 0 [,] A ) i^i Prime ) e. Fin )
2 simpr 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. ( ( 0 [,] A ) i^i Prime ) )
3 2 elin2d 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. Prime )
4 prmuz2 
 |-  ( p e. Prime -> p e. ( ZZ>= ` 2 ) )
5 3 4 syl 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. ( ZZ>= ` 2 ) )
6 eluz2b2 
 |-  ( p e. ( ZZ>= ` 2 ) <-> ( p e. NN /\ 1 < p ) )
7 5 6 sylib 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( p e. NN /\ 1 < p ) )
8 7 simpld 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. NN )
9 8 nnrpd 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. RR+ )
10 9 relogcld 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( log ` p ) e. RR )
11 8 nnred 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. RR )
12 7 simprd 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> 1 < p )
13 11 12 rplogcld 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( log ` p ) e. RR+ )
14 13 rpge0d 
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> 0 <_ ( log ` p ) )
15 1 10 14 fsumge0 
 |-  ( A e. RR -> 0 <_ sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` p ) )
16 chtval 
 |-  ( A e. RR -> ( theta ` A ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` p ) )
17 15 16 breqtrrd 
 |-  ( A e. RR -> 0 <_ ( theta ` A ) )