Metamath Proof Explorer


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 addid1i ( i + 0 ) = i
6 4 mulid1i ( 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 addid2i ( 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 mulid2i ( 1 · ( π / 2 ) ) = ( π / 2 )
60 58 59 eqtr3i ( - i · ( i · ( π / 2 ) ) ) = ( π / 2 )
61 3 49 60 3eqtri ( arcsin ‘ 1 ) = ( π / 2 )