Metamath Proof Explorer

Theorem lmconst

Description: A constant sequence converges to its value. (Contributed by NM, 8-Nov-2007) (Revised by Mario Carneiro, 14-Nov-2013)

Ref Expression
Hypothesis lmconst.2 ⊢ Z = ℤ ≥ M
Assertion lmconst ⊢ J ∈ TopOn ⁡ X ∧ P ∈ X ∧ M ∈ ℤ → Z × P ⇝t ⁡ J P

Proof

Step Hyp Ref Expression
1 lmconst.2 ⊢ Z = ℤ ≥ M
2 simp2 ⊢ J ∈ TopOn ⁡ X ∧ P ∈ X ∧ M ∈ ℤ → P ∈ X
3 simp3 ⊢ J ∈ TopOn ⁡ X ∧ P ∈ X ∧ M ∈ ℤ → M ∈ ℤ
4 uzid ⊢ M ∈ ℤ → M ∈ ℤ ≥ M
5 3 4 syl ⊢ J ∈ TopOn ⁡ X ∧ P ∈ X ∧ M ∈ ℤ → M ∈ ℤ ≥ M
6 5 1 eleqtrrdi ⊢ J ∈ TopOn ⁡ X ∧ P ∈ X ∧ M ∈ ℤ → M ∈ Z
7 idd ⊢ J ∈ TopOn ⁡ X ∧ P ∈ X ∧ M ∈ ℤ ∧ k ∈ ℤ ≥ M → P ∈ u → P ∈ u
8 7 ralrimdva ⊢ J ∈ TopOn ⁡ X ∧ P ∈ X ∧ M ∈ ℤ → P ∈ u → ∀ k ∈ ℤ ≥ M P ∈ u
9 fveq2 ⊢ j = M → ℤ ≥ j = ℤ ≥ M
10 9 raleqdv ⊢ j = M → ∀ k ∈ ℤ ≥ j P ∈ u ↔ ∀ k ∈ ℤ ≥ M P ∈ u
11 10 rspcev ⊢ M ∈ Z ∧ ∀ k ∈ ℤ ≥ M P ∈ u → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j P ∈ u
12 6 8 11 syl6an ⊢ J ∈ TopOn ⁡ X ∧ P ∈ X ∧ M ∈ ℤ → P ∈ u → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j P ∈ u
13 12 ralrimivw ⊢ J ∈ TopOn ⁡ X ∧ P ∈ X ∧ M ∈ ℤ → ∀ u ∈ J P ∈ u → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j P ∈ u
14 simp1 ⊢ J ∈ TopOn ⁡ X ∧ P ∈ X ∧ M ∈ ℤ → J ∈ TopOn ⁡ X
15 fconst6g ⊢ P ∈ X → Z × P : Z ⟶ X
16 2 15 syl ⊢ J ∈ TopOn ⁡ X ∧ P ∈ X ∧ M ∈ ℤ → Z × P : Z ⟶ X
17 fvconst2g ⊢ P ∈ X ∧ k ∈ Z → Z × P ⁡ k = P
18 2 17 sylan ⊢ J ∈ TopOn ⁡ X ∧ P ∈ X ∧ M ∈ ℤ ∧ k ∈ Z → Z × P ⁡ k = P
19 14 1 3 16 18 lmbrf ⊢ J ∈ TopOn ⁡ X ∧ P ∈ X ∧ M ∈ ℤ → Z × P ⇝t ⁡ J P ↔ P ∈ X ∧ ∀ u ∈ J P ∈ u → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j P ∈ u
20 2 13 19 mpbir2and ⊢ J ∈ TopOn ⁡ X ∧ P ∈ X ∧ M ∈ ℤ → Z × P ⇝t ⁡ J P