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	⊢ 𝐹 = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑛 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) )
	divsqrsum2.1	⊢ ( 𝜑 → 𝐹 ⇝𝑟 𝐿 )
Assertion	divsqrtsumo1	⊢ ( 𝜑 → ( 𝑦 ∈ ℝ+ ↦ ( ( ( 𝐹 ‘ 𝑦 ) − 𝐿 ) · ( √ ‘ 𝑦 ) ) ) ∈ 𝑂(1) )

Proof

Step	Hyp	Ref	Expression
1		divsqrtsum.2	⊢ 𝐹 = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑛 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) )
2		divsqrsum2.1	⊢ ( 𝜑 → 𝐹 ⇝𝑟 𝐿 )
3		rpssre	⊢ ℝ+ ⊆ ℝ
4	3	a1i	⊢ ( 𝜑 → ℝ+ ⊆ ℝ )
5	1	divsqrsumf	⊢ 𝐹 : ℝ+ ⟶ ℝ
6	5	ffvelrni	⊢ ( 𝑦 ∈ ℝ+ → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
7		rpsup	⊢ sup ( ℝ+ , ℝ* , < ) = +∞
8	7	a1i	⊢ ( 𝜑 → sup ( ℝ+ , ℝ* , < ) = +∞ )
9	5	a1i	⊢ ( 𝜑 → 𝐹 : ℝ+ ⟶ ℝ )
10	9	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ℝ+ ↦ ( 𝐹 ‘ 𝑦 ) ) )
11	10 2	eqbrtrrd	⊢ ( 𝜑 → ( 𝑦 ∈ ℝ+ ↦ ( 𝐹 ‘ 𝑦 ) ) ⇝𝑟 𝐿 )
12	6	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
13	8 11 12	rlimrecl	⊢ ( 𝜑 → 𝐿 ∈ ℝ )
14		resubcl	⊢ ( ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑦 ) − 𝐿 ) ∈ ℝ )
15	6 13 14	syl2anr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝐹 ‘ 𝑦 ) − 𝐿 ) ∈ ℝ )
16	15	recnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝐹 ‘ 𝑦 ) − 𝐿 ) ∈ ℂ )
17		rpsqrtcl	⊢ ( 𝑦 ∈ ℝ+ → ( √ ‘ 𝑦 ) ∈ ℝ+ )
18	17	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( √ ‘ 𝑦 ) ∈ ℝ+ )
19	18	rpcnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( √ ‘ 𝑦 ) ∈ ℂ )
20	16 19	mulcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ( ( 𝐹 ‘ 𝑦 ) − 𝐿 ) · ( √ ‘ 𝑦 ) ) ∈ ℂ )
21		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
22	16 19	absmuld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑦 ) − 𝐿 ) · ( √ ‘ 𝑦 ) ) ) = ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − 𝐿 ) ) · ( abs ‘ ( √ ‘ 𝑦 ) ) ) )
23	18	rprege0d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ( √ ‘ 𝑦 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑦 ) ) )
24		absid	⊢ ( ( ( √ ‘ 𝑦 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑦 ) ) → ( abs ‘ ( √ ‘ 𝑦 ) ) = ( √ ‘ 𝑦 ) )
25	23 24	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( abs ‘ ( √ ‘ 𝑦 ) ) = ( √ ‘ 𝑦 ) )
26	25	oveq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − 𝐿 ) ) · ( abs ‘ ( √ ‘ 𝑦 ) ) ) = ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − 𝐿 ) ) · ( √ ‘ 𝑦 ) ) )
27	22 26	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑦 ) − 𝐿 ) · ( √ ‘ 𝑦 ) ) ) = ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − 𝐿 ) ) · ( √ ‘ 𝑦 ) ) )
28	1 2	divsqrtsum2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − 𝐿 ) ) ≤ ( 1 / ( √ ‘ 𝑦 ) ) )
29	16	abscld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − 𝐿 ) ) ∈ ℝ )
30		1red	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 1 ∈ ℝ )
31	29 30 18	lemuldivd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − 𝐿 ) ) · ( √ ‘ 𝑦 ) ) ≤ 1 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − 𝐿 ) ) ≤ ( 1 / ( √ ‘ 𝑦 ) ) ) )
32	28 31	mpbird	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − 𝐿 ) ) · ( √ ‘ 𝑦 ) ) ≤ 1 )
33	27 32	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑦 ) − 𝐿 ) · ( √ ‘ 𝑦 ) ) ) ≤ 1 )
34	33	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ+ ∧ 1 ≤ 𝑦 ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑦 ) − 𝐿 ) · ( √ ‘ 𝑦 ) ) ) ≤ 1 )
35	4 20 21 21 34	elo1d	⊢ ( 𝜑 → ( 𝑦 ∈ ℝ+ ↦ ( ( ( 𝐹 ‘ 𝑦 ) − 𝐿 ) · ( √ ‘ 𝑦 ) ) ) ∈ 𝑂(1) )