logdivsum

Description: Asymptotic analysis of sum_ n <_ x , log n / n = ( log x ) ^ 2 / 2 + L + O ( log x / x ) . (Contributed by Mario Carneiro, 18-May-2016)

		Ref	Expression
	Hypothesis	logdivsum.1	⊢ 𝐹 = ( 𝑦 ∈ ℝ⁺ ↦ ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑖 ) / 𝑖 ) − ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) )
	Assertion	logdivsum	⊢ ( 𝐹 : ℝ⁺ ⟶ ℝ ∧ 𝐹 ∈ dom ⇝_𝑟 ∧ ( ( 𝐹 ⇝_𝑟 𝐿 ∧ 𝐴 ∈ ℝ⁺ ∧ e ≤ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − 𝐿 ) ) ≤ ( ( log ‘ 𝐴 ) / 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		logdivsum.1	⊢ 𝐹 = ( 𝑦 ∈ ℝ⁺ ↦ ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑖 ) / 𝑖 ) − ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) )
2		ioorp	⊢ ( 0 (,) +∞ ) = ℝ⁺
3	2	eqcomi	⊢ ℝ⁺ = ( 0 (,) +∞ )
4		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
5		1zzd	⊢ ( ⊤ → 1 ∈ ℤ )
6		ere	⊢ e ∈ ℝ
7	6	a1i	⊢ ( ⊤ → e ∈ ℝ )
8		0re	⊢ 0 ∈ ℝ
9		epos	⊢ 0 < e
10	8 6 9	ltleii	⊢ 0 ≤ e
11	10	a1i	⊢ ( ⊤ → 0 ≤ e )
12		1re	⊢ 1 ∈ ℝ
13		addge02	⊢ ( ( 1 ∈ ℝ ∧ e ∈ ℝ ) → ( 0 ≤ e ↔ 1 ≤ ( e + 1 ) ) )
14	12 6 13	mp2an	⊢ ( 0 ≤ e ↔ 1 ≤ ( e + 1 ) )
15	11 14	sylib	⊢ ( ⊤ → 1 ≤ ( e + 1 ) )
16	8	a1i	⊢ ( ⊤ → 0 ∈ ℝ )
17		relogcl	⊢ ( 𝑦 ∈ ℝ⁺ → ( log ‘ 𝑦 ) ∈ ℝ )
18	17	adantl	⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ⁺ ) → ( log ‘ 𝑦 ) ∈ ℝ )
19	18	resqcld	⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ⁺ ) → ( ( log ‘ 𝑦 ) ↑ 2 ) ∈ ℝ )
20	19	rehalfcld	⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ⁺ ) → ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ∈ ℝ )
21		rerpdivcl	⊢ ( ( ( log ‘ 𝑦 ) ∈ ℝ ∧ 𝑦 ∈ ℝ⁺ ) → ( ( log ‘ 𝑦 ) / 𝑦 ) ∈ ℝ )
22	17 21	mpancom	⊢ ( 𝑦 ∈ ℝ⁺ → ( ( log ‘ 𝑦 ) / 𝑦 ) ∈ ℝ )
23	22	adantl	⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ⁺ ) → ( ( log ‘ 𝑦 ) / 𝑦 ) ∈ ℝ )
24		nnrp	⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ⁺ )
25	24 23	sylan2	⊢ ( ( ⊤ ∧ 𝑦 ∈ ℕ ) → ( ( log ‘ 𝑦 ) / 𝑦 ) ∈ ℝ )
26		reelprrecn	⊢ ℝ ∈ { ℝ , ℂ }
27	26	a1i	⊢ ( ⊤ → ℝ ∈ { ℝ , ℂ } )
28		cnelprrecn	⊢ ℂ ∈ { ℝ , ℂ }
29	28	a1i	⊢ ( ⊤ → ℂ ∈ { ℝ , ℂ } )
30	18	recnd	⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ⁺ ) → ( log ‘ 𝑦 ) ∈ ℂ )
31		ovexd	⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ⁺ ) → ( 1 / 𝑦 ) ∈ V )
32		sqcl	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ↑ 2 ) ∈ ℂ )
33	32	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ↑ 2 ) ∈ ℂ )
34	33	halfcld	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( 𝑥 ↑ 2 ) / 2 ) ∈ ℂ )
35		simpr	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
36		relogf1o	⊢ ( log ↾ ℝ⁺ ) : ℝ⁺ –1-1-onto→ ℝ
37		f1of	⊢ ( ( log ↾ ℝ⁺ ) : ℝ⁺ –1-1-onto→ ℝ → ( log ↾ ℝ⁺ ) : ℝ⁺ ⟶ ℝ )
38	36 37	mp1i	⊢ ( ⊤ → ( log ↾ ℝ⁺ ) : ℝ⁺ ⟶ ℝ )
39	38	feqmptd	⊢ ( ⊤ → ( log ↾ ℝ⁺ ) = ( 𝑦 ∈ ℝ⁺ ↦ ( ( log ↾ ℝ⁺ ) ‘ 𝑦 ) ) )
40		fvres	⊢ ( 𝑦 ∈ ℝ⁺ → ( ( log ↾ ℝ⁺ ) ‘ 𝑦 ) = ( log ‘ 𝑦 ) )
41	40	mpteq2ia	⊢ ( 𝑦 ∈ ℝ⁺ ↦ ( ( log ↾ ℝ⁺ ) ‘ 𝑦 ) ) = ( 𝑦 ∈ ℝ⁺ ↦ ( log ‘ 𝑦 ) )
42	39 41	eqtrdi	⊢ ( ⊤ → ( log ↾ ℝ⁺ ) = ( 𝑦 ∈ ℝ⁺ ↦ ( log ‘ 𝑦 ) ) )
43	42	oveq2d	⊢ ( ⊤ → ( ℝ D ( log ↾ ℝ⁺ ) ) = ( ℝ D ( 𝑦 ∈ ℝ⁺ ↦ ( log ‘ 𝑦 ) ) ) )
44		dvrelog	⊢ ( ℝ D ( log ↾ ℝ⁺ ) ) = ( 𝑦 ∈ ℝ⁺ ↦ ( 1 / 𝑦 ) )
45	43 44	eqtr3di	⊢ ( ⊤ → ( ℝ D ( 𝑦 ∈ ℝ⁺ ↦ ( log ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ℝ⁺ ↦ ( 1 / 𝑦 ) ) )
46		ovexd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 2 · 𝑥 ) ∈ V )
47		2nn	⊢ 2 ∈ ℕ
48		dvexp	⊢ ( 2 ∈ ℕ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 2 · ( 𝑥 ↑ ( 2 − 1 ) ) ) ) )
49	47 48	mp1i	⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 2 · ( 𝑥 ↑ ( 2 − 1 ) ) ) ) )
50		2m1e1	⊢ ( 2 − 1 ) = 1
51	50	oveq2i	⊢ ( 𝑥 ↑ ( 2 − 1 ) ) = ( 𝑥 ↑ 1 )
52		exp1	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ↑ 1 ) = 𝑥 )
53	52	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ↑ 1 ) = 𝑥 )
54	51 53	syl5eq	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ↑ ( 2 − 1 ) ) = 𝑥 )
55	54	oveq2d	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 2 · ( 𝑥 ↑ ( 2 − 1 ) ) ) = ( 2 · 𝑥 ) )
56	55	mpteq2dva	⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( 2 · ( 𝑥 ↑ ( 2 − 1 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 2 · 𝑥 ) ) )
57	49 56	eqtrd	⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 2 · 𝑥 ) ) )
58		2cnd	⊢ ( ⊤ → 2 ∈ ℂ )
59		2ne0	⊢ 2 ≠ 0
60	59	a1i	⊢ ( ⊤ → 2 ≠ 0 )
61	29 33 46 57 58 60	dvmptdivc	⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( 𝑥 ↑ 2 ) / 2 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 2 · 𝑥 ) / 2 ) ) )
62		2cn	⊢ 2 ∈ ℂ
63		divcan3	⊢ ( ( 𝑥 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( 2 · 𝑥 ) / 2 ) = 𝑥 )
64	62 59 63	mp3an23	⊢ ( 𝑥 ∈ ℂ → ( ( 2 · 𝑥 ) / 2 ) = 𝑥 )
65	64	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( 2 · 𝑥 ) / 2 ) = 𝑥 )
66	65	mpteq2dva	⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( ( 2 · 𝑥 ) / 2 ) ) = ( 𝑥 ∈ ℂ ↦ 𝑥 ) )
67	61 66	eqtrd	⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( 𝑥 ↑ 2 ) / 2 ) ) ) = ( 𝑥 ∈ ℂ ↦ 𝑥 ) )
68		oveq1	⊢ ( 𝑥 = ( log ‘ 𝑦 ) → ( 𝑥 ↑ 2 ) = ( ( log ‘ 𝑦 ) ↑ 2 ) )
69	68	oveq1d	⊢ ( 𝑥 = ( log ‘ 𝑦 ) → ( ( 𝑥 ↑ 2 ) / 2 ) = ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) )
70		id	⊢ ( 𝑥 = ( log ‘ 𝑦 ) → 𝑥 = ( log ‘ 𝑦 ) )
71	27 29 30 31 34 35 45 67 69 70	dvmptco	⊢ ( ⊤ → ( ℝ D ( 𝑦 ∈ ℝ⁺ ↦ ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) ) = ( 𝑦 ∈ ℝ⁺ ↦ ( ( log ‘ 𝑦 ) · ( 1 / 𝑦 ) ) ) )
72		rpcn	⊢ ( 𝑦 ∈ ℝ⁺ → 𝑦 ∈ ℂ )
73	72	adantl	⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ⁺ ) → 𝑦 ∈ ℂ )
74		rpne0	⊢ ( 𝑦 ∈ ℝ⁺ → 𝑦 ≠ 0 )
75	74	adantl	⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ⁺ ) → 𝑦 ≠ 0 )
76	30 73 75	divrecd	⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ⁺ ) → ( ( log ‘ 𝑦 ) / 𝑦 ) = ( ( log ‘ 𝑦 ) · ( 1 / 𝑦 ) ) )
77	76	mpteq2dva	⊢ ( ⊤ → ( 𝑦 ∈ ℝ⁺ ↦ ( ( log ‘ 𝑦 ) / 𝑦 ) ) = ( 𝑦 ∈ ℝ⁺ ↦ ( ( log ‘ 𝑦 ) · ( 1 / 𝑦 ) ) ) )
78	71 77	eqtr4d	⊢ ( ⊤ → ( ℝ D ( 𝑦 ∈ ℝ⁺ ↦ ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) ) = ( 𝑦 ∈ ℝ⁺ ↦ ( ( log ‘ 𝑦 ) / 𝑦 ) ) )
79		fveq2	⊢ ( 𝑦 = 𝑖 → ( log ‘ 𝑦 ) = ( log ‘ 𝑖 ) )
80		id	⊢ ( 𝑦 = 𝑖 → 𝑦 = 𝑖 )
81	79 80	oveq12d	⊢ ( 𝑦 = 𝑖 → ( ( log ‘ 𝑦 ) / 𝑦 ) = ( ( log ‘ 𝑖 ) / 𝑖 ) )
82		simp3r	⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ⁺ ∧ 𝑖 ∈ ℝ⁺ ) ∧ ( e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖 ) ) → 𝑦 ≤ 𝑖 )
83		simp2l	⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ⁺ ∧ 𝑖 ∈ ℝ⁺ ) ∧ ( e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖 ) ) → 𝑦 ∈ ℝ⁺ )
84	83	rpred	⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ⁺ ∧ 𝑖 ∈ ℝ⁺ ) ∧ ( e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖 ) ) → 𝑦 ∈ ℝ )
85		simp3l	⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ⁺ ∧ 𝑖 ∈ ℝ⁺ ) ∧ ( e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖 ) ) → e ≤ 𝑦 )
86		simp2r	⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ⁺ ∧ 𝑖 ∈ ℝ⁺ ) ∧ ( e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖 ) ) → 𝑖 ∈ ℝ⁺ )
87	86	rpred	⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ⁺ ∧ 𝑖 ∈ ℝ⁺ ) ∧ ( e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖 ) ) → 𝑖 ∈ ℝ )
88	6	a1i	⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ⁺ ∧ 𝑖 ∈ ℝ⁺ ) ∧ ( e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖 ) ) → e ∈ ℝ )
89	88 84 87 85 82	letrd	⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ⁺ ∧ 𝑖 ∈ ℝ⁺ ) ∧ ( e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖 ) ) → e ≤ 𝑖 )
90		logdivle	⊢ ( ( ( 𝑦 ∈ ℝ ∧ e ≤ 𝑦 ) ∧ ( 𝑖 ∈ ℝ ∧ e ≤ 𝑖 ) ) → ( 𝑦 ≤ 𝑖 ↔ ( ( log ‘ 𝑖 ) / 𝑖 ) ≤ ( ( log ‘ 𝑦 ) / 𝑦 ) ) )
91	84 85 87 89 90	syl22anc	⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ⁺ ∧ 𝑖 ∈ ℝ⁺ ) ∧ ( e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖 ) ) → ( 𝑦 ≤ 𝑖 ↔ ( ( log ‘ 𝑖 ) / 𝑖 ) ≤ ( ( log ‘ 𝑦 ) / 𝑦 ) ) )
92	82 91	mpbid	⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ⁺ ∧ 𝑖 ∈ ℝ⁺ ) ∧ ( e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖 ) ) → ( ( log ‘ 𝑖 ) / 𝑖 ) ≤ ( ( log ‘ 𝑦 ) / 𝑦 ) )
93	72	cxp1d	⊢ ( 𝑦 ∈ ℝ⁺ → ( 𝑦 ↑_𝑐 1 ) = 𝑦 )
94	93	oveq2d	⊢ ( 𝑦 ∈ ℝ⁺ → ( ( log ‘ 𝑦 ) / ( 𝑦 ↑_𝑐 1 ) ) = ( ( log ‘ 𝑦 ) / 𝑦 ) )
95	94	mpteq2ia	⊢ ( 𝑦 ∈ ℝ⁺ ↦ ( ( log ‘ 𝑦 ) / ( 𝑦 ↑_𝑐 1 ) ) ) = ( 𝑦 ∈ ℝ⁺ ↦ ( ( log ‘ 𝑦 ) / 𝑦 ) )
96		1rp	⊢ 1 ∈ ℝ⁺
97		cxploglim	⊢ ( 1 ∈ ℝ⁺ → ( 𝑦 ∈ ℝ⁺ ↦ ( ( log ‘ 𝑦 ) / ( 𝑦 ↑_𝑐 1 ) ) ) ⇝_𝑟 0 )
98	96 97	mp1i	⊢ ( ⊤ → ( 𝑦 ∈ ℝ⁺ ↦ ( ( log ‘ 𝑦 ) / ( 𝑦 ↑_𝑐 1 ) ) ) ⇝_𝑟 0 )
99	95 98	eqbrtrrid	⊢ ( ⊤ → ( 𝑦 ∈ ℝ⁺ ↦ ( ( log ‘ 𝑦 ) / 𝑦 ) ) ⇝_𝑟 0 )
100		fveq2	⊢ ( 𝑦 = 𝐴 → ( log ‘ 𝑦 ) = ( log ‘ 𝐴 ) )
101		id	⊢ ( 𝑦 = 𝐴 → 𝑦 = 𝐴 )
102	100 101	oveq12d	⊢ ( 𝑦 = 𝐴 → ( ( log ‘ 𝑦 ) / 𝑦 ) = ( ( log ‘ 𝐴 ) / 𝐴 ) )
103	3 4 5 7 15 16 20 23 25 78 81 92 1 99 102	dvfsumrlim3	⊢ ( ⊤ → ( 𝐹 : ℝ⁺ ⟶ ℝ ∧ 𝐹 ∈ dom ⇝_𝑟 ∧ ( ( 𝐹 ⇝_𝑟 𝐿 ∧ 𝐴 ∈ ℝ⁺ ∧ e ≤ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − 𝐿 ) ) ≤ ( ( log ‘ 𝐴 ) / 𝐴 ) ) ) )
104	103	mptru	⊢ ( 𝐹 : ℝ⁺ ⟶ ℝ ∧ 𝐹 ∈ dom ⇝_𝑟 ∧ ( ( 𝐹 ⇝_𝑟 𝐿 ∧ 𝐴 ∈ ℝ⁺ ∧ e ≤ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − 𝐿 ) ) ≤ ( ( log ‘ 𝐴 ) / 𝐴 ) ) )

Metamath Proof Explorer

Theorem logdivsum

Proof