fourierdlem32

Description: Limit of a continuous function on an open subinterval. Lower bound version. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem32.a	$⊢ φ \to A \in ℝ$
	fourierdlem32.b	$⊢ φ \to B \in ℝ$
	fourierdlem32.altb	$⊢ φ \to A < B$
	fourierdlem32.f	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℂ$
	fourierdlem32.l	$⊢ φ \to R \in (F {lim}_{ℂ} A)$
	fourierdlem32.c	$⊢ φ \to C \in ℝ$
	fourierdlem32.d	$⊢ φ \to D \in ℝ$
	fourierdlem32.cltd	$⊢ φ \to C < D$
	fourierdlem32.ss	$⊢ φ \to (C, D) \subseteq (A, B)$
	fourierdlem32.y	$⊢ Y = if (C = A, R, F (C))$
	fourierdlem32.j	$⊢ J = TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B)$
Assertion	fourierdlem32	$⊢ φ \to Y \in (({F ↾}_{(C, D)}) {lim}_{ℂ} C)$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem32.a	$⊢ φ \to A \in ℝ$
2		fourierdlem32.b	$⊢ φ \to B \in ℝ$
3		fourierdlem32.altb	$⊢ φ \to A < B$
4		fourierdlem32.f	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℂ$
5		fourierdlem32.l	$⊢ φ \to R \in (F {lim}_{ℂ} A)$
6		fourierdlem32.c	$⊢ φ \to C \in ℝ$
7		fourierdlem32.d	$⊢ φ \to D \in ℝ$
8		fourierdlem32.cltd	$⊢ φ \to C < D$
9		fourierdlem32.ss	$⊢ φ \to (C, D) \subseteq (A, B)$
10		fourierdlem32.y	$⊢ Y = if (C = A, R, F (C))$
11		fourierdlem32.j	$⊢ J = TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B)$
12	5	adantr	$⊢ (φ \land C = A) \to R \in (F {lim}_{ℂ} A)$
13		iftrue	$⊢ C = A \to if (C = A, R, F (C)) = R$
14	10 13	eqtr2id	$⊢ C = A \to R = Y$
15	14	adantl	$⊢ (φ \land C = A) \to R = Y$
16		oveq2	$⊢ C = A \to ({F ↾}_{(C, D)}) {lim}_{ℂ} C = ({F ↾}_{(C, D)}) {lim}_{ℂ} A$
17	16	adantl	$⊢ (φ \land C = A) \to ({F ↾}_{(C, D)}) {lim}_{ℂ} C = ({F ↾}_{(C, D)}) {lim}_{ℂ} A$
18		cncff	$⊢ F : (A, B) \underset{cn}{⟶} ℂ \to F : (A, B) ⟶ ℂ$
19	4 18	syl	$⊢ φ \to F : (A, B) ⟶ ℂ$
20	19	adantr	$⊢ (φ \land C = A) \to F : (A, B) ⟶ ℂ$
21	9	adantr	$⊢ (φ \land C = A) \to (C, D) \subseteq (A, B)$
22		ioosscn	$⊢ (A, B) \subseteq ℂ$
23	22	a1i	$⊢ (φ \land C = A) \to (A, B) \subseteq ℂ$
24		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
25		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B) \cup \{A\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B) \cup \{A\})$
26	6	leidd	$⊢ φ \to C \leq C$
27	7	rexrd	$⊢ φ \to D \in ℝ^{*}$
28		elico2	$⊢ (C \in ℝ \land D \in ℝ^{*}) \to (C \in [C, D) \leftrightarrow (C \in ℝ \land C \leq C \land C < D))$
29	6 27 28	syl2anc	$⊢ φ \to (C \in [C, D) \leftrightarrow (C \in ℝ \land C \leq C \land C < D))$
30	6 26 8 29	mpbir3and	$⊢ φ \to C \in [C, D)$
31	30	adantr	$⊢ (φ \land C = A) \to C \in [C, D)$
32	24	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
33		ovex	$⊢ [A, B) \in V$
34	33	a1i	$⊢ (φ \land C = A) \to [A, B) \in V$
35		resttop	$⊢ (TopOpen (ℂ_{fld}) \in Top \land [A, B) \in V) \to TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B) \in Top$
36	32 34 35	sylancr	$⊢ (φ \land C = A) \to TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B) \in Top$
37	11 36	eqeltrid	$⊢ (φ \land C = A) \to J \in Top$
38		mnfxr	$⊢ −∞ \in ℝ^{*}$
39	38	a1i	$⊢ (φ \land x \in [A, D)) \to −∞ \in ℝ^{*}$
40	27	adantr	$⊢ (φ \land x \in [A, D)) \to D \in ℝ^{*}$
41		simpr	$⊢ (φ \land x \in [A, D)) \to x \in [A, D)$
42	1	adantr	$⊢ (φ \land x \in [A, D)) \to A \in ℝ$
43		elico2	$⊢ (A \in ℝ \land D \in ℝ^{*}) \to (x \in [A, D) \leftrightarrow (x \in ℝ \land A \leq x \land x < D))$
44	42 40 43	syl2anc	$⊢ (φ \land x \in [A, D)) \to (x \in [A, D) \leftrightarrow (x \in ℝ \land A \leq x \land x < D))$
45	41 44	mpbid	$⊢ (φ \land x \in [A, D)) \to (x \in ℝ \land A \leq x \land x < D)$
46	45	simp1d	$⊢ (φ \land x \in [A, D)) \to x \in ℝ$
47	46	mnfltd	$⊢ (φ \land x \in [A, D)) \to −∞ < x$
48	45	simp3d	$⊢ (φ \land x \in [A, D)) \to x < D$
49	39 40 46 47 48	eliood	$⊢ (φ \land x \in [A, D)) \to x \in (−∞, D)$
50	45	simp2d	$⊢ (φ \land x \in [A, D)) \to A \leq x$
51	7	adantr	$⊢ (φ \land x \in [A, D)) \to D \in ℝ$
52	2	adantr	$⊢ (φ \land x \in [A, D)) \to B \in ℝ$
53	1 2 6 7 8 9	fourierdlem10	$⊢ φ \to (A \leq C \land D \leq B)$
54	53	simprd	$⊢ φ \to D \leq B$
55	54	adantr	$⊢ (φ \land x \in [A, D)) \to D \leq B$
56	46 51 52 48 55	ltletrd	$⊢ (φ \land x \in [A, D)) \to x < B$
57	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
58	57	adantr	$⊢ (φ \land x \in [A, D)) \to B \in ℝ^{*}$
59		elico2	$⊢ (A \in ℝ \land B \in ℝ^{*}) \to (x \in [A, B) \leftrightarrow (x \in ℝ \land A \leq x \land x < B))$
60	42 58 59	syl2anc	$⊢ (φ \land x \in [A, D)) \to (x \in [A, B) \leftrightarrow (x \in ℝ \land A \leq x \land x < B))$
61	46 50 56 60	mpbir3and	$⊢ (φ \land x \in [A, D)) \to x \in [A, B)$
62	49 61	elind	$⊢ (φ \land x \in [A, D)) \to x \in ((−∞, D) \cap [A, B))$
63		elinel1	$⊢ x \in ((−∞, D) \cap [A, B)) \to x \in (−∞, D)$
64		elioore	$⊢ x \in (−∞, D) \to x \in ℝ$
65	63 64	syl	$⊢ x \in ((−∞, D) \cap [A, B)) \to x \in ℝ$
66	65	adantl	$⊢ (φ \land x \in ((−∞, D) \cap [A, B))) \to x \in ℝ$
67		elinel2	$⊢ x \in ((−∞, D) \cap [A, B)) \to x \in [A, B)$
68	67	adantl	$⊢ (φ \land x \in ((−∞, D) \cap [A, B))) \to x \in [A, B)$
69	1	adantr	$⊢ (φ \land x \in ((−∞, D) \cap [A, B))) \to A \in ℝ$
70	57	adantr	$⊢ (φ \land x \in ((−∞, D) \cap [A, B))) \to B \in ℝ^{*}$
71	69 70 59	syl2anc	$⊢ (φ \land x \in ((−∞, D) \cap [A, B))) \to (x \in [A, B) \leftrightarrow (x \in ℝ \land A \leq x \land x < B))$
72	68 71	mpbid	$⊢ (φ \land x \in ((−∞, D) \cap [A, B))) \to (x \in ℝ \land A \leq x \land x < B)$
73	72	simp2d	$⊢ (φ \land x \in ((−∞, D) \cap [A, B))) \to A \leq x$
74	63	adantl	$⊢ (φ \land x \in ((−∞, D) \cap [A, B))) \to x \in (−∞, D)$
75	27	adantr	$⊢ (φ \land x \in ((−∞, D) \cap [A, B))) \to D \in ℝ^{*}$
76		elioo2	$⊢ (−∞ \in ℝ^{} \land D \in ℝ^{}) \to (x \in (−∞, D) \leftrightarrow (x \in ℝ \land −∞ < x \land x < D))$
77	38 75 76	sylancr	$⊢ (φ \land x \in ((−∞, D) \cap [A, B))) \to (x \in (−∞, D) \leftrightarrow (x \in ℝ \land −∞ < x \land x < D))$
78	74 77	mpbid	$⊢ (φ \land x \in ((−∞, D) \cap [A, B))) \to (x \in ℝ \land −∞ < x \land x < D)$
79	78	simp3d	$⊢ (φ \land x \in ((−∞, D) \cap [A, B))) \to x < D$
80	69 75 43	syl2anc	$⊢ (φ \land x \in ((−∞, D) \cap [A, B))) \to (x \in [A, D) \leftrightarrow (x \in ℝ \land A \leq x \land x < D))$
81	66 73 79 80	mpbir3and	$⊢ (φ \land x \in ((−∞, D) \cap [A, B))) \to x \in [A, D)$
82	62 81	impbida	$⊢ φ \to (x \in [A, D) \leftrightarrow x \in ((−∞, D) \cap [A, B)))$
83	82	eqrdv	$⊢ φ \to [A, D) = (−∞, D) \cap [A, B)$
84		retop	$⊢ topGen (ran (.)) \in Top$
85	84	a1i	$⊢ φ \to topGen (ran (.)) \in Top$
86	33	a1i	$⊢ φ \to [A, B) \in V$
87		iooretop	$⊢ (−∞, D) \in topGen (ran (.))$
88	87	a1i	$⊢ φ \to (−∞, D) \in topGen (ran (.))$
89		elrestr	$⊢ (topGen (ran (.)) \in Top \land [A, B) \in V \land (−∞, D) \in topGen (ran (.))) \to (−∞, D) \cap [A, B) \in (topGen (ran (.)) ↾_{𝑡} [A, B))$
90	85 86 88 89	syl3anc	$⊢ φ \to (−∞, D) \cap [A, B) \in (topGen (ran (.)) ↾_{𝑡} [A, B))$
91	83 90	eqeltrd	$⊢ φ \to [A, D) \in (topGen (ran (.)) ↾_{𝑡} [A, B))$
92	91	adantr	$⊢ (φ \land C = A) \to [A, D) \in (topGen (ran (.)) ↾_{𝑡} [A, B))$
93		simpr	$⊢ (φ \land C = A) \to C = A$
94	93	oveq1d	$⊢ (φ \land C = A) \to [C, D) = [A, D)$
95	11	a1i	$⊢ φ \to J = TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B)$
96	32	a1i	$⊢ φ \to TopOpen (ℂ_{fld}) \in Top$
97		icossre	$⊢ (A \in ℝ \land B \in ℝ^{*}) \to [A, B) \subseteq ℝ$
98	1 57 97	syl2anc	$⊢ φ \to [A, B) \subseteq ℝ$
99		reex	$⊢ ℝ \in V$
100	99	a1i	$⊢ φ \to ℝ \in V$
101		restabs	$⊢ (TopOpen (ℂ_{fld}) \in Top \land [A, B) \subseteq ℝ \land ℝ \in V) \to (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} [A, B) = TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B)$
102	96 98 100 101	syl3anc	$⊢ φ \to (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} [A, B) = TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B)$
103	24	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
104	103	eqcomi	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ = topGen (ran (.))$
105	104	oveq1i	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} [A, B) = topGen (ran (.)) ↾_{𝑡} [A, B)$
106	105	a1i	$⊢ φ \to (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} [A, B) = topGen (ran (.)) ↾_{𝑡} [A, B)$
107	95 102 106	3eqtr2d	$⊢ φ \to J = topGen (ran (.)) ↾_{𝑡} [A, B)$
108	107	adantr	$⊢ (φ \land C = A) \to J = topGen (ran (.)) ↾_{𝑡} [A, B)$
109	92 94 108	3eltr4d	$⊢ (φ \land C = A) \to [C, D) \in J$
110		isopn3i	$⊢ (J \in Top \land [C, D) \in J) \to int (J) ([C, D)) = [C, D)$
111	37 109 110	syl2anc	$⊢ (φ \land C = A) \to int (J) ([C, D)) = [C, D)$
112	31 111	eleqtrrd	$⊢ (φ \land C = A) \to C \in int (J) ([C, D))$
113		id	$⊢ C = A \to C = A$
114	113	eqcomd	$⊢ C = A \to A = C$
115	114	adantl	$⊢ (φ \land C = A) \to A = C$
116		uncom	$⊢ (A, B) \cup \{A\} = \{A\} \cup (A, B)$
117	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
118		snunioo	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to \{A\} \cup (A, B) = [A, B)$
119	117 57 3 118	syl3anc	$⊢ φ \to \{A\} \cup (A, B) = [A, B)$
120	116 119	eqtrid	$⊢ φ \to (A, B) \cup \{A\} = [A, B)$
121	120	adantr	$⊢ (φ \land C = A) \to (A, B) \cup \{A\} = [A, B)$
122	121	oveq2d	$⊢ (φ \land C = A) \to TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B) \cup \{A\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B)$
123	122 11	eqtr4di	$⊢ (φ \land C = A) \to TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B) \cup \{A\}) = J$
124	123	fveq2d	$⊢ (φ \land C = A) \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B) \cup \{A\})) = int (J)$
125		uncom	$⊢ (C, D) \cup \{A\} = \{A\} \cup (C, D)$
126		sneq	$⊢ C = A \to \{C\} = \{A\}$
127	126	eqcomd	$⊢ C = A \to \{A\} = \{C\}$
128	127	uneq1d	$⊢ C = A \to \{A\} \cup (C, D) = \{C\} \cup (C, D)$
129	125 128	eqtrid	$⊢ C = A \to (C, D) \cup \{A\} = \{C\} \cup (C, D)$
130	6	rexrd	$⊢ φ \to C \in ℝ^{*}$
131		snunioo	$⊢ (C \in ℝ^{} \land D \in ℝ^{} \land C < D) \to \{C\} \cup (C, D) = [C, D)$
132	130 27 8 131	syl3anc	$⊢ φ \to \{C\} \cup (C, D) = [C, D)$
133	129 132	sylan9eqr	$⊢ (φ \land C = A) \to (C, D) \cup \{A\} = [C, D)$
134	124 133	fveq12d	$⊢ (φ \land C = A) \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B) \cup \{A\})) ((C, D) \cup \{A\}) = int (J) ([C, D))$
135	112 115 134	3eltr4d	$⊢ (φ \land C = A) \to A \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B) \cup \{A\})) ((C, D) \cup \{A\})$
136	20 21 23 24 25 135	limcres	$⊢ (φ \land C = A) \to ({F ↾}_{(C, D)}) {lim}_{ℂ} A = F {lim}_{ℂ} A$
137	17 136	eqtr2d	$⊢ (φ \land C = A) \to F {lim}_{ℂ} A = ({F ↾}_{(C, D)}) {lim}_{ℂ} C$
138	12 15 137	3eltr3d	$⊢ (φ \land C = A) \to Y \in (({F ↾}_{(C, D)}) {lim}_{ℂ} C)$
139		limcresi	$⊢ F {lim}_{ℂ} C \subseteq ({F ↾}_{(C, D)}) {lim}_{ℂ} C$
140		iffalse	$⊢ \neg C = A \to if (C = A, R, F (C)) = F (C)$
141	10 140	eqtrid	$⊢ \neg C = A \to Y = F (C)$
142	141	adantl	$⊢ (φ \land \neg C = A) \to Y = F (C)$
143		ssid	$⊢ ℂ \subseteq ℂ$
144	143	a1i	$⊢ φ \to ℂ \subseteq ℂ$
145		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B) = TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)$
146		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
147	146	restid	$⊢ TopOpen (ℂ_{fld}) \in Top \to TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
148	32 147	ax-mp	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
149	148	eqcomi	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
150	24 145 149	cncfcn	$⊢ ((A, B) \subseteq ℂ \land ℂ \subseteq ℂ) \to (A, B) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) Cn TopOpen (ℂ_{fld})$
151	22 144 150	sylancr	$⊢ φ \to (A, B) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) Cn TopOpen (ℂ_{fld})$
152	4 151	eleqtrd	$⊢ φ \to F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) Cn TopOpen (ℂ_{fld}))$
153	24	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
154		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land (A, B) \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B) \in TopOn ((A, B))$
155	153 22 154	mp2an	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B) \in TopOn ((A, B))$
156		cncnp	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B) \in TopOn ((A, B)) \land TopOpen (ℂ_{fld}) \in TopOn (ℂ)) \to (F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) Cn TopOpen (ℂ_{fld})) \leftrightarrow (F : (A, B) ⟶ ℂ \land \forall x \in (A, B) F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (x)))$
157	155 153 156	mp2an	$⊢ F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) Cn TopOpen (ℂ_{fld})) \leftrightarrow (F : (A, B) ⟶ ℂ \land \forall x \in (A, B) F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (x))$
158	152 157	sylib	$⊢ φ \to (F : (A, B) ⟶ ℂ \land \forall x \in (A, B) F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (x))$
159	158	simprd	$⊢ φ \to \forall x \in (A, B) F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (x)$
160	159	adantr	$⊢ (φ \land \neg C = A) \to \forall x \in (A, B) F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (x)$
161	117	adantr	$⊢ (φ \land \neg C = A) \to A \in ℝ^{*}$
162	57	adantr	$⊢ (φ \land \neg C = A) \to B \in ℝ^{*}$
163	6	adantr	$⊢ (φ \land \neg C = A) \to C \in ℝ$
164	1	adantr	$⊢ (φ \land \neg C = A) \to A \in ℝ$
165	53	simpld	$⊢ φ \to A \leq C$
166	165	adantr	$⊢ (φ \land \neg C = A) \to A \leq C$
167	113	eqcoms	$⊢ A = C \to C = A$
168	167	necon3bi	$⊢ \neg C = A \to A \neq C$
169	168	adantl	$⊢ (φ \land \neg C = A) \to A \neq C$
170	169	necomd	$⊢ (φ \land \neg C = A) \to C \neq A$
171	164 163 166 170	leneltd	$⊢ (φ \land \neg C = A) \to A < C$
172	6 7 2 8 54	ltletrd	$⊢ φ \to C < B$
173	172	adantr	$⊢ (φ \land \neg C = A) \to C < B$
174	161 162 163 171 173	eliood	$⊢ (φ \land \neg C = A) \to C \in (A, B)$
175		fveq2	$⊢ x = C \to ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (x) = ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (C)$
176	175	eleq2d	$⊢ x = C \to (F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (x) \leftrightarrow F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (C))$
177	176	rspccva	$⊢ (\forall x \in (A, B) F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (x) \land C \in (A, B)) \to F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (C)$
178	160 174 177	syl2anc	$⊢ (φ \land \neg C = A) \to F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (C)$
179	24 145	cnplimc	$⊢ ((A, B) \subseteq ℂ \land C \in (A, B)) \to (F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (C) \leftrightarrow (F : (A, B) ⟶ ℂ \land F (C) \in (F {lim}_{ℂ} C)))$
180	22 174 179	sylancr	$⊢ (φ \land \neg C = A) \to (F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B)) CnP TopOpen (ℂ_{fld})) (C) \leftrightarrow (F : (A, B) ⟶ ℂ \land F (C) \in (F {lim}_{ℂ} C)))$
181	178 180	mpbid	$⊢ (φ \land \neg C = A) \to (F : (A, B) ⟶ ℂ \land F (C) \in (F {lim}_{ℂ} C))$
182	181	simprd	$⊢ (φ \land \neg C = A) \to F (C) \in (F {lim}_{ℂ} C)$
183	142 182	eqeltrd	$⊢ (φ \land \neg C = A) \to Y \in (F {lim}_{ℂ} C)$
184	139 183	sselid	$⊢ (φ \land \neg C = A) \to Y \in (({F ↾}_{(C, D)}) {lim}_{ℂ} C)$
185	138 184	pm2.61dan	$⊢ φ \to Y \in (({F ↾}_{(C, D)}) {lim}_{ℂ} C)$

Metamath Proof Explorer

Theorem fourierdlem32

Proof