This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 )