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 eqtrdi ( 𝜑 → ( 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 eqtr4di ( 𝑗 = 𝑀 → ( ℤ𝑗 ) = 𝑍 )
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 ( 𝜑𝐹𝐴 )