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 32497
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 11676 . . . 4 (𝑅 ∈ ℝ+𝑅 ∈ ℂ)
21sqcld 12826 . . 3 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℂ)
3 rpre 11674 . . . . . 6 (𝑅 ∈ ℝ+𝑅 ∈ ℝ)
43renegcld 10309 . . . . 5 (𝑅 ∈ ℝ+ → -𝑅 ∈ ℝ)
5 iccssre 12085 . . . . 5 ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (-𝑅[,]𝑅) ⊆ ℝ)
64, 3, 5syl2anc 690 . . . 4 (𝑅 ∈ ℝ+ → (-𝑅[,]𝑅) ⊆ ℝ)
7 ax-resscn 9850 . . . 4 ℝ ⊆ ℂ
86, 7syl6ss 3579 . . 3 (𝑅 ∈ ℝ+ → (-𝑅[,]𝑅) ⊆ ℂ)
9 ssid 3586 . . . 4 ℂ ⊆ ℂ
109a1i 11 . . 3 (𝑅 ∈ ℝ+ → ℂ ⊆ ℂ)
11 cncfmptc 22470 . . 3 (((𝑅↑2) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (𝑅↑2)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
122, 8, 10, 11syl3anc 1317 . 2 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (𝑅↑2)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
13 eqid 2609 . . 3 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
1413addcn 22424 . . . 4 + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
1514a1i 11 . . 3 (𝑅 ∈ ℝ+ → + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
168sselda 3567 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℂ)
171adantr 479 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 𝑅 ∈ ℂ)
18 rpne0 11683 . . . . . . . . 9 (𝑅 ∈ ℝ+𝑅 ≠ 0)
1918adantr 479 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 𝑅 ≠ 0)
2016, 17, 19divcld 10653 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) ∈ ℂ)
21 asinval 24354 . . . . . . 7 ((𝑡 / 𝑅) ∈ ℂ → (arcsin‘(𝑡 / 𝑅)) = (-i · (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
2220, 21syl 17 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (arcsin‘(𝑡 / 𝑅)) = (-i · (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
23 ax-icn 9852 . . . . . . . . . . . 12 i ∈ ℂ
2423a1i 11 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → i ∈ ℂ)
2524, 20mulcld 9917 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (i · (𝑡 / 𝑅)) ∈ ℂ)
26 1cnd 9913 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 1 ∈ ℂ)
2720sqcld 12826 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℂ)
2826, 27subcld 10244 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℂ)
2928sqrtcld 13973 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℂ)
3025, 29addcld 9916 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℂ)
31 0lt1 10402 . . . . . . . . . . . . . . 15 0 < 1
32 simp3 1055 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → 𝑡 = 0)
3332oveq1d 6542 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (𝑡 / 𝑅) = (0 / 𝑅))
341, 18div0d 10652 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ ℝ+ → (0 / 𝑅) = 0)
35343ad2ant1 1074 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 / 𝑅) = 0)
3633, 35eqtrd 2643 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (𝑡 / 𝑅) = 0)
3736oveq2d 6543 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (i · (𝑡 / 𝑅)) = (i · 0))
38 it0e0 11104 . . . . . . . . . . . . . . . . . . . 20 (i · 0) = 0
3937, 38syl6eq 2659 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (i · (𝑡 / 𝑅)) = 0)
4036oveq1d 6542 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((𝑡 / 𝑅)↑2) = (0↑2))
4140oveq2d 6543 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (1 − ((𝑡 / 𝑅)↑2)) = (1 − (0↑2)))
4241fveq2d 6092 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (√‘(1 − ((𝑡 / 𝑅)↑2))) = (√‘(1 − (0↑2))))
43 sq0 12775 . . . . . . . . . . . . . . . . . . . . . . . 24 (0↑2) = 0
4443oveq2i 6538 . . . . . . . . . . . . . . . . . . . . . . 23 (1 − (0↑2)) = (1 − 0)
45 1m0e1 10981 . . . . . . . . . . . . . . . . . . . . . . 23 (1 − 0) = 1
4644, 45eqtri 2631 . . . . . . . . . . . . . . . . . . . . . 22 (1 − (0↑2)) = 1
4746fveq2i 6091 . . . . . . . . . . . . . . . . . . . . 21 (√‘(1 − (0↑2))) = (√‘1)
48 sqrt1 13809 . . . . . . . . . . . . . . . . . . . . 21 (√‘1) = 1
4947, 48eqtri 2631 . . . . . . . . . . . . . . . . . . . 20 (√‘(1 − (0↑2))) = 1
5042, 49syl6eq 2659 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (√‘(1 − ((𝑡 / 𝑅)↑2))) = 1)
5139, 50oveq12d 6545 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (0 + 1))
52 0p1e1 10982 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
5351, 52syl6eq 2659 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) = 1)
5453breq2d 4589 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ↔ 0 < 1))
55 0red 9898 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → 0 ∈ ℝ)
56 1red 9912 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → 1 ∈ ℝ)
5753, 56eqeltrd 2687 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
5855, 57ltnled 10036 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ↔ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
5954, 58bitr3d 268 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 < 1 ↔ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
6031, 59mpbii 221 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0)
61603expa 1256 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 = 0) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0)
6261olcd 406 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 = 0) → (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
63 inelr 10860 . . . . . . . . . . . . . 14 ¬ i ∈ ℝ
6425, 29pncand 10245 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (i · (𝑡 / 𝑅)))
65643adant3 1073 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (i · (𝑡 / 𝑅)))
6665oveq1d 6542 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)) = ((i · (𝑡 / 𝑅)) · (𝑅 / 𝑡)))
6723a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → i ∈ ℂ)
68203adant3 1073 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (𝑡 / 𝑅) ∈ ℂ)
6913ad2ant1 1074 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑅 ∈ ℂ)
70163adant3 1073 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
71 simp3 1055 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑡 ≠ 0)
7269, 70, 71divcld 10653 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (𝑅 / 𝑡) ∈ ℂ)
7367, 68, 72mulassd 9920 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((i · (𝑡 / 𝑅)) · (𝑅 / 𝑡)) = (i · ((𝑡 / 𝑅) · (𝑅 / 𝑡))))
7466, 73eqtrd 2643 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)) = (i · ((𝑡 / 𝑅) · (𝑅 / 𝑡))))
75183ad2ant1 1074 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑅 ≠ 0)
7670, 69, 71, 75divcan6d 10672 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((𝑡 / 𝑅) · (𝑅 / 𝑡)) = 1)
7776oveq2d 6543 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (i · ((𝑡 / 𝑅) · (𝑅 / 𝑡))) = (i · 1))
7867mulid1d 9914 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (i · 1) = i)
7974, 77, 783eqtrrd 2648 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → i = ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)))
8079adantr 479 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → i = ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)))
81 simpr 475 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
82 1red 9912 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 1 ∈ ℝ)
836sselda 3567 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℝ)
843adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 𝑅 ∈ ℝ)
8583, 84, 19redivcld 10705 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) ∈ ℝ)
8685resqcld 12855 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℝ)
8782, 86resubcld 10310 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℝ)
88 elicc2 12068 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅)))
894, 3, 88syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅)))
90 1red 9912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 1 ∈ ℝ)
91 simpr 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
923adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
9318adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ≠ 0)
9491, 92, 93redivcld 10705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡 / 𝑅) ∈ ℝ)
9594resqcld 12855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡 / 𝑅)↑2) ∈ ℝ)
9690, 95subge0d 10469 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (0 ≤ (1 − ((𝑡 / 𝑅)↑2)) ↔ ((𝑡 / 𝑅)↑2) ≤ 1))
97 recn 9883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
9897adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑡 ∈ ℂ)
991adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ∈ ℂ)
10098, 99, 93sqdivd 12841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2)))
101100breq1d 4587 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((𝑡 / 𝑅)↑2) ≤ 1 ↔ ((𝑡↑2) / (𝑅↑2)) ≤ 1))
102 resqcl 12751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℝ)
103102adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
1043resqcld 12855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℝ)
105 rpgt0 11679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑅 ∈ ℝ+ → 0 < 𝑅)
106 0red 9898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑅 ∈ ℝ+ → 0 ∈ ℝ)
107 0le0 10960 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 0 ≤ 0
108107a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑅 ∈ ℝ+ → 0 ≤ 0)
109 rpge0 11680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑅 ∈ ℝ+ → 0 ≤ 𝑅)
110106, 3, 108, 109lt2sqd 12863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑅 ∈ ℝ+ → (0 < 𝑅 ↔ (0↑2) < (𝑅↑2)))
11143a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑅 ∈ ℝ+ → (0↑2) = 0)
112111breq1d 4587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑅 ∈ ℝ+ → ((0↑2) < (𝑅↑2) ↔ 0 < (𝑅↑2)))
113110, 112bitrd 266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑅 ∈ ℝ+ → (0 < 𝑅 ↔ 0 < (𝑅↑2)))
114105, 113mpbid 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑅 ∈ ℝ+ → 0 < (𝑅↑2))
115104, 114elrpd 11704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℝ+)
116115adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ+)
117103, 90, 116ledivmuld 11760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((𝑡↑2) / (𝑅↑2)) ≤ 1 ↔ (𝑡↑2) ≤ ((𝑅↑2) · 1)))
118 absresq 13839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 ∈ ℝ → ((abs‘𝑡)↑2) = (𝑡↑2))
119118eqcomd 2615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑡 ∈ ℝ → (𝑡↑2) = ((abs‘𝑡)↑2))
1202mulid1d 9914 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑅 ∈ ℝ+ → ((𝑅↑2) · 1) = (𝑅↑2))
121119, 120breqan12rd 4594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡↑2) ≤ ((𝑅↑2) · 1) ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
12297abscld 13972 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 ∈ ℝ → (abs‘𝑡) ∈ ℝ)
123122adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
12497absge0d 13980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 ∈ ℝ → 0 ≤ (abs‘𝑡))
125124adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
126109adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 0 ≤ 𝑅)
127123, 92, 125, 126le2sqd 12864 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
12891, 92absled 13966 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ (-𝑅𝑡𝑡𝑅)))
129121, 127, 1283bitr2d 294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡↑2) ≤ ((𝑅↑2) · 1) ↔ (-𝑅𝑡𝑡𝑅)))
130117, 129bitrd 266 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((𝑡↑2) / (𝑅↑2)) ≤ 1 ↔ (-𝑅𝑡𝑡𝑅)))
13196, 101, 1303bitrrd 293 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅𝑡𝑡𝑅) ↔ 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
132131biimpd 217 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅𝑡𝑡𝑅) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
133132exp4b 629 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑅 ∈ ℝ+ → (𝑡 ∈ ℝ → (-𝑅𝑡 → (𝑡𝑅 → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))))
1341333impd 1272 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑅 ∈ ℝ+ → ((𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
13589, 134sylbid 228 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
136135imp 443 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2)))
13787, 136resqrtcld 13953 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℝ)
1381373adant3 1073 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℝ)
139138adantr 479 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℝ)
14081, 139resubcld 10310 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
14133ad2ant1 1074 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑅 ∈ ℝ)
142833adant3 1073 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℝ)
143141, 142, 71redivcld 10705 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (𝑅 / 𝑡) ∈ ℝ)
144143adantr 479 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → (𝑅 / 𝑡) ∈ ℝ)
145140, 144remulcld 9927 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)) ∈ ℝ)
14680, 145eqeltrd 2687 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → i ∈ ℝ)
147146ex 448 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ → i ∈ ℝ))
1481473expa 1256 . . . . . . . . . . . . . 14 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 ≠ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ → i ∈ ℝ))
14963, 148mtoi 188 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 ≠ 0) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
150149orcd 405 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 ≠ 0) → (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
15162, 150pm2.61dane 2868 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
152 ianor 507 . . . . . . . . . . 11 (¬ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0) ↔ (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
153151, 152sylibr 222 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ¬ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
154 mnfxr 11786 . . . . . . . . . . . 12 -∞ ∈ ℝ*
155 0re 9897 . . . . . . . . . . . 12 0 ∈ ℝ
156 elioc2 12066 . . . . . . . . . . . 12 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0) ↔ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ -∞ < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0)))
157154, 155, 156mp2an 703 . . . . . . . . . . 11 (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0) ↔ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ -∞ < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
158 3simpb 1051 . . . . . . . . . . 11 ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ -∞ < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
159157, 158sylbi 205 . . . . . . . . . 10 (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
160153, 159nsyl 133 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0))
16130, 160eldifd 3550 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (ℂ ∖ (-∞(,]0)))
162 fvres 6102 . . . . . . . 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 6543 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) = (-i · (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
16522, 164eqtr4d 2646 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (arcsin‘(𝑡 / 𝑅)) = (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
166165mpteq2dva 4666 . . . 4 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (arcsin‘(𝑡 / 𝑅))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))))))
167 negicn 10134 . . . . . . 7 -i ∈ ℂ
168167a1i 11 . . . . . 6 (𝑅 ∈ ℝ+ → -i ∈ ℂ)
169 cncfmptc 22470 . . . . . 6 ((-i ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ -i) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
170168, 8, 10, 169syl3anc 1317 . . . . 5 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ -i) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
17113cnfldtopon 22344 . . . . . . . . 9 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
172171a1i 11 . . . . . . . 8 (𝑅 ∈ ℝ+ → (TopOpen‘ℂfld) ∈ (TopOn‘ℂ))
173 resttopon 20723 . . . . . . . 8 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (-𝑅[,]𝑅) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) ∈ (TopOn‘(-𝑅[,]𝑅)))
174172, 8, 173syl2anc 690 . . . . . . 7 (𝑅 ∈ ℝ+ → ((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) ∈ (TopOn‘(-𝑅[,]𝑅)))
175 eqid 2609 . . . . . . . . . 10 (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))
176161, 175fmptd 6277 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))):(-𝑅[,]𝑅)⟶(ℂ ∖ (-∞(,]0)))
177 difssd 3699 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → (ℂ ∖ (-∞(,]0)) ⊆ ℂ)
17816, 17, 19divrec2d 10657 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) = ((1 / 𝑅) · 𝑡))
179178oveq2d 6543 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (i · (𝑡 / 𝑅)) = (i · ((1 / 𝑅) · 𝑡)))
1801, 18reccld 10646 . . . . . . . . . . . . . . . 16 (𝑅 ∈ ℝ+ → (1 / 𝑅) ∈ ℂ)
181180adantr 479 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (1 / 𝑅) ∈ ℂ)
18224, 181, 16mulassd 9920 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((i · (1 / 𝑅)) · 𝑡) = (i · ((1 / 𝑅) · 𝑡)))
183179, 182eqtr4d 2646 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (i · (𝑡 / 𝑅)) = ((i · (1 / 𝑅)) · 𝑡))
184183mpteq2dva 4666 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (𝑡 / 𝑅))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (1 / 𝑅)) · 𝑡)))
18523a1i 11 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ+ → i ∈ ℂ)
186185, 180mulcld 9917 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → (i · (1 / 𝑅)) ∈ ℂ)
187 cncfmptc 22470 . . . . . . . . . . . . . 14 (((i · (1 / 𝑅)) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
188186, 8, 10, 187syl3anc 1317 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
189 cncfmptid 22471 . . . . . . . . . . . . . 14 (((-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ 𝑡) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
1908, 10, 189syl2anc 690 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ 𝑡) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
191188, 190mulcncf 22968 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (1 / 𝑅)) · 𝑡)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
192184, 191eqeltrd 2687 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (𝑡 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
19317, 29mulcld 9917 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℂ)
194193, 17, 19divrec2d 10657 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) / 𝑅) = ((1 / 𝑅) · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))))
19529, 17, 19divcan3d 10658 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) / 𝑅) = (√‘(1 − ((𝑡 / 𝑅)↑2))))
196104adantr 479 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℝ)
1973sqge0d 12856 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ ℝ+ → 0 ≤ (𝑅↑2))
198197adantr 479 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ (𝑅↑2))
199196, 198, 87, 136sqrtmuld 13960 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = ((√‘(𝑅↑2)) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
2002adantr 479 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℂ)
201200, 26, 27subdid 10338 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))))
202200mulid1d 9914 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · 1) = (𝑅↑2))
20316, 17, 19sqdivd 12841 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2)))
204203oveq2d 6543 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))))
20516sqcld 12826 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡↑2) ∈ ℂ)
206 sqne0 12750 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑅 ∈ ℂ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0))
2071, 206syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ ℝ+ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0))
20818, 207mpbird 245 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∈ ℝ+ → (𝑅↑2) ≠ 0)
209208adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ≠ 0)
210205, 200, 209divcan2d 10655 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))) = (𝑡↑2))
211204, 210eqtrd 2643 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = (𝑡↑2))
212202, 211oveq12d 6545 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2)))
213201, 212eqtrd 2643 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2)))
214213fveq2d 6092 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2))))
215109adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ 𝑅)
21684, 215sqrtsqd 13955 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(𝑅↑2)) = 𝑅)
217216oveq1d 6542 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((√‘(𝑅↑2)) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
218199, 214, 2173eqtr3rd 2652 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2))))
219218oveq2d 6543 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((1 / 𝑅) · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2)))))
220194, 195, 2193eqtr3d 2651 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) = ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2)))))
221220mpteq2dva 4666 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))))
222 cncfmptc 22470 . . . . . . . . . . . . . 14 (((1 / 𝑅) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (1 / 𝑅)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
223180, 8, 10, 222syl3anc 1317 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (1 / 𝑅)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
224 areacirclem2 32495 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑡↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
2253, 109, 224syl2anc 690 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑡↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
226223, 225mulcncf 22968 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
227221, 226eqeltrd 2687 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
22813, 15, 192, 227cncfmpt2f 22473 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
229 cncffvrn 22457 . . . . . . . . . 10 (((ℂ ∖ (-∞(,]0)) ⊆ ℂ ∧ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) → ((𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) ↔ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))):(-𝑅[,]𝑅)⟶(ℂ ∖ (-∞(,]0))))
230177, 228, 229syl2anc 690 . . . . . . . . 9 (𝑅 ∈ ℝ+ → ((𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) ↔ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))):(-𝑅[,]𝑅)⟶(ℂ ∖ (-∞(,]0))))
231176, 230mpbird 245 . . . . . . . 8 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))))
232 eqid 2609 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) = ((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅))
233 eqid 2609 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0))) = ((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0)))
23413, 232, 233cncfcn 22468 . . . . . . . . 9 (((-𝑅[,]𝑅) ⊆ ℂ ∧ (ℂ ∖ (-∞(,]0)) ⊆ ℂ) → ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) = (((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0)))))
2358, 177, 234syl2anc 690 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) = (((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0)))))
236231, 235eleqtrd 2689 . . . . . . 7 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ (((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0)))))
237 eqid 2609 . . . . . . . . . 10 (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
238237logcn 24138 . . . . . . . . 9 (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ)
239 difss 3698 . . . . . . . . . 10 (ℂ ∖ (-∞(,]0)) ⊆ ℂ
240 eqid 2609 . . . . . . . . . . 11 ((TopOpen‘ℂfld) ↾t ℂ) = ((TopOpen‘ℂfld) ↾t ℂ)
24113, 233, 240cncfcn 22468 . . . . . . . . . 10 (((ℂ ∖ (-∞(,]0)) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((ℂ ∖ (-∞(,]0))–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0))) Cn ((TopOpen‘ℂfld) ↾t ℂ)))
242239, 9, 241mp2an 703 . . . . . . . . 9 ((ℂ ∖ (-∞(,]0))–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0))) Cn ((TopOpen‘ℂfld) ↾t ℂ))
243238, 242eleqtri 2685 . . . . . . . 8 (log ↾ (ℂ ∖ (-∞(,]0))) ∈ (((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0))) Cn ((TopOpen‘ℂfld) ↾t ℂ))
244243a1i 11 . . . . . . 7 (𝑅 ∈ ℝ+ → (log ↾ (ℂ ∖ (-∞(,]0))) ∈ (((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0))) Cn ((TopOpen‘ℂfld) ↾t ℂ)))
245174, 236, 244cnmpt11f 21225 . . . . . 6 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) ∈ (((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld) ↾t ℂ)))
24613, 232, 240cncfcn 22468 . . . . . . 7 (((-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((-𝑅[,]𝑅)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld) ↾t ℂ)))
2478, 10, 246syl2anc 690 . . . . . 6 (𝑅 ∈ ℝ+ → ((-𝑅[,]𝑅)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld) ↾t ℂ)))
248245, 247eleqtrrd 2690 . . . . 5 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
249170, 248mulcncf 22968 . . . 4 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
250166, 249eqeltrd 2687 . . 3 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (arcsin‘(𝑡 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
251220oveq2d 6543 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = ((𝑡 / 𝑅) · ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))))
252200, 205subcld 10244 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
253252sqrtcld 13973 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
25420, 181, 253mulassd 9920 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (((𝑡 / 𝑅) · (1 / 𝑅)) · (√‘((𝑅↑2) − (𝑡↑2)))) = ((𝑡 / 𝑅) · ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))))
25516, 17, 19divrecd 10656 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) = (𝑡 · (1 / 𝑅)))
256255oveq1d 6542 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (1 / 𝑅)) = ((𝑡 · (1 / 𝑅)) · (1 / 𝑅)))
25716, 181, 181mulassd 9920 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 · (1 / 𝑅)) · (1 / 𝑅)) = (𝑡 · ((1 / 𝑅) · (1 / 𝑅))))
258256, 257eqtrd 2643 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (1 / 𝑅)) = (𝑡 · ((1 / 𝑅) · (1 / 𝑅))))
259258oveq1d 6542 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (((𝑡 / 𝑅) · (1 / 𝑅)) · (√‘((𝑅↑2) − (𝑡↑2)))) = ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2)))))
260251, 254, 2593eqtr2d 2649 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2)))))
261260mpteq2dva 4666 . . . 4 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2))))))
262180, 180mulcld 9917 . . . . . . 7 (𝑅 ∈ ℝ+ → ((1 / 𝑅) · (1 / 𝑅)) ∈ ℂ)
263 cncfmptc 22470 . . . . . . 7 ((((1 / 𝑅) · (1 / 𝑅)) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
264262, 8, 10, 263syl3anc 1317 . . . . . 6 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
265190, 264mulcncf 22968 . . . . 5 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (𝑡 · ((1 / 𝑅) · (1 / 𝑅)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
266265, 225mulcncf 22968 . . . 4 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
267261, 266eqeltrd 2687 . . 3 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
26813, 15, 250, 267cncfmpt2f 22473 . 2 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
26912, 268mulcncf 22968 1 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2779  cdif 3536  wss 3539   class class class wbr 4577  cmpt 4637  cres 5030  wf 5786  cfv 5790  (class class class)co 6527  cc 9791  cr 9792  0cc0 9793  1c1 9794  ici 9795   + caddc 9796   · cmul 9798  -∞cmnf 9929  *cxr 9930   < clt 9931  cle 9932  cmin 10118  -cneg 10119   / cdiv 10536  2c2 10920  +crp 11667  (,]cioc 12006  [,]cicc 12008  cexp 12680  csqrt 13770  abscabs 13771  t crest 15853  TopOpenctopn 15854  fldccnfld 19516  TopOnctopon 20466   Cn ccn 20786   ×t ctx 21121  cnccncf 22435  logclog 24050  arcsincasin 24334
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-inf2 8399  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870  ax-pre-sup 9871  ax-addf 9872  ax-mulf 9873
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-iin 4452  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6773  df-om 6936  df-1st 7037  df-2nd 7038  df-supp 7161  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-1o 7425  df-2o 7426  df-oadd 7429  df-er 7607  df-map 7724  df-pm 7725  df-ixp 7773  df-en 7820  df-dom 7821  df-sdom 7822  df-fin 7823  df-fsupp 8137  df-fi 8178  df-sup 8209  df-inf 8210  df-oi 8276  df-card 8626  df-cda 8851  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-div 10537  df-nn 10871  df-2 10929  df-3 10930  df-4 10931  df-5 10932  df-6 10933  df-7 10934  df-8 10935  df-9 10936  df-n0 11143  df-z 11214  df-dec 11329  df-uz 11523  df-q 11624  df-rp 11668  df-xneg 11781  df-xadd 11782  df-xmul 11783  df-ioo 12009  df-ioc 12010  df-ico 12011  df-icc 12012  df-fz 12156  df-fzo 12293  df-fl 12413  df-mod 12489  df-seq 12622  df-exp 12681  df-fac 12881  df-bc 12910  df-hash 12938  df-shft 13604  df-cj 13636  df-re 13637  df-im 13638  df-sqrt 13772  df-abs 13773  df-limsup 13999  df-clim 14016  df-rlim 14017  df-sum 14214  df-ef 14586  df-sin 14588  df-cos 14589  df-tan 14590  df-pi 14591  df-struct 15646  df-ndx 15647  df-slot 15648  df-base 15649  df-sets 15650  df-ress 15651  df-plusg 15730  df-mulr 15731  df-starv 15732  df-sca 15733  df-vsca 15734  df-ip 15735  df-tset 15736  df-ple 15737  df-ds 15740  df-unif 15741  df-hom 15742  df-cco 15743  df-rest 15855  df-topn 15856  df-0g 15874  df-gsum 15875  df-topgen 15876  df-pt 15877  df-prds 15880  df-xrs 15934  df-qtop 15939  df-imas 15940  df-xps 15942  df-mre 16018  df-mrc 16019  df-acs 16021  df-mgm 17014  df-sgrp 17056  df-mnd 17067  df-submnd 17108  df-mulg 17313  df-cntz 17522  df-cmn 17967  df-psmet 19508  df-xmet 19509  df-met 19510  df-bl 19511  df-mopn 19512  df-fbas 19513  df-fg 19514  df-cnfld 19517  df-top 20469  df-bases 20470  df-topon 20471  df-topsp 20472  df-cld 20581  df-ntr 20582  df-cls 20583  df-nei 20660  df-lp 20698  df-perf 20699  df-cn 20789  df-cnp 20790  df-haus 20877  df-cmp 20948  df-tx 21123  df-hmeo 21316  df-fil 21408  df-fm 21500  df-flim 21501  df-flf 21502  df-xms 21883  df-ms 21884  df-tms 21885  df-cncf 22437  df-limc 23381  df-dv 23382  df-log 24052  df-cxp 24053  df-asin 24337
This theorem is referenced by:  areacirc  32499
  Copyright terms: Public domain W3C validator