Metamath Proof Explorer

Theorem fourierdlem59

Description: The derivative of H is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem59.f 
|- ( ph -> F : RR --> RR )
fourierdlem59.x 
|- ( ph -> X e. RR )
fourierdlem59.a 
|- ( ph -> A e. RR )
fourierdlem59.b 
|- ( ph -> B e. RR )
fourierdlem59.n0 
|- ( ph -> -. 0 e. ( A (,) B ) )
fourierdlem59.fdv 
|- ( ph -> ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) e. ( ( ( X + A ) (,) ( X + B ) ) -cn-> RR ) )
fourierdlem59.c 
|- ( ph -> C e. RR )
fourierdlem59.h 
|- H = ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / s ) )
Assertion fourierdlem59 
|- ( ph -> ( RR _D H ) e. ( ( A (,) B ) -cn-> RR ) )

Proof

Step Hyp Ref Expression
1 fourierdlem59.f 
 |-  ( ph -> F : RR --> RR )
2 fourierdlem59.x 
 |-  ( ph -> X e. RR )
3 fourierdlem59.a 
 |-  ( ph -> A e. RR )
4 fourierdlem59.b 
 |-  ( ph -> B e. RR )
5 fourierdlem59.n0 
 |-  ( ph -> -. 0 e. ( A (,) B ) )
6 fourierdlem59.fdv 
 |-  ( ph -> ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) e. ( ( ( X + A ) (,) ( X + B ) ) -cn-> RR ) )
7 fourierdlem59.c 
 |-  ( ph -> C e. RR )
8 fourierdlem59.h 
 |-  H = ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / s ) )
9 1 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> F : RR --> RR )
10 2 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> X e. RR )
11 elioore 
 |-  ( s e. ( A (,) B ) -> s e. RR )
12 11 adantl 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s e. RR )
13 10 12 readdcld 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) e. RR )
14 9 13 ffvelcdmd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( F ` ( X + s ) ) e. RR )
15 7 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> C e. RR )
16 14 15 resubcld 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( F ` ( X + s ) ) - C ) e. RR )
17 eqcom 
 |-  ( s = 0 <-> 0 = s )
18 17 biimpi 
 |-  ( s = 0 -> 0 = s )
19 18 adantl 
 |-  ( ( s e. ( A (,) B ) /\ s = 0 ) -> 0 = s )
20 simpl 
 |-  ( ( s e. ( A (,) B ) /\ s = 0 ) -> s e. ( A (,) B ) )
21 19 20 eqeltrd 
 |-  ( ( s e. ( A (,) B ) /\ s = 0 ) -> 0 e. ( A (,) B ) )
22 21 adantll 
 |-  ( ( ( ph /\ s e. ( A (,) B ) ) /\ s = 0 ) -> 0 e. ( A (,) B ) )
23 5 ad2antrr 
 |-  ( ( ( ph /\ s e. ( A (,) B ) ) /\ s = 0 ) -> -. 0 e. ( A (,) B ) )
24 22 23 pm2.65da 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> -. s = 0 )
25 24 neqned 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s =/= 0 )
26 16 12 25 redivcld 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( ( F ` ( X + s ) ) - C ) / s ) e. RR )
27 26 8 fmptd 
 |-  ( ph -> H : ( A (,) B ) --> RR )
28 ioossre 
 |-  ( A (,) B ) C_ RR
29 28 a1i 
 |-  ( ph -> ( A (,) B ) C_ RR )
30 dvfre 
 |-  ( ( H : ( A (,) B ) --> RR /\ ( A (,) B ) C_ RR ) -> ( RR _D H ) : dom ( RR _D H ) --> RR )
31 27 29 30 syl2anc 
 |-  ( ph -> ( RR _D H ) : dom ( RR _D H ) --> RR )
32 ovex 
 |-  ( A (,) B ) e. _V
33 32 a1i 
 |-  ( ph -> ( A (,) B ) e. _V )
34 eqidd 
 |-  ( ph -> ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - C ) ) = ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - C ) ) )
35 eqidd 
 |-  ( ph -> ( s e. ( A (,) B ) |-> s ) = ( s e. ( A (,) B ) |-> s ) )
36 33 16 12 34 35 offval2 
 |-  ( ph -> ( ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - C ) ) oF / ( s e. ( A (,) B ) |-> s ) ) = ( s e. ( A (,) B ) |-> ( ( ( F ` ( X + s ) ) - C ) / s ) ) )
37 8 36 eqtr4id 
 |-  ( ph -> H = ( ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - C ) ) oF / ( s e. ( A (,) B ) |-> s ) ) )
38 37 oveq2d 
 |-  ( ph -> ( RR _D H ) = ( RR _D ( ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - C ) ) oF / ( s e. ( A (,) B ) |-> s ) ) ) )
39 reelprrecn 
 |-  RR e. { RR , CC }
40 39 a1i 
 |-  ( ph -> RR e. { RR , CC } )
41 16 recnd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( ( F ` ( X + s ) ) - C ) e. CC )
42 eqid 
 |-  ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - C ) ) = ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - C ) )
43 41 42 fmptd 
 |-  ( ph -> ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - C ) ) : ( A (,) B ) --> CC )
44 12 recnd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s e. CC )
45 eldifsn 
 |-  ( s e. ( CC \ { 0 } ) <-> ( s e. CC /\ s =/= 0 ) )
46 44 25 45 sylanbrc 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s e. ( CC \ { 0 } ) )
47 eqid 
 |-  ( s e. ( A (,) B ) |-> s ) = ( s e. ( A (,) B ) |-> s )
48 46 47 fmptd 
 |-  ( ph -> ( s e. ( A (,) B ) |-> s ) : ( A (,) B ) --> ( CC \ { 0 } ) )
49 eqidd 
 |-  ( ph -> ( s e. ( A (,) B ) |-> ( F ` ( X + s ) ) ) = ( s e. ( A (,) B ) |-> ( F ` ( X + s ) ) ) )
50 eqidd 
 |-  ( ph -> ( s e. ( A (,) B ) |-> C ) = ( s e. ( A (,) B ) |-> C ) )
51 33 14 15 49 50 offval2 
 |-  ( ph -> ( ( s e. ( A (,) B ) |-> ( F ` ( X + s ) ) ) oF - ( s e. ( A (,) B ) |-> C ) ) = ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - C ) ) )
52 51 eqcomd 
 |-  ( ph -> ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - C ) ) = ( ( s e. ( A (,) B ) |-> ( F ` ( X + s ) ) ) oF - ( s e. ( A (,) B ) |-> C ) ) )
53 52 oveq2d 
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - C ) ) ) = ( RR _D ( ( s e. ( A (,) B ) |-> ( F ` ( X + s ) ) ) oF - ( s e. ( A (,) B ) |-> C ) ) ) )
54 14 recnd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( F ` ( X + s ) ) e. CC )
55 eqid 
 |-  ( s e. ( A (,) B ) |-> ( F ` ( X + s ) ) ) = ( s e. ( A (,) B ) |-> ( F ` ( X + s ) ) )
56 54 55 fmptd 
 |-  ( ph -> ( s e. ( A (,) B ) |-> ( F ` ( X + s ) ) ) : ( A (,) B ) --> CC )
57 15 recnd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> C e. CC )
58 eqid 
 |-  ( s e. ( A (,) B ) |-> C ) = ( s e. ( A (,) B ) |-> C )
59 57 58 fmptd 
 |-  ( ph -> ( s e. ( A (,) B ) |-> C ) : ( A (,) B ) --> CC )
60 eqid 
 |-  ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) = ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) )
61 cncff 
 |-  ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) e. ( ( ( X + A ) (,) ( X + B ) ) -cn-> RR ) -> ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) : ( ( X + A ) (,) ( X + B ) ) --> RR )
62 6 61 syl 
 |-  ( ph -> ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) : ( ( X + A ) (,) ( X + B ) ) --> RR )
63 1 2 3 4 60 62 fourierdlem28 
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( F ` ( X + s ) ) ) ) = ( s e. ( A (,) B ) |-> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) ) )
64 ioosscn 
 |-  ( ( X + A ) (,) ( X + B ) ) C_ CC
65 64 a1i 
 |-  ( ph -> ( ( X + A ) (,) ( X + B ) ) C_ CC )
66 ax-resscn 
 |-  RR C_ CC
67 66 a1i 
 |-  ( ph -> RR C_ CC )
68 62 67 fssd 
 |-  ( ph -> ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) : ( ( X + A ) (,) ( X + B ) ) --> CC )
69 ssid 
 |-  CC C_ CC
70 69 a1i 
 |-  ( ph -> CC C_ CC )
71 cncfcdm 
 |-  ( ( CC C_ CC /\ ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) e. ( ( ( X + A ) (,) ( X + B ) ) -cn-> RR ) ) -> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) e. ( ( ( X + A ) (,) ( X + B ) ) -cn-> CC ) <-> ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) : ( ( X + A ) (,) ( X + B ) ) --> CC ) )
72 70 6 71 syl2anc 
 |-  ( ph -> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) e. ( ( ( X + A ) (,) ( X + B ) ) -cn-> CC ) <-> ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) : ( ( X + A ) (,) ( X + B ) ) --> CC ) )
73 68 72 mpbird 
 |-  ( ph -> ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) e. ( ( ( X + A ) (,) ( X + B ) ) -cn-> CC ) )
74 ioosscn 
 |-  ( A (,) B ) C_ CC
75 74 a1i 
 |-  ( ph -> ( A (,) B ) C_ CC )
76 2 recnd 
 |-  ( ph -> X e. CC )
77 2 3 readdcld 
 |-  ( ph -> ( X + A ) e. RR )
78 77 rexrd 
 |-  ( ph -> ( X + A ) e. RR* )
79 78 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( X + A ) e. RR* )
80 2 4 readdcld 
 |-  ( ph -> ( X + B ) e. RR )
81 80 rexrd 
 |-  ( ph -> ( X + B ) e. RR* )
82 81 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( X + B ) e. RR* )
83 3 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> A e. RR )
84 83 rexrd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> A e. RR* )
85 4 rexrd 
 |-  ( ph -> B e. RR* )
86 85 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> B e. RR* )
87 simpr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s e. ( A (,) B ) )
88 ioogtlb 
 |-  ( ( A e. RR* /\ B e. RR* /\ s e. ( A (,) B ) ) -> A < s )
89 84 86 87 88 syl3anc 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> A < s )
90 83 12 10 89 ltadd2dd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( X + A ) < ( X + s ) )
91 4 adantr 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> B e. RR )
92 iooltub 
 |-  ( ( A e. RR* /\ B e. RR* /\ s e. ( A (,) B ) ) -> s < B )
93 84 86 87 92 syl3anc 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> s < B )
94 12 91 10 93 ltadd2dd 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) < ( X + B ) )
95 79 82 13 90 94 eliood 
 |-  ( ( ph /\ s e. ( A (,) B ) ) -> ( X + s ) e. ( ( X + A ) (,) ( X + B ) ) )
96 65 73 75 76 95 fourierdlem23 
 |-  ( ph -> ( s e. ( A (,) B ) |-> ( ( RR _D ( F |` ( ( X + A ) (,) ( X + B ) ) ) ) ` ( X + s ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
97 63 96 eqeltrd 
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( F ` ( X + s ) ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
98 iooretop 
 |-  ( A (,) B ) e. ( topGen ` ran (,) )
99 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
100 98 99 eleqtri 
 |-  ( A (,) B ) e. ( ( TopOpen ` CCfld ) |`t RR )
101 100 a1i 
 |-  ( ph -> ( A (,) B ) e. ( ( TopOpen ` CCfld ) |`t RR ) )
102 7 recnd 
 |-  ( ph -> C e. CC )
103 40 101 102 dvmptconst 
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> C ) ) = ( s e. ( A (,) B ) |-> 0 ) )
104 0cnd 
 |-  ( ph -> 0 e. CC )
105 75 104 70 constcncfg 
 |-  ( ph -> ( s e. ( A (,) B ) |-> 0 ) e. ( ( A (,) B ) -cn-> CC ) )
106 103 105 eqeltrd 
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> C ) ) e. ( ( A (,) B ) -cn-> CC ) )
107 40 56 59 97 106 dvsubcncf 
 |-  ( ph -> ( RR _D ( ( s e. ( A (,) B ) |-> ( F ` ( X + s ) ) ) oF - ( s e. ( A (,) B ) |-> C ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
108 53 107 eqeltrd 
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - C ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
109 40 101 dvmptidg 
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> s ) ) = ( s e. ( A (,) B ) |-> 1 ) )
110 1cnd 
 |-  ( ph -> 1 e. CC )
111 75 110 70 constcncfg 
 |-  ( ph -> ( s e. ( A (,) B ) |-> 1 ) e. ( ( A (,) B ) -cn-> CC ) )
112 109 111 eqeltrd 
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> s ) ) e. ( ( A (,) B ) -cn-> CC ) )
113 40 43 48 108 112 dvdivcncf 
 |-  ( ph -> ( RR _D ( ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - C ) ) oF / ( s e. ( A (,) B ) |-> s ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
114 38 113 eqeltrd 
 |-  ( ph -> ( RR _D H ) e. ( ( A (,) B ) -cn-> CC ) )
115 cncff 
 |-  ( ( RR _D H ) e. ( ( A (,) B ) -cn-> CC ) -> ( RR _D H ) : ( A (,) B ) --> CC )
116 fdm 
 |-  ( ( RR _D H ) : ( A (,) B ) --> CC -> dom ( RR _D H ) = ( A (,) B ) )
117 114 115 116 3syl 
 |-  ( ph -> dom ( RR _D H ) = ( A (,) B ) )
118 117 feq2d 
 |-  ( ph -> ( ( RR _D H ) : dom ( RR _D H ) --> RR <-> ( RR _D H ) : ( A (,) B ) --> RR ) )
119 31 118 mpbid 
 |-  ( ph -> ( RR _D H ) : ( A (,) B ) --> RR )
120 cncfcdm 
 |-  ( ( RR C_ CC /\ ( RR _D H ) e. ( ( A (,) B ) -cn-> CC ) ) -> ( ( RR _D H ) e. ( ( A (,) B ) -cn-> RR ) <-> ( RR _D H ) : ( A (,) B ) --> RR ) )
121 67 114 120 syl2anc 
 |-  ( ph -> ( ( RR _D H ) e. ( ( A (,) B ) -cn-> RR ) <-> ( RR _D H ) : ( A (,) B ) --> RR ) )
122 119 121 mpbird 
 |-  ( ph -> ( RR _D H ) e. ( ( A (,) B ) -cn-> RR ) )