rlimeq

Description: Two functions that are eventually equal to one another have the same limit. (Contributed by Mario Carneiro, 16-Sep-2014)

	Ref	Expression
Hypotheses	rlimeq.1	$⊢ (φ \land x \in A) \to B \in ℂ$
	rlimeq.2	$⊢ (φ \land x \in A) \to C \in ℂ$
	rlimeq.3	$⊢ φ \to D \in ℝ$
	rlimeq.4	$⊢ (φ \land (x \in A \land D \leq x)) \to B = C$
Assertion	rlimeq	$⊢ φ \to ((x \in A ⟼ B) \underset{ℝ}{⇝} E \leftrightarrow (x \in A ⟼ C) \underset{ℝ}{⇝} E)$

Proof

Step	Hyp	Ref	Expression
1		rlimeq.1	$⊢ (φ \land x \in A) \to B \in ℂ$
2		rlimeq.2	$⊢ (φ \land x \in A) \to C \in ℂ$
3		rlimeq.3	$⊢ φ \to D \in ℝ$
4		rlimeq.4	$⊢ (φ \land (x \in A \land D \leq x)) \to B = C$
5		rlimss	$⊢ (x \in A ⟼ B) \underset{ℝ}{⇝} E \to dom (x \in A ⟼ B) \subseteq ℝ$
6		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
7	6 1	dmmptd	$⊢ φ \to dom (x \in A ⟼ B) = A$
8	7	sseq1d	$⊢ φ \to (dom (x \in A ⟼ B) \subseteq ℝ \leftrightarrow A \subseteq ℝ)$
9	5 8	imbitrid	$⊢ φ \to ((x \in A ⟼ B) \underset{ℝ}{⇝} E \to A \subseteq ℝ)$
10		rlimss	$⊢ (x \in A ⟼ C) \underset{ℝ}{⇝} E \to dom (x \in A ⟼ C) \subseteq ℝ$
11		eqid	$⊢ (x \in A ⟼ C) = (x \in A ⟼ C)$
12	11 2	dmmptd	$⊢ φ \to dom (x \in A ⟼ C) = A$
13	12	sseq1d	$⊢ φ \to (dom (x \in A ⟼ C) \subseteq ℝ \leftrightarrow A \subseteq ℝ)$
14	10 13	imbitrid	$⊢ φ \to ((x \in A ⟼ C) \underset{ℝ}{⇝} E \to A \subseteq ℝ)$
15		simpr	$⊢ (φ \land x \in (A \cap [D, +∞))) \to x \in (A \cap [D, +∞))$
16		elin	$⊢ x \in (A \cap [D, +∞)) \leftrightarrow (x \in A \land x \in [D, +∞))$
17	15 16	sylib	$⊢ (φ \land x \in (A \cap [D, +∞))) \to (x \in A \land x \in [D, +∞))$
18	17	simpld	$⊢ (φ \land x \in (A \cap [D, +∞))) \to x \in A$
19	17	simprd	$⊢ (φ \land x \in (A \cap [D, +∞))) \to x \in [D, +∞)$
20		elicopnf	$⊢ D \in ℝ \to (x \in [D, +∞) \leftrightarrow (x \in ℝ \land D \leq x))$
21	3 20	syl	$⊢ φ \to (x \in [D, +∞) \leftrightarrow (x \in ℝ \land D \leq x))$
22	21	biimpa	$⊢ (φ \land x \in [D, +∞)) \to (x \in ℝ \land D \leq x)$
23	19 22	syldan	$⊢ (φ \land x \in (A \cap [D, +∞))) \to (x \in ℝ \land D \leq x)$
24	23	simprd	$⊢ (φ \land x \in (A \cap [D, +∞))) \to D \leq x$
25	18 24	jca	$⊢ (φ \land x \in (A \cap [D, +∞))) \to (x \in A \land D \leq x)$
26	25 4	syldan	$⊢ (φ \land x \in (A \cap [D, +∞))) \to B = C$
27	26	mpteq2dva	$⊢ φ \to (x \in (A \cap [D, +∞)) ⟼ B) = (x \in (A \cap [D, +∞)) ⟼ C)$
28		inss1	$⊢ A \cap [D, +∞) \subseteq A$
29		resmpt	$⊢ A \cap [D, +∞) \subseteq A \to {(x \in A ⟼ B) ↾}_{(A \cap [D, +∞))} = (x \in (A \cap [D, +∞)) ⟼ B)$
30	28 29	ax-mp	$⊢ {(x \in A ⟼ B) ↾}_{(A \cap [D, +∞))} = (x \in (A \cap [D, +∞)) ⟼ B)$
31		resmpt	$⊢ A \cap [D, +∞) \subseteq A \to {(x \in A ⟼ C) ↾}_{(A \cap [D, +∞))} = (x \in (A \cap [D, +∞)) ⟼ C)$
32	28 31	ax-mp	$⊢ {(x \in A ⟼ C) ↾}_{(A \cap [D, +∞))} = (x \in (A \cap [D, +∞)) ⟼ C)$
33	27 30 32	3eqtr4g	$⊢ φ \to {(x \in A ⟼ B) ↾}_{(A \cap [D, +∞))} = {(x \in A ⟼ C) ↾}_{(A \cap [D, +∞))}$
34		resres	$⊢ {({(x \in A ⟼ B) ↾}_{A}) ↾}_{[D, +∞)} = {(x \in A ⟼ B) ↾}_{(A \cap [D, +∞))}$
35		resres	$⊢ {({(x \in A ⟼ C) ↾}_{A}) ↾}_{[D, +∞)} = {(x \in A ⟼ C) ↾}_{(A \cap [D, +∞))}$
36	33 34 35	3eqtr4g	$⊢ φ \to {({(x \in A ⟼ B) ↾}_{A}) ↾}_{[D, +∞)} = {({(x \in A ⟼ C) ↾}_{A}) ↾}_{[D, +∞)}$
37		ssid	$⊢ A \subseteq A$
38		resmpt	$⊢ A \subseteq A \to {(x \in A ⟼ B) ↾}_{A} = (x \in A ⟼ B)$
39		reseq1	$⊢ {(x \in A ⟼ B) ↾}_{A} = (x \in A ⟼ B) \to {({(x \in A ⟼ B) ↾}_{A}) ↾}_{[D, +∞)} = {(x \in A ⟼ B) ↾}_{[D, +∞)}$
40	37 38 39	mp2b	$⊢ {({(x \in A ⟼ B) ↾}_{A}) ↾}_{[D, +∞)} = {(x \in A ⟼ B) ↾}_{[D, +∞)}$
41		resmpt	$⊢ A \subseteq A \to {(x \in A ⟼ C) ↾}_{A} = (x \in A ⟼ C)$
42		reseq1	$⊢ {(x \in A ⟼ C) ↾}_{A} = (x \in A ⟼ C) \to {({(x \in A ⟼ C) ↾}_{A}) ↾}_{[D, +∞)} = {(x \in A ⟼ C) ↾}_{[D, +∞)}$
43	37 41 42	mp2b	$⊢ {({(x \in A ⟼ C) ↾}_{A}) ↾}_{[D, +∞)} = {(x \in A ⟼ C) ↾}_{[D, +∞)}$
44	36 40 43	3eqtr3g	$⊢ φ \to {(x \in A ⟼ B) ↾}_{[D, +∞)} = {(x \in A ⟼ C) ↾}_{[D, +∞)}$
45	44	breq1d	$⊢ φ \to (({(x \in A ⟼ B) ↾}_{[D, +∞)}) \underset{ℝ}{⇝} E \leftrightarrow ({(x \in A ⟼ C) ↾}_{[D, +∞)}) \underset{ℝ}{⇝} E)$
46	45	adantr	$⊢ (φ \land A \subseteq ℝ) \to (({(x \in A ⟼ B) ↾}_{[D, +∞)}) \underset{ℝ}{⇝} E \leftrightarrow ({(x \in A ⟼ C) ↾}_{[D, +∞)}) \underset{ℝ}{⇝} E)$
47	1	fmpttd	$⊢ φ \to (x \in A ⟼ B) : A ⟶ ℂ$
48	47	adantr	$⊢ (φ \land A \subseteq ℝ) \to (x \in A ⟼ B) : A ⟶ ℂ$
49		simpr	$⊢ (φ \land A \subseteq ℝ) \to A \subseteq ℝ$
50	3	adantr	$⊢ (φ \land A \subseteq ℝ) \to D \in ℝ$
51	48 49 50	rlimresb	$⊢ (φ \land A \subseteq ℝ) \to ((x \in A ⟼ B) \underset{ℝ}{⇝} E \leftrightarrow ({(x \in A ⟼ B) ↾}_{[D, +∞)}) \underset{ℝ}{⇝} E)$
52	2	fmpttd	$⊢ φ \to (x \in A ⟼ C) : A ⟶ ℂ$
53	52	adantr	$⊢ (φ \land A \subseteq ℝ) \to (x \in A ⟼ C) : A ⟶ ℂ$
54	53 49 50	rlimresb	$⊢ (φ \land A \subseteq ℝ) \to ((x \in A ⟼ C) \underset{ℝ}{⇝} E \leftrightarrow ({(x \in A ⟼ C) ↾}_{[D, +∞)}) \underset{ℝ}{⇝} E)$
55	46 51 54	3bitr4d	$⊢ (φ \land A \subseteq ℝ) \to ((x \in A ⟼ B) \underset{ℝ}{⇝} E \leftrightarrow (x \in A ⟼ C) \underset{ℝ}{⇝} E)$
56	55	ex	$⊢ φ \to (A \subseteq ℝ \to ((x \in A ⟼ B) \underset{ℝ}{⇝} E \leftrightarrow (x \in A ⟼ C) \underset{ℝ}{⇝} E))$
57	9 14 56	pm5.21ndd	$⊢ φ \to ((x \in A ⟼ B) \underset{ℝ}{⇝} E \leftrightarrow (x \in A ⟼ C) \underset{ℝ}{⇝} E)$

Metamath Proof Explorer

Theorem rlimeq

Proof