Theorem pntibndlem2 21238

Description: Lemma for pntibnd 21240. The main work, after eliminating all the quantifiers. (Contributed by Mario Carneiro, 10-Apr-2016.)

Hypotheses

Ref	Expression
pntibnd.r	|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )
pntibndlem1.1	|- ( ph -> A e. RR+ )
pntibndlem1.l	|- L = ( ( 1 / 4 ) / ( A + 3 ) )
pntibndlem3.2	|- ( ph -> A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A )
pntibndlem3.3	|- ( ph -> B e. RR+ )
pntibndlem3.k	|- K = ( exp ` ( B / ( E / 2 ) ) )
pntibndlem3.c	|- C = ( ( 2 x. B ) + ( log ` 2 ) )
pntibndlem3.4	|- ( ph -> E e. ( 0 (,) 1 ) )
pntibndlem3.6	|- ( ph -> Z e. RR+ )
pntibndlem2.10	|- ( ph -> N e. NN )
pntibndlem2.5	|- ( ph -> T e. RR+ )
pntibndlem2.6	|- ( ph -> A. x e. ( 1 (,) +oo ) A. y e. ( x [,] ( 2 x. x ) ) ( (ψ ` y ) - (ψ ` x ) ) <_ ( ( 2 x. ( y - x ) ) + ( T x. ( x / ( log ` x ) ) ) ) )
pntibndlem2.7	|- X = ( ( exp ` ( T / ( E / 4 ) ) ) + Z )
pntibndlem2.8	|- ( ph -> M e. ( ( exp ` ( C / E ) ) [,) +oo ) )
pntibndlem2.9	|- ( ph -> Y e. ( X (,) +oo ) )
pntibndlem2.11	|- ( ph -> ( ( Y < N /\ N <_ ( ( M / 2 ) x. Y ) ) /\ ( abs ` ( ( R ` N ) / N ) ) <_ ( E / 2 ) ) )

Assertion

Ref	Expression
pntibndlem2	|- ( ph -> E. z e. RR+ ( ( Y < z /\ ( ( 1 + ( L x. E ) ) x. z ) < ( M x. Y ) ) /\ A. u e. ( z [,] ( ( 1 + ( L x. E ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) )

Distinct variable groups:   u, a, x, y, z, E   u, L, x, z   N, a, u, x, y, z   u, A, x   u, C, x, y   u, R, x, y, z   z, M   x, T, y   z, Y   u, Z, x, y   ph, u

Allowed substitution hints:   ph( x, y, z, a)   A( y, z, a)   B( x, y, z, u, a)   C( z, a)   R( a)   T( z, u, a)   K( x, y, z, u, a)   L( y, a)   M( x, y, u, a)   X( x, y, z, u, a)   Y( x, y, u, a)   Z( z, a)

Proof of Theorem pntibndlem2

Step	Hyp	Ref	Expression
1		pntibndlem2.10	. . 3 |- ( ph -> N e. NN )
2	1	nnrpd 10603	. 2 |- ( ph -> N e. RR+ )
3		pntibndlem2.11	. . . . 5 |- ( ph -> ( ( Y < N /\ N <_ ( ( M / 2 ) x. Y ) ) /\ ( abs ` ( ( R ` N ) / N ) ) <_ ( E / 2 ) ) )
4	3	simpld 446	. . . 4 |- ( ph -> ( Y < N /\ N <_ ( ( M / 2 ) x. Y ) ) )
5	4	simpld 446	. . 3 |- ( ph -> Y < N )
6		1re 9046	. . . . . . 7 |- 1 e. RR
7	6	a1i 11	. . . . . 6 |- ( ph -> 1 e. RR )
8		ioossre 10928	. . . . . . . 8 |- ( 0 (,) 1 ) C_ RR
9		pntibnd.r	. . . . . . . . 9 |- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )
10		pntibndlem1.1	. . . . . . . . 9 |- ( ph -> A e. RR+ )
11		pntibndlem1.l	. . . . . . . . 9 |- L = ( ( 1 / 4 ) / ( A + 3 ) )
12	9, 10, 11	pntibndlem1 21236	. . . . . . . 8 |- ( ph -> L e. ( 0 (,) 1 ) )
13	8, 12	sseldi 3306	. . . . . . 7 |- ( ph -> L e. RR )
14		pntibndlem3.4	. . . . . . . 8 |- ( ph -> E e. ( 0 (,) 1 ) )
15	8, 14	sseldi 3306	. . . . . . 7 |- ( ph -> E e. RR )
16	13, 15	remulcld 9072	. . . . . 6 |- ( ph -> ( L x. E ) e. RR )
17	7, 16	readdcld 9071	. . . . 5 |- ( ph -> ( 1 + ( L x. E ) ) e. RR )
18	1	nnred 9971	. . . . 5 |- ( ph -> N e. RR )
19	17, 18	remulcld 9072	. . . 4 |- ( ph -> ( ( 1 + ( L x. E ) ) x. N ) e. RR )
20		2re 10025	. . . . 5 |- 2 e. RR
21		remulcl 9031	. . . . 5 |- ( ( 2 e. RR /\ N e. RR ) -> ( 2 x. N ) e. RR )
22	20, 18, 21	sylancr 645	. . . 4 |- ( ph -> ( 2 x. N ) e. RR )
23		pntibndlem3.c	. . . . . . . . . 10 |- C = ( ( 2 x. B ) + ( log ` 2 ) )
24		pntibndlem3.3	. . . . . . . . . . . . 13 |- ( ph -> B e. RR+ )
25	24	rpred 10604	. . . . . . . . . . . 12 |- ( ph -> B e. RR )
26		remulcl 9031	. . . . . . . . . . . 12 |- ( ( 2 e. RR /\ B e. RR ) -> ( 2 x. B ) e. RR )
27	20, 25, 26	sylancr 645	. . . . . . . . . . 11 |- ( ph -> ( 2 x. B ) e. RR )
28		2rp 10573	. . . . . . . . . . . . 13 |- 2 e. RR+
29	28	a1i 11	. . . . . . . . . . . 12 |- ( ph -> 2 e. RR+ )
30	29	relogcld 20471	. . . . . . . . . . 11 |- ( ph -> ( log ` 2 ) e. RR )
31	27, 30	readdcld 9071	. . . . . . . . . 10 |- ( ph -> ( ( 2 x. B ) + ( log ` 2 ) ) e. RR )
32	23, 31	syl5eqel 2488	. . . . . . . . 9 |- ( ph -> C e. RR )
33		eliooord 10926	. . . . . . . . . . . 12 |- ( E e. ( 0 (,) 1 ) -> ( 0 < E /\ E < 1 ) )
34	14, 33	syl 16	. . . . . . . . . . 11 |- ( ph -> ( 0 < E /\ E < 1 ) )
35	34	simpld 446	. . . . . . . . . 10 |- ( ph -> 0 < E )
36	15, 35	elrpd 10602	. . . . . . . . 9 |- ( ph -> E e. RR+ )
37	32, 36	rerpdivcld 10631	. . . . . . . 8 |- ( ph -> ( C / E ) e. RR )
38	37	reefcld 12645	. . . . . . 7 |- ( ph -> ( exp ` ( C / E ) ) e. RR )
39		pnfxr 10669	. . . . . . 7 |- +oo e. RR*
40		icossre 10947	. . . . . . 7 |- ( ( ( exp ` ( C / E ) ) e. RR /\ +oo e. RR* ) -> ( ( exp ` ( C / E ) ) [,) +oo ) C_ RR )
41	38, 39, 40	sylancl 644	. . . . . 6 |- ( ph -> ( ( exp ` ( C / E ) ) [,) +oo ) C_ RR )
42		pntibndlem2.8	. . . . . 6 |- ( ph -> M e. ( ( exp ` ( C / E ) ) [,) +oo ) )
43	41, 42	sseldd 3309	. . . . 5 |- ( ph -> M e. RR )
44		ioossre 10928	. . . . . 6 |- ( X (,) +oo ) C_ RR
45		pntibndlem2.9	. . . . . 6 |- ( ph -> Y e. ( X (,) +oo ) )
46	44, 45	sseldi 3306	. . . . 5 |- ( ph -> Y e. RR )
47	43, 46	remulcld 9072	. . . 4 |- ( ph -> ( M x. Y ) e. RR )
48	20	a1i 11	. . . . 5 |- ( ph -> 2 e. RR )
49		eliooord 10926	. . . . . . . . . . . . 13 |- ( L e. ( 0 (,) 1 ) -> ( 0 < L /\ L < 1 ) )
50	12, 49	syl 16	. . . . . . . . . . . 12 |- ( ph -> ( 0 < L /\ L < 1 ) )
51	50	simpld 446	. . . . . . . . . . 11 |- ( ph -> 0 < L )
52	13, 51	elrpd 10602	. . . . . . . . . 10 |- ( ph -> L e. RR+ )
53	52	rpge0d 10608	. . . . . . . . 9 |- ( ph -> 0 <_ L )
54	50	simprd 450	. . . . . . . . 9 |- ( ph -> L < 1 )
55	36	rpge0d 10608	. . . . . . . . 9 |- ( ph -> 0 <_ E )
56	34	simprd 450	. . . . . . . . 9 |- ( ph -> E < 1 )
57	13, 7, 15, 7, 53, 54, 55, 56	ltmul12ad 9908	. . . . . . . 8 |- ( ph -> ( L x. E ) < ( 1 x. 1 ) )
58		1t1e1 10082	. . . . . . . 8 |- ( 1 x. 1 ) = 1
59	57, 58	syl6breq 4211	. . . . . . 7 |- ( ph -> ( L x. E ) < 1 )
60	16, 7, 7, 59	ltadd2dd 9185	. . . . . 6 |- ( ph -> ( 1 + ( L x. E ) ) < ( 1 + 1 ) )
61		df-2 10014	. . . . . 6 |- 2 = ( 1 + 1 )
62	60, 61	syl6breqr 4212	. . . . 5 |- ( ph -> ( 1 + ( L x. E ) ) < 2 )
63	17, 48, 2, 62	ltmul1dd 10655	. . . 4 |- ( ph -> ( ( 1 + ( L x. E ) ) x. N ) < ( 2 x. N ) )
64	4	simprd 450	. . . . . 6 |- ( ph -> N <_ ( ( M / 2 ) x. Y ) )
65	43	recnd 9070	. . . . . . 7 |- ( ph -> M e. CC )
66	46	recnd 9070	. . . . . . 7 |- ( ph -> Y e. CC )
67		rpcnne0 10585	. . . . . . . 8 |- ( 2 e. RR+ -> ( 2 e. CC /\ 2 =/= 0 ) )
68	28, 67	mp1i 12	. . . . . . 7 |- ( ph -> ( 2 e. CC /\ 2 =/= 0 ) )
69		div23 9653	. . . . . . 7 |- ( ( M e. CC /\ Y e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( M x. Y ) / 2 ) = ( ( M / 2 ) x. Y ) )
70	65, 66, 68, 69	syl3anc 1184	. . . . . 6 |- ( ph -> ( ( M x. Y ) / 2 ) = ( ( M / 2 ) x. Y ) )
71	64, 70	breqtrrd 4198	. . . . 5 |- ( ph -> N <_ ( ( M x. Y ) / 2 ) )
72	18, 47, 29	lemuldiv2d 10650	. . . . 5 |- ( ph -> ( ( 2 x. N ) <_ ( M x. Y ) <-> N <_ ( ( M x. Y ) / 2 ) ) )
73	71, 72	mpbird 224	. . . 4 |- ( ph -> ( 2 x. N ) <_ ( M x. Y ) )
74	19, 22, 47, 63, 73	ltletrd 9186	. . 3 |- ( ph -> ( ( 1 + ( L x. E ) ) x. N ) < ( M x. Y ) )
75		pntibndlem3.2	. . . . . . . . . . . 12 |- ( ph -> A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A )
76		pntibndlem3.k	. . . . . . . . . . . 12 |- K = ( exp ` ( B / ( E / 2 ) ) )
77	9, 10, 11, 75, 24, 76, 23, 14, 10, 1	pntibndlem2a 21237	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( u e. RR /\ N <_ u /\ u <_ ( ( 1 + ( L x. E ) ) x. N ) ) )
78	77	simp1d 969	. . . . . . . . . 10 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> u e. RR )
79	2	adantr 452	. . . . . . . . . 10 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> N e. RR+ )
80	77	simp2d 970	. . . . . . . . . 10 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> N <_ u )
81	78, 79, 80	rpgecld 10639	. . . . . . . . 9 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> u e. RR+ )
82	9	pntrf 21210	. . . . . . . . . 10 |- R : RR+ --> RR
83	82	ffvelrni 5828	. . . . . . . . 9 |- ( u e. RR+ -> ( R ` u ) e. RR )
84	81, 83	syl 16	. . . . . . . 8 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( R ` u ) e. RR )
85	84, 81	rerpdivcld 10631	. . . . . . 7 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( R ` u ) / u ) e. RR )
86	85	recnd 9070	. . . . . 6 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( R ` u ) / u ) e. CC )
87	86	abscld 12193	. . . . 5 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( R ` u ) / u ) ) e. RR )
88	82	ffvelrni 5828	. . . . . . . . . . . 12 |- ( N e. RR+ -> ( R ` N ) e. RR )
89	2, 88	syl 16	. . . . . . . . . . 11 |- ( ph -> ( R ` N ) e. RR )
90	89, 1	nndivred 10004	. . . . . . . . . 10 |- ( ph -> ( ( R ` N ) / N ) e. RR )
91	90	adantr 452	. . . . . . . . 9 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( R ` N ) / N ) e. RR )
92	91	recnd 9070	. . . . . . . 8 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( R ` N ) / N ) e. CC )
93	86, 92	subcld 9367	. . . . . . 7 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) e. CC )
94	93	abscld 12193	. . . . . 6 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) ) e. RR )
95	92	abscld 12193	. . . . . 6 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( R ` N ) / N ) ) e. RR )
96	94, 95	readdcld 9071	. . . . 5 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) ) + ( abs ` ( ( R ` N ) / N ) ) ) e. RR )
97	15	adantr 452	. . . . 5 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> E e. RR )
98	86, 92	abs2difd 12214	. . . . . 6 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` ( ( R ` u ) / u ) ) - ( abs ` ( ( R ` N ) / N ) ) ) <_ ( abs ` ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) ) )
99	87, 95, 94	lesubaddd 9579	. . . . . 6 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( abs ` ( ( R ` u ) / u ) ) - ( abs ` ( ( R ` N ) / N ) ) ) <_ ( abs ` ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) ) <-> ( abs ` ( ( R ` u ) / u ) ) <_ ( ( abs ` ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) ) + ( abs ` ( ( R ` N ) / N ) ) ) ) )
100	98, 99	mpbid 202	. . . . 5 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( R ` u ) / u ) ) <_ ( ( abs ` ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) ) + ( abs ` ( ( R ` N ) / N ) ) ) )
101	97	rehalfcld 10170	. . . . . . 7 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( E / 2 ) e. RR )
102	18	adantr 452	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> N e. RR )
103	78, 102	resubcld 9421	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( u - N ) e. RR )
104	103, 79	rerpdivcld 10631	. . . . . . . . . 10 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( u - N ) / N ) e. RR )
105		3re 10027	. . . . . . . . . . . 12 |- 3 e. RR
106	105	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> 3 e. RR )
107	87, 106	readdcld 9071	. . . . . . . . . 10 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) e. RR )
108	104, 107	remulcld 9072	. . . . . . . . 9 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) ) e. RR )
109		pntibndlem2.5	. . . . . . . . . . . 12 |- ( ph -> T e. RR+ )
110	109	rpred 10604	. . . . . . . . . . 11 |- ( ph -> T e. RR )
111	110	adantr 452	. . . . . . . . . 10 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> T e. RR )
112	6	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> 1 e. RR )
113		4nn 10091	. . . . . . . . . . . . . . . . . 18 |- 4 e. NN
114		nnrp 10577	. . . . . . . . . . . . . . . . . 18 |- ( 4 e. NN -> 4 e. RR+ )
115	113, 114	mp1i 12	. . . . . . . . . . . . . . . . 17 |- ( ph -> 4 e. RR+ )
116	36, 115	rpdivcld 10621	. . . . . . . . . . . . . . . 16 |- ( ph -> ( E / 4 ) e. RR+ )
117	109, 116	rpdivcld 10621	. . . . . . . . . . . . . . 15 |- ( ph -> ( T / ( E / 4 ) ) e. RR+ )
118	117	rpred 10604	. . . . . . . . . . . . . 14 |- ( ph -> ( T / ( E / 4 ) ) e. RR )
119	118	reefcld 12645	. . . . . . . . . . . . 13 |- ( ph -> ( exp ` ( T / ( E / 4 ) ) ) e. RR )
120	119	adantr 452	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( exp ` ( T / ( E / 4 ) ) ) e. RR )
121		efgt1 12672	. . . . . . . . . . . . . 14 |- ( ( T / ( E / 4 ) ) e. RR+ -> 1 < ( exp ` ( T / ( E / 4 ) ) ) )
122	117, 121	syl 16	. . . . . . . . . . . . 13 |- ( ph -> 1 < ( exp ` ( T / ( E / 4 ) ) ) )
123	122	adantr 452	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> 1 < ( exp ` ( T / ( E / 4 ) ) ) )
124		pntibndlem2.7	. . . . . . . . . . . . . . . 16 |- X = ( ( exp ` ( T / ( E / 4 ) ) ) + Z )
125		pntibndlem3.6	. . . . . . . . . . . . . . . . . 18 |- ( ph -> Z e. RR+ )
126	125	rpred 10604	. . . . . . . . . . . . . . . . 17 |- ( ph -> Z e. RR )
127	119, 126	readdcld 9071	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( exp ` ( T / ( E / 4 ) ) ) + Z ) e. RR )
128	124, 127	syl5eqel 2488	. . . . . . . . . . . . . . 15 |- ( ph -> X e. RR )
129	119, 125	ltaddrpd 10633	. . . . . . . . . . . . . . . 16 |- ( ph -> ( exp ` ( T / ( E / 4 ) ) ) < ( ( exp ` ( T / ( E / 4 ) ) ) + Z ) )
130	129, 124	syl6breqr 4212	. . . . . . . . . . . . . . 15 |- ( ph -> ( exp ` ( T / ( E / 4 ) ) ) < X )
131		eliooord 10926	. . . . . . . . . . . . . . . . 17 |- ( Y e. ( X (,) +oo ) -> ( X < Y /\ Y < +oo ) )
132	45, 131	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> ( X < Y /\ Y < +oo ) )
133	132	simpld 446	. . . . . . . . . . . . . . 15 |- ( ph -> X < Y )
134	119, 128, 46, 130, 133	lttrd 9187	. . . . . . . . . . . . . 14 |- ( ph -> ( exp ` ( T / ( E / 4 ) ) ) < Y )
135	119, 46, 18, 134, 5	lttrd 9187	. . . . . . . . . . . . 13 |- ( ph -> ( exp ` ( T / ( E / 4 ) ) ) < N )
136	135	adantr 452	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( exp ` ( T / ( E / 4 ) ) ) < N )
137	112, 120, 102, 123, 136	lttrd 9187	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> 1 < N )
138	102, 137	rplogcld 20477	. . . . . . . . . 10 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( log ` N ) e. RR+ )
139	111, 138	rerpdivcld 10631	. . . . . . . . 9 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( T / ( log ` N ) ) e. RR )
140	108, 139	readdcld 9071	. . . . . . . 8 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) ) + ( T / ( log ` N ) ) ) e. RR )
141		peano2re 9195	. . . . . . . . . . . 12 |- ( ( abs ` ( ( R ` u ) / u ) ) e. RR -> ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) e. RR )
142	87, 141	syl 16	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) e. RR )
143	104, 142	remulcld 9072	. . . . . . . . . 10 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) e. RR )
144		chpcl 20860	. . . . . . . . . . . . 13 |- ( u e. RR -> (ψ ` u ) e. RR )
145	78, 144	syl 16	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> (ψ ` u ) e. RR )
146		chpcl 20860	. . . . . . . . . . . . 13 |- ( N e. RR -> (ψ ` N ) e. RR )
147	102, 146	syl 16	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> (ψ ` N ) e. RR )
148	145, 147	resubcld 9421	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( (ψ ` u ) - (ψ ` N ) ) e. RR )
149	148, 79	rerpdivcld 10631	. . . . . . . . . 10 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( (ψ ` u ) - (ψ ` N ) ) / N ) e. RR )
150	143, 149	readdcld 9071	. . . . . . . . 9 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( ( (ψ ` u ) - (ψ ` N ) ) / N ) ) e. RR )
151	104, 87	remulcld 9072	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) e. RR )
152	89	adantr 452	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( R ` N ) e. RR )
153	84, 152	resubcld 9421	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( R ` u ) - ( R ` N ) ) e. RR )
154	153	recnd 9070	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( R ` u ) - ( R ` N ) ) e. CC )
155	154	abscld 12193	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( R ` u ) - ( R ` N ) ) ) e. RR )
156	155, 79	rerpdivcld 10631	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` ( ( R ` u ) - ( R ` N ) ) ) / N ) e. RR )
157	151, 156	readdcld 9071	. . . . . . . . . 10 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( abs ` ( ( R ` u ) - ( R ` N ) ) ) / N ) ) e. RR )
158	104, 85	remulcld 9072	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) e. RR )
159	158	renegcld 9420	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> -u ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) e. RR )
160	159	recnd 9070	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> -u ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) e. CC )
161	153, 79	rerpdivcld 10631	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( R ` u ) - ( R ` N ) ) / N ) e. RR )
162	161	recnd 9070	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( R ` u ) - ( R ` N ) ) / N ) e. CC )
163	160, 162	abstrid 12213	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( -u ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) + ( ( ( R ` u ) - ( R ` N ) ) / N ) ) ) <_ ( ( abs ` -u ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) ) + ( abs ` ( ( ( R ` u ) - ( R ` N ) ) / N ) ) ) )
164	78	recnd 9070	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> u e. CC )
165	102	recnd 9070	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> N e. CC )
166	79	rpne0d 10609	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> N =/= 0 )
167	164, 165, 165, 166	divsubdird 9785	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( u - N ) / N ) = ( ( u / N ) - ( N / N ) ) )
168	165, 166	dividd 9744	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( N / N ) = 1 )
169	168	oveq2d 6056	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( u / N ) - ( N / N ) ) = ( ( u / N ) - 1 ) )
170	167, 169	eqtrd 2436	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( u - N ) / N ) = ( ( u / N ) - 1 ) )
171	170	oveq1d 6055	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) = ( ( ( u / N ) - 1 ) x. ( ( R ` u ) / u ) ) )
172	78, 79	rerpdivcld 10631	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( u / N ) e. RR )
173	172	recnd 9070	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( u / N ) e. CC )
174		ax-1cn 9004	. . . . . . . . . . . . . . . . . . 19 |- 1 e. CC
175	174	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> 1 e. CC )
176	173, 175, 86	subdird 9446	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u / N ) - 1 ) x. ( ( R ` u ) / u ) ) = ( ( ( u / N ) x. ( ( R ` u ) / u ) ) - ( 1 x. ( ( R ` u ) / u ) ) ) )
177	81	rpcnne0d 10613	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( u e. CC /\ u =/= 0 ) )
178	79	rpcnne0d 10613	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( N e. CC /\ N =/= 0 ) )
179	84	recnd 9070	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( R ` u ) e. CC )
180		dmdcan 9680	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( u e. CC /\ u =/= 0 ) /\ ( N e. CC /\ N =/= 0 ) /\ ( R ` u ) e. CC ) -> ( ( u / N ) x. ( ( R ` u ) / u ) ) = ( ( R ` u ) / N ) )
181	177, 178, 179, 180	syl3anc 1184	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( u / N ) x. ( ( R ` u ) / u ) ) = ( ( R ` u ) / N ) )
182	86	mulid2d 9062	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( 1 x. ( ( R ` u ) / u ) ) = ( ( R ` u ) / u ) )
183	181, 182	oveq12d 6058	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u / N ) x. ( ( R ` u ) / u ) ) - ( 1 x. ( ( R ` u ) / u ) ) ) = ( ( ( R ` u ) / N ) - ( ( R ` u ) / u ) ) )
184	171, 176, 183	3eqtrd 2440	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) = ( ( ( R ` u ) / N ) - ( ( R ` u ) / u ) ) )
185	184	negeqd 9256	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> -u ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) = -u ( ( ( R ` u ) / N ) - ( ( R ` u ) / u ) ) )
186	84, 79	rerpdivcld 10631	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( R ` u ) / N ) e. RR )
187	186	recnd 9070	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( R ` u ) / N ) e. CC )
188	187, 86	negsubdi2d 9383	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> -u ( ( ( R ` u ) / N ) - ( ( R ` u ) / u ) ) = ( ( ( R ` u ) / u ) - ( ( R ` u ) / N ) ) )
189	185, 188	eqtrd 2436	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> -u ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) = ( ( ( R ` u ) / u ) - ( ( R ` u ) / N ) ) )
190	152	recnd 9070	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( R ` N ) e. CC )
191	179, 190, 165, 166	divsubdird 9785	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( R ` u ) - ( R ` N ) ) / N ) = ( ( ( R ` u ) / N ) - ( ( R ` N ) / N ) ) )
192	189, 191	oveq12d 6058	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( -u ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) + ( ( ( R ` u ) - ( R ` N ) ) / N ) ) = ( ( ( ( R ` u ) / u ) - ( ( R ` u ) / N ) ) + ( ( ( R ` u ) / N ) - ( ( R ` N ) / N ) ) ) )
193	86, 187, 92	npncand 9391	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( R ` u ) / u ) - ( ( R ` u ) / N ) ) + ( ( ( R ` u ) / N ) - ( ( R ` N ) / N ) ) ) = ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) )
194	192, 193	eqtrd 2436	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( -u ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) + ( ( ( R ` u ) - ( R ` N ) ) / N ) ) = ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) )
195	194	fveq2d 5691	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( -u ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) + ( ( ( R ` u ) - ( R ` N ) ) / N ) ) ) = ( abs ` ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) ) )
196	158	recnd 9070	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) e. CC )
197	196	absnegd 12206	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` -u ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) ) = ( abs ` ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) ) )
198	104	recnd 9070	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( u - N ) / N ) e. CC )
199	198, 86	absmuld 12211	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) ) = ( ( abs ` ( ( u - N ) / N ) ) x. ( abs ` ( ( R ` u ) / u ) ) ) )
200	78, 102	subge0d 9572	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( 0 <_ ( u - N ) <-> N <_ u ) )
201	80, 200	mpbird 224	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> 0 <_ ( u - N ) )
202	103, 79, 201	divge0d 10640	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> 0 <_ ( ( u - N ) / N ) )
203	104, 202	absidd 12180	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( u - N ) / N ) ) = ( ( u - N ) / N ) )
204	203	oveq1d 6055	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` ( ( u - N ) / N ) ) x. ( abs ` ( ( R ` u ) / u ) ) ) = ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) )
205	197, 199, 204	3eqtrd 2440	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` -u ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) ) = ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) )
206	154, 165, 166	absdivd 12212	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( ( R ` u ) - ( R ` N ) ) / N ) ) = ( ( abs ` ( ( R ` u ) - ( R ` N ) ) ) / ( abs ` N ) ) )
207	79	rprege0d 10611	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( N e. RR /\ 0 <_ N ) )
208		absid 12056	. . . . . . . . . . . . . . 15 |- ( ( N e. RR /\ 0 <_ N ) -> ( abs ` N ) = N )
209	207, 208	syl 16	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` N ) = N )
210	209	oveq2d 6056	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` ( ( R ` u ) - ( R ` N ) ) ) / ( abs ` N ) ) = ( ( abs ` ( ( R ` u ) - ( R ` N ) ) ) / N ) )
211	206, 210	eqtrd 2436	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( ( R ` u ) - ( R ` N ) ) / N ) ) = ( ( abs ` ( ( R ` u ) - ( R ` N ) ) ) / N ) )
212	205, 211	oveq12d 6058	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` -u ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) ) + ( abs ` ( ( ( R ` u ) - ( R ` N ) ) / N ) ) ) = ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( abs ` ( ( R ` u ) - ( R ` N ) ) ) / N ) ) )
213	163, 195, 212	3brtr3d 4201	. . . . . . . . . 10 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) ) <_ ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( abs ` ( ( R ` u ) - ( R ` N ) ) ) / N ) ) )
214	103, 148	readdcld 9071	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( u - N ) + ( (ψ ` u ) - (ψ ` N ) ) ) e. RR )
215	214, 79	rerpdivcld 10631	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) + ( (ψ ` u ) - (ψ ` N ) ) ) / N ) e. RR )
216	148	recnd 9070	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( (ψ ` u ) - (ψ ` N ) ) e. CC )
217	165, 164	subcld 9367	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( N - u ) e. CC )
218	216, 217	abstrid 12213	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( (ψ ` u ) - (ψ ` N ) ) + ( N - u ) ) ) <_ ( ( abs ` ( (ψ ` u ) - (ψ ` N ) ) ) + ( abs ` ( N - u ) ) ) )
219	9	pntrval 21209	. . . . . . . . . . . . . . . . . 18 |- ( u e. RR+ -> ( R ` u ) = ( (ψ ` u ) - u ) )
220	81, 219	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( R ` u ) = ( (ψ ` u ) - u ) )
221	9	pntrval 21209	. . . . . . . . . . . . . . . . . 18 |- ( N e. RR+ -> ( R ` N ) = ( (ψ ` N ) - N ) )
222	79, 221	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( R ` N ) = ( (ψ ` N ) - N ) )
223	220, 222	oveq12d 6058	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( R ` u ) - ( R ` N ) ) = ( ( (ψ ` u ) - u ) - ( (ψ ` N ) - N ) ) )
224	145	recnd 9070	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> (ψ ` u ) e. CC )
225	147	recnd 9070	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> (ψ ` N ) e. CC )
226		subadd4 9301	. . . . . . . . . . . . . . . . . 18 |- ( ( ( (ψ ` u ) e. CC /\ (ψ ` N ) e. CC ) /\ ( u e. CC /\ N e. CC ) ) -> ( ( (ψ ` u ) - (ψ ` N ) ) - ( u - N ) ) = ( ( (ψ ` u ) + N ) - ( (ψ ` N ) + u ) ) )
227		sub4 9302	. . . . . . . . . . . . . . . . . 18 |- ( ( ( (ψ ` u ) e. CC /\ (ψ ` N ) e. CC ) /\ ( u e. CC /\ N e. CC ) ) -> ( ( (ψ ` u ) - (ψ ` N ) ) - ( u - N ) ) = ( ( (ψ ` u ) - u ) - ( (ψ ` N ) - N ) ) )
228		addsub4 9300	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( (ψ ` u ) e. CC /\ N e. CC ) /\ ( (ψ ` N ) e. CC /\ u e. CC ) ) -> ( ( (ψ ` u ) + N ) - ( (ψ ` N ) + u ) ) = ( ( (ψ ` u ) - (ψ ` N ) ) + ( N - u ) ) )
229	228	an42s 801	. . . . . . . . . . . . . . . . . 18 |- ( ( ( (ψ ` u ) e. CC /\ (ψ ` N ) e. CC ) /\ ( u e. CC /\ N e. CC ) ) -> ( ( (ψ ` u ) + N ) - ( (ψ ` N ) + u ) ) = ( ( (ψ ` u ) - (ψ ` N ) ) + ( N - u ) ) )
230	226, 227, 229	3eqtr3d 2444	. . . . . . . . . . . . . . . . 17 |- ( ( ( (ψ ` u ) e. CC /\ (ψ ` N ) e. CC ) /\ ( u e. CC /\ N e. CC ) ) -> ( ( (ψ ` u ) - u ) - ( (ψ ` N ) - N ) ) = ( ( (ψ ` u ) - (ψ ` N ) ) + ( N - u ) ) )
231	224, 225, 164, 165, 230	syl22anc 1185	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( (ψ ` u ) - u ) - ( (ψ ` N ) - N ) ) = ( ( (ψ ` u ) - (ψ ` N ) ) + ( N - u ) ) )
232	223, 231	eqtr2d 2437	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( (ψ ` u ) - (ψ ` N ) ) + ( N - u ) ) = ( ( R ` u ) - ( R ` N ) ) )
233	232	fveq2d 5691	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( (ψ ` u ) - (ψ ` N ) ) + ( N - u ) ) ) = ( abs ` ( ( R ` u ) - ( R ` N ) ) ) )
234		chpwordi 20893	. . . . . . . . . . . . . . . . . 18 |- ( ( N e. RR /\ u e. RR /\ N <_ u ) -> (ψ ` N ) <_ (ψ ` u ) )
235	102, 78, 80, 234	syl3anc 1184	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> (ψ ` N ) <_ (ψ ` u ) )
236	147, 145, 235	abssubge0d 12189	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( (ψ ` u ) - (ψ ` N ) ) ) = ( (ψ ` u ) - (ψ ` N ) ) )
237	102, 78, 80	abssuble0d 12190	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( N - u ) ) = ( u - N ) )
238	236, 237	oveq12d 6058	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` ( (ψ ` u ) - (ψ ` N ) ) ) + ( abs ` ( N - u ) ) ) = ( ( (ψ ` u ) - (ψ ` N ) ) + ( u - N ) ) )
239	103	recnd 9070	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( u - N ) e. CC )
240	216, 239	addcomd 9224	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( (ψ ` u ) - (ψ ` N ) ) + ( u - N ) ) = ( ( u - N ) + ( (ψ ` u ) - (ψ ` N ) ) ) )
241	238, 240	eqtrd 2436	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` ( (ψ ` u ) - (ψ ` N ) ) ) + ( abs ` ( N - u ) ) ) = ( ( u - N ) + ( (ψ ` u ) - (ψ ` N ) ) ) )
242	218, 233, 241	3brtr3d 4201	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( R ` u ) - ( R ` N ) ) ) <_ ( ( u - N ) + ( (ψ ` u ) - (ψ ` N ) ) ) )
243	155, 214, 79, 242	lediv1dd 10658	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` ( ( R ` u ) - ( R ` N ) ) ) / N ) <_ ( ( ( u - N ) + ( (ψ ` u ) - (ψ ` N ) ) ) / N ) )
244	156, 215, 151, 243	leadd2dd 9597	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( abs ` ( ( R ` u ) - ( R ` N ) ) ) / N ) ) <_ ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( ( u - N ) + ( (ψ ` u ) - (ψ ` N ) ) ) / N ) ) )
245	151	recnd 9070	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) e. CC )
246	149	recnd 9070	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( (ψ ` u ) - (ψ ` N ) ) / N ) e. CC )
247	245, 198, 246	addassd 9066	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( u - N ) / N ) ) + ( ( (ψ ` u ) - (ψ ` N ) ) / N ) ) = ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( ( u - N ) / N ) + ( ( (ψ ` u ) - (ψ ` N ) ) / N ) ) ) )
248	87	recnd 9070	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( R ` u ) / u ) ) e. CC )
249	198, 248, 175	adddid 9068	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) = ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( ( u - N ) / N ) x. 1 ) ) )
250	198	mulid1d 9061	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. 1 ) = ( ( u - N ) / N ) )
251	250	oveq2d 6056	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( ( u - N ) / N ) x. 1 ) ) = ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( u - N ) / N ) ) )
252	249, 251	eqtrd 2436	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) = ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( u - N ) / N ) ) )
253	252	oveq1d 6055	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( ( (ψ ` u ) - (ψ ` N ) ) / N ) ) = ( ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( u - N ) / N ) ) + ( ( (ψ ` u ) - (ψ ` N ) ) / N ) ) )
254	239, 216, 165, 166	divdird 9784	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) + ( (ψ ` u ) - (ψ ` N ) ) ) / N ) = ( ( ( u - N ) / N ) + ( ( (ψ ` u ) - (ψ ` N ) ) / N ) ) )
255	254	oveq2d 6056	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( ( u - N ) + ( (ψ ` u ) - (ψ ` N ) ) ) / N ) ) = ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( ( u - N ) / N ) + ( ( (ψ ` u ) - (ψ ` N ) ) / N ) ) ) )
256	247, 253, 255	3eqtr4d 2446	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( ( (ψ ` u ) - (ψ ` N ) ) / N ) ) = ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( ( u - N ) + ( (ψ ` u ) - (ψ ` N ) ) ) / N ) ) )
257	244, 256	breqtrrd 4198	. . . . . . . . . 10 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( abs ` ( ( R ` u ) - ( R ` N ) ) ) / N ) ) <_ ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( ( (ψ ` u ) - (ψ ` N ) ) / N ) ) )
258	94, 157, 150, 213, 257	letrd 9183	. . . . . . . . 9 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) ) <_ ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( ( (ψ ` u ) - (ψ ` N ) ) / N ) ) )
259		remulcl 9031	. . . . . . . . . . . . 13 |- ( ( 2 e. RR /\ ( ( u - N ) / N ) e. RR ) -> ( 2 x. ( ( u - N ) / N ) ) e. RR )
260	20, 104, 259	sylancr 645	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( 2 x. ( ( u - N ) / N ) ) e. RR )
261	260, 139	readdcld 9071	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( 2 x. ( ( u - N ) / N ) ) + ( T / ( log ` N ) ) ) e. RR )
262		remulcl 9031	. . . . . . . . . . . . . . 15 |- ( ( 2 e. RR /\ ( u - N ) e. RR ) -> ( 2 x. ( u - N ) ) e. RR )
263	20, 103, 262	sylancr 645	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( 2 x. ( u - N ) ) e. RR )
264	102, 138	rerpdivcld 10631	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( N / ( log ` N ) ) e. RR )
265	111, 264	remulcld 9072	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( T x. ( N / ( log ` N ) ) ) e. RR )
266	263, 265	readdcld 9071	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( 2 x. ( u - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) e. RR )
267	19	adantr 452	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( 1 + ( L x. E ) ) x. N ) e. RR )
268	22	adantr 452	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( 2 x. N ) e. RR )
269	77	simp3d 971	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> u <_ ( ( 1 + ( L x. E ) ) x. N ) )
270		ltle 9119	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 1 + ( L x. E ) ) e. RR /\ 2 e. RR ) -> ( ( 1 + ( L x. E ) ) < 2 -> ( 1 + ( L x. E ) ) <_ 2 ) )
271	17, 20, 270	sylancl 644	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( 1 + ( L x. E ) ) < 2 -> ( 1 + ( L x. E ) ) <_ 2 ) )
272	62, 271	mpd 15	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( 1 + ( L x. E ) ) <_ 2 )
273	272	adantr 452	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( 1 + ( L x. E ) ) <_ 2 )
274	17	adantr 452	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( 1 + ( L x. E ) ) e. RR )
275	20	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> 2 e. RR )
276	274, 275, 79	lemul1d 10643	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( 1 + ( L x. E ) ) <_ 2 <-> ( ( 1 + ( L x. E ) ) x. N ) <_ ( 2 x. N ) ) )
277	273, 276	mpbid 202	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( 1 + ( L x. E ) ) x. N ) <_ ( 2 x. N ) )
278	78, 267, 268, 269, 277	letrd 9183	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> u <_ ( 2 x. N ) )
279		elicc2 10931	. . . . . . . . . . . . . . . 16 |- ( ( N e. RR /\ ( 2 x. N ) e. RR ) -> ( u e. ( N [,] ( 2 x. N ) ) <-> ( u e. RR /\ N <_ u /\ u <_ ( 2 x. N ) ) ) )
280	102, 268, 279	syl2anc 643	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( u e. ( N [,] ( 2 x. N ) ) <-> ( u e. RR /\ N <_ u /\ u <_ ( 2 x. N ) ) ) )
281	78, 80, 278, 280	mpbir3and 1137	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> u e. ( N [,] ( 2 x. N ) ) )
282	6	rexri 9093	. . . . . . . . . . . . . . . . 17 |- 1 e. RR*
283		elioopnf 10954	. . . . . . . . . . . . . . . . 17 |- ( 1 e. RR* -> ( N e. ( 1 (,) +oo ) <-> ( N e. RR /\ 1 < N ) ) )
284	282, 283	ax-mp 8	. . . . . . . . . . . . . . . 16 |- ( N e. ( 1 (,) +oo ) <-> ( N e. RR /\ 1 < N ) )
285	102, 137, 284	sylanbrc 646	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> N e. ( 1 (,) +oo ) )
286		pntibndlem2.6	. . . . . . . . . . . . . . . 16 |- ( ph -> A. x e. ( 1 (,) +oo ) A. y e. ( x [,] ( 2 x. x ) ) ( (ψ ` y ) - (ψ ` x ) ) <_ ( ( 2 x. ( y - x ) ) + ( T x. ( x / ( log ` x ) ) ) ) )
287	286	adantr 452	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> A. x e. ( 1 (,) +oo ) A. y e. ( x [,] ( 2 x. x ) ) ( (ψ ` y ) - (ψ ` x ) ) <_ ( ( 2 x. ( y - x ) ) + ( T x. ( x / ( log ` x ) ) ) ) )
288		id 20	. . . . . . . . . . . . . . . . . 18 |- ( x = N -> x = N )
289		oveq2 6048	. . . . . . . . . . . . . . . . . 18 |- ( x = N -> ( 2 x. x ) = ( 2 x. N ) )
290	288, 289	oveq12d 6058	. . . . . . . . . . . . . . . . 17 |- ( x = N -> ( x [,] ( 2 x. x ) ) = ( N [,] ( 2 x. N ) ) )
291		fveq2 5687	. . . . . . . . . . . . . . . . . . 19 |- ( x = N -> (ψ ` x ) = (ψ ` N ) )
292	291	oveq2d 6056	. . . . . . . . . . . . . . . . . 18 |- ( x = N -> ( (ψ ` y ) - (ψ ` x ) ) = ( (ψ ` y ) - (ψ ` N ) ) )
293		oveq2 6048	. . . . . . . . . . . . . . . . . . . 20 |- ( x = N -> ( y - x ) = ( y - N ) )
294	293	oveq2d 6056	. . . . . . . . . . . . . . . . . . 19 |- ( x = N -> ( 2 x. ( y - x ) ) = ( 2 x. ( y - N ) ) )
295		fveq2 5687	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = N -> ( log ` x ) = ( log ` N ) )
296	288, 295	oveq12d 6058	. . . . . . . . . . . . . . . . . . . 20 |- ( x = N -> ( x / ( log ` x ) ) = ( N / ( log ` N ) ) )
297	296	oveq2d 6056	. . . . . . . . . . . . . . . . . . 19 |- ( x = N -> ( T x. ( x / ( log ` x ) ) ) = ( T x. ( N / ( log ` N ) ) ) )
298	294, 297	oveq12d 6058	. . . . . . . . . . . . . . . . . 18 |- ( x = N -> ( ( 2 x. ( y - x ) ) + ( T x. ( x / ( log ` x ) ) ) ) = ( ( 2 x. ( y - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) )
299	292, 298	breq12d 4185	. . . . . . . . . . . . . . . . 17 |- ( x = N -> ( ( (ψ ` y ) - (ψ ` x ) ) <_ ( ( 2 x. ( y - x ) ) + ( T x. ( x / ( log ` x ) ) ) ) <-> ( (ψ ` y ) - (ψ ` N ) ) <_ ( ( 2 x. ( y - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) ) )
300	290, 299	raleqbidv 2876	. . . . . . . . . . . . . . . 16 |- ( x = N -> ( A. y e. ( x [,] ( 2 x. x ) ) ( (ψ ` y ) - (ψ ` x ) ) <_ ( ( 2 x. ( y - x ) ) + ( T x. ( x / ( log ` x ) ) ) ) <-> A. y e. ( N [,] ( 2 x. N ) ) ( (ψ ` y ) - (ψ ` N ) ) <_ ( ( 2 x. ( y - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) ) )
301	300	rspcv 3008	. . . . . . . . . . . . . . 15 |- ( N e. ( 1 (,) +oo ) -> ( A. x e. ( 1 (,) +oo ) A. y e. ( x [,] ( 2 x. x ) ) ( (ψ ` y ) - (ψ ` x ) ) <_ ( ( 2 x. ( y - x ) ) + ( T x. ( x / ( log ` x ) ) ) ) -> A. y e. ( N [,] ( 2 x. N ) ) ( (ψ ` y ) - (ψ ` N ) ) <_ ( ( 2 x. ( y - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) ) )
302	285, 287, 301	sylc 58	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> A. y e. ( N [,] ( 2 x. N ) ) ( (ψ ` y ) - (ψ ` N ) ) <_ ( ( 2 x. ( y - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) )
303		fveq2 5687	. . . . . . . . . . . . . . . . 17 |- ( y = u -> (ψ ` y ) = (ψ ` u ) )
304	303	oveq1d 6055	. . . . . . . . . . . . . . . 16 |- ( y = u -> ( (ψ ` y ) - (ψ ` N ) ) = ( (ψ ` u ) - (ψ ` N ) ) )
305		oveq1 6047	. . . . . . . . . . . . . . . . . 18 |- ( y = u -> ( y - N ) = ( u - N ) )
306	305	oveq2d 6056	. . . . . . . . . . . . . . . . 17 |- ( y = u -> ( 2 x. ( y - N ) ) = ( 2 x. ( u - N ) ) )
307	306	oveq1d 6055	. . . . . . . . . . . . . . . 16 |- ( y = u -> ( ( 2 x. ( y - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) = ( ( 2 x. ( u - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) )
308	304, 307	breq12d 4185	. . . . . . . . . . . . . . 15 |- ( y = u -> ( ( (ψ ` y ) - (ψ ` N ) ) <_ ( ( 2 x. ( y - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) <-> ( (ψ ` u ) - (ψ ` N ) ) <_ ( ( 2 x. ( u - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) ) )
309	308	rspcv 3008	. . . . . . . . . . . . . 14 |- ( u e. ( N [,] ( 2 x. N ) ) -> ( A. y e. ( N [,] ( 2 x. N ) ) ( (ψ ` y ) - (ψ ` N ) ) <_ ( ( 2 x. ( y - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) -> ( (ψ ` u ) - (ψ ` N ) ) <_ ( ( 2 x. ( u - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) ) )
310	281, 302, 309	sylc 58	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( (ψ ` u ) - (ψ ` N ) ) <_ ( ( 2 x. ( u - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) )
311	148, 266, 79, 310	lediv1dd 10658	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( (ψ ` u ) - (ψ ` N ) ) / N ) <_ ( ( ( 2 x. ( u - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) / N ) )
312	263	recnd 9070	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( 2 x. ( u - N ) ) e. CC )
313	109	adantr 452	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> T e. RR+ )
314	313	rpred 10604	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> T e. RR )
315	314, 264	remulcld 9072	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( T x. ( N / ( log ` N ) ) ) e. RR )
316	315	recnd 9070	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( T x. ( N / ( log ` N ) ) ) e. CC )
317		divdir 9657	. . . . . . . . . . . . . 14 |- ( ( ( 2 x. ( u - N ) ) e. CC /\ ( T x. ( N / ( log ` N ) ) ) e. CC /\ ( N e. CC /\ N =/= 0 ) ) -> ( ( ( 2 x. ( u - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) / N ) = ( ( ( 2 x. ( u - N ) ) / N ) + ( ( T x. ( N / ( log ` N ) ) ) / N ) ) )
318	312, 316, 178, 317	syl3anc 1184	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( 2 x. ( u - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) / N ) = ( ( ( 2 x. ( u - N ) ) / N ) + ( ( T x. ( N / ( log ` N ) ) ) / N ) ) )
319		2cn 10026	. . . . . . . . . . . . . . . 16 |- 2 e. CC
320	319	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> 2 e. CC )
321	320, 239, 165, 166	divassd 9781	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( 2 x. ( u - N ) ) / N ) = ( 2 x. ( ( u - N ) / N ) ) )
322	111	recnd 9070	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> T e. CC )
323	138	rpcnne0d 10613	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( log ` N ) e. CC /\ ( log ` N ) =/= 0 ) )
324		div12 9656	. . . . . . . . . . . . . . . . 17 |- ( ( T e. CC /\ N e. CC /\ ( ( log ` N ) e. CC /\ ( log ` N ) =/= 0 ) ) -> ( T x. ( N / ( log ` N ) ) ) = ( N x. ( T / ( log ` N ) ) ) )
325	322, 165, 323, 324	syl3anc 1184	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( T x. ( N / ( log ` N ) ) ) = ( N x. ( T / ( log ` N ) ) ) )
326	325	oveq1d 6055	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( T x. ( N / ( log ` N ) ) ) / N ) = ( ( N x. ( T / ( log ` N ) ) ) / N ) )
327	313, 138	rpdivcld 10621	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( T / ( log ` N ) ) e. RR+ )
328	327	rpcnd 10606	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( T / ( log ` N ) ) e. CC )
329	328, 165, 166	divcan3d 9751	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( N x. ( T / ( log ` N ) ) ) / N ) = ( T / ( log ` N ) ) )
330	326, 329	eqtrd 2436	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( T x. ( N / ( log ` N ) ) ) / N ) = ( T / ( log ` N ) ) )
331	321, 330	oveq12d 6058	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( 2 x. ( u - N ) ) / N ) + ( ( T x. ( N / ( log ` N ) ) ) / N ) ) = ( ( 2 x. ( ( u - N ) / N ) ) + ( T / ( log ` N ) ) ) )
332	318, 331	eqtrd 2436	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( 2 x. ( u - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) / N ) = ( ( 2 x. ( ( u - N ) / N ) ) + ( T / ( log ` N ) ) ) )
333	311, 332	breqtrd 4196	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( (ψ ` u ) - (ψ ` N ) ) / N ) <_ ( ( 2 x. ( ( u - N ) / N ) ) + ( T / ( log ` N ) ) ) )
334	149, 261, 143, 333	leadd2dd 9597	. . . . . . . . . 10 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( ( (ψ ` u ) - (ψ ` N ) ) / N ) ) <_ ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( ( 2 x. ( ( u - N ) / N ) ) + ( T / ( log ` N ) ) ) ) )
335	143	recnd 9070	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) e. CC )
336	260	recnd 9070	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( 2 x. ( ( u - N ) / N ) ) e. CC )
337	139	recnd 9070	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( T / ( log ` N ) ) e. CC )
338	335, 336, 337	addassd 9066	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( 2 x. ( ( u - N ) / N ) ) ) + ( T / ( log ` N ) ) ) = ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( ( 2 x. ( ( u - N ) / N ) ) + ( T / ( log ` N ) ) ) ) )
339		mulcom 9032	. . . . . . . . . . . . . . 15 |- ( ( 2 e. CC /\ ( ( u - N ) / N ) e. CC ) -> ( 2 x. ( ( u - N ) / N ) ) = ( ( ( u - N ) / N ) x. 2 ) )
340	319, 198, 339	sylancr 645	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( 2 x. ( ( u - N ) / N ) ) = ( ( ( u - N ) / N ) x. 2 ) )
341	340	oveq2d 6056	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( 2 x. ( ( u - N ) / N ) ) ) = ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( ( ( u - N ) / N ) x. 2 ) ) )
342	142	recnd 9070	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) e. CC )
343	198, 342, 320	adddid 9068	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) + 2 ) ) = ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( ( ( u - N ) / N ) x. 2 ) ) )
344	248, 175, 320	addassd 9066	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) + 2 ) = ( ( abs ` ( ( R ` u ) / u ) ) + ( 1 + 2 ) ) )
345		2p1e3 10059	. . . . . . . . . . . . . . . . 17 |- ( 2 + 1 ) = 3
346	319, 174, 345	addcomli 9214	. . . . . . . . . . . . . . . 16 |- ( 1 + 2 ) = 3
347	346	oveq2i 6051	. . . . . . . . . . . . . . 15 |- ( ( abs ` ( ( R ` u ) / u ) ) + ( 1 + 2 ) ) = ( ( abs ` ( ( R ` u ) / u ) ) + 3 )
348	344, 347	syl6eq 2452	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) + 2 ) = ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) )
349	348	oveq2d 6056	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) + 2 ) ) = ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) ) )
350	341, 343, 349	3eqtr2d 2442	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( 2 x. ( ( u - N ) / N ) ) ) = ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) ) )
351	350	oveq1d 6055	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( 2 x. ( ( u - N ) / N ) ) ) + ( T / ( log ` N ) ) ) = ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) ) + ( T / ( log ` N ) ) ) )
352	338, 351	eqtr3d 2438	. . . . . . . . . 10 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( ( 2 x. ( ( u - N ) / N ) ) + ( T / ( log ` N ) ) ) ) = ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) ) + ( T / ( log ` N ) ) ) )
353	334, 352	breqtrd 4196	. . . . . . . . 9 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( ( (ψ ` u ) - (ψ ` N ) ) / N ) ) <_ ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) ) + ( T / ( log ` N ) ) ) )
354	94, 150, 140, 258, 353	letrd 9183	. . . . . . . 8 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) ) <_ ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) ) + ( T / ( log ` N ) ) ) )
355	101	rehalfcld 10170	. . . . . . . . . 10 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( E / 2 ) / 2 ) e. RR )
356	78, 274, 79	ledivmul2d 10654	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( u / N ) <_ ( 1 + ( L x. E ) ) <-> u <_ ( ( 1 + ( L x. E ) ) x. N ) ) )
357	269, 356	mpbird 224	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( u / N ) <_ ( 1 + ( L x. E ) ) )
358	16	adantr 452	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( L x. E ) e. RR )
359	358	recnd 9070	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( L x. E ) e. CC )
360		addcom 9208	. . . . . . . . . . . . . . . 16 |- ( ( 1 e. CC /\ ( L x. E ) e. CC ) -> ( 1 + ( L x. E ) ) = ( ( L x. E ) + 1 ) )
361	174, 359, 360	sylancr 645	. . . . . . . . . . . . . . 15 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( 1 + ( L x. E ) ) = ( ( L x. E ) + 1 ) )
362	357, 361	breqtrd 4196	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( u / N ) <_ ( ( L x. E ) + 1 ) )
363	172, 112, 358	lesubaddd 9579	. . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u / N ) - 1 ) <_ ( L x. E ) <-> ( u / N ) <_ ( ( L x. E ) + 1 ) ) )
364	362, 363	mpbird 224	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( u / N ) - 1 ) <_ ( L x. E ) )
365	170, 364	eqbrtrd 4192	. . . . . . . . . . . 12