# 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}={ℤ}_{\ge {M}}$
lmle.3 ${⊢}{J}=\mathrm{MetOpen}\left({D}\right)$
lmle.4 ${⊢}{\phi }\to {D}\in \mathrm{\infty Met}\left({X}\right)$
lmle.6 ${⊢}{\phi }\to {M}\in ℤ$
lmle.7
lmle.8 ${⊢}{\phi }\to {Q}\in {X}$
lmle.9 ${⊢}{\phi }\to {R}\in {ℝ}^{*}$
lmle.10 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {Q}{D}{F}\left({k}\right)\le {R}$
Assertion lmle ${⊢}{\phi }\to {Q}{D}{P}\le {R}$

### Proof

Step Hyp Ref Expression
1 lmle.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
2 lmle.3 ${⊢}{J}=\mathrm{MetOpen}\left({D}\right)$
3 lmle.4 ${⊢}{\phi }\to {D}\in \mathrm{\infty Met}\left({X}\right)$
4 lmle.6 ${⊢}{\phi }\to {M}\in ℤ$
5 lmle.7
6 lmle.8 ${⊢}{\phi }\to {Q}\in {X}$
7 lmle.9 ${⊢}{\phi }\to {R}\in {ℝ}^{*}$
8 lmle.10 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {Q}{D}{F}\left({k}\right)\le {R}$
9 2 mopntopon ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to {J}\in \mathrm{TopOn}\left({X}\right)$
10 3 9 syl ${⊢}{\phi }\to {J}\in \mathrm{TopOn}\left({X}\right)$
11 lmrel
12 releldm
13 11 5 12 sylancr
14 1 10 4 13 lmff ${⊢}{\phi }\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}$
15 eqid ${⊢}{ℤ}_{\ge {j}}={ℤ}_{\ge {j}}$
16 10 adantr ${⊢}\left({\phi }\wedge \left({j}\in {Z}\wedge \left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}\right)\right)\to {J}\in \mathrm{TopOn}\left({X}\right)$
17 simprl ${⊢}\left({\phi }\wedge \left({j}\in {Z}\wedge \left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}\right)\right)\to {j}\in {Z}$
18 17 1 eleqtrdi ${⊢}\left({\phi }\wedge \left({j}\in {Z}\wedge \left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}\right)\right)\to {j}\in {ℤ}_{\ge {M}}$
19 eluzelz ${⊢}{j}\in {ℤ}_{\ge {M}}\to {j}\in ℤ$
20 18 19 syl ${⊢}\left({\phi }\wedge \left({j}\in {Z}\wedge \left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}\right)\right)\to {j}\in ℤ$
22 oveq2 ${⊢}{x}={F}\left({k}\right)\to {Q}{D}{x}={Q}{D}{F}\left({k}\right)$
23 22 breq1d ${⊢}{x}={F}\left({k}\right)\to \left({Q}{D}{x}\le {R}↔{Q}{D}{F}\left({k}\right)\le {R}\right)$
24 fvres ${⊢}{k}\in {ℤ}_{\ge {j}}\to \left({{F}↾}_{{ℤ}_{\ge {j}}}\right)\left({k}\right)={F}\left({k}\right)$
25 24 adantl ${⊢}\left(\left({\phi }\wedge \left({j}\in {Z}\wedge \left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}\right)\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to \left({{F}↾}_{{ℤ}_{\ge {j}}}\right)\left({k}\right)={F}\left({k}\right)$
26 simprr ${⊢}\left({\phi }\wedge \left({j}\in {Z}\wedge \left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}\right)\right)\to \left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}$
27 26 ffvelrnda ${⊢}\left(\left({\phi }\wedge \left({j}\in {Z}\wedge \left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}\right)\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to \left({{F}↾}_{{ℤ}_{\ge {j}}}\right)\left({k}\right)\in {X}$
28 25 27 eqeltrrd ${⊢}\left(\left({\phi }\wedge \left({j}\in {Z}\wedge \left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}\right)\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {F}\left({k}\right)\in {X}$
29 1 uztrn2 ${⊢}\left({j}\in {Z}\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {k}\in {Z}$
30 17 29 sylan ${⊢}\left(\left({\phi }\wedge \left({j}\in {Z}\wedge \left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}\right)\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {k}\in {Z}$
31 8 adantlr ${⊢}\left(\left({\phi }\wedge \left({j}\in {Z}\wedge \left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}\right)\right)\wedge {k}\in {Z}\right)\to {Q}{D}{F}\left({k}\right)\le {R}$
32 30 31 syldan ${⊢}\left(\left({\phi }\wedge \left({j}\in {Z}\wedge \left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}\right)\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {Q}{D}{F}\left({k}\right)\le {R}$
33 23 28 32 elrabd ${⊢}\left(\left({\phi }\wedge \left({j}\in {Z}\wedge \left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}\right)\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {F}\left({k}\right)\in \left\{{x}\in {X}|{Q}{D}{x}\le {R}\right\}$
34 eqid ${⊢}\left\{{x}\in {X}|{Q}{D}{x}\le {R}\right\}=\left\{{x}\in {X}|{Q}{D}{x}\le {R}\right\}$
35 2 34 blcld ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {Q}\in {X}\wedge {R}\in {ℝ}^{*}\right)\to \left\{{x}\in {X}|{Q}{D}{x}\le {R}\right\}\in \mathrm{Clsd}\left({J}\right)$
36 3 6 7 35 syl3anc ${⊢}{\phi }\to \left\{{x}\in {X}|{Q}{D}{x}\le {R}\right\}\in \mathrm{Clsd}\left({J}\right)$
37 36 adantr ${⊢}\left({\phi }\wedge \left({j}\in {Z}\wedge \left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}\right)\right)\to \left\{{x}\in {X}|{Q}{D}{x}\le {R}\right\}\in \mathrm{Clsd}\left({J}\right)$
38 15 16 20 21 33 37 lmcld ${⊢}\left({\phi }\wedge \left({j}\in {Z}\wedge \left({{F}↾}_{{ℤ}_{\ge {j}}}\right):{ℤ}_{\ge {j}}⟶{X}\right)\right)\to {P}\in \left\{{x}\in {X}|{Q}{D}{x}\le {R}\right\}$
39 14 38 rexlimddv ${⊢}{\phi }\to {P}\in \left\{{x}\in {X}|{Q}{D}{x}\le {R}\right\}$
40 oveq2 ${⊢}{x}={P}\to {Q}{D}{x}={Q}{D}{P}$
41 40 breq1d ${⊢}{x}={P}\to \left({Q}{D}{x}\le {R}↔{Q}{D}{P}\le {R}\right)$
42 41 elrab ${⊢}{P}\in \left\{{x}\in {X}|{Q}{D}{x}\le {R}\right\}↔\left({P}\in {X}\wedge {Q}{D}{P}\le {R}\right)$
43 42 simprbi ${⊢}{P}\in \left\{{x}\in {X}|{Q}{D}{x}\le {R}\right\}\to {Q}{D}{P}\le {R}$
44 39 43 syl ${⊢}{\phi }\to {Q}{D}{P}\le {R}$