Theorem selbergr

Description: Selberg's symmetry formula, using the residual of the second Chebyshev function. Equation 10.6.2 of Shapiro, p. 428. (Contributed by Mario Carneiro, 16-Apr-2016)

	Ref	Expression
Hypothesis	pntrval.r	|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
Assertion	selbergr	|- ( x e. RR+ |-> ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( R ` ( x / d ) ) ) ) / x ) ) e. O(1)

Proof

Step	Hyp	Ref	Expression
1		pntrval.r	|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2		reex	|- RR e. _V
3		rpssre	|- RR+ C_ RR
4	2 3	ssexi	|- RR+ e. _V
5	4	a1i	|- ( T. -> RR+ e. _V )
6		ovexd	|- ( ( T. /\ x e. RR+ ) -> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) e. _V )
7		ovexd	|- ( ( T. /\ x e. RR+ ) -> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) - ( log ` x ) ) e. _V )
8		eqidd	|- ( T. -> ( x e. RR+ |-> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) = ( x e. RR+ |-> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) )
9		eqidd	|- ( T. -> ( x e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) - ( log ` x ) ) ) = ( x e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) - ( log ` x ) ) ) )
10	5 6 7 8 9	offval2	|- ( T. -> ( ( x e. RR+ |-> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) oF - ( x e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) - ( log ` x ) ) ) ) = ( x e. RR+ |-> ( ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) - ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) - ( log ` x ) ) ) ) )
11	10	mptru	|- ( ( x e. RR+ |-> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) oF - ( x e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) - ( log ` x ) ) ) ) = ( x e. RR+ |-> ( ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) - ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) - ( log ` x ) ) ) )
12	1	pntrf	|- R : RR+ --> RR
13	12	ffvelrni	|- ( x e. RR+ -> ( R ` x ) e. RR )
14	13	recnd	|- ( x e. RR+ -> ( R ` x ) e. CC )
15		relogcl	|- ( x e. RR+ -> ( log ` x ) e. RR )
16	15	recnd	|- ( x e. RR+ -> ( log ` x ) e. CC )
17	14 16	mulcld	|- ( x e. RR+ -> ( ( R ` x ) x. ( log ` x ) ) e. CC )
18		fzfid	|- ( x e. RR+ -> ( 1 ... ( |_ ` x ) ) e. Fin )
19		elfznn	|- ( d e. ( 1 ... ( |_ ` x ) ) -> d e. NN )
20	19	adantl	|- ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. NN )
21		vmacl	|- ( d e. NN -> ( Lam ` d ) e. RR )
22	20 21	syl	|- ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` d ) e. RR )
23	22	recnd	|- ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` d ) e. CC )
24		rpre	|- ( x e. RR+ -> x e. RR )
25		nndivre	|- ( ( x e. RR /\ d e. NN ) -> ( x / d ) e. RR )
26	24 19 25	syl2an	|- ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( x / d ) e. RR )
27		chpcl	|- ( ( x / d ) e. RR -> ( psi ` ( x / d ) ) e. RR )
28	26 27	syl	|- ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( x / d ) ) e. RR )
29	28	recnd	|- ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( x / d ) ) e. CC )
30	23 29	mulcld	|- ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) e. CC )
31	18 30	fsumcl	|- ( x e. RR+ -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) e. CC )
32	17 31	addcld	|- ( x e. RR+ -> ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) e. CC )
33		rpcn	|- ( x e. RR+ -> x e. CC )
34		rpne0	|- ( x e. RR+ -> x =/= 0 )
35	32 33 34	divcld	|- ( x e. RR+ -> ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) e. CC )
36	22 20	nndivred	|- ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` d ) / d ) e. RR )
37	36	recnd	|- ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` d ) / d ) e. CC )
38	18 37	fsumcl	|- ( x e. RR+ -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) e. CC )
39	35 38 16	nnncan2d	|- ( x e. RR+ -> ( ( ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( log ` x ) ) - ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) - ( log ` x ) ) ) = ( ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) ) )
40		chpcl	|- ( x e. RR -> ( psi ` x ) e. RR )
41	24 40	syl	|- ( x e. RR+ -> ( psi ` x ) e. RR )
42	41	recnd	|- ( x e. RR+ -> ( psi ` x ) e. CC )
43	42 16	mulcld	|- ( x e. RR+ -> ( ( psi ` x ) x. ( log ` x ) ) e. CC )
44	43 31	addcld	|- ( x e. RR+ -> ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) e. CC )
45	44 33 34	divcld	|- ( x e. RR+ -> ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) e. CC )
46	45 16 16	subsub4d	|- ( x e. RR+ -> ( ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( log ` x ) ) - ( log ` x ) ) = ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( ( log ` x ) + ( log ` x ) ) ) )
47	1	pntrval	|- ( x e. RR+ -> ( R ` x ) = ( ( psi ` x ) - x ) )
48	47	oveq1d	|- ( x e. RR+ -> ( ( R ` x ) x. ( log ` x ) ) = ( ( ( psi ` x ) - x ) x. ( log ` x ) ) )
49	42 33 16	subdird	|- ( x e. RR+ -> ( ( ( psi ` x ) - x ) x. ( log ` x ) ) = ( ( ( psi ` x ) x. ( log ` x ) ) - ( x x. ( log ` x ) ) ) )
50	48 49	eqtrd	|- ( x e. RR+ -> ( ( R ` x ) x. ( log ` x ) ) = ( ( ( psi ` x ) x. ( log ` x ) ) - ( x x. ( log ` x ) ) ) )
51	50	oveq1d	|- ( x e. RR+ -> ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) = ( ( ( ( psi ` x ) x. ( log ` x ) ) - ( x x. ( log ` x ) ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) )
52	33 16	mulcld	|- ( x e. RR+ -> ( x x. ( log ` x ) ) e. CC )
53	43 31 52	addsubd	|- ( x e. RR+ -> ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) - ( x x. ( log ` x ) ) ) = ( ( ( ( psi ` x ) x. ( log ` x ) ) - ( x x. ( log ` x ) ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) )
54	51 53	eqtr4d	|- ( x e. RR+ -> ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) = ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) - ( x x. ( log ` x ) ) ) )
55	54	oveq1d	|- ( x e. RR+ -> ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) = ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) - ( x x. ( log ` x ) ) ) / x ) )
56		rpcnne0	|- ( x e. RR+ -> ( x e. CC /\ x =/= 0 ) )
57		divsubdir	|- ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) e. CC /\ ( x x. ( log ` x ) ) e. CC /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) - ( x x. ( log ` x ) ) ) / x ) = ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( ( x x. ( log ` x ) ) / x ) ) )
58	44 52 56 57	syl3anc	|- ( x e. RR+ -> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) - ( x x. ( log ` x ) ) ) / x ) = ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( ( x x. ( log ` x ) ) / x ) ) )
59	16 33 34	divcan3d	|- ( x e. RR+ -> ( ( x x. ( log ` x ) ) / x ) = ( log ` x ) )
60	59	oveq2d	|- ( x e. RR+ -> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( ( x x. ( log ` x ) ) / x ) ) = ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( log ` x ) ) )
61	55 58 60	3eqtrd	|- ( x e. RR+ -> ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) = ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( log ` x ) ) )
62	61	oveq1d	|- ( x e. RR+ -> ( ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( log ` x ) ) = ( ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( log ` x ) ) - ( log ` x ) ) )
63	16	2timesd	|- ( x e. RR+ -> ( 2 x. ( log ` x ) ) = ( ( log ` x ) + ( log ` x ) ) )
64	63	oveq2d	|- ( x e. RR+ -> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) = ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( ( log ` x ) + ( log ` x ) ) ) )
65	46 62 64	3eqtr4d	|- ( x e. RR+ -> ( ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( log ` x ) ) = ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) )
66	65	oveq1d	|- ( x e. RR+ -> ( ( ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( log ` x ) ) - ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) - ( log ` x ) ) ) = ( ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) - ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) - ( log ` x ) ) ) )
67	33 38	mulcld	|- ( x e. RR+ -> ( x x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) ) e. CC )
68		divsubdir	|- ( ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) e. CC /\ ( x x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) ) e. CC /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) - ( x x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) ) ) / x ) = ( ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( ( x x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) ) / x ) ) )
69	32 67 56 68	syl3anc	|- ( x e. RR+ -> ( ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) - ( x x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) ) ) / x ) = ( ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( ( x x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) ) / x ) ) )
70	17 31 67	addsubassd	|- ( x e. RR+ -> ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) - ( x x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) ) ) = ( ( ( R ` x ) x. ( log ` x ) ) + ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) - ( x x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) ) ) ) )
71	33	adantr	|- ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> x e. CC )
72	71 37	mulcld	|- ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( x x. ( ( Lam ` d ) / d ) ) e. CC )
73	18 30 72	fsumsub	|- ( x e. RR+ -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) - ( x x. ( ( Lam ` d ) / d ) ) ) = ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) - sum_ d e. ( 1 ... ( |_ ` x ) ) ( x x. ( ( Lam ` d ) / d ) ) ) )
74	26	recnd	|- ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( x / d ) e. CC )
75	23 29 74	subdid	|- ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` d ) x. ( ( psi ` ( x / d ) ) - ( x / d ) ) ) = ( ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) - ( ( Lam ` d ) x. ( x / d ) ) ) )
76	19	nnrpd	|- ( d e. ( 1 ... ( |_ ` x ) ) -> d e. RR+ )
77		rpdivcl	|- ( ( x e. RR+ /\ d e. RR+ ) -> ( x / d ) e. RR+ )
78	76 77	sylan2	|- ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( x / d ) e. RR+ )
79	1	pntrval	|- ( ( x / d ) e. RR+ -> ( R ` ( x / d ) ) = ( ( psi ` ( x / d ) ) - ( x / d ) ) )
80	78 79	syl	|- ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / d ) ) = ( ( psi ` ( x / d ) ) - ( x / d ) ) )
81	80	oveq2d	|- ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` d ) x. ( R ` ( x / d ) ) ) = ( ( Lam ` d ) x. ( ( psi ` ( x / d ) ) - ( x / d ) ) ) )
82	20	nnrpd	|- ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. RR+ )
83		rpcnne0	|- ( d e. RR+ -> ( d e. CC /\ d =/= 0 ) )
84	82 83	syl	|- ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( d e. CC /\ d =/= 0 ) )
85		div12	|- ( ( x e. CC /\ ( Lam ` d ) e. CC /\ ( d e. CC /\ d =/= 0 ) ) -> ( x x. ( ( Lam ` d ) / d ) ) = ( ( Lam ` d ) x. ( x / d ) ) )
86	71 23 84 85	syl3anc	|- ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( x x. ( ( Lam ` d ) / d ) ) = ( ( Lam ` d ) x. ( x / d ) ) )
87	86	oveq2d	|- ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) - ( x x. ( ( Lam ` d ) / d ) ) ) = ( ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) - ( ( Lam ` d ) x. ( x / d ) ) ) )
88	75 81 87	3eqtr4d	|- ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` d ) x. ( R ` ( x / d ) ) ) = ( ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) - ( x x. ( ( Lam ` d ) / d ) ) ) )
89	88	sumeq2dv	|- ( x e. RR+ -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( R ` ( x / d ) ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) - ( x x. ( ( Lam ` d ) / d ) ) ) )
90	18 33 37	fsummulc2	|- ( x e. RR+ -> ( x x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) ( x x. ( ( Lam ` d ) / d ) ) )
91	90	oveq2d	|- ( x e. RR+ -> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) - ( x x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) ) ) = ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) - sum_ d e. ( 1 ... ( |_ ` x ) ) ( x x. ( ( Lam ` d ) / d ) ) ) )
92	73 89 91	3eqtr4rd	|- ( x e. RR+ -> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) - ( x x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( R ` ( x / d ) ) ) )
93	92	oveq2d	|- ( x e. RR+ -> ( ( ( R ` x ) x. ( log ` x ) ) + ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) - ( x x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) ) ) ) = ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( R ` ( x / d ) ) ) ) )
94	70 93	eqtrd	|- ( x e. RR+ -> ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) - ( x x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) ) ) = ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( R ` ( x / d ) ) ) ) )
95	94	oveq1d	|- ( x e. RR+ -> ( ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) - ( x x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) ) ) / x ) = ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( R ` ( x / d ) ) ) ) / x ) )
96	38 33 34	divcan3d	|- ( x e. RR+ -> ( ( x x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) ) / x ) = sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) )
97	96	oveq2d	|- ( x e. RR+ -> ( ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( ( x x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) ) / x ) ) = ( ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) ) )
98	69 95 97	3eqtr3rd	|- ( x e. RR+ -> ( ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) ) = ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( R ` ( x / d ) ) ) ) / x ) )
99	39 66 98	3eqtr3d	|- ( x e. RR+ -> ( ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) - ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) - ( log ` x ) ) ) = ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( R ` ( x / d ) ) ) ) / x ) )
100	99	mpteq2ia	|- ( x e. RR+ |-> ( ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) - ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) - ( log ` x ) ) ) ) = ( x e. RR+ |-> ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( R ` ( x / d ) ) ) ) / x ) )
101	11 100	eqtri	|- ( ( x e. RR+ |-> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) oF - ( x e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) - ( log ` x ) ) ) ) = ( x e. RR+ |-> ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( R ` ( x / d ) ) ) ) / x ) )
102		selberg2	|- ( x e. RR+ |-> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)
103		vmadivsum	|- ( x e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) - ( log ` x ) ) ) e. O(1)
104		o1sub	|- ( ( ( x e. RR+ |-> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1) /\ ( x e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) - ( log ` x ) ) ) e. O(1) ) -> ( ( x e. RR+ |-> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) oF - ( x e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) - ( log ` x ) ) ) ) e. O(1) )
105	102 103 104	mp2an	|- ( ( x e. RR+ |-> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) oF - ( x e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) / d ) - ( log ` x ) ) ) ) e. O(1)
106	101 105	eqeltrri	|- ( x e. RR+ |-> ( ( ( ( R ` x ) x. ( log ` x ) ) + sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( R ` ( x / d ) ) ) ) / x ) ) e. O(1)