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 eqtrid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 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 ‘ 𝐴 ) ) = 𝐴 )