neglimc

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

	Ref	Expression
Hypotheses	neglimc.f	$⊢ F = (x \in A ⟼ B)$
	neglimc.g	$⊢ G = (x \in A ⟼ - B)$
	neglimc.b	$⊢ (φ \land x \in A) \to B \in ℂ$
	neglimc.c	$⊢ φ \to C \in (F {lim}_{ℂ} D)$
Assertion	neglimc	$⊢ φ \to - C \in (G {lim}_{ℂ} D)$

Proof

Step	Hyp	Ref	Expression
1		neglimc.f	$⊢ F = (x \in A ⟼ B)$
2		neglimc.g	$⊢ G = (x \in A ⟼ - B)$
3		neglimc.b	$⊢ (φ \land x \in A) \to B \in ℂ$
4		neglimc.c	$⊢ φ \to C \in (F {lim}_{ℂ} D)$
5		limccl	$⊢ F {lim}_{ℂ} D \subseteq ℂ$
6	5 4	sselid	$⊢ φ \to C \in ℂ$
7	6	negcld	$⊢ φ \to - C \in ℂ$
8	3 1	fmptd	$⊢ φ \to F : A ⟶ ℂ$
9	1 3 4	limcmptdm	$⊢ φ \to A \subseteq ℂ$
10		limcrcl	$⊢ C \in (F {lim}_{ℂ} D) \to (F : dom F ⟶ ℂ \land dom F \subseteq ℂ \land D \in ℂ)$
11	4 10	syl	$⊢ φ \to (F : dom F ⟶ ℂ \land dom F \subseteq ℂ \land D \in ℂ)$
12	11	simp3d	$⊢ φ \to D \in ℂ$
13	8 9 12	ellimc3	$⊢ φ \to (C \in (F {lim}_{ℂ} D) \leftrightarrow (C \in ℂ \land \forall y \in ℝ^{+} \exists w \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < w) \to \|F (v) - C\| < y)))$
14	4 13	mpbid	$⊢ φ \to (C \in ℂ \land \forall y \in ℝ^{+} \exists w \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < w) \to \|F (v) - C\| < y))$
15	14	simprd	$⊢ φ \to \forall y \in ℝ^{+} \exists w \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < w) \to \|F (v) - C\| < y)$
16	15	r19.21bi	$⊢ (φ \land y \in ℝ^{+}) \to \exists w \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < w) \to \|F (v) - C\| < y)$
17		simplll	$⊢ (((φ \land y \in ℝ^{+}) \land w \in ℝ^{+}) \land v \in A) \to φ$
18	17	3ad2ant1	$⊢ ((((φ \land y \in ℝ^{+}) \land w \in ℝ^{+}) \land v \in A) \land ((v \neq D \land \|v - D\| < w) \to \|F (v) - C\| < y) \land (v \neq D \land \|v - D\| < w)) \to φ$
19		simp1r	$⊢ ((((φ \land y \in ℝ^{+}) \land w \in ℝ^{+}) \land v \in A) \land ((v \neq D \land \|v - D\| < w) \to \|F (v) - C\| < y) \land (v \neq D \land \|v - D\| < w)) \to v \in A$
20		simp3	$⊢ ((((φ \land y \in ℝ^{+}) \land w \in ℝ^{+}) \land v \in A) \land ((v \neq D \land \|v - D\| < w) \to \|F (v) - C\| < y) \land (v \neq D \land \|v - D\| < w)) \to (v \neq D \land \|v - D\| < w)$
21		simp2	$⊢ ((((φ \land y \in ℝ^{+}) \land w \in ℝ^{+}) \land v \in A) \land ((v \neq D \land \|v - D\| < w) \to \|F (v) - C\| < y) \land (v \neq D \land \|v - D\| < w)) \to ((v \neq D \land \|v - D\| < w) \to \|F (v) - C\| < y)$
22	20 21	mpd	$⊢ ((((φ \land y \in ℝ^{+}) \land w \in ℝ^{+}) \land v \in A) \land ((v \neq D \land \|v - D\| < w) \to \|F (v) - C\| < y) \land (v \neq D \land \|v - D\| < w)) \to \|F (v) - C\| < y$
23		nfv	$⊢ Ⅎ x (φ \land v \in A)$
24		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ - B)$
25	2 24	nfcxfr	$⊢ \underline{Ⅎ} x G$
26		nfcv	$⊢ \underline{Ⅎ} x v$
27	25 26	nffv	$⊢ \underline{Ⅎ} x G (v)$
28		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B)$
29	1 28	nfcxfr	$⊢ \underline{Ⅎ} x F$
30	29 26	nffv	$⊢ \underline{Ⅎ} x F (v)$
31	30	nfneg	$⊢ \underline{Ⅎ} x (- F (v))$
32	27 31	nfeq	$⊢ Ⅎ x G (v) = - F (v)$
33	23 32	nfim	$⊢ Ⅎ x ((φ \land v \in A) \to G (v) = - F (v))$
34		eleq1w	$⊢ x = v \to (x \in A \leftrightarrow v \in A)$
35	34	anbi2d	$⊢ x = v \to ((φ \land x \in A) \leftrightarrow (φ \land v \in A))$
36		fveq2	$⊢ x = v \to G (x) = G (v)$
37		fveq2	$⊢ x = v \to F (x) = F (v)$
38	37	negeqd	$⊢ x = v \to - F (x) = - F (v)$
39	36 38	eqeq12d	$⊢ x = v \to (G (x) = - F (x) \leftrightarrow G (v) = - F (v))$
40	35 39	imbi12d	$⊢ x = v \to (((φ \land x \in A) \to G (x) = - F (x)) \leftrightarrow ((φ \land v \in A) \to G (v) = - F (v)))$
41		simpr	$⊢ (φ \land x \in A) \to x \in A$
42	3	negcld	$⊢ (φ \land x \in A) \to - B \in ℂ$
43	2	fvmpt2	$⊢ (x \in A \land - B \in ℂ) \to G (x) = - B$
44	41 42 43	syl2anc	$⊢ (φ \land x \in A) \to G (x) = - B$
45	1	fvmpt2	$⊢ (x \in A \land B \in ℂ) \to F (x) = B$
46	41 3 45	syl2anc	$⊢ (φ \land x \in A) \to F (x) = B$
47	46	negeqd	$⊢ (φ \land x \in A) \to - F (x) = - B$
48	44 47	eqtr4d	$⊢ (φ \land x \in A) \to G (x) = - F (x)$
49	33 40 48	chvarfv	$⊢ (φ \land v \in A) \to G (v) = - F (v)$
50	49	oveq1d	$⊢ (φ \land v \in A) \to G (v) - (- C) = - F (v) - (- C)$
51	8	ffvelrnda	$⊢ (φ \land v \in A) \to F (v) \in ℂ$
52	6	adantr	$⊢ (φ \land v \in A) \to C \in ℂ$
53	51 52	negsubdi3d	$⊢ (φ \land v \in A) \to - (F (v) - C) = - F (v) - (- C)$
54	50 53	eqtr4d	$⊢ (φ \land v \in A) \to G (v) - (- C) = - (F (v) - C)$
55	54	fveq2d	$⊢ (φ \land v \in A) \to \|G (v) - (- C)\| = \|- (F (v) - C)\|$
56	51 52	subcld	$⊢ (φ \land v \in A) \to F (v) - C \in ℂ$
57	56	absnegd	$⊢ (φ \land v \in A) \to \|- (F (v) - C)\| = \|F (v) - C\|$
58	55 57	eqtrd	$⊢ (φ \land v \in A) \to \|G (v) - (- C)\| = \|F (v) - C\|$
59	58	adantr	$⊢ ((φ \land v \in A) \land \|F (v) - C\| < y) \to \|G (v) - (- C)\| = \|F (v) - C\|$
60		simpr	$⊢ ((φ \land v \in A) \land \|F (v) - C\| < y) \to \|F (v) - C\| < y$
61	59 60	eqbrtrd	$⊢ ((φ \land v \in A) \land \|F (v) - C\| < y) \to \|G (v) - (- C)\| < y$
62	18 19 22 61	syl21anc	$⊢ ((((φ \land y \in ℝ^{+}) \land w \in ℝ^{+}) \land v \in A) \land ((v \neq D \land \|v - D\| < w) \to \|F (v) - C\| < y) \land (v \neq D \land \|v - D\| < w)) \to \|G (v) - (- C)\| < y$
63	62	3exp	$⊢ (((φ \land y \in ℝ^{+}) \land w \in ℝ^{+}) \land v \in A) \to (((v \neq D \land \|v - D\| < w) \to \|F (v) - C\| < y) \to ((v \neq D \land \|v - D\| < w) \to \|G (v) - (- C)\| < y))$
64	63	ralimdva	$⊢ ((φ \land y \in ℝ^{+}) \land w \in ℝ^{+}) \to (\forall v \in A ((v \neq D \land \|v - D\| < w) \to \|F (v) - C\| < y) \to \forall v \in A ((v \neq D \land \|v - D\| < w) \to \|G (v) - (- C)\| < y))$
65	64	reximdva	$⊢ (φ \land y \in ℝ^{+}) \to (\exists w \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < w) \to \|F (v) - C\| < y) \to \exists w \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < w) \to \|G (v) - (- C)\| < y))$
66	16 65	mpd	$⊢ (φ \land y \in ℝ^{+}) \to \exists w \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < w) \to \|G (v) - (- C)\| < y)$
67	66	ralrimiva	$⊢ φ \to \forall y \in ℝ^{+} \exists w \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < w) \to \|G (v) - (- C)\| < y)$
68	42 2	fmptd	$⊢ φ \to G : A ⟶ ℂ$
69	68 9 12	ellimc3	$⊢ φ \to (- C \in (G {lim}_{ℂ} D) \leftrightarrow (- C \in ℂ \land \forall y \in ℝ^{+} \exists w \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < w) \to \|G (v) - (- C)\| < y)))$
70	7 67 69	mpbir2and	$⊢ φ \to - C \in (G {lim}_{ℂ} D)$

Metamath Proof Explorer

Theorem neglimc

Proof