fourierdlem33

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

	Ref	Expression
Hypotheses	fourierdlem33.1	$⊢ φ \to A \in ℝ$
	fourierdlem33.2	$⊢ φ \to B \in ℝ$
	fourierdlem33.3	$⊢ φ \to A < B$
	fourierdlem33.4	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℂ$
	fourierdlem33.5	$⊢ φ \to L \in (F {lim}_{ℂ} B)$
	fourierdlem33.6	$⊢ φ \to C \in ℝ$
	fourierdlem33.7	$⊢ φ \to D \in ℝ$
	fourierdlem33.8	$⊢ φ \to C < D$
	fourierdlem33.ss	$⊢ φ \to (C, D) \subseteq (A, B)$
	fourierdlem33.y	$⊢ Y = if (D = B, L, F (D))$
	fourierdlem33.10	$⊢ J = TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B) \cup \{B\})$
Assertion	fourierdlem33	$⊢ φ \to Y \in (({F ↾}_{(C, D)}) {lim}_{ℂ} D)$

Proof

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

Metamath Proof Explorer

Theorem fourierdlem33

Proof