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