Theorem pntrlog2bndlem5 22805

Description: Lemma for pntrlog2bnd 22808. 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 11322	. . . . . . . . . . . . 13 |- ( x e. ( 1 (,) +oo ) -> x e. RR )
2	1	adantl 466	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
3		1rp 10987	. . . . . . . . . . . . 13 |- 1 e. RR+
4	3	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ )
5		1red 9393	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR )
6		eliooord 11347	. . . . . . . . . . . . . . 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 9514	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x )
10	2, 4, 9	rpgecld 11054	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
11		pntrlog2bnd.r	. . . . . . . . . . . . 13 |- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )
12	11	pntrf 22787	. . . . . . . . . . . 12 |- R : RR+ --> RR
13	12	ffvelrni 5837	. . . . . . . . . . 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 9404	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) e. CC )
16	15	abscld 12914	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` x ) ) e. RR )
17	16	recnd 9404	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` x ) ) e. CC )
18	10	relogcld 22047	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR )
19	18	recnd 9404	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
20	17, 19	mulcld 9398	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) e. CC )
21		2cnd 10386	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 2 e. CC )
22	2, 8	rplogcld 22053	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
23	22	rpne0d 11024	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
24	21, 19, 23	divcld 10099	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 / ( log ` x ) ) e. CC )
25		fzfid 11787	. . . . . . . 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 11470	. . . . . . . . . . . . . . . 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 11018	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
30	26, 29	rpdivcld 11036	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
31	12	ffvelrni 5837	. . . . . . . . . . . . 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 9404	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. CC )
34	33	abscld 12914	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / n ) ) ) e. RR )
35	29	relogcld 22047	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. RR )
36		1red 9393	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
37	35, 36	readdcld 9405	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` n ) + 1 ) e. RR )
38	34, 37	remulcld 9406	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) e. RR )
39	38	recnd 9404	. . . . . . . 8 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( log ` n ) + 1 ) ) e. CC )
40	25, 39	fsumcl 13202	. . . . . . 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 9398	. . . . . 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 9711	. . . . 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 9404	. . . . . . 7 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / n ) ) ) e. CC )
44	25, 43	fsumcl 13202	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) e. CC )
45	24, 44	mulcld 9398	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) e. CC )
46	2	recnd 9404	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. CC )
47	10	rpne0d 11024	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x =/= 0 )
48	42, 45, 46, 47	divdird 10137	. . . 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 9406	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) e. RR )
50	49	recnd 9404	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) e. CC )
51	50, 41, 45	subsubd 9739	. . . . . 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 9792	. . . . . . . 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 13247	. . . . . . . . . 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 9404	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` n ) + 1 ) e. CC )
55		1cnd 9394	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. CC )
56	43, 54, 55	subdid 9792	. . . . . . . . . . . 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 9404	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. CC )
58	57, 55	pncand 9712	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( log ` n ) + 1 ) - 1 ) = ( log ` n ) )
59	58	oveq2d 6102	. . . . . . . . . . . 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 9395	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. 1 ) = ( abs ` ( R ` ( x / n ) ) ) )
61	60	oveq2d 6102	. . . . . . . . . . . 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 2479	. . . . . . . . . . 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 13172	. . . . . . . . . 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 2472	. . . . . . . . 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 6102	. . . . . . . 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 2472	. . . . . . 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 6102	. . . . . 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 2472	. . . . 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 6101	. . . 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 2472	. . 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 4373	. 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 10383	. . . . . . . 8 |- 2 e. RR
73	72	a1i 11	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 2 e. RR )
74	73, 22	rerpdivcld 11046	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 / ( log ` x ) ) e. RR )
75	25, 38	fsumrecl 13203	. . . . . 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 9406	. . . . 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 9768	. . . 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 11046	. . 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 13203	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) e. RR )
80	74, 79	remulcld 9406	. . . 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 11046	. . 3 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) / x ) e. RR )
82		1red 9393	. . . 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 22804	. . . . 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 10329	. . . . . . . . . . 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 22047	. . . . . . . . . . . . . . 15 |- ( ( a e. RR /\ a e. RR+ ) -> ( log ` a ) e. RR )
91	88, 90	remulcld 9406	. . . . . . . . . . . . . 14 |- ( ( a e. RR /\ a e. RR+ ) -> ( a x. ( log ` a ) ) e. RR )
92		0red 9379	. . . . . . . . . . . . . 14 |- ( ( a e. RR /\ -. a e. RR+ ) -> 0 e. RR )
93	91, 92	ifclda 3816	. . . . . . . . . . . . 13 |- ( a e. RR -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) e. RR )
94	84, 93	fmpti 5861	. . . . . . . . . . . 12 |- T : RR --> RR
95	94	ffvelrni 5837	. . . . . . . . . . 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 9768	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n - 1 ) e. RR )
98	94	ffvelrni 5837	. . . . . . . . . . 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 9768	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) e. RR )
101	34, 100	remulcld 9406	. . . . . . . 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 13203	. . . . . . 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 9406	. . . . . 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 9768	. . . . 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 11046	. . . 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 10988	. . . . . . . . . . 11 |- 2 e. RR+
107	106	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 2 e. RR+ )
108	107	rpge0d 11023	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ 2 )
109	73, 22, 108	divge0d 11055	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( 2 / ( log ` x ) ) )
110	33	absge0d 12922	. . . . . . . . . 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 11021	. . . . . . . . . . . . . . 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 9398	. . . . . . . . . . . . . 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 9377	. . . . . . . . . . . . . . . . . . 19 |- 1 e. RR
117	111	rpred 11019	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> n e. RR )
118		difrp 11016	. . . . . . . . . . . . . . . . . . 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 22047	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( log ` ( n - 1 ) ) e. RR )
122	121	recnd 9404	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( log ` ( n - 1 ) ) e. CC )
123	112, 122	mulcld 9398	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( n x. ( log ` ( n - 1 ) ) ) e. CC )
124	114, 123, 122	subsubd 9739	. . . . . . . . . . . . 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 10989	. . . . . . . . . . . . . . . . 17 |- ( n e. RR+ -> n e. RR )
126		eleq1 2498	. . . . . . . . . . . . . . . . . . 19 |- ( a = n -> ( a e. RR+ <-> n e. RR+ ) )
127		id 22	. . . . . . . . . . . . . . . . . . . 20 |- ( a = n -> a = n )
128		fveq2 5686	. . . . . . . . . . . . . . . . . . . 20 |- ( a = n -> ( log ` a ) = ( log ` n ) )
129	127, 128	oveq12d 6104	. . . . . . . . . . . . . . . . . . 19 |- ( a = n -> ( a x. ( log ` a ) ) = ( n x. ( log ` n ) ) )
130	126, 129	ifbieq1d 3807	. . . . . . . . . . . . . . . . . 18 |- ( a = n -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) )
131		ovex 6111	. . . . . . . . . . . . . . . . . . 19 |- ( n x. ( log ` n ) ) e. _V
132		c0ex 9372	. . . . . . . . . . . . . . . . . . 19 |- 0 e. _V
133	131, 132	ifex 3853	. . . . . . . . . . . . . . . . . 18 |- if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) e. _V
134	130, 84, 133	fvmpt 5769	. . . . . . . . . . . . . . . . 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 3792	. . . . . . . . . . . . . . . 16 |- ( n e. RR+ -> if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) = ( n x. ( log ` n ) ) )
137	135, 136	eqtrd 2470	. . . . . . . . . . . . . . 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 10989	. . . . . . . . . . . . . . . . . 18 |- ( ( n - 1 ) e. RR+ -> ( n - 1 ) e. RR )
140		eleq1 2498	. . . . . . . . . . . . . . . . . . . 20 |- ( a = ( n - 1 ) -> ( a e. RR+ <-> ( n - 1 ) e. RR+ ) )
141		id 22	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = ( n - 1 ) -> a = ( n - 1 ) )
142		fveq2 5686	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = ( n - 1 ) -> ( log ` a ) = ( log ` ( n - 1 ) ) )
143	141, 142	oveq12d 6104	. . . . . . . . . . . . . . . . . . . 20 |- ( a = ( n - 1 ) -> ( a x. ( log ` a ) ) = ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) )
144	140, 143	ifbieq1d 3807	. . . . . . . . . . . . . . . . . . 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 6111	. . . . . . . . . . . . . . . . . . . 20 |- ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) e. _V
146	145, 132	ifex 3853	. . . . . . . . . . . . . . . . . . 19 |- if ( ( n - 1 ) e. RR+ , ( ( n - 1 ) x. ( log ` ( n - 1 ) ) ) , 0 ) e. _V
147	144, 84, 146	fvmpt 5769	. . . . . . . . . . . . . . . . . 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 3792	. . . . . . . . . . . . . . . . 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 2470	. . . . . . . . . . . . . . . 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 9394	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> 1 e. CC )
153	112, 152, 122	subdird 9793	. . . . . . . . . . . . . . 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 9396	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( 1 x. ( log ` ( n - 1 ) ) ) = ( log ` ( n - 1 ) ) )
155	154	oveq2d 6102	. . . . . . . . . . . . . . 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 2474	. . . . . . . . . . . . . 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 6104	. . . . . . . . . . . . 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 9792	. . . . . . . . . . . . . 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 6101	. . . . . . . . . . . . 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 2480	. . . . . . . . . . . 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 22047	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( log ` n ) e. RR )
162	161, 121	resubcld 9768	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( log ` n ) - ( log ` ( n - 1 ) ) ) e. RR )
163	162	recnd 9404	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( log ` n ) - ( log ` ( n - 1 ) ) ) e. CC )
164	112, 152, 163	subdird 9793	. . . . . . . . . . . . . . 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 9396	. . . . . . . . . . . . . . . 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 6102	. . . . . . . . . . . . . . 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 9406	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( n x. ( ( log ` n ) - ( log ` ( n - 1 ) ) ) ) e. RR )
168	167	recnd 9404	. . . . . . . . . . . . . . . 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 9741	. . . . . . . . . . . . . . 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 2474	. . . . . . . . . . . . . 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 9715	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( n - 1 ) + 1 ) = n )
172	171	fveq2d 5690	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( log ` ( ( n - 1 ) + 1 ) ) = ( log ` n ) )
173	172	oveq1d 6101	. . . . . . . . . . . . . . . 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 22362	. . . . . . . . . . . . . . . . 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 4309	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( log ` n ) - ( log ` ( n - 1 ) ) ) <_ ( 1 / ( n - 1 ) ) )
177		1red 9393	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> 1 e. RR )
178	162, 177, 120	lemuldiv2d 11065	. . . . . . . . . . . . . . 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 4309	. . . . . . . . . . . . 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 9405	. . . . . . . . . . . . . 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 9930	. . . . . . . . . . . . 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 4307	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 < n ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) <_ ( ( log ` n ) + 1 ) )
185		fveq2 5686	. . . . . . . . . . . . . . . . 17 |- ( n = 1 -> ( T ` n ) = ( T ` 1 ) )
186		id 22	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = 1 -> a = 1 )
187	186, 3	syl6eqel 2526	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = 1 -> a e. RR+ )
188		iftrue 3792	. . . . . . . . . . . . . . . . . . . . 21 |- ( a e. RR+ -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = ( a x. ( log ` a ) ) )
189	187, 188	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( a = 1 -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = ( a x. ( log ` a ) ) )
190		fveq2 5686	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a = 1 -> ( log ` a ) = ( log ` 1 ) )
191		log1 22009	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( log ` 1 ) = 0
192	190, 191	syl6eq 2486	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = 1 -> ( log ` a ) = 0 )
193	186, 192	oveq12d 6104	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = 1 -> ( a x. ( log ` a ) ) = ( 1 x. 0 ) )
194		ax-1cn 9332	. . . . . . . . . . . . . . . . . . . . . 22 |- 1 e. CC
195	194	mul01i 9551	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 x. 0 ) = 0
196	193, 195	syl6eq 2486	. . . . . . . . . . . . . . . . . . . 20 |- ( a = 1 -> ( a x. ( log ` a ) ) = 0 )
197	189, 196	eqtrd 2470	. . . . . . . . . . . . . . . . . . 19 |- ( a = 1 -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = 0 )
198	197, 84, 132	fvmpt 5769	. . . . . . . . . . . . . . . . . 18 |- ( 1 e. RR -> ( T ` 1 ) = 0 )
199	116, 198	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( T ` 1 ) = 0
200	185, 199	syl6eq 2486	. . . . . . . . . . . . . . . 16 |- ( n = 1 -> ( T ` n ) = 0 )
201		oveq1 6093	. . . . . . . . . . . . . . . . . . 19 |- ( n = 1 -> ( n - 1 ) = ( 1 - 1 ) )
202		1m1e0 10382	. . . . . . . . . . . . . . . . . . 19 |- ( 1 - 1 ) = 0
203	201, 202	syl6eq 2486	. . . . . . . . . . . . . . . . . 18 |- ( n = 1 -> ( n - 1 ) = 0 )
204	203	fveq2d 5690	. . . . . . . . . . . . . . . . 17 |- ( n = 1 -> ( T ` ( n - 1 ) ) = ( T ` 0 ) )
205		0re 9378	. . . . . . . . . . . . . . . . . 18 |- 0 e. RR
206		rpne0 10998	. . . . . . . . . . . . . . . . . . . . 21 |- ( a e. RR+ -> a =/= 0 )
207	206	necon2bi 2652	. . . . . . . . . . . . . . . . . . . 20 |- ( a = 0 -> -. a e. RR+ )
208		iffalse 3794	. . . . . . . . . . . . . . . . . . . 20 |- ( -. a e. RR+ -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = 0 )
209	207, 208	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( a = 0 -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = 0 )
210	209, 84, 132	fvmpt 5769	. . . . . . . . . . . . . . . . . 18 |- ( 0 e. RR -> ( T ` 0 ) = 0 )
211	205, 210	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( T ` 0 ) = 0
212	204, 211	syl6eq 2486	. . . . . . . . . . . . . . . 16 |- ( n = 1 -> ( T ` ( n - 1 ) ) = 0 )
213	200, 212	oveq12d 6104	. . . . . . . . . . . . . . 15 |- ( n = 1 -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) = ( 0 - 0 ) )
214		0m0e0 10423	. . . . . . . . . . . . . . 15 |- ( 0 - 0 ) = 0
215	213, 214	syl6eq 2486	. . . . . . . . . . . . . 14 |- ( n = 1 -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) = 0 )
216	215	eqcoms 2441	. . . . . . . . . . . . 13 |- ( 1 = n -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) = 0 )
217	216	adantl 466	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 = n ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) = 0 )
218		0red 9379	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 e. RR )
219	28	nnge1d 10356	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ n )
220	87, 219	logge0d 22054	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( log ` n ) )
221	35	lep1d 10256	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) <_ ( ( log ` n ) + 1 ) )
222	218, 35, 37, 220, 221	letrd 9520	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( log ` n ) + 1 ) )
223	222	adantr 465	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 = n ) -> 0 <_ ( ( log ` n ) + 1 ) )
224	217, 223	eqbrtrd 4307	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ 1 = n ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) <_ ( ( log ` n ) + 1 ) )
225		elfzle1 11446	. . . . . . . . . . . . 13 |- ( n e. ( 1 ... ( |_ ` x ) ) -> 1 <_ n )
226	225	adantl 466	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ n )
227	36, 87	leloed 9509	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 <_ n <-> ( 1 < n \/ 1 = n ) ) )
228	226, 227	mpbid 210	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 < n \/ 1 = n ) )
229	184, 224, 228	mpjaodan 784	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) <_ ( ( log ` n ) + 1 ) )
230	100, 37, 34, 110, 229	lemul2ad 10265	. . . . . . . . 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 ) ) )
231	25, 101, 38, 230	fsumle 13254	. . . . . . . 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 ) ) )
232	102, 75, 74, 109, 231	lemul2ad 10265	. . . . . . 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 ) ) ) )
233	103, 76, 49, 232	lesub2dd 9948	. . . . . 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 ) ) ) ) ) ) )
234	77, 104, 10, 233	lediv1dd 11073	. . . . 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 ) )
235	234	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 ) )
236	82, 86, 105, 78, 235	lo1le 13121	. . 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) )
237	106	a1i 11	. . . . . . . 8 |- ( ph -> 2 e. RR+ )
238		pntrlog2bndlem5.1	. . . . . . . 8 |- ( ph -> B e. RR+ )
239	237, 238	rpmulcld 11035	. . . . . . 7 |- ( ph -> ( 2 x. B ) e. RR+ )
240	239	rpred 11019	. . . . . 6 |- ( ph -> ( 2 x. B ) e. RR )
241	240	adantr 465	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. B ) e. RR )
242	5, 22	rerpdivcld 11046	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 / ( log ` x ) ) e. RR )
243	5, 242	readdcld 9405	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 + ( 1 / ( log ` x ) ) ) e. RR )
244		ioossre 11349	. . . . . 6 |- ( 1 (,) +oo ) C_ RR
245		lo1const 13090	. . . . . 6 |- ( ( ( 1 (,) +oo ) C_ RR /\ ( 2 x. B ) e. RR ) -> ( x e. ( 1 (,) +oo ) |-> ( 2 x. B ) ) e. <_O(1) )
246	244, 240, 245	sylancr 663	. . . . 5 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 2 x. B ) ) e. <_O(1) )
247		lo1const 13090	. . . . . . 7 |- ( ( ( 1 (,) +oo ) C_ RR /\ 1 e. RR ) -> ( x e. ( 1 (,) +oo ) |-> 1 ) e. <_O(1) )
248	244, 82, 247	sylancr 663	. . . . . 6 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> 1 ) e. <_O(1) )
249		divlogrlim 22055	. . . . . . . 8 |- ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~> r 0
250		rlimo1 13086	. . . . . . . 8 |- ( ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~> r 0 -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O(1) )
251	249, 250	mp1i 12	. . . . . . 7 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O(1) )
252	242, 251	o1lo1d 13009	. . . . . 6 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. <_O(1) )
253	5, 242, 248, 252	lo1add 13096	. . . . 5 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 1 + ( 1 / ( log ` x ) ) ) ) e. <_O(1) )
254	239	adantr 465	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. B ) e. RR+ )
255	254	rpge0d 11023	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( 2 x. B ) )
256	241, 243, 246, 253, 255	lo1mul 13097	. . . 4 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( 2 x. B ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) ) e. <_O(1) )
257	241, 243	remulcld 9406	. . . 4 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. B ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) e. RR )
258	79, 10	rerpdivcld 11046	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) / x ) e. RR )
259	18, 5	readdcld 9405	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) + 1 ) e. RR )
260	238	adantr 465	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> B e. RR+ )
261	260	rpred 11019	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> B e. RR )
262	259, 261	remulcld 9406	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) + 1 ) x. B ) e. RR )
263	28	nnrecred 10359	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / n ) e. RR )
264	25, 263	fsumrecl 13203	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) e. RR )
265	264, 261	remulcld 9406	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) x. B ) e. RR )
266	34, 26	rerpdivcld 11046	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) / x ) e. RR )
267	261	adantr 465	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> B e. RR )
268	263, 267	remulcld 9406	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 / n ) x. B ) e. RR )
269	30	rpcnd 11021	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. CC )
270	30	rpne0d 11024	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) =/= 0 )
271	33, 269, 270	absdivd 12933	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) = ( ( abs ` ( R ` ( x / n ) ) ) / ( abs ` ( x / n ) ) ) )
272	2	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR )
273	272, 28	nndivred 10362	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR )
274	30	rpge0d 11023	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( x / n ) )
275	273, 274	absidd 12901	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( x / n ) ) = ( x / n ) )
276	275	oveq2d 6102	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) / ( abs ` ( x / n ) ) ) = ( ( abs ` ( R ` ( x / n ) ) ) / ( x / n ) ) )
277	271, 276	eqtrd 2470	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) = ( ( abs ` ( R ` ( x / n ) ) ) / ( x / n ) ) )
278	46	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. CC )
279	87	recnd 9404	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
280	47	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x =/= 0 )
281	28	nnne0d 10358	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n =/= 0 )
282	43, 278, 279, 280, 281	divdiv2d 10131	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) / ( x / n ) ) = ( ( ( abs ` ( R ` ( x / n ) ) ) x. n ) / x ) )
283	43, 279, 278, 280	div23d 10136	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( R ` ( x / n ) ) ) x. n ) / x ) = ( ( ( abs ` ( R ` ( x / n ) ) ) / x ) x. n ) )
284	277, 282, 283	3eqtrd 2474	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) = ( ( ( abs ` ( R ` ( x / n ) ) ) / x ) x. n ) )
285		pntrlog2bndlem5.2	. . . . . . . . . . . . . . 15 |- ( ph -> A. y e. RR+ ( abs ` ( ( R ` y ) / y ) ) <_ B )
286	285	ad2antrr 725	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A. y e. RR+ ( abs ` ( ( R ` y ) / y ) ) <_ B )
287		fveq2 5686	. . . . . . . . . . . . . . . . . 18 |- ( y = ( x / n ) -> ( R ` y ) = ( R ` ( x / n ) ) )
288		id 22	. . . . . . . . . . . . . . . . . 18 |- ( y = ( x / n ) -> y = ( x / n ) )
289	287, 288	oveq12d 6104	. . . . . . . . . . . . . . . . 17 |- ( y = ( x / n ) -> ( ( R ` y ) / y ) = ( ( R ` ( x / n ) ) / ( x / n ) ) )
290	289	fveq2d 5690	. . . . . . . . . . . . . . . 16 |- ( y = ( x / n ) -> ( abs ` ( ( R ` y ) / y ) ) = ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) )
291	290	breq1d 4297	. . . . . . . . . . . . . . 15 |- ( y = ( x / n ) -> ( ( abs ` ( ( R ` y ) / y ) ) <_ B <-> ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) <_ B ) )
292	291	rspcv 3064	. . . . . . . . . . . . . 14 |- ( ( x / n ) e. RR+ -> ( A. y e. RR+ ( abs ` ( ( R ` y ) / y ) ) <_ B -> ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) <_ B ) )
293	30, 286, 292	sylc 60	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / n ) ) / ( x / n ) ) ) <_ B )
294	284, 293	eqbrtrrd 4309	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( R ` ( x / n ) ) ) / x ) x. n ) <_ B )
295	266, 267, 29	lemuldivd 11064	. . . . . . . . . . . 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 ) ) )
296	294, 295	mpbid 210	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) / x ) <_ ( B / n ) )
297	267	recnd 9404	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> B e. CC )
298	297, 279, 281	divrec2d 10103	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( B / n ) = ( ( 1 / n ) x. B ) )
299	296, 298	breqtrd 4311	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) / x ) <_ ( ( 1 / n ) x. B ) )
300	25, 266, 268, 299	fsumle 13254	. . . . . . . . 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 ) )
301	25, 46, 43, 47	fsumdivc 13245	. . . . . . . . 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 ) )
302	260	rpcnd 11021	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> B e. CC )
303	263	recnd 9404	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / n ) e. CC )
304	25, 302, 303	fsummulc1 13244	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) x. B ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 / n ) x. B ) )
305	300, 301, 304	3brtr4d 4317	. . . . . . . 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 ) )
306	260	rpge0d 11023	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ B )
307		harmonicubnd 22378	. . . . . . . . . 10 |- ( ( x e. RR /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) <_ ( ( log ` x ) + 1 ) )
308	2, 9, 307	syl2anc 661	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) <_ ( ( log ` x ) + 1 ) )
309	264, 259, 261, 306, 308	lemul1ad 10264	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) x. B ) <_ ( ( ( log ` x ) + 1 ) x. B ) )
310	258, 265, 262, 305, 309	letrd 9520	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) / x ) <_ ( ( ( log ` x ) + 1 ) x. B ) )
311	258, 262, 74, 109, 310	lemul2ad 10265	. . . . . 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 ) ) )
312	24, 44, 46, 47	divassd 10134	. . . . . 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 ) ) )
313	243	recnd 9404	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 + ( 1 / ( log ` x ) ) ) e. CC )
314	21, 302, 313	mul32d 9571	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. B ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) = ( ( 2 x. ( 1 + ( 1 / ( log ` x ) ) ) ) x. B ) )
315		1cnd 9394	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. CC )
316	19, 315, 19, 23	divdird 10137	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) + 1 ) / ( log ` x ) ) = ( ( ( log ` x ) / ( log ` x ) ) + ( 1 / ( log ` x ) ) ) )
317	19, 23	dividd 10097	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / ( log ` x ) ) = 1 )
318	317	oveq1d 6101	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) / ( log ` x ) ) + ( 1 / ( log ` x ) ) ) = ( 1 + ( 1 / ( log ` x ) ) ) )
319	316, 318	eqtr2d 2471	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 + ( 1 / ( log ` x ) ) ) = ( ( ( log ` x ) + 1 ) / ( log ` x ) ) )
320	319	oveq2d 6102	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( 1 + ( 1 / ( log ` x ) ) ) ) = ( 2 x. ( ( ( log ` x ) + 1 ) / ( log ` x ) ) ) )
321	19, 315	addcld 9397	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) + 1 ) e. CC )
322	21, 19, 321, 23	div32d 10122	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. ( ( log ` x ) + 1 ) ) = ( 2 x. ( ( ( log ` x ) + 1 ) / ( log ` x ) ) ) )
323	320, 322	eqtr4d 2473	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( 1 + ( 1 / ( log ` x ) ) ) ) = ( ( 2 / ( log ` x ) ) x. ( ( log ` x ) + 1 ) ) )
324	323	oveq1d 6101	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. ( 1 + ( 1 / ( log ` x ) ) ) ) x. B ) = ( ( ( 2 / ( log ` x ) ) x. ( ( log ` x ) + 1 ) ) x. B ) )
325	24, 321, 302	mulassd 9401	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. ( ( log ` x ) + 1 ) ) x. B ) = ( ( 2 / ( log ` x ) ) x. ( ( ( log ` x ) + 1 ) x. B ) ) )
326	314, 324, 325	3eqtrd 2474	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. B ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) = ( ( 2 / ( log ` x ) ) x. ( ( ( log ` x ) + 1 ) x. B ) ) )
327	311, 312, 326	3brtr4d 4317	. . . . 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 ) ) ) ) )
328	327	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 ) ) ) ) )
329	82, 256, 257, 81, 328	lo1le 13121	. . 3 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( R ` ( x / n ) ) ) ) / x ) ) e. <_O(1) )
330	78, 81, 236, 329	lo1add 13096	. 2 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs