Metamath Proof Explorer

Theorem pnt

Description: The Prime Number Theorem: the number of prime numbers less than x tends asymptotically to x / log ( x ) as x goes to infinity. This is Metamath 100 proof #5. (Contributed by Mario Carneiro, 1-Jun-2016)

Ref Expression
Assertion pnt 
|- ( x e. ( 1 (,) +oo ) |-> ( ( ppi ` x ) / ( x / ( log ` x ) ) ) ) ~~>r 1

Proof

Step Hyp Ref Expression
1 1xr 
 |-  1 e. RR*
2 1lt2 
 |-  1 < 2
3 df-ioo 
 |-  (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
4 df-ico 
 |-  [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
5 xrltletr 
 |-  ( ( 1 e. RR* /\ 2 e. RR* /\ w e. RR* ) -> ( ( 1 < 2 /\ 2 <_ w ) -> 1 < w ) )
6 3 4 5 ixxss1 
 |-  ( ( 1 e. RR* /\ 1 < 2 ) -> ( 2 [,) +oo ) C_ ( 1 (,) +oo ) )
7 1 2 6 mp2an 
 |-  ( 2 [,) +oo ) C_ ( 1 (,) +oo )
8 resmpt 
 |-  ( ( 2 [,) +oo ) C_ ( 1 (,) +oo ) -> ( ( x e. ( 1 (,) +oo ) |-> ( ( ppi ` x ) / ( x / ( log ` x ) ) ) ) |` ( 2 [,) +oo ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( ppi ` x ) / ( x / ( log ` x ) ) ) ) )
9 7 8 mp1i 
 |-  ( T. -> ( ( x e. ( 1 (,) +oo ) |-> ( ( ppi ` x ) / ( x / ( log ` x ) ) ) ) |` ( 2 [,) +oo ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( ppi ` x ) / ( x / ( log ` x ) ) ) ) )
10 7 sseli 
 |-  ( x e. ( 2 [,) +oo ) -> x e. ( 1 (,) +oo ) )
11 ioossre 
 |-  ( 1 (,) +oo ) C_ RR
12 11 sseli 
 |-  ( x e. ( 1 (,) +oo ) -> x e. RR )
13 10 12 syl 
 |-  ( x e. ( 2 [,) +oo ) -> x e. RR )
14 2re 
 |-  2 e. RR
15 pnfxr 
 |-  +oo e. RR*
16 elico2 
 |-  ( ( 2 e. RR /\ +oo e. RR* ) -> ( x e. ( 2 [,) +oo ) <-> ( x e. RR /\ 2 <_ x /\ x < +oo ) ) )
17 14 15 16 mp2an 
 |-  ( x e. ( 2 [,) +oo ) <-> ( x e. RR /\ 2 <_ x /\ x < +oo ) )
18 17 simp2bi 
 |-  ( x e. ( 2 [,) +oo ) -> 2 <_ x )
19 chtrpcl 
 |-  ( ( x e. RR /\ 2 <_ x ) -> ( theta ` x ) e. RR+ )
20 13 18 19 syl2anc 
 |-  ( x e. ( 2 [,) +oo ) -> ( theta ` x ) e. RR+ )
21 0red 
 |-  ( x e. ( 1 (,) +oo ) -> 0 e. RR )
22 1red 
 |-  ( x e. ( 1 (,) +oo ) -> 1 e. RR )
23 0lt1 
 |-  0 < 1
24 23 a1i 
 |-  ( x e. ( 1 (,) +oo ) -> 0 < 1 )
25 eliooord 
 |-  ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
26 25 simpld 
 |-  ( x e. ( 1 (,) +oo ) -> 1 < x )
27 21 22 12 24 26 lttrd 
 |-  ( x e. ( 1 (,) +oo ) -> 0 < x )
28 12 27 elrpd 
 |-  ( x e. ( 1 (,) +oo ) -> x e. RR+ )
29 10 28 syl 
 |-  ( x e. ( 2 [,) +oo ) -> x e. RR+ )
30 20 29 rpdivcld 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( theta ` x ) / x ) e. RR+ )
31 30 adantl 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( theta ` x ) / x ) e. RR+ )
32 ppinncl 
 |-  ( ( x e. RR /\ 2 <_ x ) -> ( ppi ` x ) e. NN )
33 13 18 32 syl2anc 
 |-  ( x e. ( 2 [,) +oo ) -> ( ppi ` x ) e. NN )
34 33 nnrpd 
 |-  ( x e. ( 2 [,) +oo ) -> ( ppi ` x ) e. RR+ )
35 12 26 rplogcld 
 |-  ( x e. ( 1 (,) +oo ) -> ( log ` x ) e. RR+ )
36 10 35 syl 
 |-  ( x e. ( 2 [,) +oo ) -> ( log ` x ) e. RR+ )
37 34 36 rpmulcld 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ppi ` x ) x. ( log ` x ) ) e. RR+ )
38 20 37 rpdivcld 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) e. RR+ )
39 38 adantl 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) e. RR+ )
40 29 ssriv 
 |-  ( 2 [,) +oo ) C_ RR+
41 resmpt 
 |-  ( ( 2 [,) +oo ) C_ RR+ -> ( ( x e. RR+ |-> ( ( theta ` x ) / x ) ) |` ( 2 [,) +oo ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / x ) ) )
42 40 41 ax-mp 
 |-  ( ( x e. RR+ |-> ( ( theta ` x ) / x ) ) |` ( 2 [,) +oo ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / x ) )
43 pnt2 
 |-  ( x e. RR+ |-> ( ( theta ` x ) / x ) ) ~~>r 1
44 rlimres 
 |-  ( ( x e. RR+ |-> ( ( theta ` x ) / x ) ) ~~>r 1 -> ( ( x e. RR+ |-> ( ( theta ` x ) / x ) ) |` ( 2 [,) +oo ) ) ~~>r 1 )
45 43 44 mp1i 
 |-  ( T. -> ( ( x e. RR+ |-> ( ( theta ` x ) / x ) ) |` ( 2 [,) +oo ) ) ~~>r 1 )
46 42 45 eqbrtrrid 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / x ) ) ~~>r 1 )
47 chtppilim 
 |-  ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ~~>r 1
48 47 a1i 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ~~>r 1 )
49 ax-1ne0 
 |-  1 =/= 0
50 49 a1i 
 |-  ( T. -> 1 =/= 0 )
51 38 rpne0d 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) =/= 0 )
52 51 adantl 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) =/= 0 )
53 31 39 46 48 50 52 rlimdiv 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( ( theta ` x ) / x ) / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ) ~~>r ( 1 / 1 ) )
54 13 recnd 
 |-  ( x e. ( 2 [,) +oo ) -> x e. CC )
55 chtcl 
 |-  ( x e. RR -> ( theta ` x ) e. RR )
56 12 55 syl 
 |-  ( x e. ( 1 (,) +oo ) -> ( theta ` x ) e. RR )
57 56 recnd 
 |-  ( x e. ( 1 (,) +oo ) -> ( theta ` x ) e. CC )
58 10 57 syl 
 |-  ( x e. ( 2 [,) +oo ) -> ( theta ` x ) e. CC )
59 54 58 mulcomd 
 |-  ( x e. ( 2 [,) +oo ) -> ( x x. ( theta ` x ) ) = ( ( theta ` x ) x. x ) )
60 59 oveq2d 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ( theta ` x ) x. ( ( ppi ` x ) x. ( log ` x ) ) ) / ( x x. ( theta ` x ) ) ) = ( ( ( theta ` x ) x. ( ( ppi ` x ) x. ( log ` x ) ) ) / ( ( theta ` x ) x. x ) ) )
61 37 rpcnd 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ppi ` x ) x. ( log ` x ) ) e. CC )
62 29 rpne0d 
 |-  ( x e. ( 2 [,) +oo ) -> x =/= 0 )
63 20 rpne0d 
 |-  ( x e. ( 2 [,) +oo ) -> ( theta ` x ) =/= 0 )
64 61 54 58 62 63 divcan5d 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ( theta ` x ) x. ( ( ppi ` x ) x. ( log ` x ) ) ) / ( ( theta ` x ) x. x ) ) = ( ( ( ppi ` x ) x. ( log ` x ) ) / x ) )
65 60 64 eqtrd 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ( theta ` x ) x. ( ( ppi ` x ) x. ( log ` x ) ) ) / ( x x. ( theta ` x ) ) ) = ( ( ( ppi ` x ) x. ( log ` x ) ) / x ) )
66 37 rpne0d 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ppi ` x ) x. ( log ` x ) ) =/= 0 )
67 58 54 58 61 62 66 63 divdivdivd 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ( theta ` x ) / x ) / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) = ( ( ( theta ` x ) x. ( ( ppi ` x ) x. ( log ` x ) ) ) / ( x x. ( theta ` x ) ) ) )
68 33 nncnd 
 |-  ( x e. ( 2 [,) +oo ) -> ( ppi ` x ) e. CC )
69 36 rpcnd 
 |-  ( x e. ( 2 [,) +oo ) -> ( log ` x ) e. CC )
70 36 rpne0d 
 |-  ( x e. ( 2 [,) +oo ) -> ( log ` x ) =/= 0 )
71 68 54 69 62 70 divdiv2d 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ppi ` x ) / ( x / ( log ` x ) ) ) = ( ( ( ppi ` x ) x. ( log ` x ) ) / x ) )
72 65 67 71 3eqtr4d 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ( theta ` x ) / x ) / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) = ( ( ppi ` x ) / ( x / ( log ` x ) ) ) )
73 72 mpteq2ia 
 |-  ( x e. ( 2 [,) +oo ) |-> ( ( ( theta ` x ) / x ) / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( ppi ` x ) / ( x / ( log ` x ) ) ) )
74 1div1e1 
 |-  ( 1 / 1 ) = 1
75 53 73 74 3brtr3g 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( ppi ` x ) / ( x / ( log ` x ) ) ) ) ~~>r 1 )
76 9 75 eqbrtrd 
 |-  ( T. -> ( ( x e. ( 1 (,) +oo ) |-> ( ( ppi ` x ) / ( x / ( log ` x ) ) ) ) |` ( 2 [,) +oo ) ) ~~>r 1 )
77 ppicl 
 |-  ( x e. RR -> ( ppi ` x ) e. NN0 )
78 12 77 syl 
 |-  ( x e. ( 1 (,) +oo ) -> ( ppi ` x ) e. NN0 )
79 78 nn0red 
 |-  ( x e. ( 1 (,) +oo ) -> ( ppi ` x ) e. RR )
80 28 35 rpdivcld 
 |-  ( x e. ( 1 (,) +oo ) -> ( x / ( log ` x ) ) e. RR+ )
81 79 80 rerpdivcld 
 |-  ( x e. ( 1 (,) +oo ) -> ( ( ppi ` x ) / ( x / ( log ` x ) ) ) e. RR )
82 81 recnd 
 |-  ( x e. ( 1 (,) +oo ) -> ( ( ppi ` x ) / ( x / ( log ` x ) ) ) e. CC )
83 82 adantl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ppi ` x ) / ( x / ( log ` x ) ) ) e. CC )
84 83 fmpttd 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ppi ` x ) / ( x / ( log ` x ) ) ) ) : ( 1 (,) +oo ) --> CC )
85 11 a1i 
 |-  ( T. -> ( 1 (,) +oo ) C_ RR )
86 14 a1i 
 |-  ( T. -> 2 e. RR )
87 84 85 86 rlimresb 
 |-  ( T. -> ( ( x e. ( 1 (,) +oo ) |-> ( ( ppi ` x ) / ( x / ( log ` x ) ) ) ) ~~>r 1 <-> ( ( x e. ( 1 (,) +oo ) |-> ( ( ppi ` x ) / ( x / ( log ` x ) ) ) ) |` ( 2 [,) +oo ) ) ~~>r 1 ) )
88 76 87 mpbird 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ppi ` x ) / ( x / ( log ` x ) ) ) ) ~~>r 1 )
89 88 mptru 
 |-  ( x e. ( 1 (,) +oo ) |-> ( ( ppi ` x ) / ( x / ( log ` x ) ) ) ) ~~>r 1