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

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℤ ) → ( 𝑍 × { 𝐴 } ) ⇝ 𝐴 )