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