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) )