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 ) = ( _pi / 2 )

Proof

Step Hyp Ref Expression
1 ax-1cn
 |-  1 e. CC
2 asinval
 |-  ( 1 e. CC -> ( arcsin ` 1 ) = ( -u _i x. ( log ` ( ( _i x. 1 ) + ( sqrt ` ( 1 - ( 1 ^ 2 ) ) ) ) ) ) )
3 1 2 ax-mp
 |-  ( arcsin ` 1 ) = ( -u _i x. ( log ` ( ( _i x. 1 ) + ( sqrt ` ( 1 - ( 1 ^ 2 ) ) ) ) ) )
4 ax-icn
 |-  _i e. CC
5 4 addid1i
 |-  ( _i + 0 ) = _i
6 4 mulid1i
 |-  ( _i x. 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
 |-  ( sqrt ` ( 1 - ( 1 ^ 2 ) ) ) = ( sqrt ` 0 )
12 sqrt0
 |-  ( sqrt ` 0 ) = 0
13 11 12 eqtri
 |-  ( sqrt ` ( 1 - ( 1 ^ 2 ) ) ) = 0
14 6 13 oveq12i
 |-  ( ( _i x. 1 ) + ( sqrt ` ( 1 - ( 1 ^ 2 ) ) ) ) = ( _i + 0 )
15 efhalfpi
 |-  ( exp ` ( _i x. ( _pi / 2 ) ) ) = _i
16 5 14 15 3eqtr4i
 |-  ( ( _i x. 1 ) + ( sqrt ` ( 1 - ( 1 ^ 2 ) ) ) ) = ( exp ` ( _i x. ( _pi / 2 ) ) )
17 16 fveq2i
 |-  ( log ` ( ( _i x. 1 ) + ( sqrt ` ( 1 - ( 1 ^ 2 ) ) ) ) ) = ( log ` ( exp ` ( _i x. ( _pi / 2 ) ) ) )
18 halfpire
 |-  ( _pi / 2 ) e. RR
19 18 recni
 |-  ( _pi / 2 ) e. CC
20 4 19 mulcli
 |-  ( _i x. ( _pi / 2 ) ) e. CC
21 pipos
 |-  0 < _pi
22 pire
 |-  _pi e. RR
23 lt0neg2
 |-  ( _pi e. RR -> ( 0 < _pi <-> -u _pi < 0 ) )
24 22 23 ax-mp
 |-  ( 0 < _pi <-> -u _pi < 0 )
25 21 24 mpbi
 |-  -u _pi < 0
26 pirp
 |-  _pi e. RR+
27 rphalfcl
 |-  ( _pi e. RR+ -> ( _pi / 2 ) e. RR+ )
28 26 27 ax-mp
 |-  ( _pi / 2 ) e. RR+
29 rpgt0
 |-  ( ( _pi / 2 ) e. RR+ -> 0 < ( _pi / 2 ) )
30 28 29 ax-mp
 |-  0 < ( _pi / 2 )
31 22 renegcli
 |-  -u _pi e. RR
32 0re
 |-  0 e. RR
33 31 32 18 lttri
 |-  ( ( -u _pi < 0 /\ 0 < ( _pi / 2 ) ) -> -u _pi < ( _pi / 2 ) )
34 25 30 33 mp2an
 |-  -u _pi < ( _pi / 2 )
35 20 addid2i
 |-  ( 0 + ( _i x. ( _pi / 2 ) ) ) = ( _i x. ( _pi / 2 ) )
36 35 fveq2i
 |-  ( Im ` ( 0 + ( _i x. ( _pi / 2 ) ) ) ) = ( Im ` ( _i x. ( _pi / 2 ) ) )
37 32 18 crimi
 |-  ( Im ` ( 0 + ( _i x. ( _pi / 2 ) ) ) ) = ( _pi / 2 )
38 36 37 eqtr3i
 |-  ( Im ` ( _i x. ( _pi / 2 ) ) ) = ( _pi / 2 )
39 34 38 breqtrri
 |-  -u _pi < ( Im ` ( _i x. ( _pi / 2 ) ) )
40 rphalflt
 |-  ( _pi e. RR+ -> ( _pi / 2 ) < _pi )
41 26 40 ax-mp
 |-  ( _pi / 2 ) < _pi
42 18 22 41 ltleii
 |-  ( _pi / 2 ) <_ _pi
43 38 42 eqbrtri
 |-  ( Im ` ( _i x. ( _pi / 2 ) ) ) <_ _pi
44 ellogrn
 |-  ( ( _i x. ( _pi / 2 ) ) e. ran log <-> ( ( _i x. ( _pi / 2 ) ) e. CC /\ -u _pi < ( Im ` ( _i x. ( _pi / 2 ) ) ) /\ ( Im ` ( _i x. ( _pi / 2 ) ) ) <_ _pi ) )
45 20 39 43 44 mpbir3an
 |-  ( _i x. ( _pi / 2 ) ) e. ran log
46 logef
 |-  ( ( _i x. ( _pi / 2 ) ) e. ran log -> ( log ` ( exp ` ( _i x. ( _pi / 2 ) ) ) ) = ( _i x. ( _pi / 2 ) ) )
47 45 46 ax-mp
 |-  ( log ` ( exp ` ( _i x. ( _pi / 2 ) ) ) ) = ( _i x. ( _pi / 2 ) )
48 17 47 eqtri
 |-  ( log ` ( ( _i x. 1 ) + ( sqrt ` ( 1 - ( 1 ^ 2 ) ) ) ) ) = ( _i x. ( _pi / 2 ) )
49 48 oveq2i
 |-  ( -u _i x. ( log ` ( ( _i x. 1 ) + ( sqrt ` ( 1 - ( 1 ^ 2 ) ) ) ) ) ) = ( -u _i x. ( _i x. ( _pi / 2 ) ) )
50 4 4 mulneg1i
 |-  ( -u _i x. _i ) = -u ( _i x. _i )
51 ixi
 |-  ( _i x. _i ) = -u 1
52 51 negeqi
 |-  -u ( _i x. _i ) = -u -u 1
53 negneg1e1
 |-  -u -u 1 = 1
54 50 52 53 3eqtri
 |-  ( -u _i x. _i ) = 1
55 54 oveq1i
 |-  ( ( -u _i x. _i ) x. ( _pi / 2 ) ) = ( 1 x. ( _pi / 2 ) )
56 negicn
 |-  -u _i e. CC
57 56 4 19 mulassi
 |-  ( ( -u _i x. _i ) x. ( _pi / 2 ) ) = ( -u _i x. ( _i x. ( _pi / 2 ) ) )
58 55 57 eqtr3i
 |-  ( 1 x. ( _pi / 2 ) ) = ( -u _i x. ( _i x. ( _pi / 2 ) ) )
59 19 mulid2i
 |-  ( 1 x. ( _pi / 2 ) ) = ( _pi / 2 )
60 58 59 eqtr3i
 |-  ( -u _i x. ( _i x. ( _pi / 2 ) ) ) = ( _pi / 2 )
61 3 49 60 3eqtri
 |-  ( arcsin ` 1 ) = ( _pi / 2 )