Theorem divsqrtsumo1

Description: The sum sum_ n <_ x ( 1 / sqrt n ) has the asymptotic expansion 2 sqrt x + L + O ( 1 / sqrt x ) , for some L . (Contributed by Mario Carneiro, 10-May-2016)

	Ref	Expression
Hypotheses	divsqrtsum.2	$$⊢F=\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\left(\frac{1}{\sqrt{n}}\right)-2\sqrt{x}\right)$$
	divsqrsum2.1	$$⊢\phi \to F\underset{ℝ}{⇝}L$$
Assertion	divsqrtsumo1	$$⊢\phi \to \left(y\in {ℝ}^{+}⟼\left(F\left(y\right)-L\right)\sqrt{y}\right)\in 𝑂\left(1\right)$$

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		divsqrsum2.1	$$⊢\phi \to F\underset{ℝ}{⇝}L$$
3		rpssre	$$⊢{ℝ}^{+}\subseteq ℝ$$
4	3	a1i	$$⊢\phi \to {ℝ}^{+}\subseteq ℝ$$
5	1	divsqrsumf	$$⊢F:{ℝ}^{+}⟶ℝ$$
6	5	ffvelrni	$$⊢y\in {ℝ}^{+}\to F\left(y\right)\in ℝ$$
7		rpsup	$$⊢sup\left({ℝ}^{+},{ℝ}^{*},<\right)=\mathrm{+\infty }$$
8	7	a1i	$$⊢\phi \to sup\left({ℝ}^{+},{ℝ}^{*},<\right)=\mathrm{+\infty }$$
9	5	a1i	$$⊢\phi \to F:{ℝ}^{+}⟶ℝ$$
10	9	feqmptd	$$⊢\phi \to F=\left(y\in {ℝ}^{+}⟼F\left(y\right)\right)$$
11	10 2	eqbrtrrd	$$⊢\phi \to \left(y\in {ℝ}^{+}⟼F\left(y\right)\right)\underset{ℝ}{⇝}L$$
12	6	adantl	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to F\left(y\right)\in ℝ$$
13	8 11 12	rlimrecl	$$⊢\phi \to L\in ℝ$$
14		resubcl	$$⊢\left(F\left(y\right)\in ℝ\wedge L\in ℝ\right)\to F\left(y\right)-L\in ℝ$$
15	6 13 14	syl2anr	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to F\left(y\right)-L\in ℝ$$
16	15	recnd	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to F\left(y\right)-L\in ℂ$$
17		rpsqrtcl	$$⊢y\in {ℝ}^{+}\to \sqrt{y}\in {ℝ}^{+}$$
18	17	adantl	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \sqrt{y}\in {ℝ}^{+}$$
19	18	rpcnd	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \sqrt{y}\in ℂ$$
20	16 19	mulcld	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \left(F\left(y\right)-L\right)\sqrt{y}\in ℂ$$
21		1red	$$⊢\phi \to 1\in ℝ$$
22	16 19	absmuld	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \left|\left(F\left(y\right)-L\right)\sqrt{y}\right|=\left|F\left(y\right)-L\right|\left|\sqrt{y}\right|$$
23	18	rprege0d	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \left(\sqrt{y}\in ℝ\wedge 0\le \sqrt{y}\right)$$
24		absid	$$⊢\left(\sqrt{y}\in ℝ\wedge 0\le \sqrt{y}\right)\to \left|\sqrt{y}\right|=\sqrt{y}$$
25	23 24	syl	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \left|\sqrt{y}\right|=\sqrt{y}$$
26	25	oveq2d	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \left|F\left(y\right)-L\right|\left|\sqrt{y}\right|=\left|F\left(y\right)-L\right|\sqrt{y}$$
27	22 26	eqtrd	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \left|\left(F\left(y\right)-L\right)\sqrt{y}\right|=\left|F\left(y\right)-L\right|\sqrt{y}$$
28	1 2	divsqrtsum2	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \left|F\left(y\right)-L\right|\le \frac{1}{\sqrt{y}}$$
29	16	abscld	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \left|F\left(y\right)-L\right|\in ℝ$$
30		1red	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to 1\in ℝ$$
31	29 30 18	lemuldivd	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \left(\left|F\left(y\right)-L\right|\sqrt{y}\le 1\leftrightarrow \left|F\left(y\right)-L\right|\le \frac{1}{\sqrt{y}}\right)$$
32	28 31	mpbird	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \left|F\left(y\right)-L\right|\sqrt{y}\le 1$$
33	27 32	eqbrtrd	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \left|\left(F\left(y\right)-L\right)\sqrt{y}\right|\le 1$$
34	33	adantrr	$$⊢\left(\phi \wedge \left(y\in {ℝ}^{+}\wedge 1\le y\right)\right)\to \left|\left(F\left(y\right)-L\right)\sqrt{y}\right|\le 1$$
35	4 20 21 21 34	elo1d	$$⊢\phi \to \left(y\in {ℝ}^{+}⟼\left(F\left(y\right)-L\right)\sqrt{y}\right)\in 𝑂\left(1\right)$$