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