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
|- F = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` n ) ) - ( 2 x. ( sqrt ` x ) ) ) )
divsqrsum2.1
|- ( ph -> F ~~>r L )
Assertion divsqrtsumo1
|- ( ph -> ( y e. RR+ |-> ( ( ( F ` y ) - L ) x. ( sqrt ` y ) ) ) e. O(1) )

Proof

Step Hyp Ref Expression
1 divsqrtsum.2
 |-  F = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` n ) ) - ( 2 x. ( sqrt ` x ) ) ) )
2 divsqrsum2.1
 |-  ( ph -> F ~~>r L )
3 rpssre
 |-  RR+ C_ RR
4 3 a1i
 |-  ( ph -> RR+ C_ RR )
5 1 divsqrsumf
 |-  F : RR+ --> RR
6 5 ffvelrni
 |-  ( y e. RR+ -> ( F ` y ) e. RR )
7 rpsup
 |-  sup ( RR+ , RR* , < ) = +oo
8 7 a1i
 |-  ( ph -> sup ( RR+ , RR* , < ) = +oo )
9 5 a1i
 |-  ( ph -> F : RR+ --> RR )
10 9 feqmptd
 |-  ( ph -> F = ( y e. RR+ |-> ( F ` y ) ) )
11 10 2 eqbrtrrd
 |-  ( ph -> ( y e. RR+ |-> ( F ` y ) ) ~~>r L )
12 6 adantl
 |-  ( ( ph /\ y e. RR+ ) -> ( F ` y ) e. RR )
13 8 11 12 rlimrecl
 |-  ( ph -> L e. RR )
14 resubcl
 |-  ( ( ( F ` y ) e. RR /\ L e. RR ) -> ( ( F ` y ) - L ) e. RR )
15 6 13 14 syl2anr
 |-  ( ( ph /\ y e. RR+ ) -> ( ( F ` y ) - L ) e. RR )
16 15 recnd
 |-  ( ( ph /\ y e. RR+ ) -> ( ( F ` y ) - L ) e. CC )
17 rpsqrtcl
 |-  ( y e. RR+ -> ( sqrt ` y ) e. RR+ )
18 17 adantl
 |-  ( ( ph /\ y e. RR+ ) -> ( sqrt ` y ) e. RR+ )
19 18 rpcnd
 |-  ( ( ph /\ y e. RR+ ) -> ( sqrt ` y ) e. CC )
20 16 19 mulcld
 |-  ( ( ph /\ y e. RR+ ) -> ( ( ( F ` y ) - L ) x. ( sqrt ` y ) ) e. CC )
21 1red
 |-  ( ph -> 1 e. RR )
22 16 19 absmuld
 |-  ( ( ph /\ y e. RR+ ) -> ( abs ` ( ( ( F ` y ) - L ) x. ( sqrt ` y ) ) ) = ( ( abs ` ( ( F ` y ) - L ) ) x. ( abs ` ( sqrt ` y ) ) ) )
23 18 rprege0d
 |-  ( ( ph /\ y e. RR+ ) -> ( ( sqrt ` y ) e. RR /\ 0 <_ ( sqrt ` y ) ) )
24 absid
 |-  ( ( ( sqrt ` y ) e. RR /\ 0 <_ ( sqrt ` y ) ) -> ( abs ` ( sqrt ` y ) ) = ( sqrt ` y ) )
25 23 24 syl
 |-  ( ( ph /\ y e. RR+ ) -> ( abs ` ( sqrt ` y ) ) = ( sqrt ` y ) )
26 25 oveq2d
 |-  ( ( ph /\ y e. RR+ ) -> ( ( abs ` ( ( F ` y ) - L ) ) x. ( abs ` ( sqrt ` y ) ) ) = ( ( abs ` ( ( F ` y ) - L ) ) x. ( sqrt ` y ) ) )
27 22 26 eqtrd
 |-  ( ( ph /\ y e. RR+ ) -> ( abs ` ( ( ( F ` y ) - L ) x. ( sqrt ` y ) ) ) = ( ( abs ` ( ( F ` y ) - L ) ) x. ( sqrt ` y ) ) )
28 1 2 divsqrtsum2
 |-  ( ( ph /\ y e. RR+ ) -> ( abs ` ( ( F ` y ) - L ) ) <_ ( 1 / ( sqrt ` y ) ) )
29 16 abscld
 |-  ( ( ph /\ y e. RR+ ) -> ( abs ` ( ( F ` y ) - L ) ) e. RR )
30 1red
 |-  ( ( ph /\ y e. RR+ ) -> 1 e. RR )
31 29 30 18 lemuldivd
 |-  ( ( ph /\ y e. RR+ ) -> ( ( ( abs ` ( ( F ` y ) - L ) ) x. ( sqrt ` y ) ) <_ 1 <-> ( abs ` ( ( F ` y ) - L ) ) <_ ( 1 / ( sqrt ` y ) ) ) )
32 28 31 mpbird
 |-  ( ( ph /\ y e. RR+ ) -> ( ( abs ` ( ( F ` y ) - L ) ) x. ( sqrt ` y ) ) <_ 1 )
33 27 32 eqbrtrd
 |-  ( ( ph /\ y e. RR+ ) -> ( abs ` ( ( ( F ` y ) - L ) x. ( sqrt ` y ) ) ) <_ 1 )
34 33 adantrr
 |-  ( ( ph /\ ( y e. RR+ /\ 1 <_ y ) ) -> ( abs ` ( ( ( F ` y ) - L ) x. ( sqrt ` y ) ) ) <_ 1 )
35 4 20 21 21 34 elo1d
 |-  ( ph -> ( y e. RR+ |-> ( ( ( F ` y ) - L ) x. ( sqrt ` y ) ) ) e. O(1) )