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 mulid1d
 |-  ( 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