Metamath Proof Explorer

Theorem chpchtlim

Description: The psi and theta functions are asymptotic to each other, so is sufficient to prove either theta ( x ) / x ~>r 1 or psi ( x ) / x ~>r 1 to establish the PNT. (Contributed by Mario Carneiro, 8-Apr-2016)

Ref Expression
Assertion chpchtlim 
|- ( x e. ( 2 [,) +oo ) |-> ( ( psi ` x ) / ( theta ` x ) ) ) ~~>r 1

Proof

Step Hyp Ref Expression
1 1red 
 |-  ( T. -> 1 e. RR )
2 1red 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> 1 e. RR )
3 2re 
 |-  2 e. RR
4 elicopnf 
 |-  ( 2 e. RR -> ( x e. ( 2 [,) +oo ) <-> ( x e. RR /\ 2 <_ x ) ) )
5 3 4 ax-mp 
 |-  ( x e. ( 2 [,) +oo ) <-> ( x e. RR /\ 2 <_ x ) )
6 5 simplbi 
 |-  ( x e. ( 2 [,) +oo ) -> x e. RR )
7 6 adantl 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> x e. RR )
8 0red 
 |-  ( x e. ( 2 [,) +oo ) -> 0 e. RR )
9 3 a1i 
 |-  ( x e. ( 2 [,) +oo ) -> 2 e. RR )
10 2pos 
 |-  0 < 2
11 10 a1i 
 |-  ( x e. ( 2 [,) +oo ) -> 0 < 2 )
12 5 simprbi 
 |-  ( x e. ( 2 [,) +oo ) -> 2 <_ x )
13 8 9 6 11 12 ltletrd 
 |-  ( x e. ( 2 [,) +oo ) -> 0 < x )
14 6 13 elrpd 
 |-  ( x e. ( 2 [,) +oo ) -> x e. RR+ )
15 14 adantl 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> x e. RR+ )
16 15 rpge0d 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> 0 <_ x )
17 7 16 resqrtcld 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( sqrt ` x ) e. RR )
18 15 relogcld 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( log ` x ) e. RR )
19 17 18 remulcld 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( sqrt ` x ) x. ( log ` x ) ) e. RR )
20 12 adantl 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> 2 <_ x )
21 chtrpcl 
 |-  ( ( x e. RR /\ 2 <_ x ) -> ( theta ` x ) e. RR+ )
22 7 20 21 syl2anc 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( theta ` x ) e. RR+ )
23 19 22 rerpdivcld 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( ( sqrt ` x ) x. ( log ` x ) ) / ( theta ` x ) ) e. RR )
24 6 ssriv 
 |-  ( 2 [,) +oo ) C_ RR
25 1 recnd 
 |-  ( T. -> 1 e. CC )
26 rlimconst 
 |-  ( ( ( 2 [,) +oo ) C_ RR /\ 1 e. CC ) -> ( x e. ( 2 [,) +oo ) |-> 1 ) ~~>r 1 )
27 24 25 26 sylancr 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> 1 ) ~~>r 1 )
28 ovexd 
 |-  ( T. -> ( 2 [,) +oo ) e. _V )
29 7 22 rerpdivcld 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( x / ( theta ` x ) ) e. RR )
30 ovexd 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( ( sqrt ` x ) x. ( log ` x ) ) / x ) e. _V )
31 eqidd 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( x / ( theta ` x ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( x / ( theta ` x ) ) ) )
32 7 recnd 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> x e. CC )
33 cxpsqrt 
 |-  ( x e. CC -> ( x ^c ( 1 / 2 ) ) = ( sqrt ` x ) )
34 32 33 syl 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( x ^c ( 1 / 2 ) ) = ( sqrt ` x ) )
35 34 oveq2d 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( log ` x ) / ( x ^c ( 1 / 2 ) ) ) = ( ( log ` x ) / ( sqrt ` x ) ) )
36 18 recnd 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( log ` x ) e. CC )
37 15 rpsqrtcld 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( sqrt ` x ) e. RR+ )
38 37 rpcnne0d 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( sqrt ` x ) e. CC /\ ( sqrt ` x ) =/= 0 ) )
39 divcan5 
 |-  ( ( ( log ` x ) e. CC /\ ( ( sqrt ` x ) e. CC /\ ( sqrt ` x ) =/= 0 ) /\ ( ( sqrt ` x ) e. CC /\ ( sqrt ` x ) =/= 0 ) ) -> ( ( ( sqrt ` x ) x. ( log ` x ) ) / ( ( sqrt ` x ) x. ( sqrt ` x ) ) ) = ( ( log ` x ) / ( sqrt ` x ) ) )
40 36 38 38 39 syl3anc 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( ( sqrt ` x ) x. ( log ` x ) ) / ( ( sqrt ` x ) x. ( sqrt ` x ) ) ) = ( ( log ` x ) / ( sqrt ` x ) ) )
41 remsqsqrt 
 |-  ( ( x e. RR /\ 0 <_ x ) -> ( ( sqrt ` x ) x. ( sqrt ` x ) ) = x )
42 7 16 41 syl2anc 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( sqrt ` x ) x. ( sqrt ` x ) ) = x )
43 42 oveq2d 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( ( sqrt ` x ) x. ( log ` x ) ) / ( ( sqrt ` x ) x. ( sqrt ` x ) ) ) = ( ( ( sqrt ` x ) x. ( log ` x ) ) / x ) )
44 35 40 43 3eqtr2d 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( log ` x ) / ( x ^c ( 1 / 2 ) ) ) = ( ( ( sqrt ` x ) x. ( log ` x ) ) / x ) )
45 44 mpteq2dva 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( log ` x ) / ( x ^c ( 1 / 2 ) ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( ( sqrt ` x ) x. ( log ` x ) ) / x ) ) )
46 28 29 30 31 45 offval2 
 |-  ( T. -> ( ( x e. ( 2 [,) +oo ) |-> ( x / ( theta ` x ) ) ) oF x. ( x e. ( 2 [,) +oo ) |-> ( ( log ` x ) / ( x ^c ( 1 / 2 ) ) ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( x / ( theta ` x ) ) x. ( ( ( sqrt ` x ) x. ( log ` x ) ) / x ) ) ) )
47 15 rpne0d 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> x =/= 0 )
48 22 rpcnne0d 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( theta ` x ) e. CC /\ ( theta ` x ) =/= 0 ) )
49 19 recnd 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( sqrt ` x ) x. ( log ` x ) ) e. CC )
50 dmdcan 
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ ( ( theta ` x ) e. CC /\ ( theta ` x ) =/= 0 ) /\ ( ( sqrt ` x ) x. ( log ` x ) ) e. CC ) -> ( ( x / ( theta ` x ) ) x. ( ( ( sqrt ` x ) x. ( log ` x ) ) / x ) ) = ( ( ( sqrt ` x ) x. ( log ` x ) ) / ( theta ` x ) ) )
51 32 47 48 49 50 syl211anc 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( x / ( theta ` x ) ) x. ( ( ( sqrt ` x ) x. ( log ` x ) ) / x ) ) = ( ( ( sqrt ` x ) x. ( log ` x ) ) / ( theta ` x ) ) )
52 51 mpteq2dva 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( x / ( theta ` x ) ) x. ( ( ( sqrt ` x ) x. ( log ` x ) ) / x ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( ( sqrt ` x ) x. ( log ` x ) ) / ( theta ` x ) ) ) )
53 46 52 eqtrd 
 |-  ( T. -> ( ( x e. ( 2 [,) +oo ) |-> ( x / ( theta ` x ) ) ) oF x. ( x e. ( 2 [,) +oo ) |-> ( ( log ` x ) / ( x ^c ( 1 / 2 ) ) ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( ( sqrt ` x ) x. ( log ` x ) ) / ( theta ` x ) ) ) )
54 chto1lb 
 |-  ( x e. ( 2 [,) +oo ) |-> ( x / ( theta ` x ) ) ) e. O(1)
55 14 ssriv 
 |-  ( 2 [,) +oo ) C_ RR+
56 55 a1i 
 |-  ( T. -> ( 2 [,) +oo ) C_ RR+ )
57 1rp 
 |-  1 e. RR+
58 rphalfcl 
 |-  ( 1 e. RR+ -> ( 1 / 2 ) e. RR+ )
59 57 58 ax-mp 
 |-  ( 1 / 2 ) e. RR+
60 cxploglim 
 |-  ( ( 1 / 2 ) e. RR+ -> ( x e. RR+ |-> ( ( log ` x ) / ( x ^c ( 1 / 2 ) ) ) ) ~~>r 0 )
61 59 60 ax-mp 
 |-  ( x e. RR+ |-> ( ( log ` x ) / ( x ^c ( 1 / 2 ) ) ) ) ~~>r 0
62 61 a1i 
 |-  ( T. -> ( x e. RR+ |-> ( ( log ` x ) / ( x ^c ( 1 / 2 ) ) ) ) ~~>r 0 )
63 56 62 rlimres2 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( log ` x ) / ( x ^c ( 1 / 2 ) ) ) ) ~~>r 0 )
64 o1rlimmul 
 |-  ( ( ( x e. ( 2 [,) +oo ) |-> ( x / ( theta ` x ) ) ) e. O(1) /\ ( x e. ( 2 [,) +oo ) |-> ( ( log ` x ) / ( x ^c ( 1 / 2 ) ) ) ) ~~>r 0 ) -> ( ( x e. ( 2 [,) +oo ) |-> ( x / ( theta ` x ) ) ) oF x. ( x e. ( 2 [,) +oo ) |-> ( ( log ` x ) / ( x ^c ( 1 / 2 ) ) ) ) ) ~~>r 0 )
65 54 63 64 sylancr 
 |-  ( T. -> ( ( x e. ( 2 [,) +oo ) |-> ( x / ( theta ` x ) ) ) oF x. ( x e. ( 2 [,) +oo ) |-> ( ( log ` x ) / ( x ^c ( 1 / 2 ) ) ) ) ) ~~>r 0 )
66 53 65 eqbrtrrd 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( ( sqrt ` x ) x. ( log ` x ) ) / ( theta ` x ) ) ) ~~>r 0 )
67 2 23 27 66 rlimadd 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( 1 + ( ( ( sqrt ` x ) x. ( log ` x ) ) / ( theta ` x ) ) ) ) ~~>r ( 1 + 0 ) )
68 1p0e1 
 |-  ( 1 + 0 ) = 1
69 67 68 breqtrdi 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( 1 + ( ( ( sqrt ` x ) x. ( log ` x ) ) / ( theta ` x ) ) ) ) ~~>r 1 )
70 1re 
 |-  1 e. RR
71 readdcl 
 |-  ( ( 1 e. RR /\ ( ( ( sqrt ` x ) x. ( log ` x ) ) / ( theta ` x ) ) e. RR ) -> ( 1 + ( ( ( sqrt ` x ) x. ( log ` x ) ) / ( theta ` x ) ) ) e. RR )
72 70 23 71 sylancr 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( 1 + ( ( ( sqrt ` x ) x. ( log ` x ) ) / ( theta ` x ) ) ) e. RR )
73 chpcl 
 |-  ( x e. RR -> ( psi ` x ) e. RR )
74 7 73 syl 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( psi ` x ) e. RR )
75 74 22 rerpdivcld 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( psi ` x ) / ( theta ` x ) ) e. RR )
76 chtcl 
 |-  ( x e. RR -> ( theta ` x ) e. RR )
77 7 76 syl 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( theta ` x ) e. RR )
78 77 19 readdcld 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( theta ` x ) + ( ( sqrt ` x ) x. ( log ` x ) ) ) e. RR )
79 3 a1i 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> 2 e. RR )
80 1le2 
 |-  1 <_ 2
81 80 a1i 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> 1 <_ 2 )
82 2 79 7 81 20 letrd 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> 1 <_ x )
83 chpub 
 |-  ( ( x e. RR /\ 1 <_ x ) -> ( psi ` x ) <_ ( ( theta ` x ) + ( ( sqrt ` x ) x. ( log ` x ) ) ) )
84 7 82 83 syl2anc 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( psi ` x ) <_ ( ( theta ` x ) + ( ( sqrt ` x ) x. ( log ` x ) ) ) )
85 74 78 22 84 lediv1dd 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( psi ` x ) / ( theta ` x ) ) <_ ( ( ( theta ` x ) + ( ( sqrt ` x ) x. ( log ` x ) ) ) / ( theta ` x ) ) )
86 22 rpcnd 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( theta ` x ) e. CC )
87 divdir 
 |-  ( ( ( theta ` x ) e. CC /\ ( ( sqrt ` x ) x. ( log ` x ) ) e. CC /\ ( ( theta ` x ) e. CC /\ ( theta ` x ) =/= 0 ) ) -> ( ( ( theta ` x ) + ( ( sqrt ` x ) x. ( log ` x ) ) ) / ( theta ` x ) ) = ( ( ( theta ` x ) / ( theta ` x ) ) + ( ( ( sqrt ` x ) x. ( log ` x ) ) / ( theta ` x ) ) ) )
88 86 49 48 87 syl3anc 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( ( theta ` x ) + ( ( sqrt ` x ) x. ( log ` x ) ) ) / ( theta ` x ) ) = ( ( ( theta ` x ) / ( theta ` x ) ) + ( ( ( sqrt ` x ) x. ( log ` x ) ) / ( theta ` x ) ) ) )
89 divid 
 |-  ( ( ( theta ` x ) e. CC /\ ( theta ` x ) =/= 0 ) -> ( ( theta ` x ) / ( theta ` x ) ) = 1 )
90 48 89 syl 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( theta ` x ) / ( theta ` x ) ) = 1 )
91 90 oveq1d 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( ( theta ` x ) / ( theta ` x ) ) + ( ( ( sqrt ` x ) x. ( log ` x ) ) / ( theta ` x ) ) ) = ( 1 + ( ( ( sqrt ` x ) x. ( log ` x ) ) / ( theta ` x ) ) ) )
92 88 91 eqtrd 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( ( theta ` x ) + ( ( sqrt ` x ) x. ( log ` x ) ) ) / ( theta ` x ) ) = ( 1 + ( ( ( sqrt ` x ) x. ( log ` x ) ) / ( theta ` x ) ) ) )
93 85 92 breqtrd 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( psi ` x ) / ( theta ` x ) ) <_ ( 1 + ( ( ( sqrt ` x ) x. ( log ` x ) ) / ( theta ` x ) ) ) )
94 93 adantrr 
 |-  ( ( T. /\ ( x e. ( 2 [,) +oo ) /\ 1 <_ x ) ) -> ( ( psi ` x ) / ( theta ` x ) ) <_ ( 1 + ( ( ( sqrt ` x ) x. ( log ` x ) ) / ( theta ` x ) ) ) )
95 86 mulid2d 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( 1 x. ( theta ` x ) ) = ( theta ` x ) )
96 chtlepsi 
 |-  ( x e. RR -> ( theta ` x ) <_ ( psi ` x ) )
97 7 96 syl 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( theta ` x ) <_ ( psi ` x ) )
98 95 97 eqbrtrd 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( 1 x. ( theta ` x ) ) <_ ( psi ` x ) )
99 2 74 22 lemuldivd 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( 1 x. ( theta ` x ) ) <_ ( psi ` x ) <-> 1 <_ ( ( psi ` x ) / ( theta ` x ) ) ) )
100 98 99 mpbid 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> 1 <_ ( ( psi ` x ) / ( theta ` x ) ) )
101 100 adantrr 
 |-  ( ( T. /\ ( x e. ( 2 [,) +oo ) /\ 1 <_ x ) ) -> 1 <_ ( ( psi ` x ) / ( theta ` x ) ) )
102 1 1 69 72 75 94 101 rlimsqz2 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( psi ` x ) / ( theta ` x ) ) ) ~~>r 1 )
103 102 mptru 
 |-  ( x e. ( 2 [,) +oo ) |-> ( ( psi ` x ) / ( theta ` x ) ) ) ~~>r 1