Metamath Proof Explorer

Theorem pnt2

Description: The Prime Number Theorem, version 2: the first Chebyshev function tends asymptotically to x . (Contributed by Mario Carneiro, 1-Jun-2016)

Ref Expression
Assertion pnt2 
|- ( x e. RR+ |-> ( ( theta ` x ) / x ) ) ~~>r 1

Proof

Step Hyp Ref Expression
1 2re 
 |-  2 e. RR
2 elicopnf 
 |-  ( 2 e. RR -> ( x e. ( 2 [,) +oo ) <-> ( x e. RR /\ 2 <_ x ) ) )
3 1 2 ax-mp 
 |-  ( x e. ( 2 [,) +oo ) <-> ( x e. RR /\ 2 <_ x ) )
4 chprpcl 
 |-  ( ( x e. RR /\ 2 <_ x ) -> ( psi ` x ) e. RR+ )
5 3 4 sylbi 
 |-  ( x e. ( 2 [,) +oo ) -> ( psi ` x ) e. RR+ )
6 3 simplbi 
 |-  ( x e. ( 2 [,) +oo ) -> x e. RR )
7 0red 
 |-  ( x e. ( 2 [,) +oo ) -> 0 e. RR )
8 1 a1i 
 |-  ( x e. ( 2 [,) +oo ) -> 2 e. RR )
9 2pos 
 |-  0 < 2
10 9 a1i 
 |-  ( x e. ( 2 [,) +oo ) -> 0 < 2 )
11 3 simprbi 
 |-  ( x e. ( 2 [,) +oo ) -> 2 <_ x )
12 7 8 6 10 11 ltletrd 
 |-  ( x e. ( 2 [,) +oo ) -> 0 < x )
13 6 12 elrpd 
 |-  ( x e. ( 2 [,) +oo ) -> x e. RR+ )
14 5 13 rpdivcld 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( psi ` x ) / x ) e. RR+ )
15 14 adantl 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( psi ` x ) / x ) e. RR+ )
16 chtrpcl 
 |-  ( ( x e. RR /\ 2 <_ x ) -> ( theta ` x ) e. RR+ )
17 3 16 sylbi 
 |-  ( x e. ( 2 [,) +oo ) -> ( theta ` x ) e. RR+ )
18 5 17 rpdivcld 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( psi ` x ) / ( theta ` x ) ) e. RR+ )
19 18 adantl 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( psi ` x ) / ( theta ` x ) ) e. RR+ )
20 13 ssriv 
 |-  ( 2 [,) +oo ) C_ RR+
21 20 a1i 
 |-  ( T. -> ( 2 [,) +oo ) C_ RR+ )
22 pnt3 
 |-  ( x e. RR+ |-> ( ( psi ` x ) / x ) ) ~~>r 1
23 22 a1i 
 |-  ( T. -> ( x e. RR+ |-> ( ( psi ` x ) / x ) ) ~~>r 1 )
24 21 23 rlimres2 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( psi ` x ) / x ) ) ~~>r 1 )
25 chpchtlim 
 |-  ( x e. ( 2 [,) +oo ) |-> ( ( psi ` x ) / ( theta ` x ) ) ) ~~>r 1
26 25 a1i 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( psi ` x ) / ( theta ` x ) ) ) ~~>r 1 )
27 ax-1ne0 
 |-  1 =/= 0
28 27 a1i 
 |-  ( T. -> 1 =/= 0 )
29 19 rpne0d 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( psi ` x ) / ( theta ` x ) ) =/= 0 )
30 15 19 24 26 28 29 rlimdiv 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( ( psi ` x ) / x ) / ( ( psi ` x ) / ( theta ` x ) ) ) ) ~~>r ( 1 / 1 ) )
31 rpre 
 |-  ( x e. RR+ -> x e. RR )
32 chpcl 
 |-  ( x e. RR -> ( psi ` x ) e. RR )
33 31 32 syl 
 |-  ( x e. RR+ -> ( psi ` x ) e. RR )
34 33 recnd 
 |-  ( x e. RR+ -> ( psi ` x ) e. CC )
35 13 34 syl 
 |-  ( x e. ( 2 [,) +oo ) -> ( psi ` x ) e. CC )
36 13 rpcnne0d 
 |-  ( x e. ( 2 [,) +oo ) -> ( x e. CC /\ x =/= 0 ) )
37 5 rpcnne0d 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( psi ` x ) e. CC /\ ( psi ` x ) =/= 0 ) )
38 17 rpcnne0d 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( theta ` x ) e. CC /\ ( theta ` x ) =/= 0 ) )
39 divdivdiv 
 |-  ( ( ( ( psi ` x ) e. CC /\ ( x e. CC /\ x =/= 0 ) ) /\ ( ( ( psi ` x ) e. CC /\ ( psi ` x ) =/= 0 ) /\ ( ( theta ` x ) e. CC /\ ( theta ` x ) =/= 0 ) ) ) -> ( ( ( psi ` x ) / x ) / ( ( psi ` x ) / ( theta ` x ) ) ) = ( ( ( psi ` x ) x. ( theta ` x ) ) / ( x x. ( psi ` x ) ) ) )
40 35 36 37 38 39 syl22anc 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ( psi ` x ) / x ) / ( ( psi ` x ) / ( theta ` x ) ) ) = ( ( ( psi ` x ) x. ( theta ` x ) ) / ( x x. ( psi ` x ) ) ) )
41 6 recnd 
 |-  ( x e. ( 2 [,) +oo ) -> x e. CC )
42 41 35 mulcomd 
 |-  ( x e. ( 2 [,) +oo ) -> ( x x. ( psi ` x ) ) = ( ( psi ` x ) x. x ) )
43 42 oveq2d 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ( psi ` x ) x. ( theta ` x ) ) / ( x x. ( psi ` x ) ) ) = ( ( ( psi ` x ) x. ( theta ` x ) ) / ( ( psi ` x ) x. x ) ) )
44 chtcl 
 |-  ( x e. RR -> ( theta ` x ) e. RR )
45 31 44 syl 
 |-  ( x e. RR+ -> ( theta ` x ) e. RR )
46 45 recnd 
 |-  ( x e. RR+ -> ( theta ` x ) e. CC )
47 13 46 syl 
 |-  ( x e. ( 2 [,) +oo ) -> ( theta ` x ) e. CC )
48 divcan5 
 |-  ( ( ( theta ` x ) e. CC /\ ( x e. CC /\ x =/= 0 ) /\ ( ( psi ` x ) e. CC /\ ( psi ` x ) =/= 0 ) ) -> ( ( ( psi ` x ) x. ( theta ` x ) ) / ( ( psi ` x ) x. x ) ) = ( ( theta ` x ) / x ) )
49 47 36 37 48 syl3anc 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ( psi ` x ) x. ( theta ` x ) ) / ( ( psi ` x ) x. x ) ) = ( ( theta ` x ) / x ) )
50 40 43 49 3eqtrd 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ( psi ` x ) / x ) / ( ( psi ` x ) / ( theta ` x ) ) ) = ( ( theta ` x ) / x ) )
51 50 mpteq2ia 
 |-  ( x e. ( 2 [,) +oo ) |-> ( ( ( psi ` x ) / x ) / ( ( psi ` x ) / ( theta ` x ) ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / x ) )
52 resmpt 
 |-  ( ( 2 [,) +oo ) C_ RR+ -> ( ( x e. RR+ |-> ( ( theta ` x ) / x ) ) |` ( 2 [,) +oo ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / x ) ) )
53 20 52 ax-mp 
 |-  ( ( x e. RR+ |-> ( ( theta ` x ) / x ) ) |` ( 2 [,) +oo ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / x ) )
54 51 53 eqtr4i 
 |-  ( x e. ( 2 [,) +oo ) |-> ( ( ( psi ` x ) / x ) / ( ( psi ` x ) / ( theta ` x ) ) ) ) = ( ( x e. RR+ |-> ( ( theta ` x ) / x ) ) |` ( 2 [,) +oo ) )
55 1div1e1 
 |-  ( 1 / 1 ) = 1
56 30 54 55 3brtr3g 
 |-  ( T. -> ( ( x e. RR+ |-> ( ( theta ` x ) / x ) ) |` ( 2 [,) +oo ) ) ~~>r 1 )
57 rerpdivcl 
 |-  ( ( ( theta ` x ) e. RR /\ x e. RR+ ) -> ( ( theta ` x ) / x ) e. RR )
58 45 57 mpancom 
 |-  ( x e. RR+ -> ( ( theta ` x ) / x ) e. RR )
59 58 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( theta ` x ) / x ) e. RR )
60 59 recnd 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( theta ` x ) / x ) e. CC )
61 60 fmpttd 
 |-  ( T. -> ( x e. RR+ |-> ( ( theta ` x ) / x ) ) : RR+ --> CC )
62 rpssre 
 |-  RR+ C_ RR
63 62 a1i 
 |-  ( T. -> RR+ C_ RR )
64 1 a1i 
 |-  ( T. -> 2 e. RR )
65 61 63 64 rlimresb 
 |-  ( T. -> ( ( x e. RR+ |-> ( ( theta ` x ) / x ) ) ~~>r 1 <-> ( ( x e. RR+ |-> ( ( theta ` x ) / x ) ) |` ( 2 [,) +oo ) ) ~~>r 1 ) )
66 56 65 mpbird 
 |-  ( T. -> ( x e. RR+ |-> ( ( theta ` x ) / x ) ) ~~>r 1 )
67 66 mptru 
 |-  ( x e. RR+ |-> ( ( theta ` x ) / x ) ) ~~>r 1