Theorem pntrlog2bndlem4 22804

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

Hypotheses

Ref	Expression
pntsval.1	|- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) )
pntrlog2bnd.r	|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )
pntrlog2bnd.t	|- T = ( a e. RR |-> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) )

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 11322	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( 1 (,) +oo ) -> x e. RR )
2	1	adantl 466	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
3		1rp 10987	. . . . . . . . . . . . . . . . . . . 20 |- 1 e. RR+
4	3	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ )
5		1red 9393	. . . . . . . . . . . . . . . . . . . 20 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR )
6		eliooord 11347	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
7	6	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 < x /\ x < +oo ) )
8	7	simpld 459	. . . . . . . . . . . . . . . . . . . 20 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 < x )
9	5, 2, 8	ltled 9514	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x )
10	2, 4, 9	rpgecld 11054	. . . . . . . . . . . . . . . . . 18 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
11	10	rprege0d 11026	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x e. RR /\ 0 <_ x ) )
12		flge0nn0 11658	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. RR /\ 0 <_ x ) -> ( |_ ` x ) e. NN0 )
13	11, 12	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` x ) e. NN0 )
14		nn0p1nn 10611	. . . . . . . . . . . . . . . . . . . 20 |- ( ( |_ ` x ) e. NN0 -> ( ( |_ ` x ) + 1 ) e. NN )
15	13, 14	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) e. NN )
16	15	nnrpd 11018	. . . . . . . . . . . . . . . . . 18 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) e. RR+ )
17	10, 16	rpdivcld 11036	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) e. RR+ )
18		pntrlog2bnd.r	. . . . . . . . . . . . . . . . . 18 |- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )
19	18	pntrval 22786	. . . . . . . . . . . . . . . . 17 |- ( ( x / ( ( |_ ` x ) + 1 ) ) e. RR+ -> ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) = ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) - ( x / ( ( |_ ` x ) + 1 ) ) ) )
20	17, 19	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) = ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) - ( x / ( ( |_ ` x ) + 1 ) ) ) )
21	2, 15	nndivred 10362	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) e. RR )
22		2re 10383	. . . . . . . . . . . . . . . . . . . 20 |- 2 e. RR
23	22	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 e. RR )
24		flltp1 11642	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. RR -> x < ( ( |_ ` x ) + 1 ) )
25	2, 24	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x < ( ( |_ ` x ) + 1 ) )
26	15	nncnd 10330	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) e. CC )
27	26	mulid1d 9395	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( |_ ` x ) + 1 ) x. 1 ) = ( ( |_ ` x ) + 1 ) )
28	25, 27	breqtrrd 4313	. . . . . . . . . . . . . . . . . . . 20 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x < ( ( ( |_ ` x ) + 1 ) x. 1 ) )
29	2, 5, 16	ltdivmuld 11066	. . . . . . . . . . . . . . . . . . . 20 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( x / ( ( |_ ` x ) + 1 ) ) < 1 <-> x < ( ( ( |_ ` x ) + 1 ) x. 1 ) ) )
30	28, 29	mpbird 232	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) < 1 )
31		1lt2 10480	. . . . . . . . . . . . . . . . . . . 20 |- 1 < 2
32	31	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 < 2 )
33	21, 5, 23, 30, 32	lttrd 9524	. . . . . . . . . . . . . . . . . 18 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) < 2 )
34		chpeq0 22522	. . . . . . . . . . . . . . . . . . 19 |- ( ( x / ( ( |_ ` x ) + 1 ) ) e. RR -> ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) = 0 <-> ( x / ( ( |_ ` x ) + 1 ) ) < 2 ) )
35	21, 34	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) = 0 <-> ( x / ( ( |_ ` x ) + 1 ) ) < 2 ) )
36	33, 35	mpbird 232	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) = 0 )
37	36	oveq1d 6101	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) - ( x / ( ( |_ ` x ) + 1 ) ) ) = ( 0 - ( x / ( ( |_ ` x ) + 1 ) ) ) )
38	20, 37	eqtrd 2470	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) = ( 0 - ( x / ( ( |_ ` x ) + 1 ) ) ) )
39	38	fveq2d 5690	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) = ( abs ` ( 0 - ( x / ( ( |_ ` x ) + 1 ) ) ) ) )
40		0red 9379	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 0 e. RR )
41	17	rpge0d 11023	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( x / ( ( |_ ` x ) + 1 ) ) )
42	40, 21, 41	abssuble0d 12911	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( 0 - ( x / ( ( |_ ` x ) + 1 ) ) ) ) = ( ( x / ( ( |_ ` x ) + 1 ) ) - 0 ) )
43	21	recnd 9404	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) e. CC )
44	43	subid1d 9700	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( x / ( ( |_ ` x ) + 1 ) ) - 0 ) = ( x / ( ( |_ ` x ) + 1 ) ) )
45	39, 42, 44	3eqtrd 2474	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) = ( x / ( ( |_ ` x ) + 1 ) ) )
46	13	nn0red 10629	. . . . . . . . . . . . . . . 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 22800	. . . . . . . . . . . . . . . 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 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 ) ) ) ) )
50	13	nn0cnd 10630	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` x ) e. CC )
51		1cnd 9394	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. CC )
52	50, 51	pncand 9712	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( |_ ` x ) + 1 ) - 1 ) = ( |_ ` x ) )
53	52	fveq2d 5690	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) = ( S ` ( |_ ` x ) ) )
54	47	pntsval2 22800	. . . . . . . . . . . . . . . . 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 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 ) ) ) ) )
56		flidm 11650	. . . . . . . . . . . . . . . . . . 19 |- ( x e. RR -> ( |_ ` ( |_ ` x ) ) = ( |_ ` x ) )
57	2, 56	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` ( |_ ` x ) ) = ( |_ ` x ) )
58	57	oveq2d 6102	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` ( |_ ` x ) ) ) = ( 1 ... ( |_ ` x ) ) )
59	58	sumeq1d 13170	. . . . . . . . . . . . . . . 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 2473	. . . . . . . . . . . . . . 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 2480	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) = ( S ` x ) )
62	52	fveq2d 5690	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) = ( T ` ( |_ ` x ) ) )
63	62	oveq2d 6102	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) = ( 2 x. ( T ` ( |_ ` x ) ) ) )
64	61, 63	oveq12d 6104	. . . . . . . . . . . . 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 6104	. . . . . . . . . . . 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 9404	. . . . . . . . . . . . . . . . . . 19 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. CC )
67	66	div1d 10091	. . . . . . . . . . . . . . . . . 18 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x / 1 ) = x )
68	67	fveq2d 5690	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` ( x / 1 ) ) = ( R ` x ) )
69	18	pntrf 22787	. . . . . . . . . . . . . . . . . . 19 |- R : RR+ --> RR
70	69	ffvelrni 5837	. . . . . . . . . . . . . . . . . 18 |- ( x e. RR+ -> ( R ` x ) e. RR )
71	10, 70	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) e. RR )
72	68, 71	eqeltrd 2512	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` ( x / 1 ) ) e. RR )
73	72	recnd 9404	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` ( x / 1 ) ) e. CC )
74	73	abscld 12914	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` ( x / 1 ) ) ) e. RR )
75	74	recnd 9404	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` ( x / 1 ) ) ) e. CC )
76	75	mul01d 9560	. . . . . . . . . . . 12 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` ( x / 1 ) ) ) x. 0 ) = 0 )
77	65, 76	oveq12d 6104	. . . . . . . . . . 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 22797	. . . . . . . . . . . . . . . . 17 |- S : RR --> RR
79	78	ffvelrni 5837	. . . . . . . . . . . . . . . 16 |- ( x e. RR -> ( S ` x ) e. RR )
80	2, 79	syl 16	. . . . . . . . . . . . . . 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 22002	. . . . . . . . . . . . . . . . . . . . 21 |- ( a e. RR+ -> ( log ` a ) e. RR )
83		remulcl 9359	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( a e. RR /\ ( log ` a ) e. RR ) -> ( a x. ( log ` a ) ) e. RR )
84	82, 83	sylan2 474	. . . . . . . . . . . . . . . . . . . 20 |- ( ( a e. RR /\ a e. RR+ ) -> ( a x. ( log ` a ) ) e. RR )
85		0red 9379	. . . . . . . . . . . . . . . . . . . 20 |- ( ( a e. RR /\ -. a e. RR+ ) -> 0 e. RR )
86	84, 85	ifclda 3816	. . . . . . . . . . . . . . . . . . 19 |- ( a e. RR -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) e. RR )
87	81, 86	fmpti 5861	. . . . . . . . . . . . . . . . . 18 |- T : RR --> RR
88	87	ffvelrni 5837	. . . . . . . . . . . . . . . . 17 |- ( ( |_ ` x ) e. RR -> ( T ` ( |_ ` x ) ) e. RR )
89	46, 88	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( T ` ( |_ ` x ) ) e. RR )
90	23, 89	remulcld 9406	. . . . . . . . . . . . . . 15 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( T ` ( |_ ` x ) ) ) e. RR )
91	80, 90	resubcld 9768	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) e. RR )
92	21, 91	remulcld 9406	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) e. RR )
93	92	recnd 9404	. . . . . . . . . . . 12 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( x / ( ( |_ ` x ) + 1 ) ) x. ( ( S ` x ) - ( 2 x. ( T ` ( |_ ` x ) ) ) ) ) e. CC )
94	93	subid1d 9700	. . . . . . . . . . 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 2470	. . . . . . . . . 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 11640	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` x ) e. ZZ )
97		fzval3 11597	. . . . . . . . . . . . . 14 |- ( ( |_ ` x ) e. ZZ -> ( 1 ... ( |_ ` x ) ) = ( 1..^ ( ( |_ ` x ) + 1 ) ) )
98	96, 97	syl 16	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) = ( 1..^ ( ( |_ ` x ) + 1 ) ) )
99	98	eqcomd 2443	. . . . . . . . . . . 12 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1..^ ( ( |_ ` x ) + 1 ) ) = ( 1 ... ( |_ ` x ) ) )
100	10	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ )
101		elfznn 11470	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
102	101	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
103	102	nnrpd 11018	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
104	100, 103	rpdivcld 11036	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
105	69	ffvelrni 5837	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x / n ) e. RR+ -> ( R ` ( x / n ) ) e. RR )
106	104, 105	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. RR )
107	106	recnd 9404	. . . . . . . . . . . . . . . . . 18 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. CC )
108	107	abscld 12914	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / n ) ) ) e. RR )
109	108	recnd 9404	. . . . . . . . . . . . . . . 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 11034	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n + 1 ) e. RR+ )
112	100, 111	rpdivcld 11036	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / ( n + 1 ) ) e. RR+ )
113	69	ffvelrni 5837	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x / ( n + 1 ) ) e. RR+ -> ( R ` ( x / ( n + 1 ) ) ) e. RR )
114	112, 113	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / ( n + 1 ) ) ) e. RR )
115	114	recnd 9404	. . . . . . . . . . . . . . . . . 18 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / ( n + 1 ) ) ) e. CC )
116	115	abscld 12914	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) e. RR )
117	116	recnd 9404	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) e. CC )
118	109, 117	negsubdi2d 9727	. . . . . . . . . . . . . . 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 2443	. . . . . . . . . . . . . 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 10330	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
121		1cnd 9394	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. CC )
122	120, 121	pncand 9712	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n + 1 ) - 1 ) = n )
123	122	fveq2d 5690	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` ( ( n + 1 ) - 1 ) ) = ( S ` n ) )
124	122	fveq2d 5690	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` ( ( n + 1 ) - 1 ) ) = ( T ` n ) )
125		rpre 10989	. . . . . . . . . . . . . . . . . . . 20 |- ( n e. RR+ -> n e. RR )
126		eleq1 2498	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = n -> ( a e. RR+ <-> n e. RR+ ) )
127		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a = n -> a = n )
128		fveq2 5686	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( a = n -> ( log ` a ) = ( log ` n ) )
129	127, 128	oveq12d 6104	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = n -> ( a x. ( log ` a ) ) = ( n x. ( log ` n ) ) )
130	126, 129	ifbieq1d 3807	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = n -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) )
131		ovex 6111	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n x. ( log ` n ) ) e. _V
132		c0ex 9372	. . . . . . . . . . . . . . . . . . . . . 22 |- 0 e. _V
133	131, 132	ifex 3853	. . . . . . . . . . . . . . . . . . . . 21 |- if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) e. _V
134	130, 81, 133	fvmpt 5769	. . . . . . . . . . . . . . . . . . . 20 |- ( n e. RR -> ( T ` n ) = if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) )
135	125, 134	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( n e. RR+ -> ( T ` n ) = if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) )
136		iftrue 3792	. . . . . . . . . . . . . . . . . . 19 |- ( n e. RR+ -> if ( n e. RR+ , ( n x. ( log ` n ) ) , 0 ) = ( n x. ( log ` n ) ) )
137	135, 136	eqtrd 2470	. . . . . . . . . . . . . . . . . 18 |- ( n e. RR+ -> ( T ` n ) = ( n x. ( log ` n ) ) )
138	103, 137	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` n ) = ( n x. ( log ` n ) ) )
139	124, 138	eqtrd 2470	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` ( ( n + 1 ) - 1 ) ) = ( n x. ( log ` n ) ) )
140	139	oveq2d 6102	. . . . . . . . . . . . . . 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 6104	. . . . . . . . . . . . . 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 6104	. . . . . . . . . . . . 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 9768	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) e. RR )
144	143	recnd 9404	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) - ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) ) e. CC )
145	102	nnred 10329	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR )
146	78	ffvelrni 5837	. . . . . . . . . . . . . . . . 17 |- ( n e. RR -> ( S ` n ) e. RR )
147	145, 146	syl 16	. . . . . . . . . . . . . . . 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 22047	. . . . . . . . . . . . . . . . . 18 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. RR )
150	145, 149	remulcld 9406	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. ( log ` n ) ) e. RR )
151	148, 150	remulcld 9406	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( n x. ( log ` n ) ) ) e. RR )
152	147, 151	resubcld 9768	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) e. RR )
153	152	recnd 9404	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` n ) - ( 2 x. ( n x. ( log ` n ) ) ) ) e. CC )
154	144, 153	mulneg1d 9789	. . . . . . . . . . . . 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 2470	. . . . . . . . . . . 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 13176	. . . . . . . . . . 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 11787	. . . . . . . . . . . 12 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
158	143, 152	remulcld 9406	. . . . . . . . . . . . 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 9404	. . . . . . . . . . . 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 13246	. . . . . . . . . . 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 2470	. . . . . . . . . 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 6104	. . . . . . . . 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 6094	. . . . . . . . . . . . . 14 |- ( m = n -> ( x / m ) = ( x / n ) )
164	163	fveq2d 5690	. . . . . . . . . . . . 13 |- ( m = n -> ( R ` ( x / m ) ) = ( R ` ( x / n ) ) )
165	164	fveq2d 5690	. . . . . . . . . . . 12 |- ( m = n -> ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / n ) ) ) )
166		oveq1 6093	. . . . . . . . . . . . . 14 |- ( m = n -> ( m - 1 ) = ( n - 1 ) )
167	166	fveq2d 5690	. . . . . . . . . . . . 13 |- ( m = n -> ( S ` ( m - 1 ) ) = ( S ` ( n - 1 ) ) )
168	166	fveq2d 5690	. . . . . . . . . . . . . 14 |- ( m = n -> ( T ` ( m - 1 ) ) = ( T ` ( n - 1 ) ) )
169	168	oveq2d 6102	. . . . . . . . . . . . 13 |- ( m = n -> ( 2 x. ( T ` ( m - 1 ) ) ) = ( 2 x. ( T ` ( n - 1 ) ) ) )
170	167, 169	oveq12d 6104	. . . . . . . . . . . 12 |- ( m = n -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = ( ( S ` ( n - 1 ) ) - ( 2 x. ( T ` ( n - 1 ) ) ) ) )
171	165, 170	jca 532	. . . . . . . . . . 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 6094	. . . . . . . . . . . . . 14 |- ( m = ( n + 1 ) -> ( x / m ) = ( x / ( n + 1 ) ) )
173	172	fveq2d 5690	. . . . . . . . . . . . 13 |- ( m = ( n + 1 ) -> ( R ` ( x / m ) ) = ( R ` ( x / ( n + 1 ) ) ) )
174	173	fveq2d 5690	. . . . . . . . . . . 12 |- ( m = ( n + 1 ) -> ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / ( n + 1 ) ) ) ) )
175		oveq1 6093	. . . . . . . . . . . . . 14 |- ( m = ( n + 1 ) -> ( m - 1 ) = ( ( n + 1 ) - 1 ) )
176	175	fveq2d 5690	. . . . . . . . . . . . 13 |- ( m = ( n + 1 ) -> ( S ` ( m - 1 ) ) = ( S ` ( ( n + 1 ) - 1 ) ) )
177	175	fveq2d 5690	. . . . . . . . . . . . . 14 |- ( m = ( n + 1 ) -> ( T ` ( m - 1 ) ) = ( T ` ( ( n + 1 ) - 1 ) ) )
178	177	oveq2d 6102	. . . . . . . . . . . . 13 |- ( m = ( n + 1 ) -> ( 2 x. ( T ` ( m - 1 ) ) ) = ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) )
179	176, 178	oveq12d 6104	. . . . . . . . . . . 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 532	. . . . . . . . . . 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 6094	. . . . . . . . . . . . . 14 |- ( m = 1 -> ( x / m ) = ( x / 1 ) )
182	181	fveq2d 5690	. . . . . . . . . . . . 13 |- ( m = 1 -> ( R ` ( x / m ) ) = ( R ` ( x / 1 ) ) )
183	182	fveq2d 5690	. . . . . . . . . . . 12 |- ( m = 1 -> ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / 1 ) ) ) )
184		oveq1 6093	. . . . . . . . . . . . . . . . 17 |- ( m = 1 -> ( m - 1 ) = ( 1 - 1 ) )
185		1m1e0 10382	. . . . . . . . . . . . . . . . 17 |- ( 1 - 1 ) = 0
186	184, 185	syl6eq 2486	. . . . . . . . . . . . . . . 16 |- ( m = 1 -> ( m - 1 ) = 0 )
187	186	fveq2d 5690	. . . . . . . . . . . . . . 15 |- ( m = 1 -> ( S ` ( m - 1 ) ) = ( S ` 0 ) )
188		0re 9378	. . . . . . . . . . . . . . . 16 |- 0 e. RR
189		fveq2 5686	. . . . . . . . . . . . . . . . . . . . . 22 |- ( a = 0 -> ( |_ ` a ) = ( |_ ` 0 ) )
190		0z 10649	. . . . . . . . . . . . . . . . . . . . . . 23 |- 0 e. ZZ
191		flid 11649	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 0 e. ZZ -> ( |_ ` 0 ) = 0 )
192	190, 191	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 |- ( |_ ` 0 ) = 0
193	189, 192	syl6eq 2486	. . . . . . . . . . . . . . . . . . . . 21 |- ( a = 0 -> ( |_ ` a ) = 0 )
194	193	oveq2d 6102	. . . . . . . . . . . . . . . . . . . 20 |- ( a = 0 -> ( 1 ... ( |_ ` a ) ) = ( 1 ... 0 ) )
195		fz10 11462	. . . . . . . . . . . . . . . . . . . 20 |- ( 1 ... 0 ) = (/)
196	194, 195	syl6eq 2486	. . . . . . . . . . . . . . . . . . 19 |- ( a = 0 -> ( 1 ... ( |_ ` a ) ) = (/) )
197	196	sumeq1d 13170	. . . . . . . . . . . . . . . . . 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 13190	. . . . . . . . . . . . . . . . . 18 |- sum_ i e. (/) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) = 0
199	197, 198	syl6eq 2486	. . . . . . . . . . . . . . . . 17 |- ( a = 0 -> sum_ i e. ( 1 ... ( |_ ` a ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) = 0 )
200	199, 47, 132	fvmpt 5769	. . . . . . . . . . . . . . . 16 |- ( 0 e. RR -> ( S ` 0 ) = 0 )
201	188, 200	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( S ` 0 ) = 0
202	187, 201	syl6eq 2486	. . . . . . . . . . . . . 14 |- ( m = 1 -> ( S ` ( m - 1 ) ) = 0 )
203	186	fveq2d 5690	. . . . . . . . . . . . . . . . 17 |- ( m = 1 -> ( T ` ( m - 1 ) ) = ( T ` 0 ) )
204		rpne0 10998	. . . . . . . . . . . . . . . . . . . . 21 |- ( a e. RR+ -> a =/= 0 )
205	204	necon2bi 2652	. . . . . . . . . . . . . . . . . . . 20 |- ( a = 0 -> -. a e. RR+ )
206		iffalse 3794	. . . . . . . . . . . . . . . . . . . 20 |- ( -. a e. RR+ -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = 0 )
207	205, 206	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( a = 0 -> if ( a e. RR+ , ( a x. ( log ` a ) ) , 0 ) = 0 )
208	207, 81, 132	fvmpt 5769	. . . . . . . . . . . . . . . . . 18 |- ( 0 e. RR -> ( T ` 0 ) = 0 )
209	188, 208	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( T ` 0 ) = 0
210	203, 209	syl6eq 2486	. . . . . . . . . . . . . . . 16 |- ( m = 1 -> ( T ` ( m - 1 ) ) = 0 )
211	210	oveq2d 6102	. . . . . . . . . . . . . . 15 |- ( m = 1 -> ( 2 x. ( T ` ( m - 1 ) ) ) = ( 2 x. 0 ) )
212		2t0e0 10469	. . . . . . . . . . . . . . 15 |- ( 2 x. 0 ) = 0
213	211, 212	syl6eq 2486	. . . . . . . . . . . . . 14 |- ( m = 1 -> ( 2 x. ( T ` ( m - 1 ) ) ) = 0 )
214	202, 213	oveq12d 6104	. . . . . . . . . . . . 13 |- ( m = 1 -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = ( 0 - 0 ) )
215		0m0e0 10423	. . . . . . . . . . . . 13 |- ( 0 - 0 ) = 0
216	214, 215	syl6eq 2486	. . . . . . . . . . . 12 |- ( m = 1 -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = 0 )
217	183, 216	jca 532	. . . . . . . . . . 11 |- ( m = 1 -> ( ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / 1 ) ) ) /\ ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = 0 ) )
218		oveq2 6094	. . . . . . . . . . . . . 14 |- ( m = ( ( |_ ` x ) + 1 ) -> ( x / m ) = ( x / ( ( |_ ` x ) + 1 ) ) )
219	218	fveq2d 5690	. . . . . . . . . . . . 13 |- ( m = ( ( |_ ` x ) + 1 ) -> ( R ` ( x / m ) ) = ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) )
220	219	fveq2d 5690	. . . . . . . . . . . 12 |- ( m = ( ( |_ ` x ) + 1 ) -> ( abs ` ( R ` ( x / m ) ) ) = ( abs ` ( R ` ( x / ( ( |_ ` x ) + 1 ) ) ) ) )
221		oveq1 6093	. . . . . . . . . . . . . 14 |- ( m = ( ( |_ ` x ) + 1 ) -> ( m - 1 ) = ( ( ( |_ ` x ) + 1 ) - 1 ) )
222	221	fveq2d 5690	. . . . . . . . . . . . 13 |- ( m = ( ( |_ ` x ) + 1 ) -> ( S ` ( m - 1 ) ) = ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) )
223	221	fveq2d 5690	. . . . . . . . . . . . . 14 |- ( m = ( ( |_ ` x ) + 1 ) -> ( T ` ( m - 1 ) ) = ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) )
224	223	oveq2d 6102	. . . . . . . . . . . . 13 |- ( m = ( ( |_ ` x ) + 1 ) -> ( 2 x. ( T ` ( m - 1 ) ) ) = ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) )
225	222, 224	oveq12d 6104	. . . . . . . . . . . 12 |- ( m = ( ( |_ ` x ) + 1 ) -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) = ( ( S ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( 2 x. ( T ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) ) )
226	220, 225	jca 532	. . . . . . . . . . 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 ) ) ) ) ) )
227		nnuz 10888	. . . . . . . . . . . 12 |- NN = ( ZZ>= ` 1 )
228	15, 227	syl6eleq 2528	. . . . . . . . . . 11 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) e. ( ZZ>= ` 1 ) )
229	10	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> x e. RR+ )
230		elfznn 11470	. . . . . . . . . . . . . . . . . 18 |- ( m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) -> m e. NN )
231	230	adantl 466	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> m e. NN )
232	231	nnrpd 11018	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> m e. RR+ )
233	229, 232	rpdivcld 11036	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( x / m ) e. RR+ )
234	69	ffvelrni 5837	. . . . . . . . . . . . . . 15 |- ( ( x / m ) e. RR+ -> ( R ` ( x / m ) ) e. RR )
235	233, 234	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( R ` ( x / m ) ) e. RR )
236	235	recnd 9404	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( R ` ( x / m ) ) e. CC )
237	236	abscld 12914	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( abs ` ( R ` ( x / m ) ) ) e. RR )
238	237	recnd 9404	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( abs ` ( R ` ( x / m ) ) ) e. CC )
239	231	nnred 10329	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> m e. RR )
240		1red 9393	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> 1 e. RR )
241	239, 240	resubcld 9768	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( m - 1 ) e. RR )
242	78	ffvelrni 5837	. . . . . . . . . . . . . 14 |- ( ( m - 1 ) e. RR -> ( S ` ( m - 1 ) ) e. RR )
243	241, 242	syl 16	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( S ` ( m - 1 ) ) e. RR )
244	22	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> 2 e. RR )
245	87	ffvelrni 5837	. . . . . . . . . . . . . . 15 |- ( ( m - 1 ) e. RR -> ( T ` ( m - 1 ) ) e. RR )
246	241, 245	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( T ` ( m - 1 ) ) e. RR )
247	244, 246	remulcld 9406	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( 2 x. ( T ` ( m - 1 ) ) ) e. RR )
248	243, 247	resubcld 9768	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) e. RR )
249	248	recnd 9404	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( ( S ` ( m - 1 ) ) - ( 2 x. ( T ` ( m - 1 ) ) ) ) e. CC )
250	171, 180, 217, 226, 228, 238, 249	fsumparts 13261	. . . . . . . . . 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 ) ) ) ) ) ) )
251	147	recnd 9404	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` n ) e. CC )
252	87	ffvelrni 5837	. . . . . . . . . . . . . . . . 17 |- ( n e. RR -> ( T ` n ) e. RR )
253	145, 252	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` n ) e. RR )
254	148, 253	remulcld 9406	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( T ` n ) ) e. RR )
255	254	recnd 9404	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( T ` n ) ) e. CC )
256		1red 9393	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
257	145, 256	resubcld 9768	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n - 1 ) e. RR )
258	78	ffvelrni 5837	. . . . . . . . . . . . . . . 16 |- ( ( n - 1 ) e. RR -> ( S ` ( n - 1 ) ) e. RR )
259	257, 258	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` ( n - 1 ) ) e. RR )
260	259	recnd 9404	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` ( n - 1 ) ) e. CC )
261	87	ffvelrni 5837	. . . . . . . . . . . . . . . . 17 |- ( ( n - 1 ) e. RR -> ( T ` ( n - 1 ) ) e. RR )
262	257, 261	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` ( n - 1 ) ) e. RR )
263	148, 262	remulcld 9406	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( T ` ( n - 1 ) ) ) e. RR )
264	263	recnd 9404	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( T ` ( n - 1 ) ) ) e. CC )
265	251, 255, 260, 264	sub4d 9760	. . . . . . . . . . . . 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 ) ) ) ) ) )
266	124	oveq2d 6102	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( T ` ( ( n + 1 ) - 1 ) ) ) = ( 2 x. ( T ` n ) ) )
267	123, 266	oveq12d 6104	. . . . . . . . . . . . . 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 ) ) ) )
268	267	oveq1d 6101	. . . . . . . . . . . . 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 ) ) ) ) ) )
269		2cnd 10386	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 2 e. CC )
270	253	recnd 9404	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` n ) e. CC )
271	262	recnd 9404	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T ` ( n - 1 ) ) e. CC )
272	269, 270, 271	subdid 9792	. . . . . . . . . . . . . 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 ) ) ) ) )
273	272	oveq2d 6102	. . . . . . . . . . . . 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 ) ) ) ) ) )
274	265, 268, 273	3eqtr4d 2480	. . . . . . . . . . . 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 ) ) ) ) ) )
275	274	oveq2d 6102	. . . . . . . . . . 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 ) ) ) ) ) ) )
276	99, 275	sumeq12rdv 13176	. . . . . . . . . 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 ) ) ) ) ) ) )
277	250, 276	eqtr3d 2472	. . . . . . . . 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 ) ) ) ) ) ) )
278	157, 159	fsumcl 13202	. . . . . . . . . 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 )
279	93, 278	subnegd 9718	. . . . . . . . 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 ) ) ) ) ) ) )
280	162, 277, 279	3eqtr3rd 2479	. . . . . . . 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 ) ) ) ) ) ) )
281	10	relogcld 22047	. . . . . . . . . 10 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR )
282	281	recnd 9404	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
283	66, 282	mulcomd 9399	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) = ( ( log ` x ) x. x ) )
284	280, 283	oveq12d 6104	. . . . . . 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 ) ) )
285	147, 259	resubcld 9768	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` n ) - ( S ` ( n - 1 ) ) ) e. RR )
286	253, 262	resubcld 9768	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) e. RR )
287	148, 286	remulcld 9406	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) e. RR )
288	285, 287	resubcld 9768	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( S ` n ) - ( S ` ( n - 1 ) ) ) - ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) ) e. RR )
289	108, 288	remulcld 9406	. . . . . . . . . 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 )
290	157, 289	fsumrecl 13203	. . . . . . . . 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 )
291	290	recnd 9404	. . . . . . . 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 )
292	2, 8	rplogcld 22053	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
293	292	rpne0d 11024	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
294	10	rpne0d 11024	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x =/= 0 )
295	291, 282, 66, 293, 294	divdiv1d 10130	. . . . . . 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 ) ) )
296	284, 295	eqtr4d 2473	. . . . . 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 ) )
297	296	oveq2d 6102	. . . . 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 ) ) )
298	71	recnd 9404	. . . . . . . . . 10 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) e. CC )
299	298	abscld 12914	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` x ) ) e. RR )
300	299, 281	remulcld 9406	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) e. RR )
301	108, 285	remulcld 9406	. . . . . . . . . 10 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) e. RR )
302	157, 301	fsumrecl 13203	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) e. RR )
303	302, 292	rerpdivcld 11046	. . . . . . . 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 )
304	300, 303	resubcld 9768	. . . . . . 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 )
305	304	recnd 9404	. . . . . 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 )
306	291, 282, 293	divcld 10099	. . . . . 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 )
307	305, 306, 66, 294	divdird 10137	. . . . 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 ) ) )
308	300	recnd 9404	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) e. CC )
309	303	recnd 9404	. . . . . . . 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 )
310	308, 309, 306	subsubd 9739	. . . . . . 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 ) ) ) )
311		2cnd 10386	. . . . . . . . . . . 12 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 e. CC )
312	270, 271	subcld 9711	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( T ` n ) - ( T ` ( n - 1 ) ) ) e. CC )
313	109, 312	mulcld 9398	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) e. CC )
314	157, 311, 313	fsummulc2 13243	. . . . . . . . . . 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 ) ) ) ) ) )
315	285	recnd 9404	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` n ) - ( S ` ( n - 1 ) ) ) e. CC )
316	269, 312	mulcld 9398	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( T ` n ) - ( T ` ( n - 1 ) ) ) ) e. CC )
317	315, 316	nncand 9716	. . . . . . . . . . . . . 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 ) ) ) ) )
318	317	oveq2d 6102	. . . . . . . . . . . . 13