fourierdlem60

Description: Given a differentiable function F , with finite limit of the derivative at A the derived function H has a limit at 0 . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem60.a	$⊢ φ \to A \in ℝ$
	fourierdlem60.b	$⊢ φ \to B \in ℝ$
	fourierdlem60.altb	$⊢ φ \to A < B$
	fourierdlem60.f	$⊢ φ \to F : (A, B) ⟶ ℝ$
	fourierdlem60.y	$⊢ φ \to Y \in (F {lim}_{ℂ} B)$
	fourierdlem60.g	$⊢ G = ℝ D F$
	fourierdlem60.domg	$⊢ φ \to dom G = (A, B)$
	fourierdlem60.e	$⊢ φ \to E \in (G {lim}_{ℂ} B)$
	fourierdlem60.h	$⊢ H = (s \in (A - B, 0) ⟼ \frac{F (B + s) - Y}{s})$
	fourierdlem60.n	$⊢ N = (s \in (A - B, 0) ⟼ F (B + s) - Y)$
	fourierdlem60.d	$⊢ D = (s \in (A - B, 0) ⟼ s)$
Assertion	fourierdlem60	$⊢ φ \to E \in (H {lim}_{ℂ} 0)$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem60.a	$⊢ φ \to A \in ℝ$
2		fourierdlem60.b	$⊢ φ \to B \in ℝ$
3		fourierdlem60.altb	$⊢ φ \to A < B$
4		fourierdlem60.f	$⊢ φ \to F : (A, B) ⟶ ℝ$
5		fourierdlem60.y	$⊢ φ \to Y \in (F {lim}_{ℂ} B)$
6		fourierdlem60.g	$⊢ G = ℝ D F$
7		fourierdlem60.domg	$⊢ φ \to dom G = (A, B)$
8		fourierdlem60.e	$⊢ φ \to E \in (G {lim}_{ℂ} B)$
9		fourierdlem60.h	$⊢ H = (s \in (A - B, 0) ⟼ \frac{F (B + s) - Y}{s})$
10		fourierdlem60.n	$⊢ N = (s \in (A - B, 0) ⟼ F (B + s) - Y)$
11		fourierdlem60.d	$⊢ D = (s \in (A - B, 0) ⟼ s)$
12	1 2	resubcld	$⊢ φ \to A - B \in ℝ$
13	12	rexrd	$⊢ φ \to A - B \in ℝ^{*}$
14		0red	$⊢ φ \to 0 \in ℝ$
15	1 2	sublt0d	$⊢ φ \to (A - B < 0 \leftrightarrow A < B)$
16	3 15	mpbird	$⊢ φ \to A - B < 0$
17	4	adantr	$⊢ (φ \land s \in (A - B, 0)) \to F : (A, B) ⟶ ℝ$
18	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
19	18	adantr	$⊢ (φ \land s \in (A - B, 0)) \to A \in ℝ^{*}$
20	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
21	20	adantr	$⊢ (φ \land s \in (A - B, 0)) \to B \in ℝ^{*}$
22	2	adantr	$⊢ (φ \land s \in (A - B, 0)) \to B \in ℝ$
23		elioore	$⊢ s \in (A - B, 0) \to s \in ℝ$
24	23	adantl	$⊢ (φ \land s \in (A - B, 0)) \to s \in ℝ$
25	22 24	readdcld	$⊢ (φ \land s \in (A - B, 0)) \to B + s \in ℝ$
26	2	recnd	$⊢ φ \to B \in ℂ$
27	1	recnd	$⊢ φ \to A \in ℂ$
28	26 27	pncan3d	$⊢ φ \to B + A - B = A$
29	28	eqcomd	$⊢ φ \to A = B + A - B$
30	29	adantr	$⊢ (φ \land s \in (A - B, 0)) \to A = B + A - B$
31	12	adantr	$⊢ (φ \land s \in (A - B, 0)) \to A - B \in ℝ$
32	13	adantr	$⊢ (φ \land s \in (A - B, 0)) \to A - B \in ℝ^{*}$
33		0xr	$⊢ 0 \in ℝ^{*}$
34	33	a1i	$⊢ (φ \land s \in (A - B, 0)) \to 0 \in ℝ^{*}$
35		simpr	$⊢ (φ \land s \in (A - B, 0)) \to s \in (A - B, 0)$
36	32 34 35	ioogtlbd	$⊢ (φ \land s \in (A - B, 0)) \to A - B < s$
37	31 24 22 36	ltadd2dd	$⊢ (φ \land s \in (A - B, 0)) \to B + A - B < B + s$
38	30 37	eqbrtrd	$⊢ (φ \land s \in (A - B, 0)) \to A < B + s$
39		0red	$⊢ (φ \land s \in (A - B, 0)) \to 0 \in ℝ$
40	32 34 35	iooltubd	$⊢ (φ \land s \in (A - B, 0)) \to s < 0$
41	24 39 22 40	ltadd2dd	$⊢ (φ \land s \in (A - B, 0)) \to B + s < B + 0$
42	26	addid1d	$⊢ φ \to B + 0 = B$
43	42	adantr	$⊢ (φ \land s \in (A - B, 0)) \to B + 0 = B$
44	41 43	breqtrd	$⊢ (φ \land s \in (A - B, 0)) \to B + s < B$
45	19 21 25 38 44	eliood	$⊢ (φ \land s \in (A - B, 0)) \to B + s \in (A, B)$
46	17 45	ffvelrnd	$⊢ (φ \land s \in (A - B, 0)) \to F (B + s) \in ℝ$
47		ioossre	$⊢ (A, B) \subseteq ℝ$
48	47	a1i	$⊢ φ \to (A, B) \subseteq ℝ$
49		ax-resscn	$⊢ ℝ \subseteq ℂ$
50	48 49	sstrdi	$⊢ φ \to (A, B) \subseteq ℂ$
51		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
52	51 18 2 3	lptioo2cn	$⊢ φ \to B \in limPt (TopOpen (ℂ_{fld})) ((A, B))$
53	4 50 52 5	limcrecl	$⊢ φ \to Y \in ℝ$
54	53	adantr	$⊢ (φ \land s \in (A - B, 0)) \to Y \in ℝ$
55	46 54	resubcld	$⊢ (φ \land s \in (A - B, 0)) \to F (B + s) - Y \in ℝ$
56	55 10	fmptd	$⊢ φ \to N : (A - B, 0) ⟶ ℝ$
57	24 11	fmptd	$⊢ φ \to D : (A - B, 0) ⟶ ℝ$
58	10	oveq2i	$⊢ ℝ D N = \frac{d (s \in (A - B, 0)⟼ F (B + s) - Y)}{d_{ℝ} s}$
59	58	a1i	$⊢ φ \to ℝ D N = \frac{d (s \in (A - B, 0)⟼ F (B + s) - Y)}{d_{ℝ} s}$
60	59	dmeqd	$⊢ φ \to dom N_{ℝ}^{'} = dom \frac{d (s \in (A - B, 0)⟼ F (B + s) - Y)}{d_{ℝ} s}$
61		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
62	61	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
63	46	recnd	$⊢ (φ \land s \in (A - B, 0)) \to F (B + s) \in ℂ$
64		dvfre	$⊢ (F : (A, B) ⟶ ℝ \land (A, B) \subseteq ℝ) \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
65	4 48 64	syl2anc	$⊢ φ \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
66	6	a1i	$⊢ φ \to G = ℝ D F$
67	66	feq1d	$⊢ φ \to (G : dom F_{ℝ}^{'} ⟶ ℝ \leftrightarrow F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ)$
68	65 67	mpbird	$⊢ φ \to G : dom F_{ℝ}^{'} ⟶ ℝ$
69	68	adantr	$⊢ (φ \land s \in (A - B, 0)) \to G : dom F_{ℝ}^{'} ⟶ ℝ$
70	66	eqcomd	$⊢ φ \to ℝ D F = G$
71	70	dmeqd	$⊢ φ \to dom F_{ℝ}^{'} = dom G$
72	71 7	eqtr2d	$⊢ φ \to (A, B) = dom F_{ℝ}^{'}$
73	72	adantr	$⊢ (φ \land s \in (A - B, 0)) \to (A, B) = dom F_{ℝ}^{'}$
74	45 73	eleqtrd	$⊢ (φ \land s \in (A - B, 0)) \to B + s \in dom F_{ℝ}^{'}$
75	69 74	ffvelrnd	$⊢ (φ \land s \in (A - B, 0)) \to G (B + s) \in ℝ$
76		1red	$⊢ (φ \land s \in (A - B, 0)) \to 1 \in ℝ$
77	4	ffvelrnda	$⊢ (φ \land x \in (A, B)) \to F (x) \in ℝ$
78	77	recnd	$⊢ (φ \land x \in (A, B)) \to F (x) \in ℂ$
79	72	feq2d	$⊢ φ \to (G : (A, B) ⟶ ℝ \leftrightarrow G : dom F_{ℝ}^{'} ⟶ ℝ)$
80	68 79	mpbird	$⊢ φ \to G : (A, B) ⟶ ℝ$
81	80	ffvelrnda	$⊢ (φ \land x \in (A, B)) \to G (x) \in ℝ$
82	26	adantr	$⊢ (φ \land s \in (A - B, 0)) \to B \in ℂ$
83	26	adantr	$⊢ (φ \land s \in ℝ) \to B \in ℂ$
84		0red	$⊢ (φ \land s \in ℝ) \to 0 \in ℝ$
85	62 26	dvmptc	$⊢ φ \to \frac{d (s \in ℝ⟼ B)}{d_{ℝ} s} = (s \in ℝ ⟼ 0)$
86		ioossre	$⊢ (A - B, 0) \subseteq ℝ$
87	86	a1i	$⊢ φ \to (A - B, 0) \subseteq ℝ$
88		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
89		iooretop	$⊢ (A - B, 0) \in topGen (ran (.))$
90	89	a1i	$⊢ φ \to (A - B, 0) \in topGen (ran (.))$
91	62 83 84 85 87 88 51 90	dvmptres	$⊢ φ \to \frac{d (s \in (A - B, 0)⟼ B)}{d_{ℝ} s} = (s \in (A - B, 0) ⟼ 0)$
92	24	recnd	$⊢ (φ \land s \in (A - B, 0)) \to s \in ℂ$
93		recn	$⊢ s \in ℝ \to s \in ℂ$
94	93	adantl	$⊢ (φ \land s \in ℝ) \to s \in ℂ$
95		1red	$⊢ (φ \land s \in ℝ) \to 1 \in ℝ$
96	62	dvmptid	$⊢ φ \to \frac{d (s \in ℝ⟼ s)}{d_{ℝ} s} = (s \in ℝ ⟼ 1)$
97	62 94 95 96 87 88 51 90	dvmptres	$⊢ φ \to \frac{d (s \in (A - B, 0)⟼ s)}{d_{ℝ} s} = (s \in (A - B, 0) ⟼ 1)$
98	62 82 39 91 92 76 97	dvmptadd	$⊢ φ \to \frac{d (s \in (A - B, 0)⟼ B + s)}{d_{ℝ} s} = (s \in (A - B, 0) ⟼ 0 + 1)$
99		0p1e1	$⊢ 0 + 1 = 1$
100	99	mpteq2i	$⊢ (s \in (A - B, 0) ⟼ 0 + 1) = (s \in (A - B, 0) ⟼ 1)$
101	98 100	eqtrdi	$⊢ φ \to \frac{d (s \in (A - B, 0)⟼ B + s)}{d_{ℝ} s} = (s \in (A - B, 0) ⟼ 1)$
102	4	feqmptd	$⊢ φ \to F = (x \in (A, B) ⟼ F (x))$
103	102	eqcomd	$⊢ φ \to (x \in (A, B) ⟼ F (x)) = F$
104	103	oveq2d	$⊢ φ \to \frac{d (x \in (A, B)⟼ F (x))}{d_{ℝ} x} = ℝ D F$
105	80	feqmptd	$⊢ φ \to G = (x \in (A, B) ⟼ G (x))$
106	104 70 105	3eqtrd	$⊢ φ \to \frac{d (x \in (A, B)⟼ F (x))}{d_{ℝ} x} = (x \in (A, B) ⟼ G (x))$
107		fveq2	$⊢ x = B + s \to F (x) = F (B + s)$
108		fveq2	$⊢ x = B + s \to G (x) = G (B + s)$
109	62 62 45 76 78 81 101 106 107 108	dvmptco	$⊢ φ \to \frac{d (s \in (A - B, 0)⟼ F (B + s))}{d_{ℝ} s} = (s \in (A - B, 0) ⟼ G (B + s) \cdot 1)$
110	75	recnd	$⊢ (φ \land s \in (A - B, 0)) \to G (B + s) \in ℂ$
111	110	mulid1d	$⊢ (φ \land s \in (A - B, 0)) \to G (B + s) \cdot 1 = G (B + s)$
112	111	mpteq2dva	$⊢ φ \to (s \in (A - B, 0) ⟼ G (B + s) \cdot 1) = (s \in (A - B, 0) ⟼ G (B + s))$
113	109 112	eqtrd	$⊢ φ \to \frac{d (s \in (A - B, 0)⟼ F (B + s))}{d_{ℝ} s} = (s \in (A - B, 0) ⟼ G (B + s))$
114		limccl	$⊢ F {lim}_{ℂ} B \subseteq ℂ$
115	114 5	sselid	$⊢ φ \to Y \in ℂ$
116	115	adantr	$⊢ (φ \land s \in (A - B, 0)) \to Y \in ℂ$
117	115	adantr	$⊢ (φ \land s \in ℝ) \to Y \in ℂ$
118	62 115	dvmptc	$⊢ φ \to \frac{d (s \in ℝ⟼ Y)}{d_{ℝ} s} = (s \in ℝ ⟼ 0)$
119	62 117 84 118 87 88 51 90	dvmptres	$⊢ φ \to \frac{d (s \in (A - B, 0)⟼ Y)}{d_{ℝ} s} = (s \in (A - B, 0) ⟼ 0)$
120	62 63 75 113 116 34 119	dvmptsub	$⊢ φ \to \frac{d (s \in (A - B, 0)⟼ F (B + s) - Y)}{d_{ℝ} s} = (s \in (A - B, 0) ⟼ G (B + s) - 0)$
121	110	subid1d	$⊢ (φ \land s \in (A - B, 0)) \to G (B + s) - 0 = G (B + s)$
122	121	mpteq2dva	$⊢ φ \to (s \in (A - B, 0) ⟼ G (B + s) - 0) = (s \in (A - B, 0) ⟼ G (B + s))$
123	120 122	eqtrd	$⊢ φ \to \frac{d (s \in (A - B, 0)⟼ F (B + s) - Y)}{d_{ℝ} s} = (s \in (A - B, 0) ⟼ G (B + s))$
124	123	dmeqd	$⊢ φ \to dom \frac{d (s \in (A - B, 0)⟼ F (B + s) - Y)}{d_{ℝ} s} = dom (s \in (A - B, 0) ⟼ G (B + s))$
125	75	ralrimiva	$⊢ φ \to \forall s \in (A - B, 0) G (B + s) \in ℝ$
126		dmmptg	$⊢ \forall s \in (A - B, 0) G (B + s) \in ℝ \to dom (s \in (A - B, 0) ⟼ G (B + s)) = (A - B, 0)$
127	125 126	syl	$⊢ φ \to dom (s \in (A - B, 0) ⟼ G (B + s)) = (A - B, 0)$
128	60 124 127	3eqtrd	$⊢ φ \to dom N_{ℝ}^{'} = (A - B, 0)$
129	11	a1i	$⊢ φ \to D = (s \in (A - B, 0) ⟼ s)$
130	129	oveq2d	$⊢ φ \to ℝ D D = \frac{d (s \in (A - B, 0)⟼ s)}{d_{ℝ} s}$
131	130 97	eqtrd	$⊢ φ \to ℝ D D = (s \in (A - B, 0) ⟼ 1)$
132	131	dmeqd	$⊢ φ \to dom D_{ℝ}^{'} = dom (s \in (A - B, 0) ⟼ 1)$
133	76	ralrimiva	$⊢ φ \to \forall s \in (A - B, 0) 1 \in ℝ$
134		dmmptg	$⊢ \forall s \in (A - B, 0) 1 \in ℝ \to dom (s \in (A - B, 0) ⟼ 1) = (A - B, 0)$
135	133 134	syl	$⊢ φ \to dom (s \in (A - B, 0) ⟼ 1) = (A - B, 0)$
136	132 135	eqtrd	$⊢ φ \to dom D_{ℝ}^{'} = (A - B, 0)$
137		eqid	$⊢ (s \in (A - B, 0) ⟼ F (B + s)) = (s \in (A - B, 0) ⟼ F (B + s))$
138		eqid	$⊢ (s \in (A - B, 0) ⟼ Y) = (s \in (A - B, 0) ⟼ Y)$
139		eqid	$⊢ (s \in (A - B, 0) ⟼ F (B + s) - Y) = (s \in (A - B, 0) ⟼ F (B + s) - Y)$
140	45	adantrr	$⊢ (φ \land (s \in (A - B, 0) \land B + s \neq B)) \to B + s \in (A, B)$
141		eqid	$⊢ (s \in (A - B, 0) ⟼ B) = (s \in (A - B, 0) ⟼ B)$
142		eqid	$⊢ (s \in (A - B, 0) ⟼ s) = (s \in (A - B, 0) ⟼ s)$
143		eqid	$⊢ (s \in (A - B, 0) ⟼ B + s) = (s \in (A - B, 0) ⟼ B + s)$
144	87 49	sstrdi	$⊢ φ \to (A - B, 0) \subseteq ℂ$
145	14	recnd	$⊢ φ \to 0 \in ℂ$
146	141 144 26 145	constlimc	$⊢ φ \to B \in ((s \in (A - B, 0) ⟼ B) {lim}_{ℂ} 0)$
147	144 142 145	idlimc	$⊢ φ \to 0 \in ((s \in (A - B, 0) ⟼ s) {lim}_{ℂ} 0)$
148	141 142 143 82 92 146 147	addlimc	$⊢ φ \to B + 0 \in ((s \in (A - B, 0) ⟼ B + s) {lim}_{ℂ} 0)$
149	42 148	eqeltrrd	$⊢ φ \to B \in ((s \in (A - B, 0) ⟼ B + s) {lim}_{ℂ} 0)$
150	102	oveq1d	$⊢ φ \to F {lim}_{ℂ} B = (x \in (A, B) ⟼ F (x)) {lim}_{ℂ} B$
151	5 150	eleqtrd	$⊢ φ \to Y \in ((x \in (A, B) ⟼ F (x)) {lim}_{ℂ} B)$
152		simplrr	$⊢ ((φ \land (s \in (A - B, 0) \land B + s = B)) \land \neg F (B + s) = Y) \to B + s = B$
153	25 44	ltned	$⊢ (φ \land s \in (A - B, 0)) \to B + s \neq B$
154	153	neneqd	$⊢ (φ \land s \in (A - B, 0)) \to \neg B + s = B$
155	154	adantrr	$⊢ (φ \land (s \in (A - B, 0) \land B + s = B)) \to \neg B + s = B$
156	155	adantr	$⊢ ((φ \land (s \in (A - B, 0) \land B + s = B)) \land \neg F (B + s) = Y) \to \neg B + s = B$
157	152 156	condan	$⊢ (φ \land (s \in (A - B, 0) \land B + s = B)) \to F (B + s) = Y$
158	140 78 149 151 107 157	limcco	$⊢ φ \to Y \in ((s \in (A - B, 0) ⟼ F (B + s)) {lim}_{ℂ} 0)$
159	138 144 115 145	constlimc	$⊢ φ \to Y \in ((s \in (A - B, 0) ⟼ Y) {lim}_{ℂ} 0)$
160	137 138 139 63 116 158 159	sublimc	$⊢ φ \to Y - Y \in ((s \in (A - B, 0) ⟼ F (B + s) - Y) {lim}_{ℂ} 0)$
161	115	subidd	$⊢ φ \to Y - Y = 0$
162	10	eqcomi	$⊢ (s \in (A - B, 0) ⟼ F (B + s) - Y) = N$
163	162	oveq1i	$⊢ (s \in (A - B, 0) ⟼ F (B + s) - Y) {lim}_{ℂ} 0 = N {lim}_{ℂ} 0$
164	163	a1i	$⊢ φ \to (s \in (A - B, 0) ⟼ F (B + s) - Y) {lim}_{ℂ} 0 = N {lim}_{ℂ} 0$
165	160 161 164	3eltr3d	$⊢ φ \to 0 \in (N {lim}_{ℂ} 0)$
166	144 11 145	idlimc	$⊢ φ \to 0 \in (D {lim}_{ℂ} 0)$
167		ubioo	$⊢ \neg 0 \in (A - B, 0)$
168	167	a1i	$⊢ φ \to \neg 0 \in (A - B, 0)$
169		mptresid	$⊢ {I ↾}_{(A - B, 0)} = (s \in (A - B, 0) ⟼ s)$
170	129 169	eqtr4di	$⊢ φ \to D = {I ↾}_{(A - B, 0)}$
171	170	rneqd	$⊢ φ \to ran D = ran ({I ↾}_{(A - B, 0)})$
172		rnresi	$⊢ ran ({I ↾}_{(A - B, 0)}) = (A - B, 0)$
173	171 172	eqtr2di	$⊢ φ \to (A - B, 0) = ran D$
174	168 173	neleqtrd	$⊢ φ \to \neg 0 \in ran D$
175		0ne1	$⊢ 0 \neq 1$
176	175	neii	$⊢ \neg 0 = 1$
177		elsng	$⊢ 0 \in ℝ \to (0 \in \{1\} \leftrightarrow 0 = 1)$
178	14 177	syl	$⊢ φ \to (0 \in \{1\} \leftrightarrow 0 = 1)$
179	176 178	mtbiri	$⊢ φ \to \neg 0 \in \{1\}$
180	131	rneqd	$⊢ φ \to ran D_{ℝ}^{'} = ran (s \in (A - B, 0) ⟼ 1)$
181		eqid	$⊢ (s \in (A - B, 0) ⟼ 1) = (s \in (A - B, 0) ⟼ 1)$
182	33	a1i	$⊢ φ \to 0 \in ℝ^{*}$
183		ioon0	$⊢ (A - B \in ℝ^{} \land 0 \in ℝ^{}) \to ((A - B, 0) \neq \emptyset \leftrightarrow A - B < 0)$
184	13 182 183	syl2anc	$⊢ φ \to ((A - B, 0) \neq \emptyset \leftrightarrow A - B < 0)$
185	16 184	mpbird	$⊢ φ \to (A - B, 0) \neq \emptyset$
186	181 185	rnmptc	$⊢ φ \to ran (s \in (A - B, 0) ⟼ 1) = \{1\}$
187	180 186	eqtr2d	$⊢ φ \to \{1\} = ran D_{ℝ}^{'}$
188	179 187	neleqtrd	$⊢ φ \to \neg 0 \in ran D_{ℝ}^{'}$
189	81	recnd	$⊢ (φ \land x \in (A, B)) \to G (x) \in ℂ$
190	105	oveq1d	$⊢ φ \to G {lim}_{ℂ} B = (x \in (A, B) ⟼ G (x)) {lim}_{ℂ} B$
191	8 190	eleqtrd	$⊢ φ \to E \in ((x \in (A, B) ⟼ G (x)) {lim}_{ℂ} B)$
192		simplrr	$⊢ ((φ \land (s \in (A - B, 0) \land B + s = B)) \land \neg G (B + s) = E) \to B + s = B$
193	155	adantr	$⊢ ((φ \land (s \in (A - B, 0) \land B + s = B)) \land \neg G (B + s) = E) \to \neg B + s = B$
194	192 193	condan	$⊢ (φ \land (s \in (A - B, 0) \land B + s = B)) \to G (B + s) = E$
195	140 189 149 191 108 194	limcco	$⊢ φ \to E \in ((s \in (A - B, 0) ⟼ G (B + s)) {lim}_{ℂ} 0)$
196	110	div1d	$⊢ (φ \land s \in (A - B, 0)) \to \frac{G (B + s)}{1} = G (B + s)$
197	58 123	syl5eq	$⊢ φ \to ℝ D N = (s \in (A - B, 0) ⟼ G (B + s))$
198	197	adantr	$⊢ (φ \land s \in (A - B, 0)) \to ℝ D N = (s \in (A - B, 0) ⟼ G (B + s))$
199	198	fveq1d	$⊢ (φ \land s \in (A - B, 0)) \to N_{ℝ}^{'} (s) = (s \in (A - B, 0) ⟼ G (B + s)) (s)$
200		fvmpt4	$⊢ (s \in (A - B, 0) \land G (B + s) \in ℝ) \to (s \in (A - B, 0) ⟼ G (B + s)) (s) = G (B + s)$
201	35 75 200	syl2anc	$⊢ (φ \land s \in (A - B, 0)) \to (s \in (A - B, 0) ⟼ G (B + s)) (s) = G (B + s)$
202	199 201	eqtr2d	$⊢ (φ \land s \in (A - B, 0)) \to G (B + s) = N_{ℝ}^{'} (s)$
203	131	fveq1d	$⊢ φ \to D_{ℝ}^{'} (s) = (s \in (A - B, 0) ⟼ 1) (s)$
204	203	adantr	$⊢ (φ \land s \in (A - B, 0)) \to D_{ℝ}^{'} (s) = (s \in (A - B, 0) ⟼ 1) (s)$
205		fvmpt4	$⊢ (s \in (A - B, 0) \land 1 \in ℝ) \to (s \in (A - B, 0) ⟼ 1) (s) = 1$
206	35 76 205	syl2anc	$⊢ (φ \land s \in (A - B, 0)) \to (s \in (A - B, 0) ⟼ 1) (s) = 1$
207	204 206	eqtr2d	$⊢ (φ \land s \in (A - B, 0)) \to 1 = D_{ℝ}^{'} (s)$
208	202 207	oveq12d	$⊢ (φ \land s \in (A - B, 0)) \to \frac{G (B + s)}{1} = \frac{N_{ℝ}^{'} (s)}{D_{ℝ}^{'} (s)}$
209	196 208	eqtr3d	$⊢ (φ \land s \in (A - B, 0)) \to G (B + s) = \frac{N_{ℝ}^{'} (s)}{D_{ℝ}^{'} (s)}$
210	209	mpteq2dva	$⊢ φ \to (s \in (A - B, 0) ⟼ G (B + s)) = (s \in (A - B, 0) ⟼ \frac{N_{ℝ}^{'} (s)}{D_{ℝ}^{'} (s)})$
211	210	oveq1d	$⊢ φ \to (s \in (A - B, 0) ⟼ G (B + s)) {lim}_{ℂ} 0 = (s \in (A - B, 0) ⟼ \frac{N_{ℝ}^{'} (s)}{D_{ℝ}^{'} (s)}) {lim}_{ℂ} 0$
212	195 211	eleqtrd	$⊢ φ \to E \in ((s \in (A - B, 0) ⟼ \frac{N_{ℝ}^{'} (s)}{D_{ℝ}^{'} (s)}) {lim}_{ℂ} 0)$
213	13 14 16 56 57 128 136 165 166 174 188 212	lhop2	$⊢ φ \to E \in ((s \in (A - B, 0) ⟼ \frac{N (s)}{D (s)}) {lim}_{ℂ} 0)$
214	10	fvmpt2	$⊢ (s \in (A - B, 0) \land F (B + s) - Y \in ℝ) \to N (s) = F (B + s) - Y$
215	35 55 214	syl2anc	$⊢ (φ \land s \in (A - B, 0)) \to N (s) = F (B + s) - Y$
216	11	fvmpt2	$⊢ (s \in (A - B, 0) \land s \in (A - B, 0)) \to D (s) = s$
217	35 35 216	syl2anc	$⊢ (φ \land s \in (A - B, 0)) \to D (s) = s$
218	215 217	oveq12d	$⊢ (φ \land s \in (A - B, 0)) \to \frac{N (s)}{D (s)} = \frac{F (B + s) - Y}{s}$
219	218	mpteq2dva	$⊢ φ \to (s \in (A - B, 0) ⟼ \frac{N (s)}{D (s)}) = (s \in (A - B, 0) ⟼ \frac{F (B + s) - Y}{s})$
220	219 9	eqtr4di	$⊢ φ \to (s \in (A - B, 0) ⟼ \frac{N (s)}{D (s)}) = H$
221	220	oveq1d	$⊢ φ \to (s \in (A - B, 0) ⟼ \frac{N (s)}{D (s)}) {lim}_{ℂ} 0 = H {lim}_{ℂ} 0$
222	213 221	eleqtrd	$⊢ φ \to E \in (H {lim}_{ℂ} 0)$

Metamath Proof Explorer

Theorem fourierdlem60

Proof