Metamath Proof Explorer

Theorem chtleppi

Description: Upper bound on the theta function. (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Assertion chtleppi 
|- ( A e. RR+ -> ( theta ` A ) <_ ( ( ppi ` A ) x. ( log ` A ) ) )

Proof

Step Hyp Ref Expression
1 rpre 
 |-  ( A e. RR+ -> A e. RR )
2 ppifi 
 |-  ( A e. RR -> ( ( 0 [,] A ) i^i Prime ) e. Fin )
3 1 2 syl 
 |-  ( A e. RR+ -> ( ( 0 [,] A ) i^i Prime ) e. Fin )
4 simpr 
 |-  ( ( A e. RR+ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. ( ( 0 [,] A ) i^i Prime ) )
5 4 elin2d 
 |-  ( ( A e. RR+ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. Prime )
6 prmnn 
 |-  ( p e. Prime -> p e. NN )
7 5 6 syl 
 |-  ( ( A e. RR+ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. NN )
8 7 nnrpd 
 |-  ( ( A e. RR+ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. RR+ )
9 8 relogcld 
 |-  ( ( A e. RR+ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( log ` p ) e. RR )
10 relogcl 
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
11 10 adantr 
 |-  ( ( A e. RR+ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( log ` A ) e. RR )
12 4 elin1d 
 |-  ( ( A e. RR+ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. ( 0 [,] A ) )
13 0re 
 |-  0 e. RR
14 elicc2 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( p e. ( 0 [,] A ) <-> ( p e. RR /\ 0 <_ p /\ p <_ A ) ) )
15 13 1 14 sylancr 
 |-  ( A e. RR+ -> ( p e. ( 0 [,] A ) <-> ( p e. RR /\ 0 <_ p /\ p <_ A ) ) )
16 15 biimpa 
 |-  ( ( A e. RR+ /\ p e. ( 0 [,] A ) ) -> ( p e. RR /\ 0 <_ p /\ p <_ A ) )
17 12 16 syldan 
 |-  ( ( A e. RR+ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( p e. RR /\ 0 <_ p /\ p <_ A ) )
18 17 simp3d 
 |-  ( ( A e. RR+ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p <_ A )
19 8 reeflogd 
 |-  ( ( A e. RR+ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( exp ` ( log ` p ) ) = p )
20 reeflog 
 |-  ( A e. RR+ -> ( exp ` ( log ` A ) ) = A )
21 20 adantr 
 |-  ( ( A e. RR+ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( exp ` ( log ` A ) ) = A )
22 18 19 21 3brtr4d 
 |-  ( ( A e. RR+ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( exp ` ( log ` p ) ) <_ ( exp ` ( log ` A ) ) )
23 efle 
 |-  ( ( ( log ` p ) e. RR /\ ( log ` A ) e. RR ) -> ( ( log ` p ) <_ ( log ` A ) <-> ( exp ` ( log ` p ) ) <_ ( exp ` ( log ` A ) ) ) )
24 9 11 23 syl2anc 
 |-  ( ( A e. RR+ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( log ` p ) <_ ( log ` A ) <-> ( exp ` ( log ` p ) ) <_ ( exp ` ( log ` A ) ) ) )
25 22 24 mpbird 
 |-  ( ( A e. RR+ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( log ` p ) <_ ( log ` A ) )
26 3 9 11 25 fsumle 
 |-  ( A e. RR+ -> sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` p ) <_ sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` A ) )
27 chtval 
 |-  ( A e. RR -> ( theta ` A ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` p ) )
28 1 27 syl 
 |-  ( A e. RR+ -> ( theta ` A ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` p ) )
29 ppival 
 |-  ( A e. RR -> ( ppi ` A ) = ( # ` ( ( 0 [,] A ) i^i Prime ) ) )
30 1 29 syl 
 |-  ( A e. RR+ -> ( ppi ` A ) = ( # ` ( ( 0 [,] A ) i^i Prime ) ) )
31 30 oveq1d 
 |-  ( A e. RR+ -> ( ( ppi ` A ) x. ( log ` A ) ) = ( ( # ` ( ( 0 [,] A ) i^i Prime ) ) x. ( log ` A ) ) )
32 10 recnd 
 |-  ( A e. RR+ -> ( log ` A ) e. CC )
33 fsumconst 
 |-  ( ( ( ( 0 [,] A ) i^i Prime ) e. Fin /\ ( log ` A ) e. CC ) -> sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` A ) = ( ( # ` ( ( 0 [,] A ) i^i Prime ) ) x. ( log ` A ) ) )
34 3 32 33 syl2anc 
 |-  ( A e. RR+ -> sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` A ) = ( ( # ` ( ( 0 [,] A ) i^i Prime ) ) x. ( log ` A ) ) )
35 31 34 eqtr4d 
 |-  ( A e. RR+ -> ( ( ppi ` A ) x. ( log ` A ) ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` A ) )
36 26 28 35 3brtr4d 
 |-  ( A e. RR+ -> ( theta ` A ) <_ ( ( ppi ` A ) x. ( log ` A ) ) )