Theorem asin1

Description: The arcsine of 1 is _pi / 2 . (Contributed by Mario Carneiro, 2-Apr-2015)

	Ref	Expression
Assertion	asin1	$$⊢arcsin\left(1\right)=\frac{\mathrm{\pi }}{2}$$

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	$$⊢1\in ℂ$$
2		asinval	$$⊢1\in ℂ\to arcsin\left(1\right)=\left(-\mathrm{i}\right)\log \left(\mathrm{i}\cdot 1+\sqrt{1-1^2}\right)$$
3	1 2	ax-mp	$$⊢arcsin\left(1\right)=\left(-\mathrm{i}\right)\log \left(\mathrm{i}\cdot 1+\sqrt{1-1^2}\right)$$
4		ax-icn	$$⊢\mathrm{i}\in ℂ$$
5	4	addid1i	$$⊢\mathrm{i}+0=\mathrm{i}$$
6	4	mulid1i	$$⊢\mathrm{i}\cdot 1=\mathrm{i}$$
7		sq1	$$⊢1^2=1$$
8	7	oveq2i	$$⊢1-1^2=1-1$$
9		1m1e0	$$⊢1-1=0$$
10	8 9	eqtri	$$⊢1-1^2=0$$
11	10	fveq2i	$$⊢\sqrt{1-1^2}=\sqrt{0}$$
12		sqrt0	$$⊢\sqrt{0}=0$$
13	11 12	eqtri	$$⊢\sqrt{1-1^2}=0$$
14	6 13	oveq12i	$$⊢\mathrm{i}\cdot 1+\sqrt{1-1^2}=\mathrm{i}+0$$
15		efhalfpi	$$⊢{\mathrm{e}}^{\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)}=\mathrm{i}$$
16	5 14 15	3eqtr4i	$$⊢\mathrm{i}\cdot 1+\sqrt{1-1^2}={\mathrm{e}}^{\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)}$$
17	16	fveq2i	$$⊢\log \left(\mathrm{i}\cdot 1+\sqrt{1-1^2}\right)=\log {\mathrm{e}}^{\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)}$$
18		halfpire	$$⊢\frac{\mathrm{\pi }}{2}\in ℝ$$
19	18	recni	$$⊢\frac{\mathrm{\pi }}{2}\in ℂ$$
20	4 19	mulcli	$$⊢\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\in ℂ$$
21		pipos	$$⊢0<\mathrm{\pi }$$
22		pire	$$⊢\mathrm{\pi }\in ℝ$$
23		lt0neg2	$$⊢\mathrm{\pi }\in ℝ\to \left(0<\mathrm{\pi }\leftrightarrow -\mathrm{\pi }<0\right)$$
24	22 23	ax-mp	$$⊢0<\mathrm{\pi }\leftrightarrow -\mathrm{\pi }<0$$
25	21 24	mpbi	$$⊢-\mathrm{\pi }<0$$
26		pirp	$$⊢\mathrm{\pi }\in {ℝ}^{+}$$
27		rphalfcl	$$⊢\mathrm{\pi }\in {ℝ}^{+}\to \frac{\mathrm{\pi }}{2}\in {ℝ}^{+}$$
28	26 27	ax-mp	$$⊢\frac{\mathrm{\pi }}{2}\in {ℝ}^{+}$$
29		rpgt0	$$⊢\frac{\mathrm{\pi }}{2}\in {ℝ}^{+}\to 0<\frac{\mathrm{\pi }}{2}$$
30	28 29	ax-mp	$$⊢0<\frac{\mathrm{\pi }}{2}$$
31	22	renegcli	$$⊢-\mathrm{\pi }\in ℝ$$
32		0re	$$⊢0\in ℝ$$
33	31 32 18	lttri	$$⊢\left(-\mathrm{\pi }<0\wedge 0<\frac{\mathrm{\pi }}{2}\right)\to -\mathrm{\pi }<\frac{\mathrm{\pi }}{2}$$
34	25 30 33	mp2an	$$⊢-\mathrm{\pi }<\frac{\mathrm{\pi }}{2}$$
35	20	addid2i	$$⊢0+\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)=\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)$$
36	35	fveq2i	$$⊢\Im \left(0+\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\right)=\Im \left(\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\right)$$
37	32 18	crimi	$$⊢\Im \left(0+\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\right)=\frac{\mathrm{\pi }}{2}$$
38	36 37	eqtr3i	$$⊢\Im \left(\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\right)=\frac{\mathrm{\pi }}{2}$$
39	34 38	breqtrri	$$⊢-\mathrm{\pi }<\Im \left(\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\right)$$
40		rphalflt	$$⊢\mathrm{\pi }\in {ℝ}^{+}\to \frac{\mathrm{\pi }}{2}<\mathrm{\pi }$$
41	26 40	ax-mp	$$⊢\frac{\mathrm{\pi }}{2}<\mathrm{\pi }$$
42	18 22 41	ltleii	$$⊢\frac{\mathrm{\pi }}{2}\le \mathrm{\pi }$$
43	38 42	eqbrtri	$$⊢\Im \left(\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\right)\le \mathrm{\pi }$$
44		ellogrn	$$⊢\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\in \mathrm{ran}log\leftrightarrow \left(\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\in ℂ\wedge -\mathrm{\pi }<\Im \left(\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\right)\wedge \Im \left(\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\right)\le \mathrm{\pi }\right)$$
45	20 39 43 44	mpbir3an	$$⊢\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\in \mathrm{ran}log$$
46		logef	$$⊢\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)\in \mathrm{ran}log\to \log {\mathrm{e}}^{\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)}=\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)$$
47	45 46	ax-mp	$$⊢\log {\mathrm{e}}^{\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)}=\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)$$
48	17 47	eqtri	$$⊢\log \left(\mathrm{i}\cdot 1+\sqrt{1-1^2}\right)=\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)$$
49	48	oveq2i	$$⊢\left(-\mathrm{i}\right)\log \left(\mathrm{i}\cdot 1+\sqrt{1-1^2}\right)=\left(-\mathrm{i}\right)\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)$$
50	4 4	mulneg1i	$$⊢\left(-\mathrm{i}\right)\mathrm{i}=-\mathrm{i}\mathrm{i}$$
51		ixi	$$⊢\mathrm{i}\mathrm{i}=-1$$
52	51	negeqi	$$⊢-\mathrm{i}\mathrm{i}=--1$$
53		negneg1e1	$$⊢--1=1$$
54	50 52 53	3eqtri	$$⊢\left(-\mathrm{i}\right)\mathrm{i}=1$$
55	54	oveq1i	$$⊢\left(-\mathrm{i}\right)\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)=1\left(\frac{\mathrm{\pi }}{2}\right)$$
56		negicn	$$⊢-\mathrm{i}\in ℂ$$
57	56 4 19	mulassi	$$⊢\left(-\mathrm{i}\right)\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)=\left(-\mathrm{i}\right)\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)$$
58	55 57	eqtr3i	$$⊢1\left(\frac{\mathrm{\pi }}{2}\right)=\left(-\mathrm{i}\right)\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)$$
59	19	mulid2i	$$⊢1\left(\frac{\mathrm{\pi }}{2}\right)=\frac{\mathrm{\pi }}{2}$$
60	58 59	eqtr3i	$$⊢\left(-\mathrm{i}\right)\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)=\frac{\mathrm{\pi }}{2}$$
61	3 49 60	3eqtri	$$⊢arcsin\left(1\right)=\frac{\mathrm{\pi }}{2}$$