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

Metamath Proof Explorer

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 ffvelcdmi ⊢ ( 𝑦 ∈ ℝ+ → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
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) )