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

Metamath Proof Explorer

Theorem climz

Description: The zero sequence converges to zero. (Contributed by NM, 2-Oct-1999) (Revised by Mario Carneiro, 31-Jan-2014)

Ref Expression
Assertion climz ⊢ ℤ × 0 ⇝ 0

Proof

Step Hyp Ref Expression
1 0cn ⊢ 0 ∈ ℂ
2 0z ⊢ 0 ∈ ℤ
3 uzssz ⊢ ℤ ≥ 0 ⊆ ℤ
4 zex ⊢ ℤ ∈ V
5 3 4 climconst2 ⊢ 0 ∈ ℂ ∧ 0 ∈ ℤ → ℤ × 0 ⇝ 0
6 1 2 5 mp2an ⊢ ℤ × 0 ⇝ 0