Metamath Proof Explorer

Theorem chtppilimlem2

Description: Lemma for chtppilim . (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Hypotheses chtppilim.1 
|- ( ph -> A e. RR+ )
chtppilim.2 
|- ( ph -> A < 1 )
Assertion chtppilimlem2 
|- ( ph -> E. z e. RR A. x e. ( 2 [,) +oo ) ( z <_ x -> ( ( A ^ 2 ) x. ( ( ppi ` x ) x. ( log ` x ) ) ) < ( theta ` x ) ) )

Proof

Step Hyp Ref Expression
1 chtppilim.1 
 |-  ( ph -> A e. RR+ )
2 chtppilim.2 
 |-  ( ph -> A < 1 )
3 simpr 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> x e. ( 2 [,) +oo ) )
4 2re 
 |-  2 e. RR
5 elicopnf 
 |-  ( 2 e. RR -> ( x e. ( 2 [,) +oo ) <-> ( x e. RR /\ 2 <_ x ) ) )
6 4 5 ax-mp 
 |-  ( x e. ( 2 [,) +oo ) <-> ( x e. RR /\ 2 <_ x ) )
7 3 6 sylib 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( x e. RR /\ 2 <_ x ) )
8 7 simpld 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> x e. RR )
9 0red 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> 0 e. RR )
10 4 a1i 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> 2 e. RR )
11 2pos 
 |-  0 < 2
12 11 a1i 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> 0 < 2 )
13 7 simprd 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> 2 <_ x )
14 9 10 8 12 13 ltletrd 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> 0 < x )
15 8 14 elrpd 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> x e. RR+ )
16 1 rpred 
 |-  ( ph -> A e. RR )
17 16 adantr 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> A e. RR )
18 15 17 rpcxpcld 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( x ^c A ) e. RR+ )
19 ppinncl 
 |-  ( ( x e. RR /\ 2 <_ x ) -> ( ppi ` x ) e. NN )
20 7 19 syl 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( ppi ` x ) e. NN )
21 20 nnrpd 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( ppi ` x ) e. RR+ )
22 18 21 rpdivcld 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( ( x ^c A ) / ( ppi ` x ) ) e. RR+ )
23 22 ralrimiva 
 |-  ( ph -> A. x e. ( 2 [,) +oo ) ( ( x ^c A ) / ( ppi ` x ) ) e. RR+ )
24 1re 
 |-  1 e. RR
25 difrp 
 |-  ( ( A e. RR /\ 1 e. RR ) -> ( A < 1 <-> ( 1 - A ) e. RR+ ) )
26 16 24 25 sylancl 
 |-  ( ph -> ( A < 1 <-> ( 1 - A ) e. RR+ ) )
27 2 26 mpbid 
 |-  ( ph -> ( 1 - A ) e. RR+ )
28 ovexd 
 |-  ( ph -> ( 2 [,) +oo ) e. _V )
29 24 a1i 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> 1 e. RR )
30 1lt2 
 |-  1 < 2
31 30 a1i 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> 1 < 2 )
32 29 10 8 31 13 ltletrd 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> 1 < x )
33 8 32 rplogcld 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( log ` x ) e. RR+ )
34 15 33 rpdivcld 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( x / ( log ` x ) ) e. RR+ )
35 34 21 rpdivcld 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) e. RR+ )
36 27 adantr 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( 1 - A ) e. RR+ )
37 36 rpred 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( 1 - A ) e. RR )
38 15 37 rpcxpcld 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( x ^c ( 1 - A ) ) e. RR+ )
39 33 38 rpdivcld 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) e. RR+ )
40 eqidd 
 |-  ( ph -> ( x e. ( 2 [,) +oo ) |-> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) )
41 eqidd 
 |-  ( ph -> ( x e. ( 2 [,) +oo ) |-> ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) ) )
42 28 35 39 40 41 offval2 
 |-  ( ph -> ( ( x e. ( 2 [,) +oo ) |-> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) oF x. ( x e. ( 2 [,) +oo ) |-> ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( ( x / ( log ` x ) ) / ( ppi ` x ) ) x. ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) ) ) )
43 34 rpcnd 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( x / ( log ` x ) ) e. CC )
44 39 rpcnd 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) e. CC )
45 21 rpcnne0d 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( ( ppi ` x ) e. CC /\ ( ppi ` x ) =/= 0 ) )
46 div23 
 |-  ( ( ( x / ( log ` x ) ) e. CC /\ ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) e. CC /\ ( ( ppi ` x ) e. CC /\ ( ppi ` x ) =/= 0 ) ) -> ( ( ( x / ( log ` x ) ) x. ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) ) / ( ppi ` x ) ) = ( ( ( x / ( log ` x ) ) / ( ppi ` x ) ) x. ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) ) )
47 43 44 45 46 syl3anc 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( ( ( x / ( log ` x ) ) x. ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) ) / ( ppi ` x ) ) = ( ( ( x / ( log ` x ) ) / ( ppi ` x ) ) x. ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) ) )
48 33 rpcnne0d 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( ( log ` x ) e. CC /\ ( log ` x ) =/= 0 ) )
49 38 rpcnne0d 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( ( x ^c ( 1 - A ) ) e. CC /\ ( x ^c ( 1 - A ) ) =/= 0 ) )
50 8 recnd 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> x e. CC )
51 dmdcan 
 |-  ( ( ( ( log ` x ) e. CC /\ ( log ` x ) =/= 0 ) /\ ( ( x ^c ( 1 - A ) ) e. CC /\ ( x ^c ( 1 - A ) ) =/= 0 ) /\ x e. CC ) -> ( ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) x. ( x / ( log ` x ) ) ) = ( x / ( x ^c ( 1 - A ) ) ) )
52 48 49 50 51 syl3anc 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) x. ( x / ( log ` x ) ) ) = ( x / ( x ^c ( 1 - A ) ) ) )
53 43 44 mulcomd 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( ( x / ( log ` x ) ) x. ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) ) = ( ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) x. ( x / ( log ` x ) ) ) )
54 15 rpcnne0d 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( x e. CC /\ x =/= 0 ) )
55 ax-1cn 
 |-  1 e. CC
56 55 a1i 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> 1 e. CC )
57 36 rpcnd 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( 1 - A ) e. CC )
58 cxpsub 
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ 1 e. CC /\ ( 1 - A ) e. CC ) -> ( x ^c ( 1 - ( 1 - A ) ) ) = ( ( x ^c 1 ) / ( x ^c ( 1 - A ) ) ) )
59 54 56 57 58 syl3anc 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( x ^c ( 1 - ( 1 - A ) ) ) = ( ( x ^c 1 ) / ( x ^c ( 1 - A ) ) ) )
60 17 recnd 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> A e. CC )
61 nncan 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( 1 - ( 1 - A ) ) = A )
62 55 60 61 sylancr 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( 1 - ( 1 - A ) ) = A )
63 62 oveq2d 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( x ^c ( 1 - ( 1 - A ) ) ) = ( x ^c A ) )
64 59 63 eqtr3d 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( ( x ^c 1 ) / ( x ^c ( 1 - A ) ) ) = ( x ^c A ) )
65 50 cxp1d 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( x ^c 1 ) = x )
66 65 oveq1d 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( ( x ^c 1 ) / ( x ^c ( 1 - A ) ) ) = ( x / ( x ^c ( 1 - A ) ) ) )
67 64 66 eqtr3d 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( x ^c A ) = ( x / ( x ^c ( 1 - A ) ) ) )
68 52 53 67 3eqtr4d 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( ( x / ( log ` x ) ) x. ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) ) = ( x ^c A ) )
69 68 oveq1d 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( ( ( x / ( log ` x ) ) x. ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) ) / ( ppi ` x ) ) = ( ( x ^c A ) / ( ppi ` x ) ) )
70 47 69 eqtr3d 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( ( ( x / ( log ` x ) ) / ( ppi ` x ) ) x. ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) ) = ( ( x ^c A ) / ( ppi ` x ) ) )
71 70 mpteq2dva 
 |-  ( ph -> ( x e. ( 2 [,) +oo ) |-> ( ( ( x / ( log ` x ) ) / ( ppi ` x ) ) x. ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( x ^c A ) / ( ppi ` x ) ) ) )
72 42 71 eqtrd 
 |-  ( ph -> ( ( x e. ( 2 [,) +oo ) |-> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) oF x. ( x e. ( 2 [,) +oo ) |-> ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( x ^c A ) / ( ppi ` x ) ) ) )
73 chebbnd1 
 |-  ( x e. ( 2 [,) +oo ) |-> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) e. O(1)
74 15 ex 
 |-  ( ph -> ( x e. ( 2 [,) +oo ) -> x e. RR+ ) )
75 74 ssrdv 
 |-  ( ph -> ( 2 [,) +oo ) C_ RR+ )
76 cxploglim 
 |-  ( ( 1 - A ) e. RR+ -> ( x e. RR+ |-> ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) ) ~~>r 0 )
77 27 76 syl 
 |-  ( ph -> ( x e. RR+ |-> ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) ) ~~>r 0 )
78 75 77 rlimres2 
 |-  ( ph -> ( x e. ( 2 [,) +oo ) |-> ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) ) ~~>r 0 )
79 o1rlimmul 
 |-  ( ( ( x e. ( 2 [,) +oo ) |-> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) e. O(1) /\ ( x e. ( 2 [,) +oo ) |-> ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) ) ~~>r 0 ) -> ( ( x e. ( 2 [,) +oo ) |-> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) oF x. ( x e. ( 2 [,) +oo ) |-> ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) ) ) ~~>r 0 )
80 73 78 79 sylancr 
 |-  ( ph -> ( ( x e. ( 2 [,) +oo ) |-> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) oF x. ( x e. ( 2 [,) +oo ) |-> ( ( log ` x ) / ( x ^c ( 1 - A ) ) ) ) ) ~~>r 0 )
81 72 80 eqbrtrrd 
 |-  ( ph -> ( x e. ( 2 [,) +oo ) |-> ( ( x ^c A ) / ( ppi ` x ) ) ) ~~>r 0 )
82 23 27 81 rlimi 
 |-  ( ph -> E. z e. RR A. x e. ( 2 [,) +oo ) ( z <_ x -> ( abs ` ( ( ( x ^c A ) / ( ppi ` x ) ) - 0 ) ) < ( 1 - A ) ) )
83 22 rpcnd 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( ( x ^c A ) / ( ppi ` x ) ) e. CC )
84 83 subid1d 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( ( ( x ^c A ) / ( ppi ` x ) ) - 0 ) = ( ( x ^c A ) / ( ppi ` x ) ) )
85 84 fveq2d 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( abs ` ( ( ( x ^c A ) / ( ppi ` x ) ) - 0 ) ) = ( abs ` ( ( x ^c A ) / ( ppi ` x ) ) ) )
86 22 rpred 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( ( x ^c A ) / ( ppi ` x ) ) e. RR )
87 22 rpge0d 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> 0 <_ ( ( x ^c A ) / ( ppi ` x ) ) )
88 86 87 absidd 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( abs ` ( ( x ^c A ) / ( ppi ` x ) ) ) = ( ( x ^c A ) / ( ppi ` x ) ) )
89 85 88 eqtrd 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( abs ` ( ( ( x ^c A ) / ( ppi ` x ) ) - 0 ) ) = ( ( x ^c A ) / ( ppi ` x ) ) )
90 89 breq1d 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( ( abs ` ( ( ( x ^c A ) / ( ppi ` x ) ) - 0 ) ) < ( 1 - A ) <-> ( ( x ^c A ) / ( ppi ` x ) ) < ( 1 - A ) ) )
91 1 adantr 
 |-  ( ( ph /\ ( x e. ( 2 [,) +oo ) /\ ( ( x ^c A ) / ( ppi ` x ) ) < ( 1 - A ) ) ) -> A e. RR+ )
92 2 adantr 
 |-  ( ( ph /\ ( x e. ( 2 [,) +oo ) /\ ( ( x ^c A ) / ( ppi ` x ) ) < ( 1 - A ) ) ) -> A < 1 )
93 simprl 
 |-  ( ( ph /\ ( x e. ( 2 [,) +oo ) /\ ( ( x ^c A ) / ( ppi ` x ) ) < ( 1 - A ) ) ) -> x e. ( 2 [,) +oo ) )
94 simprr 
 |-  ( ( ph /\ ( x e. ( 2 [,) +oo ) /\ ( ( x ^c A ) / ( ppi ` x ) ) < ( 1 - A ) ) ) -> ( ( x ^c A ) / ( ppi ` x ) ) < ( 1 - A ) )
95 91 92 93 94 chtppilimlem1 
 |-  ( ( ph /\ ( x e. ( 2 [,) +oo ) /\ ( ( x ^c A ) / ( ppi ` x ) ) < ( 1 - A ) ) ) -> ( ( A ^ 2 ) x. ( ( ppi ` x ) x. ( log ` x ) ) ) < ( theta ` x ) )
96 95 expr 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( ( ( x ^c A ) / ( ppi ` x ) ) < ( 1 - A ) -> ( ( A ^ 2 ) x. ( ( ppi ` x ) x. ( log ` x ) ) ) < ( theta ` x ) ) )
97 90 96 sylbid 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( ( abs ` ( ( ( x ^c A ) / ( ppi ` x ) ) - 0 ) ) < ( 1 - A ) -> ( ( A ^ 2 ) x. ( ( ppi ` x ) x. ( log ` x ) ) ) < ( theta ` x ) ) )
98 97 imim2d 
 |-  ( ( ph /\ x e. ( 2 [,) +oo ) ) -> ( ( z <_ x -> ( abs ` ( ( ( x ^c A ) / ( ppi ` x ) ) - 0 ) ) < ( 1 - A ) ) -> ( z <_ x -> ( ( A ^ 2 ) x. ( ( ppi ` x ) x. ( log ` x ) ) ) < ( theta ` x ) ) ) )
99 98 ralimdva 
 |-  ( ph -> ( A. x e. ( 2 [,) +oo ) ( z <_ x -> ( abs ` ( ( ( x ^c A ) / ( ppi ` x ) ) - 0 ) ) < ( 1 - A ) ) -> A. x e. ( 2 [,) +oo ) ( z <_ x -> ( ( A ^ 2 ) x. ( ( ppi ` x ) x. ( log ` x ) ) ) < ( theta ` x ) ) ) )
100 99 reximdv 
 |-  ( ph -> ( E. z e. RR A. x e. ( 2 [,) +oo ) ( z <_ x -> ( abs ` ( ( ( x ^c A ) / ( ppi ` x ) ) - 0 ) ) < ( 1 - A ) ) -> E. z e. RR A. x e. ( 2 [,) +oo ) ( z <_ x -> ( ( A ^ 2 ) x. ( ( ppi ` x ) x. ( log ` x ) ) ) < ( theta ` x ) ) ) )
101 82 100 mpd 
 |-  ( ph -> E. z e. RR A. x e. ( 2 [,) +oo ) ( z <_ x -> ( ( A ^ 2 ) x. ( ( ppi ` x ) x. ( log ` x ) ) ) < ( theta ` x ) ) )