limcresiooub

Description: The left limit doesn't change if the function is restricted to a smaller open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	limcresiooub.f	$⊢ φ \to F : A ⟶ ℂ$
	limcresiooub.b	$⊢ φ \to B \in ℝ^{*}$
	limcresiooub.c	$⊢ φ \to C \in ℝ$
	limcresiooub.bltc	$⊢ φ \to B < C$
	limcresiooub.bcss	$⊢ φ \to (B, C) \subseteq A$
	limcresiooub.d	$⊢ φ \to D \in ℝ^{*}$
	limcresiooub.cled	$⊢ φ \to D \leq B$
Assertion	limcresiooub	$⊢ φ \to ({F ↾}_{(B, C)}) {lim}_{ℂ} C = ({F ↾}_{(D, C)}) {lim}_{ℂ} C$

Proof

Step	Hyp	Ref	Expression
1		limcresiooub.f	$⊢ φ \to F : A ⟶ ℂ$
2		limcresiooub.b	$⊢ φ \to B \in ℝ^{*}$
3		limcresiooub.c	$⊢ φ \to C \in ℝ$
4		limcresiooub.bltc	$⊢ φ \to B < C$
5		limcresiooub.bcss	$⊢ φ \to (B, C) \subseteq A$
6		limcresiooub.d	$⊢ φ \to D \in ℝ^{*}$
7		limcresiooub.cled	$⊢ φ \to D \leq B$
8		iooss1	$⊢ (D \in ℝ^{*} \land D \leq B) \to (B, C) \subseteq (D, C)$
9	6 7 8	syl2anc	$⊢ φ \to (B, C) \subseteq (D, C)$
10	9	resabs1d	$⊢ φ \to {({F ↾}_{(D, C)}) ↾}_{(B, C)} = {F ↾}_{(B, C)}$
11	10	eqcomd	$⊢ φ \to {F ↾}_{(B, C)} = {({F ↾}_{(D, C)}) ↾}_{(B, C)}$
12	11	oveq1d	$⊢ φ \to ({F ↾}_{(B, C)}) {lim}_{ℂ} C = ({({F ↾}_{(D, C)}) ↾}_{(B, C)}) {lim}_{ℂ} C$
13		fresin	$⊢ F : A ⟶ ℂ \to ({F ↾}_{(D, C)}) : A \cap (D, C) ⟶ ℂ$
14	1 13	syl	$⊢ φ \to ({F ↾}_{(D, C)}) : A \cap (D, C) ⟶ ℂ$
15	5 9	ssind	$⊢ φ \to (B, C) \subseteq A \cap (D, C)$
16		inss2	$⊢ A \cap (D, C) \subseteq (D, C)$
17		ioosscn	$⊢ (D, C) \subseteq ℂ$
18	16 17	sstri	$⊢ A \cap (D, C) \subseteq ℂ$
19	18	a1i	$⊢ φ \to A \cap (D, C) \subseteq ℂ$
20		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
21		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (D, C)) \cup \{C\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (D, C)) \cup \{C\})$
22	3	rexrd	$⊢ φ \to C \in ℝ^{*}$
23		ubioc1	$⊢ (B \in ℝ^{} \land C \in ℝ^{} \land B < C) \to C \in (B, C]$
24	2 22 4 23	syl3anc	$⊢ φ \to C \in (B, C]$
25		ioounsn	$⊢ (B \in ℝ^{} \land C \in ℝ^{} \land B < C) \to (B, C) \cup \{C\} = (B, C]$
26	2 22 4 25	syl3anc	$⊢ φ \to (B, C) \cup \{C\} = (B, C]$
27	26	fveq2d	$⊢ φ \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (D, C)) \cup \{C\})) ((B, C) \cup \{C\}) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (D, C)) \cup \{C\})) ((B, C])$
28	20	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
29		ovex	$⊢ (D, C) \in V$
30	29	inex2	$⊢ A \cap (D, C) \in V$
31		snex	$⊢ \{C\} \in V$
32	30 31	unex	$⊢ (A \cap (D, C)) \cup \{C\} \in V$
33		resttop	$⊢ (TopOpen (ℂ_{fld}) \in Top \land (A \cap (D, C)) \cup \{C\} \in V) \to TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (D, C)) \cup \{C\}) \in Top$
34	28 32 33	mp2an	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (D, C)) \cup \{C\}) \in Top$
35	34	a1i	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (D, C)) \cup \{C\}) \in Top$
36		pnfxr	$⊢ +∞ \in ℝ^{*}$
37	36	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
38	2	xrleidd	$⊢ φ \to B \leq B$
39	3	ltpnfd	$⊢ φ \to C < +∞$
40		iocssioo	$⊢ ((B \in ℝ^{} \land +∞ \in ℝ^{}) \land (B \leq B \land C < +∞)) \to (B, C] \subseteq (B, +∞)$
41	2 37 38 39 40	syl22anc	$⊢ φ \to (B, C] \subseteq (B, +∞)$
42		simpr	$⊢ (φ \land x = C) \to x = C$
43		snidg	$⊢ C \in ℝ \to C \in \{C\}$
44		elun2	$⊢ C \in \{C\} \to C \in ((A \cap (D, C)) \cup \{C\})$
45	3 43 44	3syl	$⊢ φ \to C \in ((A \cap (D, C)) \cup \{C\})$
46	45	adantr	$⊢ (φ \land x = C) \to C \in ((A \cap (D, C)) \cup \{C\})$
47	42 46	eqeltrd	$⊢ (φ \land x = C) \to x \in ((A \cap (D, C)) \cup \{C\})$
48	47	adantlr	$⊢ ((φ \land x \in (B, C]) \land x = C) \to x \in ((A \cap (D, C)) \cup \{C\})$
49		simpll	$⊢ ((φ \land x \in (B, C]) \land \neg x = C) \to φ$
50	2	adantr	$⊢ (φ \land x \in (B, C]) \to B \in ℝ^{*}$
51	50	adantr	$⊢ ((φ \land x \in (B, C]) \land \neg x = C) \to B \in ℝ^{*}$
52	22	adantr	$⊢ (φ \land x \in (B, C]) \to C \in ℝ^{*}$
53	52	adantr	$⊢ ((φ \land x \in (B, C]) \land \neg x = C) \to C \in ℝ^{*}$
54		iocssre	$⊢ (B \in ℝ^{*} \land C \in ℝ) \to (B, C] \subseteq ℝ$
55	2 3 54	syl2anc	$⊢ φ \to (B, C] \subseteq ℝ$
56	55	sselda	$⊢ (φ \land x \in (B, C]) \to x \in ℝ$
57	56	adantr	$⊢ ((φ \land x \in (B, C]) \land \neg x = C) \to x \in ℝ$
58		simpr	$⊢ (φ \land x \in (B, C]) \to x \in (B, C]$
59		iocgtlb	$⊢ (B \in ℝ^{} \land C \in ℝ^{} \land x \in (B, C]) \to B < x$
60	50 52 58 59	syl3anc	$⊢ (φ \land x \in (B, C]) \to B < x$
61	60	adantr	$⊢ ((φ \land x \in (B, C]) \land \neg x = C) \to B < x$
62	3	ad2antrr	$⊢ ((φ \land x \in (B, C]) \land \neg x = C) \to C \in ℝ$
63		iocleub	$⊢ (B \in ℝ^{} \land C \in ℝ^{} \land x \in (B, C]) \to x \leq C$
64	50 52 58 63	syl3anc	$⊢ (φ \land x \in (B, C]) \to x \leq C$
65	64	adantr	$⊢ ((φ \land x \in (B, C]) \land \neg x = C) \to x \leq C$
66		neqne	$⊢ \neg x = C \to x \neq C$
67	66	adantl	$⊢ ((φ \land x \in (B, C]) \land \neg x = C) \to x \neq C$
68	67	necomd	$⊢ ((φ \land x \in (B, C]) \land \neg x = C) \to C \neq x$
69	57 62 65 68	leneltd	$⊢ ((φ \land x \in (B, C]) \land \neg x = C) \to x < C$
70	51 53 57 61 69	eliood	$⊢ ((φ \land x \in (B, C]) \land \neg x = C) \to x \in (B, C)$
71	15	sselda	$⊢ (φ \land x \in (B, C)) \to x \in (A \cap (D, C))$
72		elun1	$⊢ x \in (A \cap (D, C)) \to x \in ((A \cap (D, C)) \cup \{C\})$
73	71 72	syl	$⊢ (φ \land x \in (B, C)) \to x \in ((A \cap (D, C)) \cup \{C\})$
74	49 70 73	syl2anc	$⊢ ((φ \land x \in (B, C]) \land \neg x = C) \to x \in ((A \cap (D, C)) \cup \{C\})$
75	48 74	pm2.61dan	$⊢ (φ \land x \in (B, C]) \to x \in ((A \cap (D, C)) \cup \{C\})$
76	75	ralrimiva	$⊢ φ \to \forall x \in (B, C] x \in ((A \cap (D, C)) \cup \{C\})$
77		dfss3	$⊢ (B, C] \subseteq (A \cap (D, C)) \cup \{C\} \leftrightarrow \forall x \in (B, C] x \in ((A \cap (D, C)) \cup \{C\})$
78	76 77	sylibr	$⊢ φ \to (B, C] \subseteq (A \cap (D, C)) \cup \{C\}$
79	41 78	ssind	$⊢ φ \to (B, C] \subseteq (B, +∞) \cap ((A \cap (D, C)) \cup \{C\})$
80	79	sseld	$⊢ φ \to (x \in (B, C] \to x \in ((B, +∞) \cap ((A \cap (D, C)) \cup \{C\})))$
81	24	adantr	$⊢ (φ \land x = C) \to C \in (B, C]$
82	42 81	eqeltrd	$⊢ (φ \land x = C) \to x \in (B, C]$
83	82	adantlr	$⊢ ((φ \land x \in ((B, +∞) \cap ((A \cap (D, C)) \cup \{C\}))) \land x = C) \to x \in (B, C]$
84		ioossioc	$⊢ (B, C) \subseteq (B, C]$
85	2	ad2antrr	$⊢ ((φ \land x \in ((B, +∞) \cap ((A \cap (D, C)) \cup \{C\}))) \land \neg x = C) \to B \in ℝ^{*}$
86	22	ad2antrr	$⊢ ((φ \land x \in ((B, +∞) \cap ((A \cap (D, C)) \cup \{C\}))) \land \neg x = C) \to C \in ℝ^{*}$
87		elinel1	$⊢ x \in ((B, +∞) \cap ((A \cap (D, C)) \cup \{C\})) \to x \in (B, +∞)$
88	87	elioored	$⊢ x \in ((B, +∞) \cap ((A \cap (D, C)) \cup \{C\})) \to x \in ℝ$
89	88	ad2antlr	$⊢ ((φ \land x \in ((B, +∞) \cap ((A \cap (D, C)) \cup \{C\}))) \land \neg x = C) \to x \in ℝ$
90	36	a1i	$⊢ ((φ \land x \in ((B, +∞) \cap ((A \cap (D, C)) \cup \{C\}))) \land \neg x = C) \to +∞ \in ℝ^{*}$
91	87	ad2antlr	$⊢ ((φ \land x \in ((B, +∞) \cap ((A \cap (D, C)) \cup \{C\}))) \land \neg x = C) \to x \in (B, +∞)$
92		ioogtlb	$⊢ (B \in ℝ^{} \land +∞ \in ℝ^{} \land x \in (B, +∞)) \to B < x$
93	85 90 91 92	syl3anc	$⊢ ((φ \land x \in ((B, +∞) \cap ((A \cap (D, C)) \cup \{C\}))) \land \neg x = C) \to B < x$
94	6	ad2antrr	$⊢ ((φ \land x \in ((B, +∞) \cap ((A \cap (D, C)) \cup \{C\}))) \land \neg x = C) \to D \in ℝ^{*}$
95		elinel2	$⊢ x \in ((B, +∞) \cap ((A \cap (D, C)) \cup \{C\})) \to x \in ((A \cap (D, C)) \cup \{C\})$
96		id	$⊢ \neg x = C \to \neg x = C$
97		velsn	$⊢ x \in \{C\} \leftrightarrow x = C$
98	96 97	sylnibr	$⊢ \neg x = C \to \neg x \in \{C\}$
99		elunnel2	$⊢ (x \in ((A \cap (D, C)) \cup \{C\}) \land \neg x \in \{C\}) \to x \in (A \cap (D, C))$
100	95 98 99	syl2an	$⊢ (x \in ((B, +∞) \cap ((A \cap (D, C)) \cup \{C\})) \land \neg x = C) \to x \in (A \cap (D, C))$
101	16 100	sselid	$⊢ (x \in ((B, +∞) \cap ((A \cap (D, C)) \cup \{C\})) \land \neg x = C) \to x \in (D, C)$
102	101	adantll	$⊢ ((φ \land x \in ((B, +∞) \cap ((A \cap (D, C)) \cup \{C\}))) \land \neg x = C) \to x \in (D, C)$
103		iooltub	$⊢ (D \in ℝ^{} \land C \in ℝ^{} \land x \in (D, C)) \to x < C$
104	94 86 102 103	syl3anc	$⊢ ((φ \land x \in ((B, +∞) \cap ((A \cap (D, C)) \cup \{C\}))) \land \neg x = C) \to x < C$
105	85 86 89 93 104	eliood	$⊢ ((φ \land x \in ((B, +∞) \cap ((A \cap (D, C)) \cup \{C\}))) \land \neg x = C) \to x \in (B, C)$
106	84 105	sselid	$⊢ ((φ \land x \in ((B, +∞) \cap ((A \cap (D, C)) \cup \{C\}))) \land \neg x = C) \to x \in (B, C]$
107	83 106	pm2.61dan	$⊢ (φ \land x \in ((B, +∞) \cap ((A \cap (D, C)) \cup \{C\}))) \to x \in (B, C]$
108	107	ex	$⊢ φ \to (x \in ((B, +∞) \cap ((A \cap (D, C)) \cup \{C\})) \to x \in (B, C])$
109	80 108	impbid	$⊢ φ \to (x \in (B, C] \leftrightarrow x \in ((B, +∞) \cap ((A \cap (D, C)) \cup \{C\})))$
110	109	eqrdv	$⊢ φ \to (B, C] = (B, +∞) \cap ((A \cap (D, C)) \cup \{C\})$
111		retop	$⊢ topGen (ran (.)) \in Top$
112	111	a1i	$⊢ φ \to topGen (ran (.)) \in Top$
113	32	a1i	$⊢ φ \to (A \cap (D, C)) \cup \{C\} \in V$
114		iooretop	$⊢ (B, +∞) \in topGen (ran (.))$
115	114	a1i	$⊢ φ \to (B, +∞) \in topGen (ran (.))$
116		elrestr	$⊢ (topGen (ran (.)) \in Top \land (A \cap (D, C)) \cup \{C\} \in V \land (B, +∞) \in topGen (ran (.))) \to (B, +∞) \cap ((A \cap (D, C)) \cup \{C\}) \in (topGen (ran (.)) ↾_{𝑡} ((A \cap (D, C)) \cup \{C\}))$
117	112 113 115 116	syl3anc	$⊢ φ \to (B, +∞) \cap ((A \cap (D, C)) \cup \{C\}) \in (topGen (ran (.)) ↾_{𝑡} ((A \cap (D, C)) \cup \{C\}))$
118	110 117	eqeltrd	$⊢ φ \to (B, C] \in (topGen (ran (.)) ↾_{𝑡} ((A \cap (D, C)) \cup \{C\}))$
119		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
120	119	oveq1i	$⊢ topGen (ran (.)) ↾_{𝑡} ((A \cap (D, C)) \cup \{C\}) = (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} ((A \cap (D, C)) \cup \{C\})$
121	28	a1i	$⊢ φ \to TopOpen (ℂ_{fld}) \in Top$
122		ioossre	$⊢ (D, C) \subseteq ℝ$
123	16 122	sstri	$⊢ A \cap (D, C) \subseteq ℝ$
124	123	a1i	$⊢ φ \to A \cap (D, C) \subseteq ℝ$
125	3	snssd	$⊢ φ \to \{C\} \subseteq ℝ$
126	124 125	unssd	$⊢ φ \to (A \cap (D, C)) \cup \{C\} \subseteq ℝ$
127		reex	$⊢ ℝ \in V$
128	127	a1i	$⊢ φ \to ℝ \in V$
129		restabs	$⊢ (TopOpen (ℂ_{fld}) \in Top \land (A \cap (D, C)) \cup \{C\} \subseteq ℝ \land ℝ \in V) \to (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} ((A \cap (D, C)) \cup \{C\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (D, C)) \cup \{C\})$
130	121 126 128 129	syl3anc	$⊢ φ \to (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} ((A \cap (D, C)) \cup \{C\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (D, C)) \cup \{C\})$
131	120 130	eqtrid	$⊢ φ \to topGen (ran (.)) ↾_{𝑡} ((A \cap (D, C)) \cup \{C\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (D, C)) \cup \{C\})$
132	118 131	eleqtrd	$⊢ φ \to (B, C] \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (D, C)) \cup \{C\}))$
133		isopn3i	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (D, C)) \cup \{C\}) \in Top \land (B, C] \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (D, C)) \cup \{C\}))) \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (D, C)) \cup \{C\})) ((B, C]) = (B, C]$
134	35 132 133	syl2anc	$⊢ φ \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (D, C)) \cup \{C\})) ((B, C]) = (B, C]$
135	27 134	eqtr2d	$⊢ φ \to (B, C] = int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (D, C)) \cup \{C\})) ((B, C) \cup \{C\})$
136	24 135	eleqtrd	$⊢ φ \to C \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A \cap (D, C)) \cup \{C\})) ((B, C) \cup \{C\})$
137	14 15 19 20 21 136	limcres	$⊢ φ \to ({({F ↾}_{(D, C)}) ↾}_{(B, C)}) {lim}_{ℂ} C = ({F ↾}_{(D, C)}) {lim}_{ℂ} C$
138	12 137	eqtrd	$⊢ φ \to ({F ↾}_{(B, C)}) {lim}_{ℂ} C = ({F ↾}_{(D, C)}) {lim}_{ℂ} C$

Metamath Proof Explorer

Theorem limcresiooub

Proof