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	⊢ ( 𝜑 → ( 𝑄 𝐷 𝑃 ) ≤ 𝑅 )