Theorem constlimc

Description: Limit of constant function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	constlimc.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	constlimc.a	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
	constlimc.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	constlimc.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
Assertion	constlimc	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐹 limℂ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		constlimc.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		constlimc.a	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
3		constlimc.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
4		constlimc.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
5		1rp	⊢ 1 ∈ ℝ+
6	5	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 1 ∈ ℝ+ )
7		simpr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → 𝑣 ∈ 𝐴 )
8		vex	⊢ 𝑣 ∈ V
9		nfcv	⊢ Ⅎ 𝑥 𝐵
10		csbtt	⊢ ( ( 𝑣 ∈ V ∧ Ⅎ 𝑥 𝐵 ) → ⦋ 𝑣 / 𝑥 ⦌ 𝐵 = 𝐵 )
11	8 9 10	mp2an	⊢ ⦋ 𝑣 / 𝑥 ⦌ 𝐵 = 𝐵
12	11 3	eqeltrid	⊢ ( 𝜑 → ⦋ 𝑣 / 𝑥 ⦌ 𝐵 ∈ ℂ )
13	12	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ⦋ 𝑣 / 𝑥 ⦌ 𝐵 ∈ ℂ )
14	1	fvmpts	⊢ ( ( 𝑣 ∈ 𝐴 ∧ ⦋ 𝑣 / 𝑥 ⦌ 𝐵 ∈ ℂ ) → ( 𝐹 ‘ 𝑣 ) = ⦋ 𝑣 / 𝑥 ⦌ 𝐵 )
15	7 13 14	syl2anc	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑣 ) = ⦋ 𝑣 / 𝑥 ⦌ 𝐵 )
16	15	oveq1d	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑣 ) − 𝐵 ) = ( ⦋ 𝑣 / 𝑥 ⦌ 𝐵 − 𝐵 ) )
17	11	oveq1i	⊢ ( ⦋ 𝑣 / 𝑥 ⦌ 𝐵 − 𝐵 ) = ( 𝐵 − 𝐵 )
18	16 17	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑣 ) − 𝐵 ) = ( 𝐵 − 𝐵 ) )
19	18	fveq2d	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐵 ) ) = ( abs ‘ ( 𝐵 − 𝐵 ) ) )
20	3	subidd	⊢ ( 𝜑 → ( 𝐵 − 𝐵 ) = 0 )
21	20	fveq2d	⊢ ( 𝜑 → ( abs ‘ ( 𝐵 − 𝐵 ) ) = ( abs ‘ 0 ) )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( abs ‘ ( 𝐵 − 𝐵 ) ) = ( abs ‘ 0 ) )
23		abs0	⊢ ( abs ‘ 0 ) = 0
24	23	a1i	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( abs ‘ 0 ) = 0 )
25	19 22 24	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐵 ) ) = 0 )
26	25	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑣 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐵 ) ) = 0 )
27		rpgt0	⊢ ( 𝑦 ∈ ℝ+ → 0 < 𝑦 )
28	27	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑣 ∈ 𝐴 ) → 0 < 𝑦 )
29	26 28	eqbrtrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑣 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐵 ) ) < 𝑦 )
30	29	a1d	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑣 ∈ 𝐴 ) → ( ( 𝑣 ≠ 𝐶 ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 1 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐵 ) ) < 𝑦 ) )
31	30	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐶 ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 1 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐵 ) ) < 𝑦 ) )
32		brimralrspcev	⊢ ( ( 1 ∈ ℝ+ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐶 ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 1 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐵 ) ) < 𝑦 ) ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐶 ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐵 ) ) < 𝑦 ) )
33	6 31 32	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐶 ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐵 ) ) < 𝑦 ) )
34	33	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐶 ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐵 ) ) < 𝑦 ) )
35	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
36	35 1	fmptd	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
37	36 2 4	ellimc3	⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐹 limℂ 𝐶 ) ↔ ( 𝐵 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐶 ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 𝐵 ) ) < 𝑦 ) ) ) )
38	3 34 37	mpbir2and	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐹 limℂ 𝐶 ) )