Theorem asinsin

Description: The arcsine function composed with sin is equal to the identity. This plus sinasin allow 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		mullid	⊢ ( 𝐴 ∈ ℂ → ( 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 ‘ 𝐴 ) ) = 𝐴 )