This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ 𝐹 = ( 𝑥 ∈ ℝ⁺ ↦ ( Σ 𝑛 ∈ ( 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 ⇝_𝑟