Theorem vmalogdivsum2 24362

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 12185	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
2		elfznn 11828	. . . . . . . . . . . . 13 |- ( k e. ( 1 ... ( |_ ` x ) ) -> k e. NN )
3	2	adantl 467	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> k e. NN )
4	3	nnrpd 11339	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> k e. RR+ )
5	4	relogcld 23558	. . . . . . . . . 10 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` k ) e. RR )
6	5, 3	nndivred 10658	. . . . . . . . 9 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` k ) / k ) e. RR )
7	1, 6	fsumrecl 13787	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) e. RR )
8	7	recnd 9669	. . . . . . 7 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) e. CC )
9		elioore 11666	. . . . . . . . . . . . 13 |- ( x e. ( 1 (,) +oo ) -> x e. RR )
10	9	adantl 467	. . . . . . . . . . . 12 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
11		1rp 11306	. . . . . . . . . . . . 13 |- 1 e. RR+
12	11	a1i 11	. . . . . . . . . . . 12 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ )
13		1red 9658	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR )
14		eliooord 11694	. . . . . . . . . . . . . . 15 |- ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
15	14	adantl 467	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 < x /\ x < +oo ) )
16	15	simpld 460	. . . . . . . . . . . . 13 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 < x )
17	13, 10, 16	ltled 9783	. . . . . . . . . . . 12 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x )
18	10, 12, 17	rpgecld 11377	. . . . . . . . . . 11 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
19	18	relogcld 23558	. . . . . . . . . 10 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR )
20	19	resqcld 12441	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) ^ 2 ) e. RR )
21	20	rehalfcld 10859	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) ^ 2 ) / 2 ) e. RR )
22	21	recnd 9669	. . . . . . 7 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) ^ 2 ) / 2 ) e. CC )
23	19	recnd 9669	. . . . . . 7 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
24	10, 16	rplogcld 23564	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
25	24	rpne0d 11346	. . . . . . 7 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
26	8, 22, 23, 25	divsubdird 10422	. . . . . 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 10047	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) e. RR )
28	27	recnd 9669	. . . . . . 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 10386	. . . . . 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 9669	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) ^ 2 ) e. CC )
31		2cnd 10682	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 e. CC )
32		2ne0 10702	. . . . . . . . . 10 |- 2 =/= 0
33	32	a1i 11	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 =/= 0 )
34	30, 31, 23, 33, 25	divdiv32d 10408	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( log ` x ) ^ 2 ) / 2 ) / ( log ` x ) ) = ( ( ( ( log ` x ) ^ 2 ) / ( log ` x ) ) / 2 ) )
35	23	sqvald 12412	. . . . . . . . . . 11 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) ^ 2 ) = ( ( log ` x ) x. ( log ` x ) ) )
36	35	oveq1d 6316	. . . . . . . . . 10 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) ^ 2 ) / ( log ` x ) ) = ( ( ( log ` x ) x. ( log ` x ) ) / ( log ` x ) ) )
37	23, 23, 25	divcan3d 10388	. . . . . . . . . 10 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) x. ( log ` x ) ) / ( log ` x ) ) = ( log ` x ) )
38	36, 37	eqtrd 2463	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( log ` x ) ^ 2 ) / ( log ` x ) ) = ( log ` x ) )
39	38	oveq1d 6316	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( log ` x ) ^ 2 ) / ( log ` x ) ) / 2 ) = ( ( log ` x ) / 2 ) )
40	34, 39	eqtrd 2463	. . . . . . 7 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( log ` x ) ^ 2 ) / 2 ) / ( log ` x ) ) = ( ( log ` x ) / 2 ) )
41	40	oveq2d 6317	. . . . . 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 2472	. . . . 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 4507	. . . 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 11352	. . . . 5 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 / ( log ` x ) ) e. RR )
45	18	ex 435	. . . . . . 7 |- ( T. -> ( x e. ( 1 (,) +oo ) -> x e. RR+ ) )
46	45	ssrdv 3470	. . . . . 6 |- ( T. -> ( 1 (,) +oo ) C_ RR+ )
47		eqid 2422	. . . . . . . . 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 24357	. . . . . . . 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 1015	. . . . . . 7 |- ( x e. RR+ |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) ) e. dom ~~> r
50		rlimdmo1 13668	. . . . . . 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 13614	. . . . 5 |- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) - ( ( ( log ` x ) ^ 2 ) / 2 ) ) ) e. O(1) )
53		divlogrlim 23566	. . . . . 6 |- ( x e. ( 1 (,) +oo ) |-> ( 1 / ( log ` x ) ) ) ~~> r 0
54		rlimo1 13667	. . . . . 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 13675	. . . 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 2510	. . 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 10383	. . . . 5 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) e. CC )
59	23	halfcld 10857	. . . . 5 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / 2 ) e. CC )
60	58, 59	subcld 9986	. . . 4 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( log ` k ) / k ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) e. CC )
61		elfznn 11828	. . . . . . . . . . . 12 |- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
62	61	adantl 467	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
63		vmacl 24031	. . . . . . . . . . 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 10658	. . . . . . . . 9 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (Λ ` n ) / n ) e. RR )
66	18	adantr 466	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ )
67	62	nnrpd 11339	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
68	66, 67	rpdivcld 11358	. . . . . . . . . 10 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
69	68	relogcld 23558	. . . . . . . . 9 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. RR )
70	65, 69	remulcld 9671	. . . . . . . 8 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) e. RR )
71	1, 70	fsumrecl 13787	. . . . . . 7 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) e. RR )
72	71	recnd 9669	. . . . . 6 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC )
73	24	rpcnd 11343	. . . . . 6 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
74	72, 73, 25	divcld 10383	. . . . 5 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) / ( log ` x ) ) e. CC )
75	73	halfcld 10857	. . . . 5 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / 2 ) e. CC )
76	74, 75	subcld 9986	. . . 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 10021	. . . . . . 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 10422	. . . . . . 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 12185	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( x / n ) ) ) e. Fin )
80	64	adantr 466	. . . . . . . . . . . . 13 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> (Λ ` n ) e. RR )
81	62	adantr 466	. . . . . . . . . . . . . 14 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> n e. NN )
82		elfznn 11828	. . . . . . . . . . . . . . 15 |- ( m e. ( 1 ... ( |_ ` ( x / n ) ) ) -> m e. NN )
83	82	adantl 467	. . . . . . . . . . . . . 14 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. NN )
84	81, 83	nnmulcld 10657	. . . . . . . . . . . . 13 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( n x. m ) e. NN )
85	80, 84	nndivred 10658	. . . . . . . . . . . 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 13787	. . . . . . . . . . 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 9669	. . . . . . . . . 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 9669	. . . . . . . . . 10 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( (Λ ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC )
89	1, 87, 88	fsumsub 13836	. . . . . . . . 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 9669	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> (Λ ` n ) e. CC )
91	62	nncnd 10625	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
92	62	nnne0d 10654	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n =/= 0 )
93	90, 91, 92	divcld 10383	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( (Λ ` n ) / n ) e. CC )
94	83	nnrecred 10655	. . . . . . . . . . . . . 14 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( 1 / m ) e. RR )
95	79, 94	fsumrecl 13787	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) e. RR )
96	95	recnd 9669	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) e. CC )
97	69	recnd 9669	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. CC )
98	93, 96, 97	subdid 10074	. . . . . . . . . . 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 466	. . . . . . . . . . . . . . . 16 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> (Λ ` n ) e. CC )
100	91	adantr 466	. . . . . . . . . . . . . . . 16 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> n e. CC )
101	83	nncnd 10625	. . . . . . . . . . . . . . . 16 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. CC )
102	92	adantr 466	. . . . . . . . . . . . . . . 16 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> n =/= 0 )
103	83	nnne0d 10654	. . . . . . . . . . . . . . . 16 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m =/= 0 )
104	99, 100, 101, 102, 103	divdiv1d 10414	. . . . . . . . . . . . . . 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 10383	. . . . . . . . . . . . . . . 16 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( (Λ ` n ) / n ) e. CC )
106	105, 101, 103	divrecd 10386	. . . . . . . . . . . . . . 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 2465	. . . . . . . . . . . . . 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 13756	. . . . . . . . . . . . 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 10376	. . . . . . . . . . . . . 14 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( 1 / m ) e. CC )
110	79, 93, 109	fsummulc2 13832	. . . . . . . . . . . . 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 2466	. . . . . . . . . . . 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 6316	. . . . . . . . . . 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 2466	. . . . . . . . . 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 13756	. . . . . . . . 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 24130	. . . . . . . . . . . . . . 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 6316	. . . . . . . . . . . . 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 12185	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... k ) e. Fin )
119		sgmss 24019	. . . . . . . . . . . . . . . 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 7794	. . . . . . . . . . . . . . 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 665	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> { y e. NN | y || k } e. Fin )
123	3	nncnd 10625	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> k e. CC )
124		ssrab2 3546	. . . . . . . . . . . . . . . . . 18 |- { y e. NN | y || k } C_ NN
125		simprr 764	. . . . . . . . . . . . . . . . . 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 3462	. . . . . . . . . . . . . . . . 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 9669	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> (Λ ` n ) e. CC )
129	128	anassrs 652	. . . . . . . . . . . . . 14 |- ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) /\ n e. { y e. NN | y || k } ) -> (Λ ` n ) e. CC )
130	3	nnne0d 10654	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> k =/= 0 )
131	122, 123, 129, 130	fsumdivc 13834	. . . . . . . . . . . . 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 2465	. . . . . . . . . . . 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 13756	. . . . . . . . . . 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 6309	. . . . . . . . . . . 12 |- ( k = ( n x. m ) -> ( (Λ ` n ) / k ) = ( (Λ ` n ) / ( n x. m ) ) )
135	2	ad2antrl 732	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> k e. NN )
136	135	nncnd 10625	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> k e. CC )
137	135	nnne0d 10654	. . . . . . . . . . . . 13 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> k =/= 0 )
138	128, 136, 137	divcld 10383	. . . . . . . . . . . 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 24103	. . . . . . . . . . 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 2463	. . . . . . . . . 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 6316	. . . . . . . . 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 2474	. . . . . . . 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 6316	. . . . . . 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 2469	. . . . . 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 4507	. . . . 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 9658	. . . . . . 7 |- ( T. -> 1 e. RR )
147	1, 65	fsumrecl 13787	. . . . . . . . 9 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) e. RR )
148	147, 24	rerpdivcld 11369	. . . . . . . 8 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) e. RR )
149		ioossre 11696	. . . . . . . . . . 11 |- ( 1 (,) +oo ) C_ RR
150		ax-1cn 9597	. . . . . . . . . . 11 |- 1 e. CC
151		o1const 13670	. . . . . . . . . . 11 |- ( ( ( 1 (,) +oo ) C_ RR /\ 1 e. CC ) -> ( x e. ( 1 (,) +oo ) |-> 1 ) e. O(1) )
152	149, 150, 151	mp2an 676	. . . . . . . . . 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 9669	. . . . . . . . . 10 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) e. CC )
155	12	rpcnd 11343	. . . . . . . . . 10 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. CC )
156	147	recnd 9669	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) e. CC )
157	156, 23, 23, 25	divsubdird 10422	. . . . . . . . . . . . 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 9986	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) - ( log ` x ) ) e. CC )
159	158, 23, 25	divrecd 10386	. . . . . . . . . . . . 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 10381	. . . . . . . . . . . . . 14 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / ( log ` x ) ) = 1 )
161	160	oveq2d 6317	. . . . . . . . . . . . 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 2472	. . . . . . . . . . . 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 4507	. . . . . . . . . . 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 10047	. . . . . . . . . . . 12 |- ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) - ( log ` x ) ) e. RR )
165		vmadivsum 24306	. . . . . . . . . . . . . 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 13614	. . . . . . . . . . . 12 |- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) - ( log ` x ) ) ) e. O(1) )
168	164, 44, 167, 55	o1mul2 13675	. . . . . . . . . . 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 2510	. . . . . . . . . 10 |- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) - 1 ) ) e. O(1) )
170	154, 155, 169	o1dif 13680	. . . . . . . . 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 235	. . . . . . . 8 |- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) ) e. O(1) )
172	148, 171	o1lo1d 13590	. . . . . . 7 |- ( T. -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( (Λ ` n ) / n ) / ( log ` x ) ) ) e. <_O(1) )
173	95, 69	resubcld 10047	. . . . . . . . . 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 9671	. . . . . . . . 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 13787	. . . . . . . 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 11369	. . . . . . 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 9658	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
178		vmage0 24034	. . . . . . . . . . . . . 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 11378	. . . . . . . . . . . 12 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( (Λ ` n ) / n ) )
181	68	rpred 11341	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR )
182	91	mulid2d 9661	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. n ) = n )
183		fznnfl 12088	. . . . . . . . . . . . . . . . . 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 628	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n <_ x )
186	182, 185	eqbrtrd 4441	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. n ) <_ x )
187	10	adantr 466	. . . . . . . . . . . . . . . 16 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR )
188	177, 187, 67	lemuldivd 11387	. . . . . . . . . . . . . . 15 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 x. n ) <_ x <-> 1 <_ ( x / n ) ) )
189	186, 188	mpbid 213	. . . . . . . . . . . . . 14 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ ( x / n ) )
190		harmonicubnd 23921	. . . . . . . . . . . . . 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 665	. . . . . . . . . . . . 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 10212	. . . . . . . . . . . . 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 235	. . . . . . . . . . . 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 10547	. . . . . . . . . . 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 9660	. . . . . . . . . . 11 |- ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( (Λ ` n ) / n ) x. 1 ) = ( (Λ ` n ) / n ) )
196	194, 195	breqtrd 4445	. . . . . . . . . 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 13846	. . . . . . . . 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 11396	. . . . . . . 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 721	. . . . . . 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 13702	. . . . . 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 9644	. . . . . . 7 |- ( T. -> 0 e. RR )
202		harmoniclbnd 23920	. . . . . . . . . . . 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 10203	. . . . . . . . . . 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 235	. . . . . . . . . 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 10190	. . . . . . . . 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 13842	. . . . . . . 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 11378	. . . . . . 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 13589	. . . . . 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 235	. . . . 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 2510	. . . 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 13680	. . 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 213	. 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 1446	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 187   /\ wa 370   /\ w3a 982   = wceq 1437   T. wtru 1438   e. wcel 1868   =/= wne 2618   {crab 2779   C_ wss 3436   class class class wbr 4420   |-> cmpt 4479   dom cdm 4849   -->wf 5593   ` cfv 5597  (class class class)co 6301   Fincfn 7573   CCcc 9537   RRcr 9538   0cc0 9539   1c1 9540   + caddc 9542   x. cmul 9544   +oocpnf 9672   < clt 9675   <_ cle 9676   - cmin 9860   / cdiv 10269   NNcn 10609   2c2 10659   RR+crp 11302   (,)cioo 11635   ...cfz 11784   |_cfl 12025   ^cexp 12271   abscabs 13285   ~~> r crli 13536   O(1)co1 13537   <_O(1)clo1 13538   sum_csu 13739   _eceu 14102   || cdvds 14292   logclog 23490  Λcvma 24004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-inf2 8148  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616  ax-pre-sup 9617  ax-addf 9618  ax-mulf 9619

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-int 4253  df-iun 4298  df-iin 4299  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-se 4809  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-isom 5606  df-riota 6263  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-of 6541  df-om 6703  df-1st 6803  df-2nd 6804  df-supp 6922  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-1o 7186  df-2o 7187  df-oadd 7190  df-er 7367  df-map 7478  df-pm 7479  df-ixp 7527  df-en 7574  df-dom 7575  df-sdom 7576  df-fin 7577  df-fsupp 7886  df-fi 7927  df-sup 7958  df-inf 7959  df-oi 8027  df-card 8374  df-cda 8598  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-div 10270  df-nn 10610  df-2 10668  df-3 10669  df-4 10670  df-5 10671  df-6 10672  df-7 10673  df-8 10674  df-9 10675  df-10 10676  df-n0 10870  df-z 10938  df-dec 11052  df-uz 11160  df-q 11265  df-rp 11303  df-xneg 11409  df-xadd 11410  df-xmul 11411  df-ioo 11639  df-ioc 11640  df-ico 11641  df-icc 11642  df-fz 11785  df-fzo 11916  df-fl 12027  df-mod 12096  df-seq 12213  df-exp 12272  df-fac 12459  df-bc 12487  df-hash 12515  df-shft 13118  df-cj 13150  df-re 13151  df-im 13152  df-sqrt 13286  df-abs 13287  df-limsup 13513  df-clim 13539  df-rlim 13540  df-o1 13541  df-lo1 13542  df-sum 13740  df-ef 14108  df-e 14109  df-sin 14110  df-cos 14111  df-pi 14113  df-dvds 14293  df-gcd 14456  df-prm 14610  df-pc 14774  df-struct 15110  df-ndx 15111  df-slot 15112  df-base 15113  df-sets 15114  df-ress 15115  df-plusg 15190  df-mulr 15191  df-starv 15192  df-sca 15193  df-vsca 15194  df-ip 15195  df-tset 15196  df-ple 15197  df-ds 15199  df-unif 15200  df-hom 15201  df-cco 15202  df-rest 15308  df-topn 15309  df-0g 15327  df-gsum 15328  df-topgen 15329  df-pt 15330  df-prds 15333  df-xrs 15387  df-qtop 15393  df-imas 15394  df-xps 15397  df-mre 15479  df-mrc 15480  df-acs 15482  df-mgm 16475  df-sgrp 16514  df-mnd 16524  df-submnd 16570  df-mulg 16663  df-cntz 16958  df-cmn 17419  df-psmet 18949  df-xmet 18950  df-met 18951  df-bl 18952  df-mopn 18953  df-fbas 18954  df-fg 18955  df-cnfld 18958  df-top 19907  df-bases 19908  df-topon 19909  df-topsp 19910  df-cld 20020  df-ntr 20021  df-cls 20022  df-nei 20100  df-lp 20138  df-perf 20139  df-cn 20229  df-cnp 20230  df-haus 20317  df-cmp 20388  df-tx 20563  df-hmeo 20756  df-fil 20847  df-fm 20939  df-flim 20940  df-flf 20941  df-xms 21321  df-ms 21322  df-tms 21323  df-cncf 21896  df-limc 22807  df-dv 22808  df-log 23492  df-cxp 23493  df-em 23904  df-cht 24009  df-vma 24010  df-chp 24011  df-ppi 24012

This theorem is referenced by:  vmalogdivsum  24363  2vmadivsumlem  24364  selberg4lem1  24384