# 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 𝑍 = ( ℤ𝑀 )
lmle.3 𝐽 = ( MetOpen ‘ 𝐷 )
lmle.4 ( 𝜑𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
lmle.6 ( 𝜑𝑀 ∈ ℤ )
lmle.7 ( 𝜑𝐹 ( ⇝𝑡𝐽 ) 𝑃 )
lmle.8 ( 𝜑𝑄𝑋 )
lmle.9 ( 𝜑𝑅 ∈ ℝ* )
lmle.10 ( ( 𝜑𝑘𝑍 ) → ( 𝑄 𝐷 ( 𝐹𝑘 ) ) ≤ 𝑅 )
Assertion lmle ( 𝜑 → ( 𝑄 𝐷 𝑃 ) ≤ 𝑅 )

### Proof

Step Hyp Ref Expression
1 lmle.1 𝑍 = ( ℤ𝑀 )
2 lmle.3 𝐽 = ( MetOpen ‘ 𝐷 )
3 lmle.4 ( 𝜑𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
4 lmle.6 ( 𝜑𝑀 ∈ ℤ )
5 lmle.7 ( 𝜑𝐹 ( ⇝𝑡𝐽 ) 𝑃 )
6 lmle.8 ( 𝜑𝑄𝑋 )
7 lmle.9 ( 𝜑𝑅 ∈ ℝ* )
8 lmle.10 ( ( 𝜑𝑘𝑍 ) → ( 𝑄 𝐷 ( 𝐹𝑘 ) ) ≤ 𝑅 )
9 2 mopntopon ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
10 3 9 syl ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
11 lmrel Rel ( ⇝𝑡𝐽 )
12 releldm ( ( Rel ( ⇝𝑡𝐽 ) ∧ 𝐹 ( ⇝𝑡𝐽 ) 𝑃 ) → 𝐹 ∈ dom ( ⇝𝑡𝐽 ) )
13 11 5 12 sylancr ( 𝜑𝐹 ∈ dom ( ⇝𝑡𝐽 ) )
14 1 10 4 13 lmff ( 𝜑 → ∃ 𝑗𝑍 ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 )
15 eqid ( ℤ𝑗 ) = ( ℤ𝑗 )
16 10 adantr ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
17 simprl ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 ) ) → 𝑗𝑍 )
18 17 1 eleqtrdi ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 ) ) → 𝑗 ∈ ( ℤ𝑀 ) )
19 eluzelz ( 𝑗 ∈ ( ℤ𝑀 ) → 𝑗 ∈ ℤ )
20 18 19 syl ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 ) ) → 𝑗 ∈ ℤ )
21 5 adantr ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 ) ) → 𝐹 ( ⇝𝑡𝐽 ) 𝑃 )
22 oveq2 ( 𝑥 = ( 𝐹𝑘 ) → ( 𝑄 𝐷 𝑥 ) = ( 𝑄 𝐷 ( 𝐹𝑘 ) ) )
23 22 breq1d ( 𝑥 = ( 𝐹𝑘 ) → ( ( 𝑄 𝐷 𝑥 ) ≤ 𝑅 ↔ ( 𝑄 𝐷 ( 𝐹𝑘 ) ) ≤ 𝑅 ) )
24 fvres ( 𝑘 ∈ ( ℤ𝑗 ) → ( ( 𝐹 ↾ ( ℤ𝑗 ) ) ‘ 𝑘 ) = ( 𝐹𝑘 ) )
25 24 adantl ( ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → ( ( 𝐹 ↾ ( ℤ𝑗 ) ) ‘ 𝑘 ) = ( 𝐹𝑘 ) )
26 simprr ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 ) ) → ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 )
27 26 ffvelrnda ( ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → ( ( 𝐹 ↾ ( ℤ𝑗 ) ) ‘ 𝑘 ) ∈ 𝑋 )
28 25 27 eqeltrrd ( ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → ( 𝐹𝑘 ) ∈ 𝑋 )
29 1 uztrn2 ( ( 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ) → 𝑘𝑍 )
30 17 29 sylan ( ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → 𝑘𝑍 )
31 8 adantlr ( ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 ) ) ∧ 𝑘𝑍 ) → ( 𝑄 𝐷 ( 𝐹𝑘 ) ) ≤ 𝑅 )
32 30 31 syldan ( ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → ( 𝑄 𝐷 ( 𝐹𝑘 ) ) ≤ 𝑅 )
33 23 28 32 elrabd ( ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 ) ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → ( 𝐹𝑘 ) ∈ { 𝑥𝑋 ∣ ( 𝑄 𝐷 𝑥 ) ≤ 𝑅 } )
34 eqid { 𝑥𝑋 ∣ ( 𝑄 𝐷 𝑥 ) ≤ 𝑅 } = { 𝑥𝑋 ∣ ( 𝑄 𝐷 𝑥 ) ≤ 𝑅 }
35 2 34 blcld ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑄𝑋𝑅 ∈ ℝ* ) → { 𝑥𝑋 ∣ ( 𝑄 𝐷 𝑥 ) ≤ 𝑅 } ∈ ( Clsd ‘ 𝐽 ) )
36 3 6 7 35 syl3anc ( 𝜑 → { 𝑥𝑋 ∣ ( 𝑄 𝐷 𝑥 ) ≤ 𝑅 } ∈ ( Clsd ‘ 𝐽 ) )
37 36 adantr ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 ) ) → { 𝑥𝑋 ∣ ( 𝑄 𝐷 𝑥 ) ≤ 𝑅 } ∈ ( Clsd ‘ 𝐽 ) )
38 15 16 20 21 33 37 lmcld ( ( 𝜑 ∧ ( 𝑗𝑍 ∧ ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 ) ) → 𝑃 ∈ { 𝑥𝑋 ∣ ( 𝑄 𝐷 𝑥 ) ≤ 𝑅 } )
39 14 38 rexlimddv ( 𝜑𝑃 ∈ { 𝑥𝑋 ∣ ( 𝑄 𝐷 𝑥 ) ≤ 𝑅 } )
40 oveq2 ( 𝑥 = 𝑃 → ( 𝑄 𝐷 𝑥 ) = ( 𝑄 𝐷 𝑃 ) )
41 40 breq1d ( 𝑥 = 𝑃 → ( ( 𝑄 𝐷 𝑥 ) ≤ 𝑅 ↔ ( 𝑄 𝐷 𝑃 ) ≤ 𝑅 ) )
42 41 elrab ( 𝑃 ∈ { 𝑥𝑋 ∣ ( 𝑄 𝐷 𝑥 ) ≤ 𝑅 } ↔ ( 𝑃𝑋 ∧ ( 𝑄 𝐷 𝑃 ) ≤ 𝑅 ) )
43 42 simprbi ( 𝑃 ∈ { 𝑥𝑋 ∣ ( 𝑄 𝐷 𝑥 ) ≤ 𝑅 } → ( 𝑄 𝐷 𝑃 ) ≤ 𝑅 )
44 39 43 syl ( 𝜑 → ( 𝑄 𝐷 𝑃 ) ≤ 𝑅 )