Theorem pntrlog2bndlem3

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

	Ref	Expression
Hypotheses	pntsval.1	|- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) )
	pntrlog2bnd.r	|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
	pntrlog2bndlem3.1	|- ( ph -> A e. RR+ )
	pntrlog2bndlem3.2	|- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( ( S ` y ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ A )
Assertion	pntrlog2bndlem3	|- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) e. O(1) )

Proof

Step	Hyp	Ref	Expression
1		pntsval.1	|- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) )
2		pntrlog2bnd.r	|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
3		pntrlog2bndlem3.1	|- ( ph -> A e. RR+ )
4		pntrlog2bndlem3.2	|- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( ( S ` y ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ A )
5		1red	|- ( ph -> 1 e. RR )
6	3	rpred	|- ( ph -> A e. RR )
7	6	adantr	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> A e. RR )
8		fzfid	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
9		elfznn	|- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
10	9	adantl	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
11	10	nnred	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR )
12		elioore	|- ( x e. ( 1 (,) +oo ) -> x e. RR )
13	12	adantl	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
14		1rp	|- 1 e. RR+
15	14	a1i	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ )
16		1red	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR )
17		eliooord	|- ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
18	17	adantl	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 < x /\ x < +oo ) )
19	18	simpld	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 < x )
20	16 13 19	ltled	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x )
21	13 15 20	rpgecld	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
22	21	adantr	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ )
23	10	nnrpd	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
24	14	a1i	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR+ )
25	23 24	rpaddcld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n + 1 ) e. RR+ )
26	22 25	rpdivcld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / ( n + 1 ) ) e. RR+ )
27	2	pntrf	|- R : RR+ --> RR
28	27	ffvelrni	|- ( ( x / ( n + 1 ) ) e. RR+ -> ( R ` ( x / ( n + 1 ) ) ) e. RR )
29	26 28	syl	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / ( n + 1 ) ) ) e. RR )
30	29	recnd	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / ( n + 1 ) ) ) e. CC )
31	22 23	rpdivcld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
32	27	ffvelrni	|- ( ( x / n ) e. RR+ -> ( R ` ( x / n ) ) e. RR )
33	31 32	syl	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. RR )
34	33	recnd	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. CC )
35	30 34	subcld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) e. CC )
36	35	abscld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) e. RR )
37	11 36	remulcld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) e. RR )
38	8 37	fsumrecl	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) e. RR )
39	13 19	rplogcld	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
40	21 39	rpmulcld	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) e. RR+ )
41	38 40	rerpdivcld	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) e. RR )
42		ioossre	|- ( 1 (,) +oo ) C_ RR
43	3	rpcnd	|- ( ph -> A e. CC )
44		o1const	|- ( ( ( 1 (,) +oo ) C_ RR /\ A e. CC ) -> ( x e. ( 1 (,) +oo ) |-> A ) e. O(1) )
45	42 43 44	sylancr	|- ( ph -> ( x e. ( 1 (,) +oo ) |-> A ) e. O(1) )
46		chpo1ubb	|- E. c e. RR+ A. y e. RR+ ( psi ` y ) <_ ( c x. y )
47		simpl	|- ( ( c e. RR+ /\ A. y e. RR+ ( psi ` y ) <_ ( c x. y ) ) -> c e. RR+ )
48		simpr	|- ( ( c e. RR+ /\ A. y e. RR+ ( psi ` y ) <_ ( c x. y ) ) -> A. y e. RR+ ( psi ` y ) <_ ( c x. y ) )
49	1 2 47 48	pntrlog2bndlem2	|- ( ( c e. RR+ /\ A. y e. RR+ ( psi ` y ) <_ ( c x. y ) ) -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) e. O(1) )
50	49	rexlimiva	|- ( E. c e. RR+ A. y e. RR+ ( psi ` y ) <_ ( c x. y ) -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) e. O(1) )
51	46 50	mp1i	|- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) e. O(1) )
52	7 41 45 51	o1mul2	|- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( A x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) ) e. O(1) )
53	7 41	remulcld	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( A x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) e. RR )
54	34	abscld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / n ) ) ) e. RR )
55	30	abscld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) e. RR )
56	54 55	resubcld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) e. RR )
57	1	pntsf	|- S : RR --> RR
58	57	ffvelrni	|- ( n e. RR -> ( S ` n ) e. RR )
59	11 58	syl	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` n ) e. RR )
60		2re	|- 2 e. RR
61	60	a1i	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 2 e. RR )
62	23	relogcld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. RR )
63	11 62	remulcld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. ( log ` n ) ) e. RR )
64	61 63	remulcld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( n x. ( log ` n ) ) ) e. RR )
65	59 64	resubcld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) e. RR )
66	56 65	remulcld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) e. RR )
67	8 66	fsumrecl	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) e. RR )
68	67 40	rerpdivcld	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) / ( x x. ( log ` x ) ) ) e. RR )
69	68	recnd	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) / ( x x. ( log ` x ) ) ) e. CC )
70	69	abscld	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) e. RR )
71	53	recnd	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( A x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) e. CC )
72	71	abscld	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( A x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) ) e. RR )
73	67	recnd	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) e. CC )
74	73	abscld	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) e. RR )
75	7 38	remulcld	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( A x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) ) e. RR )
76	66	recnd	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) e. CC )
77	76	abscld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) e. RR )
78	8 77	fsumrecl	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) e. RR )
79	8 76	fsumabs	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) )
80	7	adantr	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A e. RR )
81	80 37	remulcld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( A x. ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) ) e. RR )
82	56	recnd	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) e. CC )
83	82	abscld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) ) e. RR )
84	65	recnd	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) e. CC )
85	84	abscld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) e. RR )
86	80 11	remulcld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( A x. n ) e. RR )
87	82	absge0d	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) ) )
88	84	absge0d	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) )
89	34 30	abs2difabsd	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) ) <_ ( abs ` ( ( R ` ( x / n ) ) - ( R ` ( x / ( n + 1 ) ) ) ) ) )
90	34 30	abssubd	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / n ) ) - ( R ` ( x / ( n + 1 ) ) ) ) ) = ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) )
91	89 90	breqtrd	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) ) <_ ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) )
92	59	recnd	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` n ) e. CC )
93	11	recnd	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
94	10	nnne0d	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n =/= 0 )
95	92 93 94	divcld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` n ) / n ) e. CC )
96		2cnd	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 2 e. CC )
97	62	recnd	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. CC )
98	96 97	mulcld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( log ` n ) ) e. CC )
99	95 98	subcld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( S ` n ) / n ) - ( 2 x. ( log ` n ) ) ) e. CC )
100	99 93	absmuld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( ( S ` n ) / n ) - ( 2 x. ( log ` n ) ) ) x. n ) ) = ( ( abs ` ( ( ( S ` n ) / n ) - ( 2 x. ( log ` n ) ) ) ) x. ( abs ` n ) ) )
101	95 98 93	subdird	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( S ` n ) / n ) - ( 2 x. ( log ` n ) ) ) x. n ) = ( ( ( ( S ` n ) / n ) x. n ) - ( ( 2 x. ( log ` n ) ) x. n ) ) )
102	92 93 94	divcan1d	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( S ` n ) / n ) x. n ) = ( S ` n ) )
103	96 93 97	mul32d	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 2 x. n ) x. ( log ` n ) ) = ( ( 2 x. ( log ` n ) ) x. n ) )
104	96 93 97	mulassd	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 2 x. n ) x. ( log ` n ) ) = ( 2 x. ( n x. ( log ` n ) ) ) )
105	103 104	eqtr3d	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 2 x. ( log ` n ) ) x. n ) = ( 2 x. ( n x. ( log ` n ) ) ) )
106	102 105	oveq12d	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( S ` n ) / n ) x. n ) - ( ( 2 x. ( log ` n ) ) x. n ) ) = ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) )
107	101 106	eqtrd	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( S ` n ) / n ) - ( 2 x. ( log ` n ) ) ) x. n ) = ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) )
108	107	fveq2d	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( ( S ` n ) / n ) - ( 2 x. ( log ` n ) ) ) x. n ) ) = ( abs ` ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) )
109	23	rpge0d	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ n )
110	11 109	absidd	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` n ) = n )
111	110	oveq2d	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( ( ( S ` n ) / n ) - ( 2 x. ( log ` n ) ) ) ) x. ( abs ` n ) ) = ( ( abs ` ( ( ( S ` n ) / n ) - ( 2 x. ( log ` n ) ) ) ) x. n ) )
112	100 108 111	3eqtr3d	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) = ( ( abs ` ( ( ( S ` n ) / n ) - ( 2 x. ( log ` n ) ) ) ) x. n ) )
113	99	abscld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( S ` n ) / n ) - ( 2 x. ( log ` n ) ) ) ) e. RR )
114		fveq2	|- ( y = n -> ( S ` y ) = ( S ` n ) )
115		id	|- ( y = n -> y = n )
116	114 115	oveq12d	|- ( y = n -> ( ( S ` y ) / y ) = ( ( S ` n ) / n ) )
117		fveq2	|- ( y = n -> ( log ` y ) = ( log ` n ) )
118	117	oveq2d	|- ( y = n -> ( 2 x. ( log ` y ) ) = ( 2 x. ( log ` n ) ) )
119	116 118	oveq12d	|- ( y = n -> ( ( ( S ` y ) / y ) - ( 2 x. ( log ` y ) ) ) = ( ( ( S ` n ) / n ) - ( 2 x. ( log ` n ) ) ) )
120	119	fveq2d	|- ( y = n -> ( abs ` ( ( ( S ` y ) / y ) - ( 2 x. ( log ` y ) ) ) ) = ( abs ` ( ( ( S ` n ) / n ) - ( 2 x. ( log ` n ) ) ) ) )
121	120	breq1d	|- ( y = n -> ( ( abs ` ( ( ( S ` y ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ A <-> ( abs ` ( ( ( S ` n ) / n ) - ( 2 x. ( log ` n ) ) ) ) <_ A ) )
122	4	ad2antrr	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( ( S ` y ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ A )
123	10	nnge1d	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ n )
124		1re	|- 1 e. RR
125		elicopnf	|- ( 1 e. RR -> ( n e. ( 1 [,) +oo ) <-> ( n e. RR /\ 1 <_ n ) ) )
126	124 125	ax-mp	|- ( n e. ( 1 [,) +oo ) <-> ( n e. RR /\ 1 <_ n ) )
127	11 123 126	sylanbrc	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. ( 1 [,) +oo ) )
128	121 122 127	rspcdva	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( S ` n ) / n ) - ( 2 x. ( log ` n ) ) ) ) <_ A )
129	113 80 11 109 128	lemul1ad	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( ( ( S ` n ) / n ) - ( 2 x. ( log ` n ) ) ) ) x. n ) <_ ( A x. n ) )
130	112 129	eqbrtrd	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) <_ ( A x. n ) )
131	83 36 85 86 87 88 91 130	lemul12ad	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) ) x. ( abs ` ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) <_ ( ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) x. ( A x. n ) ) )
132	82 84	absmuld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) = ( ( abs ` ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) ) x. ( abs ` ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) )
133	43	ad2antrr	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A e. CC )
134	36	recnd	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) e. CC )
135	133 93 134	mulassd	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( A x. n ) x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) = ( A x. ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) ) )
136	133 93	mulcld	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( A x. n ) e. CC )
137	136 134	mulcomd	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( A x. n ) x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) = ( ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) x. ( A x. n ) ) )
138	135 137	eqtr3d	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( A x. ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) ) = ( ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) x. ( A x. n ) ) )
139	131 132 138	3brtr4d	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) <_ ( A x. ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) ) )
140	8 77 81 139	fsumle	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( A x. ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) ) )
141	43	adantr	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> A e. CC )
142	37	recnd	|- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) e. CC )
143	8 141 142	fsummulc2	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( A x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( A x. ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) ) )
144	140 143	breqtrrd	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) <_ ( A x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) ) )
145	74 78 75 79 144	letrd	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) <_ ( A x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) ) )
146	74 75 40 145	lediv1dd	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) / ( x x. ( log ` x ) ) ) <_ ( ( A x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) ) / ( x x. ( log ` x ) ) ) )
147	40	rpcnd	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) e. CC )
148	40	rpne0d	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) =/= 0 )
149	73 147 148	absdivd	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) = ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) / ( abs ` ( x x. ( log ` x ) ) ) ) )
150	40	rpred	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) e. RR )
151	40	rpge0d	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( x x. ( log ` x ) ) )
152	150 151	absidd	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( x x. ( log ` x ) ) ) = ( x x. ( log ` x ) ) )
153	152	oveq2d	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) / ( abs ` ( x x. ( log ` x ) ) ) ) = ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) / ( x x. ( log ` x ) ) ) )
154	149 153	eqtr2d	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) / ( x x. ( log ` x ) ) ) = ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) )
155	38	recnd	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) e. CC )
156	141 155 147 148	divassd	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( A x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) ) / ( x x. ( log ` x ) ) ) = ( A x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) )
157	146 154 156	3brtr3d	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) <_ ( A x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) )
158	53	leabsd	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( A x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) <_ ( abs ` ( A x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) ) )
159	70 53 72 157 158	letrd	|- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) <_ ( abs ` ( A x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) ) )
160	159	adantrr	|- ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ 1 <_ x ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) <_ ( abs ` ( A x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) ) )
161	5 52 53 69 160	o1le	|- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) e. O(1) )