Metamath Proof Explorer


Theorem pntlemj

Description: Lemma for pnt . The induction step. Using pntibnd , we find an interval in K ^ J ... K ^ ( J + 1 ) which is sufficiently large and has a much smaller value, R ( z ) / z <_ E (instead of our original bound R ( z ) / z <_ U ). (Contributed by Mario Carneiro, 13-Apr-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 pntlemj
|- ( ph -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) <_ sum_ n e. O ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )

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 pntlemc
 |-  ( ph -> ( E e. RR+ /\ K e. RR+ /\ ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) ) )
26 25 simp3d
 |-  ( ph -> ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) )
27 26 simp3d
 |-  ( ph -> ( U - E ) e. RR+ )
28 1 2 3 4 5 6 pntlemd
 |-  ( ph -> ( L e. RR+ /\ D e. RR+ /\ F e. RR+ ) )
29 28 simp1d
 |-  ( ph -> L e. RR+ )
30 25 simp1d
 |-  ( ph -> E e. RR+ )
31 29 30 rpmulcld
 |-  ( ph -> ( L x. E ) e. RR+ )
32 8nn
 |-  8 e. NN
33 nnrp
 |-  ( 8 e. NN -> 8 e. RR+ )
34 32 33 ax-mp
 |-  8 e. RR+
35 rpdivcl
 |-  ( ( ( L x. E ) e. RR+ /\ 8 e. RR+ ) -> ( ( L x. E ) / 8 ) e. RR+ )
36 31 34 35 sylancl
 |-  ( ph -> ( ( L x. E ) / 8 ) e. RR+ )
37 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 ) ) ) ) )
38 37 simp1d
 |-  ( ph -> Z e. RR+ )
39 38 rpred
 |-  ( ph -> Z e. RR )
40 37 simp2d
 |-  ( ph -> ( 1 < Z /\ _e <_ ( sqrt ` Z ) /\ ( sqrt ` Z ) <_ ( Z / Y ) ) )
41 40 simp1d
 |-  ( ph -> 1 < Z )
42 39 41 rplogcld
 |-  ( ph -> ( log ` Z ) e. RR+ )
43 36 42 rpmulcld
 |-  ( ph -> ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) e. RR+ )
44 27 43 rpmulcld
 |-  ( ph -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) e. RR+ )
45 44 rpred
 |-  ( ph -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) e. RR )
46 fzfid
 |-  ( ph -> ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) ) e. Fin )
47 24 46 eqeltrid
 |-  ( ph -> I e. Fin )
48 hashcl
 |-  ( I e. Fin -> ( # ` I ) e. NN0 )
49 47 48 syl
 |-  ( ph -> ( # ` I ) e. NN0 )
50 49 nn0red
 |-  ( ph -> ( # ` I ) e. RR )
51 27 rpred
 |-  ( ph -> ( U - E ) e. RR )
52 38 21 rpdivcld
 |-  ( ph -> ( Z / V ) e. RR+ )
53 52 relogcld
 |-  ( ph -> ( log ` ( Z / V ) ) e. RR )
54 53 52 rerpdivcld
 |-  ( ph -> ( ( log ` ( Z / V ) ) / ( Z / V ) ) e. RR )
55 51 54 remulcld
 |-  ( ph -> ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) e. RR )
56 50 55 remulcld
 |-  ( ph -> ( ( # ` I ) x. ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) e. RR )
57 fzfid
 |-  ( ph -> ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ J ) ) ) ) e. Fin )
58 20 57 eqeltrid
 |-  ( ph -> O e. Fin )
59 7 rpred
 |-  ( ph -> U e. RR )
60 59 adantr
 |-  ( ( ph /\ n e. O ) -> U e. RR )
61 25 simp2d
 |-  ( ph -> K e. RR+ )
62 elfzoelz
 |-  ( J e. ( M ..^ N ) -> J e. ZZ )
63 23 62 syl
 |-  ( ph -> J e. ZZ )
64 63 peano2zd
 |-  ( ph -> ( J + 1 ) e. ZZ )
65 61 64 rpexpcld
 |-  ( ph -> ( K ^ ( J + 1 ) ) e. RR+ )
66 38 65 rpdivcld
 |-  ( ph -> ( Z / ( K ^ ( J + 1 ) ) ) e. RR+ )
67 66 rprege0d
 |-  ( ph -> ( ( Z / ( K ^ ( J + 1 ) ) ) e. RR /\ 0 <_ ( Z / ( K ^ ( J + 1 ) ) ) ) )
68 flge0nn0
 |-  ( ( ( Z / ( K ^ ( J + 1 ) ) ) e. RR /\ 0 <_ ( Z / ( K ^ ( J + 1 ) ) ) ) -> ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) e. NN0 )
69 nn0p1nn
 |-  ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) e. NN0 -> ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) e. NN )
70 67 68 69 3syl
 |-  ( ph -> ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) e. NN )
71 elfzuz
 |-  ( n e. ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ J ) ) ) ) -> n e. ( ZZ>= ` ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ) )
72 71 20 eleq2s
 |-  ( n e. O -> n e. ( ZZ>= ` ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ) )
73 eluznn
 |-  ( ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) e. NN /\ n e. ( ZZ>= ` ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ) ) -> n e. NN )
74 70 72 73 syl2an
 |-  ( ( ph /\ n e. O ) -> n e. NN )
75 60 74 nndivred
 |-  ( ( ph /\ n e. O ) -> ( U / n ) e. RR )
76 38 adantr
 |-  ( ( ph /\ n e. O ) -> Z e. RR+ )
77 74 nnrpd
 |-  ( ( ph /\ n e. O ) -> n e. RR+ )
78 76 77 rpdivcld
 |-  ( ( ph /\ n e. O ) -> ( Z / n ) e. RR+ )
79 1 pntrf
 |-  R : RR+ --> RR
80 79 ffvelrni
 |-  ( ( Z / n ) e. RR+ -> ( R ` ( Z / n ) ) e. RR )
81 78 80 syl
 |-  ( ( ph /\ n e. O ) -> ( R ` ( Z / n ) ) e. RR )
82 81 76 rerpdivcld
 |-  ( ( ph /\ n e. O ) -> ( ( R ` ( Z / n ) ) / Z ) e. RR )
83 82 recnd
 |-  ( ( ph /\ n e. O ) -> ( ( R ` ( Z / n ) ) / Z ) e. CC )
84 83 abscld
 |-  ( ( ph /\ n e. O ) -> ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) e. RR )
85 75 84 resubcld
 |-  ( ( ph /\ n e. O ) -> ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) e. RR )
86 77 relogcld
 |-  ( ( ph /\ n e. O ) -> ( log ` n ) e. RR )
87 85 86 remulcld
 |-  ( ( ph /\ n e. O ) -> ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) e. RR )
88 58 87 fsumrecl
 |-  ( ph -> sum_ n e. O ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) e. RR )
89 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 pntlemr
 |-  ( ph -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) <_ ( ( # ` I ) x. ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) )
90 55 recnd
 |-  ( ph -> ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) e. CC )
91 fsumconst
 |-  ( ( I e. Fin /\ ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) e. CC ) -> sum_ n e. I ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) = ( ( # ` I ) x. ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) )
92 47 90 91 syl2anc
 |-  ( ph -> sum_ n e. I ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) = ( ( # ` I ) x. ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) )
93 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 pntlemq
 |-  ( ph -> I C_ O )
94 90 ralrimivw
 |-  ( ph -> A. n e. I ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) e. CC )
95 58 olcd
 |-  ( ph -> ( O C_ ( ZZ>= ` 1 ) \/ O e. Fin ) )
96 sumss2
 |-  ( ( ( I C_ O /\ A. n e. I ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) e. CC ) /\ ( O C_ ( ZZ>= ` 1 ) \/ O e. Fin ) ) -> sum_ n e. I ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) = sum_ n e. O if ( n e. I , ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) , 0 ) )
97 93 94 95 96 syl21anc
 |-  ( ph -> sum_ n e. I ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) = sum_ n e. O if ( n e. I , ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) , 0 ) )
98 92 97 eqtr3d
 |-  ( ph -> ( ( # ` I ) x. ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) = sum_ n e. O if ( n e. I , ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) , 0 ) )
99 55 adantr
 |-  ( ( ph /\ n e. I ) -> ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) e. RR )
100 99 adantlr
 |-  ( ( ( ph /\ n e. O ) /\ n e. I ) -> ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) e. RR )
101 0red
 |-  ( ( ( ph /\ n e. O ) /\ -. n e. I ) -> 0 e. RR )
102 100 101 ifclda
 |-  ( ( ph /\ n e. O ) -> if ( n e. I , ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) , 0 ) e. RR )
103 breq1
 |-  ( ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) = if ( n e. I , ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) , 0 ) -> ( ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) <-> if ( n e. I , ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) , 0 ) <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) )
104 breq1
 |-  ( 0 = if ( n e. I , ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) , 0 ) -> ( 0 <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) <-> if ( n e. I , ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) , 0 ) <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) )
105 27 rpregt0d
 |-  ( ph -> ( ( U - E ) e. RR /\ 0 < ( U - E ) ) )
106 105 adantr
 |-  ( ( ph /\ n e. I ) -> ( ( U - E ) e. RR /\ 0 < ( U - E ) ) )
107 106 simpld
 |-  ( ( ph /\ n e. I ) -> ( U - E ) e. RR )
108 1rp
 |-  1 e. RR+
109 rpaddcl
 |-  ( ( 1 e. RR+ /\ ( L x. E ) e. RR+ ) -> ( 1 + ( L x. E ) ) e. RR+ )
110 108 31 109 sylancr
 |-  ( ph -> ( 1 + ( L x. E ) ) e. RR+ )
111 110 21 rpmulcld
 |-  ( ph -> ( ( 1 + ( L x. E ) ) x. V ) e. RR+ )
112 38 111 rpdivcld
 |-  ( ph -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR+ )
113 112 rprege0d
 |-  ( ph -> ( ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR /\ 0 <_ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) )
114 flge0nn0
 |-  ( ( ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR /\ 0 <_ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) -> ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) e. NN0 )
115 nn0p1nn
 |-  ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) e. NN0 -> ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) e. NN )
116 113 114 115 3syl
 |-  ( ph -> ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) e. NN )
117 elfzuz
 |-  ( n e. ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) ) -> n e. ( ZZ>= ` ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ) )
118 117 24 eleq2s
 |-  ( n e. I -> n e. ( ZZ>= ` ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ) )
119 eluznn
 |-  ( ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) e. NN /\ n e. ( ZZ>= ` ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ) ) -> n e. NN )
120 116 118 119 syl2an
 |-  ( ( ph /\ n e. I ) -> n e. NN )
121 120 nnrpd
 |-  ( ( ph /\ n e. I ) -> n e. RR+ )
122 121 relogcld
 |-  ( ( ph /\ n e. I ) -> ( log ` n ) e. RR )
123 122 120 nndivred
 |-  ( ( ph /\ n e. I ) -> ( ( log ` n ) / n ) e. RR )
124 107 123 remulcld
 |-  ( ( ph /\ n e. I ) -> ( ( U - E ) x. ( ( log ` n ) / n ) ) e. RR )
125 93 sselda
 |-  ( ( ph /\ n e. I ) -> n e. O )
126 125 87 syldan
 |-  ( ( ph /\ n e. I ) -> ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) e. RR )
127 simpr
 |-  ( ( ph /\ n e. I ) -> n e. I )
128 127 24 eleqtrdi
 |-  ( ( ph /\ n e. I ) -> n e. ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) ) )
129 elfzle2
 |-  ( n e. ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) ) -> n <_ ( |_ ` ( Z / V ) ) )
130 128 129 syl
 |-  ( ( ph /\ n e. I ) -> n <_ ( |_ ` ( Z / V ) ) )
131 52 rpred
 |-  ( ph -> ( Z / V ) e. RR )
132 131 adantr
 |-  ( ( ph /\ n e. I ) -> ( Z / V ) e. RR )
133 128 elfzelzd
 |-  ( ( ph /\ n e. I ) -> n e. ZZ )
134 flge
 |-  ( ( ( Z / V ) e. RR /\ n e. ZZ ) -> ( n <_ ( Z / V ) <-> n <_ ( |_ ` ( Z / V ) ) ) )
135 132 133 134 syl2anc
 |-  ( ( ph /\ n e. I ) -> ( n <_ ( Z / V ) <-> n <_ ( |_ ` ( Z / V ) ) ) )
136 130 135 mpbird
 |-  ( ( ph /\ n e. I ) -> n <_ ( Z / V ) )
137 120 nnred
 |-  ( ( ph /\ n e. I ) -> n e. RR )
138 ere
 |-  _e e. RR
139 138 a1i
 |-  ( ( ph /\ n e. I ) -> _e e. RR )
140 112 rpred
 |-  ( ph -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR )
141 140 adantr
 |-  ( ( ph /\ n e. I ) -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR )
142 138 a1i
 |-  ( ph -> _e e. RR )
143 38 rpsqrtcld
 |-  ( ph -> ( sqrt ` Z ) e. RR+ )
144 143 rpred
 |-  ( ph -> ( sqrt ` Z ) e. RR )
145 40 simp2d
 |-  ( ph -> _e <_ ( sqrt ` Z ) )
146 111 rpred
 |-  ( ph -> ( ( 1 + ( L x. E ) ) x. V ) e. RR )
147 65 rpred
 |-  ( ph -> ( K ^ ( J + 1 ) ) e. RR )
148 22 simpld
 |-  ( ph -> ( ( K ^ J ) < V /\ ( ( 1 + ( L x. E ) ) x. V ) < ( K x. ( K ^ J ) ) ) )
149 148 simprd
 |-  ( ph -> ( ( 1 + ( L x. E ) ) x. V ) < ( K x. ( K ^ J ) ) )
150 61 rpcnd
 |-  ( ph -> K e. CC )
151 61 63 rpexpcld
 |-  ( ph -> ( K ^ J ) e. RR+ )
152 151 rpcnd
 |-  ( ph -> ( K ^ J ) e. CC )
153 150 152 mulcomd
 |-  ( ph -> ( K x. ( K ^ J ) ) = ( ( K ^ J ) x. K ) )
154 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 ) ) )
155 154 simp1d
 |-  ( ph -> M e. NN )
156 elfzouz
 |-  ( J e. ( M ..^ N ) -> J e. ( ZZ>= ` M ) )
157 23 156 syl
 |-  ( ph -> J e. ( ZZ>= ` M ) )
158 eluznn
 |-  ( ( M e. NN /\ J e. ( ZZ>= ` M ) ) -> J e. NN )
159 155 157 158 syl2anc
 |-  ( ph -> J e. NN )
160 159 nnnn0d
 |-  ( ph -> J e. NN0 )
161 150 160 expp1d
 |-  ( ph -> ( K ^ ( J + 1 ) ) = ( ( K ^ J ) x. K ) )
162 153 161 eqtr4d
 |-  ( ph -> ( K x. ( K ^ J ) ) = ( K ^ ( J + 1 ) ) )
163 149 162 breqtrd
 |-  ( ph -> ( ( 1 + ( L x. E ) ) x. V ) < ( K ^ ( J + 1 ) ) )
164 146 147 163 ltled
 |-  ( ph -> ( ( 1 + ( L x. E ) ) x. V ) <_ ( K ^ ( J + 1 ) ) )
165 fzofzp1
 |-  ( J e. ( M ..^ N ) -> ( J + 1 ) e. ( M ... N ) )
166 23 165 syl
 |-  ( ph -> ( J + 1 ) e. ( M ... N ) )
167 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 pntlemh
 |-  ( ( ph /\ ( J + 1 ) e. ( M ... N ) ) -> ( X < ( K ^ ( J + 1 ) ) /\ ( K ^ ( J + 1 ) ) <_ ( sqrt ` Z ) ) )
168 166 167 mpdan
 |-  ( ph -> ( X < ( K ^ ( J + 1 ) ) /\ ( K ^ ( J + 1 ) ) <_ ( sqrt ` Z ) ) )
169 168 simprd
 |-  ( ph -> ( K ^ ( J + 1 ) ) <_ ( sqrt ` Z ) )
170 146 147 144 164 169 letrd
 |-  ( ph -> ( ( 1 + ( L x. E ) ) x. V ) <_ ( sqrt ` Z ) )
171 146 144 143 lemul2d
 |-  ( ph -> ( ( ( 1 + ( L x. E ) ) x. V ) <_ ( sqrt ` Z ) <-> ( ( sqrt ` Z ) x. ( ( 1 + ( L x. E ) ) x. V ) ) <_ ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) ) )
172 170 171 mpbid
 |-  ( ph -> ( ( sqrt ` Z ) x. ( ( 1 + ( L x. E ) ) x. V ) ) <_ ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) )
173 38 rprege0d
 |-  ( ph -> ( Z e. RR /\ 0 <_ Z ) )
174 remsqsqrt
 |-  ( ( Z e. RR /\ 0 <_ Z ) -> ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) = Z )
175 173 174 syl
 |-  ( ph -> ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) = Z )
176 172 175 breqtrd
 |-  ( ph -> ( ( sqrt ` Z ) x. ( ( 1 + ( L x. E ) ) x. V ) ) <_ Z )
177 144 39 111 lemuldivd
 |-  ( ph -> ( ( ( sqrt ` Z ) x. ( ( 1 + ( L x. E ) ) x. V ) ) <_ Z <-> ( sqrt ` Z ) <_ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) )
178 176 177 mpbid
 |-  ( ph -> ( sqrt ` Z ) <_ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) )
179 142 144 140 145 178 letrd
 |-  ( ph -> _e <_ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) )
180 179 adantr
 |-  ( ( ph /\ n e. I ) -> _e <_ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) )
181 reflcl
 |-  ( ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR -> ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) e. RR )
182 peano2re
 |-  ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) e. RR -> ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) e. RR )
183 140 181 182 3syl
 |-  ( ph -> ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) e. RR )
184 183 adantr
 |-  ( ( ph /\ n e. I ) -> ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) e. RR )
185 fllep1
 |-  ( ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) <_ ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) )
186 141 185 syl
 |-  ( ( ph /\ n e. I ) -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) <_ ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) )
187 elfzle1
 |-  ( n e. ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) ) -> ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) <_ n )
188 128 187 syl
 |-  ( ( ph /\ n e. I ) -> ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) <_ n )
189 141 184 137 186 188 letrd
 |-  ( ( ph /\ n e. I ) -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) <_ n )
190 139 141 137 180 189 letrd
 |-  ( ( ph /\ n e. I ) -> _e <_ n )
191 139 137 132 190 136 letrd
 |-  ( ( ph /\ n e. I ) -> _e <_ ( Z / V ) )
192 logdivle
 |-  ( ( ( n e. RR /\ _e <_ n ) /\ ( ( Z / V ) e. RR /\ _e <_ ( Z / V ) ) ) -> ( n <_ ( Z / V ) <-> ( ( log ` ( Z / V ) ) / ( Z / V ) ) <_ ( ( log ` n ) / n ) ) )
193 137 190 132 191 192 syl22anc
 |-  ( ( ph /\ n e. I ) -> ( n <_ ( Z / V ) <-> ( ( log ` ( Z / V ) ) / ( Z / V ) ) <_ ( ( log ` n ) / n ) ) )
194 136 193 mpbid
 |-  ( ( ph /\ n e. I ) -> ( ( log ` ( Z / V ) ) / ( Z / V ) ) <_ ( ( log ` n ) / n ) )
195 54 adantr
 |-  ( ( ph /\ n e. I ) -> ( ( log ` ( Z / V ) ) / ( Z / V ) ) e. RR )
196 lemul2
 |-  ( ( ( ( log ` ( Z / V ) ) / ( Z / V ) ) e. RR /\ ( ( log ` n ) / n ) e. RR /\ ( ( U - E ) e. RR /\ 0 < ( U - E ) ) ) -> ( ( ( log ` ( Z / V ) ) / ( Z / V ) ) <_ ( ( log ` n ) / n ) <-> ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) <_ ( ( U - E ) x. ( ( log ` n ) / n ) ) ) )
197 195 123 106 196 syl3anc
 |-  ( ( ph /\ n e. I ) -> ( ( ( log ` ( Z / V ) ) / ( Z / V ) ) <_ ( ( log ` n ) / n ) <-> ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) <_ ( ( U - E ) x. ( ( log ` n ) / n ) ) ) )
198 194 197 mpbid
 |-  ( ( ph /\ n e. I ) -> ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) <_ ( ( U - E ) x. ( ( log ` n ) / n ) ) )
199 27 rpcnd
 |-  ( ph -> ( U - E ) e. CC )
200 199 adantr
 |-  ( ( ph /\ n e. I ) -> ( U - E ) e. CC )
201 122 recnd
 |-  ( ( ph /\ n e. I ) -> ( log ` n ) e. CC )
202 121 rpcnne0d
 |-  ( ( ph /\ n e. I ) -> ( n e. CC /\ n =/= 0 ) )
203 div23
 |-  ( ( ( U - E ) e. CC /\ ( log ` n ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( ( U - E ) x. ( log ` n ) ) / n ) = ( ( ( U - E ) / n ) x. ( log ` n ) ) )
204 200 201 202 203 syl3anc
 |-  ( ( ph /\ n e. I ) -> ( ( ( U - E ) x. ( log ` n ) ) / n ) = ( ( ( U - E ) / n ) x. ( log ` n ) ) )
205 divass
 |-  ( ( ( U - E ) e. CC /\ ( log ` n ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( ( U - E ) x. ( log ` n ) ) / n ) = ( ( U - E ) x. ( ( log ` n ) / n ) ) )
206 200 201 202 205 syl3anc
 |-  ( ( ph /\ n e. I ) -> ( ( ( U - E ) x. ( log ` n ) ) / n ) = ( ( U - E ) x. ( ( log ` n ) / n ) ) )
207 204 206 eqtr3d
 |-  ( ( ph /\ n e. I ) -> ( ( ( U - E ) / n ) x. ( log ` n ) ) = ( ( U - E ) x. ( ( log ` n ) / n ) ) )
208 51 adantr
 |-  ( ( ph /\ n e. I ) -> ( U - E ) e. RR )
209 208 120 nndivred
 |-  ( ( ph /\ n e. I ) -> ( ( U - E ) / n ) e. RR )
210 125 85 syldan
 |-  ( ( ph /\ n e. I ) -> ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) e. RR )
211 log1
 |-  ( log ` 1 ) = 0
212 120 nnge1d
 |-  ( ( ph /\ n e. I ) -> 1 <_ n )
213 logleb
 |-  ( ( 1 e. RR+ /\ n e. RR+ ) -> ( 1 <_ n <-> ( log ` 1 ) <_ ( log ` n ) ) )
214 108 121 213 sylancr
 |-  ( ( ph /\ n e. I ) -> ( 1 <_ n <-> ( log ` 1 ) <_ ( log ` n ) ) )
215 212 214 mpbid
 |-  ( ( ph /\ n e. I ) -> ( log ` 1 ) <_ ( log ` n ) )
216 211 215 eqbrtrrid
 |-  ( ( ph /\ n e. I ) -> 0 <_ ( log ` n ) )
217 7 rpcnd
 |-  ( ph -> U e. CC )
218 217 adantr
 |-  ( ( ph /\ n e. I ) -> U e. CC )
219 30 rpred
 |-  ( ph -> E e. RR )
220 219 adantr
 |-  ( ( ph /\ n e. I ) -> E e. RR )
221 220 recnd
 |-  ( ( ph /\ n e. I ) -> E e. CC )
222 divsubdir
 |-  ( ( U e. CC /\ E e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( U - E ) / n ) = ( ( U / n ) - ( E / n ) ) )
223 218 221 202 222 syl3anc
 |-  ( ( ph /\ n e. I ) -> ( ( U - E ) / n ) = ( ( U / n ) - ( E / n ) ) )
224 125 84 syldan
 |-  ( ( ph /\ n e. I ) -> ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) e. RR )
225 220 120 nndivred
 |-  ( ( ph /\ n e. I ) -> ( E / n ) e. RR )
226 125 75 syldan
 |-  ( ( ph /\ n e. I ) -> ( U / n ) e. RR )
227 125 81 syldan
 |-  ( ( ph /\ n e. I ) -> ( R ` ( Z / n ) ) e. RR )
228 227 recnd
 |-  ( ( ph /\ n e. I ) -> ( R ` ( Z / n ) ) e. CC )
229 38 adantr
 |-  ( ( ph /\ n e. I ) -> Z e. RR+ )
230 229 rpcnne0d
 |-  ( ( ph /\ n e. I ) -> ( Z e. CC /\ Z =/= 0 ) )
231 divdiv2
 |-  ( ( ( R ` ( Z / n ) ) e. CC /\ ( Z e. CC /\ Z =/= 0 ) /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( R ` ( Z / n ) ) / ( Z / n ) ) = ( ( ( R ` ( Z / n ) ) x. n ) / Z ) )
232 228 230 202 231 syl3anc
 |-  ( ( ph /\ n e. I ) -> ( ( R ` ( Z / n ) ) / ( Z / n ) ) = ( ( ( R ` ( Z / n ) ) x. n ) / Z ) )
233 121 rpcnd
 |-  ( ( ph /\ n e. I ) -> n e. CC )
234 div23
 |-  ( ( ( R ` ( Z / n ) ) e. CC /\ n e. CC /\ ( Z e. CC /\ Z =/= 0 ) ) -> ( ( ( R ` ( Z / n ) ) x. n ) / Z ) = ( ( ( R ` ( Z / n ) ) / Z ) x. n ) )
235 228 233 230 234 syl3anc
 |-  ( ( ph /\ n e. I ) -> ( ( ( R ` ( Z / n ) ) x. n ) / Z ) = ( ( ( R ` ( Z / n ) ) / Z ) x. n ) )
236 232 235 eqtrd
 |-  ( ( ph /\ n e. I ) -> ( ( R ` ( Z / n ) ) / ( Z / n ) ) = ( ( ( R ` ( Z / n ) ) / Z ) x. n ) )
237 236 fveq2d
 |-  ( ( ph /\ n e. I ) -> ( abs ` ( ( R ` ( Z / n ) ) / ( Z / n ) ) ) = ( abs ` ( ( ( R ` ( Z / n ) ) / Z ) x. n ) ) )
238 125 83 syldan
 |-  ( ( ph /\ n e. I ) -> ( ( R ` ( Z / n ) ) / Z ) e. CC )
239 238 233 absmuld
 |-  ( ( ph /\ n e. I ) -> ( abs ` ( ( ( R ` ( Z / n ) ) / Z ) x. n ) ) = ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( abs ` n ) ) )
240 121 rprege0d
 |-  ( ( ph /\ n e. I ) -> ( n e. RR /\ 0 <_ n ) )
241 absid
 |-  ( ( n e. RR /\ 0 <_ n ) -> ( abs ` n ) = n )
242 240 241 syl
 |-  ( ( ph /\ n e. I ) -> ( abs ` n ) = n )
243 242 oveq2d
 |-  ( ( ph /\ n e. I ) -> ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. ( abs ` n ) ) = ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. n ) )
244 237 239 243 3eqtrd
 |-  ( ( ph /\ n e. I ) -> ( abs ` ( ( R ` ( Z / n ) ) / ( Z / n ) ) ) = ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. n ) )
245 fveq2
 |-  ( u = ( Z / n ) -> ( R ` u ) = ( R ` ( Z / n ) ) )
246 id
 |-  ( u = ( Z / n ) -> u = ( Z / n ) )
247 245 246 oveq12d
 |-  ( u = ( Z / n ) -> ( ( R ` u ) / u ) = ( ( R ` ( Z / n ) ) / ( Z / n ) ) )
248 247 fveq2d
 |-  ( u = ( Z / n ) -> ( abs ` ( ( R ` u ) / u ) ) = ( abs ` ( ( R ` ( Z / n ) ) / ( Z / n ) ) ) )
249 248 breq1d
 |-  ( u = ( Z / n ) -> ( ( abs ` ( ( R ` u ) / u ) ) <_ E <-> ( abs ` ( ( R ` ( Z / n ) ) / ( Z / n ) ) ) <_ E ) )
250 22 simprd
 |-  ( ph -> A. u e. ( V [,] ( ( 1 + ( L x. E ) ) x. V ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E )
251 250 adantr
 |-  ( ( ph /\ n e. I ) -> A. u e. ( V [,] ( ( 1 + ( L x. E ) ) x. V ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E )
252 39 adantr
 |-  ( ( ph /\ n e. I ) -> Z e. RR )
253 252 120 nndivred
 |-  ( ( ph /\ n e. I ) -> ( Z / n ) e. RR )
254 21 rpregt0d
 |-  ( ph -> ( V e. RR /\ 0 < V ) )
255 254 adantr
 |-  ( ( ph /\ n e. I ) -> ( V e. RR /\ 0 < V ) )
256 lemuldiv2
 |-  ( ( n e. RR /\ Z e. RR /\ ( V e. RR /\ 0 < V ) ) -> ( ( V x. n ) <_ Z <-> n <_ ( Z / V ) ) )
257 137 252 255 256 syl3anc
 |-  ( ( ph /\ n e. I ) -> ( ( V x. n ) <_ Z <-> n <_ ( Z / V ) ) )
258 136 257 mpbird
 |-  ( ( ph /\ n e. I ) -> ( V x. n ) <_ Z )
259 255 simpld
 |-  ( ( ph /\ n e. I ) -> V e. RR )
260 259 252 121 lemuldivd
 |-  ( ( ph /\ n e. I ) -> ( ( V x. n ) <_ Z <-> V <_ ( Z / n ) ) )
261 258 260 mpbid
 |-  ( ( ph /\ n e. I ) -> V <_ ( Z / n ) )
262 111 rpregt0d
 |-  ( ph -> ( ( ( 1 + ( L x. E ) ) x. V ) e. RR /\ 0 < ( ( 1 + ( L x. E ) ) x. V ) ) )
263 262 adantr
 |-  ( ( ph /\ n e. I ) -> ( ( ( 1 + ( L x. E ) ) x. V ) e. RR /\ 0 < ( ( 1 + ( L x. E ) ) x. V ) ) )
264 121 rpregt0d
 |-  ( ( ph /\ n e. I ) -> ( n e. RR /\ 0 < n ) )
265 lediv23
 |-  ( ( Z e. RR /\ ( ( ( 1 + ( L x. E ) ) x. V ) e. RR /\ 0 < ( ( 1 + ( L x. E ) ) x. V ) ) /\ ( n e. RR /\ 0 < n ) ) -> ( ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) <_ n <-> ( Z / n ) <_ ( ( 1 + ( L x. E ) ) x. V ) ) )
266 252 263 264 265 syl3anc
 |-  ( ( ph /\ n e. I ) -> ( ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) <_ n <-> ( Z / n ) <_ ( ( 1 + ( L x. E ) ) x. V ) ) )
267 189 266 mpbid
 |-  ( ( ph /\ n e. I ) -> ( Z / n ) <_ ( ( 1 + ( L x. E ) ) x. V ) )
268 21 rpred
 |-  ( ph -> V e. RR )
269 268 adantr
 |-  ( ( ph /\ n e. I ) -> V e. RR )
270 146 adantr
 |-  ( ( ph /\ n e. I ) -> ( ( 1 + ( L x. E ) ) x. V ) e. RR )
271 elicc2
 |-  ( ( V e. RR /\ ( ( 1 + ( L x. E ) ) x. V ) e. RR ) -> ( ( Z / n ) e. ( V [,] ( ( 1 + ( L x. E ) ) x. V ) ) <-> ( ( Z / n ) e. RR /\ V <_ ( Z / n ) /\ ( Z / n ) <_ ( ( 1 + ( L x. E ) ) x. V ) ) ) )
272 269 270 271 syl2anc
 |-  ( ( ph /\ n e. I ) -> ( ( Z / n ) e. ( V [,] ( ( 1 + ( L x. E ) ) x. V ) ) <-> ( ( Z / n ) e. RR /\ V <_ ( Z / n ) /\ ( Z / n ) <_ ( ( 1 + ( L x. E ) ) x. V ) ) ) )
273 253 261 267 272 mpbir3and
 |-  ( ( ph /\ n e. I ) -> ( Z / n ) e. ( V [,] ( ( 1 + ( L x. E ) ) x. V ) ) )
274 249 251 273 rspcdva
 |-  ( ( ph /\ n e. I ) -> ( abs ` ( ( R ` ( Z / n ) ) / ( Z / n ) ) ) <_ E )
275 244 274 eqbrtrrd
 |-  ( ( ph /\ n e. I ) -> ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. n ) <_ E )
276 224 220 121 lemuldivd
 |-  ( ( ph /\ n e. I ) -> ( ( ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) x. n ) <_ E <-> ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) <_ ( E / n ) ) )
277 275 276 mpbid
 |-  ( ( ph /\ n e. I ) -> ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) <_ ( E / n ) )
278 224 225 226 277 lesub2dd
 |-  ( ( ph /\ n e. I ) -> ( ( U / n ) - ( E / n ) ) <_ ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) )
279 223 278 eqbrtrd
 |-  ( ( ph /\ n e. I ) -> ( ( U - E ) / n ) <_ ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) )
280 209 210 122 216 279 lemul1ad
 |-  ( ( ph /\ n e. I ) -> ( ( ( U - E ) / n ) x. ( log ` n ) ) <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
281 207 280 eqbrtrrd
 |-  ( ( ph /\ n e. I ) -> ( ( U - E ) x. ( ( log ` n ) / n ) ) <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
282 99 124 126 198 281 letrd
 |-  ( ( ph /\ n e. I ) -> ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
283 282 adantlr
 |-  ( ( ( ph /\ n e. O ) /\ n e. I ) -> ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
284 74 nnred
 |-  ( ( ph /\ n e. O ) -> n e. RR )
285 38 151 rpdivcld
 |-  ( ph -> ( Z / ( K ^ J ) ) e. RR+ )
286 285 rpred
 |-  ( ph -> ( Z / ( K ^ J ) ) e. RR )
287 286 adantr
 |-  ( ( ph /\ n e. O ) -> ( Z / ( K ^ J ) ) e. RR )
288 11 simpld
 |-  ( ph -> Y e. RR+ )
289 38 288 rpdivcld
 |-  ( ph -> ( Z / Y ) e. RR+ )
290 289 rpred
 |-  ( ph -> ( Z / Y ) e. RR )
291 290 adantr
 |-  ( ( ph /\ n e. O ) -> ( Z / Y ) e. RR )
292 simpr
 |-  ( ( ph /\ n e. O ) -> n e. O )
293 292 20 eleqtrdi
 |-  ( ( ph /\ n e. O ) -> n e. ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ J ) ) ) ) )
294 elfzle2
 |-  ( n e. ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ J ) ) ) ) -> n <_ ( |_ ` ( Z / ( K ^ J ) ) ) )
295 293 294 syl
 |-  ( ( ph /\ n e. O ) -> n <_ ( |_ ` ( Z / ( K ^ J ) ) ) )
296 74 nnzd
 |-  ( ( ph /\ n e. O ) -> n e. ZZ )
297 flge
 |-  ( ( ( Z / ( K ^ J ) ) e. RR /\ n e. ZZ ) -> ( n <_ ( Z / ( K ^ J ) ) <-> n <_ ( |_ ` ( Z / ( K ^ J ) ) ) ) )
298 287 296 297 syl2anc
 |-  ( ( ph /\ n e. O ) -> ( n <_ ( Z / ( K ^ J ) ) <-> n <_ ( |_ ` ( Z / ( K ^ J ) ) ) ) )
299 295 298 mpbird
 |-  ( ( ph /\ n e. O ) -> n <_ ( Z / ( K ^ J ) ) )
300 288 rpred
 |-  ( ph -> Y e. RR )
301 12 simpld
 |-  ( ph -> X e. RR+ )
302 301 rpred
 |-  ( ph -> X e. RR )
303 151 rpred
 |-  ( ph -> ( K ^ J ) e. RR )
304 12 simprd
 |-  ( ph -> Y < X )
305 300 302 304 ltled
 |-  ( ph -> Y <_ X )
306 elfzofz
 |-  ( J e. ( M ..^ N ) -> J e. ( M ... N ) )
307 23 306 syl
 |-  ( ph -> J e. ( M ... N ) )
308 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 pntlemh
 |-  ( ( ph /\ J e. ( M ... N ) ) -> ( X < ( K ^ J ) /\ ( K ^ J ) <_ ( sqrt ` Z ) ) )
309 307 308 mpdan
 |-  ( ph -> ( X < ( K ^ J ) /\ ( K ^ J ) <_ ( sqrt ` Z ) ) )
310 309 simpld
 |-  ( ph -> X < ( K ^ J ) )
311 302 303 310 ltled
 |-  ( ph -> X <_ ( K ^ J ) )
312 300 302 303 305 311 letrd
 |-  ( ph -> Y <_ ( K ^ J ) )
313 288 151 38 lediv2d
 |-  ( ph -> ( Y <_ ( K ^ J ) <-> ( Z / ( K ^ J ) ) <_ ( Z / Y ) ) )
314 312 313 mpbid
 |-  ( ph -> ( Z / ( K ^ J ) ) <_ ( Z / Y ) )
315 314 adantr
 |-  ( ( ph /\ n e. O ) -> ( Z / ( K ^ J ) ) <_ ( Z / Y ) )
316 284 287 291 299 315 letrd
 |-  ( ( ph /\ n e. O ) -> n <_ ( Z / Y ) )
317 74 316 jca
 |-  ( ( ph /\ n e. O ) -> ( n e. NN /\ n <_ ( Z / Y ) ) )
318 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 pntlemn
 |-  ( ( ph /\ ( n e. NN /\ n <_ ( Z / Y ) ) ) -> 0 <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
319 317 318 syldan
 |-  ( ( ph /\ n e. O ) -> 0 <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
320 319 adantr
 |-  ( ( ( ph /\ n e. O ) /\ -. n e. I ) -> 0 <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
321 103 104 283 320 ifbothda
 |-  ( ( ph /\ n e. O ) -> if ( n e. I , ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) , 0 ) <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
322 58 102 87 321 fsumle
 |-  ( ph -> sum_ n e. O if ( n e. I , ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) , 0 ) <_ sum_ n e. O ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
323 98 322 eqbrtrd
 |-  ( ph -> ( ( # ` I ) x. ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) <_ sum_ n e. O ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
324 45 56 88 89 323 letrd
 |-  ( ph -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) <_ sum_ n e. O ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )