Theorem climconst2

Description: A constant sequence converges to its value. (Contributed by NM, 6-Feb-2008) (Revised by Mario Carneiro, 31-Jan-2014)

	Ref	Expression
Hypotheses	climconst2.1	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ 𝑍
	climconst2.2	⊢ 𝑍 ∈ V
Assertion	climconst2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℤ ) → ( 𝑍 × { 𝐴 } ) ⇝ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		climconst2.1	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ 𝑍
2		climconst2.2	⊢ 𝑍 ∈ V
3		eqid	⊢ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑀 )
4		simpr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ ℤ )
5		snex	⊢ { 𝐴 } ∈ V
6	2 5	xpex	⊢ ( 𝑍 × { 𝐴 } ) ∈ V
7	6	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℤ ) → ( 𝑍 × { 𝐴 } ) ∈ V )
8		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℤ ) → 𝐴 ∈ ℂ )
9	1	sseli	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ 𝑍 )
10		fvconst2g	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑍 × { 𝐴 } ) ‘ 𝑘 ) = 𝐴 )
11	8 9 10	syl2an	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℤ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑍 × { 𝐴 } ) ‘ 𝑘 ) = 𝐴 )
12	3 4 7 8 11	climconst	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℤ ) → ( 𝑍 × { 𝐴 } ) ⇝ 𝐴 )