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

Metamath Proof Explorer

Theorem rlimconst

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

Ref Expression
Assertion rlimconst ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐵 )

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 simpllr ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
3 2 subidd ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 − 𝐵 ) = 0 )
4 3 fveq2d ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( 𝐵 − 𝐵 ) ) = ( abs ‘ 0 ) )
5 abs0 ⊢ ( abs ‘ 0 ) = 0
6 4 5 eqtrdi ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( 𝐵 − 𝐵 ) ) = 0 )
7 rpgt0 ⊢ ( 𝑦 ∈ ℝ+ → 0 < 𝑦 )
8 7 ad2antlr ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) → 0 < 𝑦 )
9 6 8 eqbrtrd ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( 𝐵 − 𝐵 ) ) < 𝑦 )
10 9 a1d ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) → ( 0 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐵 ) ) < 𝑦 ) )
11 10 ralrimiva ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) → ∀ 𝑥 ∈ 𝐴 ( 0 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐵 ) ) < 𝑦 ) )
12 breq1 ⊢ ( 𝑧 = 0 → ( 𝑧 ≤ 𝑥 ↔ 0 ≤ 𝑥 ) )
13 12 rspceaimv ⊢ ( ( 0 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( 0 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐵 ) ) < 𝑦 ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐵 ) ) < 𝑦 ) )
14 1 11 13 sylancr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐵 ) ) < 𝑦 ) )
15 14 ralrimiva ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ ) → ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐵 ) ) < 𝑦 ) )
16 simplr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
17 16 ralrimiva ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ ) → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ℂ )
18 simpl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ ) → 𝐴 ⊆ ℝ )
19 simpr ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
20 17 18 19 rlim2 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐵 ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → ( abs ‘ ( 𝐵 − 𝐵 ) ) < 𝑦 ) ) )
21 15 20 mpbird ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐵 )