fourierdlem61

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

Proof

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

Metamath Proof Explorer

Theorem fourierdlem61

Proof