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=\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\left(\frac{1}{\sqrt{n}}\right)-2\sqrt{x}\right)$$
Assertion	divsqrsumf	$$⊢F:{ℝ}^{+}⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		divsqrtsum.2	$$⊢F=\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\left(\frac{1}{\sqrt{n}}\right)-2\sqrt{x}\right)$$
2	1	divsqrtsumlem	$$⊢\left(F:{ℝ}^{+}⟶ℝ\wedge F\in \mathrm{dom}\underset{ℝ}{⇝}\wedge \left(\left(F\underset{ℝ}{⇝}1\wedge 1\in {ℝ}^{+}\right)\to \left|F\left(1\right)-1\right|\le \frac{1}{\sqrt{1}}\right)\right)$$
3	2	simp1i	$$⊢F:{ℝ}^{+}⟶ℝ$$