Metamath Proof Explorer

Theorem pntlemq

Description: Lemma for pntlemj . (Contributed by Mario Carneiro, 7-Jun-2016)

Ref Expression
Hypotheses pntlem1.r 
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
pntlem1.a 
|- ( ph -> A e. RR+ )
pntlem1.b 
|- ( ph -> B e. RR+ )
pntlem1.l 
|- ( ph -> L e. ( 0 (,) 1 ) )
pntlem1.d 
|- D = ( A + 1 )
pntlem1.f 
|- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) )
pntlem1.u 
|- ( ph -> U e. RR+ )
pntlem1.u2 
|- ( ph -> U <_ A )
pntlem1.e 
|- E = ( U / D )
pntlem1.k 
|- K = ( exp ` ( B / E ) )
pntlem1.y 
|- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )
pntlem1.x 
|- ( ph -> ( X e. RR+ /\ Y < X ) )
pntlem1.c 
|- ( ph -> C e. RR+ )
pntlem1.w 
|- W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )
pntlem1.z 
|- ( ph -> Z e. ( W [,) +oo ) )
pntlem1.m 
|- M = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 )
pntlem1.n 
|- N = ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) )
pntlem1.U 
|- ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )
pntlem1.K 
|- ( ph -> A. y e. ( X (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( L x. E ) ) x. z ) < ( K x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( L x. E ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) )
pntlem1.o 
|- O = ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ J ) ) ) )
pntlem1.v 
|- ( ph -> V e. RR+ )
pntlem1.V 
|- ( ph -> ( ( ( K ^ J ) < V /\ ( ( 1 + ( L x. E ) ) x. V ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( V [,] ( ( 1 + ( L x. E ) ) x. V ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) )
pntlem1.j 
|- ( ph -> J e. ( M ..^ N ) )
pntlem1.i 
|- I = ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) )
Assertion pntlemq 
|- ( ph -> I C_ O )

Proof

Step Hyp Ref Expression
1 pntlem1.r 
 |-  R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2 pntlem1.a 
 |-  ( ph -> A e. RR+ )
3 pntlem1.b 
 |-  ( ph -> B e. RR+ )
4 pntlem1.l 
 |-  ( ph -> L e. ( 0 (,) 1 ) )
5 pntlem1.d 
 |-  D = ( A + 1 )
6 pntlem1.f 
 |-  F = ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) )
7 pntlem1.u 
 |-  ( ph -> U e. RR+ )
8 pntlem1.u2 
 |-  ( ph -> U <_ A )
9 pntlem1.e 
 |-  E = ( U / D )
10 pntlem1.k 
 |-  K = ( exp ` ( B / E ) )
11 pntlem1.y 
 |-  ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )
12 pntlem1.x 
 |-  ( ph -> ( X e. RR+ /\ Y < X ) )
13 pntlem1.c 
 |-  ( ph -> C e. RR+ )
14 pntlem1.w 
 |-  W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )
15 pntlem1.z 
 |-  ( ph -> Z e. ( W [,) +oo ) )
16 pntlem1.m 
 |-  M = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 )
17 pntlem1.n 
 |-  N = ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) )
18 pntlem1.U 
 |-  ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )
19 pntlem1.K 
 |-  ( ph -> A. y e. ( X (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( L x. E ) ) x. z ) < ( K x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( L x. E ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) )
20 pntlem1.o 
 |-  O = ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ J ) ) ) )
21 pntlem1.v 
 |-  ( ph -> V e. RR+ )
22 pntlem1.V 
 |-  ( ph -> ( ( ( K ^ J ) < V /\ ( ( 1 + ( L x. E ) ) x. V ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( V [,] ( ( 1 + ( L x. E ) ) x. V ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) )
23 pntlem1.j 
 |-  ( ph -> J e. ( M ..^ N ) )
24 pntlem1.i 
 |-  I = ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) )
25 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 pntlemb 
 |-  ( ph -> ( Z e. RR+ /\ ( 1 < Z /\ _e <_ ( sqrt ` Z ) /\ ( sqrt ` Z ) <_ ( Z / Y ) ) /\ ( ( 4 / ( L x. E ) ) <_ ( sqrt ` Z ) /\ ( ( ( log ` X ) / ( log ` K ) ) + 2 ) <_ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) /\ ( ( U x. 3 ) + C ) <_ ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) )
26 25 simp1d 
 |-  ( ph -> Z e. RR+ )
27 1 2 3 4 5 6 7 8 9 10 pntlemc 
 |-  ( ph -> ( E e. RR+ /\ K e. RR+ /\ ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) ) )
28 27 simp2d 
 |-  ( ph -> K e. RR+ )
29 elfzoelz 
 |-  ( J e. ( M ..^ N ) -> J e. ZZ )
30 23 29 syl 
 |-  ( ph -> J e. ZZ )
31 30 peano2zd 
 |-  ( ph -> ( J + 1 ) e. ZZ )
32 28 31 rpexpcld 
 |-  ( ph -> ( K ^ ( J + 1 ) ) e. RR+ )
33 26 32 rpdivcld 
 |-  ( ph -> ( Z / ( K ^ ( J + 1 ) ) ) e. RR+ )
34 33 rpred 
 |-  ( ph -> ( Z / ( K ^ ( J + 1 ) ) ) e. RR )
35 34 flcld 
 |-  ( ph -> ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) e. ZZ )
36 1rp 
 |-  1 e. RR+
37 1 2 3 4 5 6 pntlemd 
 |-  ( ph -> ( L e. RR+ /\ D e. RR+ /\ F e. RR+ ) )
38 37 simp1d 
 |-  ( ph -> L e. RR+ )
39 27 simp1d 
 |-  ( ph -> E e. RR+ )
40 38 39 rpmulcld 
 |-  ( ph -> ( L x. E ) e. RR+ )
41 rpaddcl 
 |-  ( ( 1 e. RR+ /\ ( L x. E ) e. RR+ ) -> ( 1 + ( L x. E ) ) e. RR+ )
42 36 40 41 sylancr 
 |-  ( ph -> ( 1 + ( L x. E ) ) e. RR+ )
43 42 21 rpmulcld 
 |-  ( ph -> ( ( 1 + ( L x. E ) ) x. V ) e. RR+ )
44 26 43 rpdivcld 
 |-  ( ph -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR+ )
45 44 rpred 
 |-  ( ph -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR )
46 45 flcld 
 |-  ( ph -> ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) e. ZZ )
47 43 rpred 
 |-  ( ph -> ( ( 1 + ( L x. E ) ) x. V ) e. RR )
48 32 rpred 
 |-  ( ph -> ( K ^ ( J + 1 ) ) e. RR )
49 22 simpld 
 |-  ( ph -> ( ( K ^ J ) < V /\ ( ( 1 + ( L x. E ) ) x. V ) < ( K x. ( K ^ J ) ) ) )
50 49 simprd 
 |-  ( ph -> ( ( 1 + ( L x. E ) ) x. V ) < ( K x. ( K ^ J ) ) )
51 28 rpcnd 
 |-  ( ph -> K e. CC )
52 28 30 rpexpcld 
 |-  ( ph -> ( K ^ J ) e. RR+ )
53 52 rpcnd 
 |-  ( ph -> ( K ^ J ) e. CC )
54 51 53 mulcomd 
 |-  ( ph -> ( K x. ( K ^ J ) ) = ( ( K ^ J ) x. K ) )
55 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 pntlemg 
 |-  ( ph -> ( M e. NN /\ N e. ( ZZ>= ` M ) /\ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) <_ ( N - M ) ) )
56 55 simp1d 
 |-  ( ph -> M e. NN )
57 elfzouz 
 |-  ( J e. ( M ..^ N ) -> J e. ( ZZ>= ` M ) )
58 23 57 syl 
 |-  ( ph -> J e. ( ZZ>= ` M ) )
59 eluznn 
 |-  ( ( M e. NN /\ J e. ( ZZ>= ` M ) ) -> J e. NN )
60 56 58 59 syl2anc 
 |-  ( ph -> J e. NN )
61 60 nnnn0d 
 |-  ( ph -> J e. NN0 )
62 51 61 expp1d 
 |-  ( ph -> ( K ^ ( J + 1 ) ) = ( ( K ^ J ) x. K ) )
63 54 62 eqtr4d 
 |-  ( ph -> ( K x. ( K ^ J ) ) = ( K ^ ( J + 1 ) ) )
64 50 63 breqtrd 
 |-  ( ph -> ( ( 1 + ( L x. E ) ) x. V ) < ( K ^ ( J + 1 ) ) )
65 47 48 64 ltled 
 |-  ( ph -> ( ( 1 + ( L x. E ) ) x. V ) <_ ( K ^ ( J + 1 ) ) )
66 43 32 26 lediv2d 
 |-  ( ph -> ( ( ( 1 + ( L x. E ) ) x. V ) <_ ( K ^ ( J + 1 ) ) <-> ( Z / ( K ^ ( J + 1 ) ) ) <_ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) )
67 65 66 mpbid 
 |-  ( ph -> ( Z / ( K ^ ( J + 1 ) ) ) <_ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) )
68 flwordi 
 |-  ( ( ( Z / ( K ^ ( J + 1 ) ) ) e. RR /\ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR /\ ( Z / ( K ^ ( J + 1 ) ) ) <_ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) -> ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) <_ ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) )
69 34 45 67 68 syl3anc 
 |-  ( ph -> ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) <_ ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) )
70 eluz2 
 |-  ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) e. ( ZZ>= ` ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) ) <-> ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) e. ZZ /\ ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) e. ZZ /\ ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) <_ ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) )
71 35 46 69 70 syl3anbrc 
 |-  ( ph -> ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) e. ( ZZ>= ` ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) ) )
72 eluzp1p1 
 |-  ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) e. ( ZZ>= ` ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) ) -> ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) e. ( ZZ>= ` ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ) )
73 fzss1 
 |-  ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) e. ( ZZ>= ` ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ) -> ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) ) C_ ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) ) )
74 71 72 73 3syl 
 |-  ( ph -> ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) ) C_ ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) ) )
75 26 21 rpdivcld 
 |-  ( ph -> ( Z / V ) e. RR+ )
76 75 rpred 
 |-  ( ph -> ( Z / V ) e. RR )
77 76 flcld 
 |-  ( ph -> ( |_ ` ( Z / V ) ) e. ZZ )
78 26 52 rpdivcld 
 |-  ( ph -> ( Z / ( K ^ J ) ) e. RR+ )
79 78 rpred 
 |-  ( ph -> ( Z / ( K ^ J ) ) e. RR )
80 79 flcld 
 |-  ( ph -> ( |_ ` ( Z / ( K ^ J ) ) ) e. ZZ )
81 52 rpred 
 |-  ( ph -> ( K ^ J ) e. RR )
82 21 rpred 
 |-  ( ph -> V e. RR )
83 49 simpld 
 |-  ( ph -> ( K ^ J ) < V )
84 81 82 83 ltled 
 |-  ( ph -> ( K ^ J ) <_ V )
85 52 21 26 lediv2d 
 |-  ( ph -> ( ( K ^ J ) <_ V <-> ( Z / V ) <_ ( Z / ( K ^ J ) ) ) )
86 84 85 mpbid 
 |-  ( ph -> ( Z / V ) <_ ( Z / ( K ^ J ) ) )
87 flwordi 
 |-  ( ( ( Z / V ) e. RR /\ ( Z / ( K ^ J ) ) e. RR /\ ( Z / V ) <_ ( Z / ( K ^ J ) ) ) -> ( |_ ` ( Z / V ) ) <_ ( |_ ` ( Z / ( K ^ J ) ) ) )
88 76 79 86 87 syl3anc 
 |-  ( ph -> ( |_ ` ( Z / V ) ) <_ ( |_ ` ( Z / ( K ^ J ) ) ) )
89 eluz2 
 |-  ( ( |_ ` ( Z / ( K ^ J ) ) ) e. ( ZZ>= ` ( |_ ` ( Z / V ) ) ) <-> ( ( |_ ` ( Z / V ) ) e. ZZ /\ ( |_ ` ( Z / ( K ^ J ) ) ) e. ZZ /\ ( |_ ` ( Z / V ) ) <_ ( |_ ` ( Z / ( K ^ J ) ) ) ) )
90 77 80 88 89 syl3anbrc 
 |-  ( ph -> ( |_ ` ( Z / ( K ^ J ) ) ) e. ( ZZ>= ` ( |_ ` ( Z / V ) ) ) )
91 fzss2 
 |-  ( ( |_ ` ( Z / ( K ^ J ) ) ) e. ( ZZ>= ` ( |_ ` ( Z / V ) ) ) -> ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) ) C_ ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ J ) ) ) ) )
92 90 91 syl 
 |-  ( ph -> ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) ) C_ ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ J ) ) ) ) )
93 74 92 sstrd 
 |-  ( ph -> ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) ) C_ ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ J ) ) ) ) )
94 93 24 20 3sstr4g 
 |-  ( ph -> I C_ O )