Metamath Proof Explorer

Theorem rlimconst

Description: A constant sequence converges to its value. (Contributed by Mario Carneiro, 16-Sep-2014)

Ref Expression
Assertion rlimconst ⊢ A ⊆ ℝ ∧ B ∈ ℂ → x ∈ A ⟼ B ⇝ℝ B

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 simpllr ⊢ A ⊆ ℝ ∧ B ∈ ℂ ∧ y ∈ ℝ + ∧ x ∈ A → B ∈ ℂ
3 2 subidd ⊢ A ⊆ ℝ ∧ B ∈ ℂ ∧ y ∈ ℝ + ∧ x ∈ A → B − B = 0
4 3 fveq2d ⊢ A ⊆ ℝ ∧ B ∈ ℂ ∧ y ∈ ℝ + ∧ x ∈ A → B − B = 0
5 abs0 ⊢ 0 = 0
6 4 5 eqtrdi ⊢ A ⊆ ℝ ∧ B ∈ ℂ ∧ y ∈ ℝ + ∧ x ∈ A → B − B = 0
7 rpgt0 ⊢ y ∈ ℝ + → 0 < y
8 7 ad2antlr ⊢ A ⊆ ℝ ∧ B ∈ ℂ ∧ y ∈ ℝ + ∧ x ∈ A → 0 < y
9 6 8 eqbrtrd ⊢ A ⊆ ℝ ∧ B ∈ ℂ ∧ y ∈ ℝ + ∧ x ∈ A → B − B < y
10 9 a1d ⊢ A ⊆ ℝ ∧ B ∈ ℂ ∧ y ∈ ℝ + ∧ x ∈ A → 0 ≤ x → B − B < y
11 10 ralrimiva ⊢ A ⊆ ℝ ∧ B ∈ ℂ ∧ y ∈ ℝ + → ∀ x ∈ A 0 ≤ x → B − B < y
12 breq1 ⊢ z = 0 → z ≤ x ↔ 0 ≤ x
13 12 rspceaimv ⊢ 0 ∈ ℝ ∧ ∀ x ∈ A 0 ≤ x → B − B < y → ∃ z ∈ ℝ ∀ x ∈ A z ≤ x → B − B < y
14 1 11 13 sylancr ⊢ A ⊆ ℝ ∧ B ∈ ℂ ∧ y ∈ ℝ + → ∃ z ∈ ℝ ∀ x ∈ A z ≤ x → B − B < y
15 14 ralrimiva ⊢ A ⊆ ℝ ∧ B ∈ ℂ → ∀ y ∈ ℝ + ∃ z ∈ ℝ ∀ x ∈ A z ≤ x → B − B < y
16 simplr ⊢ A ⊆ ℝ ∧ B ∈ ℂ ∧ x ∈ A → B ∈ ℂ
17 16 ralrimiva ⊢ A ⊆ ℝ ∧ B ∈ ℂ → ∀ x ∈ A B ∈ ℂ
18 simpl ⊢ A ⊆ ℝ ∧ B ∈ ℂ → A ⊆ ℝ
19 simpr ⊢ A ⊆ ℝ ∧ B ∈ ℂ → B ∈ ℂ
20 17 18 19 rlim2 ⊢ A ⊆ ℝ ∧ B ∈ ℂ → x ∈ A ⟼ B ⇝ℝ B ↔ ∀ y ∈ ℝ + ∃ z ∈ ℝ ∀ x ∈ A z ≤ x → B − B < y
21 15 20 mpbird ⊢ A ⊆ ℝ ∧ B ∈ ℂ → x ∈ A ⟼ B ⇝ℝ B