Theorem fourierdlem28

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

	Ref	Expression
Hypotheses	fourierdlem28.1	|- ( ph -> F : RR --> RR )
	fourierdlem28.x	|- ( ph -> X e. RR )
	fourierdlem28.a	|- ( ph -> A e. RR )
	fourierdlem28.3b	|- ( ph -> B e. RR )
	fourierdlem28.d	|- D = ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) )
	fourierdlem28.df	|- ( ph -> D : ( ( X + A ) (,) ( X + B ) ) --> RR )
Assertion	fourierdlem28	|- ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( F ` ( X + s ) ) ) ) = ( s e. ( A (,) B ) |-> ( D ` ( X + s ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem28.1	|- ( ph -> F : RR --> RR )
2		fourierdlem28.x	|- ( ph -> X e. RR )
3		fourierdlem28.a	|- ( ph -> A e. RR )
4		fourierdlem28.3b	|- ( ph -> B e. RR )
5		fourierdlem28.d	|- D = ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) )
6		fourierdlem28.df	|- ( ph -> D : ( ( X + A ) (,) ( X + B ) ) --> RR )
7		reelprrecn	|- RR e. { RR , CC }
8	7	a1i	|- ( ph -> RR e. { RR , CC } )
9	2 3	readdcld	|- ( ph -> ( X + A ) e. RR )
10	9	rexrd	|- ( ph -> ( X + A ) e. RR* )
11	10	adantr	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( X + A ) e. RR* )
12	2 4	readdcld	|- ( ph -> ( X + B ) e. RR )
13	12	rexrd	|- ( ph -> ( X + B ) e. RR* )
14	13	adantr	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( X + B ) e. RR* )
15	2	adantr	|- ( ( ph /\ s e. ( A (,) B ) ) -> X e. RR )
16		elioore	|- ( s e. ( A (,) B ) -> s e. RR )
17	16	adantl	|- ( ( ph /\ s e. ( A (,) B ) ) -> s e. RR )
18	15 17	readdcld	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) e. RR )
19	3	adantr	|- ( ( ph /\ s e. ( A (,) B ) ) -> A e. RR )
20	19	rexrd	|- ( ( ph /\ s e. ( A (,) B ) ) -> A e. RR* )
21	4	rexrd	|- ( ph -> B e. RR* )
22	21	adantr	|- ( ( ph /\ s e. ( A (,) B ) ) -> B e. RR* )
23		simpr	|- ( ( ph /\ s e. ( A (,) B ) ) -> s e. ( A (,) B ) )
24		ioogtlb	|- ( ( A e. RR* /\ B e. RR* /\ s e. ( A (,) B ) ) -> A < s )
25	20 22 23 24	syl3anc	|- ( ( ph /\ s e. ( A (,) B ) ) -> A < s )
26	19 17 15 25	ltadd2dd	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( X + A ) < ( X + s ) )
27	4	adantr	|- ( ( ph /\ s e. ( A (,) B ) ) -> B e. RR )
28		iooltub	|- ( ( A e. RR* /\ B e. RR* /\ s e. ( A (,) B ) ) -> s < B )
29	20 22 23 28	syl3anc	|- ( ( ph /\ s e. ( A (,) B ) ) -> s < B )
30	17 27 15 29	ltadd2dd	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) < ( X + B ) )
31	11 14 18 26 30	eliood	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) e. ( ( X + A ) (,) ( X + B ) ) )
32		1red	|- ( ( ph /\ s e. ( A (,) B ) ) -> 1 e. RR )
33	1	adantr	|- ( ( ph /\ y e. ( ( X + A ) (,) ( X + B ) ) ) -> F : RR --> RR )
34		elioore	|- ( y e. ( ( X + A ) (,) ( X + B ) ) -> y e. RR )
35	34	adantl	|- ( ( ph /\ y e. ( ( X + A ) (,) ( X + B ) ) ) -> y e. RR )
36	33 35	ffvelrnd	|- ( ( ph /\ y e. ( ( X + A ) (,) ( X + B ) ) ) -> ( F ` y ) e. RR )
37	36	recnd	|- ( ( ph /\ y e. ( ( X + A ) (,) ( X + B ) ) ) -> ( F ` y ) e. CC )
38	6	ffvelrnda	|- ( ( ph /\ y e. ( ( X + A ) (,) ( X + B ) ) ) -> ( D ` y ) e. RR )
39	15	recnd	|- ( ( ph /\ s e. ( A (,) B ) ) -> X e. CC )
40		0red	|- ( ( ph /\ s e. ( A (,) B ) ) -> 0 e. RR )
41		iooretop	|- ( A (,) B ) e. ( topGen ` ran (,) )
42		eqid	|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
43	42	tgioo2	|- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
44	41 43	eleqtri	|- ( A (,) B ) e. ( ( TopOpen ` CCfld ) |`t RR )
45	44	a1i	|- ( ph -> ( A (,) B ) e. ( ( TopOpen ` CCfld ) |`t RR ) )
46	2	recnd	|- ( ph -> X e. CC )
47	8 45 46	dvmptconst	|- ( ph -> ( RR _D ( s e. ( A (,) B ) |-> X ) ) = ( s e. ( A (,) B ) |-> 0 ) )
48	17	recnd	|- ( ( ph /\ s e. ( A (,) B ) ) -> s e. CC )
49	8 45	dvmptidg	|- ( ph -> ( RR _D ( s e. ( A (,) B ) |-> s ) ) = ( s e. ( A (,) B ) |-> 1 ) )
50	8 39 40 47 48 32 49	dvmptadd	|- ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( X + s ) ) ) = ( s e. ( A (,) B ) |-> ( 0 + 1 ) ) )
51		0p1e1	|- ( 0 + 1 ) = 1
52	51	a1i	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( 0 + 1 ) = 1 )
53	52	mpteq2dva	|- ( ph -> ( s e. ( A (,) B ) |-> ( 0 + 1 ) ) = ( s e. ( A (,) B ) |-> 1 ) )
54	50 53	eqtrd	|- ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( X + s ) ) ) = ( s e. ( A (,) B ) |-> 1 ) )
55	1	feqmptd	|- ( ph -> F = ( y e. RR |-> ( F ` y ) ) )
56	55	reseq1d	|- ( ph -> ( F |` ( ( X + A ) (,) ( X + B ) ) ) = ( ( y e. RR |-> ( F ` y ) ) |` ( ( X + A ) (,) ( X + B ) ) ) )
57		ioossre	|- ( ( X + A ) (,) ( X + B ) ) C_ RR
58	57	a1i	|- ( ph -> ( ( X + A ) (,) ( X + B ) ) C_ RR )
59	58	resmptd	|- ( ph -> ( ( y e. RR |-> ( F ` y ) ) |` ( ( X + A ) (,) ( X + B ) ) ) = ( y e. ( ( X + A ) (,) ( X + B ) ) |-> ( F ` y ) ) )
60	56 59	eqtr2d	|- ( ph -> ( y e. ( ( X + A ) (,) ( X + B ) ) |-> ( F ` y ) ) = ( F |` ( ( X + A ) (,) ( X + B ) ) ) )
61	60	oveq2d	|- ( ph -> ( RR _D ( y e. ( ( X + A ) (,) ( X + B ) ) |-> ( F ` y ) ) ) = ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) )
62	5	eqcomi	|- ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) = D
63	62	a1i	|- ( ph -> ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) = D )
64	6	feqmptd	|- ( ph -> D = ( y e. ( ( X + A ) (,) ( X + B ) ) |-> ( D ` y ) ) )
65	61 63 64	3eqtrd	|- ( ph -> ( RR _D ( y e. ( ( X + A ) (,) ( X + B ) ) |-> ( F ` y ) ) ) = ( y e. ( ( X + A ) (,) ( X + B ) ) |-> ( D ` y ) ) )
66		fveq2	|- ( y = ( X + s ) -> ( F ` y ) = ( F ` ( X + s ) ) )
67		fveq2	|- ( y = ( X + s ) -> ( D ` y ) = ( D ` ( X + s ) ) )
68	8 8 31 32 37 38 54 65 66 67	dvmptco	|- ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( F ` ( X + s ) ) ) ) = ( s e. ( A (,) B ) |-> ( ( D ` ( X + s ) ) x. 1 ) ) )
69	6	adantr	|- ( ( ph /\ s e. ( A (,) B ) ) -> D : ( ( X + A ) (,) ( X + B ) ) --> RR )
70	69 31	ffvelrnd	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( D ` ( X + s ) ) e. RR )
71	70	recnd	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( D ` ( X + s ) ) e. CC )
72	71	mulid1d	|- ( ( ph /\ s e. ( A (,) B ) ) -> ( ( D ` ( X + s ) ) x. 1 ) = ( D ` ( X + s ) ) )
73	72	mpteq2dva	|- ( ph -> ( s e. ( A (,) B ) |-> ( ( D ` ( X + s ) ) x. 1 ) ) = ( s e. ( A (,) B ) |-> ( D ` ( X + s ) ) ) )
74	68 73	eqtrd	|- ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( F ` ( X + s ) ) ) ) = ( s e. ( A (,) B ) |-> ( D ` ( X + s ) ) ) )