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	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )

Metamath Proof Explorer

Theorem climconst

Proof