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		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
43	42	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
44	41 43	eleqtri	$⊢ (A, B) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
45	44	a1i	$⊢ φ \to (A, B) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
46	2	recnd	$⊢ φ \to X \in ℂ$
47	8 45 46	dvmptconst	$⊢ φ \to \frac{d (s \in (A, B)⟼ X)}{d_{ℝ} s} = (s \in (A, B) ⟼ 0)$
48	17	recnd	$⊢ (φ \land s \in (A, B)) \to s \in ℂ$
49	8 45	dvmptidg	$⊢ φ \to \frac{d (s \in (A, B)⟼ s)}{d_{ℝ} s} = (s \in (A, B) ⟼ 1)$
50	8 39 40 47 48 32 49	dvmptadd	$⊢ φ \to \frac{d (s \in (A, B)⟼ X + s)}{d_{ℝ} s} = (s \in (A, B) ⟼ 0 + 1)$
51		0p1e1	$⊢ 0 + 1 = 1$
52	51	a1i	$⊢ (φ \land s \in (A, B)) \to 0 + 1 = 1$
53	52	mpteq2dva	$⊢ φ \to (s \in (A, B) ⟼ 0 + 1) = (s \in (A, B) ⟼ 1)$
54	50 53	eqtrd	$⊢ φ \to \frac{d (s \in (A, B)⟼ X + s)}{d_{ℝ} s} = (s \in (A, B) ⟼ 1)$
55	1	feqmptd	$⊢ φ \to F = (y \in ℝ ⟼ F (y))$
56	55	reseq1d	$⊢ φ \to {F ↾}_{(X + A, X + B)} = {(y \in ℝ ⟼ F (y)) ↾}_{(X + A, X + B)}$
57		ioossre	$⊢ (X + A, X + B) \subseteq ℝ$
58	57	a1i	$⊢ φ \to (X + A, X + B) \subseteq ℝ$
59	58	resmptd	$⊢ φ \to {(y \in ℝ ⟼ F (y)) ↾}_{(X + A, X + B)} = (y \in (X + A, X + B) ⟼ F (y))$
60	56 59	eqtr2d	$⊢ φ \to (y \in (X + A, X + B) ⟼ F (y)) = {F ↾}_{(X + A, X + B)}$
61	60	oveq2d	$⊢ φ \to \frac{d (y \in (X + A, X + B)⟼ F (y))}{d_{ℝ} y} = ℝ D ({F ↾}_{(X + A, X + B)})$
62	5	eqcomi	$⊢ ℝ D ({F ↾}_{(X + A, X + B)}) = D$
63	62	a1i	$⊢ φ \to ℝ D ({F ↾}_{(X + A, X + B)}) = D$
64	6	feqmptd	$⊢ φ \to D = (y \in (X + A, X + B) ⟼ D (y))$
65	61 63 64	3eqtrd	$⊢ φ \to \frac{d (y \in (X + A, X + B)⟼ F (y))}{d_{ℝ} y} = (y \in (X + A, X + B) ⟼ D (y))$
66		fveq2	$⊢ y = X + s \to F (y) = F (X + s)$
67		fveq2	$⊢ y = X + s \to D (y) = D (X + s)$
68	8 8 31 32 37 38 54 65 66 67	dvmptco	$⊢ φ \to \frac{d (s \in (A, B)⟼ F (X + s))}{d_{ℝ} s} = (s \in (A, B) ⟼ D (X + s) \cdot 1)$
69	6	adantr	$⊢ (φ \land s \in (A, B)) \to D : (X + A, X + B) ⟶ ℝ$
70	69 31	ffvelcdmd	$⊢ (φ \land s \in (A, B)) \to D (X + s) \in ℝ$
71	70	recnd	$⊢ (φ \land s \in (A, B)) \to D (X + s) \in ℂ$
72	71	mulridd	$⊢ (φ \land s \in (A, B)) \to D (X + s) \cdot 1 = D (X + s)$
73	72	mpteq2dva	$⊢ φ \to (s \in (A, B) ⟼ D (X + s) \cdot 1) = (s \in (A, B) ⟼ D (X + s))$
74	68 73	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