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	$⊢ (A \in ℂ \land ℜ (A) \in (- \frac{π}{2}, \frac{π}{2})) \to arcsin (\sin A) = A$

Proof

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

Metamath Proof Explorer

Theorem asinsin

Proof