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

Metamath Proof Explorer

Theorem rlimeq

Proof