Theorem pntlemf

Description: Lemma for pnt . Add up the pieces in pntlemi to get an estimate slightly better than the naive lower bound 0 . (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 ) )
Assertion	pntlemf	|- ( ph -> ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( ( 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	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+ ) ) )
21	20	simp3d	|- ( ph -> ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) )
22	21	simp3d	|- ( ph -> ( U - E ) e. RR+ )
23	1 2 3 4 5 6	pntlemd	|- ( ph -> ( L e. RR+ /\ D e. RR+ /\ F e. RR+ ) )
24	23	simp1d	|- ( ph -> L e. RR+ )
25	20	simp1d	|- ( ph -> E e. RR+ )
26		2z	|- 2 e. ZZ
27		rpexpcl	|- ( ( E e. RR+ /\ 2 e. ZZ ) -> ( E ^ 2 ) e. RR+ )
28	25 26 27	sylancl	|- ( ph -> ( E ^ 2 ) e. RR+ )
29	24 28	rpmulcld	|- ( ph -> ( L x. ( E ^ 2 ) ) e. RR+ )
30		3nn0	|- 3 e. NN0
31		2nn	|- 2 e. NN
32	30 31	decnncl	|- ; 3 2 e. NN
33		nnrp	|- ( ; 3 2 e. NN -> ; 3 2 e. RR+ )
34	32 33	ax-mp	|- ; 3 2 e. RR+
35		rpmulcl	|- ( ( ; 3 2 e. RR+ /\ B e. RR+ ) -> ( ; 3 2 x. B ) e. RR+ )
36	34 3 35	sylancr	|- ( ph -> ( ; 3 2 x. B ) e. RR+ )
37	29 36	rpdivcld	|- ( ph -> ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) e. RR+ )
38	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 ) ) ) ) )
39	38	simp1d	|- ( ph -> Z e. RR+ )
40	39	rpred	|- ( ph -> Z e. RR )
41	38	simp2d	|- ( ph -> ( 1 < Z /\ _e <_ ( sqrt ` Z ) /\ ( sqrt ` Z ) <_ ( Z / Y ) ) )
42	41	simp1d	|- ( ph -> 1 < Z )
43	40 42	rplogcld	|- ( ph -> ( log ` Z ) e. RR+ )
44		rpexpcl	|- ( ( ( log ` Z ) e. RR+ /\ 2 e. ZZ ) -> ( ( log ` Z ) ^ 2 ) e. RR+ )
45	43 26 44	sylancl	|- ( ph -> ( ( log ` Z ) ^ 2 ) e. RR+ )
46	37 45	rpmulcld	|- ( ph -> ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) e. RR+ )
47	22 46	rpmulcld	|- ( ph -> ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) e. RR+ )
48	47	rpred	|- ( ph -> ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) e. RR )
49	24 25	rpmulcld	|- ( ph -> ( L x. E ) e. RR+ )
50		8re	|- 8 e. RR
51		8pos	|- 0 < 8
52	50 51	elrpii	|- 8 e. RR+
53		rpdivcl	|- ( ( ( L x. E ) e. RR+ /\ 8 e. RR+ ) -> ( ( L x. E ) / 8 ) e. RR+ )
54	49 52 53	sylancl	|- ( ph -> ( ( L x. E ) / 8 ) e. RR+ )
55	54 43	rpmulcld	|- ( ph -> ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) e. RR+ )
56	22 55	rpmulcld	|- ( ph -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) e. RR+ )
57	56	rpred	|- ( ph -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) e. RR )
58	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 ) ) )
59	58	simp1d	|- ( ph -> M e. NN )
60	58	simp2d	|- ( ph -> N e. ( ZZ>= ` M ) )
61		eluznn	|- ( ( M e. NN /\ N e. ( ZZ>= ` M ) ) -> N e. NN )
62	59 60 61	syl2anc	|- ( ph -> N e. NN )
63	62	nnred	|- ( ph -> N e. RR )
64	59	nnred	|- ( ph -> M e. RR )
65	63 64	resubcld	|- ( ph -> ( N - M ) e. RR )
66	57 65	remulcld	|- ( ph -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( N - M ) ) e. RR )
67		fzfid	|- ( ph -> ( 1 ... ( |_ ` ( Z / Y ) ) ) e. Fin )
68	7	rpred	|- ( ph -> U e. RR )
69		elfznn	|- ( n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) -> n e. NN )
70		nndivre	|- ( ( U e. RR /\ n e. NN ) -> ( U / n ) e. RR )
71	68 69 70	syl2an	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( U / n ) e. RR )
72	39	adantr	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> Z e. RR+ )
73	69	adantl	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> n e. NN )
74	73	nnrpd	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> n e. RR+ )
75	72 74	rpdivcld	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( Z / n ) e. RR+ )
76	1	pntrf	|- R : RR+ --> RR
77	76	ffvelrni	|- ( ( Z / n ) e. RR+ -> ( R ` ( Z / n ) ) e. RR )
78	75 77	syl	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( R ` ( Z / n ) ) e. RR )
79	78 72	rerpdivcld	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( R ` ( Z / n ) ) / Z ) e. RR )
80	79	recnd	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( R ` ( Z / n ) ) / Z ) e. CC )
81	80	abscld	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) e. RR )
82	71 81	resubcld	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) e. RR )
83	74	relogcld	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( log ` n ) e. RR )
84	82 83	remulcld	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) e. RR )
85	67 84	fsumrecl	|- ( ph -> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) e. RR )
86	49	rpcnd	|- ( ph -> ( L x. E ) e. CC )
87	20	simp2d	|- ( ph -> K e. RR+ )
88	87	rpred	|- ( ph -> K e. RR )
89	21	simp2d	|- ( ph -> 1 < K )
90	88 89	rplogcld	|- ( ph -> ( log ` K ) e. RR+ )
91	43 90	rpdivcld	|- ( ph -> ( ( log ` Z ) / ( log ` K ) ) e. RR+ )
92	91	rpcnd	|- ( ph -> ( ( log ` Z ) / ( log ` K ) ) e. CC )
93		rpcnne0	|- ( 8 e. RR+ -> ( 8 e. CC /\ 8 =/= 0 ) )
94	52 93	mp1i	|- ( ph -> ( 8 e. CC /\ 8 =/= 0 ) )
95		4re	|- 4 e. RR
96		4pos	|- 0 < 4
97	95 96	elrpii	|- 4 e. RR+
98		rpcnne0	|- ( 4 e. RR+ -> ( 4 e. CC /\ 4 =/= 0 ) )
99	97 98	mp1i	|- ( ph -> ( 4 e. CC /\ 4 =/= 0 ) )
100		divmuldiv	|- ( ( ( ( L x. E ) e. CC /\ ( ( log ` Z ) / ( log ` K ) ) e. CC ) /\ ( ( 8 e. CC /\ 8 =/= 0 ) /\ ( 4 e. CC /\ 4 =/= 0 ) ) ) -> ( ( ( L x. E ) / 8 ) x. ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) ) = ( ( ( L x. E ) x. ( ( log ` Z ) / ( log ` K ) ) ) / ( 8 x. 4 ) ) )
101	86 92 94 99 100	syl22anc	|- ( ph -> ( ( ( L x. E ) / 8 ) x. ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) ) = ( ( ( L x. E ) x. ( ( log ` Z ) / ( log ` K ) ) ) / ( 8 x. 4 ) ) )
102	10	fveq2i	|- ( log ` K ) = ( log ` ( exp ` ( B / E ) ) )
103	3 25	rpdivcld	|- ( ph -> ( B / E ) e. RR+ )
104	103	rpred	|- ( ph -> ( B / E ) e. RR )
105	104	relogefd	|- ( ph -> ( log ` ( exp ` ( B / E ) ) ) = ( B / E ) )
106	102 105	syl5eq	|- ( ph -> ( log ` K ) = ( B / E ) )
107	106	oveq2d	|- ( ph -> ( ( log ` Z ) / ( log ` K ) ) = ( ( log ` Z ) / ( B / E ) ) )
108	43	rpcnd	|- ( ph -> ( log ` Z ) e. CC )
109	3	rpcnne0d	|- ( ph -> ( B e. CC /\ B =/= 0 ) )
110	25	rpcnne0d	|- ( ph -> ( E e. CC /\ E =/= 0 ) )
111		divdiv2	|- ( ( ( log ` Z ) e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( E e. CC /\ E =/= 0 ) ) -> ( ( log ` Z ) / ( B / E ) ) = ( ( ( log ` Z ) x. E ) / B ) )
112	108 109 110 111	syl3anc	|- ( ph -> ( ( log ` Z ) / ( B / E ) ) = ( ( ( log ` Z ) x. E ) / B ) )
113	107 112	eqtrd	|- ( ph -> ( ( log ` Z ) / ( log ` K ) ) = ( ( ( log ` Z ) x. E ) / B ) )
114	113	oveq2d	|- ( ph -> ( ( L x. E ) x. ( ( log ` Z ) / ( log ` K ) ) ) = ( ( L x. E ) x. ( ( ( log ` Z ) x. E ) / B ) ) )
115	25	rpcnd	|- ( ph -> E e. CC )
116	108 115	mulcld	|- ( ph -> ( ( log ` Z ) x. E ) e. CC )
117		divass	|- ( ( ( L x. E ) e. CC /\ ( ( log ` Z ) x. E ) e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( ( L x. E ) x. ( ( log ` Z ) x. E ) ) / B ) = ( ( L x. E ) x. ( ( ( log ` Z ) x. E ) / B ) ) )
118	86 116 109 117	syl3anc	|- ( ph -> ( ( ( L x. E ) x. ( ( log ` Z ) x. E ) ) / B ) = ( ( L x. E ) x. ( ( ( log ` Z ) x. E ) / B ) ) )
119	24	rpcnd	|- ( ph -> L e. CC )
120	119 115 108 115	mul4d	|- ( ph -> ( ( L x. E ) x. ( ( log ` Z ) x. E ) ) = ( ( L x. ( log ` Z ) ) x. ( E x. E ) ) )
121	115	sqvald	|- ( ph -> ( E ^ 2 ) = ( E x. E ) )
122	121	oveq2d	|- ( ph -> ( ( L x. ( log ` Z ) ) x. ( E ^ 2 ) ) = ( ( L x. ( log ` Z ) ) x. ( E x. E ) ) )
123	115	sqcld	|- ( ph -> ( E ^ 2 ) e. CC )
124	119 108 123	mul32d	|- ( ph -> ( ( L x. ( log ` Z ) ) x. ( E ^ 2 ) ) = ( ( L x. ( E ^ 2 ) ) x. ( log ` Z ) ) )
125	120 122 124	3eqtr2d	|- ( ph -> ( ( L x. E ) x. ( ( log ` Z ) x. E ) ) = ( ( L x. ( E ^ 2 ) ) x. ( log ` Z ) ) )
126	125	oveq1d	|- ( ph -> ( ( ( L x. E ) x. ( ( log ` Z ) x. E ) ) / B ) = ( ( ( L x. ( E ^ 2 ) ) x. ( log ` Z ) ) / B ) )
127	114 118 126	3eqtr2d	|- ( ph -> ( ( L x. E ) x. ( ( log ` Z ) / ( log ` K ) ) ) = ( ( ( L x. ( E ^ 2 ) ) x. ( log ` Z ) ) / B ) )
128		8t4e32	|- ( 8 x. 4 ) = ; 3 2
129	128	a1i	|- ( ph -> ( 8 x. 4 ) = ; 3 2 )
130	127 129	oveq12d	|- ( ph -> ( ( ( L x. E ) x. ( ( log ` Z ) / ( log ` K ) ) ) / ( 8 x. 4 ) ) = ( ( ( ( L x. ( E ^ 2 ) ) x. ( log ` Z ) ) / B ) / ; 3 2 ) )
131	29	rpcnd	|- ( ph -> ( L x. ( E ^ 2 ) ) e. CC )
132	131 108	mulcld	|- ( ph -> ( ( L x. ( E ^ 2 ) ) x. ( log ` Z ) ) e. CC )
133		rpcnne0	|- ( ; 3 2 e. RR+ -> ( ; 3 2 e. CC /\ ; 3 2 =/= 0 ) )
134	34 133	mp1i	|- ( ph -> ( ; 3 2 e. CC /\ ; 3 2 =/= 0 ) )
135		divdiv1	|- ( ( ( ( L x. ( E ^ 2 ) ) x. ( log ` Z ) ) e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( ; 3 2 e. CC /\ ; 3 2 =/= 0 ) ) -> ( ( ( ( L x. ( E ^ 2 ) ) x. ( log ` Z ) ) / B ) / ; 3 2 ) = ( ( ( L x. ( E ^ 2 ) ) x. ( log ` Z ) ) / ( B x. ; 3 2 ) ) )
136	132 109 134 135	syl3anc	|- ( ph -> ( ( ( ( L x. ( E ^ 2 ) ) x. ( log ` Z ) ) / B ) / ; 3 2 ) = ( ( ( L x. ( E ^ 2 ) ) x. ( log ` Z ) ) / ( B x. ; 3 2 ) ) )
137	32	nncni	|- ; 3 2 e. CC
138	3	rpcnd	|- ( ph -> B e. CC )
139		mulcom	|- ( ( ; 3 2 e. CC /\ B e. CC ) -> ( ; 3 2 x. B ) = ( B x. ; 3 2 ) )
140	137 138 139	sylancr	|- ( ph -> ( ; 3 2 x. B ) = ( B x. ; 3 2 ) )
141	140	oveq2d	|- ( ph -> ( ( ( L x. ( E ^ 2 ) ) x. ( log ` Z ) ) / ( ; 3 2 x. B ) ) = ( ( ( L x. ( E ^ 2 ) ) x. ( log ` Z ) ) / ( B x. ; 3 2 ) ) )
142	36	rpcnne0d	|- ( ph -> ( ( ; 3 2 x. B ) e. CC /\ ( ; 3 2 x. B ) =/= 0 ) )
143		div23	|- ( ( ( L x. ( E ^ 2 ) ) e. CC /\ ( log ` Z ) e. CC /\ ( ( ; 3 2 x. B ) e. CC /\ ( ; 3 2 x. B ) =/= 0 ) ) -> ( ( ( L x. ( E ^ 2 ) ) x. ( log ` Z ) ) / ( ; 3 2 x. B ) ) = ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( log ` Z ) ) )
144	131 108 142 143	syl3anc	|- ( ph -> ( ( ( L x. ( E ^ 2 ) ) x. ( log ` Z ) ) / ( ; 3 2 x. B ) ) = ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( log ` Z ) ) )
145	136 141 144	3eqtr2d	|- ( ph -> ( ( ( ( L x. ( E ^ 2 ) ) x. ( log ` Z ) ) / B ) / ; 3 2 ) = ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( log ` Z ) ) )
146	101 130 145	3eqtrd	|- ( ph -> ( ( ( L x. E ) / 8 ) x. ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) ) = ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( log ` Z ) ) )
147	146	oveq1d	|- ( ph -> ( ( ( ( L x. E ) / 8 ) x. ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) ) x. ( log ` Z ) ) = ( ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( log ` Z ) ) x. ( log ` Z ) ) )
148	54	rpcnd	|- ( ph -> ( ( L x. E ) / 8 ) e. CC )
149	91	rpred	|- ( ph -> ( ( log ` Z ) / ( log ` K ) ) e. RR )
150		4nn	|- 4 e. NN
151		nndivre	|- ( ( ( ( log ` Z ) / ( log ` K ) ) e. RR /\ 4 e. NN ) -> ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) e. RR )
152	149 150 151	sylancl	|- ( ph -> ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) e. RR )
153	152	recnd	|- ( ph -> ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) e. CC )
154	148 108 153	mul32d	|- ( ph -> ( ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) x. ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) ) = ( ( ( ( L x. E ) / 8 ) x. ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) ) x. ( log ` Z ) ) )
155	108	sqvald	|- ( ph -> ( ( log ` Z ) ^ 2 ) = ( ( log ` Z ) x. ( log ` Z ) ) )
156	155	oveq2d	|- ( ph -> ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) = ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) x. ( log ` Z ) ) ) )
157	37	rpcnd	|- ( ph -> ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) e. CC )
158	157 108 108	mulassd	|- ( ph -> ( ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( log ` Z ) ) x. ( log ` Z ) ) = ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) x. ( log ` Z ) ) ) )
159	156 158	eqtr4d	|- ( ph -> ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) = ( ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( log ` Z ) ) x. ( log ` Z ) ) )
160	147 154 159	3eqtr4d	|- ( ph -> ( ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) x. ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) ) = ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) )
161	58	simp3d	|- ( ph -> ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) <_ ( N - M ) )
162	152 65 55	lemul2d	|- ( ph -> ( ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) <_ ( N - M ) <-> ( ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) x. ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) ) <_ ( ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) x. ( N - M ) ) ) )
163	161 162	mpbid	|- ( ph -> ( ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) x. ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) ) <_ ( ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) x. ( N - M ) ) )
164	160 163	eqbrtrrd	|- ( ph -> ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) <_ ( ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) x. ( N - M ) ) )
165	46	rpred	|- ( ph -> ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) e. RR )
166	55	rpred	|- ( ph -> ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) e. RR )
167	166 65	remulcld	|- ( ph -> ( ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) x. ( N - M ) ) e. RR )
168	165 167 22	lemul2d	|- ( ph -> ( ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) <_ ( ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) x. ( N - M ) ) <-> ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) <_ ( ( U - E ) x. ( ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) x. ( N - M ) ) ) ) )
169	164 168	mpbid	|- ( ph -> ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) <_ ( ( U - E ) x. ( ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) x. ( N - M ) ) ) )
170	22	rpcnd	|- ( ph -> ( U - E ) e. CC )
171	55	rpcnd	|- ( ph -> ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) e. CC )
172	65	recnd	|- ( ph -> ( N - M ) e. CC )
173	170 171 172	mulassd	|- ( ph -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( N - M ) ) = ( ( U - E ) x. ( ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) x. ( N - M ) ) ) )
174	169 173	breqtrrd	|- ( ph -> ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) <_ ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( N - M ) ) )
175		fzfid	|- ( ph -> ( ( ( |_ ` ( Z / ( K ^ N ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) e. Fin )
176	62	nnzd	|- ( ph -> N e. ZZ )
177	87 176	rpexpcld	|- ( ph -> ( K ^ N ) e. RR+ )
178	39 177	rpdivcld	|- ( ph -> ( Z / ( K ^ N ) ) e. RR+ )
179	178	rprege0d	|- ( ph -> ( ( Z / ( K ^ N ) ) e. RR /\ 0 <_ ( Z / ( K ^ N ) ) ) )
180		flge0nn0	|- ( ( ( Z / ( K ^ N ) ) e. RR /\ 0 <_ ( Z / ( K ^ N ) ) ) -> ( |_ ` ( Z / ( K ^ N ) ) ) e. NN0 )
181		nn0p1nn	|- ( ( |_ ` ( Z / ( K ^ N ) ) ) e. NN0 -> ( ( |_ ` ( Z / ( K ^ N ) ) ) + 1 ) e. NN )
182	179 180 181	3syl	|- ( ph -> ( ( |_ ` ( Z / ( K ^ N ) ) ) + 1 ) e. NN )
183		nnuz	|- NN = ( ZZ>= ` 1 )
184	182 183	eleqtrdi	|- ( ph -> ( ( |_ ` ( Z / ( K ^ N ) ) ) + 1 ) e. ( ZZ>= ` 1 ) )
185		fzss1	|- ( ( ( |_ ` ( Z / ( K ^ N ) ) ) + 1 ) e. ( ZZ>= ` 1 ) -> ( ( ( |_ ` ( Z / ( K ^ N ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) C_ ( 1 ... ( |_ ` ( Z / Y ) ) ) )
186	184 185	syl	|- ( ph -> ( ( ( |_ ` ( Z / ( K ^ N ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) C_ ( 1 ... ( |_ ` ( Z / Y ) ) ) )
187	186	sselda	|- ( ( ph /\ n e. ( ( ( |_ ` ( Z / ( K ^ N ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ) -> n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) )
188	187 84	syldan	|- ( ( ph /\ n e. ( ( ( |_ ` ( Z / ( K ^ N ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) e. RR )
189	175 188	fsumrecl	|- ( ph -> sum_ n e. ( ( ( |_ ` ( Z / ( K ^ N ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) e. RR )
190		eluzfz2	|- ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )
191	60 190	syl	|- ( ph -> N e. ( M ... N ) )
192		oveq1	|- ( m = M -> ( m - M ) = ( M - M ) )
193	192	oveq2d	|- ( m = M -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( m - M ) ) = ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( M - M ) ) )
194		oveq2	|- ( m = M -> ( K ^ m ) = ( K ^ M ) )
195	194	oveq2d	|- ( m = M -> ( Z / ( K ^ m ) ) = ( Z / ( K ^ M ) ) )
196	195	fveq2d	|- ( m = M -> ( |_ ` ( Z / ( K ^ m ) ) ) = ( |_ ` ( Z / ( K ^ M ) ) ) )
197	196	oveq1d	|- ( m = M -> ( ( |_ ` ( Z / ( K ^ m ) ) ) + 1 ) = ( ( |_ ` ( Z / ( K ^ M ) ) ) + 1 ) )
198	197	oveq1d	|- ( m = M -> ( ( ( |_ ` ( Z / ( K ^ m ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) = ( ( ( |_ ` ( Z / ( K ^ M ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) )
199	198	sumeq1d	|- ( m = M -> sum_ n e. ( ( ( |_ ` ( Z / ( K ^ m ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) = sum_ n e. ( ( ( |_ ` ( Z / ( K ^ M ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
200	193 199	breq12d	|- ( m = M -> ( ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( m - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ m ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) <-> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( M - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ M ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) )
201	200	imbi2d	|- ( m = M -> ( ( ph -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( m - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ m ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) <-> ( ph -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( M - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ M ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) ) )
202		oveq1	|- ( m = j -> ( m - M ) = ( j - M ) )
203	202	oveq2d	|- ( m = j -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( m - M ) ) = ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( j - M ) ) )
204		oveq2	|- ( m = j -> ( K ^ m ) = ( K ^ j ) )
205	204	oveq2d	|- ( m = j -> ( Z / ( K ^ m ) ) = ( Z / ( K ^ j ) ) )
206	205	fveq2d	|- ( m = j -> ( |_ ` ( Z / ( K ^ m ) ) ) = ( |_ ` ( Z / ( K ^ j ) ) ) )
207	206	oveq1d	|- ( m = j -> ( ( |_ ` ( Z / ( K ^ m ) ) ) + 1 ) = ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) )
208	207	oveq1d	|- ( m = j -> ( ( ( |_ ` ( Z / ( K ^ m ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) = ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) )
209	208	sumeq1d	|- ( m = j -> sum_ n e. ( ( ( |_ ` ( Z / ( K ^ m ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) = sum_ n e. ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
210	203 209	breq12d	|- ( m = j -> ( ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( m - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ m ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) <-> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( j - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) )
211	210	imbi2d	|- ( m = j -> ( ( ph -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( m - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ m ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) <-> ( ph -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( j - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) ) )
212		oveq1	|- ( m = ( j + 1 ) -> ( m - M ) = ( ( j + 1 ) - M ) )
213	212	oveq2d	|- ( m = ( j + 1 ) -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( m - M ) ) = ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( ( j + 1 ) - M ) ) )
214		oveq2	|- ( m = ( j + 1 ) -> ( K ^ m ) = ( K ^ ( j + 1 ) ) )
215	214	oveq2d	|- ( m = ( j + 1 ) -> ( Z / ( K ^ m ) ) = ( Z / ( K ^ ( j + 1 ) ) ) )
216	215	fveq2d	|- ( m = ( j + 1 ) -> ( |_ ` ( Z / ( K ^ m ) ) ) = ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) )
217	216	oveq1d	|- ( m = ( j + 1 ) -> ( ( |_ ` ( Z / ( K ^ m ) ) ) + 1 ) = ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) )
218	217	oveq1d	|- ( m = ( j + 1 ) -> ( ( ( |_ ` ( Z / ( K ^ m ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) = ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) )
219	218	sumeq1d	|- ( m = ( j + 1 ) -> sum_ n e. ( ( ( |_ ` ( Z / ( K ^ m ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) = sum_ n e. ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
220	213 219	breq12d	|- ( m = ( j + 1 ) -> ( ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( m - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ m ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) <-> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( ( j + 1 ) - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) )
221	220	imbi2d	|- ( m = ( j + 1 ) -> ( ( ph -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( m - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ m ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) <-> ( ph -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( ( j + 1 ) - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) ) )
222		oveq1	|- ( m = N -> ( m - M ) = ( N - M ) )
223	222	oveq2d	|- ( m = N -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( m - M ) ) = ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( N - M ) ) )
224		oveq2	|- ( m = N -> ( K ^ m ) = ( K ^ N ) )
225	224	oveq2d	|- ( m = N -> ( Z / ( K ^ m ) ) = ( Z / ( K ^ N ) ) )
226	225	fveq2d	|- ( m = N -> ( |_ ` ( Z / ( K ^ m ) ) ) = ( |_ ` ( Z / ( K ^ N ) ) ) )
227	226	oveq1d	|- ( m = N -> ( ( |_ ` ( Z / ( K ^ m ) ) ) + 1 ) = ( ( |_ ` ( Z / ( K ^ N ) ) ) + 1 ) )
228	227	oveq1d	|- ( m = N -> ( ( ( |_ ` ( Z / ( K ^ m ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) = ( ( ( |_ ` ( Z / ( K ^ N ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) )
229	228	sumeq1d	|- ( m = N -> sum_ n e. ( ( ( |_ ` ( Z / ( K ^ m ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) = sum_ n e. ( ( ( |_ ` ( Z / ( K ^ N ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
230	223 229	breq12d	|- ( m = N -> ( ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( m - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ m ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) <-> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( N - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ N ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) )
231	230	imbi2d	|- ( m = N -> ( ( ph -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( m - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ m ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) <-> ( ph -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( N - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ N ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) ) )
232	59	nncnd	|- ( ph -> M e. CC )
233	232	subidd	|- ( ph -> ( M - M ) = 0 )
234	233	oveq2d	|- ( ph -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( M - M ) ) = ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. 0 ) )
235	56	rpcnd	|- ( ph -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) e. CC )
236	235	mul01d	|- ( ph -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. 0 ) = 0 )
237	234 236	eqtrd	|- ( ph -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( M - M ) ) = 0 )
238		fzfid	|- ( ph -> ( ( ( |_ ` ( Z / ( K ^ M ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) e. Fin )
239	59	nnzd	|- ( ph -> M e. ZZ )
240	87 239	rpexpcld	|- ( ph -> ( K ^ M ) e. RR+ )
241	39 240	rpdivcld	|- ( ph -> ( Z / ( K ^ M ) ) e. RR+ )
242	241	rprege0d	|- ( ph -> ( ( Z / ( K ^ M ) ) e. RR /\ 0 <_ ( Z / ( K ^ M ) ) ) )
243		flge0nn0	|- ( ( ( Z / ( K ^ M ) ) e. RR /\ 0 <_ ( Z / ( K ^ M ) ) ) -> ( |_ ` ( Z / ( K ^ M ) ) ) e. NN0 )
244		nn0p1nn	|- ( ( |_ ` ( Z / ( K ^ M ) ) ) e. NN0 -> ( ( |_ ` ( Z / ( K ^ M ) ) ) + 1 ) e. NN )
245	242 243 244	3syl	|- ( ph -> ( ( |_ ` ( Z / ( K ^ M ) ) ) + 1 ) e. NN )
246	245 183	eleqtrdi	|- ( ph -> ( ( |_ ` ( Z / ( K ^ M ) ) ) + 1 ) e. ( ZZ>= ` 1 ) )
247		fzss1	|- ( ( ( |_ ` ( Z / ( K ^ M ) ) ) + 1 ) e. ( ZZ>= ` 1 ) -> ( ( ( |_ ` ( Z / ( K ^ M ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) C_ ( 1 ... ( |_ ` ( Z / Y ) ) ) )
248	246 247	syl	|- ( ph -> ( ( ( |_ ` ( Z / ( K ^ M ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) C_ ( 1 ... ( |_ ` ( Z / Y ) ) ) )
249	248	sselda	|- ( ( ph /\ n e. ( ( ( |_ ` ( Z / ( K ^ M ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ) -> n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) )
250	249 84	syldan	|- ( ( ph /\ n e. ( ( ( |_ ` ( Z / ( K ^ M ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) e. RR )
251		elfzle2	|- ( n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) -> n <_ ( |_ ` ( Z / Y ) ) )
252	251	adantl	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> n <_ ( |_ ` ( Z / Y ) ) )
253	11	simpld	|- ( ph -> Y e. RR+ )
254	39 253	rpdivcld	|- ( ph -> ( Z / Y ) e. RR+ )
255	254	rpred	|- ( ph -> ( Z / Y ) e. RR )
256		elfzelz	|- ( n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) -> n e. ZZ )
257		flge	|- ( ( ( Z / Y ) e. RR /\ n e. ZZ ) -> ( n <_ ( Z / Y ) <-> n <_ ( |_ ` ( Z / Y ) ) ) )
258	255 256 257	syl2an	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( n <_ ( Z / Y ) <-> n <_ ( |_ ` ( Z / Y ) ) ) )
259	252 258	mpbird	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> n <_ ( Z / Y ) )
260	73 259	jca	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( n e. NN /\ n <_ ( Z / Y ) ) )
261	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 ) ) )
262	260 261	syldan	|- ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> 0 <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
263	249 262	syldan	|- ( ( ph /\ n e. ( ( ( |_ ` ( Z / ( K ^ M ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ) -> 0 <_ ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
264	238 250 263	fsumge0	|- ( ph -> 0 <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ M ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
265	237 264	eqbrtrd	|- ( ph -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( M - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ M ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
266	265	a1i	|- ( N e. ( ZZ>= ` M ) -> ( ph -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( M - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ M ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) )
267		eqid	|- ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ j ) ) ) ) = ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ j ) ) ) )
268	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 267	pntlemi	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ j ) ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
269	56	adantr	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) e. RR+ )
270	269	rpred	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) e. RR )
271		elfzoelz	|- ( j e. ( M ..^ N ) -> j e. ZZ )
272	271	adantl	|- ( ( ph /\ j e. ( M ..^ N ) ) -> j e. ZZ )
273	272	zred	|- ( ( ph /\ j e. ( M ..^ N ) ) -> j e. RR )
274	59	adantr	|- ( ( ph /\ j e. ( M ..^ N ) ) -> M e. NN )
275	274	nnred	|- ( ( ph /\ j e. ( M ..^ N ) ) -> M e. RR )
276	273 275	resubcld	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( j - M ) e. RR )
277	270 276	remulcld	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( j - M ) ) e. RR )
278		fzfid	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ j ) ) ) ) e. Fin )
279		ssun1	|- ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ j ) ) ) ) C_ ( ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ j ) ) ) ) u. ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) )
280	40	adantr	|- ( ( ph /\ j e. ( M ..^ N ) ) -> Z e. RR )
281	87	adantr	|- ( ( ph /\ j e. ( M ..^ N ) ) -> K e. RR+ )
282	272	peano2zd	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( j + 1 ) e. ZZ )
283	281 282	rpexpcld	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( K ^ ( j + 1 ) ) e. RR+ )
284	280 283	rerpdivcld	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( Z / ( K ^ ( j + 1 ) ) ) e. RR )
285	281 272	rpexpcld	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( K ^ j ) e. RR+ )
286	280 285	rerpdivcld	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( Z / ( K ^ j ) ) e. RR )
287	88	adantr	|- ( ( ph /\ j e. ( M ..^ N ) ) -> K e. RR )
288		1re	|- 1 e. RR
289		ltle	|- ( ( 1 e. RR /\ K e. RR ) -> ( 1 < K -> 1 <_ K ) )
290	288 88 289	sylancr	|- ( ph -> ( 1 < K -> 1 <_ K ) )
291	89 290	mpd	|- ( ph -> 1 <_ K )
292	291	adantr	|- ( ( ph /\ j e. ( M ..^ N ) ) -> 1 <_ K )
293		uzid	|- ( j e. ZZ -> j e. ( ZZ>= ` j ) )
294		peano2uz	|- ( j e. ( ZZ>= ` j ) -> ( j + 1 ) e. ( ZZ>= ` j ) )
295	272 293 294	3syl	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( j + 1 ) e. ( ZZ>= ` j ) )
296	287 292 295	leexp2ad	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( K ^ j ) <_ ( K ^ ( j + 1 ) ) )
297	39	adantr	|- ( ( ph /\ j e. ( M ..^ N ) ) -> Z e. RR+ )
298	285 283 297	lediv2d	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( K ^ j ) <_ ( K ^ ( j + 1 ) ) <-> ( Z / ( K ^ ( j + 1 ) ) ) <_ ( Z / ( K ^ j ) ) ) )
299	296 298	mpbid	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( Z / ( K ^ ( j + 1 ) ) ) <_ ( Z / ( K ^ j ) ) )
300		flword2	|- ( ( ( Z / ( K ^ ( j + 1 ) ) ) e. RR /\ ( Z / ( K ^ j ) ) e. RR /\ ( Z / ( K ^ ( j + 1 ) ) ) <_ ( Z / ( K ^ j ) ) ) -> ( |_ ` ( Z / ( K ^ j ) ) ) e. ( ZZ>= ` ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) ) )
301	284 286 299 300	syl3anc	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( |_ ` ( Z / ( K ^ j ) ) ) e. ( ZZ>= ` ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) ) )
302		eluzp1p1	|- ( ( |_ ` ( Z / ( K ^ j ) ) ) e. ( ZZ>= ` ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) ) -> ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) e. ( ZZ>= ` ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ) )
303	301 302	syl	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) e. ( ZZ>= ` ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ) )
304	286	flcld	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( |_ ` ( Z / ( K ^ j ) ) ) e. ZZ )
305	254	adantr	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( Z / Y ) e. RR+ )
306	305	rpred	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( Z / Y ) e. RR )
307	306	flcld	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( |_ ` ( Z / Y ) ) e. ZZ )
308	253	adantr	|- ( ( ph /\ j e. ( M ..^ N ) ) -> Y e. RR+ )
309	308	rpred	|- ( ( ph /\ j e. ( M ..^ N ) ) -> Y e. RR )
310	285	rpred	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( K ^ j ) e. RR )
311	12	simpld	|- ( ph -> X e. RR+ )
312	311	rpred	|- ( ph -> X e. RR )
313	312	adantr	|- ( ( ph /\ j e. ( M ..^ N ) ) -> X e. RR )
314	12	simprd	|- ( ph -> Y < X )
315	314	adantr	|- ( ( ph /\ j e. ( M ..^ N ) ) -> Y < X )
316		elfzofz	|- ( j e. ( M ..^ N ) -> j e. ( M ... N ) )
317	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 ) ) )
318	316 317	sylan2	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( X < ( K ^ j ) /\ ( K ^ j ) <_ ( sqrt ` Z ) ) )
319	318	simpld	|- ( ( ph /\ j e. ( M ..^ N ) ) -> X < ( K ^ j ) )
320	309 313 310 315 319	lttrd	|- ( ( ph /\ j e. ( M ..^ N ) ) -> Y < ( K ^ j ) )
321	309 310 320	ltled	|- ( ( ph /\ j e. ( M ..^ N ) ) -> Y <_ ( K ^ j ) )
322	308 285 297	lediv2d	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( Y <_ ( K ^ j ) <-> ( Z / ( K ^ j ) ) <_ ( Z / Y ) ) )
323	321 322	mpbid	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( Z / ( K ^ j ) ) <_ ( Z / Y ) )
324		flwordi	|- ( ( ( Z / ( K ^ j ) ) e. RR /\ ( Z / Y ) e. RR /\ ( Z / ( K ^ j ) ) <_ ( Z / Y ) ) -> ( |_ ` ( Z / ( K ^ j ) ) ) <_ ( |_ ` ( Z / Y ) ) )
325	286 306 323 324	syl3anc	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( |_ ` ( Z / ( K ^ j ) ) ) <_ ( |_ ` ( Z / Y ) ) )
326		eluz2	|- ( ( |_ ` ( Z / Y ) ) e. ( ZZ>= ` ( |_ ` ( Z / ( K ^ j ) ) ) ) <-> ( ( |_ ` ( Z / ( K ^ j ) ) ) e. ZZ /\ ( |_ ` ( Z / Y ) ) e. ZZ /\ ( |_ ` ( Z / ( K ^ j ) ) ) <_ ( |_ ` ( Z / Y ) ) ) )
327	304 307 325 326	syl3anbrc	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( |_ ` ( Z / Y ) ) e. ( ZZ>= ` ( |_ ` ( Z / ( K ^ j ) ) ) ) )
328		fzsplit2	|- ( ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) e. ( ZZ>= ` ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ) /\ ( |_ ` ( Z / Y ) ) e. ( ZZ>= ` ( |_ ` ( Z / ( K ^ j ) ) ) ) ) -> ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) = ( ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ j ) ) ) ) u. ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ) )
329	303 327 328	syl2anc	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) = ( ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ j ) ) ) ) u. ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ) )
330	279 329	sseqtrrid	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ j ) ) ) ) C_ ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) )
331	297 283	rpdivcld	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( Z / ( K ^ ( j + 1 ) ) ) e. RR+ )
332	331	rprege0d	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( Z / ( K ^ ( j + 1 ) ) ) e. RR /\ 0 <_ ( Z / ( K ^ ( j + 1 ) ) ) ) )
333		flge0nn0	|- ( ( ( Z / ( K ^ ( j + 1 ) ) ) e. RR /\ 0 <_ ( Z / ( K ^ ( j + 1 ) ) ) ) -> ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) e. NN0 )
334		nn0p1nn	|- ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) e. NN0 -> ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) e. NN )
335	332 333 334	3syl	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) e. NN )
336	335 183	eleqtrdi	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) e. ( ZZ>= ` 1 ) )
337		fzss1	|- ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) e. ( ZZ>= ` 1 ) -> ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) C_ ( 1 ... ( |_ ` ( Z / Y ) ) ) )
338	336 337	syl	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) C_ ( 1 ... ( |_ ` ( Z / Y ) ) ) )
339	330 338	sstrd	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ j ) ) ) ) C_ ( 1 ... ( |_ ` ( Z / Y ) ) ) )
340	339	sselda	|- ( ( ( ph /\ j e. ( M ..^ N ) ) /\ n e. ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ j ) ) ) ) ) -> n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) )
341	84	adantlr	|- ( ( ( ph /\ j e. ( M ..^ N ) ) /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) e. RR )
342	340 341	syldan	|- ( ( ( ph /\ j e. ( M ..^ N ) ) /\ n e. ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ j ) ) ) ) ) -> ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) e. RR )
343	278 342	fsumrecl	|- ( ( ph /\ j e. ( M ..^ N ) ) -> sum_ n e. ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ j ) ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) e. RR )
344		fzfid	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) e. Fin )
345		ssun2	|- ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) C_ ( ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ j ) ) ) ) u. ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) )
346	345 329	sseqtrrid	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) C_ ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) )
347	346 338	sstrd	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) C_ ( 1 ... ( |_ ` ( Z / Y ) ) ) )
348	347	sselda	|- ( ( ( ph /\ j e. ( M ..^ N ) ) /\ n e. ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ) -> n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) )
349	348 341	syldan	|- ( ( ( ph /\ j e. ( M ..^ N ) ) /\ n e. ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) e. RR )
350	344 349	fsumrecl	|- ( ( ph /\ j e. ( M ..^ N ) ) -> sum_ n e. ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) e. RR )
351		le2add	|- ( ( ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) e. RR /\ ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( j - M ) ) e. RR ) /\ ( sum_ n e. ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ j ) ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) e. RR /\ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) e. RR ) ) -> ( ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ j ) ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) /\ ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( j - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) + ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( j - M ) ) ) <_ ( sum_ n e. ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ j ) ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) + sum_ n e. ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) ) )
352	270 277 343 350 351	syl22anc	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ j ) ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) /\ ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( j - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) + ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( j - M ) ) ) <_ ( sum_ n e. ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ j ) ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) + sum_ n e. ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) ) )
353	268 352	mpand	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( j - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) + ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( j - M ) ) ) <_ ( sum_ n e. ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ j ) ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) + sum_ n e. ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) ) )
354	235	adantr	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) e. CC )
355		1cnd	|- ( ( ph /\ j e. ( M ..^ N ) ) -> 1 e. CC )
356	272	zcnd	|- ( ( ph /\ j e. ( M ..^ N ) ) -> j e. CC )
357	232	adantr	|- ( ( ph /\ j e. ( M ..^ N ) ) -> M e. CC )
358	356 357	subcld	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( j - M ) e. CC )
359	354 355 358	adddid	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( 1 + ( j - M ) ) ) = ( ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. 1 ) + ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( j - M ) ) ) )
360	355 358	addcomd	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( 1 + ( j - M ) ) = ( ( j - M ) + 1 ) )
361	356 355 357	addsubd	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( j + 1 ) - M ) = ( ( j - M ) + 1 ) )
362	360 361	eqtr4d	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( 1 + ( j - M ) ) = ( ( j + 1 ) - M ) )
363	362	oveq2d	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( 1 + ( j - M ) ) ) = ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( ( j + 1 ) - M ) ) )
364	354	mulid1d	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. 1 ) = ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) )
365	364	oveq1d	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. 1 ) + ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( j - M ) ) ) = ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) + ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( j - M ) ) ) )
366	359 363 365	3eqtr3d	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( ( j + 1 ) - M ) ) = ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) + ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( j - M ) ) ) )
367		reflcl	|- ( ( Z / ( K ^ j ) ) e. RR -> ( |_ ` ( Z / ( K ^ j ) ) ) e. RR )
368	286 367	syl	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( |_ ` ( Z / ( K ^ j ) ) ) e. RR )
369	368	ltp1d	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( |_ ` ( Z / ( K ^ j ) ) ) < ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) )
370		fzdisj	|- ( ( |_ ` ( Z / ( K ^ j ) ) ) < ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) -> ( ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ j ) ) ) ) i^i ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ) = (/) )
371	369 370	syl	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ j ) ) ) ) i^i ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ) = (/) )
372		fzfid	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) e. Fin )
373	338	sselda	|- ( ( ( ph /\ j e. ( M ..^ N ) ) /\ n e. ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ) -> n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) )
374	373 341	syldan	|- ( ( ( ph /\ j e. ( M ..^ N ) ) /\ n e. ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) e. RR )
375	374	recnd	|- ( ( ( ph /\ j e. ( M ..^ N ) ) /\ n e. ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) e. CC )
376	371 329 372 375	fsumsplit	|- ( ( ph /\ j e. ( M ..^ N ) ) -> sum_ n e. ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) = ( sum_ n e. ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ j ) ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) + sum_ n e. ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) )
377	366 376	breq12d	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( ( j + 1 ) - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) <-> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) + ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( j - M ) ) ) <_ ( sum_ n e. ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ j ) ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) + sum_ n e. ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) ) )
378	353 377	sylibrd	|- ( ( ph /\ j e. ( M ..^ N ) ) -> ( ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( j - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( ( j + 1 ) - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) )
379	378	expcom	|- ( j e. ( M ..^ N ) -> ( ph -> ( ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( j - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( ( j + 1 ) - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) ) )
380	379	a2d	|- ( j e. ( M ..^ N ) -> ( ( ph -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( j - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ j ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) -> ( ph -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( ( j + 1 ) - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ ( j + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) ) )
381	201 211 221 231 266 380	fzind2	|- ( N e. ( M ... N ) -> ( ph -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( N - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ N ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) ) )
382	191 381	mpcom	|- ( ph -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( N - M ) ) <_ sum_ n e. ( ( ( |_ ` ( Z / ( K ^ N ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
383	67 84 262 186	fsumless	|- ( ph -> sum_ n e. ( ( ( |_ ` ( Z / ( K ^ N ) ) ) + 1 ) ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) <_ sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
384	66 189 85 382 383	letrd	|- ( ph -> ( ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) x. ( N - M ) ) <_ sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
385	48 66 85 174 384	letrd	|- ( ph -> ( ( U - E ) x. ( ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) x. ( ( log ` Z ) ^ 2 ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )