This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem chtppilim

Description: The theta function is asymptotic to ppi ( x ) log ( x ) , so it is sufficient to prove theta ( x ) / x ~>r 1 to establish the PNT. (Contributed by Mario Carneiro, 22-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 halfre 
 |-  ( 1 / 2 ) e. RR
2 1re 
 |-  1 e. RR
3 rpre 
 |-  ( y e. RR+ -> y e. RR )
4 resubcl 
 |-  ( ( 1 e. RR /\ y e. RR ) -> ( 1 - y ) e. RR )
5 2 3 4 sylancr 
 |-  ( y e. RR+ -> ( 1 - y ) e. RR )
6 ifcl 
 |-  ( ( ( 1 / 2 ) e. RR /\ ( 1 - y ) e. RR ) -> if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) e. RR )
7 1 5 6 sylancr 
 |-  ( y e. RR+ -> if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) e. RR )
8 0red 
 |-  ( y e. RR+ -> 0 e. RR )
9 1 a1i 
 |-  ( y e. RR+ -> ( 1 / 2 ) e. RR )
10 halfgt0 
 |-  0 < ( 1 / 2 )
11 10 a1i 
 |-  ( y e. RR+ -> 0 < ( 1 / 2 ) )
12 max2 
 |-  ( ( ( 1 - y ) e. RR /\ ( 1 / 2 ) e. RR ) -> ( 1 / 2 ) <_ if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) )
13 5 1 12 sylancl 
 |-  ( y e. RR+ -> ( 1 / 2 ) <_ if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) )
14 8 9 7 11 13 ltletrd 
 |-  ( y e. RR+ -> 0 < if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) )
15 7 14 elrpd 
 |-  ( y e. RR+ -> if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) e. RR+ )
16 15 rpsqrtcld 
 |-  ( y e. RR+ -> ( sqrt ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) e. RR+ )
17 halflt1 
 |-  ( 1 / 2 ) < 1
18 ltsubrp 
 |-  ( ( 1 e. RR /\ y e. RR+ ) -> ( 1 - y ) < 1 )
19 2 18 mpan 
 |-  ( y e. RR+ -> ( 1 - y ) < 1 )
20 breq1 
 |-  ( ( 1 / 2 ) = if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) -> ( ( 1 / 2 ) < 1 <-> if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) < 1 ) )
21 breq1 
 |-  ( ( 1 - y ) = if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) -> ( ( 1 - y ) < 1 <-> if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) < 1 ) )
22 20 21 ifboth 
 |-  ( ( ( 1 / 2 ) < 1 /\ ( 1 - y ) < 1 ) -> if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) < 1 )
23 17 19 22 sylancr 
 |-  ( y e. RR+ -> if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) < 1 )
24 15 rpge0d 
 |-  ( y e. RR+ -> 0 <_ if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) )
25 2 a1i 
 |-  ( y e. RR+ -> 1 e. RR )
26 0le1 
 |-  0 <_ 1
27 26 a1i 
 |-  ( y e. RR+ -> 0 <_ 1 )
28 7 24 25 27 sqrtltd 
 |-  ( y e. RR+ -> ( if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) < 1 <-> ( sqrt ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) < ( sqrt ` 1 ) ) )
29 23 28 mpbid 
 |-  ( y e. RR+ -> ( sqrt ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) < ( sqrt ` 1 ) )
30 sqrt1 
 |-  ( sqrt ` 1 ) = 1
31 29 30 breqtrdi 
 |-  ( y e. RR+ -> ( sqrt ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) < 1 )
32 16 31 chtppilimlem2 
 |-  ( y e. RR+ -> E. z e. RR A. x e. ( 2 [,) +oo ) ( z <_ x -> ( ( ( sqrt ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) ^ 2 ) x. ( ( ppi ` x ) x. ( log ` x ) ) ) < ( theta ` x ) ) )
33 5 adantr 
 |-  ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( 1 - y ) e. RR )
34 max1 
 |-  ( ( ( 1 - y ) e. RR /\ ( 1 / 2 ) e. RR ) -> ( 1 - y ) <_ if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) )
35 33 1 34 sylancl 
 |-  ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( 1 - y ) <_ if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) )
36 7 adantr 
 |-  ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) e. RR )
37 2re 
 |-  2 e. RR
38 elicopnf 
 |-  ( 2 e. RR -> ( x e. ( 2 [,) +oo ) <-> ( x e. RR /\ 2 <_ x ) ) )
39 37 38 ax-mp 
 |-  ( x e. ( 2 [,) +oo ) <-> ( x e. RR /\ 2 <_ x ) )
40 39 simplbi 
 |-  ( x e. ( 2 [,) +oo ) -> x e. RR )
41 chtcl 
 |-  ( x e. RR -> ( theta ` x ) e. RR )
42 40 41 syl 
 |-  ( x e. ( 2 [,) +oo ) -> ( theta ` x ) e. RR )
43 ppinncl 
 |-  ( ( x e. RR /\ 2 <_ x ) -> ( ppi ` x ) e. NN )
44 39 43 sylbi 
 |-  ( x e. ( 2 [,) +oo ) -> ( ppi ` x ) e. NN )
45 44 nnrpd 
 |-  ( x e. ( 2 [,) +oo ) -> ( ppi ` x ) e. RR+ )
46 2 a1i 
 |-  ( x e. ( 2 [,) +oo ) -> 1 e. RR )
47 37 a1i 
 |-  ( x e. ( 2 [,) +oo ) -> 2 e. RR )
48 1lt2 
 |-  1 < 2
49 48 a1i 
 |-  ( x e. ( 2 [,) +oo ) -> 1 < 2 )
50 39 simprbi 
 |-  ( x e. ( 2 [,) +oo ) -> 2 <_ x )
51 46 47 40 49 50 ltletrd 
 |-  ( x e. ( 2 [,) +oo ) -> 1 < x )
52 40 51 rplogcld 
 |-  ( x e. ( 2 [,) +oo ) -> ( log ` x ) e. RR+ )
53 45 52 rpmulcld 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ppi ` x ) x. ( log ` x ) ) e. RR+ )
54 42 53 rerpdivcld 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) e. RR )
55 54 adantl 
 |-  ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) e. RR )
56 lelttr 
 |-  ( ( ( 1 - y ) e. RR /\ if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) e. RR /\ ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) e. RR ) -> ( ( ( 1 - y ) <_ if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) /\ if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) < ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) -> ( 1 - y ) < ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) )
57 33 36 55 56 syl3anc 
 |-  ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( ( 1 - y ) <_ if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) /\ if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) < ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) -> ( 1 - y ) < ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) )
58 35 57 mpand 
 |-  ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) < ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) -> ( 1 - y ) < ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) )
59 7 recnd 
 |-  ( y e. RR+ -> if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) e. CC )
60 59 sqsqrtd 
 |-  ( y e. RR+ -> ( ( sqrt ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) ^ 2 ) = if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) )
61 60 adantr 
 |-  ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( sqrt ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) ^ 2 ) = if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) )
62 61 oveq1d 
 |-  ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( ( sqrt ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) ^ 2 ) x. ( ( ppi ` x ) x. ( log ` x ) ) ) = ( if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) x. ( ( ppi ` x ) x. ( log ` x ) ) ) )
63 62 breq1d 
 |-  ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( ( ( sqrt ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) ^ 2 ) x. ( ( ppi ` x ) x. ( log ` x ) ) ) < ( theta ` x ) <-> ( if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) x. ( ( ppi ` x ) x. ( log ` x ) ) ) < ( theta ` x ) ) )
64 42 adantl 
 |-  ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( theta ` x ) e. RR )
65 53 rpregt0d 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ( ppi ` x ) x. ( log ` x ) ) e. RR /\ 0 < ( ( ppi ` x ) x. ( log ` x ) ) ) )
66 65 adantl 
 |-  ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( ( ppi ` x ) x. ( log ` x ) ) e. RR /\ 0 < ( ( ppi ` x ) x. ( log ` x ) ) ) )
67 ltmuldiv 
 |-  ( ( if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) e. RR /\ ( theta ` x ) e. RR /\ ( ( ( ppi ` x ) x. ( log ` x ) ) e. RR /\ 0 < ( ( ppi ` x ) x. ( log ` x ) ) ) ) -> ( ( if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) x. ( ( ppi ` x ) x. ( log ` x ) ) ) < ( theta ` x ) <-> if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) < ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) )
68 36 64 66 67 syl3anc 
 |-  ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) x. ( ( ppi ` x ) x. ( log ` x ) ) ) < ( theta ` x ) <-> if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) < ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) )
69 63 68 bitrd 
 |-  ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( ( ( sqrt ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) ^ 2 ) x. ( ( ppi ` x ) x. ( log ` x ) ) ) < ( theta ` x ) <-> if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) < ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) )
70 0red 
 |-  ( x e. ( 2 [,) +oo ) -> 0 e. RR )
71 2pos 
 |-  0 < 2
72 71 a1i 
 |-  ( x e. ( 2 [,) +oo ) -> 0 < 2 )
73 70 47 40 72 50 ltletrd 
 |-  ( x e. ( 2 [,) +oo ) -> 0 < x )
74 40 73 elrpd 
 |-  ( x e. ( 2 [,) +oo ) -> x e. RR+ )
75 chtleppi 
 |-  ( x e. RR+ -> ( theta ` x ) <_ ( ( ppi ` x ) x. ( log ` x ) ) )
76 74 75 syl 
 |-  ( x e. ( 2 [,) +oo ) -> ( theta ` x ) <_ ( ( ppi ` x ) x. ( log ` x ) ) )
77 53 rpcnd 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ppi ` x ) x. ( log ` x ) ) e. CC )
78 77 mulridd 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ( ppi ` x ) x. ( log ` x ) ) x. 1 ) = ( ( ppi ` x ) x. ( log ` x ) ) )
79 76 78 breqtrrd 
 |-  ( x e. ( 2 [,) +oo ) -> ( theta ` x ) <_ ( ( ( ppi ` x ) x. ( log ` x ) ) x. 1 ) )
80 42 46 53 ledivmuld 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) <_ 1 <-> ( theta ` x ) <_ ( ( ( ppi ` x ) x. ( log ` x ) ) x. 1 ) ) )
81 79 80 mpbird 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) <_ 1 )
82 54 46 81 abssuble0d 
 |-  ( x e. ( 2 [,) +oo ) -> ( abs ` ( ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) - 1 ) ) = ( 1 - ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) )
83 82 breq1d 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( abs ` ( ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) - 1 ) ) < y <-> ( 1 - ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) < y ) )
84 83 adantl 
 |-  ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( abs ` ( ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) - 1 ) ) < y <-> ( 1 - ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) < y ) )
85 2 a1i 
 |-  ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> 1 e. RR )
86 3 adantr 
 |-  ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> y e. RR )
87 ltsub23 
 |-  ( ( 1 e. RR /\ ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) e. RR /\ y e. RR ) -> ( ( 1 - ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) < y <-> ( 1 - y ) < ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) )
88 85 55 86 87 syl3anc 
 |-  ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( 1 - ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) < y <-> ( 1 - y ) < ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) )
89 84 88 bitrd 
 |-  ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( abs ` ( ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) - 1 ) ) < y <-> ( 1 - y ) < ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) )
90 58 69 89 3imtr4d 
 |-  ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( ( ( sqrt ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) ^ 2 ) x. ( ( ppi ` x ) x. ( log ` x ) ) ) < ( theta ` x ) -> ( abs ` ( ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) - 1 ) ) < y ) )
91 90 imim2d 
 |-  ( ( y e. RR+ /\ x e. ( 2 [,) +oo ) ) -> ( ( z <_ x -> ( ( ( sqrt ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) ^ 2 ) x. ( ( ppi ` x ) x. ( log ` x ) ) ) < ( theta ` x ) ) -> ( z <_ x -> ( abs ` ( ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) - 1 ) ) < y ) ) )
92 91 ralimdva 
 |-  ( y e. RR+ -> ( A. x e. ( 2 [,) +oo ) ( z <_ x -> ( ( ( sqrt ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) ^ 2 ) x. ( ( ppi ` x ) x. ( log ` x ) ) ) < ( theta ` x ) ) -> A. x e. ( 2 [,) +oo ) ( z <_ x -> ( abs ` ( ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) - 1 ) ) < y ) ) )
93 92 reximdv 
 |-  ( y e. RR+ -> ( E. z e. RR A. x e. ( 2 [,) +oo ) ( z <_ x -> ( ( ( sqrt ` if ( ( 1 - y ) <_ ( 1 / 2 ) , ( 1 / 2 ) , ( 1 - y ) ) ) ^ 2 ) x. ( ( ppi ` x ) x. ( log ` x ) ) ) < ( theta ` x ) ) -> E. z e. RR A. x e. ( 2 [,) +oo ) ( z <_ x -> ( abs ` ( ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) - 1 ) ) < y ) ) )
94 32 93 mpd 
 |-  ( y e. RR+ -> E. z e. RR A. x e. ( 2 [,) +oo ) ( z <_ x -> ( abs ` ( ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) - 1 ) ) < y ) )
95 94 rgen 
 |-  A. y e. RR+ E. z e. RR A. x e. ( 2 [,) +oo ) ( z <_ x -> ( abs ` ( ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) - 1 ) ) < y )
96 54 recnd 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) e. CC )
97 96 adantl 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) e. CC )
98 97 ralrimiva 
 |-  ( T. -> A. x e. ( 2 [,) +oo ) ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) e. CC )
99 40 ssriv 
 |-  ( 2 [,) +oo ) C_ RR
100 99 a1i 
 |-  ( T. -> ( 2 [,) +oo ) C_ RR )
101 1cnd 
 |-  ( T. -> 1 e. CC )
102 98 100 101 rlim2 
 |-  ( T. -> ( ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ~~>r 1 <-> A. y e. RR+ E. z e. RR A. x e. ( 2 [,) +oo ) ( z <_ x -> ( abs ` ( ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) - 1 ) ) < y ) ) )
103 95 102 mpbiri 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ~~>r 1 )
104 103 mptru 
 |-  ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ~~>r 1