Metamath Proof Explorer


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 = x + n = 1 x 1 n 2 x
Assertion divsqrsum F dom

Proof

Step Hyp Ref Expression
1 divsqrtsum.2 F = x + n = 1 x 1 n 2 x
2 1 divsqrtsumlem F : + F dom F 1 1 + F 1 1 1 1
3 2 simp2i F dom