Metamath Proof Explorer

Theorem lmnn

Description: A condition that implies convergence. (Contributed by NM, 8-Jun-2007) (Revised by Mario Carneiro, 1-May-2014)

Ref Expression
Hypotheses lmnn.2 
|- J = ( MetOpen ` D )
lmnn.3 
|- ( ph -> D e. ( *Met ` X ) )
lmnn.4 
|- ( ph -> P e. X )
lmnn.5 
|- ( ph -> F : NN --> X )
lmnn.6 
|- ( ( ph /\ k e. NN ) -> ( ( F ` k ) D P ) < ( 1 / k ) )
Assertion lmnn 
|- ( ph -> F ( ~~>t ` J ) P )

Proof

Step Hyp Ref Expression
1 lmnn.2 
 |-  J = ( MetOpen ` D )
2 lmnn.3 
 |-  ( ph -> D e. ( *Met ` X ) )
3 lmnn.4 
 |-  ( ph -> P e. X )
4 lmnn.5 
 |-  ( ph -> F : NN --> X )
5 lmnn.6 
 |-  ( ( ph /\ k e. NN ) -> ( ( F ` k ) D P ) < ( 1 / k ) )
6 rpreccl 
 |-  ( x e. RR+ -> ( 1 / x ) e. RR+ )
7 6 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 / x ) e. RR+ )
8 7 rpred 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 / x ) e. RR )
9 7 rpge0d 
 |-  ( ( ph /\ x e. RR+ ) -> 0 <_ ( 1 / x ) )
10 flge0nn0 
 |-  ( ( ( 1 / x ) e. RR /\ 0 <_ ( 1 / x ) ) -> ( |_ ` ( 1 / x ) ) e. NN0 )
11 8 9 10 syl2anc 
 |-  ( ( ph /\ x e. RR+ ) -> ( |_ ` ( 1 / x ) ) e. NN0 )
12 nn0p1nn 
 |-  ( ( |_ ` ( 1 / x ) ) e. NN0 -> ( ( |_ ` ( 1 / x ) ) + 1 ) e. NN )
13 11 12 syl 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( |_ ` ( 1 / x ) ) + 1 ) e. NN )
14 2 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) ) -> D e. ( *Met ` X ) )
15 4 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) ) -> F : NN --> X )
16 eluznn 
 |-  ( ( ( ( |_ ` ( 1 / x ) ) + 1 ) e. NN /\ k e. ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) ) -> k e. NN )
17 13 16 sylan 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) ) -> k e. NN )
18 15 17 ffvelcdmd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) ) -> ( F ` k ) e. X )
19 3 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) ) -> P e. X )
20 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ ( F ` k ) e. X /\ P e. X ) -> ( ( F ` k ) D P ) e. RR* )
21 14 18 19 20 syl3anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) ) -> ( ( F ` k ) D P ) e. RR* )
22 17 nnrecred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) ) -> ( 1 / k ) e. RR )
23 22 rexrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) ) -> ( 1 / k ) e. RR* )
24 rpxr 
 |-  ( x e. RR+ -> x e. RR* )
25 24 ad2antlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) ) -> x e. RR* )
26 5 adantlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. NN ) -> ( ( F ` k ) D P ) < ( 1 / k ) )
27 17 26 syldan 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) ) -> ( ( F ` k ) D P ) < ( 1 / k ) )
28 8 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) ) -> ( 1 / x ) e. RR )
29 13 nnred 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( |_ ` ( 1 / x ) ) + 1 ) e. RR )
30 29 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) ) -> ( ( |_ ` ( 1 / x ) ) + 1 ) e. RR )
31 17 nnred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) ) -> k e. RR )
32 flltp1 
 |-  ( ( 1 / x ) e. RR -> ( 1 / x ) < ( ( |_ ` ( 1 / x ) ) + 1 ) )
33 28 32 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) ) -> ( 1 / x ) < ( ( |_ ` ( 1 / x ) ) + 1 ) )
34 eluzle 
 |-  ( k e. ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) -> ( ( |_ ` ( 1 / x ) ) + 1 ) <_ k )
35 34 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) ) -> ( ( |_ ` ( 1 / x ) ) + 1 ) <_ k )
36 28 30 31 33 35 ltletrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) ) -> ( 1 / x ) < k )
37 simplr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) ) -> x e. RR+ )
38 rpregt0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 < x ) )
39 nnrp 
 |-  ( k e. NN -> k e. RR+ )
40 39 rpregt0d 
 |-  ( k e. NN -> ( k e. RR /\ 0 < k ) )
41 ltrec1 
 |-  ( ( ( x e. RR /\ 0 < x ) /\ ( k e. RR /\ 0 < k ) ) -> ( ( 1 / x ) < k <-> ( 1 / k ) < x ) )
42 38 40 41 syl2an 
 |-  ( ( x e. RR+ /\ k e. NN ) -> ( ( 1 / x ) < k <-> ( 1 / k ) < x ) )
43 37 17 42 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) ) -> ( ( 1 / x ) < k <-> ( 1 / k ) < x ) )
44 36 43 mpbid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) ) -> ( 1 / k ) < x )
45 21 23 25 27 44 xrlttrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) ) -> ( ( F ` k ) D P ) < x )
46 45 ralrimiva 
 |-  ( ( ph /\ x e. RR+ ) -> A. k e. ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) ( ( F ` k ) D P ) < x )
47 fveq2 
 |-  ( j = ( ( |_ ` ( 1 / x ) ) + 1 ) -> ( ZZ>= ` j ) = ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) )
48 47 raleqdv 
 |-  ( j = ( ( |_ ` ( 1 / x ) ) + 1 ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) D P ) < x <-> A. k e. ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) ( ( F ` k ) D P ) < x ) )
49 48 rspcev 
 |-  ( ( ( ( |_ ` ( 1 / x ) ) + 1 ) e. NN /\ A. k e. ( ZZ>= ` ( ( |_ ` ( 1 / x ) ) + 1 ) ) ( ( F ` k ) D P ) < x ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) D P ) < x )
50 13 46 49 syl2anc 
 |-  ( ( ph /\ x e. RR+ ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) D P ) < x )
51 50 ralrimiva 
 |-  ( ph -> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) D P ) < x )
52 nnuz 
 |-  NN = ( ZZ>= ` 1 )
53 1zzd 
 |-  ( ph -> 1 e. ZZ )
54 eqidd 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) = ( F ` k ) )
55 1 2 52 53 54 4 lmmbrf 
 |-  ( ph -> ( F ( ~~>t ` J ) P <-> ( P e. X /\ A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) D P ) < x ) ) )
56 3 51 55 mpbir2and 
 |-  ( ph -> F ( ~~>t ` J ) P )