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	ffvelcdmi	|- ( ( 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 ) ) )