Theorem asin1

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

	Ref	Expression
Assertion	asin1	⊢ ( arcsin ‘ 1 ) = ( π / 2 )

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	⊢ 1 ∈ ℂ
2		asinval	⊢ ( 1 ∈ ℂ → ( arcsin ‘ 1 ) = ( - i · ( log ‘ ( ( i · 1 ) + ( √ ‘ ( 1 − ( 1 ↑ 2 ) ) ) ) ) ) )
3	1 2	ax-mp	⊢ ( arcsin ‘ 1 ) = ( - i · ( log ‘ ( ( i · 1 ) + ( √ ‘ ( 1 − ( 1 ↑ 2 ) ) ) ) ) )
4		ax-icn	⊢ i ∈ ℂ
5	4	addridi	⊢ ( i + 0 ) = i
6	4	mulridi	⊢ ( i · 1 ) = 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	⊢ ( √ ‘ ( 1 − ( 1 ↑ 2 ) ) ) = ( √ ‘ 0 )
12		sqrt0	⊢ ( √ ‘ 0 ) = 0
13	11 12	eqtri	⊢ ( √ ‘ ( 1 − ( 1 ↑ 2 ) ) ) = 0
14	6 13	oveq12i	⊢ ( ( i · 1 ) + ( √ ‘ ( 1 − ( 1 ↑ 2 ) ) ) ) = ( i + 0 )
15		efhalfpi	⊢ ( exp ‘ ( i · ( π / 2 ) ) ) = i
16	5 14 15	3eqtr4i	⊢ ( ( i · 1 ) + ( √ ‘ ( 1 − ( 1 ↑ 2 ) ) ) ) = ( exp ‘ ( i · ( π / 2 ) ) )
17	16	fveq2i	⊢ ( log ‘ ( ( i · 1 ) + ( √ ‘ ( 1 − ( 1 ↑ 2 ) ) ) ) ) = ( log ‘ ( exp ‘ ( i · ( π / 2 ) ) ) )
18		halfpire	⊢ ( π / 2 ) ∈ ℝ
19	18	recni	⊢ ( π / 2 ) ∈ ℂ
20	4 19	mulcli	⊢ ( i · ( π / 2 ) ) ∈ ℂ
21		pipos	⊢ 0 < π
22		pire	⊢ π ∈ ℝ
23		lt0neg2	⊢ ( π ∈ ℝ → ( 0 < π ↔ - π < 0 ) )
24	22 23	ax-mp	⊢ ( 0 < π ↔ - π < 0 )
25	21 24	mpbi	⊢ - π < 0
26		pirp	⊢ π ∈ ℝ+
27		rphalfcl	⊢ ( π ∈ ℝ+ → ( π / 2 ) ∈ ℝ+ )
28	26 27	ax-mp	⊢ ( π / 2 ) ∈ ℝ+
29		rpgt0	⊢ ( ( π / 2 ) ∈ ℝ+ → 0 < ( π / 2 ) )
30	28 29	ax-mp	⊢ 0 < ( π / 2 )
31	22	renegcli	⊢ - π ∈ ℝ
32		0re	⊢ 0 ∈ ℝ
33	31 32 18	lttri	⊢ ( ( - π < 0 ∧ 0 < ( π / 2 ) ) → - π < ( π / 2 ) )
34	25 30 33	mp2an	⊢ - π < ( π / 2 )
35	20	addlidi	⊢ ( 0 + ( i · ( π / 2 ) ) ) = ( i · ( π / 2 ) )
36	35	fveq2i	⊢ ( ℑ ‘ ( 0 + ( i · ( π / 2 ) ) ) ) = ( ℑ ‘ ( i · ( π / 2 ) ) )
37	32 18	crimi	⊢ ( ℑ ‘ ( 0 + ( i · ( π / 2 ) ) ) ) = ( π / 2 )
38	36 37	eqtr3i	⊢ ( ℑ ‘ ( i · ( π / 2 ) ) ) = ( π / 2 )
39	34 38	breqtrri	⊢ - π < ( ℑ ‘ ( i · ( π / 2 ) ) )
40		rphalflt	⊢ ( π ∈ ℝ+ → ( π / 2 ) < π )
41	26 40	ax-mp	⊢ ( π / 2 ) < π
42	18 22 41	ltleii	⊢ ( π / 2 ) ≤ π
43	38 42	eqbrtri	⊢ ( ℑ ‘ ( i · ( π / 2 ) ) ) ≤ π
44		ellogrn	⊢ ( ( i · ( π / 2 ) ) ∈ ran log ↔ ( ( i · ( π / 2 ) ) ∈ ℂ ∧ - π < ( ℑ ‘ ( i · ( π / 2 ) ) ) ∧ ( ℑ ‘ ( i · ( π / 2 ) ) ) ≤ π ) )
45	20 39 43 44	mpbir3an	⊢ ( i · ( π / 2 ) ) ∈ ran log
46		logef	⊢ ( ( i · ( π / 2 ) ) ∈ ran log → ( log ‘ ( exp ‘ ( i · ( π / 2 ) ) ) ) = ( i · ( π / 2 ) ) )
47	45 46	ax-mp	⊢ ( log ‘ ( exp ‘ ( i · ( π / 2 ) ) ) ) = ( i · ( π / 2 ) )
48	17 47	eqtri	⊢ ( log ‘ ( ( i · 1 ) + ( √ ‘ ( 1 − ( 1 ↑ 2 ) ) ) ) ) = ( i · ( π / 2 ) )
49	48	oveq2i	⊢ ( - i · ( log ‘ ( ( i · 1 ) + ( √ ‘ ( 1 − ( 1 ↑ 2 ) ) ) ) ) ) = ( - i · ( i · ( π / 2 ) ) )
50	4 4	mulneg1i	⊢ ( - i · i ) = - ( i · i )
51		ixi	⊢ ( i · i ) = - 1
52	51	negeqi	⊢ - ( i · i ) = - - 1
53		negneg1e1	⊢ - - 1 = 1
54	50 52 53	3eqtri	⊢ ( - i · i ) = 1
55	54	oveq1i	⊢ ( ( - i · i ) · ( π / 2 ) ) = ( 1 · ( π / 2 ) )
56		negicn	⊢ - i ∈ ℂ
57	56 4 19	mulassi	⊢ ( ( - i · i ) · ( π / 2 ) ) = ( - i · ( i · ( π / 2 ) ) )
58	55 57	eqtr3i	⊢ ( 1 · ( π / 2 ) ) = ( - i · ( i · ( π / 2 ) ) )
59	19	mullidi	⊢ ( 1 · ( π / 2 ) ) = ( π / 2 )
60	58 59	eqtr3i	⊢ ( - i · ( i · ( π / 2 ) ) ) = ( π / 2 )
61	3 49 60	3eqtri	⊢ ( arcsin ‘ 1 ) = ( π / 2 )