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 35966
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 12833 . . . 4 (𝑅 ∈ ℝ+𝑅 ∈ ℂ)
21sqcld 13955 . . 3 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℂ)
3 rpre 12831 . . . . . 6 (𝑅 ∈ ℝ+𝑅 ∈ ℝ)
43renegcld 11495 . . . . 5 (𝑅 ∈ ℝ+ → -𝑅 ∈ ℝ)
5 iccssre 13254 . . . . 5 ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (-𝑅[,]𝑅) ⊆ ℝ)
64, 3, 5syl2anc 584 . . . 4 (𝑅 ∈ ℝ+ → (-𝑅[,]𝑅) ⊆ ℝ)
7 ax-resscn 11021 . . . 4 ℝ ⊆ ℂ
86, 7sstrdi 3943 . . 3 (𝑅 ∈ ℝ+ → (-𝑅[,]𝑅) ⊆ ℂ)
9 ssid 3953 . . . 4 ℂ ⊆ ℂ
109a1i 11 . . 3 (𝑅 ∈ ℝ+ → ℂ ⊆ ℂ)
11 cncfmptc 24173 . . 3 (((𝑅↑2) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (𝑅↑2)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
122, 8, 10, 11syl3anc 1370 . 2 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (𝑅↑2)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
13 eqid 2736 . . 3 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
1413addcn 24126 . . . 4 + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
1514a1i 11 . . 3 (𝑅 ∈ ℝ+ → + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
168sselda 3931 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℂ)
171adantr 481 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 𝑅 ∈ ℂ)
18 rpne0 12839 . . . . . . . . 9 (𝑅 ∈ ℝ+𝑅 ≠ 0)
1918adantr 481 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 𝑅 ≠ 0)
2016, 17, 19divcld 11844 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) ∈ ℂ)
21 asinval 26130 . . . . . . 7 ((𝑡 / 𝑅) ∈ ℂ → (arcsin‘(𝑡 / 𝑅)) = (-i · (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
2220, 21syl 17 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (arcsin‘(𝑡 / 𝑅)) = (-i · (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
23 ax-icn 11023 . . . . . . . . . . . 12 i ∈ ℂ
2423a1i 11 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → i ∈ ℂ)
2524, 20mulcld 11088 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (i · (𝑡 / 𝑅)) ∈ ℂ)
26 1cnd 11063 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 1 ∈ ℂ)
2720sqcld 13955 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℂ)
2826, 27subcld 11425 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℂ)
2928sqrtcld 15240 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℂ)
3025, 29addcld 11087 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℂ)
31 0lt1 11590 . . . . . . . . . . . . . . 15 0 < 1
32 simp3 1137 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → 𝑡 = 0)
3332oveq1d 7344 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (𝑡 / 𝑅) = (0 / 𝑅))
341, 18div0d 11843 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ ℝ+ → (0 / 𝑅) = 0)
35343ad2ant1 1132 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 / 𝑅) = 0)
3633, 35eqtrd 2776 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (𝑡 / 𝑅) = 0)
3736oveq2d 7345 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (i · (𝑡 / 𝑅)) = (i · 0))
38 it0e0 12288 . . . . . . . . . . . . . . . . . . . 20 (i · 0) = 0
3937, 38eqtrdi 2792 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (i · (𝑡 / 𝑅)) = 0)
4036oveq1d 7344 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((𝑡 / 𝑅)↑2) = (0↑2))
4140oveq2d 7345 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (1 − ((𝑡 / 𝑅)↑2)) = (1 − (0↑2)))
4241fveq2d 6823 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (√‘(1 − ((𝑡 / 𝑅)↑2))) = (√‘(1 − (0↑2))))
43 sq0 14002 . . . . . . . . . . . . . . . . . . . . . . . 24 (0↑2) = 0
4443oveq2i 7340 . . . . . . . . . . . . . . . . . . . . . . 23 (1 − (0↑2)) = (1 − 0)
45 1m0e1 12187 . . . . . . . . . . . . . . . . . . . . . . 23 (1 − 0) = 1
4644, 45eqtri 2764 . . . . . . . . . . . . . . . . . . . . . 22 (1 − (0↑2)) = 1
4746fveq2i 6822 . . . . . . . . . . . . . . . . . . . . 21 (√‘(1 − (0↑2))) = (√‘1)
48 sqrt1 15074 . . . . . . . . . . . . . . . . . . . . 21 (√‘1) = 1
4947, 48eqtri 2764 . . . . . . . . . . . . . . . . . . . 20 (√‘(1 − (0↑2))) = 1
5042, 49eqtrdi 2792 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (√‘(1 − ((𝑡 / 𝑅)↑2))) = 1)
5139, 50oveq12d 7347 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (0 + 1))
52 0p1e1 12188 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
5351, 52eqtrdi 2792 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) = 1)
5453breq2d 5101 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ↔ 0 < 1))
55 0red 11071 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → 0 ∈ ℝ)
56 1red 11069 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → 1 ∈ ℝ)
5753, 56eqeltrd 2837 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
5855, 57ltnled 11215 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ↔ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
5954, 58bitr3d 280 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 < 1 ↔ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
6031, 59mpbii 232 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0)
61603expa 1117 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 = 0) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0)
6261olcd 871 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 = 0) → (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
63 inelr 12056 . . . . . . . . . . . . . 14 ¬ i ∈ ℝ
6425, 29pncand 11426 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (i · (𝑡 / 𝑅)))
65643adant3 1131 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (i · (𝑡 / 𝑅)))
6665oveq1d 7344 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)) = ((i · (𝑡 / 𝑅)) · (𝑅 / 𝑡)))
6723a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → i ∈ ℂ)
68203adant3 1131 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (𝑡 / 𝑅) ∈ ℂ)
6913ad2ant1 1132 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑅 ∈ ℂ)
70163adant3 1131 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
71 simp3 1137 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑡 ≠ 0)
7269, 70, 71divcld 11844 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (𝑅 / 𝑡) ∈ ℂ)
7367, 68, 72mulassd 11091 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((i · (𝑡 / 𝑅)) · (𝑅 / 𝑡)) = (i · ((𝑡 / 𝑅) · (𝑅 / 𝑡))))
7466, 73eqtrd 2776 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)) = (i · ((𝑡 / 𝑅) · (𝑅 / 𝑡))))
75183ad2ant1 1132 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑅 ≠ 0)
7670, 69, 71, 75divcan6d 11863 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((𝑡 / 𝑅) · (𝑅 / 𝑡)) = 1)
7776oveq2d 7345 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (i · ((𝑡 / 𝑅) · (𝑅 / 𝑡))) = (i · 1))
7867mulid1d 11085 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (i · 1) = i)
7974, 77, 783eqtrrd 2781 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → i = ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)))
8079adantr 481 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → i = ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)))
81 simpr 485 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
82 1red 11069 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 1 ∈ ℝ)
836sselda 3931 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℝ)
843adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 𝑅 ∈ ℝ)
8583, 84, 19redivcld 11896 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) ∈ ℝ)
8685resqcld 14058 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℝ)
8782, 86resubcld 11496 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℝ)
88 elicc2 13237 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅)))
894, 3, 88syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅)))
90 1red 11069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 1 ∈ ℝ)
91 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
923adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
9318adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ≠ 0)
9491, 92, 93redivcld 11896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡 / 𝑅) ∈ ℝ)
9594resqcld 14058 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡 / 𝑅)↑2) ∈ ℝ)
9690, 95subge0d 11658 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (0 ≤ (1 − ((𝑡 / 𝑅)↑2)) ↔ ((𝑡 / 𝑅)↑2) ≤ 1))
97 recn 11054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
9897adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑡 ∈ ℂ)
991adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ∈ ℂ)
10098, 99, 93sqdivd 13970 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2)))
101100breq1d 5099 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((𝑡 / 𝑅)↑2) ≤ 1 ↔ ((𝑡↑2) / (𝑅↑2)) ≤ 1))
102 resqcl 13937 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℝ)
103102adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
1043resqcld 14058 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℝ)
105 rpgt0 12835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑅 ∈ ℝ+ → 0 < 𝑅)
106 0red 11071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑅 ∈ ℝ+ → 0 ∈ ℝ)
107 0le0 12167 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 0 ≤ 0
108107a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑅 ∈ ℝ+ → 0 ≤ 0)
109 rpge0 12836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑅 ∈ ℝ+ → 0 ≤ 𝑅)
110106, 3, 108, 109lt2sqd 14066 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑅 ∈ ℝ+ → (0 < 𝑅 ↔ (0↑2) < (𝑅↑2)))
11143a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑅 ∈ ℝ+ → (0↑2) = 0)
112111breq1d 5099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑅 ∈ ℝ+ → ((0↑2) < (𝑅↑2) ↔ 0 < (𝑅↑2)))
113110, 112bitrd 278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑅 ∈ ℝ+ → (0 < 𝑅 ↔ 0 < (𝑅↑2)))
114105, 113mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑅 ∈ ℝ+ → 0 < (𝑅↑2))
115104, 114elrpd 12862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℝ+)
116115adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ+)
117103, 90, 116ledivmuld 12918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((𝑡↑2) / (𝑅↑2)) ≤ 1 ↔ (𝑡↑2) ≤ ((𝑅↑2) · 1)))
118 absresq 15105 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 ∈ ℝ → ((abs‘𝑡)↑2) = (𝑡↑2))
119118eqcomd 2742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑡 ∈ ℝ → (𝑡↑2) = ((abs‘𝑡)↑2))
1202mulid1d 11085 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑅 ∈ ℝ+ → ((𝑅↑2) · 1) = (𝑅↑2))
121119, 120breqan12rd 5106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡↑2) ≤ ((𝑅↑2) · 1) ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
12297abscld 15239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 ∈ ℝ → (abs‘𝑡) ∈ ℝ)
123122adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
12497absge0d 15247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 ∈ ℝ → 0 ≤ (abs‘𝑡))
125124adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
126109adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 0 ≤ 𝑅)
127123, 92, 125, 126le2sqd 14067 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
12891, 92absled 15233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ (-𝑅𝑡𝑡𝑅)))
129121, 127, 1283bitr2d 306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡↑2) ≤ ((𝑅↑2) · 1) ↔ (-𝑅𝑡𝑡𝑅)))
130117, 129bitrd 278 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((𝑡↑2) / (𝑅↑2)) ≤ 1 ↔ (-𝑅𝑡𝑡𝑅)))
13196, 101, 1303bitrrd 305 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅𝑡𝑡𝑅) ↔ 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
132131biimpd 228 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅𝑡𝑡𝑅) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
133132exp4b 431 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑅 ∈ ℝ+ → (𝑡 ∈ ℝ → (-𝑅𝑡 → (𝑡𝑅 → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))))
1341333impd 1347 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑅 ∈ ℝ+ → ((𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
13589, 134sylbid 239 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
136135imp 407 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2)))
13787, 136resqrtcld 15220 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℝ)
1381373adant3 1131 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℝ)
139138adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℝ)
14081, 139resubcld 11496 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
14133ad2ant1 1132 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑅 ∈ ℝ)
142833adant3 1131 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℝ)
143141, 142, 71redivcld 11896 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (𝑅 / 𝑡) ∈ ℝ)
144143adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → (𝑅 / 𝑡) ∈ ℝ)
145140, 144remulcld 11098 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)) ∈ ℝ)
14680, 145eqeltrd 2837 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → i ∈ ℝ)
147146ex 413 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ → i ∈ ℝ))
1481473expa 1117 . . . . . . . . . . . . . 14 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 ≠ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ → i ∈ ℝ))
14963, 148mtoi 198 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 ≠ 0) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
150149orcd 870 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 ≠ 0) → (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
15162, 150pm2.61dane 3029 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
152 ianor 979 . . . . . . . . . . 11 (¬ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0) ↔ (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
153151, 152sylibr 233 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ¬ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
154 mnfxr 11125 . . . . . . . . . . . 12 -∞ ∈ ℝ*
155 0re 11070 . . . . . . . . . . . 12 0 ∈ ℝ
156 elioc2 13235 . . . . . . . . . . . 12 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0) ↔ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ -∞ < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0)))
157154, 155, 156mp2an 689 . . . . . . . . . . 11 (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0) ↔ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ -∞ < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
158 3simpb 1148 . . . . . . . . . . 11 ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ -∞ < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
159157, 158sylbi 216 . . . . . . . . . 10 (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
160153, 159nsyl 140 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0))
16130, 160eldifd 3908 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (ℂ ∖ (-∞(,]0)))
162 fvres 6838 . . . . . . . 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 7345 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) = (-i · (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
16522, 164eqtr4d 2779 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (arcsin‘(𝑡 / 𝑅)) = (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
166165mpteq2dva 5189 . . . 4 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (arcsin‘(𝑡 / 𝑅))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))))))
167 negicn 11315 . . . . . . 7 -i ∈ ℂ
168167a1i 11 . . . . . 6 (𝑅 ∈ ℝ+ → -i ∈ ℂ)
169 cncfmptc 24173 . . . . . 6 ((-i ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ -i) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
170168, 8, 10, 169syl3anc 1370 . . . . 5 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ -i) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
17113cnfldtopon 24044 . . . . . . . . 9 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
172171a1i 11 . . . . . . . 8 (𝑅 ∈ ℝ+ → (TopOpen‘ℂfld) ∈ (TopOn‘ℂ))
173 resttopon 22410 . . . . . . . 8 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (-𝑅[,]𝑅) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) ∈ (TopOn‘(-𝑅[,]𝑅)))
174172, 8, 173syl2anc 584 . . . . . . 7 (𝑅 ∈ ℝ+ → ((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) ∈ (TopOn‘(-𝑅[,]𝑅)))
175161fmpttd 7039 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))):(-𝑅[,]𝑅)⟶(ℂ ∖ (-∞(,]0)))
176 difssd 4078 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → (ℂ ∖ (-∞(,]0)) ⊆ ℂ)
17716, 17, 19divrec2d 11848 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) = ((1 / 𝑅) · 𝑡))
178177oveq2d 7345 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (i · (𝑡 / 𝑅)) = (i · ((1 / 𝑅) · 𝑡)))
1791, 18reccld 11837 . . . . . . . . . . . . . . . 16 (𝑅 ∈ ℝ+ → (1 / 𝑅) ∈ ℂ)
180179adantr 481 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (1 / 𝑅) ∈ ℂ)
18124, 180, 16mulassd 11091 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((i · (1 / 𝑅)) · 𝑡) = (i · ((1 / 𝑅) · 𝑡)))
182178, 181eqtr4d 2779 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (i · (𝑡 / 𝑅)) = ((i · (1 / 𝑅)) · 𝑡))
183182mpteq2dva 5189 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (𝑡 / 𝑅))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (1 / 𝑅)) · 𝑡)))
18423a1i 11 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ+ → i ∈ ℂ)
185184, 179mulcld 11088 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → (i · (1 / 𝑅)) ∈ ℂ)
186 cncfmptc 24173 . . . . . . . . . . . . . 14 (((i · (1 / 𝑅)) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
187185, 8, 10, 186syl3anc 1370 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
188 cncfmptid 24174 . . . . . . . . . . . . . 14 (((-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ 𝑡) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
1898, 10, 188syl2anc 584 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ 𝑡) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
190187, 189mulcncf 24708 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (1 / 𝑅)) · 𝑡)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
191183, 190eqeltrd 2837 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (𝑡 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
19217, 29mulcld 11088 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℂ)
193192, 17, 19divrec2d 11848 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) / 𝑅) = ((1 / 𝑅) · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))))
19429, 17, 19divcan3d 11849 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) / 𝑅) = (√‘(1 − ((𝑡 / 𝑅)↑2))))
195104adantr 481 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℝ)
1963sqge0d 14059 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ ℝ+ → 0 ≤ (𝑅↑2))
197196adantr 481 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ (𝑅↑2))
198195, 197, 87, 136sqrtmuld 15227 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = ((√‘(𝑅↑2)) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
1992adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℂ)
200199, 26, 27subdid 11524 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))))
201199mulid1d 11085 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · 1) = (𝑅↑2))
20216, 17, 19sqdivd 13970 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2)))
203202oveq2d 7345 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))))
20416sqcld 13955 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡↑2) ∈ ℂ)
205 sqne0 13936 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑅 ∈ ℂ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0))
2061, 205syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ ℝ+ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0))
20718, 206mpbird 256 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∈ ℝ+ → (𝑅↑2) ≠ 0)
208207adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ≠ 0)
209204, 199, 208divcan2d 11846 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))) = (𝑡↑2))
210203, 209eqtrd 2776 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = (𝑡↑2))
211201, 210oveq12d 7347 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2)))
212200, 211eqtrd 2776 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2)))
213212fveq2d 6823 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2))))
214109adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ 𝑅)
21584, 214sqrtsqd 15222 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(𝑅↑2)) = 𝑅)
216215oveq1d 7344 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((√‘(𝑅↑2)) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
217198, 213, 2163eqtr3rd 2785 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2))))
218217oveq2d 7345 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((1 / 𝑅) · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2)))))
219193, 194, 2183eqtr3d 2784 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) = ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2)))))
220219mpteq2dva 5189 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))))
221 cncfmptc 24173 . . . . . . . . . . . . . 14 (((1 / 𝑅) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (1 / 𝑅)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
222179, 8, 10, 221syl3anc 1370 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (1 / 𝑅)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
223 areacirclem2 35964 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑡↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
2243, 109, 223syl2anc 584 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑡↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
225222, 224mulcncf 24708 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
226220, 225eqeltrd 2837 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
22713, 15, 191, 226cncfmpt2f 24176 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
228 cncfcdm 24159 . . . . . . . . . 10 (((ℂ ∖ (-∞(,]0)) ⊆ ℂ ∧ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) → ((𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) ↔ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))):(-𝑅[,]𝑅)⟶(ℂ ∖ (-∞(,]0))))
229176, 227, 228syl2anc 584 . . . . . . . . 9 (𝑅 ∈ ℝ+ → ((𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) ↔ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))):(-𝑅[,]𝑅)⟶(ℂ ∖ (-∞(,]0))))
230175, 229mpbird 256 . . . . . . . 8 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))))
231 eqid 2736 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) = ((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅))
232 eqid 2736 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0))) = ((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0)))
23313, 231, 232cncfcn 24171 . . . . . . . . 9 (((-𝑅[,]𝑅) ⊆ ℂ ∧ (ℂ ∖ (-∞(,]0)) ⊆ ℂ) → ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) = (((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0)))))
2348, 176, 233syl2anc 584 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) = (((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0)))))
235230, 234eleqtrd 2839 . . . . . . 7 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ (((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0)))))
236 eqid 2736 . . . . . . . . . 10 (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
237236logcn 25900 . . . . . . . . 9 (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ)
238 difss 4077 . . . . . . . . . 10 (ℂ ∖ (-∞(,]0)) ⊆ ℂ
239 eqid 2736 . . . . . . . . . . 11 ((TopOpen‘ℂfld) ↾t ℂ) = ((TopOpen‘ℂfld) ↾t ℂ)
24013, 232, 239cncfcn 24171 . . . . . . . . . 10 (((ℂ ∖ (-∞(,]0)) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((ℂ ∖ (-∞(,]0))–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0))) Cn ((TopOpen‘ℂfld) ↾t ℂ)))
241238, 9, 240mp2an 689 . . . . . . . . 9 ((ℂ ∖ (-∞(,]0))–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0))) Cn ((TopOpen‘ℂfld) ↾t ℂ))
242237, 241eleqtri 2835 . . . . . . . 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 22913 . . . . . 6 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) ∈ (((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld) ↾t ℂ)))
24513, 231, 239cncfcn 24171 . . . . . . 7 (((-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((-𝑅[,]𝑅)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld) ↾t ℂ)))
2468, 10, 245syl2anc 584 . . . . . 6 (𝑅 ∈ ℝ+ → ((-𝑅[,]𝑅)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld) ↾t ℂ)))
247244, 246eleqtrrd 2840 . . . . 5 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
248170, 247mulcncf 24708 . . . 4 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
249166, 248eqeltrd 2837 . . 3 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (arcsin‘(𝑡 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
250219oveq2d 7345 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = ((𝑡 / 𝑅) · ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))))
251199, 204subcld 11425 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
252251sqrtcld 15240 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
25320, 180, 252mulassd 11091 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (((𝑡 / 𝑅) · (1 / 𝑅)) · (√‘((𝑅↑2) − (𝑡↑2)))) = ((𝑡 / 𝑅) · ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))))
25416, 17, 19divrecd 11847 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) = (𝑡 · (1 / 𝑅)))
255254oveq1d 7344 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (1 / 𝑅)) = ((𝑡 · (1 / 𝑅)) · (1 / 𝑅)))
25616, 180, 180mulassd 11091 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 · (1 / 𝑅)) · (1 / 𝑅)) = (𝑡 · ((1 / 𝑅) · (1 / 𝑅))))
257255, 256eqtrd 2776 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (1 / 𝑅)) = (𝑡 · ((1 / 𝑅) · (1 / 𝑅))))
258257oveq1d 7344 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (((𝑡 / 𝑅) · (1 / 𝑅)) · (√‘((𝑅↑2) − (𝑡↑2)))) = ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2)))))
259250, 253, 2583eqtr2d 2782 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2)))))
260259mpteq2dva 5189 . . . 4 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2))))))
261179, 179mulcld 11088 . . . . . . 7 (𝑅 ∈ ℝ+ → ((1 / 𝑅) · (1 / 𝑅)) ∈ ℂ)
262 cncfmptc 24173 . . . . . . 7 ((((1 / 𝑅) · (1 / 𝑅)) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
263261, 8, 10, 262syl3anc 1370 . . . . . 6 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
264189, 263mulcncf 24708 . . . . 5 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (𝑡 · ((1 / 𝑅) · (1 / 𝑅)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
265264, 224mulcncf 24708 . . . 4 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
266260, 265eqeltrd 2837 . . 3 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
26713, 15, 249, 266cncfmpt2f 24176 . 2 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
26812, 267mulcncf 24708 1 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 844  w3a 1086   = wceq 1540  wcel 2105  wne 2940  cdif 3894  wss 3897   class class class wbr 5089  cmpt 5172  cres 5616  wf 6469  cfv 6473  (class class class)co 7329  cc 10962  cr 10963  0cc0 10964  1c1 10965  ici 10966   + caddc 10967   · cmul 10969  -∞cmnf 11100  *cxr 11101   < clt 11102  cle 11103  cmin 11298  -cneg 11299   / cdiv 11725  2c2 12121  +crp 12823  (,]cioc 13173  [,]cicc 13175  cexp 13875  csqrt 15035  abscabs 15036  t crest 17220  TopOpenctopn 17221  fldccnfld 20695  TopOnctopon 22157   Cn ccn 22473   ×t ctx 22809  cnccncf 24137  logclog 25808  arcsincasin 26110
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5226  ax-sep 5240  ax-nul 5247  ax-pow 5305  ax-pr 5369  ax-un 7642  ax-inf2 9490  ax-cnex 11020  ax-resscn 11021  ax-1cn 11022  ax-icn 11023  ax-addcl 11024  ax-addrcl 11025  ax-mulcl 11026  ax-mulrcl 11027  ax-mulcom 11028  ax-addass 11029  ax-mulass 11030  ax-distr 11031  ax-i2m1 11032  ax-1ne0 11033  ax-1rid 11034  ax-rnegex 11035  ax-rrecex 11036  ax-cnre 11037  ax-pre-lttri 11038  ax-pre-lttrn 11039  ax-pre-ltadd 11040  ax-pre-mulgt0 11041  ax-pre-sup 11042  ax-addf 11043  ax-mulf 11044
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-tp 4577  df-op 4579  df-uni 4852  df-int 4894  df-iun 4940  df-iin 4941  df-br 5090  df-opab 5152  df-mpt 5173  df-tr 5207  df-id 5512  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5569  df-se 5570  df-we 5571  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6232  df-ord 6299  df-on 6300  df-lim 6301  df-suc 6302  df-iota 6425  df-fun 6475  df-fn 6476  df-f 6477  df-f1 6478  df-fo 6479  df-f1o 6480  df-fv 6481  df-isom 6482  df-riota 7286  df-ov 7332  df-oprab 7333  df-mpo 7334  df-of 7587  df-om 7773  df-1st 7891  df-2nd 7892  df-supp 8040  df-frecs 8159  df-wrecs 8190  df-recs 8264  df-rdg 8303  df-1o 8359  df-2o 8360  df-er 8561  df-map 8680  df-pm 8681  df-ixp 8749  df-en 8797  df-dom 8798  df-sdom 8799  df-fin 8800  df-fsupp 9219  df-fi 9260  df-sup 9291  df-inf 9292  df-oi 9359  df-card 9788  df-pnf 11104  df-mnf 11105  df-xr 11106  df-ltxr 11107  df-le 11108  df-sub 11300  df-neg 11301  df-div 11726  df-nn 12067  df-2 12129  df-3 12130  df-4 12131  df-5 12132  df-6 12133  df-7 12134  df-8 12135  df-9 12136  df-n0 12327  df-z 12413  df-dec 12531  df-uz 12676  df-q 12782  df-rp 12824  df-xneg 12941  df-xadd 12942  df-xmul 12943  df-ioo 13176  df-ioc 13177  df-ico 13178  df-icc 13179  df-fz 13333  df-fzo 13476  df-fl 13605  df-mod 13683  df-seq 13815  df-exp 13876  df-fac 14081  df-bc 14110  df-hash 14138  df-shft 14869  df-cj 14901  df-re 14902  df-im 14903  df-sqrt 15037  df-abs 15038  df-limsup 15271  df-clim 15288  df-rlim 15289  df-sum 15489  df-ef 15868  df-sin 15870  df-cos 15871  df-tan 15872  df-pi 15873  df-struct 16937  df-sets 16954  df-slot 16972  df-ndx 16984  df-base 17002  df-ress 17031  df-plusg 17064  df-mulr 17065  df-starv 17066  df-sca 17067  df-vsca 17068  df-ip 17069  df-tset 17070  df-ple 17071  df-ds 17073  df-unif 17074  df-hom 17075  df-cco 17076  df-rest 17222  df-topn 17223  df-0g 17241  df-gsum 17242  df-topgen 17243  df-pt 17244  df-prds 17247  df-xrs 17302  df-qtop 17307  df-imas 17308  df-xps 17310  df-mre 17384  df-mrc 17385  df-acs 17387  df-mgm 18415  df-sgrp 18464  df-mnd 18475  df-submnd 18520  df-mulg 18789  df-cntz 19011  df-cmn 19475  df-psmet 20687  df-xmet 20688  df-met 20689  df-bl 20690  df-mopn 20691  df-fbas 20692  df-fg 20693  df-cnfld 20696  df-top 22141  df-topon 22158  df-topsp 22180  df-bases 22194  df-cld 22268  df-ntr 22269  df-cls 22270  df-nei 22347  df-lp 22385  df-perf 22386  df-cn 22476  df-cnp 22477  df-haus 22564  df-cmp 22636  df-tx 22811  df-hmeo 23004  df-fil 23095  df-fm 23187  df-flim 23188  df-flf 23189  df-xms 23571  df-ms 23572  df-tms 23573  df-cncf 24139  df-limc 25128  df-dv 25129  df-log 25810  df-cxp 25811  df-asin 26113
This theorem is referenced by:  areacirc  35968
  Copyright terms: Public domain W3C validator