Database
BASIC REAL AND COMPLEX FUNCTIONS
Basic trigonometry
More miscellaneous converging sequences
divsqrsum
Metamath Proof Explorer
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 ⁡ ⇝ ℝ