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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climconst.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climconst.3 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
climconst.4 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
climconst.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
Assertion climconst ( 𝜑 → 𝐹 ⇝ 𝐴 )

Proof

Step Hyp Ref Expression
1 climconst.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 climconst.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 climconst.3 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
4 climconst.4 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
5 climconst.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
6 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
7 2 6 syl ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
8 7 1 eleqtrrdi ⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
9 4 subidd ⊢ ( 𝜑 → ( 𝐴 − 𝐴 ) = 0 )
10 9 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐴 ) ) = ( abs ‘ 0 ) )
11 abs0 ⊢ ( abs ‘ 0 ) = 0
12 10 11 syl6eq ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐴 ) ) = 0 )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ ( 𝐴 − 𝐴 ) ) = 0 )
14 rpgt0 ⊢ ( 𝑥 ∈ ℝ+ → 0 < 𝑥 )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 0 < 𝑥 )
16 13 15 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ ( 𝐴 − 𝐴 ) ) < 𝑥 )
17 16 ralrimivw ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐴 − 𝐴 ) ) < 𝑥 )
18 fveq2 ⊢ ( 𝑗 = 𝑀 → ( ℤ≥ ‘ 𝑗 ) = ( ℤ≥ ‘ 𝑀 ) )
19 18 1 syl6eqr ⊢ ( 𝑗 = 𝑀 → ( ℤ≥ ‘ 𝑗 ) = 𝑍 )
20 19 raleqdv ⊢ ( 𝑗 = 𝑀 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐴 − 𝐴 ) ) < 𝑥 ↔ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐴 − 𝐴 ) ) < 𝑥 ) )
21 20 rspcev ⊢ ( ( 𝑀 ∈ 𝑍 ∧ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐴 − 𝐴 ) ) < 𝑥 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐴 − 𝐴 ) ) < 𝑥 )
22 8 17 21 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐴 − 𝐴 ) ) < 𝑥 )
23 22 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐴 − 𝐴 ) ) < 𝑥 )
24 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
25 1 2 3 5 4 24 clim2c ⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐴 − 𝐴 ) ) < 𝑥 ) )
26 23 25 mpbird ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )