Theorem selberg4lem1 20703

Description: Lemma for selberg4 20704. Equation 10.4.20 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)

Hypotheses

Ref	Expression
selberg4lem1.1	|- ( ph -> A e. RR+ )
selberg4lem1.2	|- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( y / i ) ) ) ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ A )

Assertion

Ref	Expression
selberg4lem1	|- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( log ` x ) ) ) e. O ( 1 ) )

Distinct variable groups:   i, m, n, x, y, A   ph, m, n, x

Allowed substitution hints:   ph( y, i)

Proof of Theorem selberg4lem1

Step	Hyp	Ref	Expression
1		2cn 9811	. . . . . . 7 |- 2 e. CC
2	1	a1i 12	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 2 e. CC )
3		fzfid 11029	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
4		elfznn 10813	. . . . . . . . . . . . 13 |- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
5	4	adantl 454	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
6		vmacl 20350	. . . . . . . . . . . 12 |- ( n e. NN -> (Λ ` n ) e. RR )
7	5, 6	syl 17	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> (Λ ` n ) e. RR )
8	7, 5	nndivred 9789	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (Λ ` n ) / n ) e. RR )
9		elioore 10680	. . . . . . . . . . . . . . 15 |- ( x e. ( 1 (,) +oo ) -> x e. RR )
10	9	adantl 454	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
11		1rp 10353	. . . . . . . . . . . . . . 15 |- 1 e. RR+
12	11	a1i 12	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ )
13	12	rpred 10385	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR )
14		eliooord 10704	. . . . . . . . . . . . . . . . 17 |- ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
15	14	adantl 454	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 < x /\ x < +oo ) )
16	15	simpld 447	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 < x )
17	13, 10, 16	ltled 8962	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x )
18	10, 12, 17	rpgecld 10420	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
19	18	adantr 453	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ )
20	5	nnrpd 10384	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
21	19, 20	rpdivcld 10402	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
22	21	relogcld 19968	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. RR )
23	8, 22	remulcld 8858	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) e. RR )
24	3, 23	fsumrecl 12201	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) e. RR )
25	10, 16	rplogcld 19974	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
26	24, 25	rerpdivcld 10412	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) e. RR )
27	26	recnd 8856	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) e. CC )
28	18	relogcld 19968	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR )
29	28	rehalfcld 9953	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / 2 ) e. RR )
30	29	recnd 8856	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / 2 ) e. CC )
31	2, 27, 30	subdid 9230	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) = ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) - ( 2 x. ( ( log ` x ) / 2 ) ) ) )
32	28	recnd 8856	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
33		2ne0 9824	. . . . . . . 8 |- 2 =/= 0
34	33	a1i 12	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 2 =/= 0 )
35	32, 2, 34	divcan2d 9533	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( ( log ` x ) / 2 ) ) = ( log ` x ) )
36	35	oveq2d 5835	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) - ( 2 x. ( ( log ` x ) / 2 ) ) ) = ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) - ( log ` x ) ) )
37	31, 36	eqtrd 2316	. . . 4 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) = ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) - ( log ` x ) ) )
38	37	mpteq2dva 4107	. . 3 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 2 x. ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) - ( log ` x ) ) ) )
39		2re 9810	. . . . 5 |- 2 e. RR
40	39	a1i 12	. . . 4 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 2 e. RR )
41	26, 29	resubcld 9206	. . . 4 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) e. RR )
42		ioossre 10706	. . . . . 6 |- ( 1 (,) +oo ) C_ RR
43		o1const 12087	. . . . . 6 |- ( ( ( 1 (,) +oo ) C_ RR /\ 2 e. CC ) -> ( x e. ( 1 (,) +oo ) |-> 2 ) e. O ( 1 ) )
44	42, 1, 43	mp2an 656	. . . . 5 |- ( x e. ( 1 (,) +oo ) |-> 2 ) e. O ( 1 )
45	44	a1i 12	. . . 4 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> 2 ) e. O ( 1 ) )
46		vmalogdivsum2 20681	. . . . 5 |- ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O ( 1 )
47	46	a1i 12	. . . 4 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O ( 1 ) )
48	40, 41, 45, 47	o1mul2 12092	. . 3 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 2 x. ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) ) e. O ( 1 ) )
49	38, 48	eqeltrrd 2359	. 2 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) - ( log ` x ) ) ) e. O ( 1 ) )
50		fzfid 11029	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( x / n ) ) ) e. Fin )
51		elfznn 10813	. . . . . . . . . . . 12 |- ( m e. ( 1 ... ( |_ ` ( x / n ) ) ) -> m e. NN )
52	51	adantl 454	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. NN )
53		vmacl 20350	. . . . . . . . . . 11 |- ( m e. NN -> (Λ ` m ) e. RR )
54	52, 53	syl 17	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> (Λ ` m ) e. RR )
55	52	nnrpd 10384	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. RR+ )
56	55	relogcld 19968	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( log ` m ) e. RR )
57	10	adantr 453	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR )
58	57, 5	nndivred 9789	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR )
59	58	adantr 453	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( x / n ) e. RR )
60	59, 52	nndivred 9789	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( x / n ) / m ) e. RR )
61		chpcl 20356	. . . . . . . . . . . 12 |- ( ( ( x / n ) / m ) e. RR -> (ψ ` ( ( x / n ) / m ) ) e. RR )
62	60, 61	syl 17	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> (ψ ` ( ( x / n ) / m ) ) e. RR )
63	56, 62	readdcld 8857	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) e. RR )
64	54, 63	remulcld 8858	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) e. RR )
65	50, 64	fsumrecl 12201	. . . . . . . 8 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) e. RR )
66	7, 65	remulcld 8858	. . . . . . 7 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) e. RR )
67	3, 66	fsumrecl 12201	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) e. RR )
68	18, 25	rpmulcld 10401	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) e. RR+ )
69	67, 68	rerpdivcld 10412	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) e. RR )
70	69, 28	resubcld 9206	. . . 4 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( log ` x ) ) e. RR )
71	70	recnd 8856	. . 3 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( log ` x ) ) e. CC )
72	24	recnd 8856	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC )
73	25	rpne0d 10390	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
74	72, 32, 73	divcld 9531	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) e. CC )
75	2, 74	mulcld 8850	. . . 4 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) e. CC )
76	75, 32	subcld 9152	. . 3 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) - ( log ` x ) ) e. CC )
77	69	recnd 8856	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) e. CC )
78	77, 75, 32	nnncan2d 9187	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( log ` x ) ) - ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) - ( log ` x ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) ) )
79	67	recnd 8856	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) e. CC )
80	10	recnd 8856	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. CC )
81	18	rpne0d 10390	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x =/= 0 )
82	79, 80, 32, 81, 73	divdiv1d 9562	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / x ) / ( log ` x ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) )
83	2, 72, 32, 73	divassd 9566	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) / ( log ` x ) ) = ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) )
84	82, 83	oveq12d 5837	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / x ) / ( log ` x ) ) - ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) ) )
85	67, 18	rerpdivcld 10412	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / x ) e. RR )
86	85	recnd 8856	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / x ) e. CC )
87	2, 72	mulcld 8850	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. CC )
88	86, 87, 32, 73	divsubdird 9570	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / x ) - ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) / ( log ` x ) ) = ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / x ) / ( log ` x ) ) - ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) )
89	81	adantr 453	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x =/= 0 )
90	66, 57, 89	redivcld 9583	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / x ) e. RR )
91	90	recnd 8856	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / x ) e. CC )
92	39	a1i 12	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 2 e. RR )
93	92, 23	remulcld 8858	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. RR )
94	93	recnd 8856	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. CC )
95	3, 91, 94	fsumsub 12244	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / x ) - ( 2 x. ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / x ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( 2 x. ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) )
96	7	recnd 8856	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> (Λ ` n ) e. CC )
97	65, 57, 89	redivcld 9583	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) e. RR )
98	97	recnd 8856	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) e. CC )
99	1	a1i 12	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 2 e. CC )
100	22	recnd 8856	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. CC )
101	5	nncnd 9757	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
102	5	nnne0d 9785	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n =/= 0 )
103	100, 101, 102	divcld 9531	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / n ) ) / n ) e. CC )
104	99, 103	mulcld 8850	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( log ` ( x / n ) ) / n ) ) e. CC )
105	96, 98, 104	subdid 9230	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (Λ ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) = ( ( (Λ ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) ) - ( (Λ ` n ) x. ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) )
106	65	recnd 8856	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) e. CC )
107	80	adantr 453	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. CC )
108	96, 106, 107, 89	divassd 9566	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / x ) = ( (Λ ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) ) )
109	96, 101, 100, 102	div32d 9554	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) = ( (Λ ` n ) x. ( ( log ` ( x / n ) ) / n ) ) )
110	109	oveq2d 5835	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = ( 2 x. ( (Λ ` n ) x. ( ( log ` ( x / n ) ) / n ) ) ) )
111	99, 96, 103	mul12d 9016	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( (Λ ` n ) x. ( ( log ` ( x / n ) ) / n ) ) ) = ( (Λ ` n ) x. ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) )
112	110, 111	eqtrd 2316	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = ( (Λ ` n ) x. ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) )
113	108, 112	oveq12d 5837	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / x ) - ( 2 x. ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) = ( ( (Λ ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) ) - ( (Λ ` n ) x. ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) )
114	105, 113	eqtr4d 2319	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (Λ ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) = ( ( ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / x ) - ( 2 x. ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) )
115	114	sumeq2dv 12170	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / x ) - ( 2 x. ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) )
116	66	recnd 8856	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) e. CC )
117	3, 80, 116, 81	fsumdivc 12242	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / x ) )
118	23	recnd 8856	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC )
119	3, 2, 118	fsummulc2 12240	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( 2 x. ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
120	117, 119	oveq12d 5837	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / x ) - ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / x ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( 2 x. ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) )
121	95, 115, 120	3eqtr4rd 2327	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / x ) - ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) )
122	121	oveq1d 5834	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / x ) - ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) / ( log ` x ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) / ( log ` x ) ) )
123	88, 122	eqtr3d 2318	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / x ) / ( log ` x ) ) - ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) / ( log ` x ) ) )
124	78, 84, 123	3eqtr2d 2322	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( log ` x ) ) - ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) - ( log ` x ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) / ( log ` x ) ) )
125	124	mpteq2dva 4107	. . . 4 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( log ` x ) ) - ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) - ( log ` x ) ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) / ( log ` x ) ) ) )
126		1re 8832	. . . . . 6 |- 1 e. RR
127	126	a1i 12	. . . . 5 |- ( ph -> 1 e. RR )
128		selberg4lem1.1	. . . . . . . 8 |- ( ph -> A e. RR+ )
129	128	adantr 453	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> A e. RR+ )
130	129	rpred 10385	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> A e. RR )
131	3, 8	fsumrecl 12201	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) e. RR )
132	131, 25	rerpdivcld 10412	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) e. RR )
133	128	rpcnd 10387	. . . . . . 7 |- ( ph -> A e. CC )
134		o1const 12087	. . . . . . 7 |- ( ( ( 1 (,) +oo ) C_ RR /\ A e. CC ) -> ( x e. ( 1 (,) +oo ) |-> A ) e. O ( 1 ) )
135	42, 133, 134	sylancr 647	. . . . . 6 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> A ) e. O ( 1 ) )
136	127	recnd 8856	. . . . . . . 8 |- ( ph -> 1 e. CC )
137		o1const 12087	. . . . . . . 8 |- ( ( ( 1 (,) +oo ) C_ RR /\ 1 e. CC ) -> ( x e. ( 1 (,) +oo ) |-> 1 ) e. O ( 1 ) )
138	42, 136, 137	sylancr 647	. . . . . . 7 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> 1 ) e. O ( 1 ) )
139	132	recnd 8856	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) e. CC )
140	13	recnd 8856	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. CC )
141	131	recnd 8856	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) e. CC )
142	141, 32, 32, 73	divsubdird 9570	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) - ( log ` x ) ) / ( log ` x ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) - ( ( log ` x ) / ( log ` x ) ) ) )
143	141, 32	subcld 9152	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) - ( log ` x ) ) e. CC )
144	143, 32, 73	divrecd 9534	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) - ( log ` x ) ) / ( log ` x ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) - ( log ` x ) ) x. ( 1 / ( log ` x ) ) ) )
145	32, 73	dividd 9529	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / ( log ` x ) ) = 1 )
146	145	oveq2d 5835	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) - ( ( log ` x ) / ( log ` x ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) - 1 ) )
147	142, 144, 146	3eqtr3d 2324	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) - ( log ` x ) ) x. ( 1 / ( log ` x ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) - 1 ) )
148	147	mpteq2dva 4107	. . . . . . . . 9 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) - ( log ` x ) ) x. ( 1 / ( log ` x ) ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) - 1 ) ) )
149	131, 28	resubcld 9206	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) - ( log ` x ) ) e. RR )
150	13, 25	rerpdivcld 10412	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 / ( log ` x ) ) e. RR )
151	18	ex 425	. . . . . . . . . . . 12 |- ( ph -> ( x e. ( 1 (,) +oo ) -> x e. RR+ ) )
152	151	ssrdv 3186	. . . . . . . . . . 11 |- ( ph -> ( 1 (,) +oo ) C_ RR+ )
153		vmadivsum 20625	. . . . . . . . . . . 12 |- ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) - ( log ` x ) ) ) e. O ( 1 )
154	153	a1i 12	. . . . . . . . . . 11 |- ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) - ( log ` x ) ) ) e. O ( 1 ) )
155	152, 154	o1res2 12031	. . . . . . . . . 10 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) - ( log ` x ) ) ) e. O ( 1 ) )
156		divlogrlim 19976	. . . . . . . . . . 11 |- ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~> r 0
157		rlimo1 12084	. . . . . . . . . . 11 |- ( ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~> r 0 -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O ( 1 ) )
158	156, 157	mp1i 13	. . . . . . . . . 10 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O ( 1 ) )
159	149, 150, 155, 158	o1mul2 12092	. . . . . . . . 9 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) - ( log ` x ) ) x. ( 1 / ( log ` x ) ) ) ) e. O ( 1 ) )
160	148, 159	eqeltrrd 2359	. . . . . . . 8 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) - 1 ) ) e. O ( 1 ) )
161	139, 140, 160	o1dif 12097	. . . . . . 7 |- ( ph -> ( ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) ) e. O ( 1 ) <-> ( x e. ( 1 (,) +oo ) |-> 1 ) e. O ( 1 ) ) )
162	138, 161	mpbird 225	. . . . . 6 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) ) e. O ( 1 ) )
163	130, 132, 135, 162	o1mul2 12092	. . . . 5 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( A x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) ) ) e. O ( 1 ) )
164	130, 132	remulcld 8858	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( A x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) ) e. RR )
165	22, 5	nndivred 9789	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / n ) ) / n ) e. RR )
166	92, 165	remulcld 8858	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( log ` ( x / n ) ) / n ) ) e. RR )
167	97, 166	resubcld 9206	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) e. RR )
168	7, 167	remulcld 8858	. . . . . . . 8 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (Λ ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) e. RR )
169	3, 168	fsumrecl 12201	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) e. RR )
170	169, 25	rerpdivcld 10412	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) / ( log ` x ) ) e. RR )
171	170	recnd 8856	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) / ( log ` x ) ) e. CC )
172	169	recnd 8856	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) e. CC )
173	172	abscld 11912	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) e. RR )
174	130, 131	remulcld 8858	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( A x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) ) e. RR )
175	98, 104	subcld 9152	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) e. CC )
176	96, 175	mulcld 8850	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (Λ ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) e. CC )
177	176	abscld 11912	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( (Λ ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) e. RR )
178	3, 177	fsumrecl 12201	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( (Λ ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) e. RR )
179	168	recnd 8856	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (Λ ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) e. CC )
180	3, 179	fsumabs 12253	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( (Λ ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) ) )
181	130	adantr 453	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A e. RR )
182	181, 8	remulcld 8858	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( A x. ( (Λ ` n ) / n ) ) e. RR )
183	175	abscld 11912	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) e. RR )
184	181, 5	nndivred 9789	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( A / n ) e. RR )
185		vmage0 20353	. . . . . . . . . . . . . . 15 |- ( n e. NN -> 0 <_ (Λ ` n ) )
186	5, 185	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ (Λ ` n ) )
187	106, 107, 101, 89, 102	divdiv2d 9563	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / ( x / n ) ) = ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) x. n ) / x ) )
188	106, 101, 107, 89	div23d 9568	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) x. n ) / x ) = ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) x. n ) )
189	187, 188	eqtrd 2316	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / ( x / n ) ) = ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) x. n ) )
190	99, 103, 101	mulassd 8853	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 2 x. ( ( log ` ( x / n ) ) / n ) ) x. n ) = ( 2 x. ( ( ( log ` ( x / n ) ) / n ) x. n ) ) )
191	100, 101, 102	divcan1d 9532	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( log ` ( x / n ) ) / n ) x. n ) = ( log ` ( x / n ) ) )
192	191	oveq2d 5835	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( ( log ` ( x / n ) ) / n ) x. n ) ) = ( 2 x. ( log ` ( x / n ) ) ) )
193	190, 192	eqtr2d 2317	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( log ` ( x / n ) ) ) = ( ( 2 x. ( ( log ` ( x / n ) ) / n ) ) x. n ) )
194	189, 193	oveq12d 5837	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / ( x / n ) ) - ( 2 x. ( log ` ( x / n ) ) ) ) = ( ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) x. n ) - ( ( 2 x. ( ( log ` ( x / n ) ) / n ) ) x. n ) ) )
195	98, 104, 101	subdird 9231	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) x. n ) = ( ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) x. n ) - ( ( 2 x. ( ( log ` ( x / n ) ) / n ) ) x. n ) ) )
196	194, 195	eqtr4d 2319	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / ( x / n ) ) - ( 2 x. ( log ` ( x / n ) ) ) ) = ( ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) x. n ) )
197	196	fveq2d 5489	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / ( x / n ) ) - ( 2 x. ( log ` ( x / n ) ) ) ) ) = ( abs ` ( ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) x. n ) ) )
198	175, 101	absmuld 11930	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) x. n ) ) = ( ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) x. ( abs ` n ) ) )
199	5	nnred 9756	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR )
200	20	rpge0d 10389	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ n )
201	199, 200	absidd 11899	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` n ) = n )
202	201	oveq2d 5835	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) x. ( abs ` n ) ) = ( ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) x. n ) )
203	197, 198, 202	3eqtrd 2320	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / ( x / n ) ) - ( 2 x. ( log ` ( x / n ) ) ) ) ) = ( ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / x ) - ( 2 x. ( ( log ` ( x / n ) ) / n ) ) ) ) x. n ) )
204	101	mulid2d 8848	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. n ) = n )
205		fznnfl 10960	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. RR -> ( n e. ( 1 ... ( |_ ` x ) ) <-> ( n e. NN /\ n <_ x ) ) )
206	10, 205	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( n e. ( 1 ... ( |_ ` x ) ) <-> ( n e. NN /\ n <_ x ) ) )
207	206	simplbda 610	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n <_ x )
208	204, 207	eqbrtrd 4044	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. n ) <_ x )
209	126	a1i 12	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
210	209, 57, 20	lemuldivd 10430	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 x. n ) <_ x <-> 1 <_ ( x / n ) ) )
211	208, 210	mpbid 203	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ ( x / n ) )
212		elicopnf 10733	. . . . . . . . . . . . . . . . . . 19 |- ( 1 e. RR -> ( ( x / n ) e. ( 1 [,) +oo ) <-> ( ( x / n ) e. RR /\ 1 <_ ( x / n ) ) ) )
213	126, 212	ax-mp 10	. . . . . . . . . . . . . . . . . 18 |- ( ( x / n ) e. ( 1 [,) +oo ) <-> ( ( x / n ) e. RR /\ 1 <_ ( x / n ) ) )
214	58, 211, 213	sylanbrc 648	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. ( 1 [,) +oo ) )
215		selberg4lem1.2	. . . . . . . . . . . . . . . . . 18 |- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( y / i ) ) ) ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ A )
216	215	ad2antrr 709	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( y / i ) ) ) ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ A )
217		fveq2 5485	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( i = m -> (Λ ` i ) = (Λ ` m ) )
218		fveq2 5485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( i = m -> ( log ` i ) = ( log ` m ) )
219		oveq2 5827	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( i = m -> ( y / i ) = ( y / m ) )
220	219	fveq2d 5489	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( i = m -> (ψ ` ( y / i ) ) = (ψ ` ( y / m ) ) )
221	218, 220	oveq12d 5837	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( i = m -> ( ( log ` i ) + (ψ ` ( y / i ) ) ) = ( ( log ` m ) + (ψ ` ( y / m ) ) ) )
222	217, 221	oveq12d 5837	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( i = m -> ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( y / i ) ) ) ) = ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( y / m ) ) ) ) )
223	222	cbvsumv 12163	. . . . . . . . . . . . . . . . . . . . . . 23 |- sum_ i e. ( 1 ... ( |_ ` y ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( y / i ) ) ) ) = sum_ m e. ( 1 ... ( |_ ` y ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( y / m ) ) ) )
224		fveq2 5485	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y = ( x / n ) -> ( |_ ` y ) = ( |_ ` ( x / n ) ) )
225	224	oveq2d 5835	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y = ( x / n ) -> ( 1 ... ( |_ ` y ) ) = ( 1 ... ( |_ ` ( x / n ) ) ) )
226		oveq1 5826	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( y = ( x / n ) -> ( y / m ) = ( ( x / n ) / m ) )
227	226	fveq2d 5489	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( y = ( x / n ) -> (ψ ` ( y / m ) ) = (ψ ` ( ( x / n ) / m ) ) )
228	227	oveq2d 5835	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y = ( x / n ) -> ( ( log ` m ) + (ψ ` ( y / m ) ) ) = ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) )
229	228	oveq2d 5835	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y = ( x / n ) -> ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( y / m ) ) ) ) = ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) )
230	229	adantr 453	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( y = ( x / n ) /\ m e. ( 1 ... ( |_ ` y ) ) ) -> ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( y / m ) ) ) ) = ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) )
231	225, 230	sumeq12dv 12173	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y = ( x / n ) -> sum_ m e. ( 1 ... ( |_ ` y ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( y / m ) ) ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) )
232	223, 231	syl5eq 2328	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y = ( x / n ) -> sum_ i e. ( 1 ... ( |_ ` y ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( y / i ) ) ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) )
233		id 21	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y = ( x / n ) -> y = ( x / n ) )
234	232, 233	oveq12d 5837	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = ( x / n ) -> ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( y / i ) ) ) ) / y ) = ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / ( x / n ) ) )
235		fveq2 5485	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y = ( x / n ) -> ( log ` y ) = ( log ` ( x / n ) ) )
236	235	oveq2d 5835	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = ( x / n ) -> ( 2 x. ( log ` y ) ) = ( 2 x. ( log ` ( x / n ) ) ) )
237	234, 236	oveq12d 5837	. . . . . . . . . . . . . . . . . . . 20 |- ( y = ( x / n ) -> ( ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( y / i ) ) ) ) / y ) - ( 2 x. ( log ` y ) ) ) = ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / ( x / n ) ) - ( 2 x. ( log ` ( x / n ) ) ) ) )
238	237	fveq2d 5489	. . . . . . . . . . . . . . . . . . 19 |- ( y = ( x / n ) -> ( abs ` ( ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( y / i ) ) ) ) / y ) - ( 2 x. ( log ` y ) ) ) ) = ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / ( x / n ) ) - ( 2 x. ( log ` ( x / n ) ) ) ) ) )
239	238	breq1d 4034	. . . . . . . . . . . . . . . . . 18 |- ( y = ( x / n ) -> ( ( abs ` ( ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( y / i ) ) ) ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ A <-> ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / ( x / n ) ) - ( 2 x. ( log ` ( x / n ) ) ) ) ) <_ A ) )
240	239	rspcv 2881	. . . . . . . . . . . . . . . . 17 |- ( ( x / n ) e. ( 1 [,) +oo ) -> ( A. y e. ( 1 [,) +oo ) ( abs ` ( ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( y / i ) ) ) ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ A -> ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / ( x / n ) ) - ( 2 x. ( log ` ( x / n ) ) ) ) ) <_ A ) )
241	214, 216, 240	sylc 58	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` m ) x. ( ( log ` m ) + (ψ ` ( ( x / n ) / m ) ) ) ) / ( x / n ) ) - ( 2 x. ( log ` ( x / n ) )