Metamath Proof Explorer


Theorem asinsin

Description: The arcsine function composed with sin is equal to the identity. This plus sinasin allow us to view sin and arcsin as inverse operations to each other. For ease of use, we have not defined precisely the correct domain of correctness of this identity; in addition to the main region described here it is also true forsome points on the branch cuts, namely when A = (pi / 2 ) - i y for nonnegative real y and also symmetrically at A =i y - ( pi / 2 ) . In particular, when restricted to reals this identity extends to the closed interval [ -u (pi / 2 ) , ( pi / 2 ) ] , not just the open interval (see reasinsin ). (Contributed by Mario Carneiro, 2-Apr-2015)

Ref Expression
Assertion asinsin ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( arcsin ‘ ( sin ‘ 𝐴 ) ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 sincl ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) ∈ ℂ )
2 1 adantr ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( sin ‘ 𝐴 ) ∈ ℂ )
3 asinval ( ( sin ‘ 𝐴 ) ∈ ℂ → ( arcsin ‘ ( sin ‘ 𝐴 ) ) = ( - i · ( log ‘ ( ( i · ( sin ‘ 𝐴 ) ) + ( √ ‘ ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) ) ) ) )
4 2 3 syl ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( arcsin ‘ ( sin ‘ 𝐴 ) ) = ( - i · ( log ‘ ( ( i · ( sin ‘ 𝐴 ) ) + ( √ ‘ ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) ) ) ) )
5 ax-icn i ∈ ℂ
6 mulcl ( ( i ∈ ℂ ∧ ( sin ‘ 𝐴 ) ∈ ℂ ) → ( i · ( sin ‘ 𝐴 ) ) ∈ ℂ )
7 5 2 6 sylancr ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( i · ( sin ‘ 𝐴 ) ) ∈ ℂ )
8 simpl ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 𝐴 ∈ ℂ )
9 mulcl ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
10 5 8 9 sylancr ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( i · 𝐴 ) ∈ ℂ )
11 efcl ( ( i · 𝐴 ) ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ )
12 10 11 syl ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ )
13 7 12 pncan3d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( i · ( sin ‘ 𝐴 ) ) + ( ( exp ‘ ( i · 𝐴 ) ) − ( i · ( sin ‘ 𝐴 ) ) ) ) = ( exp ‘ ( i · 𝐴 ) ) )
14 12 7 subcld ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( exp ‘ ( i · 𝐴 ) ) − ( i · ( sin ‘ 𝐴 ) ) ) ∈ ℂ )
15 ax-1cn 1 ∈ ℂ
16 2 sqcld ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( sin ‘ 𝐴 ) ↑ 2 ) ∈ ℂ )
17 subcl ( ( 1 ∈ ℂ ∧ ( ( sin ‘ 𝐴 ) ↑ 2 ) ∈ ℂ ) → ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ∈ ℂ )
18 15 16 17 sylancr ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ∈ ℂ )
19 binom2sub ( ( ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ ∧ ( i · ( sin ‘ 𝐴 ) ) ∈ ℂ ) → ( ( ( exp ‘ ( i · 𝐴 ) ) − ( i · ( sin ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( ( ( exp ‘ ( i · 𝐴 ) ) ↑ 2 ) − ( 2 · ( ( exp ‘ ( i · 𝐴 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) + ( ( i · ( sin ‘ 𝐴 ) ) ↑ 2 ) ) )
20 12 7 19 syl2anc ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( exp ‘ ( i · 𝐴 ) ) − ( i · ( sin ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( ( ( exp ‘ ( i · 𝐴 ) ) ↑ 2 ) − ( 2 · ( ( exp ‘ ( i · 𝐴 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) + ( ( i · ( sin ‘ 𝐴 ) ) ↑ 2 ) ) )
21 12 sqvald ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( exp ‘ ( i · 𝐴 ) ) ↑ 2 ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) )
22 2cn 2 ∈ ℂ
23 22 a1i ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 2 ∈ ℂ )
24 23 12 7 mul12d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 2 · ( ( exp ‘ ( i · 𝐴 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( 2 · ( i · ( sin ‘ 𝐴 ) ) ) ) )
25 21 24 oveq12d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( exp ‘ ( i · 𝐴 ) ) ↑ 2 ) − ( 2 · ( ( exp ‘ ( i · 𝐴 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) = ( ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) − ( ( exp ‘ ( i · 𝐴 ) ) · ( 2 · ( i · ( sin ‘ 𝐴 ) ) ) ) ) )
26 coscl ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ )
27 26 adantr ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( cos ‘ 𝐴 ) ∈ ℂ )
28 subsq ( ( ( cos ‘ 𝐴 ) ∈ ℂ ∧ ( i · ( sin ‘ 𝐴 ) ) ∈ ℂ ) → ( ( ( cos ‘ 𝐴 ) ↑ 2 ) − ( ( i · ( sin ‘ 𝐴 ) ) ↑ 2 ) ) = ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) · ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) ) )
29 27 7 28 syl2anc ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( cos ‘ 𝐴 ) ↑ 2 ) − ( ( i · ( sin ‘ 𝐴 ) ) ↑ 2 ) ) = ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) · ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) ) )
30 sqmul ( ( i ∈ ℂ ∧ ( sin ‘ 𝐴 ) ∈ ℂ ) → ( ( i · ( sin ‘ 𝐴 ) ) ↑ 2 ) = ( ( i ↑ 2 ) · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) )
31 5 2 30 sylancr ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( i · ( sin ‘ 𝐴 ) ) ↑ 2 ) = ( ( i ↑ 2 ) · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) )
32 i2 ( i ↑ 2 ) = - 1
33 32 oveq1i ( ( i ↑ 2 ) · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) = ( - 1 · ( ( sin ‘ 𝐴 ) ↑ 2 ) )
34 16 mulm1d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( - 1 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) = - ( ( sin ‘ 𝐴 ) ↑ 2 ) )
35 33 34 syl5eq ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( i ↑ 2 ) · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) = - ( ( sin ‘ 𝐴 ) ↑ 2 ) )
36 31 35 eqtrd ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( i · ( sin ‘ 𝐴 ) ) ↑ 2 ) = - ( ( sin ‘ 𝐴 ) ↑ 2 ) )
37 36 oveq2d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( cos ‘ 𝐴 ) ↑ 2 ) − ( ( i · ( sin ‘ 𝐴 ) ) ↑ 2 ) ) = ( ( ( cos ‘ 𝐴 ) ↑ 2 ) − - ( ( sin ‘ 𝐴 ) ↑ 2 ) ) )
38 27 sqcld ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( cos ‘ 𝐴 ) ↑ 2 ) ∈ ℂ )
39 38 16 subnegd ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( cos ‘ 𝐴 ) ↑ 2 ) − - ( ( sin ‘ 𝐴 ) ↑ 2 ) ) = ( ( ( cos ‘ 𝐴 ) ↑ 2 ) + ( ( sin ‘ 𝐴 ) ↑ 2 ) ) )
40 38 16 addcomd ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( cos ‘ 𝐴 ) ↑ 2 ) + ( ( sin ‘ 𝐴 ) ↑ 2 ) ) = ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) )
41 37 39 40 3eqtrd ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( cos ‘ 𝐴 ) ↑ 2 ) − ( ( i · ( sin ‘ 𝐴 ) ) ↑ 2 ) ) = ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) )
42 efival ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) = ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) )
43 42 adantr ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ ( i · 𝐴 ) ) = ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) )
44 7 2timesd ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 2 · ( i · ( sin ‘ 𝐴 ) ) ) = ( ( i · ( sin ‘ 𝐴 ) ) + ( i · ( sin ‘ 𝐴 ) ) ) )
45 43 44 oveq12d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( exp ‘ ( i · 𝐴 ) ) − ( 2 · ( i · ( sin ‘ 𝐴 ) ) ) ) = ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) − ( ( i · ( sin ‘ 𝐴 ) ) + ( i · ( sin ‘ 𝐴 ) ) ) ) )
46 27 7 7 pnpcan2d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) − ( ( i · ( sin ‘ 𝐴 ) ) + ( i · ( sin ‘ 𝐴 ) ) ) ) = ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) )
47 45 46 eqtrd ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( exp ‘ ( i · 𝐴 ) ) − ( 2 · ( i · ( sin ‘ 𝐴 ) ) ) ) = ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) )
48 43 47 oveq12d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( exp ‘ ( i · 𝐴 ) ) · ( ( exp ‘ ( i · 𝐴 ) ) − ( 2 · ( i · ( sin ‘ 𝐴 ) ) ) ) ) = ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) · ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) ) )
49 mulcl ( ( 2 ∈ ℂ ∧ ( i · ( sin ‘ 𝐴 ) ) ∈ ℂ ) → ( 2 · ( i · ( sin ‘ 𝐴 ) ) ) ∈ ℂ )
50 22 7 49 sylancr ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 2 · ( i · ( sin ‘ 𝐴 ) ) ) ∈ ℂ )
51 12 12 50 subdid ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( exp ‘ ( i · 𝐴 ) ) · ( ( exp ‘ ( i · 𝐴 ) ) − ( 2 · ( i · ( sin ‘ 𝐴 ) ) ) ) ) = ( ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) − ( ( exp ‘ ( i · 𝐴 ) ) · ( 2 · ( i · ( sin ‘ 𝐴 ) ) ) ) ) )
52 48 51 eqtr3d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) · ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) ) = ( ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) − ( ( exp ‘ ( i · 𝐴 ) ) · ( 2 · ( i · ( sin ‘ 𝐴 ) ) ) ) ) )
53 29 41 52 3eqtr3d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = ( ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) − ( ( exp ‘ ( i · 𝐴 ) ) · ( 2 · ( i · ( sin ‘ 𝐴 ) ) ) ) ) )
54 sincossq ( 𝐴 ∈ ℂ → ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = 1 )
55 54 adantr ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = 1 )
56 25 53 55 3eqtr2d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( exp ‘ ( i · 𝐴 ) ) ↑ 2 ) − ( 2 · ( ( exp ‘ ( i · 𝐴 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) = 1 )
57 56 36 oveq12d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( ( exp ‘ ( i · 𝐴 ) ) ↑ 2 ) − ( 2 · ( ( exp ‘ ( i · 𝐴 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) + ( ( i · ( sin ‘ 𝐴 ) ) ↑ 2 ) ) = ( 1 + - ( ( sin ‘ 𝐴 ) ↑ 2 ) ) )
58 negsub ( ( 1 ∈ ℂ ∧ ( ( sin ‘ 𝐴 ) ↑ 2 ) ∈ ℂ ) → ( 1 + - ( ( sin ‘ 𝐴 ) ↑ 2 ) ) = ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) )
59 15 16 58 sylancr ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 1 + - ( ( sin ‘ 𝐴 ) ↑ 2 ) ) = ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) )
60 20 57 59 3eqtrd ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( exp ‘ ( i · 𝐴 ) ) − ( i · ( sin ‘ 𝐴 ) ) ) ↑ 2 ) = ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) )
61 halfre ( 1 / 2 ) ∈ ℝ
62 61 a1i ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 1 / 2 ) ∈ ℝ )
63 negicn - i ∈ ℂ
64 mulcl ( ( - i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · 𝐴 ) ∈ ℂ )
65 63 8 64 sylancr ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( - i · 𝐴 ) ∈ ℂ )
66 efcl ( ( - i · 𝐴 ) ∈ ℂ → ( exp ‘ ( - i · 𝐴 ) ) ∈ ℂ )
67 65 66 syl ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ ( - i · 𝐴 ) ) ∈ ℂ )
68 12 67 addcld ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ )
69 68 recld ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ∈ ℝ )
70 halfgt0 0 < ( 1 / 2 )
71 70 a1i ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < ( 1 / 2 ) )
72 12 recld ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( exp ‘ ( i · 𝐴 ) ) ) ∈ ℝ )
73 67 recld ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℝ )
74 asinsinlem ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < ( ℜ ‘ ( exp ‘ ( i · 𝐴 ) ) ) )
75 negcl ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
76 75 adantr ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - 𝐴 ∈ ℂ )
77 reneg ( 𝐴 ∈ ℂ → ( ℜ ‘ - 𝐴 ) = - ( ℜ ‘ 𝐴 ) )
78 77 adantr ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ - 𝐴 ) = - ( ℜ ‘ 𝐴 ) )
79 halfpire ( π / 2 ) ∈ ℝ
80 79 renegcli - ( π / 2 ) ∈ ℝ
81 recl ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℝ )
82 iooneg ( ( - ( π / 2 ) ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ∧ ( ℜ ‘ 𝐴 ) ∈ ℝ ) → ( ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ↔ - ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) - - ( π / 2 ) ) ) )
83 80 79 81 82 mp3an12i ( 𝐴 ∈ ℂ → ( ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ↔ - ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) - - ( π / 2 ) ) ) )
84 83 biimpa ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) - - ( π / 2 ) ) )
85 79 recni ( π / 2 ) ∈ ℂ
86 85 negnegi - - ( π / 2 ) = ( π / 2 )
87 86 oveq2i ( - ( π / 2 ) (,) - - ( π / 2 ) ) = ( - ( π / 2 ) (,) ( π / 2 ) )
88 84 87 eleqtrdi ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )
89 78 88 eqeltrd ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ - 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )
90 asinsinlem ( ( - 𝐴 ∈ ℂ ∧ ( ℜ ‘ - 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < ( ℜ ‘ ( exp ‘ ( i · - 𝐴 ) ) ) )
91 76 89 90 syl2anc ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < ( ℜ ‘ ( exp ‘ ( i · - 𝐴 ) ) ) )
92 mulneg12 ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · 𝐴 ) = ( i · - 𝐴 ) )
93 5 8 92 sylancr ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( - i · 𝐴 ) = ( i · - 𝐴 ) )
94 93 fveq2d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ ( - i · 𝐴 ) ) = ( exp ‘ ( i · - 𝐴 ) ) )
95 94 fveq2d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( exp ‘ ( - i · 𝐴 ) ) ) = ( ℜ ‘ ( exp ‘ ( i · - 𝐴 ) ) ) )
96 91 95 breqtrrd ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < ( ℜ ‘ ( exp ‘ ( - i · 𝐴 ) ) ) )
97 72 73 74 96 addgt0d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < ( ( ℜ ‘ ( exp ‘ ( i · 𝐴 ) ) ) + ( ℜ ‘ ( exp ‘ ( - i · 𝐴 ) ) ) ) )
98 12 67 readdd ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) = ( ( ℜ ‘ ( exp ‘ ( i · 𝐴 ) ) ) + ( ℜ ‘ ( exp ‘ ( - i · 𝐴 ) ) ) ) )
99 97 98 breqtrrd ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < ( ℜ ‘ ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) )
100 62 69 71 99 mulgt0d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < ( ( 1 / 2 ) · ( ℜ ‘ ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) )
101 cosval ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) )
102 101 adantr ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( cos ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) )
103 2ne0 2 ≠ 0
104 103 a1i ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 2 ≠ 0 )
105 68 23 104 divrec2d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) = ( ( 1 / 2 ) · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) )
106 102 105 eqtrd ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( cos ‘ 𝐴 ) = ( ( 1 / 2 ) · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) )
107 106 fveq2d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( cos ‘ 𝐴 ) ) = ( ℜ ‘ ( ( 1 / 2 ) · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) )
108 remul2 ( ( ( 1 / 2 ) ∈ ℝ ∧ ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ ) → ( ℜ ‘ ( ( 1 / 2 ) · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) = ( ( 1 / 2 ) · ( ℜ ‘ ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) )
109 61 68 108 sylancr ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( ( 1 / 2 ) · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) = ( ( 1 / 2 ) · ( ℜ ‘ ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) )
110 107 109 eqtrd ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( cos ‘ 𝐴 ) ) = ( ( 1 / 2 ) · ( ℜ ‘ ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) )
111 100 110 breqtrrd ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < ( ℜ ‘ ( cos ‘ 𝐴 ) ) )
112 27 7 43 mvrraddd ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( exp ‘ ( i · 𝐴 ) ) − ( i · ( sin ‘ 𝐴 ) ) ) = ( cos ‘ 𝐴 ) )
113 112 fveq2d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( ( exp ‘ ( i · 𝐴 ) ) − ( i · ( sin ‘ 𝐴 ) ) ) ) = ( ℜ ‘ ( cos ‘ 𝐴 ) ) )
114 111 113 breqtrrd ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < ( ℜ ‘ ( ( exp ‘ ( i · 𝐴 ) ) − ( i · ( sin ‘ 𝐴 ) ) ) ) )
115 14 18 60 114 eqsqrt2d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( exp ‘ ( i · 𝐴 ) ) − ( i · ( sin ‘ 𝐴 ) ) ) = ( √ ‘ ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) )
116 115 oveq2d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( i · ( sin ‘ 𝐴 ) ) + ( ( exp ‘ ( i · 𝐴 ) ) − ( i · ( sin ‘ 𝐴 ) ) ) ) = ( ( i · ( sin ‘ 𝐴 ) ) + ( √ ‘ ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) ) )
117 13 116 eqtr3d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ ( i · 𝐴 ) ) = ( ( i · ( sin ‘ 𝐴 ) ) + ( √ ‘ ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) ) )
118 117 fveq2d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( log ‘ ( exp ‘ ( i · 𝐴 ) ) ) = ( log ‘ ( ( i · ( sin ‘ 𝐴 ) ) + ( √ ‘ ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) ) ) )
119 pire π ∈ ℝ
120 119 renegcli - π ∈ ℝ
121 120 a1i ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - π ∈ ℝ )
122 80 a1i ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - ( π / 2 ) ∈ ℝ )
123 elioore ( ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( ℜ ‘ 𝐴 ) ∈ ℝ )
124 123 adantl ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ 𝐴 ) ∈ ℝ )
125 pirp π ∈ ℝ+
126 rphalflt ( π ∈ ℝ+ → ( π / 2 ) < π )
127 125 126 ax-mp ( π / 2 ) < π
128 79 119 ltnegi ( ( π / 2 ) < π ↔ - π < - ( π / 2 ) )
129 127 128 mpbi - π < - ( π / 2 )
130 129 a1i ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - π < - ( π / 2 ) )
131 eliooord ( ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( - ( π / 2 ) < ( ℜ ‘ 𝐴 ) ∧ ( ℜ ‘ 𝐴 ) < ( π / 2 ) ) )
132 131 adantl ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( - ( π / 2 ) < ( ℜ ‘ 𝐴 ) ∧ ( ℜ ‘ 𝐴 ) < ( π / 2 ) ) )
133 132 simpld ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - ( π / 2 ) < ( ℜ ‘ 𝐴 ) )
134 121 122 124 130 133 lttrd ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - π < ( ℜ ‘ 𝐴 ) )
135 imre ( ( i · 𝐴 ) ∈ ℂ → ( ℑ ‘ ( i · 𝐴 ) ) = ( ℜ ‘ ( - i · ( i · 𝐴 ) ) ) )
136 10 135 syl ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℑ ‘ ( i · 𝐴 ) ) = ( ℜ ‘ ( - i · ( i · 𝐴 ) ) ) )
137 5 5 mulneg1i ( - i · i ) = - ( i · i )
138 ixi ( i · i ) = - 1
139 138 negeqi - ( i · i ) = - - 1
140 15 negnegi - - 1 = 1
141 137 139 140 3eqtri ( - i · i ) = 1
142 141 oveq1i ( ( - i · i ) · 𝐴 ) = ( 1 · 𝐴 )
143 63 a1i ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - i ∈ ℂ )
144 5 a1i ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → i ∈ ℂ )
145 143 144 8 mulassd ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( - i · i ) · 𝐴 ) = ( - i · ( i · 𝐴 ) ) )
146 mulid2 ( 𝐴 ∈ ℂ → ( 1 · 𝐴 ) = 𝐴 )
147 146 adantr ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 1 · 𝐴 ) = 𝐴 )
148 142 145 147 3eqtr3a ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( - i · ( i · 𝐴 ) ) = 𝐴 )
149 148 fveq2d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( - i · ( i · 𝐴 ) ) ) = ( ℜ ‘ 𝐴 ) )
150 136 149 eqtrd ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℑ ‘ ( i · 𝐴 ) ) = ( ℜ ‘ 𝐴 ) )
151 134 150 breqtrrd ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - π < ( ℑ ‘ ( i · 𝐴 ) ) )
152 119 a1i ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → π ∈ ℝ )
153 79 a1i ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( π / 2 ) ∈ ℝ )
154 132 simprd ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ 𝐴 ) < ( π / 2 ) )
155 127 a1i ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( π / 2 ) < π )
156 124 153 152 154 155 lttrd ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ 𝐴 ) < π )
157 124 152 156 ltled ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ 𝐴 ) ≤ π )
158 150 157 eqbrtrd ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℑ ‘ ( i · 𝐴 ) ) ≤ π )
159 ellogrn ( ( i · 𝐴 ) ∈ ran log ↔ ( ( i · 𝐴 ) ∈ ℂ ∧ - π < ( ℑ ‘ ( i · 𝐴 ) ) ∧ ( ℑ ‘ ( i · 𝐴 ) ) ≤ π ) )
160 10 151 158 159 syl3anbrc ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( i · 𝐴 ) ∈ ran log )
161 logef ( ( i · 𝐴 ) ∈ ran log → ( log ‘ ( exp ‘ ( i · 𝐴 ) ) ) = ( i · 𝐴 ) )
162 160 161 syl ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( log ‘ ( exp ‘ ( i · 𝐴 ) ) ) = ( i · 𝐴 ) )
163 118 162 eqtr3d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( log ‘ ( ( i · ( sin ‘ 𝐴 ) ) + ( √ ‘ ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) ) ) = ( i · 𝐴 ) )
164 163 oveq2d ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( - i · ( log ‘ ( ( i · ( sin ‘ 𝐴 ) ) + ( √ ‘ ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) ) ) ) = ( - i · ( i · 𝐴 ) ) )
165 4 164 148 3eqtrd ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( arcsin ‘ ( sin ‘ 𝐴 ) ) = 𝐴 )