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