Theorem pntrlog2bndlem4 21227

Description: Lemma for pntrlog2bnd 21231. 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 ) )

Assertion

Ref	Expression
pntrlog2bndlem4	|- ( 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 )

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

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

Proof of Theorem pntrlog2bndlem4

Dummy variables c m y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elioore 10902	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( 1 (,) +oo ) -> x e. RR )
2	1	adantl 453	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
3		1rp 10572	. . . . . . . . . . . . . . . . . . . 20 |- 1 e. RR+
4	3	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ )
5		1re 9046	. . . . . . . . . . . . . . . . . . . . 21 |- 1 e. RR
6	5	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR )
7		eliooord 10926	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
8	7	adantl 453	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 < x /\ x < +oo ) )
9	8	simpld 446	. . . . . . . . . . . . . . . . . . . 20 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 < x )
10	6, 2, 9	ltled 9177	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x )
11	2, 4, 10	rpgecld 10639	. . . . . . . . . . . . . . . . . 18 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
12	11	rprege0d 10611	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x e. RR /\ 0 <_ x ) )
13		flge0nn0 11180	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. RR /\ 0 <_ x ) -> ( |_ ` x ) e. NN0 )
14	12, 13	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` x ) e. NN0 )
15		nn0p1nn 10215	. . . . . . . . . . . . . . . . . . . 20 |- ( ( |_ ` x ) e. NN0 -> ( ( |_ ` x ) + 1 ) e. NN )
16	14, 15	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) e. NN )
17	16	nnrpd 10603	. . . . . . . . . . . . . . . . . 18 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) e. RR+ )
18	11, 17	rpdivcld 10621	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) e. RR+ )
19		pntrlog2bnd.r	. . . . . . . . . . . . . . . . . 18 |- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )
20	19	pntrval 21209	. . . . . . . . . . . . . . . . 17 |- ( ( x / ( ( |_ ` x ) + 1 ) ) e. RR+ -> ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) = ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) - ( x / ( ( |_ ` x ) + 1 ) ) ) )
21	18, 20	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) = ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) - ( x / ( ( |_ ` x ) + 1 ) ) ) )
22	2, 16	nndivred 10004	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) e. RR )
23		2re 10025	. . . . . . . . . . . . . . . . . . . 20 |- 2 e. RR
24	23	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 e. RR )
25		flltp1 11164	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. RR -> x < ( ( |_ ` x ) + 1 ) )
26	2, 25	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x < ( ( |_ ` x ) + 1 ) )
27	16	nncnd 9972	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) e. CC )
28	27	mulid1d 9061	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( |_ ` x ) + 1 ) x. 1 ) = ( ( |_ ` x ) + 1 ) )
29	26, 28	breqtrrd 4198	. . . . . . . . . . . . . . . . . . . 20 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x < ( ( ( |_ ` x ) + 1 ) x. 1 ) )
30	2, 6, 17	ltdivmuld 10651	. . . . . . . . . . . . . . . . . . . 20 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( x / ( ( |_ ` x ) + 1 ) ) < 1 <-> x < ( ( ( |_ ` x ) + 1 ) x. 1 ) ) )
31	29, 30	mpbird 224	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) < 1 )
32		1lt2 10098	. . . . . . . . . . . . . . . . . . . 20 |- 1 < 2
33	32	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 < 2 )
34	22, 6, 24, 31, 33	lttrd 9187	. . . . . . . . . . . . . . . . . 18 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) < 2 )
35		chpeq0 20945	. . . . . . . . . . . . . . . . . . 19 |- ( ( x / ( ( |_ ` x ) + 1 ) ) e. RR -> ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) = 0 <-> ( x / ( ( |_ ` x ) + 1 ) ) < 2 ) )
36	22, 35	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) = 0 <-> ( x / ( ( |_ ` x ) + 1 ) ) < 2 ) )
37	34, 36	mpbird 224	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) = 0 )
38	37	oveq1d 6055	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) - ( x / ( ( |_ ` x ) + 1 ) ) ) = ( 0 - ( x / ( ( |_ ` x ) + 1 ) ) ) )
39	21, 38	eqtrd 2436	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) = ( 0 - ( x / ( ( |_ ` x ) + 1 ) ) ) )
40	39	fveq2d 5691	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) = ( abs ` ( 0 - ( x / ( ( |_ ` x ) + 1 ) ) ) ) )
41		0re 9047	. . . . . . . . . . . . . . . 16 |- 0 e. RR
42	41	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 0 e. RR )
43	18	rpge0d 10608	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( x / ( ( |_ ` x ) + 1 ) ) )
44	42, 22, 43	abssuble0d 12190	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( 0 - ( x / ( ( |_ ` x ) + 1 ) ) ) ) = ( ( x / ( ( |_ ` x ) + 1 ) ) - 0 ) )
45	22	recnd 9070	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) e. CC )
46	45	subid1d 9356	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( x / ( ( |_ ` x ) + 1 ) ) - 0 ) = ( x / ( ( |_ ` x ) + 1 ) ) )
47	40, 44, 46	3eqtrd 2440	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) = ( x / ( ( |_ ` x ) + 1 ) ) )
48	14	nn0red 10231	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` x ) e. RR )
49		pntsval.1	. . . . . . . . . . . . . . . . 17 |- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) )
50	49	pntsval2 21223	. . . . . . . . . . . . . . . 16 |- ( ( |_ ` x ) e. RR -> ( S ` ( |_ ` x ) ) = sum_ n e. ( 1 ... ( |_ ` ( |_ ` x ) ) ) ( ( (Λ ` n ) x. ( log ` n ) ) + sum_ m e. { y e. NN | y || n } ( (Λ ` m ) x. (Λ ` ( n / m ) ) ) ) )
51	48, 50	syl 16	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( S ` ( |_ ` x ) ) = sum_ n e. ( 1 ... ( |_ ` ( |_ ` x ) ) ) ( ( (Λ ` n ) x. ( log ` n ) ) + sum_ m e. { y e. NN | y || n } ( (Λ ` m ) x. (Λ ` ( n / m ) ) ) ) )
52	14	nn0cnd 10232	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` x ) e. CC )
53		ax-1cn 9004	. . . . . . . . . . . . . . . . . 18 |- 1 e. CC
54	53	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. CC )
55	52, 54	pncand 9368	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( |_ ` x ) + 1 ) - 1 ) = ( |_ ` x ) )
56	55	fveq2d 5691	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) = ( S ` ( |_ ` x ) ) )
57	49	pntsval2 21223	. . . . . . . . . . . . . . . . 17 |- ( x e. RR -> ( S ` x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) x. ( log ` n ) ) + sum_ m e. { y e. NN | y || n } ( (Λ ` m ) x. (Λ ` ( n / m ) ) ) ) )
58	2, 57	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( S ` x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) x. ( log ` n ) ) + sum_ m e. { y e. NN | y || n } ( (Λ ` m ) x. (Λ ` ( n / m ) ) ) ) )
59		flidm 11172	. . . . . . . . . . . . . . . . . . 19 |- ( x e. RR -> ( |_ ` ( |_ ` x ) ) = ( |_ ` x ) )
60	2, 59	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` ( |_ ` x ) ) = ( |_ ` x ) )
61	60	oveq2d 6056	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` ( |_ ` x ) ) ) = ( 1 ... ( |_ ` x ) ) )
62	61	sumeq1d 12450	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` ( |_ ` x ) ) ) ( ( (Λ ` n ) x. ( log ` n ) ) + sum_ m e. { y e. NN | y || n } ( (Λ ` m ) x. (Λ ` ( n / m ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) x. ( log ` n ) ) + sum_ m e. { y e. NN | y || n } ( (Λ ` m ) x. (Λ ` ( n / m ) ) ) ) )
63	58, 62	eqtr4d 2439	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( S ` x ) = sum_ n e. ( 1 ... ( |_ ` ( |_ ` x ) ) ) ( ( (Λ ` n ) x. ( log ` n ) ) + sum_ m e. { y e. NN | y || n } ( (Λ ` m ) x. (Λ ` ( n / m ) ) ) ) )
64	51, 56, 63	3eqtr4d 2446	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) = ( S ` x ) )
65	55	fveq2d 5691	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) = ( T ` ( |_ ` x ) ) )
66	65	oveq2d 6056	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) = ( 2 x. ( T ` ( |_ ` x ) ) ) )
67	64, 66	oveq12d 6058	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) ) = ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) )
68	47, 67	oveq12d 6058	. . . . . . . . . . . 12 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) x. ( ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) ) ) = ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) )
69	2	recnd 9070	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. CC )
70	69	div1d 9738	. . . . . . . . . . . . . . . . . 18 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x / 1 ) = x )
71	70	fveq2d 5691	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` ( x / 1 ) ) = ( R ` x ) )
72	19	pntrf 21210	. . . . . . . . . . . . . . . . . . 19 |- R : RR+ --> RR
73	72	ffvelrni 5828	. . . . . . . . . . . . . . . . . 18 |- ( x e. RR+ -> ( R ` x ) e. RR )
74	11, 73	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) e. RR )
75	71, 74	eqeltrd 2478	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` ( x / 1 ) ) e. RR )
76	75	recnd 9070	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` ( x / 1 ) ) e. CC )
77	76	abscld 12193	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` ( x / 1 ) ) ) e. RR )
78	77	recnd 9070	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` ( x / 1 ) ) ) e. CC )
79	78	mul01d 9221	. . . . . . . . . . . 12 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` ( x / 1 ) ) ) x. 0 ) = 0 )
80	68, 79	oveq12d 6058	. . . . . . . . . . 11 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) x. ( ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) ) ) - ( ( abs ` ( R ` ( x / 1 ) ) ) x. 0 ) ) = ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) - 0 ) )
81	49	pntsf 21220	. . . . . . . . . . . . . . . . 17 |- S : RR --> RR
82	81	ffvelrni 5828	. . . . . . . . . . . . . . . 16 |- ( x e. RR -> ( S ` x ) e. RR )
83	2, 82	syl 16	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( S ` x ) e. RR )
84		pntrlog2bnd.t	. . . . . . . . . . . . . . . . . . 19 |- T = ( a e. RR |-> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) )
85		relogcl 20426	. . . . . . . . . . . . . . . . . . . . 21 |- ( a e. RR+ -> ( log ` a ) e. RR )
86		remulcl 9031	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( a e. RR /\ ( log ` a ) e. RR ) -> ( a x. ( log ` a ) ) e. RR )
87	85, 86	sylan2 461	. . . . . . . . . . . . . . . . . . . 20 |- ( ( a e. RR /\ a e. RR+ ) -> ( a x. ( log ` a ) ) e. RR )
88	41	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( a e. RR /\ -. a e. RR+ ) -> 0 e. RR )
89	87, 88	ifclda 3726	. . . . . . . . . . . . . . . . . . 19 |- ( a e. RR -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) e. RR )
90	84, 89	fmpti 5851	. . . . . . . . . . . . . . . . . 18 |- T : RR --> RR
91	90	ffvelrni 5828	. . . . . . . . . . . . . . . . 17 |- ( ( |_ ` x ) e. RR -> ( T ` ( |_ ` x ) ) e. RR )
92	48, 91	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( T ` ( |_ ` x ) ) e. RR )
93	24, 92	remulcld 9072	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( T ` ( |_ ` x ) ) ) e. RR )
94	83, 93	resubcld 9421	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) e. RR )
95	22, 94	remulcld 9072	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) e. RR )
96	95	recnd 9070	. . . . . . . . . . . 12 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) e. CC )
97	96	subid1d 9356	. . . . . . . . . . 11 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) - 0 ) = ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) )
98	80, 97	eqtrd 2436	. . . . . . . . . 10 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) x. ( ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) ) ) - ( ( abs ` ( R ` ( x / 1 ) ) ) x. 0 ) ) = ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) )
99	2	flcld 11162	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` x ) e. ZZ )
100		fzval3 11135	. . . . . . . . . . . . . 14 |- ( ( |_ ` x ) e. ZZ -> ( 1 ... ( |_ ` x ) ) = ( 1..^ ( ( |_ ` x ) + 1 ) ) )
101	99, 100	syl 16	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) = ( 1..^ ( ( |_ ` x ) + 1 ) ) )
102	101	eqcomd 2409	. . . . . . . . . . . 12 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1..^ ( ( |_ ` x ) + 1 ) ) = ( 1 ... ( |_ ` x ) ) )
103	11	adantr 452	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ )
104		elfznn 11036	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
105	104	adantl 453	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
106	105	nnrpd 10603	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
107	103, 106	rpdivcld 10621	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
108	72	ffvelrni 5828	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x / n ) e. RR+ -> ( R ` ( x / n ) ) e. RR )
109	107, 108	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. RR )
110	109	recnd 9070	. . . . . . . . . . . . . . . . . 18 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. CC )
111	110	abscld 12193	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / n ) ) ) e. RR )
112	111	recnd 9070	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / n ) ) ) e. CC )
113	3	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR+ )
114	106, 113	rpaddcld 10619	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n + 1 ) e. RR+ )
115	103, 114	rpdivcld 10621	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / ( n + 1 ) ) e. RR+ )
116	72	ffvelrni 5828	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x / ( n + 1 ) ) e. RR+ -> ( R ` ( x / ( n + 1 ) ) ) e. RR )
117	115, 116	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / ( n + 1 ) ) ) e. RR )
118	117	recnd 9070	. . . . . . . . . . . . . . . . . 18 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / ( n + 1 ) ) ) e. CC )
119	118	abscld 12193	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) e. RR )
120	119	recnd 9070	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) e. CC )
121	112, 120	negsubdi2d 9383	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> -u ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) = ( ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) - ( abs ` ( R ` ( x / n ) ) ) ) )
122	121	eqcomd 2409	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) - ( abs ` ( R ` ( x / n ) ) ) ) = -u ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) )
123	105	nncnd 9972	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
124	53	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. CC )
125	123, 124	pncand 9368	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n + 1 ) - 1 ) = n )
126	125	fveq2d 5691	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` ( ( n + 1 ) - 1 ) ) = ( S ` n ) )
127	125	fveq2d 5691	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` ( ( n + 1 ) - 1 ) ) = ( T ` n ) )
128		rpre 10574	. . . . . . . . . . . . . . . . . . . 20 |- ( n e. RR+ -> n e. RR )
129		eleq1 2464	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = n -> ( a e. RR+ <-> n e. RR+ ) )
130		id 20	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a = n -> a = n )
131		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a = n -> ( log ` a ) = ( log ` n ) )
132	130, 131	oveq12d 6058	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = n -> ( a x. ( log ` a ) ) = ( n x. ( log ` n ) ) )
133		eqidd 2405	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = n -> 0 = 0 )
134	129, 132, 133	ifbieq12d 3721	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = n -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) )
135		ovex 6065	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n x. ( log ` n ) ) e. _V
136		c0ex 9041	. . . . . . . . . . . . . . . . . . . . . 22 |- 0 e. _V
137	135, 136	ifex 3757	. . . . . . . . . . . . . . . . . . . . 21 |- if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) e. _V
138	134, 84, 137	fvmpt 5765	. . . . . . . . . . . . . . . . . . . 20 |- ( n e. RR -> ( T ` n ) = if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) )
139	128, 138	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( n e. RR+ -> ( T ` n ) = if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) )
140		iftrue 3705	. . . . . . . . . . . . . . . . . . 19 |- ( n e. RR+ -> if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) = ( n x. ( log ` n ) ) )
141	139, 140	eqtrd 2436	. . . . . . . . . . . . . . . . . 18 |- ( n e. RR+ -> ( T ` n ) = ( n x. ( log ` n ) ) )
142	106, 141	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` n ) = ( n x. ( log ` n ) ) )
143	127, 142	eqtrd 2436	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` ( ( n + 1 ) - 1 ) ) = ( n x. ( log ` n ) ) )
144	143	oveq2d 6056	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) = ( 2 x. ( n x. ( log ` n ) ) ) )
145	126, 144	oveq12d 6058	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) = ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) )
146	122, 145	oveq12d 6058	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) - ( abs ` ( R ` ( x / n ) ) ) ) x. ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) ) = ( -u ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) )
147	111, 119	resubcld 9421	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) e. RR )
148	147	recnd 9070	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) e. CC )
149	105	nnred 9971	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR )
150	81	ffvelrni 5828	. . . . . . . . . . . . . . . . 17 |- ( n e. RR -> ( S ` n ) e. RR )
151	149, 150	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` n ) e. RR )
152	23	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 2 e. RR )
153	106	relogcld 20471	. . . . . . . . . . . . . . . . . 18 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. RR )
154	149, 153	remulcld 9072	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. ( log ` n ) ) e. RR )
155	152, 154	remulcld 9072	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( n x. ( log ` n ) ) ) e. RR )
156	151, 155	resubcld 9421	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) e. RR )
157	156	recnd 9070	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) e. CC )
158	148, 157	mulneg1d 9442	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( -u ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) = -u ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) )
159	146, 158	eqtrd 2436	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) - ( abs ` ( R ` ( x / n ) ) ) ) x. ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) ) = -u ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) )
160	102, 159	sumeq12rdv 12456	. . . . . . . . . . 11 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1..^ ( ( |_ ` x ) + 1 ) ) ( ( ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) - ( abs ` ( R ` ( x / n ) ) ) ) x. ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) -u ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) )
161		fzfid 11267	. . . . . . . . . . . 12 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
162	147, 156	remulcld 9072	. . . . . . . . . . . . 13 |- ( ( ( T. /\ 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 )
163	162	recnd 9070	. . . . . . . . . . . 12 |- ( ( ( T. /\ 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 )
164	161, 163	fsumneg 12525	. . . . . . . . . . 11 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) -u ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) = -u sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) )
165	160, 164	eqtrd 2436	. . . . . . . . . 10 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1..^ ( ( |_ ` x ) + 1 ) ) ( ( ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) - ( abs ` ( R ` ( x / n ) ) ) ) x. ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) ) = -u sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) )
166	98, 165	oveq12d 6058	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) x. ( ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) ) ) - ( ( abs ` ( R ` ( x / 1 ) ) ) x. 0 ) ) - sum_ n e. ( 1..^ ( ( |_ ` x ) + 1 ) ) ( ( ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) - ( abs ` ( R ` ( x / n ) ) ) ) x. ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) ) ) = ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) - -u sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) )
167		oveq2 6048	. . . . . . . . . . . . . 14 |- ( m = n -> ( x / m ) = ( x / n ) )
168	167	fveq2d 5691	. . . . . . . . . . . . 13 |- ( m = n -> ( R ` ( x / m ) ) = ( R ` ( x / n ) ) )
169	168	fveq2d 5691	. . . . . . . . . . . 12 |- ( m = n -> ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / n ) ) ) )
170		oveq1 6047	. . . . . . . . . . . . . 14 |- ( m = n -> ( m - 1 ) = ( n - 1 ) )
171	170	fveq2d 5691	. . . . . . . . . . . . 13 |- ( m = n -> ( S ` ( m - 1 ) ) = ( S ` ( n - 1 ) ) )
172	170	fveq2d 5691	. . . . . . . . . . . . . 14 |- ( m = n -> ( T ` ( m - 1 ) ) = ( T ` ( n - 1 ) ) )
173	172	oveq2d 6056	. . . . . . . . . . . . 13 |- ( m = n -> ( 2 x. ( T ` ( m - 1 ) ) ) = ( 2 x. ( T ` ( n - 1 ) ) ) )
174	171, 173	oveq12d 6058	. . . . . . . . . . . 12 |- ( m = n -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = ( ( S ` ( n - 1 ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) )
175	169, 174	jca 519	. . . . . . . . . . 11 |- ( m = n -> ( ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / n ) ) ) /\ ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = ( ( S ` ( n - 1 ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) ) )
176		oveq2 6048	. . . . . . . . . . . . . 14 |- ( m = ( n + 1 ) -> ( x / m ) = ( x / ( n + 1 ) ) )
177	176	fveq2d 5691	. . . . . . . . . . . . 13 |- ( m = ( n + 1 ) -> ( R ` ( x / m ) ) = ( R ` ( x / ( n + 1 ) ) ) )
178	177	fveq2d 5691	. . . . . . . . . . . 12 |- ( m = ( n + 1 ) -> ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) )
179		oveq1 6047	. . . . . . . . . . . . . 14 |- ( m = ( n + 1 ) -> ( m - 1 ) = ( ( n + 1 ) - 1 ) )
180	179	fveq2d 5691	. . . . . . . . . . . . 13 |- ( m = ( n + 1 ) -> ( S ` ( m - 1 ) ) = ( S ` ( ( n + 1 ) - 1 ) ) )
181	179	fveq2d 5691	. . . . . . . . . . . . . 14 |- ( m = ( n + 1 ) -> ( T ` ( m - 1 ) ) = ( T ` ( ( n + 1 ) - 1 ) ) )
182	181	oveq2d 6056	. . . . . . . . . . . . 13 |- ( m = ( n + 1 ) -> ( 2 x. ( T ` ( m - 1 ) ) ) = ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) )
183	180, 182	oveq12d 6058	. . . . . . . . . . . 12 |- ( m = ( n + 1 ) -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) )
184	178, 183	jca 519	. . . . . . . . . . 11 |- ( m = ( n + 1 ) -> ( ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) /\ ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) ) )
185		oveq2 6048	. . . . . . . . . . . . . 14 |- ( m = 1 -> ( x / m ) = ( x / 1 ) )
186	185	fveq2d 5691	. . . . . . . . . . . . 13 |- ( m = 1 -> ( R ` ( x / m ) ) = ( R ` ( x / 1 ) ) )
187	186	fveq2d 5691	. . . . . . . . . . . 12 |- ( m = 1 -> ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / 1 ) ) ) )
188		oveq1 6047	. . . . . . . . . . . . . . . . 17 |- ( m = 1 -> ( m - 1 ) = ( 1 - 1 ) )
189	53	subidi 9327	. . . . . . . . . . . . . . . . 17 |- ( 1 - 1 ) = 0
190	188, 189	syl6eq 2452	. . . . . . . . . . . . . . . 16 |- ( m = 1 -> ( m - 1 ) = 0 )
191	190	fveq2d 5691	. . . . . . . . . . . . . . 15 |- ( m = 1 -> ( S ` ( m - 1 ) ) = ( S ` 0 ) )
192		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = 0 -> ( |_ ` a ) = ( |_ ` 0 ) )
193		0z 10249	. . . . . . . . . . . . . . . . . . . . . . 23 |- 0 e. ZZ
194		flid 11171	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 0 e. ZZ -> ( |_ ` 0 ) = 0 )
195	193, 194	ax-mp 8	. . . . . . . . . . . . . . . . . . . . . 22 |- ( |_ ` 0 ) = 0
196	192, 195	syl6eq 2452	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = 0 -> ( |_ ` a ) = 0 )
197	196	oveq2d 6056	. . . . . . . . . . . . . . . . . . . 20 |- ( a = 0 -> ( 1 ... ( |_ ` a ) ) = ( 1 ... 0 ) )
198		fz10 11031	. . . . . . . . . . . . . . . . . . . 20 |- ( 1 ... 0 ) = (/)
199	197, 198	syl6eq 2452	. . . . . . . . . . . . . . . . . . 19 |- ( a = 0 -> ( 1 ... ( |_ ` a ) ) = (/) )
200	199	sumeq1d 12450	. . . . . . . . . . . . . . . . . 18 |- ( a = 0 -> sum_ i e. ( 1 ... ( |_ ` a ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) = sum_ i e. (/) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) )
201		sum0 12470	. . . . . . . . . . . . . . . . . 18 |- sum_ i e. (/) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) = 0
202	200, 201	syl6eq 2452	. . . . . . . . . . . . . . . . 17 |- ( a = 0 -> sum_ i e. ( 1 ... ( |_ ` a ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) = 0 )
203	202, 49, 136	fvmpt 5765	. . . . . . . . . . . . . . . 16 |- ( 0 e. RR -> ( S ` 0 ) = 0 )
204	41, 203	ax-mp 8	. . . . . . . . . . . . . . 15 |- ( S ` 0 ) = 0
205	191, 204	syl6eq 2452	. . . . . . . . . . . . . 14 |- ( m = 1 -> ( S ` ( m - 1 ) ) = 0 )
206	190	fveq2d 5691	. . . . . . . . . . . . . . . . 17 |- ( m = 1 -> ( T ` ( m - 1 ) ) = ( T ` 0 ) )
207		rpne0 10583	. . . . . . . . . . . . . . . . . . . . 21 |- ( a e. RR+ -> a =/= 0 )
208	207	necon2bi 2613	. . . . . . . . . . . . . . . . . . . 20 |- ( a = 0 -> -. a e. RR+ )
209		iffalse 3706	. . . . . . . . . . . . . . . . . . . 20 |- ( -. a e. RR+ -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = 0 )
210	208, 209	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( a = 0 -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = 0 )
211	210, 84, 136	fvmpt 5765	. . . . . . . . . . . . . . . . . 18 |- ( 0 e. RR -> ( T ` 0 ) = 0 )
212	41, 211	ax-mp 8	. . . . . . . . . . . . . . . . 17 |- ( T ` 0 ) = 0
213	206, 212	syl6eq 2452	. . . . . . . . . . . . . . . 16 |- ( m = 1 -> ( T ` ( m - 1 ) ) = 0 )
214	213	oveq2d 6056	. . . . . . . . . . . . . . 15 |- ( m = 1 -> ( 2 x. ( T ` ( m - 1 ) ) ) = ( 2 x. 0 ) )
215		2cn 10026	. . . . . . . . . . . . . . . 16 |- 2 e. CC
216	215	mul01i 9212	. . . . . . . . . . . . . . 15 |- ( 2 x. 0 ) = 0
217	214, 216	syl6eq 2452	. . . . . . . . . . . . . 14 |- ( m = 1 -> ( 2 x. ( T ` ( m - 1 ) ) ) = 0 )
218	205, 217	oveq12d 6058	. . . . . . . . . . . . 13 |- ( m = 1 -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = ( 0 - 0 ) )
219		0cn 9040	. . . . . . . . . . . . . 14 |- 0 e. CC
220	219	subidi 9327	. . . . . . . . . . . . 13 |- ( 0 - 0 ) = 0
221	218, 220	syl6eq 2452	. . . . . . . . . . . 12 |- ( m = 1 -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = 0 )
222	187, 221	jca 519	. . . . . . . . . . 11 |- ( m = 1 -> ( ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / 1 ) ) ) /\ ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = 0 ) )
223		oveq2 6048	. . . . . . . . . . . . . 14 |- ( m = ( ( |_ ` x ) + 1 ) -> ( x / m ) = ( x / ( ( |_ ` x ) + 1 ) ) )
224	223	fveq2d 5691	. . . . . . . . . . . . 13 |- ( m = ( ( |_ ` x ) + 1 ) -> ( R ` ( x / m ) ) = ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) )
225	224	fveq2d 5691	. . . . . . . . . . . 12 |- ( m = ( ( |_ ` x ) + 1 ) -> ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) )
226		oveq1 6047	. . . . . . . . . . . . . 14 |- ( m = ( ( |_ ` x ) + 1 ) -> ( m - 1 ) = ( ( ( |_ ` x ) + 1 ) - 1 ) )
227	226	fveq2d 5691	. . . . . . . . . . . . 13 |- ( m = ( ( |_ ` x ) + 1 ) -> ( S ` ( m - 1 ) ) = ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) )
228	226	fveq2d 5691	. . . . . . . . . . . . . 14 |- ( m = ( ( |_ ` x ) + 1 ) -> ( T ` ( m - 1 ) ) = ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) )
229	228	oveq2d 6056	. . . . . . . . . . . . 13 |- ( m = ( ( |_ ` x ) + 1 ) -> ( 2 x. ( T ` ( m - 1 ) ) ) = ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) )
230	227, 229	oveq12d 6058	. . . . . . . . . . . 12 |- ( m = ( ( |_ ` x ) + 1 ) -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = ( ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) ) )
231	225, 230	jca 519	. . . . . . . . . . 11 |- ( m = ( ( |_ ` x ) + 1 ) -> ( ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) /\ ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = ( ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) ) ) )
232		nnuz 10477	. . . . . . . . . . . 12 |- NN = ( ZZ>= ` 1 )
233	16, 232	syl6eleq 2494	. . . . . . . . . . 11 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) e. ( ZZ>= ` 1 ) )
234	11	adantr 452	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> x e. RR+ )
235		elfznn 11036	. . . . . . . . . . . . . . . . . 18 |- ( m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) -> m e. NN )
236	235	adantl 453	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> m e. NN )
237	236	nnrpd 10603	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> m e. RR+ )
238	234, 237	rpdivcld 10621	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( x / m ) e. RR+ )
239	72	ffvelrni 5828	. . . . . . . . . . . . . . 15 |- ( ( x / m ) e. RR+ -> ( R ` ( x / m ) ) e. RR )
240	238, 239	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( R ` ( x / m ) ) e. RR )
241	240	recnd 9070	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( R ` ( x / m ) ) e. CC )
242	241	abscld 12193	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( abs ` ( R ` ( x / m ) ) ) e. RR )
243	242	recnd 9070	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( abs ` ( R ` ( x / m ) ) ) e. CC )
244	236	nnred 9971	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> m e. RR )
245	5	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> 1 e. RR )
246	244, 245	resubcld 9421	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( m - 1 ) e. RR )
247	81	ffvelrni 5828	. . . . . . . . . . . . . 14 |- ( ( m - 1 ) e. RR -> ( S ` ( m - 1 ) ) e. RR )
248	246, 247	syl 16	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( S ` ( m - 1 ) ) e. RR )
249	23	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> 2 e. RR )
250	90	ffvelrni 5828	. . . . . . . . . . . . . . 15 |- ( ( m - 1 ) e. RR -> ( T ` ( m - 1 ) ) e. RR )
251	246, 250	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( T ` ( m - 1 ) ) e. RR )
252	249, 251	remulcld 9072	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( 2 x. ( T ` ( m - 1 ) ) ) e. RR )
253	248, 252	resubcld 9421	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) e. RR )
254	253	recnd 9070	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) e. CC )
255	175, 184, 222, 231, 233, 243, 254	fsumparts 12540	. . . . . . . . . 10 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1..^ ( ( |_ ` x ) + 1 ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) - ( ( S ` ( n - 1 ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) ) ) = ( ( ( ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) x. ( ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) ) ) - ( ( abs ` ( R ` ( x / 1 ) ) ) x. 0 ) ) - sum_ n e. ( 1..^ ( ( |_ ` x ) + 1 ) ) ( ( ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) - ( abs ` ( R ` ( x / n ) ) ) ) x. ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) ) ) )
256	151	recnd 9070	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` n ) e. CC )
257	90	ffvelrni 5828	. . . . . . . . . . . . . . . . 17 |- ( n e. RR -> ( T ` n ) e. RR )
258	149, 257	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` n ) e. RR )
259	152, 258	remulcld 9072	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( T ` n ) ) e. RR )
260	259	recnd 9070	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( T ` n ) ) e. CC )
261	5	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
262	149, 261	resubcld 9421	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n - 1 ) e. RR )
263	81	ffvelrni 5828	. . . . . . . . . . . . . . . 16 |- ( ( n - 1 ) e. RR -> ( S ` ( n - 1 ) ) e. RR )
264	262, 263	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` ( n - 1 ) ) e. RR )
265	264	recnd 9070	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` ( n - 1 ) ) e. CC )
266	90	ffvelrni 5828	. . . . . . . . . . . . . . . . 17 |- ( ( n - 1 ) e. RR -> ( T ` ( n - 1 ) ) e. RR )
267	262, 266	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` ( n - 1 ) ) e. RR )
268	152, 267	remulcld 9072	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( T ` ( n - 1 ) ) ) e. RR )
269	268	recnd 9070	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( T ` ( n - 1 ) ) ) e. CC )
270	256, 260, 265, 269	sub4d 9416	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( S ` n ) - ( 2 x. ( T ` n ) ) ) - ( ( S ` ( n - 1 ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) ) = ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( ( 2 x. ( T ` n ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) ) )
271	127	oveq2d 6056	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) = ( 2 x. ( T ` n ) ) )
272	126, 271	oveq12d 6058	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) = ( ( S ` n ) - ( 2 x. ( T ` n ) ) ) )
273	272	oveq1d 6055	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) - ( ( S ` ( n - 1 ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) ) = ( ( ( S ` n ) - ( 2 x. ( T ` n ) ) ) - ( ( S ` ( n - 1 ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) ) )
274	215	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 2 e. CC )
275	258	recnd 9070	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` n ) e. CC )
276	267	recnd 9070	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` ( n - 1 ) ) e. CC )
277	274, 275, 276	subdid 9445	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) = ( ( 2 x. ( T ` n ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) )
278	277	oveq2d 6056	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) = ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( ( 2 x. ( T ` n ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) ) )
279	270, 273, 278	3eqtr4d 2446	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) - ( ( S ` ( n - 1 ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) ) = ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) )
280	279	oveq2d 6056	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) - ( ( S ` ( n - 1 ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) ) ) = ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) )
281	102, 280	sumeq12rdv 12456	. . . . . . . . . 10 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1..^ ( ( |_ ` x ) + 1 ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) - ( ( S ` ( n - 1 ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) )
282	255, 281	eqtr3d 2438	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) x. ( ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) ) ) - ( ( abs ` ( R ` ( x / 1 ) ) ) x. 0 ) ) - sum_ n e. ( 1..^ ( ( |_ ` x ) + 1 ) ) ( ( ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) - ( abs ` ( R ` ( x / n ) ) ) ) x. ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) )
283	161, 163	fsumcl 12482	. . . . . . . . . 10 |- ( ( T. /\ 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 )
284	96, 283	subnegd 9374	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) - -u 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 ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) x. ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) ) ) )
285	166, 282, 284	3eqtr3rd 2445	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) + 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 ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) )
286	11	relogcld 20471	. . . . . . . . . 10 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR )
287	286	recnd 9070	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
288	69, 287	mulcomd 9065	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) = ( ( log ` x ) x. x ) )
289	285, 288	oveq12d 6058	. . . . . . 7 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) + 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 ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / ( ( log ` x ) x. x ) ) )
290	151, 264	resubcld 9421	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` n ) - ( S ` ( n - 1 ) ) ) e. RR )
291	258, 267	resubcld 9421	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) e. RR )
292	152, 291	remulcld 9072	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) e. RR )
293	290, 292	resubcld 9421	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) e. RR )
294	111, 293	remulcld 9072	. . . . . . . . . 10 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) e. RR )
295	161, 294	fsumrecl 12483	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) e. RR )
296	295	recnd 9070	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) e. CC )
297	2, 9	rplogcld 20477	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
298	297	rpne0d 10609	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
299	11	rpne0d 10609	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x =/= 0 )
300	296, 287, 69, 298, 299	divdiv1d 9777	. . . . . . 7 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / ( log ` x ) ) / x ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / ( ( log ` x ) x. x ) ) )
301	289, 300	eqtr4d 2439	. . . . . 6 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) + 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 ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / ( log ` x ) ) / x ) )
302	301	oveq2d 6056	. . . . 5 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) / x ) + ( ( ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) + 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 ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) / x ) + ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / ( log ` x ) ) / x ) ) )
303	74	recnd 9070	. . . . . . . . . 10 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) e. CC )
304	303	abscld 12193	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` x ) ) e. RR )
305	304, 286	remulcld 9072	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) e. RR )
306	111, 290	remulcld 9072	. . . . . . . . . 10 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) e. RR )
307	161, 306	fsumrecl 12483	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) e. RR )
308	307, 297	rerpdivcld 10631	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) e. RR )
309	305, 308	resubcld 9421	. . . . . . 7 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) e. RR )
310	309	recnd 9070	. . . . . 6 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) e. CC )
311	296, 287, 298	divcld 9746	. . . . . 6 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / ( log ` x ) ) e. CC )
312	310, 311, 69, 299	divdird 9784	. . . . 5 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) + ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / ( log ` x ) ) ) / x ) = ( ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) / x ) + ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / ( log ` x ) ) / x ) ) )
313	305	recnd 9070	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) e. CC )
314	308	recnd 9070	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) e. CC )
315	313, 314, 311	subsubd 9395	. . . . . . 7 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / ( log ` x ) ) ) ) = ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) + ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) / ( log ` x ) ) ) )
316	215	a1i 11	. . . . . . . . . . . 12 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 e. CC )
317	275, 276	subcld 9367	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) e. CC )
318	112, 317	mulcld 9064	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) e. CC )
319	161, 316, 318	fsummulc2 12522	. . . . . . . . . . 11 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( 2 x. ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) )
320	290	recnd 9070	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` n ) - ( S ` ( n - 1 ) ) ) e. CC )
321	274, 317	mulcld 9064	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) e. CC )
322	320, 321	nncand 9372	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( ( ( S ` n ) - (