Metamath Proof Explorer


Theorem fourierdlem58

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

Ref Expression
Hypotheses fourierdlem58.k K = s A s 2 sin s 2
fourierdlem58.ass φ A π π
fourierdlem58.0nA φ ¬ 0 A
fourierdlem58.4 φ A topGen ran .
Assertion fourierdlem58 φ K : A cn

Proof

Step Hyp Ref Expression
1 fourierdlem58.k K = s A s 2 sin s 2
2 fourierdlem58.ass φ A π π
3 fourierdlem58.0nA φ ¬ 0 A
4 fourierdlem58.4 φ A topGen ran .
5 pire π
6 5 a1i φ s A π
7 6 renegcld φ s A π
8 7 6 iccssred φ s A π π
9 2 sselda φ s A s π π
10 8 9 sseldd φ s A s
11 2re 2
12 11 a1i φ s A 2
13 10 rehalfcld φ s A s 2
14 13 resincld φ s A sin s 2
15 12 14 remulcld φ s A 2 sin s 2
16 2cnd φ s A 2
17 10 recnd φ s A s
18 17 halfcld φ s A s 2
19 18 sincld φ s A sin s 2
20 2ne0 2 0
21 20 a1i φ s A 2 0
22 eqcom s = 0 0 = s
23 22 biimpi s = 0 0 = s
24 23 adantl s A s = 0 0 = s
25 simpl s A s = 0 s A
26 24 25 eqeltrd s A s = 0 0 A
27 26 adantll φ s A s = 0 0 A
28 3 ad2antrr φ s A s = 0 ¬ 0 A
29 27 28 pm2.65da φ s A ¬ s = 0
30 29 neqned φ s A s 0
31 fourierdlem44 s π π s 0 sin s 2 0
32 9 30 31 syl2anc φ s A sin s 2 0
33 16 19 21 32 mulne0d φ s A 2 sin s 2 0
34 10 15 33 redivcld φ s A s 2 sin s 2
35 34 1 fmptd φ K : A
36 5 a1i φ π
37 36 renegcld φ π
38 37 36 iccssred φ π π
39 2 38 sstrd φ A
40 dvfre K : A A K : dom K
41 35 39 40 syl2anc φ K : dom K
42 eqidd φ s A s = s A s
43 eqidd φ s A 2 sin s 2 = s A 2 sin s 2
44 4 10 15 42 43 offval2 φ s A s ÷ f s A 2 sin s 2 = s A s 2 sin s 2
45 1 44 eqtr4id φ K = s A s ÷ f s A 2 sin s 2
46 45 oveq2d φ D K = D s A s ÷ f s A 2 sin s 2
47 reelprrecn
48 47 a1i φ
49 eqid s A s = s A s
50 17 49 fmptd φ s A s : A
51 16 19 mulcld φ s A 2 sin s 2
52 33 neneqd φ s A ¬ 2 sin s 2 = 0
53 elsng 2 sin s 2 2 sin s 2 0 2 sin s 2 = 0
54 15 53 syl φ s A 2 sin s 2 0 2 sin s 2 = 0
55 52 54 mtbird φ s A ¬ 2 sin s 2 0
56 51 55 eldifd φ s A 2 sin s 2 0
57 eqid s A 2 sin s 2 = s A 2 sin s 2
58 56 57 fmptd φ s A 2 sin s 2 : A 0
59 eqid TopOpen fld = TopOpen fld
60 59 tgioo2 topGen ran . = TopOpen fld 𝑡
61 4 60 eleqtrdi φ A TopOpen fld 𝑡
62 48 61 dvmptidg φ ds A s d s = s A 1
63 ax-resscn
64 63 a1i φ
65 39 64 sstrd φ A
66 1cnd φ 1
67 ssid
68 67 a1i φ
69 65 66 68 constcncfg φ s A 1 : A cn
70 62 69 eqeltrd φ ds A s d s : A cn
71 39 resmptd φ s 2 sin s 2 A = s A 2 sin s 2
72 71 eqcomd φ s A 2 sin s 2 = s 2 sin s 2 A
73 72 oveq2d φ ds A 2 sin s 2 d s = D s 2 sin s 2 A
74 eqid s 2 sin s 2 = s 2 sin s 2
75 2cnd s 2
76 recn s s
77 76 halfcld s s 2
78 77 sincld s sin s 2
79 75 78 mulcld s 2 sin s 2
80 74 79 fmpti s 2 sin s 2 :
81 80 a1i φ s 2 sin s 2 :
82 ssid
83 82 a1i φ
84 59 60 dvres s 2 sin s 2 : A D s 2 sin s 2 A = ds 2 sin s 2 d s int topGen ran . A
85 64 81 83 39 84 syl22anc φ D s 2 sin s 2 A = ds 2 sin s 2 d s int topGen ran . A
86 retop topGen ran . Top
87 86 a1i φ topGen ran . Top
88 uniretop = topGen ran .
89 88 isopn3 topGen ran . Top A A topGen ran . int topGen ran . A = A
90 87 39 89 syl2anc φ A topGen ran . int topGen ran . A = A
91 4 90 mpbid φ int topGen ran . A = A
92 91 reseq2d φ ds 2 sin s 2 d s int topGen ran . A = ds 2 sin s 2 d s A
93 resmpt s 2 sin 1 2 s = s 2 sin 1 2 s
94 63 93 ax-mp s 2 sin 1 2 s = s 2 sin 1 2 s
95 id s s
96 2cnd s 2
97 20 a1i s 2 0
98 95 96 97 divrec2d s s 2 = 1 2 s
99 98 eqcomd s 1 2 s = s 2
100 76 99 syl s 1 2 s = s 2
101 100 fveq2d s sin 1 2 s = sin s 2
102 101 oveq2d s 2 sin 1 2 s = 2 sin s 2
103 102 mpteq2ia s 2 sin 1 2 s = s 2 sin s 2
104 94 103 eqtr2i s 2 sin s 2 = s 2 sin 1 2 s
105 104 oveq2i ds 2 sin s 2 d s = D s 2 sin 1 2 s
106 eqid s 2 sin 1 2 s = s 2 sin 1 2 s
107 halfcn 1 2
108 107 a1i s 1 2
109 108 95 mulcld s 1 2 s
110 109 sincld s sin 1 2 s
111 96 110 mulcld s 2 sin 1 2 s
112 106 111 fmpti s 2 sin 1 2 s :
113 2cn 2
114 dvasinbx 2 1 2 ds 2 sin 1 2 s d s = s 2 1 2 cos 1 2 s
115 113 107 114 mp2an ds 2 sin 1 2 s d s = s 2 1 2 cos 1 2 s
116 113 20 recidi 2 1 2 = 1
117 116 a1i s 2 1 2 = 1
118 99 fveq2d s cos 1 2 s = cos s 2
119 117 118 oveq12d s 2 1 2 cos 1 2 s = 1 cos s 2
120 halfcl s s 2
121 120 coscld s cos s 2
122 121 mulid2d s 1 cos s 2 = cos s 2
123 119 122 eqtrd s 2 1 2 cos 1 2 s = cos s 2
124 123 mpteq2ia s 2 1 2 cos 1 2 s = s cos s 2
125 115 124 eqtri ds 2 sin 1 2 s d s = s cos s 2
126 125 dmeqi dom ds 2 sin 1 2 s d s = dom s cos s 2
127 dmmptg s cos s 2 dom s cos s 2 =
128 127 121 mprg dom s cos s 2 =
129 126 128 eqtri dom ds 2 sin 1 2 s d s =
130 63 129 sseqtrri dom ds 2 sin 1 2 s d s
131 dvres3 s 2 sin 1 2 s : dom ds 2 sin 1 2 s d s D s 2 sin 1 2 s = ds 2 sin 1 2 s d s
132 47 112 67 130 131 mp4an D s 2 sin 1 2 s = ds 2 sin 1 2 s d s
133 125 reseq1i ds 2 sin 1 2 s d s = s cos s 2
134 105 132 133 3eqtri ds 2 sin s 2 d s = s cos s 2
135 134 reseq1i ds 2 sin s 2 d s A = s cos s 2 A
136 135 a1i φ ds 2 sin s 2 d s A = s cos s 2 A
137 39 resabs1d φ s cos s 2 A = s cos s 2 A
138 65 resmptd φ s cos s 2 A = s A cos s 2
139 137 138 eqtrd φ s cos s 2 A = s A cos s 2
140 92 136 139 3eqtrd φ ds 2 sin s 2 d s int topGen ran . A = s A cos s 2
141 73 85 140 3eqtrd φ ds A 2 sin s 2 d s = s A cos s 2
142 coscn cos : cn
143 142 a1i φ cos : cn
144 65 68 idcncfg φ s A s : A cn
145 2cnd φ 2
146 20 a1i φ 2 0
147 eldifsn 2 0 2 2 0
148 145 146 147 sylanbrc φ 2 0
149 difssd φ 0
150 65 148 149 constcncfg φ s A 2 : A cn 0
151 144 150 divcncf φ s A s 2 : A cn
152 143 151 cncfmpt1f φ s A cos s 2 : A cn
153 141 152 eqeltrd φ ds A 2 sin s 2 d s : A cn
154 48 50 58 70 153 dvdivcncf φ s A s ÷ f s A 2 sin s 2 : A cn
155 46 154 eqeltrd φ K : A cn
156 cncff K : A cn K : A
157 fdm K : A dom K = A
158 155 156 157 3syl φ dom K = A
159 158 feq2d φ K : dom K K : A
160 41 159 mpbid φ K : A
161 cncffvrn K : A cn K : A cn K : A
162 64 155 161 syl2anc φ K : A cn K : A
163 160 162 mpbird φ K : A cn