Theorem divsqrsum

Description: The sum sum_ n <_ x ( 1 / sqrt n ) is asymptotic to 2 sqrt x + L with a finite limit L . (In fact, this limit is zeta ( 1 / 2 ) ~-u 1 . 4 6 ... .) (Contributed by Mario Carneiro, 9-May-2016)

	Ref	Expression
Hypothesis	divsqrtsum.2	$$⊢F=\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\left(\frac{1}{\sqrt{n}}\right)-2\sqrt{x}\right)$$
Assertion	divsqrsum	$$⊢F\in \mathrm{dom}\underset{ℝ}{⇝}$$

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	1	divsqrtsumlem	$$⊢\left(F:{ℝ}^{+}⟶ℝ\wedge F\in \mathrm{dom}\underset{ℝ}{⇝}\wedge \left(\left(F\underset{ℝ}{⇝}1\wedge 1\in {ℝ}^{+}\right)\to \left|F\left(1\right)-1\right|\le \frac{1}{\sqrt{1}}\right)\right)$$
3	2	simp2i	$$⊢F\in \mathrm{dom}\underset{ℝ}{⇝}$$