Metamath Proof Explorer

Theorem areacirclem4

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

Ref Expression
Assertion areacirclem4 ( 𝑅 ∈ ℝ+ → ( 𝑡 ∈ ( - 𝑅 [,] 𝑅 ) ↦ ( ( 𝑅 ↑ 2 ) · ( ( arcsin ‘ ( 𝑡 / 𝑅 ) ) + ( ( 𝑡 / 𝑅 ) · ( √ ‘ ( 1 − ( ( 𝑡 / 𝑅 ) ↑ 2 ) ) ) ) ) ) ) ∈ ( ( - 𝑅 [,] 𝑅 ) –cn→ ℂ ) )

Proof

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