fourierdlem28

Description: Derivative of ( F( X + s ) ) . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem28.1	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem28.x	$⊢ φ \to X \in ℝ$
	fourierdlem28.a	$⊢ φ \to A \in ℝ$
	fourierdlem28.3b	$⊢ φ \to B \in ℝ$
	fourierdlem28.d	$⊢ D = ℝ D ({F ↾}_{(X + A, X + B)})$
	fourierdlem28.df	$⊢ φ \to D : (X + A, X + B) ⟶ ℝ$
Assertion	fourierdlem28	$⊢ φ \to \frac{d (s \in (A, B)⟼ F (X + s))}{d_{ℝ} s} = (s \in (A, B) ⟼ D (X + s))$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem28.1	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierdlem28.x	$⊢ φ \to X \in ℝ$
3		fourierdlem28.a	$⊢ φ \to A \in ℝ$
4		fourierdlem28.3b	$⊢ φ \to B \in ℝ$
5		fourierdlem28.d	$⊢ D = ℝ D ({F ↾}_{(X + A, X + B)})$
6		fourierdlem28.df	$⊢ φ \to D : (X + A, X + B) ⟶ ℝ$
7		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
8	7	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
9	2 3	readdcld	$⊢ φ \to X + A \in ℝ$
10	9	rexrd	$⊢ φ \to X + A \in ℝ^{*}$
11	10	adantr	$⊢ (φ \land s \in (A, B)) \to X + A \in ℝ^{*}$
12	2 4	readdcld	$⊢ φ \to X + B \in ℝ$
13	12	rexrd	$⊢ φ \to X + B \in ℝ^{*}$
14	13	adantr	$⊢ (φ \land s \in (A, B)) \to X + B \in ℝ^{*}$
15	2	adantr	$⊢ (φ \land s \in (A, B)) \to X \in ℝ$
16		elioore	$⊢ s \in (A, B) \to s \in ℝ$
17	16	adantl	$⊢ (φ \land s \in (A, B)) \to s \in ℝ$
18	15 17	readdcld	$⊢ (φ \land s \in (A, B)) \to X + s \in ℝ$
19	3	adantr	$⊢ (φ \land s \in (A, B)) \to A \in ℝ$
20	19	rexrd	$⊢ (φ \land s \in (A, B)) \to A \in ℝ^{*}$
21	4	rexrd	$⊢ φ \to B \in ℝ^{*}$
22	21	adantr	$⊢ (φ \land s \in (A, B)) \to B \in ℝ^{*}$
23		simpr	$⊢ (φ \land s \in (A, B)) \to s \in (A, B)$
24		ioogtlb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land s \in (A, B)) \to A < s$
25	20 22 23 24	syl3anc	$⊢ (φ \land s \in (A, B)) \to A < s$
26	19 17 15 25	ltadd2dd	$⊢ (φ \land s \in (A, B)) \to X + A < X + s$
27	4	adantr	$⊢ (φ \land s \in (A, B)) \to B \in ℝ$
28		iooltub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land s \in (A, B)) \to s < B$
29	20 22 23 28	syl3anc	$⊢ (φ \land s \in (A, B)) \to s < B$
30	17 27 15 29	ltadd2dd	$⊢ (φ \land s \in (A, B)) \to X + s < X + B$
31	11 14 18 26 30	eliood	$⊢ (φ \land s \in (A, B)) \to X + s \in (X + A, X + B)$
32		1red	$⊢ (φ \land s \in (A, B)) \to 1 \in ℝ$
33	1	adantr	$⊢ (φ \land y \in (X + A, X + B)) \to F : ℝ ⟶ ℝ$
34		elioore	$⊢ y \in (X + A, X + B) \to y \in ℝ$
35	34	adantl	$⊢ (φ \land y \in (X + A, X + B)) \to y \in ℝ$
36	33 35	ffvelcdmd	$⊢ (φ \land y \in (X + A, X + B)) \to F (y) \in ℝ$
37	36	recnd	$⊢ (φ \land y \in (X + A, X + B)) \to F (y) \in ℂ$
38	6	ffvelcdmda	$⊢ (φ \land y \in (X + A, X + B)) \to D (y) \in ℝ$
39	15	recnd	$⊢ (φ \land s \in (A, B)) \to X \in ℂ$
40		0red	$⊢ (φ \land s \in (A, B)) \to 0 \in ℝ$
41		iooretop	$⊢ (A, B) \in topGen (ran (.))$
42		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
43	41 42	eleqtri	$⊢ (A, B) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
44	43	a1i	$⊢ φ \to (A, B) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
45	2	recnd	$⊢ φ \to X \in ℂ$
46	8 44 45	dvmptconst	$⊢ φ \to \frac{d (s \in (A, B)⟼ X)}{d_{ℝ} s} = (s \in (A, B) ⟼ 0)$
47	17	recnd	$⊢ (φ \land s \in (A, B)) \to s \in ℂ$
48	8 44	dvmptidg	$⊢ φ \to \frac{d (s \in (A, B)⟼ s)}{d_{ℝ} s} = (s \in (A, B) ⟼ 1)$
49	8 39 40 46 47 32 48	dvmptadd	$⊢ φ \to \frac{d (s \in (A, B)⟼ X + s)}{d_{ℝ} s} = (s \in (A, B) ⟼ 0 + 1)$
50		0p1e1	$⊢ 0 + 1 = 1$
51	50	a1i	$⊢ (φ \land s \in (A, B)) \to 0 + 1 = 1$
52	51	mpteq2dva	$⊢ φ \to (s \in (A, B) ⟼ 0 + 1) = (s \in (A, B) ⟼ 1)$
53	49 52	eqtrd	$⊢ φ \to \frac{d (s \in (A, B)⟼ X + s)}{d_{ℝ} s} = (s \in (A, B) ⟼ 1)$
54	1	feqmptd	$⊢ φ \to F = (y \in ℝ ⟼ F (y))$
55	54	reseq1d	$⊢ φ \to {F ↾}_{(X + A, X + B)} = {(y \in ℝ ⟼ F (y)) ↾}_{(X + A, X + B)}$
56		ioossre	$⊢ (X + A, X + B) \subseteq ℝ$
57	56	a1i	$⊢ φ \to (X + A, X + B) \subseteq ℝ$
58	57	resmptd	$⊢ φ \to {(y \in ℝ ⟼ F (y)) ↾}_{(X + A, X + B)} = (y \in (X + A, X + B) ⟼ F (y))$
59	55 58	eqtr2d	$⊢ φ \to (y \in (X + A, X + B) ⟼ F (y)) = {F ↾}_{(X + A, X + B)}$
60	59	oveq2d	$⊢ φ \to \frac{d (y \in (X + A, X + B)⟼ F (y))}{d_{ℝ} y} = ℝ D ({F ↾}_{(X + A, X + B)})$
61	5	eqcomi	$⊢ ℝ D ({F ↾}_{(X + A, X + B)}) = D$
62	61	a1i	$⊢ φ \to ℝ D ({F ↾}_{(X + A, X + B)}) = D$
63	6	feqmptd	$⊢ φ \to D = (y \in (X + A, X + B) ⟼ D (y))$
64	60 62 63	3eqtrd	$⊢ φ \to \frac{d (y \in (X + A, X + B)⟼ F (y))}{d_{ℝ} y} = (y \in (X + A, X + B) ⟼ D (y))$
65		fveq2	$⊢ y = X + s \to F (y) = F (X + s)$
66		fveq2	$⊢ y = X + s \to D (y) = D (X + s)$
67	8 8 31 32 37 38 53 64 65 66	dvmptco	$⊢ φ \to \frac{d (s \in (A, B)⟼ F (X + s))}{d_{ℝ} s} = (s \in (A, B) ⟼ D (X + s) \cdot 1)$
68	6	adantr	$⊢ (φ \land s \in (A, B)) \to D : (X + A, X + B) ⟶ ℝ$
69	68 31	ffvelcdmd	$⊢ (φ \land s \in (A, B)) \to D (X + s) \in ℝ$
70	69	recnd	$⊢ (φ \land s \in (A, B)) \to D (X + s) \in ℂ$
71	70	mulridd	$⊢ (φ \land s \in (A, B)) \to D (X + s) \cdot 1 = D (X + s)$
72	71	mpteq2dva	$⊢ φ \to (s \in (A, B) ⟼ D (X + s) \cdot 1) = (s \in (A, B) ⟼ D (X + s))$
73	67 72	eqtrd	$⊢ φ \to \frac{d (s \in (A, B)⟼ F (X + s))}{d_{ℝ} s} = (s \in (A, B) ⟼ D (X + s))$

Metamath Proof Explorer

Theorem fourierdlem28

Proof