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

Metamath Proof Explorer

Theorem climconstmpt

Description: A constant sequence converges to its value. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses climconstmpt.m ⊢ φ → M ∈ ℤ
climconstmpt.z ⊢ Z = ℤ ≥ M
climconstmpt.a ⊢ φ → A ∈ ℂ
Assertion climconstmpt ⊢ φ → x ∈ Z ⟼ A ⇝ A

Proof

Step Hyp Ref Expression
1 climconstmpt.m ⊢ φ → M ∈ ℤ
2 climconstmpt.z ⊢ Z = ℤ ≥ M
3 climconstmpt.a ⊢ φ → A ∈ ℂ
4 fconstmpt ⊢ Z × A = x ∈ Z ⟼ A
5 2 eqcomi ⊢ ℤ ≥ M = Z
6 ssid ⊢ Z ⊆ Z
7 5 6 eqsstri ⊢ ℤ ≥ M ⊆ Z
8 2 fvexi ⊢ Z ∈ V
9 7 8 climconst2 ⊢ A ∈ ℂ ∧ M ∈ ℤ → Z × A ⇝ A
10 3 1 9 syl2anc ⊢ φ → Z × A ⇝ A
11 4 10 eqbrtrrid ⊢ φ → x ∈ Z ⟼ A ⇝ A