Theorem divsqrtsum2

Description: A bound on the distance of the sum sum_ n <_ x ( 1 / sqrt n ) from its asymptotic value 2 sqrt x + L . (Contributed by Mario Carneiro, 18-May-2016)

	Ref	Expression
Hypotheses	divsqrtsum.2	$$⊢F=\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\left(\frac{1}{\sqrt{n}}\right)-2\sqrt{x}\right)$$
	divsqrsum2.1	$$⊢\phi \to F\underset{ℝ}{⇝}L$$
Assertion	divsqrtsum2	$$⊢\left(\phi \wedge A\in {ℝ}^{+}\right)\to \left|F\left(A\right)-L\right|\le \frac{1}{\sqrt{A}}$$

Proof

Step	Hyp	Ref	Expression
1		divsqrtsum.2	$$⊢F=\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\left(\frac{1}{\sqrt{n}}\right)-2\sqrt{x}\right)$$
2		divsqrsum2.1	$$⊢\phi \to F\underset{ℝ}{⇝}L$$
3	1	divsqrtsumlem	$$⊢\left(F:{ℝ}^{+}⟶ℝ\wedge F\in \mathrm{dom}\underset{ℝ}{⇝}\wedge \left(\left(F\underset{ℝ}{⇝}L\wedge A\in {ℝ}^{+}\right)\to \left|F\left(A\right)-L\right|\le \frac{1}{\sqrt{A}}\right)\right)$$
4	3	simp3i	$$⊢\left(F\underset{ℝ}{⇝}L\wedge A\in {ℝ}^{+}\right)\to \left|F\left(A\right)-L\right|\le \frac{1}{\sqrt{A}}$$
5	2 4	sylan	$$⊢\left(\phi \wedge A\in {ℝ}^{+}\right)\to \left|F\left(A\right)-L\right|\le \frac{1}{\sqrt{A}}$$