Theorem pntrlog2bndlem5 23892

Description: Lemma for pntrlog2bnd 23895. 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 11584	. . . . . . . . . . . . 13 |- ( x e. ( 1 (,) +oo ) -> x e. RR )
2	1	adantl 466	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
3		1rp 11249	. . . . . . . . . . . . 13 |- 1 e. RR+
4	3	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ )
5		1red 9628	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR )
6		eliooord 11609	. . . . . . . . . . . . . . 15 |- ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
7	6	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 < x /\ x < +oo ) )
8	7	simpld 459	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 < x )
9	5, 2, 8	ltled 9750	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x )
10	2, 4, 9	rpgecld 11316	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
11		pntrlog2bnd.r	. . . . . . . . . . . . 13 |- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )
12	11	pntrf 23874	. . . . . . . . . . . 12 |- R : RR+ --> RR
13	12	ffvelrni 6031	. . . . . . . . . . 11 |- ( x e. RR+ -> ( R ` x ) e. RR )
14	10, 13	syl 16	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) e. RR )
15	14	recnd 9639	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) e. CC )
16	15	abscld 13279	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` x ) ) e. RR )
17	16	recnd 9639	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` x ) ) e. CC )
18	10	relogcld 23134	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR )
19	18	recnd 9639	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
20	17, 19	mulcld 9633	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) e. CC )
21		2cnd 10629	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 2 e. CC )
22	2, 8	rplogcld 23140	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
23	22	rpne0d 11286	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
24	21, 19, 23	divcld 10341	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 / ( log ` x ) ) e. CC )
25		fzfid 12086	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
26	10	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ )
27		elfznn 11739	. . . . . . . . . . . . . . . 16 |- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
28	27	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
29	28	nnrpd 11280	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
30	26, 29	rpdivcld 11298	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
31	12	ffvelrni 6031	. . . . . . . . . . . . 13 |- ( ( x / n ) e. RR+ -> ( R ` ( x / n ) ) e. RR )
32	30, 31	syl 16	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. RR )
33	32	recnd 9639	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. CC )
34	33	abscld 13279	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / n ) ) ) e. RR )
35	29	relogcld 23134	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. RR )
36		1red 9628	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
37	35, 36	readdcld 9640	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` n ) + 1 ) e. RR )
38	34, 37	remulcld 9641	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) e. RR )
39	38	recnd 9639	. . . . . . . 8 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) e. CC )
40	25, 39	fsumcl 13567	. . . . . . 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 9633	. . . . . 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 9950	. . . . 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 9639	. . . . . . 7 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / n ) ) ) e. CC )
44	25, 43	fsumcl 13567	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) e. CC )
45	24, 44	mulcld 9633	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) e. CC )
46	2	recnd 9639	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. CC )
47	10	rpne0d 11286	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x =/= 0 )
48	42, 45, 46, 47	divdird 10379	. . . 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 9641	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) e. RR )
50	49	recnd 9639	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) e. CC )
51	50, 41, 45	subsubd 9978	. . . . . 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 10033	. . . . . . . 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 13615	. . . . . . . . . 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 9639	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` n ) + 1 ) e. CC )
55		1cnd 9629	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. CC )
56	43, 54, 55	subdid 10033	. . . . . . . . . . . 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 9639	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. CC )
58	57, 55	pncand 9951	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( log ` n ) + 1 ) - 1 ) = ( log ` n ) )
59	58	oveq2d 6312	. . . . . . . . . . . 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 9630	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. 1 ) = ( abs ` ( R ` ( x / n ) ) ) )
61	60	oveq2d 6312	. . . . . . . . . . . 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 2507	. . . . . . . . . . 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 13537	. . . . . . . . . 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 2500	. . . . . . . . 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 6312	. . . . . . . 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 2500	. . . . . . 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 6312	. . . . . 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 2500	. . . . 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 6311	. . . 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 2500	. . 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 4543	. 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 10626	. . . . . . . 8 |- 2 e. RR
73	72	a1i 11	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 2 e. RR )
74	73, 22	rerpdivcld 11308	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 / ( log ` x ) ) e. RR )
75	25, 38	fsumrecl 13568	. . . . . 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 9641	. . . . 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 10008	. . . 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 11308	. . 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 13568	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) e. RR )
80	74, 79	remulcld 9641	. . . 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 11308	. . 3 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) / x ) e. RR )
82		1red 9628	. . . 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 23891	. . . . 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 10571	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR )
88		simpl 457	. . . . . . . . . . . . . . 15 |- ( ( a e. RR /\ a e. RR+ ) -> a e. RR )
89		simpr 461	. . . . . . . . . . . . . . . 16 |- ( ( a e. RR /\ a e. RR+ ) -> a e. RR+ )
90	89	relogcld 23134	. . . . . . . . . . . . . . 15 |- ( ( a e. RR /\ a e. RR+ ) -> ( log ` a ) e. RR )
91	88, 90	remulcld 9641	. . . . . . . . . . . . . 14 |- ( ( a e. RR /\ a e. RR+ ) -> ( a x. ( log ` a ) ) e. RR )
92		0red 9614	. . . . . . . . . . . . . 14 |- ( ( a e. RR /\ -. a e. RR+ ) -> 0 e. RR )
93	91, 92	ifclda 3976	. . . . . . . . . . . . 13 |- ( a e. RR -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) e. RR )
94	84, 93	fmpti 6055	. . . . . . . . . . . 12 |- T : RR --> RR
95	94	ffvelrni 6031	. . . . . . . . . . 11 |- ( n e. RR -> ( T ` n ) e. RR )
96	87, 95	syl 16	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` n ) e. RR )
97	87, 36	resubcld 10008	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n - 1 ) e. RR )
98	94	ffvelrni 6031	. . . . . . . . . . 11 |- ( ( n - 1 ) e. RR -> ( T ` ( n - 1 ) ) e. RR )
99	97, 98	syl 16	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` ( n - 1 ) ) e. RR )
100	96, 99	resubcld 10008	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) e. RR )
101	34, 100	remulcld 9641	. . . . . . . 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 13568	. . . . . . 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 9641	. . . . . 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 10008	. . . . 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 11308	. . . 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 11250	. . . . . . . . . . 11 |- 2 e. RR+
107	106	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 2 e. RR+ )
108	107	rpge0d 11285	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ 2 )
109	73, 22, 108	divge0d 11317	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( 2 / ( log ` x ) ) )
110	33	absge0d 13287	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( R ` ( x / n ) ) ) )
111	29	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> n e. RR+ )
112	111	rpcnd 11283	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> n e. CC )
113	57	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( log ` n ) e. CC )
114	112, 113	mulcld 9633	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( n x. ( log ` n ) ) e. CC )
115		simpr 461	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> 1 < n )
116		1re 9612	. . . . . . . . . . . . . . . . . . 19 |- 1 e. RR
117	111	rpred 11281	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> n e. RR )
118		difrp 11278	. . . . . . . . . . . . . . . . . . 19 |- ( ( 1 e. RR /\ n e. RR ) -> ( 1 < n <-> ( n - 1 ) e. RR+ ) )
119	116, 117, 118	sylancr 663	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( 1 < n <-> ( n - 1 ) e. RR+ ) )
120	115, 119	mpbid 210	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( n - 1 ) e. RR+ )
121	120	relogcld 23134	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( log ` ( n - 1 ) ) e. RR )
122	121	recnd 9639	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( log ` ( n - 1 ) ) e. CC )
123	112, 122	mulcld 9633	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( n x. ( log ` ( n - 1 ) ) ) e. CC )
124	114, 123, 122	subsubd 9978	. . . . . . . . . . . . 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 11251	. . . . . . . . . . . . . . . . 17 |- ( n e. RR+ -> n e. RR )
126		eleq1 2529	. . . . . . . . . . . . . . . . . . 19 |- ( a = n -> ( a e. RR+ <-> n e. RR+ ) )
127		id 22	. . . . . . . . . . . . . . . . . . . 20 |- ( a = n -> a = n )
128		fveq2 5872	. . . . . . . . . . . . . . . . . . . 20 |- ( a = n -> ( log ` a ) = ( log ` n ) )
129	127, 128	oveq12d 6314	. . . . . . . . . . . . . . . . . . 19 |- ( a = n -> ( a x. ( log ` a ) ) = ( n x. ( log ` n ) ) )
130	126, 129	ifbieq1d 3967	. . . . . . . . . . . . . . . . . 18 |- ( a = n -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) )
131		ovex 6324	. . . . . . . . . . . . . . . . . . 19 |- ( n x. ( log ` n ) ) e. _V
132		c0ex 9607	. . . . . . . . . . . . . . . . . . 19 |- 0 e. _V
133	131, 132	ifex 4013	. . . . . . . . . . . . . . . . . 18 |- if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) e. _V
134	130, 84, 133	fvmpt 5956	. . . . . . . . . . . . . . . . 17 |- ( n e. RR -> ( T ` n ) = if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) )
135	125, 134	syl 16	. . . . . . . . . . . . . . . 16 |- ( n e. RR+ -> ( T ` n ) = if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) )
136		iftrue 3950	. . . . . . . . . . . . . . . 16 |- ( n e. RR+ -> if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) = ( n x. ( log ` n ) ) )
137	135, 136	eqtrd 2498	. . . . . . . . . . . . . . 15 |- ( n e. RR+ -> ( T ` n ) = ( n x. ( log ` n ) ) )
138	111, 137	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( T ` n ) = ( n x. ( log ` n ) ) )
139		rpre 11251	. . . . . . . . . . . . . . . . . 18 |- ( ( n - 1 ) e. RR+ -> ( n - 1 ) e. RR )
140		eleq1 2529	. . . . . . . . . . . . . . . . . . . 20 |- ( a = ( n - 1 ) -> ( a e. RR+ <-> ( n - 1 ) e. RR+ ) )
141		id 22	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = ( n - 1 ) -> a = ( n - 1 ) )
142		fveq2 5872	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = ( n - 1 ) -> ( log ` a ) = ( log ` ( n - 1 ) ) )
143	141, 142	oveq12d 6314	. . . . . . . . . . . . . . . . . . . 20 |- ( a = ( n - 1 ) -> ( a x. ( log ` a ) ) = ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) )
144	140, 143	ifbieq1d 3967	. . . . . . . . . . . . . . . . . . 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 6324	. . . . . . . . . . . . . . . . . . . 20 |- ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) e. _V
146	145, 132	ifex 4013	. . . . . . . . . . . . . . . . . . 19 |- if ( ( n - 1 ) e. RR+ , ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) , 0 ) e. _V
147	144, 84, 146	fvmpt 5956	. . . . . . . . . . . . . . . . . 18 |- ( ( n - 1 ) e. RR -> ( T ` ( n - 1 ) ) = if ( ( n - 1 ) e. RR+ , ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) , 0 ) )
148	139, 147	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( n - 1 ) e. RR+ -> ( T ` ( n - 1 ) ) = if ( ( n - 1 ) e. RR+ , ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) , 0 ) )
149		iftrue 3950	. . . . . . . . . . . . . . . . 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 2498	. . . . . . . . . . . . . . . 16 |- ( ( n - 1 ) e. RR+ -> ( T ` ( n - 1 ) ) = ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) )
151	120, 150	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( T ` ( n - 1 ) ) = ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) )
152		1cnd 9629	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> 1 e. CC )
153	112, 152, 122	subdird 10034	. . . . . . . . . . . . . . 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 9631	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( 1 x. ( log ` ( n - 1 ) ) ) = ( log ` ( n - 1 ) ) )
155	154	oveq2d 6312	. . . . . . . . . . . . . . 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 2502	. . . . . . . . . . . . . 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 6314	. . . . . . . . . . . . 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 10033	. . . . . . . . . . . . . 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 6311	. . . . . . . . . . . . 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 2508	. . . . . . . . . . . 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 23134	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( log ` n ) e. RR )
162	161, 121	resubcld 10008	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( log ` n ) - ( log ` ( n - 1 ) ) ) e. RR )
163	162	recnd 9639	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( log ` n ) - ( log ` ( n - 1 ) ) ) e. CC )
164	112, 152, 163	subdird 10034	. . . . . . . . . . . . . . 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 9631	. . . . . . . . . . . . . . . 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 6312	. . . . . . . . . . . . . . 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 9641	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) e. RR )
168	167	recnd 9639	. . . . . . . . . . . . . . . 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 9980	. . . . . . . . . . . . . . 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 2502	. . . . . . . . . . . . . 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 9954	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n - 1 ) + 1 ) = n )
172	171	fveq2d 5876	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( log ` ( ( n - 1 ) + 1 ) ) = ( log ` n ) )
173	172	oveq1d 6311	. . . . . . . . . . . . . . . 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 23449	. . . . . . . . . . . . . . . . 17 |- ( ( n - 1 ) e. RR+ -> ( ( log ` ( ( n - 1 ) + 1 ) ) - ( log ` ( n - 1 ) ) ) <_ ( 1 / ( n - 1 ) ) )
175	120, 174	syl 16	. . . . . . . . . . . . . . . 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 4478	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( log ` n ) - ( log ` ( n - 1 ) ) ) <_ ( 1 / ( n - 1 ) ) )
177		1red 9628	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> 1 e. RR )
178	162, 177, 120	lemuldiv2d 11327	. . . . . . . . . . . . . . 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 232	. . . . . . . . . . . . . 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 4478	. . . . . . . . . . . . 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 9640	. . . . . . . . . . . . . 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 10172	. . . . . . . . . . . . 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 210	. . . . . . . . . . . 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 4476	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) <_ ( ( log ` n ) + 1 ) )
185		fveq2 5872	. . . . . . . . . . . . . . . . 17 |- ( n = 1 -> ( T ` n ) = ( T ` 1 ) )
186		id 22	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = 1 -> a = 1 )
187	186, 3	syl6eqel 2553	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = 1 -> a e. RR+ )
188	187	iftrued 3952	. . . . . . . . . . . . . . . . . . . 20 |- ( a = 1 -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = ( a x. ( log ` a ) ) )
189		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a = 1 -> ( log ` a ) = ( log ` 1 ) )
190		log1 23096	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( log ` 1 ) = 0
191	189, 190	syl6eq 2514	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = 1 -> ( log ` a ) = 0 )
192	186, 191	oveq12d 6314	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = 1 -> ( a x. ( log ` a ) ) = ( 1 x. 0 ) )
193		ax-1cn 9567	. . . . . . . . . . . . . . . . . . . . . 22 |- 1 e. CC
194	193	mul01i 9787	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 x. 0 ) = 0
195	192, 194	syl6eq 2514	. . . . . . . . . . . . . . . . . . . 20 |- ( a = 1 -> ( a x. ( log ` a ) ) = 0 )
196	188, 195	eqtrd 2498	. . . . . . . . . . . . . . . . . . 19 |- ( a = 1 -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = 0 )
197	196, 84, 132	fvmpt 5956	. . . . . . . . . . . . . . . . . 18 |- ( 1 e. RR -> ( T ` 1 ) = 0 )
198	116, 197	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( T ` 1 ) = 0
199	185, 198	syl6eq 2514	. . . . . . . . . . . . . . . 16 |- ( n = 1 -> ( T ` n ) = 0 )
200		oveq1 6303	. . . . . . . . . . . . . . . . . . 19 |- ( n = 1 -> ( n - 1 ) = ( 1 - 1 ) )
201		1m1e0 10625	. . . . . . . . . . . . . . . . . . 19 |- ( 1 - 1 ) = 0
202	200, 201	syl6eq 2514	. . . . . . . . . . . . . . . . . 18 |- ( n = 1 -> ( n - 1 ) = 0 )
203	202	fveq2d 5876	. . . . . . . . . . . . . . . . 17 |- ( n = 1 -> ( T ` ( n - 1 ) ) = ( T ` 0 ) )
204		0re 9613	. . . . . . . . . . . . . . . . . 18 |- 0 e. RR
205		rpne0 11260	. . . . . . . . . . . . . . . . . . . . 21 |- ( a e. RR+ -> a =/= 0 )
206	205	necon2bi 2694	. . . . . . . . . . . . . . . . . . . 20 |- ( a = 0 -> -. a e. RR+ )
207	206	iffalsed 3955	. . . . . . . . . . . . . . . . . . 19 |- ( a = 0 -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = 0 )
208	207, 84, 132	fvmpt 5956	. . . . . . . . . . . . . . . . . 18 |- ( 0 e. RR -> ( T ` 0 ) = 0 )
209	204, 208	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( T ` 0 ) = 0
210	203, 209	syl6eq 2514	. . . . . . . . . . . . . . . 16 |- ( n = 1 -> ( T ` ( n - 1 ) ) = 0 )
211	199, 210	oveq12d 6314	. . . . . . . . . . . . . . 15 |- ( n = 1 -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) = ( 0 - 0 ) )
212		0m0e0 10666	. . . . . . . . . . . . . . 15 |- ( 0 - 0 ) = 0
213	211, 212	syl6eq 2514	. . . . . . . . . . . . . 14 |- ( n = 1 -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) = 0 )
214	213	eqcoms 2469	. . . . . . . . . . . . 13 |- ( 1 = n -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) = 0 )
215	214	adantl 466	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 = n ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) = 0 )
216		0red 9614	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 e. RR )
217	28	nnge1d 10599	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ n )
218	87, 217	logge0d 23141	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( log ` n ) )
219	35	lep1d 10497	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) <_ ( ( log ` n ) + 1 ) )
220	216, 35, 37, 218, 219	letrd 9756	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( log ` n ) + 1 ) )
221	220	adantr 465	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 = n ) -> 0 <_ ( ( log ` n ) + 1 ) )
222	215, 221	eqbrtrd 4476	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 = n ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) <_ ( ( log ` n ) + 1 ) )
223		elfzle1 11714	. . . . . . . . . . . . 13 |- ( n e. ( 1 ... ( |_ ` x ) ) -> 1 <_ n )
224	223	adantl 466	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ n )
225	36, 87	leloed 9745	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 <_ n <-> ( 1 < n \/ 1 = n ) ) )
226	224, 225	mpbid 210	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 < n \/ 1 = n ) )
227	184, 222, 226	mpjaodan 786	. . . . . . . . . 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 10506	. . . . . . . . 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 13625	. . . . . . . 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 10506	. . . . . . 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 10190	. . . . . 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 11335	. . . . 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 716	. . . 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 13486	. . 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 11297	. . . . . . 7 |- ( ph -> ( 2 x. B ) e. RR+ )
238	237	rpred 11281	. . . . . 6 |- ( ph -> ( 2 x. B ) e. RR )
239	238	adantr 465	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. B ) e. RR )
240	5, 22	rerpdivcld 11308	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 / ( log ` x ) ) e. RR )
241	5, 240	readdcld 9640	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 + ( 1 / ( log ` x ) ) ) e. RR )
242		ioossre 11611	. . . . . 6 |- ( 1 (,) +oo ) C_ RR
243		lo1const 13455	. . . . . 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 663	. . . . 5 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 2 x. B ) ) e. <_O(1) )
245		lo1const 13455	. . . . . . 7 |- ( ( ( 1 (,) +oo ) C_ RR /\ 1 e. RR ) -> ( x e. ( 1 (,) +oo ) |-> 1 ) e. <_O(1) )
246	242, 82, 245	sylancr 663	. . . . . 6 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> 1 ) e. <_O(1) )
247		divlogrlim 23142	. . . . . . . 8 |- ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~> r 0
248		rlimo1 13451	. . . . . . . 8 |- ( ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~> r 0 -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O(1) )
249	247, 248	mp1i 12	. . . . . . 7 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O(1) )
250	240, 249	o1lo1d 13374	. . . . . 6 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. <_O(1) )
251	5, 240, 246, 250	lo1add 13461	. . . . 5 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 1 + ( 1 / ( log ` x ) ) ) ) e. <_O(1) )
252	237	adantr 465	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. B ) e. RR+ )
253	252	rpge0d 11285	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( 2 x. B ) )
254	239, 241, 244, 251, 253	lo1mul 13462	. . . 4 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( 2 x. B ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) ) e. <_O(1) )
255	239, 241	remulcld 9641	. . . 4 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. B ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) e. RR )
256	79, 10	rerpdivcld 11308	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) / x ) e. RR )
257	18, 5	readdcld 9640	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) + 1 ) e. RR )
258	236	adantr 465	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> B e. RR+ )
259	258	rpred 11281	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> B e. RR )
260	257, 259	remulcld 9641	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) + 1 ) x. B ) e. RR )
261	28	nnrecred 10602	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / n ) e. RR )
262	25, 261	fsumrecl 13568	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) e. RR )
263	262, 259	remulcld 9641	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) x. B ) e. RR )
264	34, 26	rerpdivcld 11308	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) / x ) e. RR )
265	259	adantr 465	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> B e. RR )
266	261, 265	remulcld 9641	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 / n ) x. B ) e. RR )
267	30	rpcnd 11283	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. CC )
268	30	rpne0d 11286	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) =/= 0 )
269	33, 267, 268	absdivd 13298	. . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR )
271	270, 28	nndivred 10605	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR )
272	30	rpge0d 11285	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( x / n ) )
273	271, 272	absidd 13266	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( x / n ) ) = ( x / n ) )
274	273	oveq2d 6312	. . . . . . . . . . . . . . 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 2498	. . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. CC )
277	87	recnd 9639	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
278	47	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x =/= 0 )
279	28	nnne0d 10601	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n =/= 0 )
280	43, 276, 277, 278, 279	divdiv2d 10373	. . . . . . . . . . . . . 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 10378	. . . . . . . . . . . . . 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 2502	. . . . . . . . . . . . 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 725	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A. y e. RR+ ( abs ` ( ( R ` y ) / y ) ) <_ B )
285		fveq2 5872	. . . . . . . . . . . . . . . . . 18 |- ( y = ( x / n ) -> ( R ` y ) = ( R ` ( x / n ) ) )
286		id 22	. . . . . . . . . . . . . . . . . 18 |- ( y = ( x / n ) -> y = ( x / n ) )
287	285, 286	oveq12d 6314	. . . . . . . . . . . . . . . . 17 |- ( y = ( x / n ) -> ( ( R ` y ) / y ) = ( ( R ` ( x / n ) ) / ( x / n ) ) )
288	287	fveq2d 5876	. . . . . . . . . . . . . . . 16 |- ( y = ( x / n ) -> ( abs ` ( ( R ` y ) / y ) ) = ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) )
289	288	breq1d 4466	. . . . . . . . . . . . . . 15 |- ( y = ( x / n ) -> ( ( abs ` ( ( R ` y ) / y ) ) <_ B <-> ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) <_ B ) )
290	289	rspcv 3206	. . . . . . . . . . . . . 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 60	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) <_ B )
292	282, 291	eqbrtrrd 4478	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( R ` ( x / n ) ) ) / x ) x. n ) <_ B )
293	264, 265, 29	lemuldivd 11326	. . . . . . . . . . . 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 210	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) / x ) <_ ( B / n ) )
295	265	recnd 9639	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> B e. CC )
296	295, 277, 279	divrec2d 10345	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( B / n ) = ( ( 1 / n ) x. B ) )
297	294, 296	breqtrd 4480	. . . . . . . . . 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 13625	. . . . . . . . 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 13613	. . . . . . . . 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 11283	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> B e. CC )
301	261	recnd 9639	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / n ) e. CC )
302	25, 300, 301	fsummulc1 13612	. . . . . . . . 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 4486	. . . . . . . 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 11285	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ B )
305		harmonicubnd 23465	. . . . . . . . . 10 |- ( ( x e. RR /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) <_ ( ( log ` x ) + 1 ) )
306	2, 9, 305	syl2anc 661	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) <_ ( ( log ` x ) + 1 ) )
307	262, 257, 259, 304, 306	lemul1ad 10505	. . . . . . . 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 9756	. . . . . . 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 10506	. . . . . 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 10376	. . . . . 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 9639	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 + ( 1 / ( log ` x ) ) ) e. CC )
312	21, 300, 311	mul32d 9807	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. B ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) = ( ( 2 x. ( 1 + ( 1 / ( log ` x ) ) ) ) x. B ) )
313		1cnd 9629	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. CC )
314	19, 313, 19, 23	divdird 10379	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) + 1 ) / ( log ` x ) ) = ( ( ( log ` x ) / ( log ` x ) ) + ( 1 / ( log ` x ) ) ) )
315	19, 23	dividd 10339	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / ( log ` x ) ) = 1 )
316	315	oveq1d 6311	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) / ( log ` x ) ) + ( 1 / ( log ` x ) ) ) = ( 1 + ( 1 / ( log ` x ) ) ) )
317	314, 316	eqtr2d 2499	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 + ( 1 / ( log ` x ) ) ) = ( ( ( log ` x ) + 1 ) / ( log ` x ) ) )
318	317	oveq2d 6312	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( 1 + ( 1 / ( log ` x ) ) ) ) = ( 2 x. ( ( ( log ` x ) + 1 ) / ( log ` x ) ) ) )
319	19, 313	addcld 9632	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) + 1 ) e. CC )
320	21, 19, 319, 23	div32d 10364	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. ( ( log ` x ) + 1 ) ) = ( 2 x. ( ( ( log ` x ) + 1 ) / ( log ` x ) ) ) )
321	318, 320	eqtr4d 2501	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( 1 + ( 1 / ( log ` x ) ) ) ) = ( ( 2 / ( log ` x ) ) x. ( ( log ` x ) + 1 ) ) )
322	321	oveq1d 6311	. . . . . . 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 9636	. . . . . . 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 2502	. . . . . 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 4486	. . . . 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 716	. . . 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 13486	. . 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 13461	. 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. <_O