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	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐵 )