Theorem pntrlog2bndlem5 24498

Description: Lemma for pntrlog2bnd 24501. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)

Hypotheses

Ref	Expression
pntsval.1	|- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) )
pntrlog2bnd.r	|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )
pntrlog2bnd.t	|- T = ( a e. RR |-> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) )
pntrlog2bndlem5.1	|- ( ph -> B e. RR+ )
pntrlog2bndlem5.2	|- ( ph -> A. y e. RR+ ( abs ` ( ( R ` y ) / y ) ) <_ B )

Assertion

Ref	Expression
pntrlog2bndlem5	|- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) ) e. <_O(1) )

Distinct variable groups:   i, a, n, x, y   B, n, x, y   ph, n, x   S, n, x, y   R, n, x, y   T, n

Allowed substitution hints:   ph( y, i, a)   B( i, a)   R( i, a)   S( i, a)   T( x, y, i, a)

Proof of Theorem pntrlog2bndlem5

Step	Hyp	Ref	Expression
1		elioore 11691	. . . . . . . . . . . . 13 |- ( x e. ( 1 (,) +oo ) -> x e. RR )
2	1	adantl 473	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
3		1rp 11329	. . . . . . . . . . . . 13 |- 1 e. RR+
4	3	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ )
5		1red 9676	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR )
6		eliooord 11719	. . . . . . . . . . . . . . 15 |- ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
7	6	adantl 473	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 < x /\ x < +oo ) )
8	7	simpld 466	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 < x )
9	5, 2, 8	ltled 9800	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x )
10	2, 4, 9	rpgecld 11400	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
11		pntrlog2bnd.r	. . . . . . . . . . . . 13 |- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )
12	11	pntrf 24480	. . . . . . . . . . . 12 |- R : RR+ --> RR
13	12	ffvelrni 6036	. . . . . . . . . . 11 |- ( x e. RR+ -> ( R ` x ) e. RR )
14	10, 13	syl 17	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) e. RR )
15	14	recnd 9687	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) e. CC )
16	15	abscld 13575	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` x ) ) e. RR )
17	16	recnd 9687	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` x ) ) e. CC )
18	10	relogcld 23651	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR )
19	18	recnd 9687	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
20	17, 19	mulcld 9681	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) e. CC )
21		2cnd 10704	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 2 e. CC )
22	2, 8	rplogcld 23657	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
23	22	rpne0d 11369	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
24	21, 19, 23	divcld 10405	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 / ( log ` x ) ) e. CC )
25		fzfid 12224	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
26	10	adantr 472	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ )
27		elfznn 11854	. . . . . . . . . . . . . . . 16 |- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
28	27	adantl 473	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
29	28	nnrpd 11362	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
30	26, 29	rpdivcld 11381	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
31	12	ffvelrni 6036	. . . . . . . . . . . . 13 |- ( ( x / n ) e. RR+ -> ( R ` ( x / n ) ) e. RR )
32	30, 31	syl 17	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. RR )
33	32	recnd 9687	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. CC )
34	33	abscld 13575	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / n ) ) ) e. RR )
35	29	relogcld 23651	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. RR )
36		1red 9676	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
37	35, 36	readdcld 9688	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` n ) + 1 ) e. RR )
38	34, 37	remulcld 9689	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) e. RR )
39	38	recnd 9687	. . . . . . . 8 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) e. CC )
40	25, 39	fsumcl 13876	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) e. CC )
41	24, 40	mulcld 9681	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) e. CC )
42	20, 41	subcld 10005	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) e. CC )
43	34	recnd 9687	. . . . . . 7 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / n ) ) ) e. CC )
44	25, 43	fsumcl 13876	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) e. CC )
45	24, 44	mulcld 9681	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) e. CC )
46	2	recnd 9687	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. CC )
47	10	rpne0d 11369	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x =/= 0 )
48	42, 45, 46, 47	divdird 10443	. . . 4 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) ) / x ) = ( ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) / x ) + ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) / x ) ) )
49	16, 18	remulcld 9689	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) e. RR )
50	49	recnd 9687	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) e. CC )
51	50, 41, 45	subsubd 10033	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) ) ) = ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) ) )
52	24, 40, 44	subdid 10095	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) ) = ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) ) )
53	25, 39, 43	fsumsub 13926	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) - ( abs ` ( R ` ( x / n ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) )
54	37	recnd 9687	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` n ) + 1 ) e. CC )
55		1cnd 9677	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. CC )
56	43, 54, 55	subdid 10095	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( log ` n ) + 1 ) - 1 ) ) = ( ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) - ( ( abs ` ( R ` ( x / n ) ) ) x. 1 ) ) )
57	35	recnd 9687	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. CC )
58	57, 55	pncand 10006	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( log ` n ) + 1 ) - 1 ) = ( log ` n ) )
59	58	oveq2d 6324	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( log ` n ) + 1 ) - 1 ) ) = ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) )
60	43	mulid1d 9678	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. 1 ) = ( abs ` ( R ` ( x / n ) ) ) )
61	60	oveq2d 6324	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) - ( ( abs ` ( R ` ( x / n ) ) ) x. 1 ) ) = ( ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) - ( abs ` ( R ` ( x / n ) ) ) ) )
62	56, 59, 61	3eqtr3rd 2514	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) - ( abs ` ( R ` ( x / n ) ) ) ) = ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) )
63	62	sumeq2dv 13846	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) - ( abs ` ( R ` ( x / n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) )
64	53, 63	eqtr3d 2507	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) )
65	64	oveq2d 6324	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) ) = ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) )
66	52, 65	eqtr3d 2507	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) ) = ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) )
67	66	oveq2d 6324	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) ) ) = ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) )
68	51, 67	eqtr3d 2507	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) ) = ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) )
69	68	oveq1d 6323	. . . 4 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) ) / x ) = ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) )
70	48, 69	eqtr3d 2507	. . 3 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) / x ) + ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) / x ) ) = ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) )
71	70	mpteq2dva 4482	. 2 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) / x ) + ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) / x ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) ) )
72		2re 10701	. . . . . . . 8 |- 2 e. RR
73	72	a1i 11	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 2 e. RR )
74	73, 22	rerpdivcld 11392	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 / ( log ` x ) ) e. RR )
75	25, 38	fsumrecl 13877	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) e. RR )
76	74, 75	remulcld 9689	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) e. RR )
77	49, 76	resubcld 10068	. . . 4 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) e. RR )
78	77, 10	rerpdivcld 11392	. . 3 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) / x ) e. RR )
79	25, 34	fsumrecl 13877	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) e. RR )
80	74, 79	remulcld 9689	. . . 4 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) e. RR )
81	80, 10	rerpdivcld 11392	. . 3 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) / x ) e. RR )
82		1red 9676	. . . 4 |- ( ph -> 1 e. RR )
83		pntsval.1	. . . . . 6 |- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) )
84		pntrlog2bnd.t	. . . . . 6 |- T = ( a e. RR |-> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) )
85	83, 11, 84	pntrlog2bndlem4 24497	. . . . 5 |- ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / x ) ) e. <_O(1)
86	85	a1i 11	. . . 4 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / x ) ) e. <_O(1) )
87	28	nnred 10646	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR )
88		simpl 464	. . . . . . . . . . . . . . 15 |- ( ( a e. RR /\ a e. RR+ ) -> a e. RR )
89		simpr 468	. . . . . . . . . . . . . . . 16 |- ( ( a e. RR /\ a e. RR+ ) -> a e. RR+ )
90	89	relogcld 23651	. . . . . . . . . . . . . . 15 |- ( ( a e. RR /\ a e. RR+ ) -> ( log ` a ) e. RR )
91	88, 90	remulcld 9689	. . . . . . . . . . . . . 14 |- ( ( a e. RR /\ a e. RR+ ) -> ( a x. ( log ` a ) ) e. RR )
92		0red 9662	. . . . . . . . . . . . . 14 |- ( ( a e. RR /\ -. a e. RR+ ) -> 0 e. RR )
93	91, 92	ifclda 3904	. . . . . . . . . . . . 13 |- ( a e. RR -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) e. RR )
94	84, 93	fmpti 6060	. . . . . . . . . . . 12 |- T : RR --> RR
95	94	ffvelrni 6036	. . . . . . . . . . 11 |- ( n e. RR -> ( T ` n ) e. RR )
96	87, 95	syl 17	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` n ) e. RR )
97	87, 36	resubcld 10068	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n - 1 ) e. RR )
98	94	ffvelrni 6036	. . . . . . . . . . 11 |- ( ( n - 1 ) e. RR -> ( T ` ( n - 1 ) ) e. RR )
99	97, 98	syl 17	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` ( n - 1 ) ) e. RR )
100	96, 99	resubcld 10068	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) e. RR )
101	34, 100	remulcld 9689	. . . . . . . 8 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) e. RR )
102	25, 101	fsumrecl 13877	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) e. RR )
103	74, 102	remulcld 9689	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) e. RR )
104	49, 103	resubcld 10068	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) e. RR )
105	104, 10	rerpdivcld 11392	. . . 4 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / x ) e. RR )
106		2rp 11330	. . . . . . . . . . 11 |- 2 e. RR+
107	106	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 2 e. RR+ )
108	107	rpge0d 11368	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ 2 )
109	73, 22, 108	divge0d 11401	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( 2 / ( log ` x ) ) )
110	33	absge0d 13583	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( R ` ( x / n ) ) ) )
111	29	adantr 472	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> n e. RR+ )
112	111	rpcnd 11366	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> n e. CC )
113	57	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( log ` n ) e. CC )
114	112, 113	mulcld 9681	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( n x. ( log ` n ) ) e. CC )
115		simpr 468	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> 1 < n )
116		1re 9660	. . . . . . . . . . . . . . . . . . 19 |- 1 e. RR
117	111	rpred 11364	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> n e. RR )
118		difrp 11360	. . . . . . . . . . . . . . . . . . 19 |- ( ( 1 e. RR /\ n e. RR ) -> ( 1 < n <-> ( n - 1 ) e. RR+ ) )
119	116, 117, 118	sylancr 676	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( 1 < n <-> ( n - 1 ) e. RR+ ) )
120	115, 119	mpbid 215	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( n - 1 ) e. RR+ )
121	120	relogcld 23651	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( log ` ( n - 1 ) ) e. RR )
122	121	recnd 9687	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( log ` ( n - 1 ) ) e. CC )
123	112, 122	mulcld 9681	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( n x. ( log ` ( n - 1 ) ) ) e. CC )
124	114, 123, 122	subsubd 10033	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n x. ( log ` n ) ) - ( ( n x. ( log ` ( n - 1 ) ) ) - ( log ` ( n - 1 ) ) ) ) = ( ( ( n x. ( log ` n ) ) - ( n x. ( log ` ( n - 1 ) ) ) ) + ( log ` ( n - 1 ) ) ) )
125		rpre 11331	. . . . . . . . . . . . . . . . 17 |- ( n e. RR+ -> n e. RR )
126		eleq1 2537	. . . . . . . . . . . . . . . . . . 19 |- ( a = n -> ( a e. RR+ <-> n e. RR+ ) )
127		id 22	. . . . . . . . . . . . . . . . . . . 20 |- ( a = n -> a = n )
128		fveq2 5879	. . . . . . . . . . . . . . . . . . . 20 |- ( a = n -> ( log ` a ) = ( log ` n ) )
129	127, 128	oveq12d 6326	. . . . . . . . . . . . . . . . . . 19 |- ( a = n -> ( a x. ( log ` a ) ) = ( n x. ( log ` n ) ) )
130	126, 129	ifbieq1d 3895	. . . . . . . . . . . . . . . . . 18 |- ( a = n -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) )
131		ovex 6336	. . . . . . . . . . . . . . . . . . 19 |- ( n x. ( log ` n ) ) e. _V
132		c0ex 9655	. . . . . . . . . . . . . . . . . . 19 |- 0 e. _V
133	131, 132	ifex 3940	. . . . . . . . . . . . . . . . . 18 |- if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) e. _V
134	130, 84, 133	fvmpt 5963	. . . . . . . . . . . . . . . . 17 |- ( n e. RR -> ( T ` n ) = if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) )
135	125, 134	syl 17	. . . . . . . . . . . . . . . 16 |- ( n e. RR+ -> ( T ` n ) = if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) )
136		iftrue 3878	. . . . . . . . . . . . . . . 16 |- ( n e. RR+ -> if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) = ( n x. ( log ` n ) ) )
137	135, 136	eqtrd 2505	. . . . . . . . . . . . . . 15 |- ( n e. RR+ -> ( T ` n ) = ( n x. ( log ` n ) ) )
138	111, 137	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( T ` n ) = ( n x. ( log ` n ) ) )
139		rpre 11331	. . . . . . . . . . . . . . . . . 18 |- ( ( n - 1 ) e. RR+ -> ( n - 1 ) e. RR )
140		eleq1 2537	. . . . . . . . . . . . . . . . . . . 20 |- ( a = ( n - 1 ) -> ( a e. RR+ <-> ( n - 1 ) e. RR+ ) )
141		id 22	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = ( n - 1 ) -> a = ( n - 1 ) )
142		fveq2 5879	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = ( n - 1 ) -> ( log ` a ) = ( log ` ( n - 1 ) ) )
143	141, 142	oveq12d 6326	. . . . . . . . . . . . . . . . . . . 20 |- ( a = ( n - 1 ) -> ( a x. ( log ` a ) ) = ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) )
144	140, 143	ifbieq1d 3895	. . . . . . . . . . . . . . . . . . 19 |- ( a = ( n - 1 ) -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = if ( ( n - 1 ) e. RR+ , ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) , 0 ) )
145		ovex 6336	. . . . . . . . . . . . . . . . . . . 20 |- ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) e. _V
146	145, 132	ifex 3940	. . . . . . . . . . . . . . . . . . 19 |- if ( ( n - 1 ) e. RR+ , ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) , 0 ) e. _V
147	144, 84, 146	fvmpt 5963	. . . . . . . . . . . . . . . . . 18 |- ( ( n - 1 ) e. RR -> ( T ` ( n - 1 ) ) = if ( ( n - 1 ) e. RR+ , ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) , 0 ) )
148	139, 147	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( n - 1 ) e. RR+ -> ( T ` ( n - 1 ) ) = if ( ( n - 1 ) e. RR+ , ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) , 0 ) )
149		iftrue 3878	. . . . . . . . . . . . . . . . 17 |- ( ( n - 1 ) e. RR+ -> if ( ( n - 1 ) e. RR+ , ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) , 0 ) = ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) )
150	148, 149	eqtrd 2505	. . . . . . . . . . . . . . . 16 |- ( ( n - 1 ) e. RR+ -> ( T ` ( n - 1 ) ) = ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) )
151	120, 150	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( T ` ( n - 1 ) ) = ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) )
152		1cnd 9677	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> 1 e. CC )
153	112, 152, 122	subdird 10096	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) = ( ( n x. ( log ` ( n - 1 ) ) ) - ( 1 x. ( log ` ( n - 1 ) ) ) ) )
154	122	mulid2d 9679	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( 1 x. ( log ` ( n - 1 ) ) ) = ( log ` ( n - 1 ) ) )
155	154	oveq2d 6324	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n x. ( log ` ( n - 1 ) ) ) - ( 1 x. ( log ` ( n - 1 ) ) ) ) = ( ( n x. ( log ` ( n - 1 ) ) ) - ( log ` ( n - 1 ) ) ) )
156	151, 153, 155	3eqtrd 2509	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( T ` ( n - 1 ) ) = ( ( n x. ( log ` ( n - 1 ) ) ) - ( log ` ( n - 1 ) ) ) )
157	138, 156	oveq12d 6326	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) = ( ( n x. ( log ` n ) ) - ( ( n x. ( log ` ( n - 1 ) ) ) - ( log ` ( n - 1 ) ) ) ) )
158	112, 113, 122	subdid 10095	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) = ( ( n x. ( log ` n ) ) - ( n x. ( log ` ( n - 1 ) ) ) ) )
159	158	oveq1d 6323	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) + ( log ` ( n - 1 ) ) ) = ( ( ( n x. ( log ` n ) ) - ( n x. ( log ` ( n - 1 ) ) ) ) + ( log ` ( n - 1 ) ) ) )
160	124, 157, 159	3eqtr4d 2515	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) = ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) + ( log ` ( n - 1 ) ) ) )
161	111	relogcld 23651	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( log ` n ) e. RR )
162	161, 121	resubcld 10068	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( log ` n ) - ( log ` ( n - 1 ) ) ) e. RR )
163	162	recnd 9687	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( log ` n ) - ( log ` ( n - 1 ) ) ) e. CC )
164	112, 152, 163	subdird 10096	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n - 1 ) x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) = ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) - ( 1 x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) ) )
165	163	mulid2d 9679	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( 1 x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) = ( ( log ` n ) - ( log ` ( n - 1 ) ) ) )
166	165	oveq2d 6324	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) - ( 1 x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) ) = ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) - ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) )
167	117, 162	remulcld 9689	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) e. RR )
168	167	recnd 9687	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) e. CC )
169	168, 113, 122	subsub3d 10035	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) - ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) = ( ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) + ( log ` ( n - 1 ) ) ) - ( log ` n ) ) )
170	164, 166, 169	3eqtrd 2509	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n - 1 ) x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) = ( ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) + ( log ` ( n - 1 ) ) ) - ( log ` n ) ) )
171	112, 152	npcand 10009	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n - 1 ) + 1 ) = n )
172	171	fveq2d 5883	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( log ` ( ( n - 1 ) + 1 ) ) = ( log ` n ) )
173	172	oveq1d 6323	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( log ` ( ( n - 1 ) + 1 ) ) - ( log ` ( n - 1 ) ) ) = ( ( log ` n ) - ( log ` ( n - 1 ) ) ) )
174		logdifbnd 23998	. . . . . . . . . . . . . . . . 17 |- ( ( n - 1 ) e. RR+ -> ( ( log ` ( ( n - 1 ) + 1 ) ) - ( log ` ( n - 1 ) ) ) <_ ( 1 / ( n - 1 ) ) )
175	120, 174	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( log ` ( ( n - 1 ) + 1 ) ) - ( log ` ( n - 1 ) ) ) <_ ( 1 / ( n - 1 ) ) )
176	173, 175	eqbrtrrd 4418	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( log ` n ) - ( log ` ( n - 1 ) ) ) <_ ( 1 / ( n - 1 ) ) )
177		1red 9676	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> 1 e. RR )
178	162, 177, 120	lemuldiv2d 11411	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( ( n - 1 ) x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) <_ 1 <-> ( ( log ` n ) - ( log ` ( n - 1 ) ) ) <_ ( 1 / ( n - 1 ) ) ) )
179	176, 178	mpbird 240	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n - 1 ) x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) <_ 1 )
180	170, 179	eqbrtrrd 4418	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) + ( log ` ( n - 1 ) ) ) - ( log ` n ) ) <_ 1 )
181	167, 121	readdcld 9688	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) + ( log ` ( n - 1 ) ) ) e. RR )
182	181, 161, 177	lesubadd2d 10233	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) + ( log ` ( n - 1 ) ) ) - ( log ` n ) ) <_ 1 <-> ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) + ( log ` ( n - 1 ) ) ) <_ ( ( log ` n ) + 1 ) ) )
183	180, 182	mpbid 215	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) + ( log ` ( n - 1 ) ) ) <_ ( ( log ` n ) + 1 ) )
184	160, 183	eqbrtrd 4416	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) <_ ( ( log ` n ) + 1 ) )
185		fveq2 5879	. . . . . . . . . . . . . . . . 17 |- ( n = 1 -> ( T ` n ) = ( T ` 1 ) )
186		id 22	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = 1 -> a = 1 )
187	186, 3	syl6eqel 2557	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = 1 -> a e. RR+ )
188	187	iftrued 3880	. . . . . . . . . . . . . . . . . . . 20 |- ( a = 1 -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = ( a x. ( log ` a ) ) )
189		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a = 1 -> ( log ` a ) = ( log ` 1 ) )
190		log1 23614	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( log ` 1 ) = 0
191	189, 190	syl6eq 2521	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = 1 -> ( log ` a ) = 0 )
192	186, 191	oveq12d 6326	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = 1 -> ( a x. ( log ` a ) ) = ( 1 x. 0 ) )
193		ax-1cn 9615	. . . . . . . . . . . . . . . . . . . . . 22 |- 1 e. CC
194	193	mul01i 9841	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 x. 0 ) = 0
195	192, 194	syl6eq 2521	. . . . . . . . . . . . . . . . . . . 20 |- ( a = 1 -> ( a x. ( log ` a ) ) = 0 )
196	188, 195	eqtrd 2505	. . . . . . . . . . . . . . . . . . 19 |- ( a = 1 -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = 0 )
197	196, 84, 132	fvmpt 5963	. . . . . . . . . . . . . . . . . 18 |- ( 1 e. RR -> ( T ` 1 ) = 0 )
198	116, 197	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( T ` 1 ) = 0
199	185, 198	syl6eq 2521	. . . . . . . . . . . . . . . 16 |- ( n = 1 -> ( T ` n ) = 0 )
200		oveq1 6315	. . . . . . . . . . . . . . . . . . 19 |- ( n = 1 -> ( n - 1 ) = ( 1 - 1 ) )
201		1m1e0 10700	. . . . . . . . . . . . . . . . . . 19 |- ( 1 - 1 ) = 0
202	200, 201	syl6eq 2521	. . . . . . . . . . . . . . . . . 18 |- ( n = 1 -> ( n - 1 ) = 0 )
203	202	fveq2d 5883	. . . . . . . . . . . . . . . . 17 |- ( n = 1 -> ( T ` ( n - 1 ) ) = ( T ` 0 ) )
204		0re 9661	. . . . . . . . . . . . . . . . . 18 |- 0 e. RR
205		rpne0 11340	. . . . . . . . . . . . . . . . . . . . 21 |- ( a e. RR+ -> a =/= 0 )
206	205	necon2bi 2673	. . . . . . . . . . . . . . . . . . . 20 |- ( a = 0 -> -. a e. RR+ )
207	206	iffalsed 3883	. . . . . . . . . . . . . . . . . . 19 |- ( a = 0 -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = 0 )
208	207, 84, 132	fvmpt 5963	. . . . . . . . . . . . . . . . . 18 |- ( 0 e. RR -> ( T ` 0 ) = 0 )
209	204, 208	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( T ` 0 ) = 0
210	203, 209	syl6eq 2521	. . . . . . . . . . . . . . . 16 |- ( n = 1 -> ( T ` ( n - 1 ) ) = 0 )
211	199, 210	oveq12d 6326	. . . . . . . . . . . . . . 15 |- ( n = 1 -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) = ( 0 - 0 ) )
212		0m0e0 10741	. . . . . . . . . . . . . . 15 |- ( 0 - 0 ) = 0
213	211, 212	syl6eq 2521	. . . . . . . . . . . . . 14 |- ( n = 1 -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) = 0 )
214	213	eqcoms 2479	. . . . . . . . . . . . 13 |- ( 1 = n -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) = 0 )
215	214	adantl 473	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 = n ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) = 0 )
216		0red 9662	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 e. RR )
217	28	nnge1d 10674	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ n )
218	87, 217	logge0d 23658	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( log ` n ) )
219	35	lep1d 10560	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) <_ ( ( log ` n ) + 1 ) )
220	216, 35, 37, 218, 219	letrd 9809	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( log ` n ) + 1 ) )
221	220	adantr 472	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 = n ) -> 0 <_ ( ( log ` n ) + 1 ) )
222	215, 221	eqbrtrd 4416	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 = n ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) <_ ( ( log ` n ) + 1 ) )
223		elfzle1 11828	. . . . . . . . . . . . 13 |- ( n e. ( 1 ... ( |_ ` x ) ) -> 1 <_ n )
224	223	adantl 473	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ n )
225	36, 87	leloed 9795	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 <_ n <-> ( 1 < n \/ 1 = n ) ) )
226	224, 225	mpbid 215	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 < n \/ 1 = n ) )
227	184, 222, 226	mpjaodan 803	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) <_ ( ( log ` n ) + 1 ) )
228	100, 37, 34, 110, 227	lemul2ad 10569	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) <_ ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) )
229	25, 101, 38, 228	fsumle 13936	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) )
230	102, 75, 74, 109, 229	lemul2ad 10569	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) <_ ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) )
231	103, 76, 49, 230	lesub2dd 10251	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) <_ ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) )
232	77, 104, 10, 231	lediv1dd 11419	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) / x ) <_ ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / x ) )
233	232	adantrr 731	. . . 4 |- ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ 1 <_ x ) ) -> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) / x ) <_ ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / x ) )
234	82, 86, 105, 78, 233	lo1le 13792	. . 3 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) / x ) ) e. <_O(1) )
235	106	a1i 11	. . . . . . . 8 |- ( ph -> 2 e. RR+ )
236		pntrlog2bndlem5.1	. . . . . . . 8 |- ( ph -> B e. RR+ )
237	235, 236	rpmulcld 11380	. . . . . . 7 |- ( ph -> ( 2 x. B ) e. RR+ )
238	237	rpred 11364	. . . . . 6 |- ( ph -> ( 2 x. B ) e. RR )
239	238	adantr 472	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. B ) e. RR )
240	5, 22	rerpdivcld 11392	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 / ( log ` x ) ) e. RR )
241	5, 240	readdcld 9688	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 + ( 1 / ( log ` x ) ) ) e. RR )
242		ioossre 11721	. . . . . 6 |- ( 1 (,) +oo ) C_ RR
243		lo1const 13761	. . . . . 6 |- ( ( ( 1 (,) +oo ) C_ RR /\ ( 2 x. B ) e. RR ) -> ( x e. ( 1 (,) +oo ) |-> ( 2 x. B ) ) e. <_O(1) )
244	242, 238, 243	sylancr 676	. . . . 5 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 2 x. B ) ) e. <_O(1) )
245		lo1const 13761	. . . . . . 7 |- ( ( ( 1 (,) +oo ) C_ RR /\ 1 e. RR ) -> ( x e. ( 1 (,) +oo ) |-> 1 ) e. <_O(1) )
246	242, 82, 245	sylancr 676	. . . . . 6 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> 1 ) e. <_O(1) )
247		divlogrlim 23659	. . . . . . . 8 |- ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~> r 0
248		rlimo1 13757	. . . . . . . 8 |- ( ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~> r 0 -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O(1) )
249	247, 248	mp1i 13	. . . . . . 7 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O(1) )
250	240, 249	o1lo1d 13680	. . . . . 6 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. <_O(1) )
251	5, 240, 246, 250	lo1add 13767	. . . . 5 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 1 + ( 1 / ( log ` x ) ) ) ) e. <_O(1) )
252	237	adantr 472	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. B ) e. RR+ )
253	252	rpge0d 11368	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( 2 x. B ) )
254	239, 241, 244, 251, 253	lo1mul 13768	. . . 4 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( 2 x. B ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) ) e. <_O(1) )
255	239, 241	remulcld 9689	. . . 4 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. B ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) e. RR )
256	79, 10	rerpdivcld 11392	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) / x ) e. RR )
257	18, 5	readdcld 9688	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) + 1 ) e. RR )
258	236	adantr 472	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> B e. RR+ )
259	258	rpred 11364	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> B e. RR )
260	257, 259	remulcld 9689	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) + 1 ) x. B ) e. RR )
261	28	nnrecred 10677	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / n ) e. RR )
262	25, 261	fsumrecl 13877	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) e. RR )
263	262, 259	remulcld 9689	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) x. B ) e. RR )
264	34, 26	rerpdivcld 11392	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) / x ) e. RR )
265	259	adantr 472	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> B e. RR )
266	261, 265	remulcld 9689	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 / n ) x. B ) e. RR )
267	30	rpcnd 11366	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. CC )
268	30	rpne0d 11369	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) =/= 0 )
269	33, 267, 268	absdivd 13594	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) = ( ( abs ` ( R ` ( x / n ) ) ) / ( abs ` ( x / n ) ) ) )
270	2	adantr 472	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR )
271	270, 28	nndivred 10680	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR )
272	30	rpge0d 11368	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( x / n ) )
273	271, 272	absidd 13561	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( x / n ) ) = ( x / n ) )
274	273	oveq2d 6324	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) / ( abs ` ( x / n ) ) ) = ( ( abs ` ( R ` ( x / n ) ) ) / ( x / n ) ) )
275	269, 274	eqtrd 2505	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) = ( ( abs ` ( R ` ( x / n ) ) ) / ( x / n ) ) )
276	46	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. CC )
277	87	recnd 9687	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
278	47	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x =/= 0 )
279	28	nnne0d 10676	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n =/= 0 )
280	43, 276, 277, 278, 279	divdiv2d 10437	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) / ( x / n ) ) = ( ( ( abs ` ( R ` ( x / n ) ) ) x. n ) / x ) )
281	43, 277, 276, 278	div23d 10442	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( R ` ( x / n ) ) ) x. n ) / x ) = ( ( ( abs ` ( R ` ( x / n ) ) ) / x ) x. n ) )
282	275, 280, 281	3eqtrd 2509	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) = ( ( ( abs ` ( R ` ( x / n ) ) ) / x ) x. n ) )
283		pntrlog2bndlem5.2	. . . . . . . . . . . . . . 15 |- ( ph -> A. y e. RR+ ( abs ` ( ( R ` y ) / y ) ) <_ B )
284	283	ad2antrr 740	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A. y e. RR+ ( abs ` ( ( R ` y ) / y ) ) <_ B )
285		fveq2 5879	. . . . . . . . . . . . . . . . . 18 |- ( y = ( x / n ) -> ( R ` y ) = ( R ` ( x / n ) ) )
286		id 22	. . . . . . . . . . . . . . . . . 18 |- ( y = ( x / n ) -> y = ( x / n ) )
287	285, 286	oveq12d 6326	. . . . . . . . . . . . . . . . 17 |- ( y = ( x / n ) -> ( ( R ` y ) / y ) = ( ( R ` ( x / n ) ) / ( x / n ) ) )
288	287	fveq2d 5883	. . . . . . . . . . . . . . . 16 |- ( y = ( x / n ) -> ( abs ` ( ( R ` y ) / y ) ) = ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) )
289	288	breq1d 4405	. . . . . . . . . . . . . . 15 |- ( y = ( x / n ) -> ( ( abs ` ( ( R ` y ) / y ) ) <_ B <-> ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) <_ B ) )
290	289	rspcv 3132	. . . . . . . . . . . . . 14 |- ( ( x / n ) e. RR+ -> ( A. y e. RR+ ( abs ` ( ( R ` y ) / y ) ) <_ B -> ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) <_ B ) )
291	30, 284, 290	sylc 61	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) <_ B )
292	282, 291	eqbrtrrd 4418	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( R ` ( x / n ) ) ) / x ) x. n ) <_ B )
293	264, 265, 29	lemuldivd 11410	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( abs ` ( R ` ( x / n ) ) ) / x ) x. n ) <_ B <-> ( ( abs ` ( R ` ( x / n ) ) ) / x ) <_ ( B / n ) ) )
294	292, 293	mpbid 215	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) / x ) <_ ( B / n ) )
295	265	recnd 9687	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> B e. CC )
296	295, 277, 279	divrec2d 10409	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( B / n ) = ( ( 1 / n ) x. B ) )
297	294, 296	breqtrd 4420	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) / x ) <_ ( ( 1 / n ) x. B ) )
298	25, 264, 266, 297	fsumle 13936	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) / x ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 / n ) x. B ) )
299	25, 46, 43, 47	fsumdivc 13924	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) / x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) / x ) )
300	258	rpcnd 11366	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> B e. CC )
301	261	recnd 9687	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / n ) e. CC )
302	25, 300, 301	fsummulc1 13923	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) x. B ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 / n ) x. B ) )
303	298, 299, 302	3brtr4d 4426	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) / x ) <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) x. B ) )
304	258	rpge0d 11368	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ B )
305		harmonicubnd 24014	. . . . . . . . . 10 |- ( ( x e. RR /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) <_ ( ( log ` x ) + 1 ) )
306	2, 9, 305	syl2anc 673	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) <_ ( ( log ` x ) + 1 ) )
307	262, 257, 259, 304, 306	lemul1ad 10568	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) x. B ) <_ ( ( ( log ` x ) + 1 ) x. B ) )
308	256, 263, 260, 303, 307	letrd 9809	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) / x ) <_ ( ( ( log ` x ) + 1 ) x. B ) )
309	256, 260, 74, 109, 308	lemul2ad 10569	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) / x ) ) <_ ( ( 2 / ( log ` x ) ) x. ( ( ( log ` x ) + 1 ) x. B ) ) )
310	24, 44, 46, 47	divassd 10440	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) / x ) = ( ( 2 / ( log ` x ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) / x ) ) )
311	241	recnd 9687	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 + ( 1 / ( log ` x ) ) ) e. CC )
312	21, 300, 311	mul32d 9861	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. B ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) = ( ( 2 x. ( 1 + ( 1 / ( log ` x ) ) ) ) x. B ) )
313		1cnd 9677	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. CC )
314	19, 313, 19, 23	divdird 10443	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) + 1 ) / ( log ` x ) ) = ( ( ( log ` x ) / ( log ` x ) ) + ( 1 / ( log ` x ) ) ) )
315	19, 23	dividd 10403	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / ( log ` x ) ) = 1 )
316	315	oveq1d 6323	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) / ( log ` x ) ) + ( 1 / ( log ` x ) ) ) = ( 1 + ( 1 / ( log ` x ) ) ) )
317	314, 316	eqtr2d 2506	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 + ( 1 / ( log ` x ) ) ) = ( ( ( log ` x ) + 1 ) / ( log ` x ) ) )
318	317	oveq2d 6324	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( 1 + ( 1 / ( log ` x ) ) ) ) = ( 2 x. ( ( ( log ` x ) + 1 ) / ( log ` x ) ) ) )
319	19, 313	addcld 9680	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) + 1 ) e. CC )
320	21, 19, 319, 23	div32d 10428	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. ( ( log ` x ) + 1 ) ) = ( 2 x. ( ( ( log ` x ) + 1 ) / ( log ` x ) ) ) )
321	318, 320	eqtr4d 2508	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( 1 + ( 1 / ( log ` x ) ) ) ) = ( ( 2 / ( log ` x ) ) x. ( ( log ` x ) + 1 ) ) )
322	321	oveq1d 6323	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. ( 1 + ( 1 / ( log ` x ) ) ) ) x. B ) = ( ( ( 2 / ( log ` x ) ) x. ( ( log ` x ) + 1 ) ) x. B ) )
323	24, 319, 300	mulassd 9684	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. ( ( log ` x ) + 1 ) ) x. B ) = ( ( 2 / ( log ` x ) ) x. ( ( ( log ` x ) + 1 ) x. B ) ) )
324	312, 322, 323	3eqtrd 2509	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. B ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) = ( ( 2 / ( log ` x ) ) x. ( ( ( log ` x ) + 1 ) x. B ) ) )
325	309, 310, 324	3brtr4d 4426	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) / x ) <_ ( ( 2 x. B ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) )
326	325	adantrr 731	. . . 4 |- ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ 1 <_ x ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) / x ) <_ ( ( 2 x. B ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) )
327	82, 254, 255, 81, 326	lo1le 13792	. . 3 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) / x ) ) e. <_O(1) )
328	78, 81, 234, 327	lo1add 13767	. 2 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) ) ) / x ) + ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) / x ) ) ) e. <_