Metamath Proof Explorer

Theorem lmmcvg

Description: Convergence property of a converging sequence. (Contributed by NM, 1-Jun-2007) (Revised by Mario Carneiro, 1-May-2014)

Ref Expression
Hypotheses lmmbr.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
lmmbr.3 ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
lmmbr3.5 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
lmmbr3.6 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
lmmbrf.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
lmmcvg.8 ⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 )
lmmcvg.9 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
Assertion lmmcvg ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝑃 ) < 𝑅 ) )

Proof

Step Hyp Ref Expression
1 lmmbr.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 lmmbr.3 ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
3 lmmbr3.5 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4 lmmbr3.6 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5 lmmbrf.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
6 lmmcvg.8 ⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 )
7 lmmcvg.9 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
8 breq2 ⊢ ( 𝑥 = 𝑅 → ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ↔ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑅 ) )
9 8 3anbi3d ⊢ ( 𝑥 = 𝑅 → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ↔ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑅 ) ) )
10 9 rexralbidv ⊢ ( 𝑥 = 𝑅 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑅 ) ) )
11 1 2 3 4 lmmbr3 ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) ) )
12 6 11 mpbid ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) )
13 12 simp3d ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) )
14 10 13 7 rspcdva ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑅 ) )
15 3 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
16 3simpc ⊢ ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑅 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑅 ) )
17 5 eleq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ↔ 𝐴 ∈ 𝑋 ) )
18 5 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) = ( 𝐴 𝐷 𝑃 ) )
19 18 breq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑅 ↔ ( 𝐴 𝐷 𝑃 ) < 𝑅 ) )
20 17 19 anbi12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑅 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝑃 ) < 𝑅 ) ) )
21 16 20 syl5ib ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑅 ) → ( 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝑃 ) < 𝑅 ) ) )
22 15 21 sylan2 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑅 ) → ( 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝑃 ) < 𝑅 ) ) )
23 22 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑅 ) → ( 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝑃 ) < 𝑅 ) ) )
24 23 ralimdva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑅 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝑃 ) < 𝑅 ) ) )
25 24 reximdva ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑅 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝑃 ) < 𝑅 ) ) )
26 14 25 mpd ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝑃 ) < 𝑅 ) )