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

Theorem areacirclem4 33633
 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 11879 . . . 4 (𝑅 ∈ ℝ+𝑅 ∈ ℂ)
21sqcld 13046 . . 3 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℂ)
3 rpre 11877 . . . . . 6 (𝑅 ∈ ℝ+𝑅 ∈ ℝ)
43renegcld 10495 . . . . 5 (𝑅 ∈ ℝ+ → -𝑅 ∈ ℝ)
5 iccssre 12293 . . . . 5 ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (-𝑅[,]𝑅) ⊆ ℝ)
64, 3, 5syl2anc 694 . . . 4 (𝑅 ∈ ℝ+ → (-𝑅[,]𝑅) ⊆ ℝ)
7 ax-resscn 10031 . . . 4 ℝ ⊆ ℂ
86, 7syl6ss 3648 . . 3 (𝑅 ∈ ℝ+ → (-𝑅[,]𝑅) ⊆ ℂ)
9 ssid 3657 . . . 4 ℂ ⊆ ℂ
109a1i 11 . . 3 (𝑅 ∈ ℝ+ → ℂ ⊆ ℂ)
11 cncfmptc 22761 . . 3 (((𝑅↑2) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (𝑅↑2)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
122, 8, 10, 11syl3anc 1366 . 2 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (𝑅↑2)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
13 eqid 2651 . . 3 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
1413addcn 22715 . . . 4 + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
1514a1i 11 . . 3 (𝑅 ∈ ℝ+ → + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
168sselda 3636 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℂ)
171adantr 480 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 𝑅 ∈ ℂ)
18 rpne0 11886 . . . . . . . . 9 (𝑅 ∈ ℝ+𝑅 ≠ 0)
1918adantr 480 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 𝑅 ≠ 0)
2016, 17, 19divcld 10839 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) ∈ ℂ)
21 asinval 24654 . . . . . . 7 ((𝑡 / 𝑅) ∈ ℂ → (arcsin‘(𝑡 / 𝑅)) = (-i · (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
2220, 21syl 17 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (arcsin‘(𝑡 / 𝑅)) = (-i · (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
23 ax-icn 10033 . . . . . . . . . . . 12 i ∈ ℂ
2423a1i 11 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → i ∈ ℂ)
2524, 20mulcld 10098 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (i · (𝑡 / 𝑅)) ∈ ℂ)
26 1cnd 10094 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 1 ∈ ℂ)
2720sqcld 13046 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℂ)
2826, 27subcld 10430 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℂ)
2928sqrtcld 14220 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℂ)
3025, 29addcld 10097 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℂ)
31 0lt1 10588 . . . . . . . . . . . . . . 15 0 < 1
32 simp3 1083 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → 𝑡 = 0)
3332oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (𝑡 / 𝑅) = (0 / 𝑅))
341, 18div0d 10838 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ ℝ+ → (0 / 𝑅) = 0)
35343ad2ant1 1102 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 / 𝑅) = 0)
3633, 35eqtrd 2685 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (𝑡 / 𝑅) = 0)
3736oveq2d 6706 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (i · (𝑡 / 𝑅)) = (i · 0))
38 it0e0 11292 . . . . . . . . . . . . . . . . . . . 20 (i · 0) = 0
3937, 38syl6eq 2701 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (i · (𝑡 / 𝑅)) = 0)
4036oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((𝑡 / 𝑅)↑2) = (0↑2))
4140oveq2d 6706 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (1 − ((𝑡 / 𝑅)↑2)) = (1 − (0↑2)))
4241fveq2d 6233 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (√‘(1 − ((𝑡 / 𝑅)↑2))) = (√‘(1 − (0↑2))))
43 sq0 12995 . . . . . . . . . . . . . . . . . . . . . . . 24 (0↑2) = 0
4443oveq2i 6701 . . . . . . . . . . . . . . . . . . . . . . 23 (1 − (0↑2)) = (1 − 0)
45 1m0e1 11169 . . . . . . . . . . . . . . . . . . . . . . 23 (1 − 0) = 1
4644, 45eqtri 2673 . . . . . . . . . . . . . . . . . . . . . 22 (1 − (0↑2)) = 1
4746fveq2i 6232 . . . . . . . . . . . . . . . . . . . . 21 (√‘(1 − (0↑2))) = (√‘1)
48 sqrt1 14056 . . . . . . . . . . . . . . . . . . . . 21 (√‘1) = 1
4947, 48eqtri 2673 . . . . . . . . . . . . . . . . . . . 20 (√‘(1 − (0↑2))) = 1
5042, 49syl6eq 2701 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (√‘(1 − ((𝑡 / 𝑅)↑2))) = 1)
5139, 50oveq12d 6708 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (0 + 1))
52 0p1e1 11170 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
5351, 52syl6eq 2701 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) = 1)
5453breq2d 4697 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ↔ 0 < 1))
55 0red 10079 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → 0 ∈ ℝ)
56 1red 10093 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → 1 ∈ ℝ)
5753, 56eqeltrd 2730 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
5855, 57ltnled 10222 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ↔ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
5954, 58bitr3d 270 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → (0 < 1 ↔ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
6031, 59mpbii 223 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 = 0) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0)
61603expa 1284 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 = 0) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0)
6261olcd 407 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 = 0) → (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
63 inelr 11048 . . . . . . . . . . . . . 14 ¬ i ∈ ℝ
6425, 29pncand 10431 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (i · (𝑡 / 𝑅)))
65643adant3 1101 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (i · (𝑡 / 𝑅)))
6665oveq1d 6705 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)) = ((i · (𝑡 / 𝑅)) · (𝑅 / 𝑡)))
6723a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → i ∈ ℂ)
68203adant3 1101 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (𝑡 / 𝑅) ∈ ℂ)
6913ad2ant1 1102 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑅 ∈ ℂ)
70163adant3 1101 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
71 simp3 1083 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑡 ≠ 0)
7269, 70, 71divcld 10839 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (𝑅 / 𝑡) ∈ ℂ)
7367, 68, 72mulassd 10101 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((i · (𝑡 / 𝑅)) · (𝑅 / 𝑡)) = (i · ((𝑡 / 𝑅) · (𝑅 / 𝑡))))
7466, 73eqtrd 2685 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)) = (i · ((𝑡 / 𝑅) · (𝑅 / 𝑡))))
75183ad2ant1 1102 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑅 ≠ 0)
7670, 69, 71, 75divcan6d 10858 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → ((𝑡 / 𝑅) · (𝑅 / 𝑡)) = 1)
7776oveq2d 6706 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (i · ((𝑡 / 𝑅) · (𝑅 / 𝑡))) = (i · 1))
7867mulid1d 10095 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (i · 1) = i)
7974, 77, 783eqtrrd 2690 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → i = ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)))
8079adantr 480 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → i = ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)))
81 simpr 476 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
82 1red 10093 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 1 ∈ ℝ)
836sselda 3636 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 𝑡 ∈ ℝ)
843adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 𝑅 ∈ ℝ)
8583, 84, 19redivcld 10891 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) ∈ ℝ)
8685resqcld 13075 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅)↑2) ∈ ℝ)
8782, 86resubcld 10496 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (1 − ((𝑡 / 𝑅)↑2)) ∈ ℝ)
88 elicc2 12276 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((-𝑅 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅)))
894, 3, 88syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↔ (𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅)))
90 1red 10093 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 1 ∈ ℝ)
91 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
923adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
9318adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ≠ 0)
9491, 92, 93redivcld 10891 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡 / 𝑅) ∈ ℝ)
9594resqcld 13075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡 / 𝑅)↑2) ∈ ℝ)
9690, 95subge0d 10655 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (0 ≤ (1 − ((𝑡 / 𝑅)↑2)) ↔ ((𝑡 / 𝑅)↑2) ≤ 1))
97 recn 10064 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
9897adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑡 ∈ ℂ)
991adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 𝑅 ∈ ℂ)
10098, 99, 93sqdivd 13061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2)))
101100breq1d 4695 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((𝑡 / 𝑅)↑2) ≤ 1 ↔ ((𝑡↑2) / (𝑅↑2)) ≤ 1))
102 resqcl 12971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℝ)
103102adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
1043resqcld 13075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℝ)
105 rpgt0 11882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑅 ∈ ℝ+ → 0 < 𝑅)
106 0red 10079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑅 ∈ ℝ+ → 0 ∈ ℝ)
107 0le0 11148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 0 ≤ 0
108107a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑅 ∈ ℝ+ → 0 ≤ 0)
109 rpge0 11883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑅 ∈ ℝ+ → 0 ≤ 𝑅)
110106, 3, 108, 109lt2sqd 13083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑅 ∈ ℝ+ → (0 < 𝑅 ↔ (0↑2) < (𝑅↑2)))
11143a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑅 ∈ ℝ+ → (0↑2) = 0)
112111breq1d 4695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑅 ∈ ℝ+ → ((0↑2) < (𝑅↑2) ↔ 0 < (𝑅↑2)))
113110, 112bitrd 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑅 ∈ ℝ+ → (0 < 𝑅 ↔ 0 < (𝑅↑2)))
114105, 113mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑅 ∈ ℝ+ → 0 < (𝑅↑2))
115104, 114elrpd 11907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑅 ∈ ℝ+ → (𝑅↑2) ∈ ℝ+)
116115adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ+)
117103, 90, 116ledivmuld 11963 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((𝑡↑2) / (𝑅↑2)) ≤ 1 ↔ (𝑡↑2) ≤ ((𝑅↑2) · 1)))
118 absresq 14086 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 ∈ ℝ → ((abs‘𝑡)↑2) = (𝑡↑2))
119118eqcomd 2657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑡 ∈ ℝ → (𝑡↑2) = ((abs‘𝑡)↑2))
1202mulid1d 10095 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑅 ∈ ℝ+ → ((𝑅↑2) · 1) = (𝑅↑2))
121119, 120breqan12rd 4702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡↑2) ≤ ((𝑅↑2) · 1) ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
12297abscld 14219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 ∈ ℝ → (abs‘𝑡) ∈ ℝ)
123122adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
12497absge0d 14227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 ∈ ℝ → 0 ≤ (abs‘𝑡))
125124adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
126109adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → 0 ≤ 𝑅)
127123, 92, 125, 126le2sqd 13084 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
12891, 92absled 14213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ (-𝑅𝑡𝑡𝑅)))
129121, 127, 1283bitr2d 296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((𝑡↑2) ≤ ((𝑅↑2) · 1) ↔ (-𝑅𝑡𝑡𝑅)))
130117, 129bitrd 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → (((𝑡↑2) / (𝑅↑2)) ≤ 1 ↔ (-𝑅𝑡𝑡𝑅)))
13196, 101, 1303bitrrd 295 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅𝑡𝑡𝑅) ↔ 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
132131biimpd 219 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑅 ∈ ℝ+𝑡 ∈ ℝ) → ((-𝑅𝑡𝑡𝑅) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
133132exp4b 631 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑅 ∈ ℝ+ → (𝑡 ∈ ℝ → (-𝑅𝑡 → (𝑡𝑅 → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))))
1341333impd 1303 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑅 ∈ ℝ+ → ((𝑡 ∈ ℝ ∧ -𝑅𝑡𝑡𝑅) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
13589, 134sylbid 230 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2))))
136135imp 444 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ (1 − ((𝑡 / 𝑅)↑2)))
13787, 136resqrtcld 14200 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℝ)
1381373adant3 1101 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℝ)
139138adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → (√‘(1 − ((𝑡 / 𝑅)↑2))) ∈ ℝ)
14081, 139resubcld 10496 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
14133ad2ant1 1102 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑅 ∈ ℝ)
142833adant3 1101 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℝ)
143141, 142, 71redivcld 10891 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (𝑅 / 𝑡) ∈ ℝ)
144143adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → (𝑅 / 𝑡) ∈ ℝ)
145140, 144remulcld 10108 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) − (√‘(1 − ((𝑡 / 𝑅)↑2)))) · (𝑅 / 𝑡)) ∈ ℝ)
14680, 145eqeltrd 2730 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ) → i ∈ ℝ)
147146ex 449 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅) ∧ 𝑡 ≠ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ → i ∈ ℝ))
1481473expa 1284 . . . . . . . . . . . . . 14 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 ≠ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ → i ∈ ℝ))
14963, 148mtoi 190 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 ≠ 0) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ)
150149orcd 406 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) ∧ 𝑡 ≠ 0) → (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
15162, 150pm2.61dane 2910 . . . . . . . . . . 11 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
152 ianor 508 . . . . . . . . . . 11 (¬ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0) ↔ (¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∨ ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
153151, 152sylibr 224 . . . . . . . . . 10 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ¬ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
154 mnfxr 10134 . . . . . . . . . . . 12 -∞ ∈ ℝ*
155 0re 10078 . . . . . . . . . . . 12 0 ∈ ℝ
156 elioc2 12274 . . . . . . . . . . . 12 ((-∞ ∈ ℝ* ∧ 0 ∈ ℝ) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0) ↔ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ -∞ < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0)))
157154, 155, 156mp2an 708 . . . . . . . . . . 11 (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0) ↔ (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ -∞ < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
158 3simpb 1079 . . . . . . . . . . 11 ((((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ -∞ < ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
159157, 158sylbi 207 . . . . . . . . . 10 (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0) → (((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℝ ∧ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ≤ 0))
160153, 159nsyl 135 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ¬ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (-∞(,]0))
16130, 160eldifd 3618 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ (ℂ ∖ (-∞(,]0)))
162 fvres 6245 . . . . . . . 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 6706 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) = (-i · (log‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
16522, 164eqtr4d 2688 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (arcsin‘(𝑡 / 𝑅)) = (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))))
166165mpteq2dva 4777 . . . 4 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (arcsin‘(𝑡 / 𝑅))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))))))
167 negicn 10320 . . . . . . 7 -i ∈ ℂ
168167a1i 11 . . . . . 6 (𝑅 ∈ ℝ+ → -i ∈ ℂ)
169 cncfmptc 22761 . . . . . 6 ((-i ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ -i) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
170168, 8, 10, 169syl3anc 1366 . . . . 5 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ -i) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
17113cnfldtopon 22633 . . . . . . . . 9 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
172171a1i 11 . . . . . . . 8 (𝑅 ∈ ℝ+ → (TopOpen‘ℂfld) ∈ (TopOn‘ℂ))
173 resttopon 21013 . . . . . . . 8 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (-𝑅[,]𝑅) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) ∈ (TopOn‘(-𝑅[,]𝑅)))
174172, 8, 173syl2anc 694 . . . . . . 7 (𝑅 ∈ ℝ+ → ((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) ∈ (TopOn‘(-𝑅[,]𝑅)))
175 eqid 2651 . . . . . . . . . 10 (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))
176161, 175fmptd 6425 . . . . . . . . 9 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))):(-𝑅[,]𝑅)⟶(ℂ ∖ (-∞(,]0)))
177 difssd 3771 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → (ℂ ∖ (-∞(,]0)) ⊆ ℂ)
17816, 17, 19divrec2d 10843 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) = ((1 / 𝑅) · 𝑡))
179178oveq2d 6706 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (i · (𝑡 / 𝑅)) = (i · ((1 / 𝑅) · 𝑡)))
1801, 18reccld 10832 . . . . . . . . . . . . . . . 16 (𝑅 ∈ ℝ+ → (1 / 𝑅) ∈ ℂ)
181180adantr 480 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (1 / 𝑅) ∈ ℂ)
18224, 181, 16mulassd 10101 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((i · (1 / 𝑅)) · 𝑡) = (i · ((1 / 𝑅) · 𝑡)))
183179, 182eqtr4d 2688 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (i · (𝑡 / 𝑅)) = ((i · (1 / 𝑅)) · 𝑡))
184183mpteq2dva 4777 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (𝑡 / 𝑅))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (1 / 𝑅)) · 𝑡)))
18523a1i 11 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℝ+ → i ∈ ℂ)
186185, 180mulcld 10098 . . . . . . . . . . . . . 14 (𝑅 ∈ ℝ+ → (i · (1 / 𝑅)) ∈ ℂ)
187 cncfmptc 22761 . . . . . . . . . . . . . 14 (((i · (1 / 𝑅)) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
188186, 8, 10, 187syl3anc 1366 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
189 cncfmptid 22762 . . . . . . . . . . . . . 14 (((-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ 𝑡) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
1908, 10, 189syl2anc 694 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ 𝑡) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
191188, 190mulcncf 23261 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (1 / 𝑅)) · 𝑡)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
192184, 191eqeltrd 2730 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (i · (𝑡 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
19317, 29mulcld 10098 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ℂ)
194193, 17, 19divrec2d 10843 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) / 𝑅) = ((1 / 𝑅) · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))))
19529, 17, 19divcan3d 10844 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) / 𝑅) = (√‘(1 − ((𝑡 / 𝑅)↑2))))
196104adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℝ)
1973sqge0d 13076 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ ℝ+ → 0 ≤ (𝑅↑2))
198197adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ (𝑅↑2))
199196, 198, 87, 136sqrtmuld 14207 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = ((√‘(𝑅↑2)) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
2002adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ∈ ℂ)
201200, 26, 27subdid 10524 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))))
202200mulid1d 10095 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · 1) = (𝑅↑2))
20316, 17, 19sqdivd 13061 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅)↑2) = ((𝑡↑2) / (𝑅↑2)))
204203oveq2d 6706 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))))
20516sqcld 13046 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡↑2) ∈ ℂ)
206 sqne0 12970 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑅 ∈ ℂ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0))
2071, 206syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑅 ∈ ℝ+ → ((𝑅↑2) ≠ 0 ↔ 𝑅 ≠ 0))
20818, 207mpbird 247 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 ∈ ℝ+ → (𝑅↑2) ≠ 0)
209208adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅↑2) ≠ 0)
210205, 200, 209divcan2d 10841 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((𝑡↑2) / (𝑅↑2))) = (𝑡↑2))
211204, 210eqtrd 2685 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · ((𝑡 / 𝑅)↑2)) = (𝑡↑2))
212202, 211oveq12d 6708 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (((𝑅↑2) · 1) − ((𝑅↑2) · ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2)))
213201, 212eqtrd 2685 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2))) = ((𝑅↑2) − (𝑡↑2)))
214213fveq2d 6233 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) · (1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2))))
215109adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → 0 ≤ 𝑅)
21684, 215sqrtsqd 14202 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(𝑅↑2)) = 𝑅)
217216oveq1d 6705 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((√‘(𝑅↑2)) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))))
218199, 214, 2173eqtr3rd 2694 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (√‘((𝑅↑2) − (𝑡↑2))))
219218oveq2d 6706 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((1 / 𝑅) · (𝑅 · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2)))))
220194, 195, 2193eqtr3d 2693 . . . . . . . . . . . . 13 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘(1 − ((𝑡 / 𝑅)↑2))) = ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2)))))
221220mpteq2dva 4777 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘(1 − ((𝑡 / 𝑅)↑2)))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))))
222 cncfmptc 22761 . . . . . . . . . . . . . 14 (((1 / 𝑅) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (1 / 𝑅)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
223180, 8, 10, 222syl3anc 1366 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (1 / 𝑅)) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
224 areacirclem2 33631 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑡↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
2253, 109, 224syl2anc 694 . . . . . . . . . . . . 13 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘((𝑅↑2) − (𝑡↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
226223, 225mulcncf 23261 . . . . . . . . . . . 12 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
227221, 226eqeltrd 2730 . . . . . . . . . . 11 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (√‘(1 − ((𝑡 / 𝑅)↑2)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
22813, 15, 192, 227cncfmpt2f 22764 . . . . . . . . . 10 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
229 cncffvrn 22748 . . . . . . . . . 10 (((ℂ ∖ (-∞(,]0)) ⊆ ℂ ∧ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ)) → ((𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) ↔ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))):(-𝑅[,]𝑅)⟶(ℂ ∖ (-∞(,]0))))
230177, 228, 229syl2anc 694 . . . . . . . . 9 (𝑅 ∈ ℝ+ → ((𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) ↔ (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))):(-𝑅[,]𝑅)⟶(ℂ ∖ (-∞(,]0))))
231176, 230mpbird 247 . . . . . . . 8 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))))
232 eqid 2651 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) = ((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅))
233 eqid 2651 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0))) = ((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0)))
23413, 232, 233cncfcn 22759 . . . . . . . . 9 (((-𝑅[,]𝑅) ⊆ ℂ ∧ (ℂ ∖ (-∞(,]0)) ⊆ ℂ) → ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) = (((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0)))))
2358, 177, 234syl2anc 694 . . . . . . . 8 (𝑅 ∈ ℝ+ → ((-𝑅[,]𝑅)–cn→(ℂ ∖ (-∞(,]0))) = (((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0)))))
236231, 235eleqtrd 2732 . . . . . . 7 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ (((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0)))))
237 eqid 2651 . . . . . . . . . 10 (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
238237logcn 24438 . . . . . . . . 9 (log ↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ)
239 difss 3770 . . . . . . . . . 10 (ℂ ∖ (-∞(,]0)) ⊆ ℂ
240 eqid 2651 . . . . . . . . . . 11 ((TopOpen‘ℂfld) ↾t ℂ) = ((TopOpen‘ℂfld) ↾t ℂ)
24113, 233, 240cncfcn 22759 . . . . . . . . . 10 (((ℂ ∖ (-∞(,]0)) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((ℂ ∖ (-∞(,]0))–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0))) Cn ((TopOpen‘ℂfld) ↾t ℂ)))
242239, 9, 241mp2an 708 . . . . . . . . 9 ((ℂ ∖ (-∞(,]0))–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (ℂ ∖ (-∞(,]0))) Cn ((TopOpen‘ℂfld) ↾t ℂ))
243238, 242eleqtri 2728 . . . . . . . 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 21515 . . . . . 6 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) ∈ (((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld) ↾t ℂ)))
24613, 232, 240cncfcn 22759 . . . . . . 7 (((-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((-𝑅[,]𝑅)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld) ↾t ℂ)))
2478, 10, 246syl2anc 694 . . . . . 6 (𝑅 ∈ ℝ+ → ((-𝑅[,]𝑅)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (-𝑅[,]𝑅)) Cn ((TopOpen‘ℂfld) ↾t ℂ)))
248245, 247eleqtrrd 2733 . . . . 5 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2)))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
249170, 248mulcncf 23261 . . . 4 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (-i · ((log ↾ (ℂ ∖ (-∞(,]0)))‘((i · (𝑡 / 𝑅)) + (√‘(1 − ((𝑡 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
250166, 249eqeltrd 2730 . . 3 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (arcsin‘(𝑡 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
251220oveq2d 6706 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = ((𝑡 / 𝑅) · ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))))
252200, 205subcld 10430 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
253252sqrtcld 14220 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℂ)
25420, 181, 253mulassd 10101 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (((𝑡 / 𝑅) · (1 / 𝑅)) · (√‘((𝑅↑2) − (𝑡↑2)))) = ((𝑡 / 𝑅) · ((1 / 𝑅) · (√‘((𝑅↑2) − (𝑡↑2))))))
25516, 17, 19divrecd 10842 . . . . . . . . 9 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (𝑡 / 𝑅) = (𝑡 · (1 / 𝑅)))
256255oveq1d 6705 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (1 / 𝑅)) = ((𝑡 · (1 / 𝑅)) · (1 / 𝑅)))
25716, 181, 181mulassd 10101 . . . . . . . 8 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 · (1 / 𝑅)) · (1 / 𝑅)) = (𝑡 · ((1 / 𝑅) · (1 / 𝑅))))
258256, 257eqtrd 2685 . . . . . . 7 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (1 / 𝑅)) = (𝑡 · ((1 / 𝑅) · (1 / 𝑅))))
259258oveq1d 6705 . . . . . 6 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → (((𝑡 / 𝑅) · (1 / 𝑅)) · (√‘((𝑅↑2) − (𝑡↑2)))) = ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2)))))
260251, 254, 2593eqtr2d 2691 . . . . 5 ((𝑅 ∈ ℝ+𝑡 ∈ (-𝑅[,]𝑅)) → ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))) = ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2)))))
261260mpteq2dva 4777 . . . 4 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) = (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2))))))
262180, 180mulcld 10098 . . . . . . 7 (𝑅 ∈ ℝ+ → ((1 / 𝑅) · (1 / 𝑅)) ∈ ℂ)
263 cncfmptc 22761 . . . . . . 7 ((((1 / 𝑅) · (1 / 𝑅)) ∈ ℂ ∧ (-𝑅[,]𝑅) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
264262, 8, 10, 263syl3anc 1366 . . . . . 6 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((1 / 𝑅) · (1 / 𝑅))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
265190, 264mulcncf 23261 . . . . 5 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ (𝑡 · ((1 / 𝑅) · (1 / 𝑅)))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
266265, 225mulcncf 23261 . . . 4 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 · ((1 / 𝑅) · (1 / 𝑅))) · (√‘((𝑅↑2) − (𝑡↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
267261, 266eqeltrd 2730 . . 3 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
26813, 15, 250, 267cncfmpt2f 22764 . 2 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2)))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
26912, 268mulcncf 23261 1 (𝑅 ∈ ℝ+ → (𝑡 ∈ (-𝑅[,]𝑅) ↦ ((𝑅↑2) · ((arcsin‘(𝑡 / 𝑅)) + ((𝑡 / 𝑅) · (√‘(1 − ((𝑡 / 𝑅)↑2))))))) ∈ ((-𝑅[,]𝑅)–cn→ℂ))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   ≠ wne 2823   ∖ cdif 3604   ⊆ wss 3607   class class class wbr 4685   ↦ cmpt 4762   ↾ cres 5145  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975  ici 9976   + caddc 9977   · cmul 9979  -∞cmnf 10110  ℝ*cxr 10111   < clt 10112   ≤ cle 10113   − cmin 10304  -cneg 10305   / cdiv 10722  2c2 11108  ℝ+crp 11870  (,]cioc 12214  [,]cicc 12216  ↑cexp 12900  √csqrt 14017  abscabs 14018   ↾t crest 16128  TopOpenctopn 16129  ℂfldccnfld 19794  TopOnctopon 20763   Cn ccn 21076   ×t ctx 21411  –cn→ccncf 22726  logclog 24346  arcsincasin 24634 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ioc 12218  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-fac 13101  df-bc 13130  df-hash 13158  df-shft 13851  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-limsup 14246  df-clim 14263  df-rlim 14264  df-sum 14461  df-ef 14842  df-sin 14844  df-cos 14845  df-tan 14846  df-pi 14847  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-starv 16003  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-unif 16012  df-hom 16013  df-cco 16014  df-rest 16130  df-topn 16131  df-0g 16149  df-gsum 16150  df-topgen 16151  df-pt 16152  df-prds 16155  df-xrs 16209  df-qtop 16214  df-imas 16215  df-xps 16217  df-mre 16293  df-mrc 16294  df-acs 16296  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383  df-mulg 17588  df-cntz 17796  df-cmn 18241  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-fbas 19791  df-fg 19792  df-cnfld 19795  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cld 20871  df-ntr 20872  df-cls 20873  df-nei 20950  df-lp 20988  df-perf 20989  df-cn 21079  df-cnp 21080  df-haus 21167  df-cmp 21238  df-tx 21413  df-hmeo 21606  df-fil 21697  df-fm 21789  df-flim 21790  df-flf 21791  df-xms 22172  df-ms 22173  df-tms 22174  df-cncf 22728  df-limc 23675  df-dv 23676  df-log 24348  df-cxp 24349  df-asin 24637 This theorem is referenced by:  areacirc  33635
 Copyright terms: Public domain W3C validator