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 φ F :
fourierdlem59.x φ X
fourierdlem59.a φ A
fourierdlem59.b φ B
fourierdlem59.n0 φ ¬ 0 A B
fourierdlem59.fdv φ F X + A X + B : X + A X + B cn
fourierdlem59.c φ C
fourierdlem59.h H = s A B F X + s C s
Assertion fourierdlem59 φ H : A B cn

Proof

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