Theorem pntrlog2bndlem2 21225

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

Hypotheses

Ref	Expression
pntsval.1	|- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( (Λ ` i ) x. ( ( log ` i ) + (ψ ` ( a / i ) ) ) ) )
pntrlog2bnd.r	|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )
pntrlog2bndlem2.1	|- ( ph -> A e. RR+ )
pntrlog2bndlem2.2	|- ( ph -> A. y e. RR+ (ψ ` y ) <_ ( A x. y ) )

Assertion

Ref	Expression
pntrlog2bndlem2	|- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) e. O ( 1 ) )

Distinct variable groups:   i, a, n, x, y, A   ph, n, x   S, n, x, y   R, n, x, y

Allowed substitution hints:   ph( y, i, a)   R( i, a)   S( i, a)

Proof of Theorem pntrlog2bndlem2

Dummy variable m is distinct from all other variables.

Step	Hyp	Ref	Expression
1		1re 9046	. . 3 |- 1 e. RR
2	1	a1i 11	. 2 |- ( ph -> 1 e. RR )
3		elioore 10902	. . . . . . . 8 |- ( x e. ( 1 (,) +oo ) -> x e. RR )
4	3	adantl 453	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
5		chpcl 20860	. . . . . . 7 |- ( x e. RR -> (ψ ` x ) e. RR )
6	4, 5	syl 16	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> (ψ ` x ) e. RR )
7	6	recnd 9070	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> (ψ ` x ) e. CC )
8		fzfid 11267	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
9	4	adantr 452	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR )
10		elfznn 11036	. . . . . . . . . . . 12 |- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
11	10	adantl 453	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
12	11	peano2nnd 9973	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n + 1 ) e. NN )
13	9, 12	nndivred 10004	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / ( n + 1 ) ) e. RR )
14		chpcl 20860	. . . . . . . . 9 |- ( ( x / ( n + 1 ) ) e. RR -> (ψ ` ( x / ( n + 1 ) ) ) e. RR )
15	13, 14	syl 16	. . . . . . . 8 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> (ψ ` ( x / ( n + 1 ) ) ) e. RR )
16	15, 13	readdcld 9071	. . . . . . 7 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) e. RR )
17	8, 16	fsumrecl 12483	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) e. RR )
18	17	recnd 9070	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) e. CC )
19	4	recnd 9070	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. CC )
20		eliooord 10926	. . . . . . . . . 10 |- ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
21	20	adantl 453	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 < x /\ x < +oo ) )
22	21	simpld 446	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 < x )
23	4, 22	rplogcld 20477	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
24	23	rpcnd 10606	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
25	19, 24	mulcld 9064	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) e. CC )
26		1rp 10572	. . . . . . . . 9 |- 1 e. RR+
27	26	a1i 11	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ )
28	1	a1i 11	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR )
29	28, 4, 22	ltled 9177	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x )
30	4, 27, 29	rpgecld 10639	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
31	30	rpne0d 10609	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x =/= 0 )
32	23	rpne0d 10609	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
33	19, 24, 31, 32	mulne0d 9630	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) =/= 0 )
34	7, 18, 25, 33	divdird 9784	. . . 4 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( (ψ ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) / ( x x. ( log ` x ) ) ) = ( ( (ψ ` x ) / ( x x. ( log ` x ) ) ) + ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) ) )
35	34	mpteq2dva 4255	. . 3 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( (ψ ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) / ( x x. ( log ` x ) ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( (ψ ` x ) / ( x x. ( log ` x ) ) ) + ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) ) ) )
36	30, 23	rpmulcld 10620	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) e. RR+ )
37	6, 36	rerpdivcld 10631	. . . 4 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( (ψ ` x ) / ( x x. ( log ` x ) ) ) e. RR )
38	17, 36	rerpdivcld 10631	. . . 4 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) e. RR )
39	7, 19, 24, 31, 32	divdiv1d 9777	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( (ψ ` x ) / x ) / ( log ` x ) ) = ( (ψ ` x ) / ( x x. ( log ` x ) ) ) )
40	6, 30	rerpdivcld 10631	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( (ψ ` x ) / x ) e. RR )
41	40	recnd 9070	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( (ψ ` x ) / x ) e. CC )
42	41, 24, 32	divrecd 9749	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( (ψ ` x ) / x ) / ( log ` x ) ) = ( ( (ψ ` x ) / x ) x. ( 1 / ( log ` x ) ) ) )
43	39, 42	eqtr3d 2438	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( (ψ ` x ) / ( x x. ( log ` x ) ) ) = ( ( (ψ ` x ) / x ) x. ( 1 / ( log ` x ) ) ) )
44	43	mpteq2dva 4255	. . . . 5 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( (ψ ` x ) / ( x x. ( log ` x ) ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( (ψ ` x ) / x ) x. ( 1 / ( log ` x ) ) ) ) )
45	23	rprecred 10615	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 / ( log ` x ) ) e. RR )
46	30	ex 424	. . . . . . . 8 |- ( ph -> ( x e. ( 1 (,) +oo ) -> x e. RR+ ) )
47	46	ssrdv 3314	. . . . . . 7 |- ( ph -> ( 1 (,) +oo ) C_ RR+ )
48		chpo1ub 21127	. . . . . . . 8 |- ( x e. RR+ |-> ( (ψ ` x ) / x ) ) e. O ( 1 )
49	48	a1i 11	. . . . . . 7 |- ( ph -> ( x e. RR+ |-> ( (ψ ` x ) / x ) ) e. O ( 1 ) )
50	47, 49	o1res2 12312	. . . . . 6 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( (ψ ` x ) / x ) ) e. O ( 1 ) )
51		divlogrlim 20479	. . . . . . 7 |- ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~> r 0
52		rlimo1 12365	. . . . . . 7 |- ( ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~> r 0 -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O ( 1 ) )
53	51, 52	mp1i 12	. . . . . 6 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O ( 1 ) )
54	40, 45, 50, 53	o1mul2 12373	. . . . 5 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( (ψ ` x ) / x ) x. ( 1 / ( log ` x ) ) ) ) e. O ( 1 ) )
55	44, 54	eqeltrd 2478	. . . 4 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( (ψ ` x ) / ( x x. ( log ` x ) ) ) ) e. O ( 1 ) )
56		pntrlog2bndlem2.1	. . . . . . . . 9 |- ( ph -> A e. RR+ )
57	56	rpred 10604	. . . . . . . 8 |- ( ph -> A e. RR )
58	57, 2	readdcld 9071	. . . . . . 7 |- ( ph -> ( A + 1 ) e. RR )
59	58	adantr 452	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( A + 1 ) e. RR )
60	28, 45	readdcld 9071	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 + ( 1 / ( log ` x ) ) ) e. RR )
61		ioossre 10928	. . . . . . 7 |- ( 1 (,) +oo ) C_ RR
62	58	recnd 9070	. . . . . . 7 |- ( ph -> ( A + 1 ) e. CC )
63		o1const 12368	. . . . . . 7 |- ( ( ( 1 (,) +oo ) C_ RR /\ ( A + 1 ) e. CC ) -> ( x e. ( 1 (,) +oo ) |-> ( A + 1 ) ) e. O ( 1 ) )
64	61, 62, 63	sylancr 645	. . . . . 6 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( A + 1 ) ) e. O ( 1 ) )
65		ax-1cn 9004	. . . . . . . . 9 |- 1 e. CC
66	65	a1i 11	. . . . . . . 8 |- ( ph -> 1 e. CC )
67		o1const 12368	. . . . . . . 8 |- ( ( ( 1 (,) +oo ) C_ RR /\ 1 e. CC ) -> ( x e. ( 1 (,) +oo ) |-> 1 ) e. O ( 1 ) )
68	61, 66, 67	sylancr 645	. . . . . . 7 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> 1 ) e. O ( 1 ) )
69	28, 45, 68, 53	o1add2 12372	. . . . . 6 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( 1 + ( 1 / ( log ` x ) ) ) ) e. O ( 1 ) )
70	59, 60, 64, 69	o1mul2 12373	. . . . 5 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( A + 1 ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) ) e. O ( 1 ) )
71	59, 60	remulcld 9072	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( A + 1 ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) e. RR )
72	38	recnd 9070	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) e. CC )
73		chpge0 20862	. . . . . . . . . . . 12 |- ( ( x / ( n + 1 ) ) e. RR -> 0 <_ (ψ ` ( x / ( n + 1 ) ) ) )
74	13, 73	syl 16	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ (ψ ` ( x / ( n + 1 ) ) ) )
75	11	nnrpd 10603	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
76	26	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR+ )
77	75, 76	rpaddcld 10619	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n + 1 ) e. RR+ )
78	30	adantr 452	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ )
79	78	rpge0d 10608	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ x )
80	9, 77, 79	divge0d 10640	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( x / ( n + 1 ) ) )
81	15, 13, 74, 80	addge0d 9558	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) )
82	8, 16, 81	fsumge0 12529	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) )
83	17, 36, 82	divge0d 10640	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) )
84	38, 83	absidd 12180	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) )
85	71	recnd 9070	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( A + 1 ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) e. CC )
86	85	abscld 12193	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( ( A + 1 ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) ) e. RR )
87	17, 30	rerpdivcld 10631	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / x ) e. RR )
88	30	relogcld 20471	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR )
89	88, 28	readdcld 9071	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) + 1 ) e. RR )
90	59, 89	remulcld 9072	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( A + 1 ) x. ( ( log ` x ) + 1 ) ) e. RR )
91	59, 4	remulcld 9072	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( A + 1 ) x. x ) e. RR )
92	11	nnrecred 10001	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / n ) e. RR )
93	8, 92	fsumrecl 12483	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) e. RR )
94	91, 93	remulcld 9072	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( A + 1 ) x. x ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) ) e. RR )
95	91, 89	remulcld 9072	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( A + 1 ) x. x ) x. ( ( log ` x ) + 1 ) ) e. RR )
96	57	ad2antrr 707	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A e. RR )
97	1	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
98	96, 97	readdcld 9071	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( A + 1 ) e. RR )
99	98, 9	remulcld 9072	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( A + 1 ) x. x ) e. RR )
100	99, 92	remulcld 9072	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( A + 1 ) x. x ) x. ( 1 / n ) ) e. RR )
101	99, 12	nndivred 10004	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( A + 1 ) x. x ) / ( n + 1 ) ) e. RR )
102	99, 11	nndivred 10004	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( A + 1 ) x. x ) / n ) e. RR )
103	96, 13	remulcld 9072	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( A x. ( x / ( n + 1 ) ) ) e. RR )
104	78, 77	rpdivcld 10621	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / ( n + 1 ) ) e. RR+ )
105		pntrlog2bndlem2.2	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> A. y e. RR+ (ψ ` y ) <_ ( A x. y ) )
106	105	ad2antrr 707	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A. y e. RR+ (ψ ` y ) <_ ( A x. y ) )
107		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y = ( x / ( n + 1 ) ) -> (ψ ` y ) = (ψ ` ( x / ( n + 1 ) ) ) )
108		oveq2 6048	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y = ( x / ( n + 1 ) ) -> ( A x. y ) = ( A x. ( x / ( n + 1 ) ) ) )
109	107, 108	breq12d 4185	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = ( x / ( n + 1 ) ) -> ( (ψ ` y ) <_ ( A x. y ) <-> (ψ ` ( x / ( n + 1 ) ) ) <_ ( A x. ( x / ( n + 1 ) ) ) ) )
110	109	rspcv 3008	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x / ( n + 1 ) ) e. RR+ -> ( A. y e. RR+ (ψ ` y ) <_ ( A x. y ) -> (ψ ` ( x / ( n + 1 ) ) ) <_ ( A x. ( x / ( n + 1 ) ) ) ) )
111	104, 106, 110	sylc 58	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> (ψ ` ( x / ( n + 1 ) ) ) <_ ( A x. ( x / ( n + 1 ) ) ) )
112	15, 103, 13, 111	leadd1dd 9596	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) <_ ( ( A x. ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) )
113	62	ad2antrr 707	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( A + 1 ) e. CC )
114	19	adantr 452	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. CC )
115	11	nncnd 9972	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
116	65	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. CC )
117	115, 116	addcld 9063	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n + 1 ) e. CC )
118	12	nnne0d 10000	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n + 1 ) =/= 0 )
119	113, 114, 117, 118	divassd 9781	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( A + 1 ) x. x ) / ( n + 1 ) ) = ( ( A + 1 ) x. ( x / ( n + 1 ) ) ) )
120	96	recnd 9070	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A e. CC )
121	114, 117, 118	divcld 9746	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / ( n + 1 ) ) e. CC )
122	120, 116, 121	adddird 9069	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( A + 1 ) x. ( x / ( n + 1 ) ) ) = ( ( A x. ( x / ( n + 1 ) ) ) + ( 1 x. ( x / ( n + 1 ) ) ) ) )
123	121	mulid2d 9062	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. ( x / ( n + 1 ) ) ) = ( x / ( n + 1 ) ) )
124	123	oveq2d 6056	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( A x. ( x / ( n + 1 ) ) ) + ( 1 x. ( x / ( n + 1 ) ) ) ) = ( ( A x. ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) )
125	119, 122, 124	3eqtrd 2440	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( A + 1 ) x. x ) / ( n + 1 ) ) = ( ( A x. ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) )
126	112, 125	breqtrrd 4198	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) <_ ( ( ( A + 1 ) x. x ) / ( n + 1 ) ) )
127	57	adantr 452	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> A e. RR )
128	56	adantr 452	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> A e. RR+ )
129	128	rpge0d 10608	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ A )
130	27	rpge0d 10608	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ 1 )
131	127, 28, 129, 130	addge0d 9558	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( A + 1 ) )
132	30	rpge0d 10608	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ x )
133	59, 4, 131, 132	mulge0d 9559	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( ( A + 1 ) x. x ) )
134	133	adantr 452	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( A + 1 ) x. x ) )
135	11	nnred 9971	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR )
136	135	lep1d 9898	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n <_ ( n + 1 ) )
137	75, 77, 99, 134, 136	lediv2ad 10626	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( A + 1 ) x. x ) / ( n + 1 ) ) <_ ( ( ( A + 1 ) x. x ) / n ) )
138	16, 101, 102, 126, 137	letrd 9183	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) <_ ( ( ( A + 1 ) x. x ) / n ) )
139	99	recnd 9070	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( A + 1 ) x. x ) e. CC )
140	11	nnne0d 10000	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n =/= 0 )
141	139, 115, 140	divrecd 9749	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( A + 1 ) x. x ) / n ) = ( ( ( A + 1 ) x. x ) x. ( 1 / n ) ) )
142	138, 141	breqtrd 4196	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) <_ ( ( ( A + 1 ) x. x ) x. ( 1 / n ) ) )
143	8, 16, 100, 142	fsumle 12533	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( A + 1 ) x. x ) x. ( 1 / n ) ) )
144	91	recnd 9070	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( A + 1 ) x. x ) e. CC )
145	115, 140	reccld 9739	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / n ) e. CC )
146	8, 144, 145	fsummulc2 12522	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( A + 1 ) x. x ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( A + 1 ) x. x ) x. ( 1 / n ) ) )
147	143, 146	breqtrrd 4198	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) <_ ( ( ( A + 1 ) x. x ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) ) )
148		harmonicubnd 20801	. . . . . . . . . . . . . . 15 |- ( ( x e. RR /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) <_ ( ( log ` x ) + 1 ) )
149	4, 29, 148	syl2anc 643	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) <_ ( ( log ` x ) + 1 ) )
150	93, 89, 91, 133, 149	lemul2ad 9907	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( A + 1 ) x. x ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) ) <_ ( ( ( A + 1 ) x. x ) x. ( ( log ` x ) + 1 ) ) )
151	17, 94, 95, 147, 150	letrd 9183	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) <_ ( ( ( A + 1 ) x. x ) x. ( ( log ` x ) + 1 ) ) )
152	62	adantr 452	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( A + 1 ) e. CC )
153	89	recnd 9070	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) + 1 ) e. CC )
154	152, 19, 153	mul32d 9232	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( A + 1 ) x. x ) x. ( ( log ` x ) + 1 ) ) = ( ( ( A + 1 ) x. ( ( log ` x ) + 1 ) ) x. x ) )
155	151, 154	breqtrd 4196	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) <_ ( ( ( A + 1 ) x. ( ( log ` x ) + 1 ) ) x. x ) )
156	17, 90, 30	ledivmul2d 10654	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / x ) <_ ( ( A + 1 ) x. ( ( log ` x ) + 1 ) ) <-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) <_ ( ( ( A + 1 ) x. ( ( log ` x ) + 1 ) ) x. x ) ) )
157	155, 156	mpbird 224	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / x ) <_ ( ( A + 1 ) x. ( ( log ` x ) + 1 ) ) )
158	87, 90, 23, 157	lediv1dd 10658	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / x ) / ( log ` x ) ) <_ ( ( ( A + 1 ) x. ( ( log ` x ) + 1 ) ) / ( log ` x ) ) )
159	18, 19, 24, 31, 32	divdiv1d 9777	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / x ) / ( log ` x ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) )
160	65	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. CC )
161	24, 160	addcld 9063	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) + 1 ) e. CC )
162	152, 161, 24, 32	divassd 9781	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( A + 1 ) x. ( ( log ` x ) + 1 ) ) / ( log ` x ) ) = ( ( A + 1 ) x. ( ( ( log ` x ) + 1 ) / ( log ` x ) ) ) )
163	24, 160, 24, 32	divdird 9784	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) + 1 ) / ( log ` x ) ) = ( ( ( log ` x ) / ( log ` x ) ) + ( 1 / ( log ` x ) ) ) )
164	24, 32	dividd 9744	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / ( log ` x ) ) = 1 )
165	164	oveq1d 6055	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) / ( log ` x ) ) + ( 1 / ( log ` x ) ) ) = ( 1 + ( 1 / ( log ` x ) ) ) )
166	163, 165	eqtr2d 2437	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 + ( 1 / ( log ` x ) ) ) = ( ( ( log ` x ) + 1 ) / ( log ` x ) ) )
167	166	oveq2d 6056	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( A + 1 ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) = ( ( A + 1 ) x. ( ( ( log ` x ) + 1 ) / ( log ` x ) ) ) )
168	162, 167	eqtr4d 2439	. . . . . . . . 9 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( A + 1 ) x. ( ( log ` x ) + 1 ) ) / ( log ` x ) ) = ( ( A + 1 ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) )
169	158, 159, 168	3brtr3d 4201	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) <_ ( ( A + 1 ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) )
170	71	leabsd 12172	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( A + 1 ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) <_ ( abs ` ( ( A + 1 ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) ) )
171	38, 71, 86, 169, 170	letrd 9183	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) <_ ( abs ` ( ( A + 1 ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) ) )
172	84, 171	eqbrtrd 4192	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) ) <_ ( abs ` ( ( A + 1 ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) ) )
173	172	adantrr 698	. . . . 5 |- ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ 1 <_ x ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) ) <_ ( abs ` ( ( A + 1 ) x. ( 1 + ( 1 / ( log ` x ) ) ) ) ) )
174	2, 70, 71, 72, 173	o1le 12401	. . . 4 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) ) e. O ( 1 ) )
175	37, 38, 55, 174	o1add2 12372	. . 3 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( (ψ ` x ) / ( x x. ( log ` x ) ) ) + ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) / ( x x. ( log ` x ) ) ) ) ) e. O ( 1 ) )
176	35, 175	eqeltrd 2478	. 2 |- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( (ψ ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) / ( x x. ( log ` x ) ) ) ) e. O ( 1 ) )
177	6, 17	readdcld 9071	. . 3 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( (ψ ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) e. RR )
178	177, 36	rerpdivcld 10631	. 2 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( (ψ ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) / ( x x. ( log ` x ) ) ) e. RR )
179		pntrlog2bnd.r	. . . . . . . . . . . 12 |- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )
180	179	pntrf 21210	. . . . . . . . . . 11 |- R : RR+ --> RR
181	180	ffvelrni 5828	. . . . . . . . . 10 |- ( ( x / ( n + 1 ) ) e. RR+ -> ( R ` ( x / ( n + 1 ) ) ) e. RR )
182	104, 181	syl 16	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / ( n + 1 ) ) ) e. RR )
183	182	recnd 9070	. . . . . . . 8 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / ( n + 1 ) ) ) e. CC )
184	78, 75	rpdivcld 10621	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
185	180	ffvelrni 5828	. . . . . . . . . 10 |- ( ( x / n ) e. RR+ -> ( R ` ( x / n ) ) e. RR )
186	184, 185	syl 16	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. RR )
187	186	recnd 9070	. . . . . . . 8 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. CC )
188	183, 187	subcld 9367	. . . . . . 7 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) e. CC )
189	188	abscld 12193	. . . . . 6 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) e. RR )
190	135, 189	remulcld 9072	. . . . 5 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) e. RR )
191	8, 190	fsumrecl 12483	. . . 4 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) e. RR )
192	191, 36	rerpdivcld 10631	. . 3 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) e. RR )
193	192	recnd 9070	. 2 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) e. CC )
194	75	rpge0d 10608	. . . . . . . 8 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ n )
195	188	absge0d 12201	. . . . . . . 8 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) )
196	135, 189, 194, 195	mulge0d 9559	. . . . . . 7 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) )
197	8, 190, 196	fsumge0 12529	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) )
198	191, 36, 197	divge0d 10640	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) )
199	192, 198	absidd 12180	. . . 4 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) / ( x x. ( log ` x ) ) ) )
200	7, 18	addcld 9063	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( (ψ ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) e. CC )
201	200, 25, 33	divcld 9746	. . . . . 6 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( (ψ ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) / ( x x. ( log ` x ) ) ) e. CC )
202	201	abscld 12193	. . . . 5 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( ( (ψ ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) / ( x x. ( log ` x ) ) ) ) e. RR )
203	9, 11	nndivred 10004	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR )
204		chpcl 20860	. . . . . . . . . . . 12 |- ( ( x / n ) e. RR -> (ψ ` ( x / n ) ) e. RR )
205	203, 204	syl 16	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> (ψ ` ( x / n ) ) e. RR )
206	205, 203	readdcld 9071	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (ψ ` ( x / n ) ) + ( x / n ) ) e. RR )
207	206, 16	resubcld 9421	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( (ψ ` ( x / n ) ) + ( x / n ) ) - ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) e. RR )
208	135, 207	remulcld 9072	. . . . . . . 8 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. ( ( (ψ ` ( x / n ) ) + ( x / n ) ) - ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) e. RR )
209	179	pntrval 21209	. . . . . . . . . . . . . . 15 |- ( ( x / ( n + 1 ) ) e. RR+ -> ( R ` ( x / ( n + 1 ) ) ) = ( (ψ ` ( x / ( n + 1 ) ) ) - ( x / ( n + 1 ) ) ) )
210	104, 209	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / ( n + 1 ) ) ) = ( (ψ ` ( x / ( n + 1 ) ) ) - ( x / ( n + 1 ) ) ) )
211	179	pntrval 21209	. . . . . . . . . . . . . . 15 |- ( ( x / n ) e. RR+ -> ( R ` ( x / n ) ) = ( (ψ ` ( x / n ) ) - ( x / n ) ) )
212	184, 211	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) = ( (ψ ` ( x / n ) ) - ( x / n ) ) )
213	210, 212	oveq12d 6058	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) = ( ( (ψ ` ( x / ( n + 1 ) ) ) - ( x / ( n + 1 ) ) ) - ( (ψ ` ( x / n ) ) - ( x / n ) ) ) )
214	15	recnd 9070	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> (ψ ` ( x / ( n + 1 ) ) ) e. CC )
215	205	recnd 9070	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> (ψ ` ( x / n ) ) e. CC )
216	114, 115, 140	divcld 9746	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. CC )
217	214, 121, 215, 216	sub4d 9416	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( (ψ ` ( x / ( n + 1 ) ) ) - ( x / ( n + 1 ) ) ) - ( (ψ ` ( x / n ) ) - ( x / n ) ) ) = ( ( (ψ ` ( x / ( n + 1 ) ) ) - (ψ ` ( x / n ) ) ) - ( ( x / ( n + 1 ) ) - ( x / n ) ) ) )
218	213, 217	eqtrd 2436	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) = ( ( (ψ ` ( x / ( n + 1 ) ) ) - (ψ ` ( x / n ) ) ) - ( ( x / ( n + 1 ) ) - ( x / n ) ) ) )
219	218	fveq2d 5691	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) = ( abs ` ( ( (ψ ` ( x / ( n + 1 ) ) ) - (ψ ` ( x / n ) ) ) - ( ( x / ( n + 1 ) ) - ( x / n ) ) ) ) )
220	214, 215	subcld 9367	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (ψ ` ( x / ( n + 1 ) ) ) - (ψ ` ( x / n ) ) ) e. CC )
221	121, 216	subcld 9367	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( x / ( n + 1 ) ) - ( x / n ) ) e. CC )
222	220, 221	abs2dif2d 12215	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( (ψ ` ( x / ( n + 1 ) ) ) - (ψ ` ( x / n ) ) ) - ( ( x / ( n + 1 ) ) - ( x / n ) ) ) ) <_ ( ( abs ` ( (ψ ` ( x / ( n + 1 ) ) ) - (ψ ` ( x / n ) ) ) ) + ( abs ` ( ( x / ( n + 1 ) ) - ( x / n ) ) ) ) )
223	219, 222	eqbrtrd 4192	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) <_ ( ( abs ` ( (ψ ` ( x / ( n + 1 ) ) ) - (ψ ` ( x / n ) ) ) ) + ( abs ` ( ( x / ( n + 1 ) ) - ( x / n ) ) ) ) )
224	75, 77, 9, 79, 136	lediv2ad 10626	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / ( n + 1 ) ) <_ ( x / n ) )
225		chpwordi 20893	. . . . . . . . . . . . . 14 |- ( ( ( x / ( n + 1 ) ) e. RR /\ ( x / n ) e. RR /\ ( x / ( n + 1 ) ) <_ ( x / n ) ) -> (ψ ` ( x / ( n + 1 ) ) ) <_ (ψ ` ( x / n ) ) )
226	13, 203, 224, 225	syl3anc 1184	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> (ψ ` ( x / ( n + 1 ) ) ) <_ (ψ ` ( x / n ) ) )
227	15, 205, 226	abssuble0d 12190	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( (ψ ` ( x / ( n + 1 ) ) ) - (ψ ` ( x / n ) ) ) ) = ( (ψ ` ( x / n ) ) - (ψ ` ( x / ( n + 1 ) ) ) ) )
228	13, 203, 224	abssuble0d 12190	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( x / ( n + 1 ) ) - ( x / n ) ) ) = ( ( x / n ) - ( x / ( n + 1 ) ) ) )
229	227, 228	oveq12d 6058	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( (ψ ` ( x / ( n + 1 ) ) ) - (ψ ` ( x / n ) ) ) ) + ( abs ` ( ( x / ( n + 1 ) ) - ( x / n ) ) ) ) = ( ( (ψ ` ( x / n ) ) - (ψ ` ( x / ( n + 1 ) ) ) ) + ( ( x / n ) - ( x / ( n + 1 ) ) ) ) )
230	215, 216, 214, 121	addsub4d 9414	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( (ψ ` ( x / n ) ) + ( x / n ) ) - ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) = ( ( (ψ ` ( x / n ) ) - (ψ ` ( x / ( n + 1 ) ) ) ) + ( ( x / n ) - ( x / ( n + 1 ) ) ) ) )
231	229, 230	eqtr4d 2439	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( (ψ ` ( x / ( n + 1 ) ) ) - (ψ ` ( x / n ) ) ) ) + ( abs ` ( ( x / ( n + 1 ) ) - ( x / n ) ) ) ) = ( ( (ψ ` ( x / n ) ) + ( x / n ) ) - ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) )
232	223, 231	breqtrd 4196	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) <_ ( ( (ψ ` ( x / n ) ) + ( x / n ) ) - ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) )
233	189, 207, 135, 194, 232	lemul2ad 9907	. . . . . . . 8 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) <_ ( n x. ( ( (ψ ` ( x / n ) ) + ( x / n ) ) - ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) )
234	8, 190, 208, 233	fsumle 12533	. . . . . . 7 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( abs ` ( ( R ` ( x / ( n + 1 ) ) ) - ( R ` ( x / n ) ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( ( (ψ ` ( x / n ) ) + ( x / n ) ) - ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) )
235	207	recnd 9070	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( (ψ ` ( x / n ) ) + ( x / n ) ) - ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) e. CC )
236	115, 235	mulcld 9064	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. ( ( (ψ ` ( x / n ) ) + ( x / n ) ) - ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) e. CC )
237	8, 236	fsumcl 12482	. . . . . . . 8 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( n x. ( ( (ψ ` ( x / n ) ) + ( x / n ) ) - ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) e. CC )
238	7, 18	negdi2d 9381	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> -u ( (ψ ` x ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) = ( -u (ψ ` x ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) )
239	30	rprege0d 10611	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x e. RR /\ 0 <_ x ) )
240		flge0nn0 11180	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. RR /\ 0 <_ x ) -> ( |_ ` x ) e. NN0 )
241		nn0p1nn 10215	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( |_ ` x ) e. NN0 -> ( ( |_ ` x ) + 1 ) e. NN )
242	239, 240, 241	3syl 19	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) e. NN )
243	4, 242	nndivred 10004	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) e. RR )
244		2re 10025	. . . . . . . . . . . . . . . . . . . 20 |- 2 e. RR
245	244	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 2 e. RR )
246		flltp1 11164	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. RR -> x < ( ( |_ ` x ) + 1 ) )
247	4, 246	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x < ( ( |_ ` x ) + 1 ) )
248	242	nncnd 9972	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) e. CC )
249	248	mulid1d 9061	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( |_ ` x ) + 1 ) x. 1 ) = ( ( |_ ` x ) + 1 ) )
250	247, 249	breqtrrd 4198	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x < ( ( ( |_ ` x ) + 1 ) x. 1 ) )
251	242	nnrpd 10603	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) e. RR+ )
252	4, 28, 251	ltdivmuld 10651	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( x / ( ( |_ ` x ) + 1 ) ) < 1 <-> x < ( ( ( |_ ` x ) + 1 ) x. 1 ) ) )
253	250, 252	mpbird 224	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) < 1 )
254		1lt2 10098	. . . . . . . . . . . . . . . . . . . 20 |- 1 < 2
255	254	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 < 2 )
256	243, 28, 245, 253, 255	lttrd 9187	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) < 2 )
257		chpeq0 20945	. . . . . . . . . . . . . . . . . . 19 |- ( ( x / ( ( |_ ` x ) + 1 ) ) e. RR -> ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) = 0 <-> ( x / ( ( |_ ` x ) + 1 ) ) < 2 ) )
258	243, 257	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) = 0 <-> ( x / ( ( |_ ` x ) + 1 ) ) < 2 ) )
259	256, 258	mpbird 224	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) = 0 )
260	259	oveq1d 6055	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) + ( x / ( ( |_ ` x ) + 1 ) ) ) = ( 0 + ( x / ( ( |_ ` x ) + 1 ) ) ) )
261	243	recnd 9070	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x / ( ( |_ ` x ) + 1 ) ) e. CC )
262	261	addid2d 9223	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 0 + ( x / ( ( |_ ` x ) + 1 ) ) ) = ( x / ( ( |_ ` x ) + 1 ) ) )
263	260, 262	eqtrd 2436	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) + ( x / ( ( |_ ` x ) + 1 ) ) ) = ( x / ( ( |_ ` x ) + 1 ) ) )
264	263	oveq2d 6056	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( |_ ` x ) + 1 ) x. ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) + ( x / ( ( |_ ` x ) + 1 ) ) ) ) = ( ( ( |_ ` x ) + 1 ) x. ( x / ( ( |_ ` x ) + 1 ) ) ) )
265	242	nnne0d 10000	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) =/= 0 )
266	19, 248, 265	divcan2d 9748	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( |_ ` x ) + 1 ) x. ( x / ( ( |_ ` x ) + 1 ) ) ) = x )
267	264, 266	eqtrd 2436	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( |_ ` x ) + 1 ) x. ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) + ( x / ( ( |_ ` x ) + 1 ) ) ) ) = x )
268	19	div1d 9738	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x / 1 ) = x )
269	268	fveq2d 5691	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> (ψ ` ( x / 1 ) ) = (ψ ` x ) )
270	269, 268	oveq12d 6058	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( (ψ ` ( x / 1 ) ) + ( x / 1 ) ) = ( (ψ ` x ) + x ) )
271	270	oveq2d 6056	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 x. ( (ψ ` ( x / 1 ) ) + ( x / 1 ) ) ) = ( 1 x. ( (ψ ` x ) + x ) ) )
272	6, 4	readdcld 9071	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( (ψ ` x ) + x ) e. RR )
273	272	recnd 9070	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( (ψ ` x ) + x ) e. CC )
274	273	mulid2d 9062	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 x. ( (ψ ` x ) + x ) ) = ( (ψ ` x ) + x ) )
275	271, 274	eqtrd 2436	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 x. ( (ψ ` ( x / 1 ) ) + ( x / 1 ) ) ) = ( (ψ ` x ) + x ) )
276	267, 275	oveq12d 6058	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( |_ ` x ) + 1 ) x. ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) + ( x / ( ( |_ ` x ) + 1 ) ) ) ) - ( 1 x. ( (ψ ` ( x / 1 ) ) + ( x / 1 ) ) ) ) = ( x - ( (ψ ` x ) + x ) ) )
277	273, 19	negsubdi2d 9383	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> -u ( ( (ψ ` x ) + x ) - x ) = ( x - ( (ψ ` x ) + x ) ) )
278	7, 19	pncand 9368	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( (ψ ` x ) + x ) - x ) = (ψ ` x ) )
279	278	negeqd 9256	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> -u ( ( (ψ ` x ) + x ) - x ) = -u (ψ ` x ) )
280	276, 277, 279	3eqtr2d 2442	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( |_ ` x ) + 1 ) x. ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) + ( x / ( ( |_ ` x ) + 1 ) ) ) ) - ( 1 x. ( (ψ ` ( x / 1 ) ) + ( x / 1 ) ) ) ) = -u (ψ ` x ) )
281	4	flcld 11162	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( |_ ` x ) e. ZZ )
282		fzval3 11135	. . . . . . . . . . . . . 14 |- ( ( |_ ` x ) e. ZZ -> ( 1 ... ( |_ ` x ) ) = ( 1..^ ( ( |_ ` x ) + 1 ) ) )
283	281, 282	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) = ( 1..^ ( ( |_ ` x ) + 1 ) ) )
284	283	eqcomd 2409	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1..^ ( ( |_ ` x ) + 1 ) ) = ( 1 ... ( |_ ` x ) ) )
285	115, 116	pncan2d 9369	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n + 1 ) - n ) = 1 )
286	285	oveq1d 6055	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( n + 1 ) - n ) x. ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) = ( 1 x. ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) )
287	16	recnd 9070	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) e. CC )
288	287	mulid2d 9062	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) = ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) )
289	286, 288	eqtrd 2436	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( n + 1 ) - n ) x. ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) = ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) )
290	284, 289	sumeq12rdv 12456	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1..^ ( ( |_ ` x ) + 1 ) ) ( ( ( n + 1 ) - n ) x. ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) )
291	280, 290	oveq12d 6058	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( |_ ` x ) + 1 ) x. ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) + ( x / ( ( |_ ` x ) + 1 ) ) ) ) - ( 1 x. ( (ψ ` ( x / 1 ) ) + ( x / 1 ) ) ) ) - sum_ n e. ( 1..^ ( ( |_ ` x ) + 1 ) ) ( ( ( n + 1 ) - n ) x. ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) = ( -u (ψ ` x ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) )
292		oveq2 6048	. . . . . . . . . . . . . . 15 |- ( m = n -> ( x / m ) = ( x / n ) )
293	292	fveq2d 5691	. . . . . . . . . . . . . 14 |- ( m = n -> (ψ ` ( x / m ) ) = (ψ ` ( x / n ) ) )
294	293, 292	oveq12d 6058	. . . . . . . . . . . . 13 |- ( m = n -> ( (ψ ` ( x / m ) ) + ( x / m ) ) = ( (ψ ` ( x / n ) ) + ( x / n ) ) )
295	294	ancli 535	. . . . . . . . . . . 12 |- ( m = n -> ( m = n /\ ( (ψ ` ( x / m ) ) + ( x / m ) ) = ( (ψ ` ( x / n ) ) + ( x / n ) ) ) )
296		oveq2 6048	. . . . . . . . . . . . . . 15 |- ( m = ( n + 1 ) -> ( x / m ) = ( x / ( n + 1 ) ) )
297	296	fveq2d 5691	. . . . . . . . . . . . . 14 |- ( m = ( n + 1 ) -> (ψ ` ( x / m ) ) = (ψ ` ( x / ( n + 1 ) ) ) )
298	297, 296	oveq12d 6058	. . . . . . . . . . . . 13 |- ( m = ( n + 1 ) -> ( (ψ ` ( x / m ) ) + ( x / m ) ) = ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) )
299	298	ancli 535	. . . . . . . . . . . 12 |- ( m = ( n + 1 ) -> ( m = ( n + 1 ) /\ ( (ψ ` ( x / m ) ) + ( x / m ) ) = ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) )
300		oveq2 6048	. . . . . . . . . . . . . . 15 |- ( m = 1 -> ( x / m ) = ( x / 1 ) )
301	300	fveq2d 5691	. . . . . . . . . . . . . 14 |- ( m = 1 -> (ψ ` ( x / m ) ) = (ψ ` ( x / 1 ) ) )
302	301, 300	oveq12d 6058	. . . . . . . . . . . . 13 |- ( m = 1 -> ( (ψ ` ( x / m ) ) + ( x / m ) ) = ( (ψ ` ( x / 1 ) ) + ( x / 1 ) ) )
303	302	ancli 535	. . . . . . . . . . . 12 |- ( m = 1 -> ( m = 1 /\ ( (ψ ` ( x / m ) ) + ( x / m ) ) = ( (ψ ` ( x / 1 ) ) + ( x / 1 ) ) ) )
304		oveq2 6048	. . . . . . . . . . . . . . 15 |- ( m = ( ( |_ ` x ) + 1 ) -> ( x / m ) = ( x / ( ( |_ ` x ) + 1 ) ) )
305	304	fveq2d 5691	. . . . . . . . . . . . . 14 |- ( m = ( ( |_ ` x ) + 1 ) -> (ψ ` ( x / m ) ) = (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) )
306	305, 304	oveq12d 6058	. . . . . . . . . . . . 13 |- ( m = ( ( |_ ` x ) + 1 ) -> ( (ψ ` ( x / m ) ) + ( x / m ) ) = ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) + ( x / ( ( |_ ` x ) + 1 ) ) ) )
307	306	ancli 535	. . . . . . . . . . . 12 |- ( m = ( ( |_ ` x ) + 1 ) -> ( m = ( ( |_ ` x ) + 1 ) /\ ( (ψ ` ( x / m ) ) + ( x / m ) ) = ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) + ( x / ( ( |_ ` x ) + 1 ) ) ) ) )
308		nnuz 10477	. . . . . . . . . . . . 13 |- NN = ( ZZ>= ` 1 )
309	242, 308	syl6eleq 2494	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( |_ ` x ) + 1 ) e. ( ZZ>= ` 1 ) )
310		elfznn 11036	. . . . . . . . . . . . . 14 |- ( m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) -> m e. NN )
311	310	adantl 453	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> m e. NN )
312	311	nncnd 9972	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> m e. CC )
313	4	adantr 452	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> x e. RR )
314	313, 311	nndivred 10004	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( x / m ) e. RR )
315		chpcl 20860	. . . . . . . . . . . . . . 15 |- ( ( x / m ) e. RR -> (ψ ` ( x / m ) ) e. RR )
316	314, 315	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> (ψ ` ( x / m ) ) e. RR )
317	316, 314	readdcld 9071	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( (ψ ` ( x / m ) ) + ( x / m ) ) e. RR )
318	317	recnd 9070	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( (ψ ` ( x / m ) ) + ( x / m ) ) e. CC )
319	295, 299, 303, 307, 309, 312, 318	fsumparts 12540	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1..^ ( ( |_ ` x ) + 1 ) ) ( n x. ( ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) - ( (ψ ` ( x / n ) ) + ( x / n ) ) ) ) = ( ( ( ( ( |_ ` x ) + 1 ) x. ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) + ( x / ( ( |_ ` x ) + 1 ) ) ) ) - ( 1 x. ( (ψ ` ( x / 1 ) ) + ( x / 1 ) ) ) ) - sum_ n e. ( 1..^ ( ( |_ ` x ) + 1 ) ) ( ( ( n + 1 ) - n ) x. ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) )
320	215, 216	addcld 9063	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (ψ ` ( x / n ) ) + ( x / n ) ) e. CC )
321	214, 121	addcld 9063	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) e. CC )
322	320, 321	negsubdi2d 9383	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> -u ( ( (ψ ` ( x / n ) ) + ( x / n ) ) - ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) = ( ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) - ( (ψ ` ( x / n ) ) + ( x / n ) ) ) )
323	322	oveq2d 6056	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. -u ( ( (ψ ` ( x / n ) ) + ( x / n ) ) - ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) = ( n x. ( ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) - ( (ψ ` ( x / n ) ) + ( x / n ) ) ) ) )
324	115, 235	mulneg2d 9443	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. -u ( ( (ψ ` ( x / n ) ) + ( x / n ) ) - ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) = -u ( n x. ( ( (ψ ` ( x / n ) ) + ( x / n ) ) - ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) )
325	323, 324	eqtr3d 2438	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. ( ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) - ( (ψ ` ( x / n ) ) + ( x / n ) ) ) ) = -u ( n x. ( ( (ψ ` ( x / n ) ) + ( x / n ) ) - ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) )
326	284, 325	sumeq12rdv 12456	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1..^ ( ( |_ ` x ) + 1 ) ) ( n x. ( ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) - ( (ψ ` ( x / n ) ) + ( x / n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) -u ( n x. ( ( (ψ ` ( x / n ) ) + ( x / n ) ) - ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) )
327	319, 326	eqtr3d 2438	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( |_ ` x ) + 1 ) x. ( (ψ ` ( x / ( ( |_ ` x ) + 1 ) ) ) + ( x / ( ( |_ ` x ) + 1 ) ) ) ) - ( 1 x. ( (ψ ` ( x / 1 ) ) + ( x / 1 ) ) ) ) - sum_ n e. ( 1..^ ( ( |_ ` x ) + 1 ) ) ( ( ( n + 1 ) - n ) x. ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) -u ( n x. ( ( (ψ ` ( x / n ) ) + ( x / n ) ) - ( (ψ ` ( x / ( n + 1 ) ) ) + ( x / ( n + 1 ) ) ) ) ) )
328	238, 291, 327	3eqtr2d 2442	. . . . . . . . 9 |- ( ( ph /\