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

Metamath Proof Explorer

Theorem fourierdlem33

Proof