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 ⊢ ℤ ≥ M ⊆ Z
climconst2.2 ⊢ Z ∈ V
Assertion climconst2 ⊢ A ∈ ℂ ∧ M ∈ ℤ → Z × A ⇝ A

Proof

Step Hyp Ref Expression
1 climconst2.1 ⊢ ℤ ≥ M ⊆ Z
2 climconst2.2 ⊢ Z ∈ V
3 eqid ⊢ ℤ ≥ M = ℤ ≥ M
4 simpr ⊢ A ∈ ℂ ∧ M ∈ ℤ → M ∈ ℤ
5 snex ⊢ A ∈ V
6 2 5 xpex ⊢ Z × A ∈ V
7 6 a1i ⊢ A ∈ ℂ ∧ M ∈ ℤ → Z × A ∈ V
8 simpl ⊢ A ∈ ℂ ∧ M ∈ ℤ → A ∈ ℂ
9 1 sseli ⊢ k ∈ ℤ ≥ M → k ∈ Z
10 fvconst2g ⊢ A ∈ ℂ ∧ k ∈ Z → Z × A ⁡ k = A
11 8 9 10 syl2an ⊢ A ∈ ℂ ∧ M ∈ ℤ ∧ k ∈ ℤ ≥ M → Z × A ⁡ k = A
12 3 4 7 8 11 climconst ⊢ A ∈ ℂ ∧ M ∈ ℤ → Z × A ⇝ A