Theorem selberg34r

Description: The sum of selberg3r and selberg4r . (Contributed by Mario Carneiro, 31-May-2016)

	Ref	Expression
Hypothesis	pntrval.r	|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
Assertion	selberg34r	|- ( x e. ( 1 (,) +oo ) |-> ( ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) / x ) ) e. O(1)

Proof

Step	Hyp	Ref	Expression
1		pntrval.r	|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2		2re	|- 2 e. RR
3	2	a1i	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 e. RR )
4		elioore	|- ( x e. ( 1 (,) +oo ) -> x e. RR )
5	4	adantl	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
6		1rp	|- 1 e. RR+
7	6	a1i	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ )
8		1red	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR )
9		eliooord	|- ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
10	9	adantl	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 < x /\ x < +oo ) )
11	10	simpld	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 < x )
12	8 5 11	ltled	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x )
13	5 7 12	rpgecld	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
14	1	pntrf	|- R : RR+ --> RR
15	14	ffvelcdmi	|- ( x e. RR+ -> ( R ` x ) e. RR )
16	13 15	syl	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) e. RR )
17	13	relogcld	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR )
18	16 17	remulcld	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( R ` x ) x. ( log ` x ) ) e. RR )
19	3 18	remulcld	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) e. RR )
20	19	recnd	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) e. CC )
21	5 11	rplogcld	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
22	3 21	rerpdivcld	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 / ( log ` x ) ) e. RR )
23	22	recnd	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 / ( log ` x ) ) e. CC )
24		fzfid	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
25	13	adantr	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ )
26		elfznn	|- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
27	26	adantl	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
28	27	nnrpd	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
29	25 28	rpdivcld	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
30	14	ffvelcdmi	|- ( ( x / n ) e. RR+ -> ( R ` ( x / n ) ) e. RR )
31	29 30	syl	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. RR )
32		fzfid	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... n ) e. Fin )
33		dvdsssfz1	|- ( n e. NN -> { y e. NN | y || n } C_ ( 1 ... n ) )
34	27 33	syl	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> { y e. NN | y || n } C_ ( 1 ... n ) )
35	32 34	ssfid	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> { y e. NN | y || n } e. Fin )
36		ssrab2	|- { y e. NN | y || n } C_ NN
37		simpr	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. { y e. NN | y || n } ) -> m e. { y e. NN | y || n } )
38	36 37	sselid	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. { y e. NN | y || n } ) -> m e. NN )
39		vmacl	|- ( m e. NN -> ( Lam ` m ) e. RR )
40	38 39	syl	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. { y e. NN | y || n } ) -> ( Lam ` m ) e. RR )
41		dvdsdivcl	|- ( ( n e. NN /\ m e. { y e. NN | y || n } ) -> ( n / m ) e. { y e. NN | y || n } )
42	27 41	sylan	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. { y e. NN | y || n } ) -> ( n / m ) e. { y e. NN | y || n } )
43	36 42	sselid	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. { y e. NN | y || n } ) -> ( n / m ) e. NN )
44		vmacl	|- ( ( n / m ) e. NN -> ( Lam ` ( n / m ) ) e. RR )
45	43 44	syl	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. { y e. NN | y || n } ) -> ( Lam ` ( n / m ) ) e. RR )
46	40 45	remulcld	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. { y e. NN | y || n } ) -> ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) e. RR )
47	35 46	fsumrecl	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) e. RR )
48		vmacl	|- ( n e. NN -> ( Lam ` n ) e. RR )
49	27 48	syl	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR )
50	28	relogcld	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. RR )
51	49 50	remulcld	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( log ` n ) ) e. RR )
52	47 51	resubcld	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) e. RR )
53	31 52	remulcld	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) e. RR )
54	24 53	fsumrecl	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) e. RR )
55	54	recnd	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) e. CC )
56	23 55	mulcld	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) e. CC )
57	20 56	subcld	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) ) e. CC )
58	5	recnd	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. CC )
59		2cnd	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 e. CC )
60	13	rpne0d	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x =/= 0 )
61		2ne0	|- 2 =/= 0
62	61	a1i	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 =/= 0 )
63	57 58 59 60 62	divdiv32d	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) ) / x ) / 2 ) = ( ( ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) ) / 2 ) / x ) )
64	57 58 60	divcld	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) ) / x ) e. CC )
65	64 59 62	divrecd	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) ) / x ) / 2 ) = ( ( ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) ) / x ) x. ( 1 / 2 ) ) )
66	20 56 59 62	divsubdird	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) ) / 2 ) = ( ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) / 2 ) - ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) / 2 ) ) )
67	18	recnd	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( R ` x ) x. ( log ` x ) ) e. CC )
68	67 59 62	divcan3d	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) / 2 ) = ( ( R ` x ) x. ( log ` x ) ) )
69	21	rpcnd	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
70	21	rpne0d	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
71	59 69 55 70	div32d	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) = ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) )
72	71	oveq1d	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) / 2 ) = ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) / 2 ) )
73	54 21	rerpdivcld	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) e. RR )
74	73	recnd	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) e. CC )
75	74 59 62	divcan3d	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) / 2 ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) )
76	72 75	eqtrd	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) / 2 ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) )
77	68 76	oveq12d	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) / 2 ) - ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) / 2 ) ) = ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) )
78	66 77	eqtrd	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) ) / 2 ) = ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) )
79	78	oveq1d	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) ) / 2 ) / x ) = ( ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) / x ) )
80	63 65 79	3eqtr3d	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) ) / x ) x. ( 1 / 2 ) ) = ( ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) / x ) )
81	80	mpteq2dva	|- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) ) / x ) x. ( 1 / 2 ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) / x ) ) )
82	22 54	remulcld	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) e. RR )
83	19 82	resubcld	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) ) e. RR )
84	83 13	rerpdivcld	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) ) / x ) e. RR )
85	8	rehalfcld	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 / 2 ) e. RR )
86	31	recnd	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. CC )
87	47	recnd	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) e. CC )
88	49	recnd	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. CC )
89	50	recnd	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. CC )
90	88 89	mulcld	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( log ` n ) ) e. CC )
91	86 87 90	subdid	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) = ( ( ( R ` ( x / n ) ) x. sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) - ( ( R ` ( x / n ) ) x. ( ( Lam ` n ) x. ( log ` n ) ) ) ) )
92	86 88 89	mul12d	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( R ` ( x / n ) ) x. ( ( Lam ` n ) x. ( log ` n ) ) ) = ( ( Lam ` n ) x. ( ( R ` ( x / n ) ) x. ( log ` n ) ) ) )
93	88 86 89	mulassd	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) = ( ( Lam ` n ) x. ( ( R ` ( x / n ) ) x. ( log ` n ) ) ) )
94	92 93	eqtr4d	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( R ` ( x / n ) ) x. ( ( Lam ` n ) x. ( log ` n ) ) ) = ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) )
95	94	oveq2d	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( R ` ( x / n ) ) x. sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) - ( ( R ` ( x / n ) ) x. ( ( Lam ` n ) x. ( log ` n ) ) ) ) = ( ( ( R ` ( x / n ) ) x. sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) - ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) )
96	91 95	eqtrd	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) = ( ( ( R ` ( x / n ) ) x. sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) - ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) )
97	96	sumeq2dv	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( R ` ( x / n ) ) x. sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) - ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) )
98	86 87	mulcld	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( R ` ( x / n ) ) x. sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) e. CC )
99	88 86	mulcld	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) e. CC )
100	99 89	mulcld	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) e. CC )
101	24 98 100	fsumsub	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( R ` ( x / n ) ) x. sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) - ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) )
102	46	recnd	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. { y e. NN | y || n } ) -> ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) e. CC )
103	35 86 102	fsummulc2	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( R ` ( x / n ) ) x. sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) = sum_ m e. { y e. NN | y || n } ( ( R ` ( x / n ) ) x. ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) )
104	103	sumeq2dv	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. { y e. NN | y || n } ( ( R ` ( x / n ) ) x. ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) )
105		oveq2	|- ( n = ( m x. k ) -> ( x / n ) = ( x / ( m x. k ) ) )
106	105	fveq2d	|- ( n = ( m x. k ) -> ( R ` ( x / n ) ) = ( R ` ( x / ( m x. k ) ) ) )
107		fvoveq1	|- ( n = ( m x. k ) -> ( Lam ` ( n / m ) ) = ( Lam ` ( ( m x. k ) / m ) ) )
108	107	oveq2d	|- ( n = ( m x. k ) -> ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) = ( ( Lam ` m ) x. ( Lam ` ( ( m x. k ) / m ) ) ) )
109	106 108	oveq12d	|- ( n = ( m x. k ) -> ( ( R ` ( x / n ) ) x. ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) = ( ( R ` ( x / ( m x. k ) ) ) x. ( ( Lam ` m ) x. ( Lam ` ( ( m x. k ) / m ) ) ) ) )
110	31	adantrr	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ m e. { y e. NN | y || n } ) ) -> ( R ` ( x / n ) ) e. RR )
111	40	anasss	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ m e. { y e. NN | y || n } ) ) -> ( Lam ` m ) e. RR )
112	45	anasss	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ m e. { y e. NN | y || n } ) ) -> ( Lam ` ( n / m ) ) e. RR )
113	111 112	remulcld	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ m e. { y e. NN | y || n } ) ) -> ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) e. RR )
114	110 113	remulcld	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ m e. { y e. NN | y || n } ) ) -> ( ( R ` ( x / n ) ) x. ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) e. RR )
115	114	recnd	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ m e. { y e. NN | y || n } ) ) -> ( ( R ` ( x / n ) ) x. ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) e. CC )
116	109 5 115	dvdsflsumcom	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. { y e. NN | y || n } ( ( R ` ( x / n ) ) x. ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) = sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( R ` ( x / ( m x. k ) ) ) x. ( ( Lam ` m ) x. ( Lam ` ( ( m x. k ) / m ) ) ) ) )
117	58	ad2antrr	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> x e. CC )
118		elfznn	|- ( m e. ( 1 ... ( |_ ` x ) ) -> m e. NN )
119	118	adantl	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> m e. NN )
120	119	nnrpd	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> m e. RR+ )
121	120	adantr	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> m e. RR+ )
122	121	rpcnd	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> m e. CC )
123		elfznn	|- ( k e. ( 1 ... ( |_ ` ( x / m ) ) ) -> k e. NN )
124	123	adantl	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> k e. NN )
125	124	nncnd	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> k e. CC )
126	121	rpne0d	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> m =/= 0 )
127	124	nnne0d	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> k =/= 0 )
128	117 122 125 126 127	divdiv1d	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> ( ( x / m ) / k ) = ( x / ( m x. k ) ) )
129	128	eqcomd	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> ( x / ( m x. k ) ) = ( ( x / m ) / k ) )
130	129	fveq2d	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> ( R ` ( x / ( m x. k ) ) ) = ( R ` ( ( x / m ) / k ) ) )
131	125 122 126	divcan3d	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> ( ( m x. k ) / m ) = k )
132	131	fveq2d	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> ( Lam ` ( ( m x. k ) / m ) ) = ( Lam ` k ) )
133	132	oveq2d	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> ( ( Lam ` m ) x. ( Lam ` ( ( m x. k ) / m ) ) ) = ( ( Lam ` m ) x. ( Lam ` k ) ) )
134	130 133	oveq12d	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> ( ( R ` ( x / ( m x. k ) ) ) x. ( ( Lam ` m ) x. ( Lam ` ( ( m x. k ) / m ) ) ) ) = ( ( R ` ( ( x / m ) / k ) ) x. ( ( Lam ` m ) x. ( Lam ` k ) ) ) )
135	13	ad2antrr	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> x e. RR+ )
136	135 121	rpdivcld	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> ( x / m ) e. RR+ )
137	124	nnrpd	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> k e. RR+ )
138	136 137	rpdivcld	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> ( ( x / m ) / k ) e. RR+ )
139	14	ffvelcdmi	|- ( ( ( x / m ) / k ) e. RR+ -> ( R ` ( ( x / m ) / k ) ) e. RR )
140	138 139	syl	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> ( R ` ( ( x / m ) / k ) ) e. RR )
141	140	recnd	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> ( R ` ( ( x / m ) / k ) ) e. CC )
142	119 39	syl	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` m ) e. RR )
143	142	recnd	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` m ) e. CC )
144	143	adantr	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> ( Lam ` m ) e. CC )
145		vmacl	|- ( k e. NN -> ( Lam ` k ) e. RR )
146	124 145	syl	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> ( Lam ` k ) e. RR )
147	146	recnd	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> ( Lam ` k ) e. CC )
148	144 147	mulcld	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> ( ( Lam ` m ) x. ( Lam ` k ) ) e. CC )
149	141 148	mulcomd	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> ( ( R ` ( ( x / m ) / k ) ) x. ( ( Lam ` m ) x. ( Lam ` k ) ) ) = ( ( ( Lam ` m ) x. ( Lam ` k ) ) x. ( R ` ( ( x / m ) / k ) ) ) )
150	144 147 141	mulassd	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> ( ( ( Lam ` m ) x. ( Lam ` k ) ) x. ( R ` ( ( x / m ) / k ) ) ) = ( ( Lam ` m ) x. ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) )
151	134 149 150	3eqtrd	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> ( ( R ` ( x / ( m x. k ) ) ) x. ( ( Lam ` m ) x. ( Lam ` ( ( m x. k ) / m ) ) ) ) = ( ( Lam ` m ) x. ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) )
152	151	sumeq2dv	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( R ` ( x / ( m x. k ) ) ) x. ( ( Lam ` m ) x. ( Lam ` ( ( m x. k ) / m ) ) ) ) = sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` m ) x. ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) )
153		fzfid	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( x / m ) ) ) e. Fin )
154	146 140	remulcld	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) e. RR )
155	154	recnd	|- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) e. CC )
156	153 143 155	fsummulc2	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) = sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` m ) x. ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) )
157	152 156	eqtr4d	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( R ` ( x / ( m x. k ) ) ) x. ( ( Lam ` m ) x. ( Lam ` ( ( m x. k ) / m ) ) ) ) = ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) )
158	157	sumeq2dv	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( R ` ( x / ( m x. k ) ) ) x. ( ( Lam ` m ) x. ( Lam ` ( ( m x. k ) / m ) ) ) ) = sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) )
159	104 116 158	3eqtrd	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) = sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) )
160	159	oveq1d	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) = ( sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) )
161	97 101 160	3eqtrd	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) = ( sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) )
162	161	oveq2d	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) = ( ( 2 / ( log ` x ) ) x. ( sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) )
163	153 154	fsumrecl	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) e. RR )
164	142 163	remulcld	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) e. RR )
165	24 164	fsumrecl	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) e. RR )
166	165	recnd	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) e. CC )
167	49 31	remulcld	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) e. RR )
168	167 50	remulcld	|- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) e. RR )
169	24 168	fsumrecl	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) e. RR )
170	169	recnd	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) e. CC )
171	23 166 170	subdid	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. ( sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) = ( ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) )
172	162 171	eqtrd	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) = ( ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) )
173	172	oveq2d	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) ) = ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) - ( ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) ) )
174	23 166	mulcld	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) ) e. CC )
175	22 169	remulcld	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) e. RR )
176	175	recnd	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) e. CC )
177	20 174 176	subsub3d	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) - ( ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) ) = ( ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) ) ) )
178	173 177	eqtrd	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) ) = ( ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) ) ) )
179	67	2timesd	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) = ( ( ( R ` x ) x. ( log ` x ) ) + ( ( R ` x ) x. ( log ` x ) ) ) )
180	179	oveq1d	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) = ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( R ` x ) x. ( log ` x ) ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) )
181	67 176 67	add32d	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) + ( ( R ` x ) x. ( log ` x ) ) ) = ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( R ` x ) x. ( log ` x ) ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) )
182	180 181	eqtr4d	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) = ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) + ( ( R ` x ) x. ( log ` x ) ) ) )
183	182	oveq1d	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) ) ) = ( ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) + ( ( R ` x ) x. ( log ` x ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) ) ) )
184	18 175	readdcld	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) e. RR )
185	184	recnd	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) e. CC )
186	185 67 174	addsubassd	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) + ( ( R ` x ) x. ( log ` x ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) ) ) = ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) + ( ( ( R ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) ) ) ) )
187	178 183 186	3eqtrd	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) ) = ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) + ( ( ( R ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) ) ) ) )
188	187	oveq1d	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) ) / x ) = ( ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) + ( ( ( R ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) ) ) ) / x ) )
189	67 174	subcld	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( R ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) ) ) e. CC )
190	185 189 58 60	divdird	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) + ( ( ( R ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) ) ) ) / x ) = ( ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) + ( ( ( ( R ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) ) ) / x ) ) )
191	188 190	eqtrd	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) ) / x ) = ( ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) + ( ( ( ( R ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) ) ) / x ) ) )
192	191	mpteq2dva	|- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) ) / x ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) + ( ( ( ( R ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) ) ) / x ) ) ) )
193	184 13	rerpdivcld	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) e. RR )
194	22 165	remulcld	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) ) e. RR )
195	18 194	resubcld	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( R ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) ) ) e. RR )
196	195 13	rerpdivcld	|- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( R ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) ) ) / x ) e. RR )
197	1	selberg3r	|- ( x e. ( 1 (,) +oo ) |-> ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) ) e. O(1)
198	197	a1i	|- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) ) e. O(1) )
199	1	selberg4r	|- ( x e. ( 1 (,) +oo ) |-> ( ( ( ( R ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) ) ) / x ) ) e. O(1)
200	199	a1i	|- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( R ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) ) ) / x ) ) e. O(1) )
201	193 196 198 200	o1add2	|- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) + ( ( ( ( R ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. sum_ k e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` k ) x. ( R ` ( ( x / m ) / k ) ) ) ) ) ) / x ) ) ) e. O(1) )
202	192 201	eqeltrd	|- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) ) / x ) ) e. O(1) )
203		ioossre	|- ( 1 (,) +oo ) C_ RR
204		1cnd	|- ( T. -> 1 e. CC )
205	204	halfcld	|- ( T. -> ( 1 / 2 ) e. CC )
206		o1const	|- ( ( ( 1 (,) +oo ) C_ RR /\ ( 1 / 2 ) e. CC ) -> ( x e. ( 1 (,) +oo ) |-> ( 1 / 2 ) ) e. O(1) )
207	203 205 206	sylancr	|- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( 1 / 2 ) ) e. O(1) )
208	84 85 202 207	o1mul2	|- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( 2 x. ( ( R ` x ) x. ( log ` x ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) ) / x ) x. ( 1 / 2 ) ) ) e. O(1) )
209	81 208	eqeltrrd	|- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) / x ) ) e. O(1) )
210	209	mptru	|- ( x e. ( 1 (,) +oo ) |-> ( ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) / x ) ) e. O(1)