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