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

Metamath Proof Explorer

Theorem divsqrsumf

Description: The function F used in divsqrsum is a real function. (Contributed by Mario Carneiro, 12-May-2016)

		Ref	Expression
	Hypothesis	divsqrtsum.2	$⊢ F = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{1}{\sqrt{n}}) - 2 \sqrt{x})$
	Assertion	divsqrsumf	$⊢ F : ℝ^{+} ⟶ ℝ$

Step	Hyp	Ref	Expression
1		divsqrtsum.2	$⊢ F = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{1}{\sqrt{n}}) - 2 \sqrt{x})$
2	1	divsqrtsumlem	$⊢ (F : ℝ^{+} ⟶ ℝ \land F \in dom \underset{ℝ}{⇝} \land ((F \underset{ℝ}{⇝} 1 \land 1 \in ℝ^{+}) \to \|F (1) - 1\| \leq \frac{1}{\sqrt{1}}))$
3	2	simp1i	$⊢ F : ℝ^{+} ⟶ ℝ$