This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmda 
 |-  ( ( 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 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
43 41 42 eleqtri 
 |-  ( A (,) B ) e. ( ( TopOpen ` CCfld ) |`t RR )
44 43 a1i 
 |-  ( ph -> ( A (,) B ) e. ( ( TopOpen ` CCfld ) |`t RR ) )
45 2 recnd 
 |-  ( ph -> X e. CC )
46 8 44 45 dvmptconst 
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> X ) ) = ( s e. ( A (,) B ) |-> 0 ) )
47 17 recnd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s e. CC )
48 8 44 dvmptidg 
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> s ) ) = ( s e. ( A (,) B ) |-> 1 ) )
49 8 39 40 46 47 32 48 dvmptadd 
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( X + s ) ) ) = ( s e. ( A (,) B ) |-> ( 0 + 1 ) ) )
50 0p1e1 
 |-  ( 0 + 1 ) = 1
51 50 a1i 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( 0 + 1 ) = 1 )
52 51 mpteq2dva 
 |-  ( ph -> ( s e. ( A (,) B ) |-> ( 0 + 1 ) ) = ( s e. ( A (,) B ) |-> 1 ) )
53 49 52 eqtrd 
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( X + s ) ) ) = ( s e. ( A (,) B ) |-> 1 ) )
54 1 feqmptd 
 |-  ( ph -> F = ( y e. RR |-> ( F ` y ) ) )
55 54 reseq1d 
 |-  ( ph -> ( F |` ( ( X + A ) (,) ( X + B ) ) ) = ( ( y e. RR |-> ( F ` y ) ) |` ( ( X + A ) (,) ( X + B ) ) ) )
56 ioossre 
 |-  ( ( X + A ) (,) ( X + B ) ) C_ RR
57 56 a1i 
 |-  ( ph -> ( ( X + A ) (,) ( X + B ) ) C_ RR )
58 57 resmptd 
 |-  ( ph -> ( ( y e. RR |-> ( F ` y ) ) |` ( ( X + A ) (,) ( X + B ) ) ) = ( y e. ( ( X + A ) (,) ( X + B ) ) |-> ( F ` y ) ) )
59 55 58 eqtr2d 
 |-  ( ph -> ( y e. ( ( X + A ) (,) ( X + B ) ) |-> ( F ` y ) ) = ( F |` ( ( X + A ) (,) ( X + B ) ) ) )
60 59 oveq2d 
 |-  ( ph -> ( RR _D ( y e. ( ( X + A ) (,) ( X + B ) ) |-> ( F ` y ) ) ) = ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) )
61 5 eqcomi 
 |-  ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) = D
62 61 a1i 
 |-  ( ph -> ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) = D )
63 6 feqmptd 
 |-  ( ph -> D = ( y e. ( ( X + A ) (,) ( X + B ) ) |-> ( D ` y ) ) )
64 60 62 63 3eqtrd 
 |-  ( ph -> ( RR _D ( y e. ( ( X + A ) (,) ( X + B ) ) |-> ( F ` y ) ) ) = ( y e. ( ( X + A ) (,) ( X + B ) ) |-> ( D ` y ) ) )
65 fveq2 
 |-  ( y = ( X + s ) -> ( F ` y ) = ( F ` ( X + s ) ) )
66 fveq2 
 |-  ( y = ( X + s ) -> ( D ` y ) = ( D ` ( X + s ) ) )
67 8 8 31 32 37 38 53 64 65 66 dvmptco 
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( F ` ( X + s ) ) ) ) = ( s e. ( A (,) B ) |-> ( ( D ` ( X + s ) ) x. 1 ) ) )
68 6 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> D : ( ( X + A ) (,) ( X + B ) ) --> RR )
69 68 31 ffvelcdmd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( D ` ( X + s ) ) e. RR )
70 69 recnd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( D ` ( X + s ) ) e. CC )
71 70 mulridd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( D ` ( X + s ) ) x. 1 ) = ( D ` ( X + s ) ) )
72 71 mpteq2dva 
 |-  ( ph -> ( s e. ( A (,) B ) |-> ( ( D ` ( X + s ) ) x. 1 ) ) = ( s e. ( A (,) B ) |-> ( D ` ( X + s ) ) ) )
73 67 72 eqtrd 
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( F ` ( X + s ) ) ) ) = ( s e. ( A (,) B ) |-> ( D ` ( X + s ) ) ) )