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	⊢ 𝐹 = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑛 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) )
Assertion	divsqrsum	⊢ 𝐹 ∈ dom ⇝𝑟

Proof

Step	Hyp	Ref	Expression
1		divsqrtsum.2	⊢ 𝐹 = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑛 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) )
2	1	divsqrtsumlem	⊢ ( 𝐹 : ℝ+ ⟶ ℝ ∧ 𝐹 ∈ dom ⇝𝑟 ∧ ( ( 𝐹 ⇝𝑟 1 ∧ 1 ∈ ℝ+ ) → ( abs ‘ ( ( 𝐹 ‘ 1 ) − 1 ) ) ≤ ( 1 / ( √ ‘ 1 ) ) ) )
3	2	simp2i	⊢ 𝐹 ∈ dom ⇝𝑟