harmonicbnd4

Description: The asymptotic behavior of sum_ m <_ A , 1 / m = log A + gamma + O ( 1 / A ) . (Contributed by Mario Carneiro, 14-May-2016)

		Ref	Expression
	Assertion	harmonicbnd4	$⊢ A \in ℝ^{+} \to \|\sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - (\log A + γ)\| \leq \frac{1}{A}$

Proof

Step	Hyp	Ref	Expression
1		fzfid	$⊢ A \in ℝ^{+} \to (1 \dots ⌊A⌋) \in Fin$
2		elfznn	$⊢ m \in (1 \dots ⌊A⌋) \to m \in ℕ$
3	2	adantl	$⊢ (A \in ℝ^{+} \land m \in (1 \dots ⌊A⌋)) \to m \in ℕ$
4	3	nnrecred	$⊢ (A \in ℝ^{+} \land m \in (1 \dots ⌊A⌋)) \to \frac{1}{m} \in ℝ$
5	1 4	fsumrecl	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) \in ℝ$
6	5	recnd	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) \in ℂ$
7		relogcl	$⊢ A \in ℝ^{+} \to \log A \in ℝ$
8	7	recnd	$⊢ A \in ℝ^{+} \to \log A \in ℂ$
9		emre	$⊢ γ \in ℝ$
10	9	a1i	$⊢ A \in ℝ^{+} \to γ \in ℝ$
11	10	recnd	$⊢ A \in ℝ^{+} \to γ \in ℂ$
12	6 8 11	subsub4d	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log A - γ = \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - (\log A + γ)$
13	12	fveq2d	$⊢ A \in ℝ^{+} \to \|\sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log A - γ\| = \|\sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - (\log A + γ)\|$
14		rpreccl	$⊢ A \in ℝ^{+} \to \frac{1}{A} \in ℝ^{+}$
15	14	rpred	$⊢ A \in ℝ^{+} \to \frac{1}{A} \in ℝ$
16		resubcl	$⊢ (γ \in ℝ \land \frac{1}{A} \in ℝ) \to γ - (\frac{1}{A}) \in ℝ$
17	9 15 16	sylancr	$⊢ A \in ℝ^{+} \to γ - (\frac{1}{A}) \in ℝ$
18		rprege0	$⊢ A \in ℝ^{+} \to (A \in ℝ \land 0 \leq A)$
19		flge0nn0	$⊢ (A \in ℝ \land 0 \leq A) \to ⌊A⌋ \in ℕ_{0}$
20	18 19	syl	$⊢ A \in ℝ^{+} \to ⌊A⌋ \in ℕ_{0}$
21		nn0p1nn	$⊢ ⌊A⌋ \in ℕ_{0} \to ⌊A⌋ + 1 \in ℕ$
22	20 21	syl	$⊢ A \in ℝ^{+} \to ⌊A⌋ + 1 \in ℕ$
23	22	nnrpd	$⊢ A \in ℝ^{+} \to ⌊A⌋ + 1 \in ℝ^{+}$
24		relogcl	$⊢ ⌊A⌋ + 1 \in ℝ^{+} \to \log (⌊A⌋ + 1) \in ℝ$
25	23 24	syl	$⊢ A \in ℝ^{+} \to \log (⌊A⌋ + 1) \in ℝ$
26	5 25	resubcld	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log (⌊A⌋ + 1) \in ℝ$
27	5 7	resubcld	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log A \in ℝ$
28	22	nnrecred	$⊢ A \in ℝ^{+} \to \frac{1}{⌊A⌋ + 1} \in ℝ$
29		fzfid	$⊢ A \in ℝ^{+} \to (1 \dots ⌊A⌋ + 1) \in Fin$
30		elfznn	$⊢ m \in (1 \dots ⌊A⌋ + 1) \to m \in ℕ$
31	30	adantl	$⊢ (A \in ℝ^{+} \land m \in (1 \dots ⌊A⌋ + 1)) \to m \in ℕ$
32	31	nnrecred	$⊢ (A \in ℝ^{+} \land m \in (1 \dots ⌊A⌋ + 1)) \to \frac{1}{m} \in ℝ$
33	29 32	fsumrecl	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋ + 1} (\frac{1}{m}) \in ℝ$
34	33 25	resubcld	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋ + 1} (\frac{1}{m}) - \log (⌊A⌋ + 1) \in ℝ$
35		harmonicbnd	$⊢ ⌊A⌋ + 1 \in ℕ \to \sum_{m = 1}^{⌊A⌋ + 1} (\frac{1}{m}) - \log (⌊A⌋ + 1) \in [γ, 1]$
36	22 35	syl	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋ + 1} (\frac{1}{m}) - \log (⌊A⌋ + 1) \in [γ, 1]$
37		1re	$⊢ 1 \in ℝ$
38	9 37	elicc2i	$⊢ \sum_{m = 1}^{⌊A⌋ + 1} (\frac{1}{m}) - \log (⌊A⌋ + 1) \in [γ, 1] \leftrightarrow (\sum_{m = 1}^{⌊A⌋ + 1} (\frac{1}{m}) - \log (⌊A⌋ + 1) \in ℝ \land γ \leq \sum_{m = 1}^{⌊A⌋ + 1} (\frac{1}{m}) - \log (⌊A⌋ + 1) \land \sum_{m = 1}^{⌊A⌋ + 1} (\frac{1}{m}) - \log (⌊A⌋ + 1) \leq 1)$
39	38	simp2bi	$⊢ \sum_{m = 1}^{⌊A⌋ + 1} (\frac{1}{m}) - \log (⌊A⌋ + 1) \in [γ, 1] \to γ \leq \sum_{m = 1}^{⌊A⌋ + 1} (\frac{1}{m}) - \log (⌊A⌋ + 1)$
40	36 39	syl	$⊢ A \in ℝ^{+} \to γ \leq \sum_{m = 1}^{⌊A⌋ + 1} (\frac{1}{m}) - \log (⌊A⌋ + 1)$
41		rpre	$⊢ A \in ℝ^{+} \to A \in ℝ$
42		fllep1	$⊢ A \in ℝ \to A \leq ⌊A⌋ + 1$
43	41 42	syl	$⊢ A \in ℝ^{+} \to A \leq ⌊A⌋ + 1$
44		rpregt0	$⊢ A \in ℝ^{+} \to (A \in ℝ \land 0 < A)$
45	22	nnred	$⊢ A \in ℝ^{+} \to ⌊A⌋ + 1 \in ℝ$
46	22	nngt0d	$⊢ A \in ℝ^{+} \to 0 < ⌊A⌋ + 1$
47		lerec	$⊢ ((A \in ℝ \land 0 < A) \land (⌊A⌋ + 1 \in ℝ \land 0 < ⌊A⌋ + 1)) \to (A \leq ⌊A⌋ + 1 \leftrightarrow \frac{1}{⌊A⌋ + 1} \leq \frac{1}{A})$
48	44 45 46 47	syl12anc	$⊢ A \in ℝ^{+} \to (A \leq ⌊A⌋ + 1 \leftrightarrow \frac{1}{⌊A⌋ + 1} \leq \frac{1}{A})$
49	43 48	mpbid	$⊢ A \in ℝ^{+} \to \frac{1}{⌊A⌋ + 1} \leq \frac{1}{A}$
50	10 28 34 15 40 49	le2subd	$⊢ A \in ℝ^{+} \to γ - (\frac{1}{A}) \leq \sum_{m = 1}^{⌊A⌋ + 1} (\frac{1}{m}) - \log (⌊A⌋ + 1) - (\frac{1}{⌊A⌋ + 1})$
51	33	recnd	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋ + 1} (\frac{1}{m}) \in ℂ$
52	25	recnd	$⊢ A \in ℝ^{+} \to \log (⌊A⌋ + 1) \in ℂ$
53	28	recnd	$⊢ A \in ℝ^{+} \to \frac{1}{⌊A⌋ + 1} \in ℂ$
54	51 52 53	sub32d	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋ + 1} (\frac{1}{m}) - \log (⌊A⌋ + 1) - (\frac{1}{⌊A⌋ + 1}) = \sum_{m = 1}^{⌊A⌋ + 1} (\frac{1}{m}) - (\frac{1}{⌊A⌋ + 1}) - \log (⌊A⌋ + 1)$
55		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
56	22 55	eleqtrdi	$⊢ A \in ℝ^{+} \to ⌊A⌋ + 1 \in ℤ_{\geq 1}$
57	32	recnd	$⊢ (A \in ℝ^{+} \land m \in (1 \dots ⌊A⌋ + 1)) \to \frac{1}{m} \in ℂ$
58		oveq2	$⊢ m = ⌊A⌋ + 1 \to \frac{1}{m} = \frac{1}{⌊A⌋ + 1}$
59	56 57 58	fsumm1	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋ + 1} (\frac{1}{m}) = \sum_{m = 1}^{⌊A⌋ + 1 - 1} (\frac{1}{m}) + (\frac{1}{⌊A⌋ + 1})$
60	20	nn0cnd	$⊢ A \in ℝ^{+} \to ⌊A⌋ \in ℂ$
61		ax-1cn	$⊢ 1 \in ℂ$
62		pncan	$⊢ (⌊A⌋ \in ℂ \land 1 \in ℂ) \to ⌊A⌋ + 1 - 1 = ⌊A⌋$
63	60 61 62	sylancl	$⊢ A \in ℝ^{+} \to ⌊A⌋ + 1 - 1 = ⌊A⌋$
64	63	oveq2d	$⊢ A \in ℝ^{+} \to (1 \dots ⌊A⌋ + 1 - 1) = (1 \dots ⌊A⌋)$
65	64	sumeq1d	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋ + 1 - 1} (\frac{1}{m}) = \sum_{m = 1}^{⌊A⌋} (\frac{1}{m})$
66	65	oveq1d	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋ + 1 - 1} (\frac{1}{m}) + (\frac{1}{⌊A⌋ + 1}) = \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) + (\frac{1}{⌊A⌋ + 1})$
67	59 66	eqtrd	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋ + 1} (\frac{1}{m}) = \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) + (\frac{1}{⌊A⌋ + 1})$
68	6 53 67	mvrraddd	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋ + 1} (\frac{1}{m}) - (\frac{1}{⌊A⌋ + 1}) = \sum_{m = 1}^{⌊A⌋} (\frac{1}{m})$
69	68	oveq1d	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋ + 1} (\frac{1}{m}) - (\frac{1}{⌊A⌋ + 1}) - \log (⌊A⌋ + 1) = \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log (⌊A⌋ + 1)$
70	54 69	eqtrd	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋ + 1} (\frac{1}{m}) - \log (⌊A⌋ + 1) - (\frac{1}{⌊A⌋ + 1}) = \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log (⌊A⌋ + 1)$
71	50 70	breqtrd	$⊢ A \in ℝ^{+} \to γ - (\frac{1}{A}) \leq \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log (⌊A⌋ + 1)$
72		logleb	$⊢ (A \in ℝ^{+} \land ⌊A⌋ + 1 \in ℝ^{+}) \to (A \leq ⌊A⌋ + 1 \leftrightarrow \log A \leq \log (⌊A⌋ + 1))$
73	23 72	mpdan	$⊢ A \in ℝ^{+} \to (A \leq ⌊A⌋ + 1 \leftrightarrow \log A \leq \log (⌊A⌋ + 1))$
74	43 73	mpbid	$⊢ A \in ℝ^{+} \to \log A \leq \log (⌊A⌋ + 1)$
75	7 25 5 74	lesub2dd	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log (⌊A⌋ + 1) \leq \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log A$
76	17 26 27 71 75	letrd	$⊢ A \in ℝ^{+} \to γ - (\frac{1}{A}) \leq \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log A$
77	27 15	resubcld	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log A - (\frac{1}{A}) \in ℝ$
78	15	recnd	$⊢ A \in ℝ^{+} \to \frac{1}{A} \in ℂ$
79	6 8 78	subsub4d	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log A - (\frac{1}{A}) = \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - (\log A + (\frac{1}{A}))$
80	7 15	readdcld	$⊢ A \in ℝ^{+} \to \log A + (\frac{1}{A}) \in ℝ$
81		id	$⊢ A \in ℝ^{+} \to A \in ℝ^{+}$
82	23 81	relogdivd	$⊢ A \in ℝ^{+} \to \log (\frac{⌊A⌋ + 1}{A}) = \log (⌊A⌋ + 1) - \log A$
83		rerpdivcl	$⊢ (⌊A⌋ + 1 \in ℝ \land A \in ℝ^{+}) \to \frac{⌊A⌋ + 1}{A} \in ℝ$
84	45 83	mpancom	$⊢ A \in ℝ^{+} \to \frac{⌊A⌋ + 1}{A} \in ℝ$
85	37	a1i	$⊢ A \in ℝ^{+} \to 1 \in ℝ$
86	85 15	readdcld	$⊢ A \in ℝ^{+} \to 1 + (\frac{1}{A}) \in ℝ$
87	15	reefcld	$⊢ A \in ℝ^{+} \to e^{\frac{1}{A}} \in ℝ$
88	61	a1i	$⊢ A \in ℝ^{+} \to 1 \in ℂ$
89		rpcnne0	$⊢ A \in ℝ^{+} \to (A \in ℂ \land A \neq 0)$
90		divdir	$⊢ (⌊A⌋ \in ℂ \land 1 \in ℂ \land (A \in ℂ \land A \neq 0)) \to \frac{⌊A⌋ + 1}{A} = (\frac{⌊A⌋}{A}) + (\frac{1}{A})$
91	60 88 89 90	syl3anc	$⊢ A \in ℝ^{+} \to \frac{⌊A⌋ + 1}{A} = (\frac{⌊A⌋}{A}) + (\frac{1}{A})$
92		reflcl	$⊢ A \in ℝ \to ⌊A⌋ \in ℝ$
93	41 92	syl	$⊢ A \in ℝ^{+} \to ⌊A⌋ \in ℝ$
94		rerpdivcl	$⊢ (⌊A⌋ \in ℝ \land A \in ℝ^{+}) \to \frac{⌊A⌋}{A} \in ℝ$
95	93 94	mpancom	$⊢ A \in ℝ^{+} \to \frac{⌊A⌋}{A} \in ℝ$
96		flle	$⊢ A \in ℝ \to ⌊A⌋ \leq A$
97	41 96	syl	$⊢ A \in ℝ^{+} \to ⌊A⌋ \leq A$
98		rpcn	$⊢ A \in ℝ^{+} \to A \in ℂ$
99	98	mulid1d	$⊢ A \in ℝ^{+} \to A \cdot 1 = A$
100	97 99	breqtrrd	$⊢ A \in ℝ^{+} \to ⌊A⌋ \leq A \cdot 1$
101		ledivmul	$⊢ (⌊A⌋ \in ℝ \land 1 \in ℝ \land (A \in ℝ \land 0 < A)) \to (\frac{⌊A⌋}{A} \leq 1 \leftrightarrow ⌊A⌋ \leq A \cdot 1)$
102	93 85 44 101	syl3anc	$⊢ A \in ℝ^{+} \to (\frac{⌊A⌋}{A} \leq 1 \leftrightarrow ⌊A⌋ \leq A \cdot 1)$
103	100 102	mpbird	$⊢ A \in ℝ^{+} \to \frac{⌊A⌋}{A} \leq 1$
104	95 85 15 103	leadd1dd	$⊢ A \in ℝ^{+} \to (\frac{⌊A⌋}{A}) + (\frac{1}{A}) \leq 1 + (\frac{1}{A})$
105	91 104	eqbrtrd	$⊢ A \in ℝ^{+} \to \frac{⌊A⌋ + 1}{A} \leq 1 + (\frac{1}{A})$
106		efgt1p	$⊢ \frac{1}{A} \in ℝ^{+} \to 1 + (\frac{1}{A}) < e^{\frac{1}{A}}$
107	14 106	syl	$⊢ A \in ℝ^{+} \to 1 + (\frac{1}{A}) < e^{\frac{1}{A}}$
108	86 87 107	ltled	$⊢ A \in ℝ^{+} \to 1 + (\frac{1}{A}) \leq e^{\frac{1}{A}}$
109	84 86 87 105 108	letrd	$⊢ A \in ℝ^{+} \to \frac{⌊A⌋ + 1}{A} \leq e^{\frac{1}{A}}$
110		rpdivcl	$⊢ (⌊A⌋ + 1 \in ℝ^{+} \land A \in ℝ^{+}) \to \frac{⌊A⌋ + 1}{A} \in ℝ^{+}$
111	23 110	mpancom	$⊢ A \in ℝ^{+} \to \frac{⌊A⌋ + 1}{A} \in ℝ^{+}$
112	15	rpefcld	$⊢ A \in ℝ^{+} \to e^{\frac{1}{A}} \in ℝ^{+}$
113	111 112	logled	$⊢ A \in ℝ^{+} \to (\frac{⌊A⌋ + 1}{A} \leq e^{\frac{1}{A}} \leftrightarrow \log (\frac{⌊A⌋ + 1}{A}) \leq \log e^{\frac{1}{A}})$
114	109 113	mpbid	$⊢ A \in ℝ^{+} \to \log (\frac{⌊A⌋ + 1}{A}) \leq \log e^{\frac{1}{A}}$
115	15	relogefd	$⊢ A \in ℝ^{+} \to \log e^{\frac{1}{A}} = \frac{1}{A}$
116	114 115	breqtrd	$⊢ A \in ℝ^{+} \to \log (\frac{⌊A⌋ + 1}{A}) \leq \frac{1}{A}$
117	82 116	eqbrtrrd	$⊢ A \in ℝ^{+} \to \log (⌊A⌋ + 1) - \log A \leq \frac{1}{A}$
118	25 7 15	lesubadd2d	$⊢ A \in ℝ^{+} \to (\log (⌊A⌋ + 1) - \log A \leq \frac{1}{A} \leftrightarrow \log (⌊A⌋ + 1) \leq \log A + (\frac{1}{A}))$
119	117 118	mpbid	$⊢ A \in ℝ^{+} \to \log (⌊A⌋ + 1) \leq \log A + (\frac{1}{A})$
120	25 80 5 119	lesub2dd	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - (\log A + (\frac{1}{A})) \leq \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log (⌊A⌋ + 1)$
121	79 120	eqbrtrd	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log A - (\frac{1}{A}) \leq \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log (⌊A⌋ + 1)$
122		harmonicbnd3	$⊢ ⌊A⌋ \in ℕ_{0} \to \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log (⌊A⌋ + 1) \in [0, γ]$
123	20 122	syl	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log (⌊A⌋ + 1) \in [0, γ]$
124		0re	$⊢ 0 \in ℝ$
125	124 9	elicc2i	$⊢ \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log (⌊A⌋ + 1) \in [0, γ] \leftrightarrow (\sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log (⌊A⌋ + 1) \in ℝ \land 0 \leq \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log (⌊A⌋ + 1) \land \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log (⌊A⌋ + 1) \leq γ)$
126	125	simp3bi	$⊢ \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log (⌊A⌋ + 1) \in [0, γ] \to \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log (⌊A⌋ + 1) \leq γ$
127	123 126	syl	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log (⌊A⌋ + 1) \leq γ$
128	77 26 10 121 127	letrd	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log A - (\frac{1}{A}) \leq γ$
129	27 15 10	lesubaddd	$⊢ A \in ℝ^{+} \to (\sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log A - (\frac{1}{A}) \leq γ \leftrightarrow \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log A \leq γ + (\frac{1}{A}))$
130	128 129	mpbid	$⊢ A \in ℝ^{+} \to \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log A \leq γ + (\frac{1}{A})$
131	27 10 15	absdifled	$⊢ A \in ℝ^{+} \to (\|\sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log A - γ\| \leq \frac{1}{A} \leftrightarrow (γ - (\frac{1}{A}) \leq \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log A \land \sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log A \leq γ + (\frac{1}{A})))$
132	76 130 131	mpbir2and	$⊢ A \in ℝ^{+} \to \|\sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - \log A - γ\| \leq \frac{1}{A}$
133	13 132	eqbrtrrd	$⊢ A \in ℝ^{+} \to \|\sum_{m = 1}^{⌊A⌋} (\frac{1}{m}) - (\log A + γ)\| \leq \frac{1}{A}$

Metamath Proof Explorer

Theorem harmonicbnd4

Proof