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

Metamath Proof Explorer

Theorem climconst

Description: An (eventually) constant sequence converges to its value. (Contributed by NM, 28-Aug-2005) (Revised by Mario Carneiro, 31-Jan-2014)

Ref Expression
Hypotheses climconst.1 ⊢ Z = ℤ ≥ M
climconst.2 ⊢ φ → M ∈ ℤ
climconst.3 ⊢ φ → F ∈ V
climconst.4 ⊢ φ → A ∈ ℂ
climconst.5 ⊢ φ ∧ k ∈ Z → F ⁡ k = A
Assertion climconst ⊢ φ → F ⇝ A

Proof

Step Hyp Ref Expression
1 climconst.1 ⊢ Z = ℤ ≥ M
2 climconst.2 ⊢ φ → M ∈ ℤ
3 climconst.3 ⊢ φ → F ∈ V
4 climconst.4 ⊢ φ → A ∈ ℂ
5 climconst.5 ⊢ φ ∧ k ∈ Z → F ⁡ k = A
6 uzid ⊢ M ∈ ℤ → M ∈ ℤ ≥ M
7 2 6 syl ⊢ φ → M ∈ ℤ ≥ M
8 7 1 eleqtrrdi ⊢ φ → M ∈ Z
9 4 subidd ⊢ φ → A − A = 0
10 9 fveq2d ⊢ φ → A − A = 0
11 abs0 ⊢ 0 = 0
12 10 11 eqtrdi ⊢ φ → A − A = 0
13 12 adantr ⊢ φ ∧ x ∈ ℝ + → A − A = 0
14 rpgt0 ⊢ x ∈ ℝ + → 0 < x
15 14 adantl ⊢ φ ∧ x ∈ ℝ + → 0 < x
16 13 15 eqbrtrd ⊢ φ ∧ x ∈ ℝ + → A − A < x
17 16 ralrimivw ⊢ φ ∧ x ∈ ℝ + → ∀ k ∈ Z A − A < x
18 fveq2 ⊢ j = M → ℤ ≥ j = ℤ ≥ M
19 18 1 eqtr4di ⊢ j = M → ℤ ≥ j = Z
20 19 raleqdv ⊢ j = M → ∀ k ∈ ℤ ≥ j A − A < x ↔ ∀ k ∈ Z A − A < x
21 20 rspcev ⊢ M ∈ Z ∧ ∀ k ∈ Z A − A < x → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j A − A < x
22 8 17 21 syl2an2r ⊢ φ ∧ x ∈ ℝ + → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j A − A < x
23 22 ralrimiva ⊢ φ → ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j A − A < x
24 4 adantr ⊢ φ ∧ k ∈ Z → A ∈ ℂ
25 1 2 3 5 4 24 clim2c ⊢ φ → F ⇝ A ↔ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j A − A < x
26 23 25 mpbird ⊢ φ → F ⇝ A