# Metamath Proof Explorer

## Theorem lmle

Description: If the distance from each member of a converging sequence to a given point is less than or equal to a given amount, so is the convergence value. (Contributed by NM, 23-Dec-2007) (Proof shortened by Mario Carneiro, 1-May-2014)

Ref Expression
Hypotheses lmle.1
`|- Z = ( ZZ>= ` M )`
lmle.3
`|- J = ( MetOpen ` D )`
lmle.4
`|- ( ph -> D e. ( *Met ` X ) )`
lmle.6
`|- ( ph -> M e. ZZ )`
lmle.7
`|- ( ph -> F ( ~~>t ` J ) P )`
lmle.8
`|- ( ph -> Q e. X )`
lmle.9
`|- ( ph -> R e. RR* )`
lmle.10
`|- ( ( ph /\ k e. Z ) -> ( Q D ( F ` k ) ) <_ R )`
Assertion lmle
`|- ( ph -> ( Q D P ) <_ R )`

### Proof

Step Hyp Ref Expression
1 lmle.1
` |-  Z = ( ZZ>= ` M )`
2 lmle.3
` |-  J = ( MetOpen ` D )`
3 lmle.4
` |-  ( ph -> D e. ( *Met ` X ) )`
4 lmle.6
` |-  ( ph -> M e. ZZ )`
5 lmle.7
` |-  ( ph -> F ( ~~>t ` J ) P )`
6 lmle.8
` |-  ( ph -> Q e. X )`
7 lmle.9
` |-  ( ph -> R e. RR* )`
8 lmle.10
` |-  ( ( ph /\ k e. Z ) -> ( Q D ( F ` k ) ) <_ R )`
9 2 mopntopon
` |-  ( D e. ( *Met ` X ) -> J e. ( TopOn ` X ) )`
10 3 9 syl
` |-  ( ph -> J e. ( TopOn ` X ) )`
11 lmrel
` |-  Rel ( ~~>t ` J )`
12 releldm
` |-  ( ( Rel ( ~~>t ` J ) /\ F ( ~~>t ` J ) P ) -> F e. dom ( ~~>t ` J ) )`
13 11 5 12 sylancr
` |-  ( ph -> F e. dom ( ~~>t ` J ) )`
14 1 10 4 13 lmff
` |-  ( ph -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X )`
15 eqid
` |-  ( ZZ>= ` j ) = ( ZZ>= ` j )`
` |-  ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) -> J e. ( TopOn ` X ) )`
17 simprl
` |-  ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) -> j e. Z )`
18 17 1 eleqtrdi
` |-  ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) -> j e. ( ZZ>= ` M ) )`
19 eluzelz
` |-  ( j e. ( ZZ>= ` M ) -> j e. ZZ )`
20 18 19 syl
` |-  ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) -> j e. ZZ )`
` |-  ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) -> F ( ~~>t ` J ) P )`
22 oveq2
` |-  ( x = ( F ` k ) -> ( Q D x ) = ( Q D ( F ` k ) ) )`
23 22 breq1d
` |-  ( x = ( F ` k ) -> ( ( Q D x ) <_ R <-> ( Q D ( F ` k ) ) <_ R ) )`
24 fvres
` |-  ( k e. ( ZZ>= ` j ) -> ( ( F |` ( ZZ>= ` j ) ) ` k ) = ( F ` k ) )`
` |-  ( ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F |` ( ZZ>= ` j ) ) ` k ) = ( F ` k ) )`
26 simprr
` |-  ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) -> ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X )`
27 26 ffvelrnda
` |-  ( ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F |` ( ZZ>= ` j ) ) ` k ) e. X )`
28 25 27 eqeltrrd
` |-  ( ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. X )`
29 1 uztrn2
` |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )`
30 17 29 sylan
` |-  ( ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) /\ k e. ( ZZ>= ` j ) ) -> k e. Z )`
` |-  ( ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) /\ k e. Z ) -> ( Q D ( F ` k ) ) <_ R )`
32 30 31 syldan
` |-  ( ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) /\ k e. ( ZZ>= ` j ) ) -> ( Q D ( F ` k ) ) <_ R )`
33 23 28 32 elrabd
` |-  ( ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. { x e. X | ( Q D x ) <_ R } )`
34 eqid
` |-  { x e. X | ( Q D x ) <_ R } = { x e. X | ( Q D x ) <_ R }`
35 2 34 blcld
` |-  ( ( D e. ( *Met ` X ) /\ Q e. X /\ R e. RR* ) -> { x e. X | ( Q D x ) <_ R } e. ( Clsd ` J ) )`
36 3 6 7 35 syl3anc
` |-  ( ph -> { x e. X | ( Q D x ) <_ R } e. ( Clsd ` J ) )`
` |-  ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) -> { x e. X | ( Q D x ) <_ R } e. ( Clsd ` J ) )`
38 15 16 20 21 33 37 lmcld
` |-  ( ( ph /\ ( j e. Z /\ ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X ) ) -> P e. { x e. X | ( Q D x ) <_ R } )`
39 14 38 rexlimddv
` |-  ( ph -> P e. { x e. X | ( Q D x ) <_ R } )`
40 oveq2
` |-  ( x = P -> ( Q D x ) = ( Q D P ) )`
41 40 breq1d
` |-  ( x = P -> ( ( Q D x ) <_ R <-> ( Q D P ) <_ R ) )`
42 41 elrab
` |-  ( P e. { x e. X | ( Q D x ) <_ R } <-> ( P e. X /\ ( Q D P ) <_ R ) )`
43 42 simprbi
` |-  ( P e. { x e. X | ( Q D x ) <_ R } -> ( Q D P ) <_ R )`
44 39 43 syl
` |-  ( ph -> ( Q D P ) <_ R )`