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