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 ffvelrnd
 |-  ( ( 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 cncffvrn
 |-  ( ( 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 eqid
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
100 99 tgioo2
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
101 98 100 eleqtri
 |-  ( A (,) B ) e. ( ( TopOpen ` CCfld ) |`t RR )
102 101 a1i
 |-  ( ph -> ( A (,) B ) e. ( ( TopOpen ` CCfld ) |`t RR ) )
103 7 recnd
 |-  ( ph -> C e. CC )
104 40 102 103 dvmptconst
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> C ) ) = ( s e. ( A (,) B ) |-> 0 ) )
105 0cnd
 |-  ( ph -> 0 e. CC )
106 75 105 70 constcncfg
 |-  ( ph -> ( s e. ( A (,) B ) |-> 0 ) e. ( ( A (,) B ) -cn-> CC ) )
107 104 106 eqeltrd
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> C ) ) e. ( ( A (,) B ) -cn-> CC ) )
108 40 56 59 97 107 dvsubcncf
 |-  ( ph -> ( RR _D ( ( s e. ( A (,) B ) |-> ( F ` ( X + s ) ) ) oF - ( s e. ( A (,) B ) |-> C ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
109 53 108 eqeltrd
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - C ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
110 40 102 dvmptidg
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> s ) ) = ( s e. ( A (,) B ) |-> 1 ) )
111 1cnd
 |-  ( ph -> 1 e. CC )
112 75 111 70 constcncfg
 |-  ( ph -> ( s e. ( A (,) B ) |-> 1 ) e. ( ( A (,) B ) -cn-> CC ) )
113 110 112 eqeltrd
 |-  ( ph -> ( RR _D ( s e. ( A (,) B ) |-> s ) ) e. ( ( A (,) B ) -cn-> CC ) )
114 40 43 48 109 113 dvdivcncf
 |-  ( ph -> ( RR _D ( ( s e. ( A (,) B ) |-> ( ( F ` ( X + s ) ) - C ) ) oF / ( s e. ( A (,) B ) |-> s ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
115 38 114 eqeltrd
 |-  ( ph -> ( RR _D H ) e. ( ( A (,) B ) -cn-> CC ) )
116 cncff
 |-  ( ( RR _D H ) e. ( ( A (,) B ) -cn-> CC ) -> ( RR _D H ) : ( A (,) B ) --> CC )
117 fdm
 |-  ( ( RR _D H ) : ( A (,) B ) --> CC -> dom ( RR _D H ) = ( A (,) B ) )
118 115 116 117 3syl
 |-  ( ph -> dom ( RR _D H ) = ( A (,) B ) )
119 118 feq2d
 |-  ( ph -> ( ( RR _D H ) : dom ( RR _D H ) --> RR <-> ( RR _D H ) : ( A (,) B ) --> RR ) )
120 31 119 mpbid
 |-  ( ph -> ( RR _D H ) : ( A (,) B ) --> RR )
121 cncffvrn
 |-  ( ( 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 ) )
122 67 115 121 syl2anc
 |-  ( ph -> ( ( RR _D H ) e. ( ( A (,) B ) -cn-> RR ) <-> ( RR _D H ) : ( A (,) B ) --> RR ) )
123 120 122 mpbird
 |-  ( ph -> ( RR _D H ) e. ( ( A (,) B ) -cn-> RR ) )