This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ 𝑋 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) ‘ 𝑘 ) ∈ 𝑋 )
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 ⊢ ( 𝜑 → ( 𝑄 𝐷 𝑃 ) ≤ 𝑅 )