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