Metamath Proof Explorer


Theorem areacirclem4

Description: Endpoint-inclusive continuity of antiderivative of cross-section of circle. (Contributed by Brendan Leahy, 31-Aug-2017) (Revised by Brendan Leahy, 11-Jul-2018)

Ref Expression
Assertion areacirclem4 R + t R R R 2 arcsin t R + t R 1 t R 2 : R R cn

Proof

Step Hyp Ref Expression
1 rpcn R + R
2 1 sqcld R + R 2
3 rpre R + R
4 3 renegcld R + R
5 iccssre R R R R
6 4 3 5 syl2anc R + R R
7 ax-resscn
8 6 7 sstrdi R + R R
9 ssid
10 9 a1i R +
11 cncfmptc R 2 R R t R R R 2 : R R cn
12 2 8 10 11 syl3anc R + t R R R 2 : R R cn
13 eqid TopOpen fld = TopOpen fld
14 13 addcn + TopOpen fld × t TopOpen fld Cn TopOpen fld
15 14 a1i R + + TopOpen fld × t TopOpen fld Cn TopOpen fld
16 8 sselda R + t R R t
17 1 adantr R + t R R R
18 rpne0 R + R 0
19 18 adantr R + t R R R 0
20 16 17 19 divcld R + t R R t R
21 asinval t R arcsin t R = i log i t R + 1 t R 2
22 20 21 syl R + t R R arcsin t R = i log i t R + 1 t R 2
23 ax-icn i
24 23 a1i R + t R R i
25 24 20 mulcld R + t R R i t R
26 1cnd R + t R R 1
27 20 sqcld R + t R R t R 2
28 26 27 subcld R + t R R 1 t R 2
29 28 sqrtcld R + t R R 1 t R 2
30 25 29 addcld R + t R R i t R + 1 t R 2
31 0lt1 0 < 1
32 simp3 R + t R R t = 0 t = 0
33 32 oveq1d R + t R R t = 0 t R = 0 R
34 1 18 div0d R + 0 R = 0
35 34 3ad2ant1 R + t R R t = 0 0 R = 0
36 33 35 eqtrd R + t R R t = 0 t R = 0
37 36 oveq2d R + t R R t = 0 i t R = i 0
38 it0e0 i 0 = 0
39 37 38 eqtrdi R + t R R t = 0 i t R = 0
40 36 oveq1d R + t R R t = 0 t R 2 = 0 2
41 40 oveq2d R + t R R t = 0 1 t R 2 = 1 0 2
42 41 fveq2d R + t R R t = 0 1 t R 2 = 1 0 2
43 sq0 0 2 = 0
44 43 oveq2i 1 0 2 = 1 0
45 1m0e1 1 0 = 1
46 44 45 eqtri 1 0 2 = 1
47 46 fveq2i 1 0 2 = 1
48 sqrt1 1 = 1
49 47 48 eqtri 1 0 2 = 1
50 42 49 eqtrdi R + t R R t = 0 1 t R 2 = 1
51 39 50 oveq12d R + t R R t = 0 i t R + 1 t R 2 = 0 + 1
52 0p1e1 0 + 1 = 1
53 51 52 eqtrdi R + t R R t = 0 i t R + 1 t R 2 = 1
54 53 breq2d R + t R R t = 0 0 < i t R + 1 t R 2 0 < 1
55 0red R + t R R t = 0 0
56 1red R + t R R t = 0 1
57 53 56 eqeltrd R + t R R t = 0 i t R + 1 t R 2
58 55 57 ltnled R + t R R t = 0 0 < i t R + 1 t R 2 ¬ i t R + 1 t R 2 0
59 54 58 bitr3d R + t R R t = 0 0 < 1 ¬ i t R + 1 t R 2 0
60 31 59 mpbii R + t R R t = 0 ¬ i t R + 1 t R 2 0
61 60 3expa R + t R R t = 0 ¬ i t R + 1 t R 2 0
62 61 olcd R + t R R t = 0 ¬ i t R + 1 t R 2 ¬ i t R + 1 t R 2 0
63 inelr ¬ i
64 25 29 pncand R + t R R i t R + 1 t R 2 - 1 t R 2 = i t R
65 64 3adant3 R + t R R t 0 i t R + 1 t R 2 - 1 t R 2 = i t R
66 65 oveq1d R + t R R t 0 i t R + 1 t R 2 - 1 t R 2 R t = i t R R t
67 23 a1i R + t R R t 0 i
68 20 3adant3 R + t R R t 0 t R
69 1 3ad2ant1 R + t R R t 0 R
70 16 3adant3 R + t R R t 0 t
71 simp3 R + t R R t 0 t 0
72 69 70 71 divcld R + t R R t 0 R t
73 67 68 72 mulassd R + t R R t 0 i t R R t = i t R R t
74 66 73 eqtrd R + t R R t 0 i t R + 1 t R 2 - 1 t R 2 R t = i t R R t
75 18 3ad2ant1 R + t R R t 0 R 0
76 70 69 71 75 divcan6d R + t R R t 0 t R R t = 1
77 76 oveq2d R + t R R t 0 i t R R t = i 1
78 67 mulid1d R + t R R t 0 i 1 = i
79 74 77 78 3eqtrrd R + t R R t 0 i = i t R + 1 t R 2 - 1 t R 2 R t
80 79 adantr R + t R R t 0 i t R + 1 t R 2 i = i t R + 1 t R 2 - 1 t R 2 R t
81 simpr R + t R R t 0 i t R + 1 t R 2 i t R + 1 t R 2
82 1red R + t R R 1
83 6 sselda R + t R R t
84 3 adantr R + t R R R
85 83 84 19 redivcld R + t R R t R
86 85 resqcld R + t R R t R 2
87 82 86 resubcld R + t R R 1 t R 2
88 elicc2 R R t R R t R t t R
89 4 3 88 syl2anc R + t R R t R t t R
90 1red R + t 1
91 simpr R + t t
92 3 adantr R + t R
93 18 adantr R + t R 0
94 91 92 93 redivcld R + t t R
95 94 resqcld R + t t R 2
96 90 95 subge0d R + t 0 1 t R 2 t R 2 1
97 recn t t
98 97 adantl R + t t
99 1 adantr R + t R
100 98 99 93 sqdivd R + t t R 2 = t 2 R 2
101 100 breq1d R + t t R 2 1 t 2 R 2 1
102 resqcl t t 2
103 102 adantl R + t t 2
104 3 resqcld R + R 2
105 rpgt0 R + 0 < R
106 0red R + 0
107 0le0 0 0
108 107 a1i R + 0 0
109 rpge0 R + 0 R
110 106 3 108 109 lt2sqd R + 0 < R 0 2 < R 2
111 43 a1i R + 0 2 = 0
112 111 breq1d R + 0 2 < R 2 0 < R 2
113 110 112 bitrd R + 0 < R 0 < R 2
114 105 113 mpbid R + 0 < R 2
115 104 114 elrpd R + R 2 +
116 115 adantr R + t R 2 +
117 103 90 116 ledivmuld R + t t 2 R 2 1 t 2 R 2 1
118 absresq t t 2 = t 2
119 118 eqcomd t t 2 = t 2
120 2 mulid1d R + R 2 1 = R 2
121 119 120 breqan12rd R + t t 2 R 2 1 t 2 R 2
122 97 abscld t t
123 122 adantl R + t t
124 97 absge0d t 0 t
125 124 adantl R + t 0 t
126 109 adantr R + t 0 R
127 123 92 125 126 le2sqd R + t t R t 2 R 2
128 91 92 absled R + t t R R t t R
129 121 127 128 3bitr2d R + t t 2 R 2 1 R t t R
130 117 129 bitrd R + t t 2 R 2 1 R t t R
131 96 101 130 3bitrrd R + t R t t R 0 1 t R 2
132 131 biimpd R + t R t t R 0 1 t R 2
133 132 exp4b R + t R t t R 0 1 t R 2
134 133 3impd R + t R t t R 0 1 t R 2
135 89 134 sylbid R + t R R 0 1 t R 2
136 135 imp R + t R R 0 1 t R 2
137 87 136 resqrtcld R + t R R 1 t R 2
138 137 3adant3 R + t R R t 0 1 t R 2
139 138 adantr R + t R R t 0 i t R + 1 t R 2 1 t R 2
140 81 139 resubcld R + t R R t 0 i t R + 1 t R 2 i t R + 1 t R 2 - 1 t R 2
141 3 3ad2ant1 R + t R R t 0 R
142 83 3adant3 R + t R R t 0 t
143 141 142 71 redivcld R + t R R t 0 R t
144 143 adantr R + t R R t 0 i t R + 1 t R 2 R t
145 140 144 remulcld R + t R R t 0 i t R + 1 t R 2 i t R + 1 t R 2 - 1 t R 2 R t
146 80 145 eqeltrd R + t R R t 0 i t R + 1 t R 2 i
147 146 ex R + t R R t 0 i t R + 1 t R 2 i
148 147 3expa R + t R R t 0 i t R + 1 t R 2 i
149 63 148 mtoi R + t R R t 0 ¬ i t R + 1 t R 2
150 149 orcd R + t R R t 0 ¬ i t R + 1 t R 2 ¬ i t R + 1 t R 2 0
151 62 150 pm2.61dane R + t R R ¬ i t R + 1 t R 2 ¬ i t R + 1 t R 2 0
152 ianor ¬ i t R + 1 t R 2 i t R + 1 t R 2 0 ¬ i t R + 1 t R 2 ¬ i t R + 1 t R 2 0
153 151 152 sylibr R + t R R ¬ i t R + 1 t R 2 i t R + 1 t R 2 0
154 mnfxr −∞ *
155 0re 0
156 elioc2 −∞ * 0 i t R + 1 t R 2 −∞ 0 i t R + 1 t R 2 −∞ < i t R + 1 t R 2 i t R + 1 t R 2 0
157 154 155 156 mp2an i t R + 1 t R 2 −∞ 0 i t R + 1 t R 2 −∞ < i t R + 1 t R 2 i t R + 1 t R 2 0
158 3simpb i t R + 1 t R 2 −∞ < i t R + 1 t R 2 i t R + 1 t R 2 0 i t R + 1 t R 2 i t R + 1 t R 2 0
159 157 158 sylbi i t R + 1 t R 2 −∞ 0 i t R + 1 t R 2 i t R + 1 t R 2 0
160 153 159 nsyl R + t R R ¬ i t R + 1 t R 2 −∞ 0
161 30 160 eldifd R + t R R i t R + 1 t R 2 −∞ 0
162 fvres i t R + 1 t R 2 −∞ 0 log −∞ 0 i t R + 1 t R 2 = log i t R + 1 t R 2
163 161 162 syl R + t R R log −∞ 0 i t R + 1 t R 2 = log i t R + 1 t R 2
164 163 oveq2d R + t R R i log −∞ 0 i t R + 1 t R 2 = i log i t R + 1 t R 2
165 22 164 eqtr4d R + t R R arcsin t R = i log −∞ 0 i t R + 1 t R 2
166 165 mpteq2dva R + t R R arcsin t R = t R R i log −∞ 0 i t R + 1 t R 2
167 negicn i
168 167 a1i R + i
169 cncfmptc i R R t R R i : R R cn
170 168 8 10 169 syl3anc R + t R R i : R R cn
171 13 cnfldtopon TopOpen fld TopOn
172 171 a1i R + TopOpen fld TopOn
173 resttopon TopOpen fld TopOn R R TopOpen fld 𝑡 R R TopOn R R
174 172 8 173 syl2anc R + TopOpen fld 𝑡 R R TopOn R R
175 161 fmpttd R + t R R i t R + 1 t R 2 : R R −∞ 0
176 difssd R + −∞ 0
177 16 17 19 divrec2d R + t R R t R = 1 R t
178 177 oveq2d R + t R R i t R = i 1 R t
179 1 18 reccld R + 1 R
180 179 adantr R + t R R 1 R
181 24 180 16 mulassd R + t R R i 1 R t = i 1 R t
182 178 181 eqtr4d R + t R R i t R = i 1 R t
183 182 mpteq2dva R + t R R i t R = t R R i 1 R t
184 23 a1i R + i
185 184 179 mulcld R + i 1 R
186 cncfmptc i 1 R R R t R R i 1 R : R R cn
187 185 8 10 186 syl3anc R + t R R i 1 R : R R cn
188 cncfmptid R R t R R t : R R cn
189 8 10 188 syl2anc R + t R R t : R R cn
190 187 189 mulcncf R + t R R i 1 R t : R R cn
191 183 190 eqeltrd R + t R R i t R : R R cn
192 17 29 mulcld R + t R R R 1 t R 2
193 192 17 19 divrec2d R + t R R R 1 t R 2 R = 1 R R 1 t R 2
194 29 17 19 divcan3d R + t R R R 1 t R 2 R = 1 t R 2
195 104 adantr R + t R R R 2
196 3 sqge0d R + 0 R 2
197 196 adantr R + t R R 0 R 2
198 195 197 87 136 sqrtmuld R + t R R R 2 1 t R 2 = R 2 1 t R 2
199 2 adantr R + t R R R 2
200 199 26 27 subdid R + t R R R 2 1 t R 2 = R 2 1 R 2 t R 2
201 199 mulid1d R + t R R R 2 1 = R 2
202 16 17 19 sqdivd R + t R R t R 2 = t 2 R 2
203 202 oveq2d R + t R R R 2 t R 2 = R 2 t 2 R 2
204 16 sqcld R + t R R t 2
205 sqne0 R R 2 0 R 0
206 1 205 syl R + R 2 0 R 0
207 18 206 mpbird R + R 2 0
208 207 adantr R + t R R R 2 0
209 204 199 208 divcan2d R + t R R R 2 t 2 R 2 = t 2
210 203 209 eqtrd R + t R R R 2 t R 2 = t 2
211 201 210 oveq12d R + t R R R 2 1 R 2 t R 2 = R 2 t 2
212 200 211 eqtrd R + t R R R 2 1 t R 2 = R 2 t 2
213 212 fveq2d R + t R R R 2 1 t R 2 = R 2 t 2
214 109 adantr R + t R R 0 R
215 84 214 sqrtsqd R + t R R R 2 = R
216 215 oveq1d R + t R R R 2 1 t R 2 = R 1 t R 2
217 198 213 216 3eqtr3rd R + t R R R 1 t R 2 = R 2 t 2
218 217 oveq2d R + t R R 1 R R 1 t R 2 = 1 R R 2 t 2
219 193 194 218 3eqtr3d R + t R R 1 t R 2 = 1 R R 2 t 2
220 219 mpteq2dva R + t R R 1 t R 2 = t R R 1 R R 2 t 2
221 cncfmptc 1 R R R t R R 1 R : R R cn
222 179 8 10 221 syl3anc R + t R R 1 R : R R cn
223 areacirclem2 R 0 R t R R R 2 t 2 : R R cn
224 3 109 223 syl2anc R + t R R R 2 t 2 : R R cn
225 222 224 mulcncf R + t R R 1 R R 2 t 2 : R R cn
226 220 225 eqeltrd R + t R R 1 t R 2 : R R cn
227 13 15 191 226 cncfmpt2f R + t R R i t R + 1 t R 2 : R R cn
228 cncffvrn −∞ 0 t R R i t R + 1 t R 2 : R R cn t R R i t R + 1 t R 2 : R R cn −∞ 0 t R R i t R + 1 t R 2 : R R −∞ 0
229 176 227 228 syl2anc R + t R R i t R + 1 t R 2 : R R cn −∞ 0 t R R i t R + 1 t R 2 : R R −∞ 0
230 175 229 mpbird R + t R R i t R + 1 t R 2 : R R cn −∞ 0
231 eqid TopOpen fld 𝑡 R R = TopOpen fld 𝑡 R R
232 eqid TopOpen fld 𝑡 −∞ 0 = TopOpen fld 𝑡 −∞ 0
233 13 231 232 cncfcn R R −∞ 0 R R cn −∞ 0 = TopOpen fld 𝑡 R R Cn TopOpen fld 𝑡 −∞ 0
234 8 176 233 syl2anc R + R R cn −∞ 0 = TopOpen fld 𝑡 R R Cn TopOpen fld 𝑡 −∞ 0
235 230 234 eleqtrd R + t R R i t R + 1 t R 2 TopOpen fld 𝑡 R R Cn TopOpen fld 𝑡 −∞ 0
236 eqid −∞ 0 = −∞ 0
237 236 logcn log −∞ 0 : −∞ 0 cn
238 difss −∞ 0
239 eqid TopOpen fld 𝑡 = TopOpen fld 𝑡
240 13 232 239 cncfcn −∞ 0 −∞ 0 cn = TopOpen fld 𝑡 −∞ 0 Cn TopOpen fld 𝑡
241 238 9 240 mp2an −∞ 0 cn = TopOpen fld 𝑡 −∞ 0 Cn TopOpen fld 𝑡
242 237 241 eleqtri log −∞ 0 TopOpen fld 𝑡 −∞ 0 Cn TopOpen fld 𝑡
243 242 a1i R + log −∞ 0 TopOpen fld 𝑡 −∞ 0 Cn TopOpen fld 𝑡
244 174 235 243 cnmpt11f R + t R R log −∞ 0 i t R + 1 t R 2 TopOpen fld 𝑡 R R Cn TopOpen fld 𝑡
245 13 231 239 cncfcn R R R R cn = TopOpen fld 𝑡 R R Cn TopOpen fld 𝑡
246 8 10 245 syl2anc R + R R cn = TopOpen fld 𝑡 R R Cn TopOpen fld 𝑡
247 244 246 eleqtrrd R + t R R log −∞ 0 i t R + 1 t R 2 : R R cn
248 170 247 mulcncf R + t R R i log −∞ 0 i t R + 1 t R 2 : R R cn
249 166 248 eqeltrd R + t R R arcsin t R : R R cn
250 219 oveq2d R + t R R t R 1 t R 2 = t R 1 R R 2 t 2
251 199 204 subcld R + t R R R 2 t 2
252 251 sqrtcld R + t R R R 2 t 2
253 20 180 252 mulassd R + t R R t R 1 R R 2 t 2 = t R 1 R R 2 t 2
254 16 17 19 divrecd R + t R R t R = t 1 R
255 254 oveq1d R + t R R t R 1 R = t 1 R 1 R
256 16 180 180 mulassd R + t R R t 1 R 1 R = t 1 R 1 R
257 255 256 eqtrd R + t R R t R 1 R = t 1 R 1 R
258 257 oveq1d R + t R R t R 1 R R 2 t 2 = t 1 R 1 R R 2 t 2
259 250 253 258 3eqtr2d R + t R R t R 1 t R 2 = t 1 R 1 R R 2 t 2
260 259 mpteq2dva R + t R R t R 1 t R 2 = t R R t 1 R 1 R R 2 t 2
261 179 179 mulcld R + 1 R 1 R
262 cncfmptc 1 R 1 R R R t R R 1 R 1 R : R R cn
263 261 8 10 262 syl3anc R + t R R 1 R 1 R : R R cn
264 189 263 mulcncf R + t R R t 1 R 1 R : R R cn
265 264 224 mulcncf R + t R R t 1 R 1 R R 2 t 2 : R R cn
266 260 265 eqeltrd R + t R R t R 1 t R 2 : R R cn
267 13 15 249 266 cncfmpt2f R + t R R arcsin t R + t R 1 t R 2 : R R cn
268 12 267 mulcncf R + t R R R 2 arcsin t R + t R 1 t R 2 : R R cn