Theorem constlimc

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

	Ref	Expression
Hypotheses	constlimc.f	$$⊢F=\left(x\in A⟼B\right)$$
	constlimc.a	$$⊢\phi \to A\subseteq ℂ$$
	constlimc.b	$$⊢\phi \to B\in ℂ$$
	constlimc.c	$$⊢\phi \to C\in ℂ$$
Assertion	constlimc	$$⊢\phi \to B\in \left(F{lim}_{ℂ}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		constlimc.f	$$⊢F=\left(x\in A⟼B\right)$$
2		constlimc.a	$$⊢\phi \to A\subseteq ℂ$$
3		constlimc.b	$$⊢\phi \to B\in ℂ$$
4		constlimc.c	$$⊢\phi \to C\in ℂ$$
5		1rp	$$⊢1\in {ℝ}^{+}$$
6	5	a1i	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to 1\in {ℝ}^{+}$$
7		simpr	$$⊢\left(\phi \wedge v\in A\right)\to v\in A$$
8		vex	$$⊢v\in \mathrm{V}$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}xB$$
10		csbtt	$$⊢\left(v\in \mathrm{V}\wedge \underset{\_}{Ⅎ}xB\right)\to ⦋v/x⦌B=B$$
11	8 9 10	mp2an	$$⊢⦋v/x⦌B=B$$
12	11 3	eqeltrid	$$⊢\phi \to ⦋v/x⦌B\in ℂ$$
13	12	adantr	$$⊢\left(\phi \wedge v\in A\right)\to ⦋v/x⦌B\in ℂ$$
14	1	fvmpts	$$⊢\left(v\in A\wedge ⦋v/x⦌B\in ℂ\right)\to F\left(v\right)=⦋v/x⦌B$$
15	7 13 14	syl2anc	$$⊢\left(\phi \wedge v\in A\right)\to F\left(v\right)=⦋v/x⦌B$$
16	15	oveq1d	$$⊢\left(\phi \wedge v\in A\right)\to F\left(v\right)-B=⦋v/x⦌B-B$$
17	11	oveq1i	$$⊢⦋v/x⦌B-B=B-B$$
18	16 17	eqtrdi	$$⊢\left(\phi \wedge v\in A\right)\to F\left(v\right)-B=B-B$$
19	18	fveq2d	$$⊢\left(\phi \wedge v\in A\right)\to \left|F\left(v\right)-B\right|=\left|B-B\right|$$
20	3	subidd	$$⊢\phi \to B-B=0$$
21	20	fveq2d	$$⊢\phi \to \left|B-B\right|=\left|0\right|$$
22	21	adantr	$$⊢\left(\phi \wedge v\in A\right)\to \left|B-B\right|=\left|0\right|$$
23		abs0	$$⊢\left|0\right|=0$$
24	23	a1i	$$⊢\left(\phi \wedge v\in A\right)\to \left|0\right|=0$$
25	19 22 24	3eqtrd	$$⊢\left(\phi \wedge v\in A\right)\to \left|F\left(v\right)-B\right|=0$$
26	25	adantlr	$$⊢\left(\left(\phi \wedge y\in {ℝ}^{+}\right)\wedge v\in A\right)\to \left|F\left(v\right)-B\right|=0$$
27		rpgt0	$$⊢y\in {ℝ}^{+}\to 0<y$$
28	27	ad2antlr	$$⊢\left(\left(\phi \wedge y\in {ℝ}^{+}\right)\wedge v\in A\right)\to 0<y$$
29	26 28	eqbrtrd	$$⊢\left(\left(\phi \wedge y\in {ℝ}^{+}\right)\wedge v\in A\right)\to \left|F\left(v\right)-B\right|<y$$
30	29	a1d	$$⊢\left(\left(\phi \wedge y\in {ℝ}^{+}\right)\wedge v\in A\right)\to \left(\left(v\ne C\wedge \left|v-C\right|<1\right)\to \left|F\left(v\right)-B\right|<y\right)$$
31	30	ralrimiva	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \forall v\in A\left(\left(v\ne C\wedge \left|v-C\right|<1\right)\to \left|F\left(v\right)-B\right|<y\right)$$
32		brimralrspcev	$$⊢\left(1\in {ℝ}^{+}\wedge \forall v\in A\left(\left(v\ne C\wedge \left|v-C\right|<1\right)\to \left|F\left(v\right)-B\right|<y\right)\right)\to \exists w\in {ℝ}^{+}\forall v\in A\left(\left(v\ne C\wedge \left|v-C\right|<w\right)\to \left|F\left(v\right)-B\right|<y\right)$$
33	6 31 32	syl2anc	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \exists w\in {ℝ}^{+}\forall v\in A\left(\left(v\ne C\wedge \left|v-C\right|<w\right)\to \left|F\left(v\right)-B\right|<y\right)$$
34	33	ralrimiva	$$⊢\phi \to \forall y\in {ℝ}^{+}\exists w\in {ℝ}^{+}\forall v\in A\left(\left(v\ne C\wedge \left|v-C\right|<w\right)\to \left|F\left(v\right)-B\right|<y\right)$$
35	3	adantr	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℂ$$
36	35 1	fmptd	$$⊢\phi \to F:A⟶ℂ$$
37	36 2 4	ellimc3	$$⊢\phi \to \left(B\in \left(F{lim}_{ℂ}C\right)\leftrightarrow \left(B\in ℂ\wedge \forall y\in {ℝ}^{+}\exists w\in {ℝ}^{+}\forall v\in A\left(\left(v\ne C\wedge \left|v-C\right|<w\right)\to \left|F\left(v\right)-B\right|<y\right)\right)\right)$$
38	3 34 37	mpbir2and	$$⊢\phi \to B\in \left(F{lim}_{ℂ}C\right)$$