Theorem pntpbnd2

Description: Lemma for pntpbnd . (Contributed by Mario Carneiro, 11-Apr-2016)

	Ref	Expression
Hypotheses	pntpbnd.r	|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
	pntpbnd1.e	|- ( ph -> E e. ( 0 (,) 1 ) )
	pntpbnd1.x	|- X = ( exp ` ( 2 / E ) )
	pntpbnd1.y	|- ( ph -> Y e. ( X (,) +oo ) )
	pntpbnd1.1	|- ( ph -> A e. RR+ )
	pntpbnd1.2	|- ( ph -> A. i e. NN A. j e. ZZ ( abs ` sum_ y e. ( i ... j ) ( ( R ` y ) / ( y x. ( y + 1 ) ) ) ) <_ A )
	pntpbnd1.c	|- C = ( A + 2 )
	pntpbnd1.k	|- ( ph -> K e. ( ( exp ` ( C / E ) ) [,) +oo ) )
	pntpbnd1.3	|- ( ph -> -. E. y e. NN ( ( Y < y /\ y <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` y ) / y ) ) <_ E ) )
Assertion	pntpbnd2	|- -. ph

Proof

Step	Hyp	Ref	Expression
1		pntpbnd.r	|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2		pntpbnd1.e	|- ( ph -> E e. ( 0 (,) 1 ) )
3		pntpbnd1.x	|- X = ( exp ` ( 2 / E ) )
4		pntpbnd1.y	|- ( ph -> Y e. ( X (,) +oo ) )
5		pntpbnd1.1	|- ( ph -> A e. RR+ )
6		pntpbnd1.2	|- ( ph -> A. i e. NN A. j e. ZZ ( abs ` sum_ y e. ( i ... j ) ( ( R ` y ) / ( y x. ( y + 1 ) ) ) ) <_ A )
7		pntpbnd1.c	|- C = ( A + 2 )
8		pntpbnd1.k	|- ( ph -> K e. ( ( exp ` ( C / E ) ) [,) +oo ) )
9		pntpbnd1.3	|- ( ph -> -. E. y e. NN ( ( Y < y /\ y <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` y ) / y ) ) <_ E ) )
10		2div2e1	|- ( 2 / 2 ) = 1
11		2re	|- 2 e. RR
12	11	a1i	|- ( ph -> 2 e. RR )
13		ioossre	|- ( 0 (,) 1 ) C_ RR
14	13 2	sselid	|- ( ph -> E e. RR )
15		eliooord	|- ( E e. ( 0 (,) 1 ) -> ( 0 < E /\ E < 1 ) )
16	2 15	syl	|- ( ph -> ( 0 < E /\ E < 1 ) )
17	16	simpld	|- ( ph -> 0 < E )
18	14 17	elrpd	|- ( ph -> E e. RR+ )
19		2rp	|- 2 e. RR+
20	19	a1i	|- ( ph -> 2 e. RR+ )
21	7	oveq1i	|- ( C - A ) = ( ( A + 2 ) - A )
22	5	rpcnd	|- ( ph -> A e. CC )
23		2cn	|- 2 e. CC
24		pncan2	|- ( ( A e. CC /\ 2 e. CC ) -> ( ( A + 2 ) - A ) = 2 )
25	22 23 24	sylancl	|- ( ph -> ( ( A + 2 ) - A ) = 2 )
26	21 25	eqtrid	|- ( ph -> ( C - A ) = 2 )
27	26	oveq1d	|- ( ph -> ( ( C - A ) / E ) = ( 2 / E ) )
28		rpaddcl	|- ( ( A e. RR+ /\ 2 e. RR+ ) -> ( A + 2 ) e. RR+ )
29	5 19 28	sylancl	|- ( ph -> ( A + 2 ) e. RR+ )
30	7 29	eqeltrid	|- ( ph -> C e. RR+ )
31	30	rpcnd	|- ( ph -> C e. CC )
32	14	recnd	|- ( ph -> E e. CC )
33	18	rpne0d	|- ( ph -> E =/= 0 )
34	31 22 32 33	divsubdird	|- ( ph -> ( ( C - A ) / E ) = ( ( C / E ) - ( A / E ) ) )
35	27 34	eqtr3d	|- ( ph -> ( 2 / E ) = ( ( C / E ) - ( A / E ) ) )
36	30 18	rpdivcld	|- ( ph -> ( C / E ) e. RR+ )
37	36	rpred	|- ( ph -> ( C / E ) e. RR )
38	5	rpred	|- ( ph -> A e. RR )
39	38 18	rerpdivcld	|- ( ph -> ( A / E ) e. RR )
40		resubcl	|- ( ( ( C / E ) e. RR /\ 2 e. RR ) -> ( ( C / E ) - 2 ) e. RR )
41	37 11 40	sylancl	|- ( ph -> ( ( C / E ) - 2 ) e. RR )
42	37	reefcld	|- ( ph -> ( exp ` ( C / E ) ) e. RR )
43		elicopnf	|- ( ( exp ` ( C / E ) ) e. RR -> ( K e. ( ( exp ` ( C / E ) ) [,) +oo ) <-> ( K e. RR /\ ( exp ` ( C / E ) ) <_ K ) ) )
44	42 43	syl	|- ( ph -> ( K e. ( ( exp ` ( C / E ) ) [,) +oo ) <-> ( K e. RR /\ ( exp ` ( C / E ) ) <_ K ) ) )
45	8 44	mpbid	|- ( ph -> ( K e. RR /\ ( exp ` ( C / E ) ) <_ K ) )
46	45	simpld	|- ( ph -> K e. RR )
47		0red	|- ( ph -> 0 e. RR )
48		1re	|- 1 e. RR
49	48	a1i	|- ( ph -> 1 e. RR )
50		0lt1	|- 0 < 1
51	50	a1i	|- ( ph -> 0 < 1 )
52		efgt1	|- ( ( C / E ) e. RR+ -> 1 < ( exp ` ( C / E ) ) )
53	36 52	syl	|- ( ph -> 1 < ( exp ` ( C / E ) ) )
54	45	simprd	|- ( ph -> ( exp ` ( C / E ) ) <_ K )
55	49 42 46 53 54	ltletrd	|- ( ph -> 1 < K )
56	47 49 46 51 55	lttrd	|- ( ph -> 0 < K )
57	46 56	elrpd	|- ( ph -> K e. RR+ )
58	57	relogcld	|- ( ph -> ( log ` K ) e. RR )
59		resubcl	|- ( ( ( log ` K ) e. RR /\ 2 e. RR ) -> ( ( log ` K ) - 2 ) e. RR )
60	58 11 59	sylancl	|- ( ph -> ( ( log ` K ) - 2 ) e. RR )
61	57	reeflogd	|- ( ph -> ( exp ` ( log ` K ) ) = K )
62	54 61	breqtrrd	|- ( ph -> ( exp ` ( C / E ) ) <_ ( exp ` ( log ` K ) ) )
63		efle	|- ( ( ( C / E ) e. RR /\ ( log ` K ) e. RR ) -> ( ( C / E ) <_ ( log ` K ) <-> ( exp ` ( C / E ) ) <_ ( exp ` ( log ` K ) ) ) )
64	37 58 63	syl2anc	|- ( ph -> ( ( C / E ) <_ ( log ` K ) <-> ( exp ` ( C / E ) ) <_ ( exp ` ( log ` K ) ) ) )
65	62 64	mpbird	|- ( ph -> ( C / E ) <_ ( log ` K ) )
66	37 58 12 65	lesub1dd	|- ( ph -> ( ( C / E ) - 2 ) <_ ( ( log ` K ) - 2 ) )
67		fzfid	|- ( ph -> ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) e. Fin )
68		ioossre	|- ( X (,) +oo ) C_ RR
69	68 4	sselid	|- ( ph -> Y e. RR )
70		rerpdivcl	|- ( ( 2 e. RR /\ E e. RR+ ) -> ( 2 / E ) e. RR )
71	11 18 70	sylancr	|- ( ph -> ( 2 / E ) e. RR )
72	71	reefcld	|- ( ph -> ( exp ` ( 2 / E ) ) e. RR )
73	3 72	eqeltrid	|- ( ph -> X e. RR )
74		efgt0	|- ( ( 2 / E ) e. RR -> 0 < ( exp ` ( 2 / E ) ) )
75	71 74	syl	|- ( ph -> 0 < ( exp ` ( 2 / E ) ) )
76	75 3	breqtrrdi	|- ( ph -> 0 < X )
77	73	rexrd	|- ( ph -> X e. RR* )
78		elioopnf	|- ( X e. RR* -> ( Y e. ( X (,) +oo ) <-> ( Y e. RR /\ X < Y ) ) )
79	77 78	syl	|- ( ph -> ( Y e. ( X (,) +oo ) <-> ( Y e. RR /\ X < Y ) ) )
80	4 79	mpbid	|- ( ph -> ( Y e. RR /\ X < Y ) )
81	80	simprd	|- ( ph -> X < Y )
82	47 73 69 76 81	lttrd	|- ( ph -> 0 < Y )
83	47 69 82	ltled	|- ( ph -> 0 <_ Y )
84		flge0nn0	|- ( ( Y e. RR /\ 0 <_ Y ) -> ( |_ ` Y ) e. NN0 )
85	69 83 84	syl2anc	|- ( ph -> ( |_ ` Y ) e. NN0 )
86		nn0p1nn	|- ( ( |_ ` Y ) e. NN0 -> ( ( |_ ` Y ) + 1 ) e. NN )
87	85 86	syl	|- ( ph -> ( ( |_ ` Y ) + 1 ) e. NN )
88		elfzuz	|- ( n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) -> n e. ( ZZ>= ` ( ( |_ ` Y ) + 1 ) ) )
89		eluznn	|- ( ( ( ( |_ ` Y ) + 1 ) e. NN /\ n e. ( ZZ>= ` ( ( |_ ` Y ) + 1 ) ) ) -> n e. NN )
90	87 88 89	syl2an	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> n e. NN )
91	90	peano2nnd	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( n + 1 ) e. NN )
92	91	nnrecred	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( 1 / ( n + 1 ) ) e. RR )
93	67 92	fsumrecl	|- ( ph -> sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( 1 / ( n + 1 ) ) e. RR )
94	58	recnd	|- ( ph -> ( log ` K ) e. CC )
95		2cnd	|- ( ph -> 2 e. CC )
96	69 82	elrpd	|- ( ph -> Y e. RR+ )
97	96	relogcld	|- ( ph -> ( log ` Y ) e. RR )
98	97	recnd	|- ( ph -> ( log ` Y ) e. CC )
99	94 95 98	pnpcan2d	|- ( ph -> ( ( ( log ` K ) + ( log ` Y ) ) - ( 2 + ( log ` Y ) ) ) = ( ( log ` K ) - 2 ) )
100	57 96	relogmuld	|- ( ph -> ( log ` ( K x. Y ) ) = ( ( log ` K ) + ( log ` Y ) ) )
101	58 97	readdcld	|- ( ph -> ( ( log ` K ) + ( log ` Y ) ) e. RR )
102	100 101	eqeltrd	|- ( ph -> ( log ` ( K x. Y ) ) e. RR )
103		fzfid	|- ( ph -> ( 0 ... ( |_ ` Y ) ) e. Fin )
104		elfznn0	|- ( n e. ( 0 ... ( |_ ` Y ) ) -> n e. NN0 )
105	104	adantl	|- ( ( ph /\ n e. ( 0 ... ( |_ ` Y ) ) ) -> n e. NN0 )
106		nn0p1nn	|- ( n e. NN0 -> ( n + 1 ) e. NN )
107	105 106	syl	|- ( ( ph /\ n e. ( 0 ... ( |_ ` Y ) ) ) -> ( n + 1 ) e. NN )
108	107	nnrecred	|- ( ( ph /\ n e. ( 0 ... ( |_ ` Y ) ) ) -> ( 1 / ( n + 1 ) ) e. RR )
109	103 108	fsumrecl	|- ( ph -> sum_ n e. ( 0 ... ( |_ ` Y ) ) ( 1 / ( n + 1 ) ) e. RR )
110	109 93	readdcld	|- ( ph -> ( sum_ n e. ( 0 ... ( |_ ` Y ) ) ( 1 / ( n + 1 ) ) + sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( 1 / ( n + 1 ) ) ) e. RR )
111		readdcl	|- ( ( 2 e. RR /\ ( log ` Y ) e. RR ) -> ( 2 + ( log ` Y ) ) e. RR )
112	11 97 111	sylancr	|- ( ph -> ( 2 + ( log ` Y ) ) e. RR )
113	112 93	readdcld	|- ( ph -> ( ( 2 + ( log ` Y ) ) + sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( 1 / ( n + 1 ) ) ) e. RR )
114	46 69	remulcld	|- ( ph -> ( K x. Y ) e. RR )
115	69	recnd	|- ( ph -> Y e. CC )
116	115	mulid2d	|- ( ph -> ( 1 x. Y ) = Y )
117	49 46 55	ltled	|- ( ph -> 1 <_ K )
118		lemul1	|- ( ( 1 e. RR /\ K e. RR /\ ( Y e. RR /\ 0 < Y ) ) -> ( 1 <_ K <-> ( 1 x. Y ) <_ ( K x. Y ) ) )
119	49 46 69 82 118	syl112anc	|- ( ph -> ( 1 <_ K <-> ( 1 x. Y ) <_ ( K x. Y ) ) )
120	117 119	mpbid	|- ( ph -> ( 1 x. Y ) <_ ( K x. Y ) )
121	116 120	eqbrtrrd	|- ( ph -> Y <_ ( K x. Y ) )
122	47 69 114 83 121	letrd	|- ( ph -> 0 <_ ( K x. Y ) )
123		flge0nn0	|- ( ( ( K x. Y ) e. RR /\ 0 <_ ( K x. Y ) ) -> ( |_ ` ( K x. Y ) ) e. NN0 )
124	114 122 123	syl2anc	|- ( ph -> ( |_ ` ( K x. Y ) ) e. NN0 )
125		nn0p1nn	|- ( ( |_ ` ( K x. Y ) ) e. NN0 -> ( ( |_ ` ( K x. Y ) ) + 1 ) e. NN )
126	124 125	syl	|- ( ph -> ( ( |_ ` ( K x. Y ) ) + 1 ) e. NN )
127	126	nnrpd	|- ( ph -> ( ( |_ ` ( K x. Y ) ) + 1 ) e. RR+ )
128	127	relogcld	|- ( ph -> ( log ` ( ( |_ ` ( K x. Y ) ) + 1 ) ) e. RR )
129		1zzd	|- ( ph -> 1 e. ZZ )
130	114	flcld	|- ( ph -> ( |_ ` ( K x. Y ) ) e. ZZ )
131	130	peano2zd	|- ( ph -> ( ( |_ ` ( K x. Y ) ) + 1 ) e. ZZ )
132		elfznn	|- ( k e. ( 1 ... ( ( |_ ` ( K x. Y ) ) + 1 ) ) -> k e. NN )
133	132	adantl	|- ( ( ph /\ k e. ( 1 ... ( ( |_ ` ( K x. Y ) ) + 1 ) ) ) -> k e. NN )
134		nnrecre	|- ( k e. NN -> ( 1 / k ) e. RR )
135	134	recnd	|- ( k e. NN -> ( 1 / k ) e. CC )
136	133 135	syl	|- ( ( ph /\ k e. ( 1 ... ( ( |_ ` ( K x. Y ) ) + 1 ) ) ) -> ( 1 / k ) e. CC )
137		oveq2	|- ( k = ( n + 1 ) -> ( 1 / k ) = ( 1 / ( n + 1 ) ) )
138	129 129 131 136 137	fsumshftm	|- ( ph -> sum_ k e. ( 1 ... ( ( |_ ` ( K x. Y ) ) + 1 ) ) ( 1 / k ) = sum_ n e. ( ( 1 - 1 ) ... ( ( ( |_ ` ( K x. Y ) ) + 1 ) - 1 ) ) ( 1 / ( n + 1 ) ) )
139		1m1e0	|- ( 1 - 1 ) = 0
140	139	a1i	|- ( ph -> ( 1 - 1 ) = 0 )
141	130	zcnd	|- ( ph -> ( |_ ` ( K x. Y ) ) e. CC )
142		ax-1cn	|- 1 e. CC
143		pncan	|- ( ( ( |_ ` ( K x. Y ) ) e. CC /\ 1 e. CC ) -> ( ( ( |_ ` ( K x. Y ) ) + 1 ) - 1 ) = ( |_ ` ( K x. Y ) ) )
144	141 142 143	sylancl	|- ( ph -> ( ( ( |_ ` ( K x. Y ) ) + 1 ) - 1 ) = ( |_ ` ( K x. Y ) ) )
145	140 144	oveq12d	|- ( ph -> ( ( 1 - 1 ) ... ( ( ( |_ ` ( K x. Y ) ) + 1 ) - 1 ) ) = ( 0 ... ( |_ ` ( K x. Y ) ) ) )
146	145	sumeq1d	|- ( ph -> sum_ n e. ( ( 1 - 1 ) ... ( ( ( |_ ` ( K x. Y ) ) + 1 ) - 1 ) ) ( 1 / ( n + 1 ) ) = sum_ n e. ( 0 ... ( |_ ` ( K x. Y ) ) ) ( 1 / ( n + 1 ) ) )
147		reflcl	|- ( Y e. RR -> ( |_ ` Y ) e. RR )
148	69 147	syl	|- ( ph -> ( |_ ` Y ) e. RR )
149	148	ltp1d	|- ( ph -> ( |_ ` Y ) < ( ( |_ ` Y ) + 1 ) )
150		fzdisj	|- ( ( |_ ` Y ) < ( ( |_ ` Y ) + 1 ) -> ( ( 0 ... ( |_ ` Y ) ) i^i ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) = (/) )
151	149 150	syl	|- ( ph -> ( ( 0 ... ( |_ ` Y ) ) i^i ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) = (/) )
152		flwordi	|- ( ( Y e. RR /\ ( K x. Y ) e. RR /\ Y <_ ( K x. Y ) ) -> ( |_ ` Y ) <_ ( |_ ` ( K x. Y ) ) )
153	69 114 121 152	syl3anc	|- ( ph -> ( |_ ` Y ) <_ ( |_ ` ( K x. Y ) ) )
154		elfz2nn0	|- ( ( |_ ` Y ) e. ( 0 ... ( |_ ` ( K x. Y ) ) ) <-> ( ( |_ ` Y ) e. NN0 /\ ( |_ ` ( K x. Y ) ) e. NN0 /\ ( |_ ` Y ) <_ ( |_ ` ( K x. Y ) ) ) )
155	85 124 153 154	syl3anbrc	|- ( ph -> ( |_ ` Y ) e. ( 0 ... ( |_ ` ( K x. Y ) ) ) )
156		fzsplit	|- ( ( |_ ` Y ) e. ( 0 ... ( |_ ` ( K x. Y ) ) ) -> ( 0 ... ( |_ ` ( K x. Y ) ) ) = ( ( 0 ... ( |_ ` Y ) ) u. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) )
157	155 156	syl	|- ( ph -> ( 0 ... ( |_ ` ( K x. Y ) ) ) = ( ( 0 ... ( |_ ` Y ) ) u. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) )
158		fzfid	|- ( ph -> ( 0 ... ( |_ ` ( K x. Y ) ) ) e. Fin )
159		elfznn0	|- ( n e. ( 0 ... ( |_ ` ( K x. Y ) ) ) -> n e. NN0 )
160	159	adantl	|- ( ( ph /\ n e. ( 0 ... ( |_ ` ( K x. Y ) ) ) ) -> n e. NN0 )
161	160 106	syl	|- ( ( ph /\ n e. ( 0 ... ( |_ ` ( K x. Y ) ) ) ) -> ( n + 1 ) e. NN )
162	161	nnrecred	|- ( ( ph /\ n e. ( 0 ... ( |_ ` ( K x. Y ) ) ) ) -> ( 1 / ( n + 1 ) ) e. RR )
163	162	recnd	|- ( ( ph /\ n e. ( 0 ... ( |_ ` ( K x. Y ) ) ) ) -> ( 1 / ( n + 1 ) ) e. CC )
164	151 157 158 163	fsumsplit	|- ( ph -> sum_ n e. ( 0 ... ( |_ ` ( K x. Y ) ) ) ( 1 / ( n + 1 ) ) = ( sum_ n e. ( 0 ... ( |_ ` Y ) ) ( 1 / ( n + 1 ) ) + sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( 1 / ( n + 1 ) ) ) )
165	138 146 164	3eqtrd	|- ( ph -> sum_ k e. ( 1 ... ( ( |_ ` ( K x. Y ) ) + 1 ) ) ( 1 / k ) = ( sum_ n e. ( 0 ... ( |_ ` Y ) ) ( 1 / ( n + 1 ) ) + sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( 1 / ( n + 1 ) ) ) )
166	165 110	eqeltrd	|- ( ph -> sum_ k e. ( 1 ... ( ( |_ ` ( K x. Y ) ) + 1 ) ) ( 1 / k ) e. RR )
167		fllep1	|- ( ( K x. Y ) e. RR -> ( K x. Y ) <_ ( ( |_ ` ( K x. Y ) ) + 1 ) )
168	114 167	syl	|- ( ph -> ( K x. Y ) <_ ( ( |_ ` ( K x. Y ) ) + 1 ) )
169	57 96	rpmulcld	|- ( ph -> ( K x. Y ) e. RR+ )
170	169 127	logled	|- ( ph -> ( ( K x. Y ) <_ ( ( |_ ` ( K x. Y ) ) + 1 ) <-> ( log ` ( K x. Y ) ) <_ ( log ` ( ( |_ ` ( K x. Y ) ) + 1 ) ) ) )
171	168 170	mpbid	|- ( ph -> ( log ` ( K x. Y ) ) <_ ( log ` ( ( |_ ` ( K x. Y ) ) + 1 ) ) )
172		emre	|- gamma e. RR
173	172	a1i	|- ( ph -> gamma e. RR )
174	166 128	resubcld	|- ( ph -> ( sum_ k e. ( 1 ... ( ( |_ ` ( K x. Y ) ) + 1 ) ) ( 1 / k ) - ( log ` ( ( |_ ` ( K x. Y ) ) + 1 ) ) ) e. RR )
175		0re	|- 0 e. RR
176		emgt0	|- 0 < gamma
177	175 172 176	ltleii	|- 0 <_ gamma
178	177	a1i	|- ( ph -> 0 <_ gamma )
179		harmonicbnd	|- ( ( ( |_ ` ( K x. Y ) ) + 1 ) e. NN -> ( sum_ k e. ( 1 ... ( ( |_ ` ( K x. Y ) ) + 1 ) ) ( 1 / k ) - ( log ` ( ( |_ ` ( K x. Y ) ) + 1 ) ) ) e. ( gamma [,] 1 ) )
180	126 179	syl	|- ( ph -> ( sum_ k e. ( 1 ... ( ( |_ ` ( K x. Y ) ) + 1 ) ) ( 1 / k ) - ( log ` ( ( |_ ` ( K x. Y ) ) + 1 ) ) ) e. ( gamma [,] 1 ) )
181	172 48	elicc2i	|- ( ( sum_ k e. ( 1 ... ( ( |_ ` ( K x. Y ) ) + 1 ) ) ( 1 / k ) - ( log ` ( ( |_ ` ( K x. Y ) ) + 1 ) ) ) e. ( gamma [,] 1 ) <-> ( ( sum_ k e. ( 1 ... ( ( |_ ` ( K x. Y ) ) + 1 ) ) ( 1 / k ) - ( log ` ( ( |_ ` ( K x. Y ) ) + 1 ) ) ) e. RR /\ gamma <_ ( sum_ k e. ( 1 ... ( ( |_ ` ( K x. Y ) ) + 1 ) ) ( 1 / k ) - ( log ` ( ( |_ ` ( K x. Y ) ) + 1 ) ) ) /\ ( sum_ k e. ( 1 ... ( ( |_ ` ( K x. Y ) ) + 1 ) ) ( 1 / k ) - ( log ` ( ( |_ ` ( K x. Y ) ) + 1 ) ) ) <_ 1 ) )
182	181	simp2bi	|- ( ( sum_ k e. ( 1 ... ( ( |_ ` ( K x. Y ) ) + 1 ) ) ( 1 / k ) - ( log ` ( ( |_ ` ( K x. Y ) ) + 1 ) ) ) e. ( gamma [,] 1 ) -> gamma <_ ( sum_ k e. ( 1 ... ( ( |_ ` ( K x. Y ) ) + 1 ) ) ( 1 / k ) - ( log ` ( ( |_ ` ( K x. Y ) ) + 1 ) ) ) )
183	180 182	syl	|- ( ph -> gamma <_ ( sum_ k e. ( 1 ... ( ( |_ ` ( K x. Y ) ) + 1 ) ) ( 1 / k ) - ( log ` ( ( |_ ` ( K x. Y ) ) + 1 ) ) ) )
184	47 173 174 178 183	letrd	|- ( ph -> 0 <_ ( sum_ k e. ( 1 ... ( ( |_ ` ( K x. Y ) ) + 1 ) ) ( 1 / k ) - ( log ` ( ( |_ ` ( K x. Y ) ) + 1 ) ) ) )
185	166 128	subge0d	|- ( ph -> ( 0 <_ ( sum_ k e. ( 1 ... ( ( |_ ` ( K x. Y ) ) + 1 ) ) ( 1 / k ) - ( log ` ( ( |_ ` ( K x. Y ) ) + 1 ) ) ) <-> ( log ` ( ( |_ ` ( K x. Y ) ) + 1 ) ) <_ sum_ k e. ( 1 ... ( ( |_ ` ( K x. Y ) ) + 1 ) ) ( 1 / k ) ) )
186	184 185	mpbid	|- ( ph -> ( log ` ( ( |_ ` ( K x. Y ) ) + 1 ) ) <_ sum_ k e. ( 1 ... ( ( |_ ` ( K x. Y ) ) + 1 ) ) ( 1 / k ) )
187	102 128 166 171 186	letrd	|- ( ph -> ( log ` ( K x. Y ) ) <_ sum_ k e. ( 1 ... ( ( |_ ` ( K x. Y ) ) + 1 ) ) ( 1 / k ) )
188	187 165	breqtrd	|- ( ph -> ( log ` ( K x. Y ) ) <_ ( sum_ n e. ( 0 ... ( |_ ` Y ) ) ( 1 / ( n + 1 ) ) + sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( 1 / ( n + 1 ) ) ) )
189	69	flcld	|- ( ph -> ( |_ ` Y ) e. ZZ )
190	189	peano2zd	|- ( ph -> ( ( |_ ` Y ) + 1 ) e. ZZ )
191		elfznn	|- ( k e. ( 1 ... ( ( |_ ` Y ) + 1 ) ) -> k e. NN )
192	191	adantl	|- ( ( ph /\ k e. ( 1 ... ( ( |_ ` Y ) + 1 ) ) ) -> k e. NN )
193	192 135	syl	|- ( ( ph /\ k e. ( 1 ... ( ( |_ ` Y ) + 1 ) ) ) -> ( 1 / k ) e. CC )
194	129 129 190 193 137	fsumshftm	|- ( ph -> sum_ k e. ( 1 ... ( ( |_ ` Y ) + 1 ) ) ( 1 / k ) = sum_ n e. ( ( 1 - 1 ) ... ( ( ( |_ ` Y ) + 1 ) - 1 ) ) ( 1 / ( n + 1 ) ) )
195	148	recnd	|- ( ph -> ( |_ ` Y ) e. CC )
196		pncan	|- ( ( ( |_ ` Y ) e. CC /\ 1 e. CC ) -> ( ( ( |_ ` Y ) + 1 ) - 1 ) = ( |_ ` Y ) )
197	195 142 196	sylancl	|- ( ph -> ( ( ( |_ ` Y ) + 1 ) - 1 ) = ( |_ ` Y ) )
198	140 197	oveq12d	|- ( ph -> ( ( 1 - 1 ) ... ( ( ( |_ ` Y ) + 1 ) - 1 ) ) = ( 0 ... ( |_ ` Y ) ) )
199	198	sumeq1d	|- ( ph -> sum_ n e. ( ( 1 - 1 ) ... ( ( ( |_ ` Y ) + 1 ) - 1 ) ) ( 1 / ( n + 1 ) ) = sum_ n e. ( 0 ... ( |_ ` Y ) ) ( 1 / ( n + 1 ) ) )
200	194 199	eqtrd	|- ( ph -> sum_ k e. ( 1 ... ( ( |_ ` Y ) + 1 ) ) ( 1 / k ) = sum_ n e. ( 0 ... ( |_ ` Y ) ) ( 1 / ( n + 1 ) ) )
201	200 109	eqeltrd	|- ( ph -> sum_ k e. ( 1 ... ( ( |_ ` Y ) + 1 ) ) ( 1 / k ) e. RR )
202	87	nnrpd	|- ( ph -> ( ( |_ ` Y ) + 1 ) e. RR+ )
203	202	relogcld	|- ( ph -> ( log ` ( ( |_ ` Y ) + 1 ) ) e. RR )
204		readdcl	|- ( ( 1 e. RR /\ ( log ` ( ( |_ ` Y ) + 1 ) ) e. RR ) -> ( 1 + ( log ` ( ( |_ ` Y ) + 1 ) ) ) e. RR )
205	48 203 204	sylancr	|- ( ph -> ( 1 + ( log ` ( ( |_ ` Y ) + 1 ) ) ) e. RR )
206		harmonicbnd	|- ( ( ( |_ ` Y ) + 1 ) e. NN -> ( sum_ k e. ( 1 ... ( ( |_ ` Y ) + 1 ) ) ( 1 / k ) - ( log ` ( ( |_ ` Y ) + 1 ) ) ) e. ( gamma [,] 1 ) )
207	87 206	syl	|- ( ph -> ( sum_ k e. ( 1 ... ( ( |_ ` Y ) + 1 ) ) ( 1 / k ) - ( log ` ( ( |_ ` Y ) + 1 ) ) ) e. ( gamma [,] 1 ) )
208	172 48	elicc2i	|- ( ( sum_ k e. ( 1 ... ( ( |_ ` Y ) + 1 ) ) ( 1 / k ) - ( log ` ( ( |_ ` Y ) + 1 ) ) ) e. ( gamma [,] 1 ) <-> ( ( sum_ k e. ( 1 ... ( ( |_ ` Y ) + 1 ) ) ( 1 / k ) - ( log ` ( ( |_ ` Y ) + 1 ) ) ) e. RR /\ gamma <_ ( sum_ k e. ( 1 ... ( ( |_ ` Y ) + 1 ) ) ( 1 / k ) - ( log ` ( ( |_ ` Y ) + 1 ) ) ) /\ ( sum_ k e. ( 1 ... ( ( |_ ` Y ) + 1 ) ) ( 1 / k ) - ( log ` ( ( |_ ` Y ) + 1 ) ) ) <_ 1 ) )
209	208	simp3bi	|- ( ( sum_ k e. ( 1 ... ( ( |_ ` Y ) + 1 ) ) ( 1 / k ) - ( log ` ( ( |_ ` Y ) + 1 ) ) ) e. ( gamma [,] 1 ) -> ( sum_ k e. ( 1 ... ( ( |_ ` Y ) + 1 ) ) ( 1 / k ) - ( log ` ( ( |_ ` Y ) + 1 ) ) ) <_ 1 )
210	207 209	syl	|- ( ph -> ( sum_ k e. ( 1 ... ( ( |_ ` Y ) + 1 ) ) ( 1 / k ) - ( log ` ( ( |_ ` Y ) + 1 ) ) ) <_ 1 )
211	201 203 49	lesubaddd	|- ( ph -> ( ( sum_ k e. ( 1 ... ( ( |_ ` Y ) + 1 ) ) ( 1 / k ) - ( log ` ( ( |_ ` Y ) + 1 ) ) ) <_ 1 <-> sum_ k e. ( 1 ... ( ( |_ ` Y ) + 1 ) ) ( 1 / k ) <_ ( 1 + ( log ` ( ( |_ ` Y ) + 1 ) ) ) ) )
212	210 211	mpbid	|- ( ph -> sum_ k e. ( 1 ... ( ( |_ ` Y ) + 1 ) ) ( 1 / k ) <_ ( 1 + ( log ` ( ( |_ ` Y ) + 1 ) ) ) )
213		readdcl	|- ( ( 1 e. RR /\ ( log ` Y ) e. RR ) -> ( 1 + ( log ` Y ) ) e. RR )
214	48 97 213	sylancr	|- ( ph -> ( 1 + ( log ` Y ) ) e. RR )
215		peano2re	|- ( ( |_ ` Y ) e. RR -> ( ( |_ ` Y ) + 1 ) e. RR )
216	148 215	syl	|- ( ph -> ( ( |_ ` Y ) + 1 ) e. RR )
217	12 69	remulcld	|- ( ph -> ( 2 x. Y ) e. RR )
218		epr	|- _e e. RR+
219		rpmulcl	|- ( ( _e e. RR+ /\ Y e. RR+ ) -> ( _e x. Y ) e. RR+ )
220	218 96 219	sylancr	|- ( ph -> ( _e x. Y ) e. RR+ )
221	220	rpred	|- ( ph -> ( _e x. Y ) e. RR )
222		flle	|- ( Y e. RR -> ( |_ ` Y ) <_ Y )
223	69 222	syl	|- ( ph -> ( |_ ` Y ) <_ Y )
224	20 18	rpdivcld	|- ( ph -> ( 2 / E ) e. RR+ )
225		efgt1	|- ( ( 2 / E ) e. RR+ -> 1 < ( exp ` ( 2 / E ) ) )
226	224 225	syl	|- ( ph -> 1 < ( exp ` ( 2 / E ) ) )
227	226 3	breqtrrdi	|- ( ph -> 1 < X )
228	49 73 69 227 81	lttrd	|- ( ph -> 1 < Y )
229	49 69 228	ltled	|- ( ph -> 1 <_ Y )
230	148 49 69 69 223 229	le2addd	|- ( ph -> ( ( |_ ` Y ) + 1 ) <_ ( Y + Y ) )
231	115	2timesd	|- ( ph -> ( 2 x. Y ) = ( Y + Y ) )
232	230 231	breqtrrd	|- ( ph -> ( ( |_ ` Y ) + 1 ) <_ ( 2 x. Y ) )
233		ere	|- _e e. RR
234		egt2lt3	|- ( 2 < _e /\ _e < 3 )
235	234	simpli	|- 2 < _e
236	11 233 235	ltleii	|- 2 <_ _e
237	236	a1i	|- ( ph -> 2 <_ _e )
238	233	a1i	|- ( ph -> _e e. RR )
239		lemul1	|- ( ( 2 e. RR /\ _e e. RR /\ ( Y e. RR /\ 0 < Y ) ) -> ( 2 <_ _e <-> ( 2 x. Y ) <_ ( _e x. Y ) ) )
240	12 238 69 82 239	syl112anc	|- ( ph -> ( 2 <_ _e <-> ( 2 x. Y ) <_ ( _e x. Y ) ) )
241	237 240	mpbid	|- ( ph -> ( 2 x. Y ) <_ ( _e x. Y ) )
242	216 217 221 232 241	letrd	|- ( ph -> ( ( |_ ` Y ) + 1 ) <_ ( _e x. Y ) )
243	202 220	logled	|- ( ph -> ( ( ( |_ ` Y ) + 1 ) <_ ( _e x. Y ) <-> ( log ` ( ( |_ ` Y ) + 1 ) ) <_ ( log ` ( _e x. Y ) ) ) )
244	242 243	mpbid	|- ( ph -> ( log ` ( ( |_ ` Y ) + 1 ) ) <_ ( log ` ( _e x. Y ) ) )
245		relogmul	|- ( ( _e e. RR+ /\ Y e. RR+ ) -> ( log ` ( _e x. Y ) ) = ( ( log ` _e ) + ( log ` Y ) ) )
246	218 96 245	sylancr	|- ( ph -> ( log ` ( _e x. Y ) ) = ( ( log ` _e ) + ( log ` Y ) ) )
247		loge	|- ( log ` _e ) = 1
248	247	oveq1i	|- ( ( log ` _e ) + ( log ` Y ) ) = ( 1 + ( log ` Y ) )
249	246 248	eqtrdi	|- ( ph -> ( log ` ( _e x. Y ) ) = ( 1 + ( log ` Y ) ) )
250	244 249	breqtrd	|- ( ph -> ( log ` ( ( |_ ` Y ) + 1 ) ) <_ ( 1 + ( log ` Y ) ) )
251	203 214 49 250	leadd2dd	|- ( ph -> ( 1 + ( log ` ( ( |_ ` Y ) + 1 ) ) ) <_ ( 1 + ( 1 + ( log ` Y ) ) ) )
252		df-2	|- 2 = ( 1 + 1 )
253	252	oveq1i	|- ( 2 + ( log ` Y ) ) = ( ( 1 + 1 ) + ( log ` Y ) )
254	142	a1i	|- ( ph -> 1 e. CC )
255	254 254 98	addassd	|- ( ph -> ( ( 1 + 1 ) + ( log ` Y ) ) = ( 1 + ( 1 + ( log ` Y ) ) ) )
256	253 255	eqtrid	|- ( ph -> ( 2 + ( log ` Y ) ) = ( 1 + ( 1 + ( log ` Y ) ) ) )
257	251 256	breqtrrd	|- ( ph -> ( 1 + ( log ` ( ( |_ ` Y ) + 1 ) ) ) <_ ( 2 + ( log ` Y ) ) )
258	201 205 112 212 257	letrd	|- ( ph -> sum_ k e. ( 1 ... ( ( |_ ` Y ) + 1 ) ) ( 1 / k ) <_ ( 2 + ( log ` Y ) ) )
259	200 258	eqbrtrrd	|- ( ph -> sum_ n e. ( 0 ... ( |_ ` Y ) ) ( 1 / ( n + 1 ) ) <_ ( 2 + ( log ` Y ) ) )
260	109 112 93 259	leadd1dd	|- ( ph -> ( sum_ n e. ( 0 ... ( |_ ` Y ) ) ( 1 / ( n + 1 ) ) + sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( 1 / ( n + 1 ) ) ) <_ ( ( 2 + ( log ` Y ) ) + sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( 1 / ( n + 1 ) ) ) )
261	102 110 113 188 260	letrd	|- ( ph -> ( log ` ( K x. Y ) ) <_ ( ( 2 + ( log ` Y ) ) + sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( 1 / ( n + 1 ) ) ) )
262	100 261	eqbrtrrd	|- ( ph -> ( ( log ` K ) + ( log ` Y ) ) <_ ( ( 2 + ( log ` Y ) ) + sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( 1 / ( n + 1 ) ) ) )
263	101 112 93	lesubadd2d	|- ( ph -> ( ( ( ( log ` K ) + ( log ` Y ) ) - ( 2 + ( log ` Y ) ) ) <_ sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( 1 / ( n + 1 ) ) <-> ( ( log ` K ) + ( log ` Y ) ) <_ ( ( 2 + ( log ` Y ) ) + sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( 1 / ( n + 1 ) ) ) ) )
264	262 263	mpbird	|- ( ph -> ( ( ( log ` K ) + ( log ` Y ) ) - ( 2 + ( log ` Y ) ) ) <_ sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( 1 / ( n + 1 ) ) )
265	99 264	eqbrtrrd	|- ( ph -> ( ( log ` K ) - 2 ) <_ sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( 1 / ( n + 1 ) ) )
266	92	recnd	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( 1 / ( n + 1 ) ) e. CC )
267	67 32 266	fsummulc2	|- ( ph -> ( E x. sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( 1 / ( n + 1 ) ) ) = sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( E x. ( 1 / ( n + 1 ) ) ) )
268	14	adantr	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> E e. RR )
269	268	recnd	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> E e. CC )
270	91	nncnd	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( n + 1 ) e. CC )
271	91	nnne0d	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( n + 1 ) =/= 0 )
272	269 270 271	divrecd	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( E / ( n + 1 ) ) = ( E x. ( 1 / ( n + 1 ) ) ) )
273	268 91	nndivred	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( E / ( n + 1 ) ) e. RR )
274	272 273	eqeltrrd	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( E x. ( 1 / ( n + 1 ) ) ) e. RR )
275	67 274	fsumrecl	|- ( ph -> sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( E x. ( 1 / ( n + 1 ) ) ) e. RR )
276	90	nnrpd	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> n e. RR+ )
277	1	pntrf	|- R : RR+ --> RR
278	277	ffvelrni	|- ( n e. RR+ -> ( R ` n ) e. RR )
279	276 278	syl	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( R ` n ) e. RR )
280	90 91	nnmulcld	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( n x. ( n + 1 ) ) e. NN )
281	279 280	nndivred	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. RR )
282	281	recnd	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. CC )
283	282	abscld	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) e. RR )
284	67 283	fsumrecl	|- ( ph -> sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) e. RR )
285	279 90	nndivred	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( R ` n ) / n ) e. RR )
286	285	recnd	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( R ` n ) / n ) e. CC )
287	286	abscld	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( abs ` ( ( R ` n ) / n ) ) e. RR )
288	91	nnrpd	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( n + 1 ) e. RR+ )
289	9	adantr	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> -. E. y e. NN ( ( Y < y /\ y <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` y ) / y ) ) <_ E ) )
290		elfzle1	|- ( n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) -> ( ( |_ ` Y ) + 1 ) <_ n )
291	290	adantl	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( |_ ` Y ) + 1 ) <_ n )
292	69	adantr	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> Y e. RR )
293	292	flcld	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( |_ ` Y ) e. ZZ )
294	90	nnzd	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> n e. ZZ )
295		zltp1le	|- ( ( ( |_ ` Y ) e. ZZ /\ n e. ZZ ) -> ( ( |_ ` Y ) < n <-> ( ( |_ ` Y ) + 1 ) <_ n ) )
296	293 294 295	syl2anc	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( |_ ` Y ) < n <-> ( ( |_ ` Y ) + 1 ) <_ n ) )
297	291 296	mpbird	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( |_ ` Y ) < n )
298		fllt	|- ( ( Y e. RR /\ n e. ZZ ) -> ( Y < n <-> ( |_ ` Y ) < n ) )
299	292 294 298	syl2anc	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( Y < n <-> ( |_ ` Y ) < n ) )
300	297 299	mpbird	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> Y < n )
301		elfzle2	|- ( n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) -> n <_ ( |_ ` ( K x. Y ) ) )
302	301	adantl	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> n <_ ( |_ ` ( K x. Y ) ) )
303	114	adantr	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( K x. Y ) e. RR )
304		flge	|- ( ( ( K x. Y ) e. RR /\ n e. ZZ ) -> ( n <_ ( K x. Y ) <-> n <_ ( |_ ` ( K x. Y ) ) ) )
305	303 294 304	syl2anc	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( n <_ ( K x. Y ) <-> n <_ ( |_ ` ( K x. Y ) ) ) )
306	302 305	mpbird	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> n <_ ( K x. Y ) )
307		breq2	|- ( y = n -> ( Y < y <-> Y < n ) )
308		breq1	|- ( y = n -> ( y <_ ( K x. Y ) <-> n <_ ( K x. Y ) ) )
309	307 308	anbi12d	|- ( y = n -> ( ( Y < y /\ y <_ ( K x. Y ) ) <-> ( Y < n /\ n <_ ( K x. Y ) ) ) )
310		fveq2	|- ( y = n -> ( R ` y ) = ( R ` n ) )
311		id	|- ( y = n -> y = n )
312	310 311	oveq12d	|- ( y = n -> ( ( R ` y ) / y ) = ( ( R ` n ) / n ) )
313	312	fveq2d	|- ( y = n -> ( abs ` ( ( R ` y ) / y ) ) = ( abs ` ( ( R ` n ) / n ) ) )
314	313	breq1d	|- ( y = n -> ( ( abs ` ( ( R ` y ) / y ) ) <_ E <-> ( abs ` ( ( R ` n ) / n ) ) <_ E ) )
315	309 314	anbi12d	|- ( y = n -> ( ( ( Y < y /\ y <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` y ) / y ) ) <_ E ) <-> ( ( Y < n /\ n <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ E ) ) )
316	315	rspcev	|- ( ( n e. NN /\ ( ( Y < n /\ n <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ E ) ) -> E. y e. NN ( ( Y < y /\ y <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` y ) / y ) ) <_ E ) )
317	316	expr	|- ( ( n e. NN /\ ( Y < n /\ n <_ ( K x. Y ) ) ) -> ( ( abs ` ( ( R ` n ) / n ) ) <_ E -> E. y e. NN ( ( Y < y /\ y <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` y ) / y ) ) <_ E ) ) )
318	90 300 306 317	syl12anc	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( abs ` ( ( R ` n ) / n ) ) <_ E -> E. y e. NN ( ( Y < y /\ y <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` y ) / y ) ) <_ E ) ) )
319	289 318	mtod	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> -. ( abs ` ( ( R ` n ) / n ) ) <_ E )
320	287 268	letrid	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( abs ` ( ( R ` n ) / n ) ) <_ E \/ E <_ ( abs ` ( ( R ` n ) / n ) ) ) )
321	320	ord	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( -. ( abs ` ( ( R ` n ) / n ) ) <_ E -> E <_ ( abs ` ( ( R ` n ) / n ) ) ) )
322	319 321	mpd	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> E <_ ( abs ` ( ( R ` n ) / n ) ) )
323	268 287 288 322	lediv1dd	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( E / ( n + 1 ) ) <_ ( ( abs ` ( ( R ` n ) / n ) ) / ( n + 1 ) ) )
324	286 270 271	absdivd	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( abs ` ( ( ( R ` n ) / n ) / ( n + 1 ) ) ) = ( ( abs ` ( ( R ` n ) / n ) ) / ( abs ` ( n + 1 ) ) ) )
325	279	recnd	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( R ` n ) e. CC )
326	90	nncnd	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> n e. CC )
327	90	nnne0d	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> n =/= 0 )
328	325 326 270 327 271	divdiv1d	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( ( R ` n ) / n ) / ( n + 1 ) ) = ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
329	328	fveq2d	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( abs ` ( ( ( R ` n ) / n ) / ( n + 1 ) ) ) = ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
330	288	rprege0d	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( n + 1 ) e. RR /\ 0 <_ ( n + 1 ) ) )
331		absid	|- ( ( ( n + 1 ) e. RR /\ 0 <_ ( n + 1 ) ) -> ( abs ` ( n + 1 ) ) = ( n + 1 ) )
332	330 331	syl	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( abs ` ( n + 1 ) ) = ( n + 1 ) )
333	332	oveq2d	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( abs ` ( ( R ` n ) / n ) ) / ( abs ` ( n + 1 ) ) ) = ( ( abs ` ( ( R ` n ) / n ) ) / ( n + 1 ) ) )
334	324 329 333	3eqtr3rd	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( abs ` ( ( R ` n ) / n ) ) / ( n + 1 ) ) = ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
335	323 272 334	3brtr3d	|- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( E x. ( 1 / ( n + 1 ) ) ) <_ ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
336	67 274 283 335	fsumle	|- ( ph -> sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( E x. ( 1 / ( n + 1 ) ) ) <_ sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
337	1 2 3 4 5 6 7 8 9	pntpbnd1	|- ( ph -> sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ A )
338	275 284 38 336 337	letrd	|- ( ph -> sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( E x. ( 1 / ( n + 1 ) ) ) <_ A )
339	267 338	eqbrtrd	|- ( ph -> ( E x. sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( 1 / ( n + 1 ) ) ) <_ A )
340	93 38 18	lemuldiv2d	|- ( ph -> ( ( E x. sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( 1 / ( n + 1 ) ) ) <_ A <-> sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( 1 / ( n + 1 ) ) <_ ( A / E ) ) )
341	339 340	mpbid	|- ( ph -> sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( 1 / ( n + 1 ) ) <_ ( A / E ) )
342	60 93 39 265 341	letrd	|- ( ph -> ( ( log ` K ) - 2 ) <_ ( A / E ) )
343	41 60 39 66 342	letrd	|- ( ph -> ( ( C / E ) - 2 ) <_ ( A / E ) )
344	37 12 39 343	subled	|- ( ph -> ( ( C / E ) - ( A / E ) ) <_ 2 )
345	35 344	eqbrtrd	|- ( ph -> ( 2 / E ) <_ 2 )
346	12 18 20 345	lediv23d	|- ( ph -> ( 2 / 2 ) <_ E )
347	10 346	eqbrtrrid	|- ( ph -> 1 <_ E )
348	16	simprd	|- ( ph -> E < 1 )
349		ltnle	|- ( ( E e. RR /\ 1 e. RR ) -> ( E < 1 <-> -. 1 <_ E ) )
350	14 48 349	sylancl	|- ( ph -> ( E < 1 <-> -. 1 <_ E ) )
351	348 350	mpbid	|- ( ph -> -. 1 <_ E )
352	347 351	pm2.65i	|- -. ph