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∈A0≤x→B−B<y
12 breq1 ⊢z=0→z≤x↔0≤x
13 12 rspceaimv ⊢0∈ℝ∧∀x∈A0≤x→B−B<y→∃z∈ℝ∀x∈Az≤x→B−B<y
14 1 11 13 sylancr ⊢A⊆ℝ∧B∈ℂ∧y∈ℝ+→∃z∈ℝ∀x∈Az≤x→B−B<y
15 14 ralrimiva ⊢A⊆ℝ∧B∈ℂ→∀y∈ℝ+∃z∈ℝ∀x∈Az≤x→B−B<y
16 simplr ⊢A⊆ℝ∧B∈ℂ∧x∈A→B∈ℂ
17 16 ralrimiva ⊢A⊆ℝ∧B∈ℂ→∀x∈AB∈ℂ
18 simpl ⊢A⊆ℝ∧B∈ℂ→A⊆ℝ
19 simpr ⊢A⊆ℝ∧B∈ℂ→B∈ℂ
20 17 18 19 rlim2 ⊢A⊆ℝ∧B∈ℂ→x∈A⟼B⇝ℝB↔∀y∈ℝ+∃z∈ℝ∀x∈Az≤x→B−B<y
21 15 20 mpbird ⊢A⊆ℝ∧B∈ℂ→x∈A⟼B⇝ℝB