Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  areacirclem4 Structured version   Visualization version   GIF version

Theorem areacirclem4 33813
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.)
Assertion
Ref Expression
areacirclem4 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
Distinct variable group:   𝑡,𝑅

Proof of Theorem areacirclem4
StepHypRef Expression
1 rpcn 12051 . . . 4 (𝑅 ∈ ℝ+𝑅 ∈ ℂ)
21sqcld 13225 . . 3 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℂ)
3 rpre 12049 . . . . . 6 (𝑅 ∈ ℝ+𝑅 ∈ ℝ)
43renegcld 10738 . . . . 5 (𝑅 ∈ ℝ+ → -𝑅 ∈ ℝ)
5 iccssre 12469 . . . . 5 ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (-𝑅[,]𝑅) ⊆ ℝ)
64, 3, 5syl2anc 575 . . . 4 (𝑅 ∈ ℝ+ → (-𝑅[,]𝑅) ⊆ ℝ)
7 ax-resscn 10274 . . . 4 ℝ ⊆ ℂ
86, 7syl6ss 3810 . . 3 (𝑅 ∈ ℝ+ → (-𝑅[,]𝑅) ⊆ ℂ)
9 ssid 3820 . . . 4 ℂ ⊆ ℂ
109a1i 11 . . 3 (𝑅 ∈ ℝ+ → ℂ ⊆ ℂ)
11 cncfmptc 22924 . . 3 (((𝑅↑2) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (𝑅↑2)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
122, 8, 10, 11syl3anc 1483 . 2 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (𝑅↑2)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
13 eqid 2806 . . 3 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
1413addcn 22878 . . . 4 + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
1514a1i 11 . . 3 (𝑅 ∈ ℝ+ → + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
168sselda 3798 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℂ)
171adantr 468 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 𝑅 ∈ ℂ)
18 rpne0 12058 . . . . . . . . 9 (𝑅 ∈ ℝ+𝑅 ≠ 0)
1918adantr 468 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 𝑅 ≠ 0)
2016, 17, 19divcld 11082 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) ∈ ℂ)
21 asinval 24822 . . . . . . 7 ((𝑡 / 𝑅) ∈ ℂ → (arcsin‘(𝑡 / 𝑅)) = (-i · (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
2220, 21syl 17 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (arcsin‘(𝑡 / 𝑅)) = (-i · (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
23 ax-icn 10276 . . . . . . . . . . . 12 i ∈ ℂ
2423a1i 11 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → i ∈ ℂ)
2524, 20mulcld 10341 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (i · (𝑡 / 𝑅)) ∈ ℂ)
26 1cnd 10316 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 1 ∈ ℂ)
2720sqcld 13225 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℂ)
2826, 27subcld 10673 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℂ)
2928sqrtcld 14395 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℂ)
3025, 29addcld 10340 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℂ)
31 0lt1 10831 . . . . . . . . . . . . . . 15 0 < 1
32 simp3 1161 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → 𝑡 = 0)
3332oveq1d 6885 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (𝑡 / 𝑅) = (0 / 𝑅))
341, 18div0d 11081 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ ℝ+ → (0 / 𝑅) = 0)
35343ad2ant1 1156 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 / 𝑅) = 0)
3633, 35eqtrd 2840 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (𝑡 / 𝑅) = 0)
3736oveq2d 6886 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (i · (𝑡 / 𝑅)) = (i · 0))
38 it0e0 11517 . . . . . . . . . . . . . . . . . . . 20 (i · 0) = 0
3937, 38syl6eq 2856 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (i · (𝑡 / 𝑅)) = 0)
4036oveq1d 6885 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((𝑡 / 𝑅)↑2) = (0↑2))
4140oveq2d 6886 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (1 − ((𝑡 / 𝑅)↑2)) = (1 − (0↑2)))
4241fveq2d 6408 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (√‘(1 − ((𝑡 / 𝑅)↑2))) = (√‘(1 − (0↑2))))
43 sq0 13174 . . . . . . . . . . . . . . . . . . . . . . . 24 (0↑2) = 0
4443oveq2i 6881 . . . . . . . . . . . . . . . . . . . . . . 23 (1 − (0↑2)) = (1 − 0)
45 1m0e1 11409 . . . . . . . . . . . . . . . . . . . . . . 23 (1 − 0) = 1
4644, 45eqtri 2828 . . . . . . . . . . . . . . . . . . . . . 22 (1 − (0↑2)) = 1
4746fveq2i 6407 . . . . . . . . . . . . . . . . . . . . 21 (√‘(1 − (0↑2))) = (√‘1)
48 sqrt1 14231 . . . . . . . . . . . . . . . . . . . . 21 (√‘1) = 1
4947, 48eqtri 2828 . . . . . . . . . . . . . . . . . . . 20 (√‘(1 − (0↑2))) = 1
5042, 49syl6eq 2856 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (√‘(1 − ((𝑡 / 𝑅)↑2))) = 1)
5139, 50oveq12d 6888 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (0 + 1))
52 0p1e1 11410 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
5351, 52syl6eq 2856 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) = 1)
5453breq2d 4856 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ↔ 0 < 1))
55 0red 10324 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → 0 ∈ ℝ)
56 1red 10322 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → 1 ∈ ℝ)
5753, 56eqeltrd 2885 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
5855, 57ltnled 10465 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ↔ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
5954, 58bitr3d 272 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 < 1 ↔ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
6031, 59mpbii 224 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0)
61603expa 1140 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 = 0) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0)
6261olcd 892 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 = 0) → (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
63 inelr 11291 . . . . . . . . . . . . . 14 ¬ i ∈ ℝ
6425, 29pncand 10674 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (i · (𝑡 / 𝑅)))
65643adant3 1155 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (i · (𝑡 / 𝑅)))
6665oveq1d 6885 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)) = ((i · (𝑡 / 𝑅)) · (𝑅 / 𝑡)))
6723a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → i ∈ ℂ)
68203adant3 1155 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (𝑡 / 𝑅) ∈ ℂ)
6913ad2ant1 1156 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑅 ∈ ℂ)
70163adant3 1155 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
71 simp3 1161 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑡 ≠ 0)
7269, 70, 71divcld 11082 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (𝑅 / 𝑡) ∈ ℂ)
7367, 68, 72mulassd 10344 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((i · (𝑡 / 𝑅)) · (𝑅 / 𝑡)) = (i · ((𝑡 / 𝑅) · (𝑅 / 𝑡))))
7466, 73eqtrd 2840 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)) = (i · ((𝑡 / 𝑅) · (𝑅 / 𝑡))))
75183ad2ant1 1156 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑅 ≠ 0)
7670, 69, 71, 75divcan6d 11101 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((𝑡 / 𝑅) · (𝑅 / 𝑡)) = 1)
7776oveq2d 6886 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (i · ((𝑡 / 𝑅) · (𝑅 / 𝑡))) = (i · 1))
7867mulid1d 10338 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (i · 1) = i)
7974, 77, 783eqtrrd 2845 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → i = ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)))
8079adantr 468 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → i = ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)))
81 simpr 473 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
82 1red 10322 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 1 ∈ ℝ)
836sselda 3798 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℝ)
843adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 𝑅 ∈ ℝ)
8583, 84, 19redivcld 11134 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) ∈ ℝ)
8685resqcld 13254 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℝ)
8782, 86resubcld 10739 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℝ)
88 elicc2 12452 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅)))
894, 3, 88syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅)))
90 1red 10322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 1 ∈ ℝ)
91 simpr 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
923adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
9318adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ≠ 0)
9491, 92, 93redivcld 11134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡 / 𝑅) ∈ ℝ)
9594resqcld 13254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡 / 𝑅)↑2) ∈ ℝ)
9690, 95subge0d 10898 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (0 ≤ (1 − ((𝑡 / 𝑅)↑2)) ↔ ((𝑡 / 𝑅)↑2) ≤ 1))
97 recn 10307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
9897adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑡 ∈ ℂ)
991adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ∈ ℂ)
10098, 99, 93sqdivd 13240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2)))
101100breq1d 4854 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((𝑡 / 𝑅)↑2) ≤ 1 ↔ ((𝑡↑2) / (𝑅↑2)) ≤ 1))
102 resqcl 13150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℝ)
103102adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
1043resqcld 13254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℝ)
105 rpgt0 12054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑅 ∈ ℝ+ → 0 < 𝑅)
106 0red 10324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑅 ∈ ℝ+ → 0 ∈ ℝ)
107 0le0 11389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 0 ≤ 0
108107a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑅 ∈ ℝ+ → 0 ≤ 0)
109 rpge0 12055 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑅 ∈ ℝ+ → 0 ≤ 𝑅)
110106, 3, 108, 109lt2sqd 13262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑅 ∈ ℝ+ → (0 < 𝑅 ↔ (0↑2) < (𝑅↑2)))
11143a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑅 ∈ ℝ+ → (0↑2) = 0)
112111breq1d 4854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑅 ∈ ℝ+ → ((0↑2) < (𝑅↑2) ↔ 0 < (𝑅↑2)))
113110, 112bitrd 270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑅 ∈ ℝ+ → (0 < 𝑅 ↔ 0 < (𝑅↑2)))
114105, 113mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑅 ∈ ℝ+ → 0 < (𝑅↑2))
115104, 114elrpd 12079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℝ+)
116115adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ+)
117103, 90, 116ledivmuld 12135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((𝑡↑2) / (𝑅↑2)) ≤ 1 ↔ (𝑡↑2) ≤ ((𝑅↑2) · 1)))
118 absresq 14261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 ∈ ℝ → ((abs‘𝑡)↑2) = (𝑡↑2))
119118eqcomd 2812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑡 ∈ ℝ → (𝑡↑2) = ((abs‘𝑡)↑2))
1202mulid1d 10338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑅 ∈ ℝ+ → ((𝑅↑2) · 1) = (𝑅↑2))
121119, 120breqan12rd 4861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡↑2) ≤ ((𝑅↑2) · 1) ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
12297abscld 14394 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 ∈ ℝ → (abs‘𝑡) ∈ ℝ)
123122adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
12497absge0d 14402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 ∈ ℝ → 0 ≤ (abs‘𝑡))
125124adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
126109adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 0 ≤ 𝑅)
127123, 92, 125, 126le2sqd 13263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
12891, 92absled 14388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ (-𝑅𝑡𝑡𝑅)))
129121, 127, 1283bitr2d 298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡↑2) ≤ ((𝑅↑2) · 1) ↔ (-𝑅𝑡𝑡𝑅)))
130117, 129bitrd 270 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((𝑡↑2) / (𝑅↑2)) ≤ 1 ↔ (-𝑅𝑡𝑡𝑅)))
13196, 101, 1303bitrrd 297 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅𝑡𝑡𝑅) ↔ 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
132131biimpd 220 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅𝑡𝑡𝑅) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
133132exp4b 419 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑅 ∈ ℝ+ → (𝑡 ∈ ℝ → (-𝑅𝑡 → (𝑡𝑅 → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))))
1341333impd 1450 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑅 ∈ ℝ+ → ((𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
13589, 134sylbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
136135imp 395 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2)))
13787, 136resqrtcld 14375 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℝ)
1381373adant3 1155 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℝ)
139138adantr 468 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℝ)
14081, 139resubcld 10739 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
14133ad2ant1 1156 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑅 ∈ ℝ)
142833adant3 1155 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℝ)
143141, 142, 71redivcld 11134 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (𝑅 / 𝑡) ∈ ℝ)
144143adantr 468 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → (𝑅 / 𝑡) ∈ ℝ)
145140, 144remulcld 10351 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)) ∈ ℝ)
14680, 145eqeltrd 2885 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → i ∈ ℝ)
147146ex 399 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ → i ∈ ℝ))
1481473expa 1140 . . . . . . . . . . . . . 14 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 ≠ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ → i ∈ ℝ))
14963, 148mtoi 190 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 ≠ 0) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
150149orcd 891 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 ≠ 0) → (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
15162, 150pm2.61dane 3065 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
152 ianor 995 . . . . . . . . . . 11 (¬ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0) ↔ (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
153151, 152sylibr 225 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ¬ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
154 mnfxr 10377 . . . . . . . . . . . 12 -∞ ∈ ℝ*
155 0re 10323 . . . . . . . . . . . 12 0 ∈ ℝ
156 elioc2 12450 . . . . . . . . . . . 12 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0) ↔ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ -∞ < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0)))
157154, 155, 156mp2an 675 . . . . . . . . . . 11 (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0) ↔ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ -∞ < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
158 3simpb 1173 . . . . . . . . . . 11 ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ -∞ < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
159157, 158sylbi 208 . . . . . . . . . 10 (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
160153, 159nsyl 137 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0))
16130, 160eldifd 3780 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (ℂ ∖ (-∞(,]0)))
162 fvres 6423 . . . . . . . 8 (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (ℂ ∖ (-∞(,]0)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))))
163161, 162syl 17 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))))
164163oveq2d 6886 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) = (-i · (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
16522, 164eqtr4d 2843 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (arcsin‘(𝑡 / 𝑅)) = (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
166165mpteq2dva 4938 . . . 4 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (arcsin‘(𝑡 / 𝑅))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))))))
167 negicn 10563 . . . . . . 7 -i ∈ ℂ
168167a1i 11 . . . . . 6 (𝑅 ∈ ℝ+ → -i ∈ ℂ)
169 cncfmptc 22924 . . . . . 6 ((-i ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ -i) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
170168, 8, 10, 169syl3anc 1483 . . . . 5 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ -i) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
17113cnfldtopon 22796 . . . . . . . . 9 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
172171a1i 11 . . . . . . . 8 (𝑅 ∈ ℝ+ → (TopOpen‘ℂfld) ∈ (TopOn‘ℂ))
173 resttopon 21176 . . . . . . . 8 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (-𝑅[,]𝑅) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) ∈ (TopOn‘(-𝑅[,]𝑅)))
174172, 8, 173syl2anc 575 . . . . . . 7 (𝑅 ∈ ℝ+ → ((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) ∈ (TopOn‘(-𝑅[,]𝑅)))
175161fmpttd 6603 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))):(-𝑅[,]𝑅)⟶(ℂ ∖ (-∞(,]0)))
176 difssd 3937 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → (ℂ ∖ (-∞(,]0)) ⊆ ℂ)
17716, 17, 19divrec2d 11086 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) = ((1 / 𝑅) · 𝑡))
178177oveq2d 6886 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (i · (𝑡 / 𝑅)) = (i · ((1 / 𝑅) · 𝑡)))
1791, 18reccld 11075 . . . . . . . . . . . . . . . 16 (𝑅 ∈ ℝ+ → (1 / 𝑅) ∈ ℂ)
180179adantr 468 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (1 / 𝑅) ∈ ℂ)
18124, 180, 16mulassd 10344 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((i · (1 / 𝑅)) · 𝑡) = (i · ((1 / 𝑅) · 𝑡)))
182178, 181eqtr4d 2843 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (i · (𝑡 / 𝑅)) = ((i · (1 / 𝑅)) · 𝑡))
183182mpteq2dva 4938 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (𝑡 / 𝑅))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (1 / 𝑅)) · 𝑡)))
18423a1i 11 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ+ → i ∈ ℂ)
185184, 179mulcld 10341 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → (i · (1 / 𝑅)) ∈ ℂ)
186 cncfmptc 22924 . . . . . . . . . . . . . 14 (((i · (1 / 𝑅)) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
187185, 8, 10, 186syl3anc 1483 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
188 cncfmptid 22925 . . . . . . . . . . . . . 14 (((-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ 𝑡) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
1898, 10, 188syl2anc 575 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ 𝑡) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
190187, 189mulcncf 23426 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (1 / 𝑅)) · 𝑡)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
191183, 190eqeltrd 2885 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (𝑡 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
19217, 29mulcld 10341 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℂ)
193192, 17, 19divrec2d 11086 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) / 𝑅) = ((1 / 𝑅) · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))))
19429, 17, 19divcan3d 11087 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) / 𝑅) = (√‘(1 − ((𝑡 / 𝑅)↑2))))
195104adantr 468 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℝ)
1963sqge0d 13255 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ ℝ+ → 0 ≤ (𝑅↑2))
197196adantr 468 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ (𝑅↑2))
198195, 197, 87, 136sqrtmuld 14382 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = ((√‘(𝑅↑2)) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
1992adantr 468 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℂ)
200199, 26, 27subdid 10767 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))))
201199mulid1d 10338 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · 1) = (𝑅↑2))
20216, 17, 19sqdivd 13240 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2)))
203202oveq2d 6886 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))))
20416sqcld 13225 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡↑2) ∈ ℂ)
205 sqne0 13149 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑅 ∈ ℂ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0))
2061, 205syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ ℝ+ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0))
20718, 206mpbird 248 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∈ ℝ+ → (𝑅↑2) ≠ 0)
208207adantr 468 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ≠ 0)
209204, 199, 208divcan2d 11084 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))) = (𝑡↑2))
210203, 209eqtrd 2840 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = (𝑡↑2))
211201, 210oveq12d 6888 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2)))
212200, 211eqtrd 2840 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2)))
213212fveq2d 6408 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2))))
214109adantr 468 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ 𝑅)
21584, 214sqrtsqd 14377 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(𝑅↑2)) = 𝑅)
216215oveq1d 6885 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((√‘(𝑅↑2)) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
217198, 213, 2163eqtr3rd 2849 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2))))
218217oveq2d 6886 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((1 / 𝑅) · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2)))))
219193, 194, 2183eqtr3d 2848 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) = ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2)))))
220219mpteq2dva 4938 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))))
221 cncfmptc 22924 . . . . . . . . . . . . . 14 (((1 / 𝑅) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (1 / 𝑅)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
222179, 8, 10, 221syl3anc 1483 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (1 / 𝑅)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
223 areacirclem2 33811 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑡↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
2243, 109, 223syl2anc 575 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑡↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
225222, 224mulcncf 23426 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
226220, 225eqeltrd 2885 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
22713, 15, 191, 226cncfmpt2f 22927 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
228 cncffvrn 22911 . . . . . . . . . 10 (((ℂ ∖ (-∞(,]0)) ⊆ ℂ ∧ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) → ((𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) ↔ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))):(-𝑅[,]𝑅)⟶(ℂ ∖ (-∞(,]0))))
229176, 227, 228syl2anc 575 . . . . . . . . 9 (𝑅 ∈ ℝ+ → ((𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) ↔ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))):(-𝑅[,]𝑅)⟶(ℂ ∖ (-∞(,]0))))
230175, 229mpbird 248 . . . . . . . 8 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))))
231 eqid 2806 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) = ((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅))
232 eqid 2806 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0))) = ((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0)))
23313, 231, 232cncfcn 22922 . . . . . . . . 9 (((-𝑅[,]𝑅) ⊆ ℂ ∧ (ℂ ∖ (-∞(,]0)) ⊆ ℂ) → ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) = (((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0)))))
2348, 176, 233syl2anc 575 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) = (((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0)))))
235230, 234eleqtrd 2887 . . . . . . 7 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ (((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0)))))
236 eqid 2806 . . . . . . . . . 10 (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
237236logcn 24606 . . . . . . . . 9 (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ)
238 difss 3936 . . . . . . . . . 10 (ℂ ∖ (-∞(,]0)) ⊆ ℂ
239 eqid 2806 . . . . . . . . . . 11 ((TopOpen‘ℂfld) ↾t ℂ) = ((TopOpen‘ℂfld) ↾t ℂ)
24013, 232, 239cncfcn 22922 . . . . . . . . . 10 (((ℂ ∖ (-∞(,]0)) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((ℂ ∖ (-∞(,]0))–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0))) Cn ((TopOpen‘ℂfld) ↾t ℂ)))
241238, 9, 240mp2an 675 . . . . . . . . 9 ((ℂ ∖ (-∞(,]0))–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0))) Cn ((TopOpen‘ℂfld) ↾t ℂ))
242237, 241eleqtri 2883 . . . . . . . 8 (log ↾ (ℂ ∖ (-∞(,]0))) ∈ (((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0))) Cn ((TopOpen‘ℂfld) ↾t ℂ))
243242a1i 11 . . . . . . 7 (𝑅 ∈ ℝ+ → (log ↾ (ℂ ∖ (-∞(,]0))) ∈ (((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0))) Cn ((TopOpen‘ℂfld) ↾t ℂ)))
244174, 235, 243cnmpt11f 21678 . . . . . 6 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) ∈ (((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld) ↾t ℂ)))
24513, 231, 239cncfcn 22922 . . . . . . 7 (((-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((-𝑅[,]𝑅)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld) ↾t ℂ)))
2468, 10, 245syl2anc 575 . . . . . 6 (𝑅 ∈ ℝ+ → ((-𝑅[,]𝑅)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld) ↾t ℂ)))
247244, 246eleqtrrd 2888 . . . . 5 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
248170, 247mulcncf 23426 . . . 4 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
249166, 248eqeltrd 2885 . . 3 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (arcsin‘(𝑡 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
250219oveq2d 6886 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = ((𝑡 / 𝑅) · ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))))
251199, 204subcld 10673 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
252251sqrtcld 14395 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
25320, 180, 252mulassd 10344 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (((𝑡 / 𝑅) · (1 / 𝑅)) · (√‘((𝑅↑2) − (𝑡↑2)))) = ((𝑡 / 𝑅) · ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))))
25416, 17, 19divrecd 11085 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) = (𝑡 · (1 / 𝑅)))
255254oveq1d 6885 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (1 / 𝑅)) = ((𝑡 · (1 / 𝑅)) · (1 / 𝑅)))
25616, 180, 180mulassd 10344 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 · (1 / 𝑅)) · (1 / 𝑅)) = (𝑡 · ((1 / 𝑅) · (1 / 𝑅))))
257255, 256eqtrd 2840 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (1 / 𝑅)) = (𝑡 · ((1 / 𝑅) · (1 / 𝑅))))
258257oveq1d 6885 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (((𝑡 / 𝑅) · (1 / 𝑅)) · (√‘((𝑅↑2) − (𝑡↑2)))) = ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2)))))
259250, 253, 2583eqtr2d 2846 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2)))))
260259mpteq2dva 4938 . . . 4 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2))))))
261179, 179mulcld 10341 . . . . . . 7 (𝑅 ∈ ℝ+ → ((1 / 𝑅) · (1 / 𝑅)) ∈ ℂ)
262 cncfmptc 22924 . . . . . . 7 ((((1 / 𝑅) · (1 / 𝑅)) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
263261, 8, 10, 262syl3anc 1483 . . . . . 6 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
264189, 263mulcncf 23426 . . . . 5 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (𝑡 · ((1 / 𝑅) · (1 / 𝑅)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
265264, 224mulcncf 23426 . . . 4 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
266260, 265eqeltrd 2885 . . 3 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
26713, 15, 249, 266cncfmpt2f 22927 . 2 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
26812, 267mulcncf 23426 1 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865  w3a 1100   = wceq 1637  wcel 2156  wne 2978  cdif 3766  wss 3769   class class class wbr 4844  cmpt 4923  cres 5313  wf 6093  cfv 6097  (class class class)co 6870  cc 10215  cr 10216  0cc0 10217  1c1 10218  ici 10219   + caddc 10220   · cmul 10222  -∞cmnf 10353  *cxr 10354   < clt 10355  cle 10356  cmin 10547  -cneg 10548   / cdiv 10965  2c2 11352  +crp 12042  (,]cioc 12390  [,]cicc 12392  cexp 13079  csqrt 14192  abscabs 14193  t crest 16282  TopOpenctopn 16283  fldccnfld 19950  TopOnctopon 20925   Cn ccn 21239   ×t ctx 21574  cnccncf 22889  logclog 24514  arcsincasin 24802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175  ax-inf2 8781  ax-cnex 10273  ax-resscn 10274  ax-1cn 10275  ax-icn 10276  ax-addcl 10277  ax-addrcl 10278  ax-mulcl 10279  ax-mulrcl 10280  ax-mulcom 10281  ax-addass 10282  ax-mulass 10283  ax-distr 10284  ax-i2m1 10285  ax-1ne0 10286  ax-1rid 10287  ax-rnegex 10288  ax-rrecex 10289  ax-cnre 10290  ax-pre-lttri 10291  ax-pre-lttrn 10292  ax-pre-ltadd 10293  ax-pre-mulgt0 10294  ax-pre-sup 10295  ax-addf 10296  ax-mulf 10297
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-iin 4715  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-isom 6106  df-riota 6831  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-of 7123  df-om 7292  df-1st 7394  df-2nd 7395  df-supp 7526  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-1o 7792  df-2o 7793  df-oadd 7796  df-er 7975  df-map 8090  df-pm 8091  df-ixp 8142  df-en 8189  df-dom 8190  df-sdom 8191  df-fin 8192  df-fsupp 8511  df-fi 8552  df-sup 8583  df-inf 8584  df-oi 8650  df-card 9044  df-cda 9271  df-pnf 10357  df-mnf 10358  df-xr 10359  df-ltxr 10360  df-le 10361  df-sub 10549  df-neg 10550  df-div 10966  df-nn 11302  df-2 11360  df-3 11361  df-4 11362  df-5 11363  df-6 11364  df-7 11365  df-8 11366  df-9 11367  df-n0 11556  df-z 11640  df-dec 11756  df-uz 11901  df-q 12004  df-rp 12043  df-xneg 12158  df-xadd 12159  df-xmul 12160  df-ioo 12393  df-ioc 12394  df-ico 12395  df-icc 12396  df-fz 12546  df-fzo 12686  df-fl 12813  df-mod 12889  df-seq 13021  df-exp 13080  df-fac 13277  df-bc 13306  df-hash 13334  df-shft 14026  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195  df-limsup 14421  df-clim 14438  df-rlim 14439  df-sum 14636  df-ef 15014  df-sin 15016  df-cos 15017  df-tan 15018  df-pi 15019  df-struct 16066  df-ndx 16067  df-slot 16068  df-base 16070  df-sets 16071  df-ress 16072  df-plusg 16162  df-mulr 16163  df-starv 16164  df-sca 16165  df-vsca 16166  df-ip 16167  df-tset 16168  df-ple 16169  df-ds 16171  df-unif 16172  df-hom 16173  df-cco 16174  df-rest 16284  df-topn 16285  df-0g 16303  df-gsum 16304  df-topgen 16305  df-pt 16306  df-prds 16309  df-xrs 16363  df-qtop 16368  df-imas 16369  df-xps 16371  df-mre 16447  df-mrc 16448  df-acs 16450  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-submnd 17537  df-mulg 17742  df-cntz 17947  df-cmn 18392  df-psmet 19942  df-xmet 19943  df-met 19944  df-bl 19945  df-mopn 19946  df-fbas 19947  df-fg 19948  df-cnfld 19951  df-top 20909  df-topon 20926  df-topsp 20948  df-bases 20961  df-cld 21034  df-ntr 21035  df-cls 21036  df-nei 21113  df-lp 21151  df-perf 21152  df-cn 21242  df-cnp 21243  df-haus 21330  df-cmp 21401  df-tx 21576  df-hmeo 21769  df-fil 21860  df-fm 21952  df-flim 21953  df-flf 21954  df-xms 22335  df-ms 22336  df-tms 22337  df-cncf 22891  df-limc 23843  df-dv 23844  df-log 24516  df-cxp 24517  df-asin 24805
This theorem is referenced by:  areacirc  33815
  Copyright terms: Public domain W3C validator