Theorem pntrlog2bndlem4 24474

Description: Lemma for pntrlog2bnd 24478. 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 11700	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( 1 (,) +oo ) -> x e. RR )
2	1	adantl 472	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
3		1rp 11340	. . . . . . . . . . . . . . . . . . . 20 |- 1 e. RR+
4	3	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ )
5		1red 9689	. . . . . . . . . . . . . . . . . . . 20 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR )
6		eliooord 11728	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
7	6	adantl 472	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 < x /\ x < +oo ) )
8	7	simpld 465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 < x )
9	5, 2, 8	ltled 9814	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x )
10	2, 4, 9	rpgecld 11411	. . . . . . . . . . . . . . . . . 18 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
11	10	rprege0d 11382	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x e. RR /\ 0 <_ x ) )
12		flge0nn0 12092	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. RR /\ 0 <_ x ) -> ( |_ ` x ) e. NN0 )
13	11, 12	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` x ) e. NN0 )
14		nn0p1nn 10943	. . . . . . . . . . . . . . . . . . . 20 |- ( ( |_ ` x ) e. NN0 -> ( ( |_ ` x ) + 1 ) e. NN )
15	13, 14	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) e. NN )
16	15	nnrpd 11373	. . . . . . . . . . . . . . . . . 18 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) e. RR+ )
17	10, 16	rpdivcld 11392	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) e. RR+ )
18		pntrlog2bnd.r	. . . . . . . . . . . . . . . . . 18 |- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )
19	18	pntrval 24456	. . . . . . . . . . . . . . . . 17 |- ( ( x / ( ( |_ ` x ) + 1 ) ) e. RR+ -> ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) = ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) - ( x / ( ( |_ ` x ) + 1 ) ) ) )
20	17, 19	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) = ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) - ( x / ( ( |_ ` x ) + 1 ) ) ) )
21	2, 15	nndivred 10691	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) e. RR )
22		2re 10712	. . . . . . . . . . . . . . . . . . . 20 |- 2 e. RR
23	22	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 e. RR )
24		flltp1 12074	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. RR -> x < ( ( |_ ` x ) + 1 ) )
25	2, 24	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x < ( ( |_ ` x ) + 1 ) )
26	15	nncnd 10658	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) e. CC )
27	26	mulid1d 9691	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( |_ ` x ) + 1 ) x. 1 ) = ( ( |_ ` x ) + 1 ) )
28	25, 27	breqtrrd 4445	. . . . . . . . . . . . . . . . . . . 20 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x < ( ( ( |_ ` x ) + 1 ) x. 1 ) )
29	2, 5, 16	ltdivmuld 11423	. . . . . . . . . . . . . . . . . . . 20 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( x / ( ( |_ ` x ) + 1 ) ) < 1 <-> x < ( ( ( |_ ` x ) + 1 ) x. 1 ) ) )
30	28, 29	mpbird 240	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) < 1 )
31		1lt2 10810	. . . . . . . . . . . . . . . . . . . 20 |- 1 < 2
32	31	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 < 2 )
33	21, 5, 23, 30, 32	lttrd 9827	. . . . . . . . . . . . . . . . . 18 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) < 2 )
34		chpeq0 24192	. . . . . . . . . . . . . . . . . . 19 |- ( ( x / ( ( |_ ` x ) + 1 ) ) e. RR -> ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) = 0 <-> ( x / ( ( |_ ` x ) + 1 ) ) < 2 ) )
35	21, 34	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) = 0 <-> ( x / ( ( |_ ` x ) + 1 ) ) < 2 ) )
36	33, 35	mpbird 240	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) = 0 )
37	36	oveq1d 6335	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) - ( x / ( ( |_ ` x ) + 1 ) ) ) = ( 0 - ( x / ( ( |_ ` x ) + 1 ) ) ) )
38	20, 37	eqtrd 2496	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) = ( 0 - ( x / ( ( |_ ` x ) + 1 ) ) ) )
39	38	fveq2d 5896	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) = ( abs ` ( 0 - ( x / ( ( |_ ` x ) + 1 ) ) ) ) )
40		0red 9675	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 0 e. RR )
41	17	rpge0d 11379	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( x / ( ( |_ ` x ) + 1 ) ) )
42	40, 21, 41	abssuble0d 13549	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( 0 - ( x / ( ( |_ ` x ) + 1 ) ) ) ) = ( ( x / ( ( |_ ` x ) + 1 ) ) - 0 ) )
43	21	recnd 9700	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) e. CC )
44	43	subid1d 10006	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( x / ( ( |_ ` x ) + 1 ) ) - 0 ) = ( x / ( ( |_ ` x ) + 1 ) ) )
45	39, 42, 44	3eqtrd 2500	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) = ( x / ( ( |_ ` x ) + 1 ) ) )
46	13	nn0red 10960	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` x ) e. RR )
47		pntsval.1	. . . . . . . . . . . . . . . . 17 |- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) )
48	47	pntsval2 24470	. . . . . . . . . . . . . . . 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 ) ) ) ) )
49	46, 48	syl 17	. . . . . . . . . . . . . . 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 ) ) ) ) )
50	13	nn0cnd 10961	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` x ) e. CC )
51		1cnd 9690	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. CC )
52	50, 51	pncand 10018	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( |_ ` x ) + 1 ) - 1 ) = ( |_ ` x ) )
53	52	fveq2d 5896	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) = ( S ` ( |_ ` x ) ) )
54	47	pntsval2 24470	. . . . . . . . . . . . . . . . 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 ) ) ) ) )
55	2, 54	syl 17	. . . . . . . . . . . . . . . 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 ) ) ) ) )
56		flidm 12083	. . . . . . . . . . . . . . . . . . 19 |- ( x e. RR -> ( |_ ` ( |_ ` x ) ) = ( |_ ` x ) )
57	2, 56	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` ( |_ ` x ) ) = ( |_ ` x ) )
58	57	oveq2d 6336	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` ( |_ ` x ) ) ) = ( 1 ... ( |_ ` x ) ) )
59	58	sumeq1d 13822	. . . . . . . . . . . . . . . 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 ) ) ) ) )
60	55, 59	eqtr4d 2499	. . . . . . . . . . . . . . 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 ) ) ) ) )
61	49, 53, 60	3eqtr4d 2506	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) = ( S ` x ) )
62	52	fveq2d 5896	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) = ( T ` ( |_ ` x ) ) )
63	62	oveq2d 6336	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) = ( 2 x. ( T ` ( |_ ` x ) ) ) )
64	61, 63	oveq12d 6338	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) ) = ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) )
65	45, 64	oveq12d 6338	. . . . . . . . . . . 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 ) ) ) ) ) )
66	2	recnd 9700	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. CC )
67	66	div1d 10408	. . . . . . . . . . . . . . . . . 18 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x / 1 ) = x )
68	67	fveq2d 5896	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` ( x / 1 ) ) = ( R ` x ) )
69	18	pntrf 24457	. . . . . . . . . . . . . . . . . . 19 |- R : RR+ --> RR
70	69	ffvelrni 6049	. . . . . . . . . . . . . . . . . 18 |- ( x e. RR+ -> ( R ` x ) e. RR )
71	10, 70	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) e. RR )
72	68, 71	eqeltrd 2540	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` ( x / 1 ) ) e. RR )
73	72	recnd 9700	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` ( x / 1 ) ) e. CC )
74	73	abscld 13553	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` ( x / 1 ) ) ) e. RR )
75	74	recnd 9700	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` ( x / 1 ) ) ) e. CC )
76	75	mul01d 9863	. . . . . . . . . . . 12 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` ( x / 1 ) ) ) x. 0 ) = 0 )
77	65, 76	oveq12d 6338	. . . . . . . . . . 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 ) )
78	47	pntsf 24467	. . . . . . . . . . . . . . . . 17 |- S : RR --> RR
79	78	ffvelrni 6049	. . . . . . . . . . . . . . . 16 |- ( x e. RR -> ( S ` x ) e. RR )
80	2, 79	syl 17	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( S ` x ) e. RR )
81		pntrlog2bnd.t	. . . . . . . . . . . . . . . . . . 19 |- T = ( a e. RR |-> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) )
82		relogcl 23581	. . . . . . . . . . . . . . . . . . . . 21 |- ( a e. RR+ -> ( log ` a ) e. RR )
83		remulcl 9655	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( a e. RR /\ ( log ` a ) e. RR ) -> ( a x. ( log ` a ) ) e. RR )
84	82, 83	sylan2 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( a e. RR /\ a e. RR+ ) -> ( a x. ( log ` a ) ) e. RR )
85		0red 9675	. . . . . . . . . . . . . . . . . . . 20 |- ( ( a e. RR /\ -. a e. RR+ ) -> 0 e. RR )
86	84, 85	ifclda 3925	. . . . . . . . . . . . . . . . . . 19 |- ( a e. RR -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) e. RR )
87	81, 86	fmpti 6073	. . . . . . . . . . . . . . . . . 18 |- T : RR --> RR
88	87	ffvelrni 6049	. . . . . . . . . . . . . . . . 17 |- ( ( |_ ` x ) e. RR -> ( T ` ( |_ ` x ) ) e. RR )
89	46, 88	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( T ` ( |_ ` x ) ) e. RR )
90	23, 89	remulcld 9702	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( T ` ( |_ ` x ) ) ) e. RR )
91	80, 90	resubcld 10080	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) e. RR )
92	21, 91	remulcld 9702	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) e. RR )
93	92	recnd 9700	. . . . . . . . . . . 12 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) e. CC )
94	93	subid1d 10006	. . . . . . . . . . 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 ) ) ) ) ) )
95	77, 94	eqtrd 2496	. . . . . . . . . 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 ) ) ) ) ) )
96	2	flcld 12072	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` x ) e. ZZ )
97		fzval3 12020	. . . . . . . . . . . . . 14 |- ( ( |_ ` x ) e. ZZ -> ( 1 ... ( |_ ` x ) ) = ( 1..^ ( ( |_ ` x ) + 1 ) ) )
98	96, 97	syl 17	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) = ( 1..^ ( ( |_ ` x ) + 1 ) ) )
99	98	eqcomd 2468	. . . . . . . . . . . 12 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1..^ ( ( |_ ` x ) + 1 ) ) = ( 1 ... ( |_ ` x ) ) )
100	10	adantr 471	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ )
101		elfznn 11863	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
102	101	adantl 472	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
103	102	nnrpd 11373	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
104	100, 103	rpdivcld 11392	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
105	69	ffvelrni 6049	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x / n ) e. RR+ -> ( R ` ( x / n ) ) e. RR )
106	104, 105	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. RR )
107	106	recnd 9700	. . . . . . . . . . . . . . . . . 18 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. CC )
108	107	abscld 13553	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / n ) ) ) e. RR )
109	108	recnd 9700	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / n ) ) ) e. CC )
110	3	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR+ )
111	103, 110	rpaddcld 11390	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n + 1 ) e. RR+ )
112	100, 111	rpdivcld 11392	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / ( n + 1 ) ) e. RR+ )
113	69	ffvelrni 6049	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x / ( n + 1 ) ) e. RR+ -> ( R ` ( x / ( n + 1 ) ) ) e. RR )
114	112, 113	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / ( n + 1 ) ) ) e. RR )
115	114	recnd 9700	. . . . . . . . . . . . . . . . . 18 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / ( n + 1 ) ) ) e. CC )
116	115	abscld 13553	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) e. RR )
117	116	recnd 9700	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) e. CC )
118	109, 117	negsubdi2d 10033	. . . . . . . . . . . . . . 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 ) ) ) ) )
119	118	eqcomd 2468	. . . . . . . . . . . . . 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 ) ) ) ) ) )
120	102	nncnd 10658	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
121		1cnd 9690	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. CC )
122	120, 121	pncand 10018	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n + 1 ) - 1 ) = n )
123	122	fveq2d 5896	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` ( ( n + 1 ) - 1 ) ) = ( S ` n ) )
124	122	fveq2d 5896	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` ( ( n + 1 ) - 1 ) ) = ( T ` n ) )
125		rpre 11342	. . . . . . . . . . . . . . . . . . . 20 |- ( n e. RR+ -> n e. RR )
126		eleq1 2528	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = n -> ( a e. RR+ <-> n e. RR+ ) )
127		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a = n -> a = n )
128		fveq2 5892	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a = n -> ( log ` a ) = ( log ` n ) )
129	127, 128	oveq12d 6338	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = n -> ( a x. ( log ` a ) ) = ( n x. ( log ` n ) ) )
130	126, 129	ifbieq1d 3916	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = n -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) )
131		ovex 6348	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n x. ( log ` n ) ) e. _V
132		c0ex 9668	. . . . . . . . . . . . . . . . . . . . . 22 |- 0 e. _V
133	131, 132	ifex 3961	. . . . . . . . . . . . . . . . . . . . 21 |- if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) e. _V
134	130, 81, 133	fvmpt 5976	. . . . . . . . . . . . . . . . . . . 20 |- ( n e. RR -> ( T ` n ) = if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) )
135	125, 134	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( n e. RR+ -> ( T ` n ) = if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) )
136		iftrue 3899	. . . . . . . . . . . . . . . . . . 19 |- ( n e. RR+ -> if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) = ( n x. ( log ` n ) ) )
137	135, 136	eqtrd 2496	. . . . . . . . . . . . . . . . . 18 |- ( n e. RR+ -> ( T ` n ) = ( n x. ( log ` n ) ) )
138	103, 137	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` n ) = ( n x. ( log ` n ) ) )
139	124, 138	eqtrd 2496	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` ( ( n + 1 ) - 1 ) ) = ( n x. ( log ` n ) ) )
140	139	oveq2d 6336	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) = ( 2 x. ( n x. ( log ` n ) ) ) )
141	123, 140	oveq12d 6338	. . . . . . . . . . . . . 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 ) ) ) ) )
142	119, 141	oveq12d 6338	. . . . . . . . . . . . 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 ) ) ) ) ) )
143	108, 116	resubcld 10080	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) e. RR )
144	143	recnd 9700	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) e. CC )
145	102	nnred 10657	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR )
146	78	ffvelrni 6049	. . . . . . . . . . . . . . . . 17 |- ( n e. RR -> ( S ` n ) e. RR )
147	145, 146	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` n ) e. RR )
148	22	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 2 e. RR )
149	103	relogcld 23628	. . . . . . . . . . . . . . . . . 18 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. RR )
150	145, 149	remulcld 9702	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. ( log ` n ) ) e. RR )
151	148, 150	remulcld 9702	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( n x. ( log ` n ) ) ) e. RR )
152	147, 151	resubcld 10080	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) e. RR )
153	152	recnd 9700	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) e. CC )
154	144, 153	mulneg1d 10104	. . . . . . . . . . . . 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 ) ) ) ) ) )
155	142, 154	eqtrd 2496	. . . . . . . . . . . 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 ) ) ) ) ) )
156	99, 155	sumeq12rdv 13828	. . . . . . . . . . 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 ) ) ) ) ) )
157		fzfid 12224	. . . . . . . . . . . 12 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
158	143, 152	remulcld 9702	. . . . . . . . . . . . 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 )
159	158	recnd 9700	. . . . . . . . . . . 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 )
160	157, 159	fsumneg 13903	. . . . . . . . . . 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 ) ) ) ) ) )
161	156, 160	eqtrd 2496	. . . . . . . . . 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 ) ) ) ) ) )
162	95, 161	oveq12d 6338	. . . . . . . . 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 ) ) ) ) ) ) )
163		oveq2 6328	. . . . . . . . . . . . . 14 |- ( m = n -> ( x / m ) = ( x / n ) )
164	163	fveq2d 5896	. . . . . . . . . . . . 13 |- ( m = n -> ( R ` ( x / m ) ) = ( R ` ( x / n ) ) )
165	164	fveq2d 5896	. . . . . . . . . . . 12 |- ( m = n -> ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / n ) ) ) )
166		oveq1 6327	. . . . . . . . . . . . . 14 |- ( m = n -> ( m - 1 ) = ( n - 1 ) )
167	166	fveq2d 5896	. . . . . . . . . . . . 13 |- ( m = n -> ( S ` ( m - 1 ) ) = ( S ` ( n - 1 ) ) )
168	166	fveq2d 5896	. . . . . . . . . . . . . 14 |- ( m = n -> ( T ` ( m - 1 ) ) = ( T ` ( n - 1 ) ) )
169	168	oveq2d 6336	. . . . . . . . . . . . 13 |- ( m = n -> ( 2 x. ( T ` ( m - 1 ) ) ) = ( 2 x. ( T ` ( n - 1 ) ) ) )
170	167, 169	oveq12d 6338	. . . . . . . . . . . 12 |- ( m = n -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = ( ( S ` ( n - 1 ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) )
171	165, 170	jca 539	. . . . . . . . . . 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 ) ) ) ) ) )
172		oveq2 6328	. . . . . . . . . . . . . 14 |- ( m = ( n + 1 ) -> ( x / m ) = ( x / ( n + 1 ) ) )
173	172	fveq2d 5896	. . . . . . . . . . . . 13 |- ( m = ( n + 1 ) -> ( R ` ( x / m ) ) = ( R ` ( x / ( n + 1 ) ) ) )
174	173	fveq2d 5896	. . . . . . . . . . . 12 |- ( m = ( n + 1 ) -> ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) )
175		oveq1 6327	. . . . . . . . . . . . . 14 |- ( m = ( n + 1 ) -> ( m - 1 ) = ( ( n + 1 ) - 1 ) )
176	175	fveq2d 5896	. . . . . . . . . . . . 13 |- ( m = ( n + 1 ) -> ( S ` ( m - 1 ) ) = ( S ` ( ( n + 1 ) - 1 ) ) )
177	175	fveq2d 5896	. . . . . . . . . . . . . 14 |- ( m = ( n + 1 ) -> ( T ` ( m - 1 ) ) = ( T ` ( ( n + 1 ) - 1 ) ) )
178	177	oveq2d 6336	. . . . . . . . . . . . 13 |- ( m = ( n + 1 ) -> ( 2 x. ( T ` ( m - 1 ) ) ) = ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) )
179	176, 178	oveq12d 6338	. . . . . . . . . . . 12 |- ( m = ( n + 1 ) -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = ( ( S ` ( ( n + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) ) )
180	174, 179	jca 539	. . . . . . . . . . 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 ) ) ) ) ) )
181		oveq2 6328	. . . . . . . . . . . . . 14 |- ( m = 1 -> ( x / m ) = ( x / 1 ) )
182	181	fveq2d 5896	. . . . . . . . . . . . 13 |- ( m = 1 -> ( R ` ( x / m ) ) = ( R ` ( x / 1 ) ) )
183	182	fveq2d 5896	. . . . . . . . . . . 12 |- ( m = 1 -> ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / 1 ) ) ) )
184		oveq1 6327	. . . . . . . . . . . . . . . . 17 |- ( m = 1 -> ( m - 1 ) = ( 1 - 1 ) )
185		1m1e0 10711	. . . . . . . . . . . . . . . . 17 |- ( 1 - 1 ) = 0
186	184, 185	syl6eq 2512	. . . . . . . . . . . . . . . 16 |- ( m = 1 -> ( m - 1 ) = 0 )
187	186	fveq2d 5896	. . . . . . . . . . . . . . 15 |- ( m = 1 -> ( S ` ( m - 1 ) ) = ( S ` 0 ) )
188		0re 9674	. . . . . . . . . . . . . . . 16 |- 0 e. RR
189		fveq2 5892	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = 0 -> ( |_ ` a ) = ( |_ ` 0 ) )
190		0z 10982	. . . . . . . . . . . . . . . . . . . . . . 23 |- 0 e. ZZ
191		flid 12082	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 0 e. ZZ -> ( |_ ` 0 ) = 0 )
192	190, 191	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 |- ( |_ ` 0 ) = 0
193	189, 192	syl6eq 2512	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = 0 -> ( |_ ` a ) = 0 )
194	193	oveq2d 6336	. . . . . . . . . . . . . . . . . . . 20 |- ( a = 0 -> ( 1 ... ( |_ ` a ) ) = ( 1 ... 0 ) )
195		fz10 11855	. . . . . . . . . . . . . . . . . . . 20 |- ( 1 ... 0 ) = (/)
196	194, 195	syl6eq 2512	. . . . . . . . . . . . . . . . . . 19 |- ( a = 0 -> ( 1 ... ( |_ ` a ) ) = (/) )
197	196	sumeq1d 13822	. . . . . . . . . . . . . . . . . 18 |- ( a = 0 -> sum_ i e. ( 1 ... ( |_ ` a ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) = sum_ i e. (/) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) )
198		sum0 13842	. . . . . . . . . . . . . . . . . 18 |- sum_ i e. (/) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) = 0
199	197, 198	syl6eq 2512	. . . . . . . . . . . . . . . . 17 |- ( a = 0 -> sum_ i e. ( 1 ... ( |_ ` a ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) = 0 )
200	199, 47, 132	fvmpt 5976	. . . . . . . . . . . . . . . 16 |- ( 0 e. RR -> ( S ` 0 ) = 0 )
201	188, 200	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( S ` 0 ) = 0
202	187, 201	syl6eq 2512	. . . . . . . . . . . . . 14 |- ( m = 1 -> ( S ` ( m - 1 ) ) = 0 )
203	186	fveq2d 5896	. . . . . . . . . . . . . . . . 17 |- ( m = 1 -> ( T ` ( m - 1 ) ) = ( T ` 0 ) )
204		rpne0 11351	. . . . . . . . . . . . . . . . . . . . 21 |- ( a e. RR+ -> a =/= 0 )
205	204	necon2bi 2666	. . . . . . . . . . . . . . . . . . . 20 |- ( a = 0 -> -. a e. RR+ )
206	205	iffalsed 3904	. . . . . . . . . . . . . . . . . . 19 |- ( a = 0 -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = 0 )
207	206, 81, 132	fvmpt 5976	. . . . . . . . . . . . . . . . . 18 |- ( 0 e. RR -> ( T ` 0 ) = 0 )
208	188, 207	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( T ` 0 ) = 0
209	203, 208	syl6eq 2512	. . . . . . . . . . . . . . . 16 |- ( m = 1 -> ( T ` ( m - 1 ) ) = 0 )
210	209	oveq2d 6336	. . . . . . . . . . . . . . 15 |- ( m = 1 -> ( 2 x. ( T ` ( m - 1 ) ) ) = ( 2 x. 0 ) )
211		2t0e0 10799	. . . . . . . . . . . . . . 15 |- ( 2 x. 0 ) = 0
212	210, 211	syl6eq 2512	. . . . . . . . . . . . . 14 |- ( m = 1 -> ( 2 x. ( T ` ( m - 1 ) ) ) = 0 )
213	202, 212	oveq12d 6338	. . . . . . . . . . . . 13 |- ( m = 1 -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = ( 0 - 0 ) )
214		0m0e0 10752	. . . . . . . . . . . . 13 |- ( 0 - 0 ) = 0
215	213, 214	syl6eq 2512	. . . . . . . . . . . 12 |- ( m = 1 -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = 0 )
216	183, 215	jca 539	. . . . . . . . . . 11 |- ( m = 1 -> ( ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / 1 ) ) ) /\ ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = 0 ) )
217		oveq2 6328	. . . . . . . . . . . . . 14 |- ( m = ( ( |_ ` x ) + 1 ) -> ( x / m ) = ( x / ( ( |_ ` x ) + 1 ) ) )
218	217	fveq2d 5896	. . . . . . . . . . . . 13 |- ( m = ( ( |_ ` x ) + 1 ) -> ( R ` ( x / m ) ) = ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) )
219	218	fveq2d 5896	. . . . . . . . . . . 12 |- ( m = ( ( |_ ` x ) + 1 ) -> ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) )
220		oveq1 6327	. . . . . . . . . . . . . 14 |- ( m = ( ( |_ ` x ) + 1 ) -> ( m - 1 ) = ( ( ( |_ ` x ) + 1 ) - 1 ) )
221	220	fveq2d 5896	. . . . . . . . . . . . 13 |- ( m = ( ( |_ ` x ) + 1 ) -> ( S ` ( m - 1 ) ) = ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) )
222	220	fveq2d 5896	. . . . . . . . . . . . . 14 |- ( m = ( ( |_ ` x ) + 1 ) -> ( T ` ( m - 1 ) ) = ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) )
223	222	oveq2d 6336	. . . . . . . . . . . . 13 |- ( m = ( ( |_ ` x ) + 1 ) -> ( 2 x. ( T ` ( m - 1 ) ) ) = ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) )
224	221, 223	oveq12d 6338	. . . . . . . . . . . 12 |- ( m = ( ( |_ ` x ) + 1 ) -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = ( ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) ) )
225	219, 224	jca 539	. . . . . . . . . . 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 ) ) ) ) ) )
226		nnuz 11228	. . . . . . . . . . . 12 |- NN = ( ZZ>= ` 1 )
227	15, 226	syl6eleq 2550	. . . . . . . . . . 11 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) e. ( ZZ>= ` 1 ) )
228	10	adantr 471	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> x e. RR+ )
229		elfznn 11863	. . . . . . . . . . . . . . . . . 18 |- ( m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) -> m e. NN )
230	229	adantl 472	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> m e. NN )
231	230	nnrpd 11373	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> m e. RR+ )
232	228, 231	rpdivcld 11392	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( x / m ) e. RR+ )
233	69	ffvelrni 6049	. . . . . . . . . . . . . . 15 |- ( ( x / m ) e. RR+ -> ( R ` ( x / m ) ) e. RR )
234	232, 233	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( R ` ( x / m ) ) e. RR )
235	234	recnd 9700	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( R ` ( x / m ) ) e. CC )
236	235	abscld 13553	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( abs ` ( R ` ( x / m ) ) ) e. RR )
237	236	recnd 9700	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( abs ` ( R ` ( x / m ) ) ) e. CC )
238	230	nnred 10657	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> m e. RR )
239		1red 9689	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> 1 e. RR )
240	238, 239	resubcld 10080	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( m - 1 ) e. RR )
241	78	ffvelrni 6049	. . . . . . . . . . . . . 14 |- ( ( m - 1 ) e. RR -> ( S ` ( m - 1 ) ) e. RR )
242	240, 241	syl 17	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( S ` ( m - 1 ) ) e. RR )
243	22	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> 2 e. RR )
244	87	ffvelrni 6049	. . . . . . . . . . . . . . 15 |- ( ( m - 1 ) e. RR -> ( T ` ( m - 1 ) ) e. RR )
245	240, 244	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( T ` ( m - 1 ) ) e. RR )
246	243, 245	remulcld 9702	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( 2 x. ( T ` ( m - 1 ) ) ) e. RR )
247	242, 246	resubcld 10080	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) e. RR )
248	247	recnd 9700	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) e. CC )
249	171, 180, 216, 225, 227, 237, 248	fsumparts 13921	. . . . . . . . . 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 ) ) ) ) ) ) )
250	147	recnd 9700	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` n ) e. CC )
251	87	ffvelrni 6049	. . . . . . . . . . . . . . . . 17 |- ( n e. RR -> ( T ` n ) e. RR )
252	145, 251	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` n ) e. RR )
253	148, 252	remulcld 9702	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( T ` n ) ) e. RR )
254	253	recnd 9700	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( T ` n ) ) e. CC )
255		1red 9689	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
256	145, 255	resubcld 10080	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n - 1 ) e. RR )
257	78	ffvelrni 6049	. . . . . . . . . . . . . . . 16 |- ( ( n - 1 ) e. RR -> ( S ` ( n - 1 ) ) e. RR )
258	256, 257	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` ( n - 1 ) ) e. RR )
259	258	recnd 9700	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` ( n - 1 ) ) e. CC )
260	87	ffvelrni 6049	. . . . . . . . . . . . . . . . 17 |- ( ( n - 1 ) e. RR -> ( T ` ( n - 1 ) ) e. RR )
261	256, 260	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` ( n - 1 ) ) e. RR )
262	148, 261	remulcld 9702	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( T ` ( n - 1 ) ) ) e. RR )
263	262	recnd 9700	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( T ` ( n - 1 ) ) ) e. CC )
264	250, 254, 259, 263	sub4d 10066	. . . . . . . . . . . . 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 ) ) ) ) ) )
265	124	oveq2d 6336	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) = ( 2 x. ( T ` n ) ) )
266	123, 265	oveq12d 6338	. . . . . . . . . . . . . 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 ) ) ) )
267	266	oveq1d 6335	. . . . . . . . . . . . 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 ) ) ) ) ) )
268		2cnd 10715	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 2 e. CC )
269	252	recnd 9700	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` n ) e. CC )
270	261	recnd 9700	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` ( n - 1 ) ) e. CC )
271	268, 269, 270	subdid 10107	. . . . . . . . . . . . . 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 ) ) ) ) )
272	271	oveq2d 6336	. . . . . . . . . . . . 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 ) ) ) ) ) )
273	264, 267, 272	3eqtr4d 2506	. . . . . . . . . . . 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 ) ) ) ) ) )
274	273	oveq2d 6336	. . . . . . . . . . 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 ) ) ) ) ) ) )
275	99, 274	sumeq12rdv 13828	. . . . . . . . . 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 ) ) ) ) ) ) )
276	249, 275	eqtr3d 2498	. . . . . . . . 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 ) ) ) ) ) ) )
277	157, 159	fsumcl 13854	. . . . . . . . . 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 )
278	93, 277	subnegd 10024	. . . . . . . . 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 ) ) ) ) ) ) )
279	162, 276, 278	3eqtr3rd 2505	. . . . . . . 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 ) ) ) ) ) ) )
280	10	relogcld 23628	. . . . . . . . . 10 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR )
281	280	recnd 9700	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
282	66, 281	mulcomd 9695	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) = ( ( log ` x ) x. x ) )
283	279, 282	oveq12d 6338	. . . . . . 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 ) ) )
284	147, 258	resubcld 10080	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` n ) - ( S ` ( n - 1 ) ) ) e. RR )
285	252, 261	resubcld 10080	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) e. RR )
286	148, 285	remulcld 9702	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) e. RR )
287	284, 286	resubcld 10080	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) e. RR )
288	108, 287	remulcld 9702	. . . . . . . . . 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 )
289	157, 288	fsumrecl 13855	. . . . . . . . 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 )
290	289	recnd 9700	. . . . . . . 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 )
291	2, 8	rplogcld 23634	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
292	291	rpne0d 11380	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
293	10	rpne0d 11380	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x =/= 0 )
294	290, 281, 66, 292, 293	divdiv1d 10447	. . . . . . 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 ) ) )
295	283, 294	eqtr4d 2499	. . . . . 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 ) )
296	295	oveq2d 6336	. . . . 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 ) ) )
297	71	recnd 9700	. . . . . . . . . 10 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) e. CC )
298	297	abscld 13553	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` x ) ) e. RR )
299	298, 280	remulcld 9702	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) e. RR )
300	108, 284	remulcld 9702	. . . . . . . . . 10 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) e. RR )
301	157, 300	fsumrecl 13855	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) e. RR )
302	301, 291	rerpdivcld 11403	. . . . . . . 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 )
303	299, 302	resubcld 10080	. . . . . . 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 )
304	303	recnd 9700	. . . . . 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 )
305	290, 281, 292	divcld 10416	. . . . . 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 )
306	304, 305, 66, 293	divdird 10454	. . . . 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 ) ) )
307	299	recnd 9700	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) e. CC )
308	302	recnd 9700	. . . . . . . 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 )
309	307, 308, 305	subsubd 10045	. . . . . . 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 ) ) ) )
310		2cnd 10715	. . . . . . . . . . . 12 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 e. CC )
311	269, 270	subcld 10017	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) e. CC )
312	109, 311	mulcld 9694	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) e. CC )
313	157, 310, 312	fsummulc2 13900	. . . . . . . . . . 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 ) ) ) ) ) )
314	284	recnd 9700	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` n ) - ( S ` ( n - 1 ) ) ) e. CC )
315	268, 311	mulcld 9694	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) e. CC )
316	314, 315	nncand 10022	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) ) = ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) )
317	316	oveq2d 6336	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs