Theorem reasinsin

Description: The arcsine function composed with sin is equal to the identity. (Contributed by Mario Carneiro, 2-Apr-2015)

	Ref	Expression
Assertion	reasinsin	$$⊢A\in \left[-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right]\to arcsin\left(\sin A\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		neghalfpire	$$⊢-\frac{\mathrm{\pi }}{2}\in ℝ$$
2	1	rexri	$$⊢-\frac{\mathrm{\pi }}{2}\in {ℝ}^{*}$$
3		halfpire	$$⊢\frac{\mathrm{\pi }}{2}\in ℝ$$
4	3	rexri	$$⊢\frac{\mathrm{\pi }}{2}\in {ℝ}^{*}$$
5		pirp	$$⊢\mathrm{\pi }\in {ℝ}^{+}$$
6		rphalfcl	$$⊢\mathrm{\pi }\in {ℝ}^{+}\to \frac{\mathrm{\pi }}{2}\in {ℝ}^{+}$$
7	5 6	ax-mp	$$⊢\frac{\mathrm{\pi }}{2}\in {ℝ}^{+}$$
8		rpgt0	$$⊢\frac{\mathrm{\pi }}{2}\in {ℝ}^{+}\to 0<\frac{\mathrm{\pi }}{2}$$
9	7 8	ax-mp	$$⊢0<\frac{\mathrm{\pi }}{2}$$
10		lt0neg2	$$⊢\frac{\mathrm{\pi }}{2}\in ℝ\to \left(0<\frac{\mathrm{\pi }}{2}\leftrightarrow -\frac{\mathrm{\pi }}{2}<0\right)$$
11	3 10	ax-mp	$$⊢0<\frac{\mathrm{\pi }}{2}\leftrightarrow -\frac{\mathrm{\pi }}{2}<0$$
12	9 11	mpbi	$$⊢-\frac{\mathrm{\pi }}{2}<0$$
13		0re	$$⊢0\in ℝ$$
14	1 13 3	lttri	$$⊢\left(-\frac{\mathrm{\pi }}{2}<0\wedge 0<\frac{\mathrm{\pi }}{2}\right)\to -\frac{\mathrm{\pi }}{2}<\frac{\mathrm{\pi }}{2}$$
15	12 9 14	mp2an	$$⊢-\frac{\mathrm{\pi }}{2}<\frac{\mathrm{\pi }}{2}$$
16	1 3 15	ltleii	$$⊢-\frac{\mathrm{\pi }}{2}\le \frac{\mathrm{\pi }}{2}$$
17		prunioo	$$⊢\left(-\frac{\mathrm{\pi }}{2}\in {ℝ}^{*}\wedge \frac{\mathrm{\pi }}{2}\in {ℝ}^{*}\wedge -\frac{\mathrm{\pi }}{2}\le \frac{\mathrm{\pi }}{2}\right)\to \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\cup \left\{-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right\}=\left[-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right]$$
18	2 4 16 17	mp3an	$$⊢\left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\cup \left\{-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right\}=\left[-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right]$$
19	18	eleq2i	$$⊢A\in \left(\left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\cup \left\{-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right\}\right)\leftrightarrow A\in \left[-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right]$$
20		elun	$$⊢A\in \left(\left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\cup \left\{-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right\}\right)\leftrightarrow \left(A\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\vee A\in \left\{-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right\}\right)$$
21	19 20	bitr3i	$$⊢A\in \left[-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right]\leftrightarrow \left(A\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\vee A\in \left\{-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right\}\right)$$
22		elioore	$$⊢A\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\to A\in ℝ$$
23	22	recnd	$$⊢A\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\to A\in ℂ$$
24	22	rered	$$⊢A\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\to \Re \left(A\right)=A$$
25		id	$$⊢A\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\to A\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)$$
26	24 25	eqeltrd	$$⊢A\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\to \Re \left(A\right)\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)$$
27		asinsin	$$⊢\left(A\in ℂ\wedge \Re \left(A\right)\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\right)\to arcsin\left(\sin A\right)=A$$
28	23 26 27	syl2anc	$$⊢A\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\to arcsin\left(\sin A\right)=A$$
29		elpri	$$⊢A\in \left\{-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right\}\to \left(A=-\frac{\mathrm{\pi }}{2}\vee A=\frac{\mathrm{\pi }}{2}\right)$$
30		ax-1cn	$$⊢1\in ℂ$$
31		asinneg	$$⊢1\in ℂ\to arcsin\left(-1\right)=-arcsin\left(1\right)$$
32	30 31	ax-mp	$$⊢arcsin\left(-1\right)=-arcsin\left(1\right)$$
33		asin1	$$⊢arcsin\left(1\right)=\frac{\mathrm{\pi }}{2}$$
34	33	negeqi	$$⊢-arcsin\left(1\right)=-\frac{\mathrm{\pi }}{2}$$
35	32 34	eqtri	$$⊢arcsin\left(-1\right)=-\frac{\mathrm{\pi }}{2}$$
36		fveq2	$$⊢A=-\frac{\mathrm{\pi }}{2}\to \sin A=\sin \left(-\frac{\mathrm{\pi }}{2}\right)$$
37	3	recni	$$⊢\frac{\mathrm{\pi }}{2}\in ℂ$$
38		sinneg	$$⊢\frac{\mathrm{\pi }}{2}\in ℂ\to \sin \left(-\frac{\mathrm{\pi }}{2}\right)=-\sin \left(\frac{\mathrm{\pi }}{2}\right)$$
39	37 38	ax-mp	$$⊢\sin \left(-\frac{\mathrm{\pi }}{2}\right)=-\sin \left(\frac{\mathrm{\pi }}{2}\right)$$
40		sinhalfpi	$$⊢\sin \left(\frac{\mathrm{\pi }}{2}\right)=1$$
41	40	negeqi	$$⊢-\sin \left(\frac{\mathrm{\pi }}{2}\right)=-1$$
42	39 41	eqtri	$$⊢\sin \left(-\frac{\mathrm{\pi }}{2}\right)=-1$$
43	36 42	eqtrdi	$$⊢A=-\frac{\mathrm{\pi }}{2}\to \sin A=-1$$
44	43	fveq2d	$$⊢A=-\frac{\mathrm{\pi }}{2}\to arcsin\left(\sin A\right)=arcsin\left(-1\right)$$
45		id	$$⊢A=-\frac{\mathrm{\pi }}{2}\to A=-\frac{\mathrm{\pi }}{2}$$
46	35 44 45	3eqtr4a	$$⊢A=-\frac{\mathrm{\pi }}{2}\to arcsin\left(\sin A\right)=A$$
47		fveq2	$$⊢A=\frac{\mathrm{\pi }}{2}\to \sin A=\sin \left(\frac{\mathrm{\pi }}{2}\right)$$
48	47 40	eqtrdi	$$⊢A=\frac{\mathrm{\pi }}{2}\to \sin A=1$$
49	48	fveq2d	$$⊢A=\frac{\mathrm{\pi }}{2}\to arcsin\left(\sin A\right)=arcsin\left(1\right)$$
50		id	$$⊢A=\frac{\mathrm{\pi }}{2}\to A=\frac{\mathrm{\pi }}{2}$$
51	33 49 50	3eqtr4a	$$⊢A=\frac{\mathrm{\pi }}{2}\to arcsin\left(\sin A\right)=A$$
52	46 51	jaoi	$$⊢\left(A=-\frac{\mathrm{\pi }}{2}\vee A=\frac{\mathrm{\pi }}{2}\right)\to arcsin\left(\sin A\right)=A$$
53	29 52	syl	$$⊢A\in \left\{-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right\}\to arcsin\left(\sin A\right)=A$$
54	28 53	jaoi	$$⊢\left(A\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\vee A\in \left\{-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right\}\right)\to arcsin\left(\sin A\right)=A$$
55	21 54	sylbi	$$⊢A\in \left[-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right]\to arcsin\left(\sin A\right)=A$$