Metamath Proof Explorer

Theorem divsqrtsumlem

Description: Lemma for divsqrsum and divsqrtsum2 . (Contributed by Mario Carneiro, 18-May-2016)

Ref Expression
Hypothesis divsqrtsum.2 
|- F = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` n ) ) - ( 2 x. ( sqrt ` x ) ) ) )
Assertion divsqrtsumlem 
|- ( F : RR+ --> RR /\ F e. dom ~~>r /\ ( ( F ~~>r L /\ A e. RR+ ) -> ( abs ` ( ( F ` A ) - L ) ) <_ ( 1 / ( sqrt ` A ) ) ) )

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 ioorp 
 |-  ( 0 (,) +oo ) = RR+
3 2 eqcomi 
 |-  RR+ = ( 0 (,) +oo )
4 nnuz 
 |-  NN = ( ZZ>= ` 1 )
5 1zzd 
 |-  ( T. -> 1 e. ZZ )
6 0red 
 |-  ( T. -> 0 e. RR )
7 1re 
 |-  1 e. RR
8 0nn0 
 |-  0 e. NN0
9 7 8 nn0addge2i 
 |-  1 <_ ( 0 + 1 )
10 9 a1i 
 |-  ( T. -> 1 <_ ( 0 + 1 ) )
11 2re 
 |-  2 e. RR
12 rpsqrtcl 
 |-  ( x e. RR+ -> ( sqrt ` x ) e. RR+ )
13 12 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( sqrt ` x ) e. RR+ )
14 13 rpred 
 |-  ( ( T. /\ x e. RR+ ) -> ( sqrt ` x ) e. RR )
15 remulcl 
 |-  ( ( 2 e. RR /\ ( sqrt ` x ) e. RR ) -> ( 2 x. ( sqrt ` x ) ) e. RR )
16 11 14 15 sylancr 
 |-  ( ( T. /\ x e. RR+ ) -> ( 2 x. ( sqrt ` x ) ) e. RR )
17 13 rprecred 
 |-  ( ( T. /\ x e. RR+ ) -> ( 1 / ( sqrt ` x ) ) e. RR )
18 nnrp 
 |-  ( x e. NN -> x e. RR+ )
19 18 17 sylan2 
 |-  ( ( T. /\ x e. NN ) -> ( 1 / ( sqrt ` x ) ) e. RR )
20 reelprrecn 
 |-  RR e. { RR , CC }
21 20 a1i 
 |-  ( T. -> RR e. { RR , CC } )
22 13 rpcnd 
 |-  ( ( T. /\ x e. RR+ ) -> ( sqrt ` x ) e. CC )
23 2rp 
 |-  2 e. RR+
24 rpmulcl 
 |-  ( ( 2 e. RR+ /\ ( sqrt ` x ) e. RR+ ) -> ( 2 x. ( sqrt ` x ) ) e. RR+ )
25 23 13 24 sylancr 
 |-  ( ( T. /\ x e. RR+ ) -> ( 2 x. ( sqrt ` x ) ) e. RR+ )
26 25 rpreccld 
 |-  ( ( T. /\ x e. RR+ ) -> ( 1 / ( 2 x. ( sqrt ` x ) ) ) e. RR+ )
27 dvsqrt 
 |-  ( RR _D ( x e. RR+ |-> ( sqrt ` x ) ) ) = ( x e. RR+ |-> ( 1 / ( 2 x. ( sqrt ` x ) ) ) )
28 27 a1i 
 |-  ( T. -> ( RR _D ( x e. RR+ |-> ( sqrt ` x ) ) ) = ( x e. RR+ |-> ( 1 / ( 2 x. ( sqrt ` x ) ) ) ) )
29 2cnd 
 |-  ( T. -> 2 e. CC )
30 21 22 26 28 29 dvmptcmul 
 |-  ( T. -> ( RR _D ( x e. RR+ |-> ( 2 x. ( sqrt ` x ) ) ) ) = ( x e. RR+ |-> ( 2 x. ( 1 / ( 2 x. ( sqrt ` x ) ) ) ) ) )
31 2cnd 
 |-  ( ( T. /\ x e. RR+ ) -> 2 e. CC )
32 1cnd 
 |-  ( ( T. /\ x e. RR+ ) -> 1 e. CC )
33 25 rpcnne0d 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( 2 x. ( sqrt ` x ) ) e. CC /\ ( 2 x. ( sqrt ` x ) ) =/= 0 ) )
34 divass 
 |-  ( ( 2 e. CC /\ 1 e. CC /\ ( ( 2 x. ( sqrt ` x ) ) e. CC /\ ( 2 x. ( sqrt ` x ) ) =/= 0 ) ) -> ( ( 2 x. 1 ) / ( 2 x. ( sqrt ` x ) ) ) = ( 2 x. ( 1 / ( 2 x. ( sqrt ` x ) ) ) ) )
35 31 32 33 34 syl3anc 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( 2 x. 1 ) / ( 2 x. ( sqrt ` x ) ) ) = ( 2 x. ( 1 / ( 2 x. ( sqrt ` x ) ) ) ) )
36 13 rpcnne0d 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( sqrt ` x ) e. CC /\ ( sqrt ` x ) =/= 0 ) )
37 rpcnne0 
 |-  ( 2 e. RR+ -> ( 2 e. CC /\ 2 =/= 0 ) )
38 23 37 mp1i 
 |-  ( ( T. /\ x e. RR+ ) -> ( 2 e. CC /\ 2 =/= 0 ) )
39 divcan5 
 |-  ( ( 1 e. CC /\ ( ( sqrt ` x ) e. CC /\ ( sqrt ` x ) =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( 2 x. 1 ) / ( 2 x. ( sqrt ` x ) ) ) = ( 1 / ( sqrt ` x ) ) )
40 32 36 38 39 syl3anc 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( 2 x. 1 ) / ( 2 x. ( sqrt ` x ) ) ) = ( 1 / ( sqrt ` x ) ) )
41 35 40 eqtr3d 
 |-  ( ( T. /\ x e. RR+ ) -> ( 2 x. ( 1 / ( 2 x. ( sqrt ` x ) ) ) ) = ( 1 / ( sqrt ` x ) ) )
42 41 mpteq2dva 
 |-  ( T. -> ( x e. RR+ |-> ( 2 x. ( 1 / ( 2 x. ( sqrt ` x ) ) ) ) ) = ( x e. RR+ |-> ( 1 / ( sqrt ` x ) ) ) )
43 30 42 eqtrd 
 |-  ( T. -> ( RR _D ( x e. RR+ |-> ( 2 x. ( sqrt ` x ) ) ) ) = ( x e. RR+ |-> ( 1 / ( sqrt ` x ) ) ) )
44 fveq2 
 |-  ( x = n -> ( sqrt ` x ) = ( sqrt ` n ) )
45 44 oveq2d 
 |-  ( x = n -> ( 1 / ( sqrt ` x ) ) = ( 1 / ( sqrt ` n ) ) )
46 simp3r 
 |-  ( ( T. /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 0 <_ x /\ x <_ n ) ) -> x <_ n )
47 simp2l 
 |-  ( ( T. /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 0 <_ x /\ x <_ n ) ) -> x e. RR+ )
48 47 rprege0d 
 |-  ( ( T. /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 0 <_ x /\ x <_ n ) ) -> ( x e. RR /\ 0 <_ x ) )
49 simp2r 
 |-  ( ( T. /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 0 <_ x /\ x <_ n ) ) -> n e. RR+ )
50 49 rprege0d 
 |-  ( ( T. /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 0 <_ x /\ x <_ n ) ) -> ( n e. RR /\ 0 <_ n ) )
51 sqrtle 
 |-  ( ( ( x e. RR /\ 0 <_ x ) /\ ( n e. RR /\ 0 <_ n ) ) -> ( x <_ n <-> ( sqrt ` x ) <_ ( sqrt ` n ) ) )
52 48 50 51 syl2anc 
 |-  ( ( T. /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 0 <_ x /\ x <_ n ) ) -> ( x <_ n <-> ( sqrt ` x ) <_ ( sqrt ` n ) ) )
53 46 52 mpbid 
 |-  ( ( T. /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 0 <_ x /\ x <_ n ) ) -> ( sqrt ` x ) <_ ( sqrt ` n ) )
54 47 rpsqrtcld 
 |-  ( ( T. /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 0 <_ x /\ x <_ n ) ) -> ( sqrt ` x ) e. RR+ )
55 49 rpsqrtcld 
 |-  ( ( T. /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 0 <_ x /\ x <_ n ) ) -> ( sqrt ` n ) e. RR+ )
56 54 55 lerecd 
 |-  ( ( T. /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 0 <_ x /\ x <_ n ) ) -> ( ( sqrt ` x ) <_ ( sqrt ` n ) <-> ( 1 / ( sqrt ` n ) ) <_ ( 1 / ( sqrt ` x ) ) ) )
57 53 56 mpbid 
 |-  ( ( T. /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 0 <_ x /\ x <_ n ) ) -> ( 1 / ( sqrt ` n ) ) <_ ( 1 / ( sqrt ` x ) ) )
58 sqrtlim 
 |-  ( x e. RR+ |-> ( 1 / ( sqrt ` x ) ) ) ~~>r 0
59 58 a1i 
 |-  ( T. -> ( x e. RR+ |-> ( 1 / ( sqrt ` x ) ) ) ~~>r 0 )
60 fveq2 
 |-  ( x = A -> ( sqrt ` x ) = ( sqrt ` A ) )
61 60 oveq2d 
 |-  ( x = A -> ( 1 / ( sqrt ` x ) ) = ( 1 / ( sqrt ` A ) ) )
62 3 4 5 6 10 6 16 17 19 43 45 57 1 59 61 dvfsumrlim3 
 |-  ( T. -> ( F : RR+ --> RR /\ F e. dom ~~>r /\ ( ( F ~~>r L /\ A e. RR+ /\ 0 <_ A ) -> ( abs ` ( ( F ` A ) - L ) ) <_ ( 1 / ( sqrt ` A ) ) ) ) )
63 62 simp1d 
 |-  ( T. -> F : RR+ --> RR )
64 63 mptru 
 |-  F : RR+ --> RR
65 62 simp2d 
 |-  ( T. -> F e. dom ~~>r )
66 65 mptru 
 |-  F e. dom ~~>r
67 rpge0 
 |-  ( A e. RR+ -> 0 <_ A )
68 67 adantl 
 |-  ( ( F ~~>r L /\ A e. RR+ ) -> 0 <_ A )
69 62 simp3d 
 |-  ( T. -> ( ( F ~~>r L /\ A e. RR+ /\ 0 <_ A ) -> ( abs ` ( ( F ` A ) - L ) ) <_ ( 1 / ( sqrt ` A ) ) ) )
70 69 mptru 
 |-  ( ( F ~~>r L /\ A e. RR+ /\ 0 <_ A ) -> ( abs ` ( ( F ` A ) - L ) ) <_ ( 1 / ( sqrt ` A ) ) )
71 68 70 mpd3an3 
 |-  ( ( F ~~>r L /\ A e. RR+ ) -> ( abs ` ( ( F ` A ) - L ) ) <_ ( 1 / ( sqrt ` A ) ) )
72 64 66 71 3pm3.2i 
 |-  ( F : RR+ --> RR /\ F e. dom ~~>r /\ ( ( F ~~>r L /\ A e. RR+ ) -> ( abs ` ( ( F ` A ) - L ) ) <_ ( 1 / ( sqrt ` A ) ) ) )