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 addridi 
 |-  ( _i + 0 ) = _i
6 4 mulridi 
 |-  ( _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 addlidi 
 |-  ( 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 mullidi 
 |-  ( 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 )