Theorem vmalogdivsum2 24425

Description: The sum sum_ n <_ x , Λ ( n ) log ( x / n ) / n is asymptotic to log ^ 2 ( x ) / 2 + O ( log x ). Exercise 9.1.7 of [Shapiro], p. 336. (Contributed by Mario Carneiro, 30-May-2016.)

Assertion

Ref	Expression
vmalogdivsum2	|- ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1)

Distinct variable group:   x, n

Proof of Theorem vmalogdivsum2

Dummy variables k m y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fzfid 12218	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
2		elfznn 11857	. . . . . . . . . . . . 13 |- ( k e. ( 1 ... ( |_ ` x ) ) -> k e. NN )
3	2	adantl 472	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> k e. NN )
4	3	nnrpd 11368	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> k e. RR+ )
5	4	relogcld 23621	. . . . . . . . . 10 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` k ) e. RR )
6	5, 3	nndivred 10686	. . . . . . . . 9 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` k ) / k ) e. RR )
7	1, 6	fsumrecl 13849	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) e. RR )
8	7	recnd 9695	. . . . . . 7 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) e. CC )
9		elioore 11695	. . . . . . . . . . . . 13 |- ( x e. ( 1 (,) +oo ) -> x e. RR )
10	9	adantl 472	. . . . . . . . . . . 12 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
11		1rp 11335	. . . . . . . . . . . . 13 |- 1 e. RR+
12	11	a1i 11	. . . . . . . . . . . 12 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ )
13		1red 9684	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR )
14		eliooord 11723	. . . . . . . . . . . . . . 15 |- ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
15	14	adantl 472	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 < x /\ x < +oo ) )
16	15	simpld 465	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 < x )
17	13, 10, 16	ltled 9809	. . . . . . . . . . . 12 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x )
18	10, 12, 17	rpgecld 11406	. . . . . . . . . . 11 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
19	18	relogcld 23621	. . . . . . . . . 10 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR )
20	19	resqcld 12474	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) ^ 2 ) e. RR )
21	20	rehalfcld 10888	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) ^ 2 ) / 2 ) e. RR )
22	21	recnd 9695	. . . . . . 7 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) ^ 2 ) / 2 ) e. CC )
23	19	recnd 9695	. . . . . . 7 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
24	10, 16	rplogcld 23627	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
25	24	rpne0d 11375	. . . . . . 7 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
26	8, 22, 23, 25	divsubdird 10450	. . . . . 6 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) / ( log ` x ) ) = ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( ( ( log ` x ) ^ 2 ) / 2 ) / ( log ` x ) ) ) )
27	7, 21	resubcld 10075	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) e. RR )
28	27	recnd 9695	. . . . . . 7 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) e. CC )
29	28, 23, 25	divrecd 10414	. . . . . 6 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) / ( log ` x ) ) = ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) x. ( 1 / ( log ` x ) ) ) )
30	20	recnd 9695	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) ^ 2 ) e. CC )
31		2cnd 10710	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 e. CC )
32		2ne0 10730	. . . . . . . . . 10 |- 2 =/= 0
33	32	a1i 11	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 =/= 0 )
34	30, 31, 23, 33, 25	divdiv32d 10436	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( log ` x ) ^ 2 ) / 2 ) / ( log ` x ) ) = ( ( ( ( log ` x ) ^ 2 ) / ( log ` x ) ) / 2 ) )
35	23	sqvald 12445	. . . . . . . . . . 11 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) ^ 2 ) = ( ( log ` x ) x. ( log ` x ) ) )
36	35	oveq1d 6330	. . . . . . . . . 10 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) ^ 2 ) / ( log ` x ) ) = ( ( ( log ` x ) x. ( log ` x ) ) / ( log ` x ) ) )
37	23, 23, 25	divcan3d 10416	. . . . . . . . . 10 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) x. ( log ` x ) ) / ( log ` x ) ) = ( log ` x ) )
38	36, 37	eqtrd 2496	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) ^ 2 ) / ( log ` x ) ) = ( log ` x ) )
39	38	oveq1d 6330	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( log ` x ) ^ 2 ) / ( log ` x ) ) / 2 ) = ( ( log ` x ) / 2 ) )
40	34, 39	eqtrd 2496	. . . . . . 7 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( log ` x ) ^ 2 ) / 2 ) / ( log ` x ) ) = ( ( log ` x ) / 2 ) )
41	40	oveq2d 6331	. . . . . 6 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( ( ( log ` x ) ^ 2 ) / 2 ) / ( log ` x ) ) ) = ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) )
42	26, 29, 41	3eqtr3rd 2505	. . . . 5 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) = ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) x. ( 1 / ( log ` x ) ) ) )
43	42	mpteq2dva 4503	. . . 4 |- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) x. ( 1 / ( log ` x ) ) ) ) )
44	24	rprecred 11381	. . . . 5 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 / ( log ` x ) ) e. RR )
45	18	ex 440	. . . . . . 7 |- ( T. -> ( x e. ( 1 (,) +oo ) -> x e. RR+ ) )
46	45	ssrdv 3450	. . . . . 6 |- ( T. -> ( 1 (,) +oo ) C_ RR+ )
47		eqid 2462	. . . . . . . . 9 |- ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) ) = ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) )
48	47	logdivsum 24420	. . . . . . . 8 |- ( ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) ) : RR+ --> RR /\ ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) ) e. dom ~~> r /\ ( ( ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) ) ~~> r 1 /\ 1 e. RR+ /\ _e <_ 1 ) -> ( abs ` ( ( ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) ) ` 1 ) - 1 ) ) <_ ( ( log ` 1 ) / 1 ) ) )
49	48	simp2i 1024	. . . . . . 7 |- ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) ) e. dom ~~> r
50		rlimdmo1 13730	. . . . . . 7 |- ( ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) ) e. dom ~~> r -> ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) ) e. O(1) )
51	49, 50	mp1i 13	. . . . . 6 |- ( T. -> ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) ) e. O(1) )
52	46, 51	o1res2 13676	. . . . 5 |- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) ) e. O(1) )
53		divlogrlim 23629	. . . . . 6 |- ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~> r 0
54		rlimo1 13729	. . . . . 6 |- ( ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~> r 0 -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O(1) )
55	53, 54	mp1i 13	. . . . 5 |- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) e. O(1) )
56	27, 44, 52, 55	o1mul2 13737	. . . 4 |- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) x. ( 1 / ( log ` x ) ) ) ) e. O(1) )
57	43, 56	eqeltrd 2540	. . 3 |- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1) )
58	8, 23, 25	divcld 10411	. . . . 5 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) e. CC )
59	23	halfcld 10886	. . . . 5 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / 2 ) e. CC )
60	58, 59	subcld 10012	. . . 4 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) e. CC )
61		elfznn 11857	. . . . . . . . . . . 12 |- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
62	61	adantl 472	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
63		vmacl 24094	. . . . . . . . . . 11 |- ( n e. NN -> (Λ ` n ) e. RR )
64	62, 63	syl 17	. . . . . . . . . 10 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> (Λ ` n ) e. RR )
65	64, 62	nndivred 10686	. . . . . . . . 9 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (Λ ` n ) / n ) e. RR )
66	18	adantr 471	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ )
67	62	nnrpd 11368	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
68	66, 67	rpdivcld 11387	. . . . . . . . . 10 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
69	68	relogcld 23621	. . . . . . . . 9 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. RR )
70	65, 69	remulcld 9697	. . . . . . . 8 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) e. RR )
71	1, 70	fsumrecl 13849	. . . . . . 7 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) e. RR )
72	71	recnd 9695	. . . . . 6 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC )
73	24	rpcnd 11372	. . . . . 6 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
74	72, 73, 25	divcld 10411	. . . . 5 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) e. CC )
75	73	halfcld 10886	. . . . 5 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / 2 ) e. CC )
76	74, 75	subcld 10012	. . . 4 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) e. CC )
77	58, 74, 59	nnncan2d 10047	. . . . . . 7 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) = ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) )
78	8, 72, 23, 25	divsubdird 10450	. . . . . . 7 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) / ( log ` x ) ) = ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) ) )
79		fzfid 12218	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( x / n ) ) ) e. Fin )
80	64	adantr 471	. . . . . . . . . . . . 13 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> (Λ ` n ) e. RR )
81	62	adantr 471	. . . . . . . . . . . . . 14 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> n e. NN )
82		elfznn 11857	. . . . . . . . . . . . . . 15 |- ( m e. ( 1 ... ( |_ ` ( x / n ) ) ) -> m e. NN )
83	82	adantl 472	. . . . . . . . . . . . . 14 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. NN )
84	81, 83	nnmulcld 10685	. . . . . . . . . . . . 13 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( n x. m ) e. NN )
85	80, 84	nndivred 10686	. . . . . . . . . . . 12 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( (Λ ` n ) / ( n x. m ) ) e. RR )
86	79, 85	fsumrecl 13849	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` n ) / ( n x. m ) ) e. RR )
87	86	recnd 9695	. . . . . . . . . 10 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` n ) / ( n x. m ) ) e. CC )
88	70	recnd 9695	. . . . . . . . . 10 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC )
89	1, 87, 88	fsumsub 13898	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` n ) / ( n x. m ) ) - ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` n ) / ( n x. m ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
90	64	recnd 9695	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> (Λ ` n ) e. CC )
91	62	nncnd 10653	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
92	62	nnne0d 10682	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n =/= 0 )
93	90, 91, 92	divcld 10411	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (Λ ` n ) / n ) e. CC )
94	83	nnrecred 10683	. . . . . . . . . . . . . 14 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( 1 / m ) e. RR )
95	79, 94	fsumrecl 13849	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) e. RR )
96	95	recnd 9695	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) e. CC )
97	69	recnd 9695	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. CC )
98	93, 96, 97	subdid 10102	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( (Λ ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) = ( ( ( (Λ ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) - ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
99	90	adantr 471	. . . . . . . . . . . . . . . 16 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> (Λ ` n ) e. CC )
100	91	adantr 471	. . . . . . . . . . . . . . . 16 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> n e. CC )
101	83	nncnd 10653	. . . . . . . . . . . . . . . 16 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. CC )
102	92	adantr 471	. . . . . . . . . . . . . . . 16 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> n =/= 0 )
103	83	nnne0d 10682	. . . . . . . . . . . . . . . 16 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m =/= 0 )
104	99, 100, 101, 102, 103	divdiv1d 10442	. . . . . . . . . . . . . . 15 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( (Λ ` n ) / n ) / m ) = ( (Λ ` n ) / ( n x. m ) ) )
105	99, 100, 102	divcld 10411	. . . . . . . . . . . . . . . 16 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( (Λ ` n ) / n ) e. CC )
106	105, 101, 103	divrecd 10414	. . . . . . . . . . . . . . 15 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( (Λ ` n ) / n ) / m ) = ( ( (Λ ` n ) / n ) x. ( 1 / m ) ) )
107	104, 106	eqtr3d 2498	. . . . . . . . . . . . . 14 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( (Λ ` n ) / ( n x. m ) ) = ( ( (Λ ` n ) / n ) x. ( 1 / m ) ) )
108	107	sumeq2dv 13818	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` n ) / ( n x. m ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( (Λ ` n ) / n ) x. ( 1 / m ) ) )
109	101, 103	reccld 10404	. . . . . . . . . . . . . 14 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( 1 / m ) e. CC )
110	79, 93, 109	fsummulc2 13894	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( (Λ ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( (Λ ` n ) / n ) x. ( 1 / m ) ) )
111	108, 110	eqtr4d 2499	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` n ) / ( n x. m ) ) = ( ( (Λ ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) )
112	111	oveq1d 6330	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` n ) / ( n x. m ) ) - ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = ( ( ( (Λ ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) - ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
113	98, 112	eqtr4d 2499	. . . . . . . . . 10 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( (Λ ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) = ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` n ) / ( n x. m ) ) - ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
114	113	sumeq2dv 13818	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` n ) / ( n x. m ) ) - ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
115		vmasum 24193	. . . . . . . . . . . . . . 15 |- ( k e. NN -> sum_ n e. { y e. NN | y || k } (Λ ` n ) = ( log ` k ) )
116	3, 115	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> sum_ n e. { y e. NN | y || k } (Λ ` n ) = ( log ` k ) )
117	116	oveq1d 6330	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ n e. { y e. NN | y || k } (Λ ` n ) / k ) = ( ( log ` k ) / k ) )
118		fzfid 12218	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... k ) e. Fin )
119		sgmss 24082	. . . . . . . . . . . . . . . 16 |- ( k e. NN -> { y e. NN | y || k } C_ ( 1 ... k ) )
120	3, 119	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> { y e. NN | y || k } C_ ( 1 ... k ) )
121		ssfi 7818	. . . . . . . . . . . . . . 15 |- ( ( ( 1 ... k ) e. Fin /\ { y e. NN | y || k } C_ ( 1 ... k ) ) -> { y e. NN | y || k } e. Fin )
122	118, 120, 121	syl2anc 671	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> { y e. NN | y || k } e. Fin )
123	3	nncnd 10653	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> k e. CC )
124		ssrab2 3526	. . . . . . . . . . . . . . . . . 18 |- { y e. NN | y || k } C_ NN
125		simprr 771	. . . . . . . . . . . . . . . . . 18 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> n e. { y e. NN | y || k } )
126	124, 125	sseldi 3442	. . . . . . . . . . . . . . . . 17 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> n e. NN )
127	126, 63	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> (Λ ` n ) e. RR )
128	127	recnd 9695	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> (Λ ` n ) e. CC )
129	128	anassrs 658	. . . . . . . . . . . . . 14 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) /\ n e. { y e. NN | y || k } ) -> (Λ ` n ) e. CC )
130	3	nnne0d 10682	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> k =/= 0 )
131	122, 123, 129, 130	fsumdivc 13896	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ n e. { y e. NN | y || k } (Λ ` n ) / k ) = sum_ n e. { y e. NN | y || k } ( (Λ ` n ) / k ) )
132	117, 131	eqtr3d 2498	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` k ) / k ) = sum_ n e. { y e. NN | y || k } ( (Λ ` n ) / k ) )
133	132	sumeq2dv 13818	. . . . . . . . . . 11 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) = sum_ k e. ( 1 ... ( |_ ` x ) ) sum_ n e. { y e. NN | y || k } ( (Λ ` n ) / k ) )
134		oveq2 6323	. . . . . . . . . . . 12 |- ( k = ( n x. m ) -> ( (Λ ` n ) / k ) = ( (Λ ` n ) / ( n x. m ) ) )
135	2	ad2antrl 739	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> k e. NN )
136	135	nncnd 10653	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> k e. CC )
137	135	nnne0d 10682	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> k =/= 0 )
138	128, 136, 137	divcld 10411	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> ( (Λ ` n ) / k ) e. CC )
139	134, 10, 138	dvdsflsumcom 24166	. . . . . . . . . . 11 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) sum_ n e. { y e. NN | y || k } ( (Λ ` n ) / k ) = sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` n ) / ( n x. m ) ) )
140	133, 139	eqtrd 2496	. . . . . . . . . 10 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) = sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` n ) / ( n x. m ) ) )
141	140	oveq1d 6330	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( (Λ ` n ) / ( n x. m ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
142	89, 114, 141	3eqtr4rd 2507	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) )
143	142	oveq1d 6330	. . . . . . 7 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) ) / ( log ` x ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) )
144	77, 78, 143	3eqtr2d 2502	. . . . . 6 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) )
145	144	mpteq2dva 4503	. . . . 5 |- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) )
146		1red 9684	. . . . . . 7 |- ( T. -> 1 e. RR )
147	1, 65	fsumrecl 13849	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) e. RR )
148	147, 24	rerpdivcld 11398	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) e. RR )
149		ioossre 11725	. . . . . . . . . . 11 |- ( 1 (,) +oo ) C_ RR
150		ax-1cn 9623	. . . . . . . . . . 11 |- 1 e. CC
151		o1const 13732	. . . . . . . . . . 11 |- ( ( ( 1 (,) +oo ) C_ RR /\ 1 e. CC ) -> ( x e. ( 1 (,) +oo ) |-> 1 ) e. O(1) )
152	149, 150, 151	mp2an 683	. . . . . . . . . 10 |- ( x e. ( 1 (,) +oo ) |-> 1 ) e. O(1)
153	152	a1i 11	. . . . . . . . 9 |- ( T. -> ( x e. ( 1 (,) +oo ) |-> 1 ) e. O(1) )
154	148	recnd 9695	. . . . . . . . . 10 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) e. CC )
155	12	rpcnd 11372	. . . . . . . . . 10 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. CC )
156	147	recnd 9695	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) e. CC )
157	156, 23, 23, 25	divsubdird 10450	. . . . . . . . . . . . 13 |- ( ( T. /\ 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 ) ) ) )
158	156, 23	subcld 10012	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) - ( log ` x ) ) e. CC )
159	158, 23, 25	divrecd 10414	. . . . . . . . . . . . 13 |- ( ( T. /\ 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 ) ) ) )
160	23, 25	dividd 10409	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / ( log ` x ) ) = 1 )
161	160	oveq2d 6331	. . . . . . . . . . . . 13 |- ( ( T. /\ 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 ) )
162	157, 159, 161	3eqtr3rd 2505	. . . . . . . . . . . 12 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) - 1 ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) - ( log ` x ) ) x. ( 1 / ( log ` x ) ) ) )
163	162	mpteq2dva 4503	. . . . . . . . . . 11 |- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) - 1 ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) - ( log ` x ) ) x. ( 1 / ( log ` x ) ) ) ) )
164	147, 19	resubcld 10075	. . . . . . . . . . . 12 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) - ( log ` x ) ) e. RR )
165		vmadivsum 24369	. . . . . . . . . . . . . 14 |- ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) - ( log ` x ) ) ) e. O(1)
166	165	a1i 11	. . . . . . . . . . . . 13 |- ( T. -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) - ( log ` x ) ) ) e. O(1) )
167	46, 166	o1res2 13676	. . . . . . . . . . . 12 |- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) - ( log ` x ) ) ) e. O(1) )
168	164, 44, 167, 55	o1mul2 13737	. . . . . . . . . . 11 |- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) - ( log ` x ) ) x. ( 1 / ( log ` x ) ) ) ) e. O(1) )
169	163, 168	eqeltrd 2540	. . . . . . . . . 10 |- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) - 1 ) ) e. O(1) )
170	154, 155, 169	o1dif 13742	. . . . . . . . 9 |- ( T. -> ( ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) ) e. O(1) <-> ( x e. ( 1 (,) +oo ) |-> 1 ) e. O(1) ) )
171	153, 170	mpbird 240	. . . . . . . 8 |- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) ) e. O(1) )
172	148, 171	o1lo1d 13652	. . . . . . 7 |- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) ) e. <_O(1) )
173	95, 69	resubcld 10075	. . . . . . . . . 10 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) e. RR )
174	65, 173	remulcld 9697	. . . . . . . . 9 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( (Λ ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) e. RR )
175	1, 174	fsumrecl 13849	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) e. RR )
176	175, 24	rerpdivcld 11398	. . . . . . 7 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) e. RR )
177		1red 9684	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
178		vmage0 24097	. . . . . . . . . . . . . 14 |- ( n e. NN -> 0 <_ (Λ ` n ) )
179	62, 178	syl 17	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ (Λ ` n ) )
180	64, 67, 179	divge0d 11407	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( (Λ ` n ) / n ) )
181	68	rpred 11370	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR )
182	91	mulid2d 9687	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. n ) = n )
183		fznnfl 12121	. . . . . . . . . . . . . . . . . 18 |- ( x e. RR -> ( n e. ( 1 ... ( |_ ` x ) ) <-> ( n e. NN /\ n <_ x ) ) )
184	10, 183	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( n e. ( 1 ... ( |_ ` x ) ) <-> ( n e. NN /\ n <_ x ) ) )
185	184	simplbda 634	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n <_ x )
186	182, 185	eqbrtrd 4437	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. n ) <_ x )
187	10	adantr 471	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR )
188	177, 187, 67	lemuldivd 11416	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 x. n ) <_ x <-> 1 <_ ( x / n ) ) )
189	186, 188	mpbid 215	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ ( x / n ) )
190		harmonicubnd 23984	. . . . . . . . . . . . . 14 |- ( ( ( x / n ) e. RR /\ 1 <_ ( x / n ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) <_ ( ( log ` ( x / n ) ) + 1 ) )
191	181, 189, 190	syl2anc 671	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) <_ ( ( log ` ( x / n ) ) + 1 ) )
192	95, 69, 177	lesubadd2d 10240	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) <_ 1 <-> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) <_ ( ( log ` ( x / n ) ) + 1 ) ) )
193	191, 192	mpbird 240	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) <_ 1 )
194	173, 177, 65, 180, 193	lemul2ad 10575	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( (Λ ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) <_ ( ( (Λ ` n ) / n ) x. 1 ) )
195	93	mulid1d 9686	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( (Λ ` n ) / n ) x. 1 ) = ( (Λ ` n ) / n ) )
196	194, 195	breqtrd 4441	. . . . . . . . . 10 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( (Λ ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) <_ ( (Λ ` n ) / n ) )
197	1, 174, 65, 196	fsumle 13908	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) )
198	175, 147, 24, 197	lediv1dd 11425	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) )
199	198	adantrr 728	. . . . . . 7 |- ( ( T. /\ ( x e. ( 1 (,) +oo ) /\ 1 <_ x ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) )
200	146, 172, 148, 176, 199	lo1le 13764	. . . . . 6 |- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) e. <_O(1) )
201		0red 9670	. . . . . . 7 |- ( T. -> 0 e. RR )
202		harmoniclbnd 23983	. . . . . . . . . . . 12 |- ( ( x / n ) e. RR+ -> ( log ` ( x / n ) ) <_ sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) )
203	68, 202	syl 17	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) <_ sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) )
204	95, 69	subge0d 10231	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 0 <_ ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) <-> ( log ` ( x / n ) ) <_ sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) )
205	203, 204	mpbird 240	. . . . . . . . . 10 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) )
206	65, 173, 180, 205	mulge0d 10218	. . . . . . . . 9 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( (Λ ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) )
207	1, 174, 206	fsumge0 13904	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 0 <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) )
208	175, 24, 207	divge0d 11407	. . . . . . 7 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) )
209	176, 201, 208	o1lo12 13651	. . . . . 6 |- ( T. -> ( ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) e. O(1) <-> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) e. <_O(1) ) )
210	200, 209	mpbird 240	. . . . 5 |- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) / ( log ` x ) ) ) e. O(1) )
211	145, 210	eqeltrd 2540	. . . 4 |- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) ) e. O(1) )
212	60, 76, 211	o1dif 13742	. . 3 |- ( T. -> ( ( x e. ( 1 (,) +oo ) |-> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1) <-> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1) ) )
213	57, 212	mpbid 215	. 2 |- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1) )
214	213	trud 1464	1 |- ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1)

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   /\ w3a 991   = wceq 1455   T. wtru 1456   e. wcel 1898   =/= wne 2633   {crab 2753   C_ wss 3416   class class class wbr 4416   |-> cmpt 4475   dom cdm 4853   -->wf 5597   ` cfv 5601  (class class class)co 6315   Fincfn 7595   CCcc 9563   RRcr 9564   0cc0 9565   1c1 9566   + caddc 9568   x. cmul 9570   +oocpnf 9698   < clt 9701   <_ cle 9702   - cmin 9886   / cdiv 10297   NNcn 10637   2c2 10687   RR+crp 11331   (,)cioo 11664   ...cfz 11813   |_cfl 12058   ^cexp 12304   abscabs 13346   ~~> r crli 13598   O(1)co1 13599   <_O(1)clo1 13600   sum_csu 13801   _eceu 14164   || cdvds 14354   logclog 23553  Λcvma 24067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-inf2 8172  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642  ax-pre-sup 9643  ax-addf 9644  ax-mulf 9645

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-fal 1461  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-iin 4295  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-se 4813  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-of 6558  df-om 6720  df-1st 6820  df-2nd 6821  df-supp 6942  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-1o 7208  df-2o 7209  df-oadd 7212  df-er 7389  df-map 7500  df-pm 7501  df-ixp 7549  df-en 7596  df-dom 7597  df-sdom 7598  df-fin 7599  df-fsupp 7910  df-fi 7951  df-sup 7982  df-inf 7983  df-oi 8051  df-card 8399  df-cda 8624  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-div 10298  df-nn 10638  df-2 10696  df-3 10697  df-4 10698  df-5 10699  df-6 10700  df-7 10701  df-8 10702  df-9 10703  df-10 10704  df-n0 10899  df-z 10967  df-dec 11081  df-uz 11189  df-q 11294  df-rp 11332  df-xneg 11438  df-xadd 11439  df-xmul 11440  df-ioo 11668  df-ioc 11669  df-ico 11670  df-icc 11671  df-fz 11814  df-fzo 11947  df-fl 12060  df-mod 12129  df-seq 12246  df-exp 12305  df-fac 12492  df-bc 12520  df-hash 12548  df-shft 13179  df-cj 13211  df-re 13212  df-im 13213  df-sqrt 13347  df-abs 13348  df-limsup 13575  df-clim 13601  df-rlim 13602  df-o1 13603  df-lo1 13604  df-sum 13802  df-ef 14170  df-e 14171  df-sin 14172  df-cos 14173  df-pi 14175  df-dvds 14355  df-gcd 14518  df-prm 14672  df-pc 14836  df-struct 15172  df-ndx 15173  df-slot 15174  df-base 15175  df-sets 15176  df-ress 15177  df-plusg 15252  df-mulr 15253  df-starv 15254  df-sca 15255  df-vsca 15256  df-ip 15257  df-tset 15258  df-ple 15259  df-ds 15261  df-unif 15262  df-hom 15263  df-cco 15264  df-rest 15370  df-topn 15371  df-0g 15389  df-gsum 15390  df-topgen 15391  df-pt 15392  df-prds 15395  df-xrs 15449  df-qtop 15455  df-imas 15456  df-xps 15459  df-mre 15541  df-mrc 15542  df-acs 15544  df-mgm 16537  df-sgrp 16576  df-mnd 16586  df-submnd 16632  df-mulg 16725  df-cntz 17020  df-cmn 17481  df-psmet 19011  df-xmet 19012  df-met 19013  df-bl 19014  df-mopn 19015  df-fbas 19016  df-fg 19017  df-cnfld 19020  df-top 19970  df-bases 19971  df-topon 19972  df-topsp 19973  df-cld 20083  df-ntr 20084  df-cls 20085  df-nei 20163  df-lp 20201  df-perf 20202  df-cn 20292  df-cnp 20293  df-haus 20380  df-cmp 20451  df-tx 20626  df-hmeo 20819  df-fil 20910  df-fm 21002  df-flim 21003  df-flf 21004  df-xms 21384  df-ms 21385  df-tms 21386  df-cncf 21959  df-limc 22870  df-dv 22871  df-log 23555  df-cxp 23556  df-em 23967  df-cht 24072  df-vma 24073  df-chp 24074  df-ppi 24075

This theorem is referenced by:  vmalogdivsum  24426  2vmadivsumlem  24427  selberg4lem1  24447