Step |
Hyp |
Ref |
Expression |
1 |
|
sincl |
⊢ ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) ∈ ℂ ) |
2 |
1
|
adantr |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( sin ‘ 𝐴 ) ∈ ℂ ) |
3 |
|
asinval |
⊢ ( ( sin ‘ 𝐴 ) ∈ ℂ → ( arcsin ‘ ( sin ‘ 𝐴 ) ) = ( - i · ( log ‘ ( ( i · ( sin ‘ 𝐴 ) ) + ( √ ‘ ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) ) ) ) ) |
4 |
2 3
|
syl |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( arcsin ‘ ( sin ‘ 𝐴 ) ) = ( - i · ( log ‘ ( ( i · ( sin ‘ 𝐴 ) ) + ( √ ‘ ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) ) ) ) ) |
5 |
|
ax-icn |
⊢ i ∈ ℂ |
6 |
|
mulcl |
⊢ ( ( i ∈ ℂ ∧ ( sin ‘ 𝐴 ) ∈ ℂ ) → ( i · ( sin ‘ 𝐴 ) ) ∈ ℂ ) |
7 |
5 2 6
|
sylancr |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( i · ( sin ‘ 𝐴 ) ) ∈ ℂ ) |
8 |
|
simpl |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 𝐴 ∈ ℂ ) |
9 |
|
mulcl |
⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ ) |
10 |
5 8 9
|
sylancr |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( i · 𝐴 ) ∈ ℂ ) |
11 |
|
efcl |
⊢ ( ( i · 𝐴 ) ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ ) |
12 |
10 11
|
syl |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ ) |
13 |
7 12
|
pncan3d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( i · ( sin ‘ 𝐴 ) ) + ( ( exp ‘ ( i · 𝐴 ) ) − ( i · ( sin ‘ 𝐴 ) ) ) ) = ( exp ‘ ( i · 𝐴 ) ) ) |
14 |
12 7
|
subcld |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( exp ‘ ( i · 𝐴 ) ) − ( i · ( sin ‘ 𝐴 ) ) ) ∈ ℂ ) |
15 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
16 |
2
|
sqcld |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( sin ‘ 𝐴 ) ↑ 2 ) ∈ ℂ ) |
17 |
|
subcl |
⊢ ( ( 1 ∈ ℂ ∧ ( ( sin ‘ 𝐴 ) ↑ 2 ) ∈ ℂ ) → ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ∈ ℂ ) |
18 |
15 16 17
|
sylancr |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ∈ ℂ ) |
19 |
|
binom2sub |
⊢ ( ( ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ ∧ ( i · ( sin ‘ 𝐴 ) ) ∈ ℂ ) → ( ( ( exp ‘ ( i · 𝐴 ) ) − ( i · ( sin ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( ( ( exp ‘ ( i · 𝐴 ) ) ↑ 2 ) − ( 2 · ( ( exp ‘ ( i · 𝐴 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) + ( ( i · ( sin ‘ 𝐴 ) ) ↑ 2 ) ) ) |
20 |
12 7 19
|
syl2anc |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( exp ‘ ( i · 𝐴 ) ) − ( i · ( sin ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( ( ( exp ‘ ( i · 𝐴 ) ) ↑ 2 ) − ( 2 · ( ( exp ‘ ( i · 𝐴 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) + ( ( i · ( sin ‘ 𝐴 ) ) ↑ 2 ) ) ) |
21 |
12
|
sqvald |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( exp ‘ ( i · 𝐴 ) ) ↑ 2 ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) ) |
22 |
|
2cn |
⊢ 2 ∈ ℂ |
23 |
22
|
a1i |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 2 ∈ ℂ ) |
24 |
23 12 7
|
mul12d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 2 · ( ( exp ‘ ( i · 𝐴 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( 2 · ( i · ( sin ‘ 𝐴 ) ) ) ) ) |
25 |
21 24
|
oveq12d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( exp ‘ ( i · 𝐴 ) ) ↑ 2 ) − ( 2 · ( ( exp ‘ ( i · 𝐴 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) = ( ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) − ( ( exp ‘ ( i · 𝐴 ) ) · ( 2 · ( i · ( sin ‘ 𝐴 ) ) ) ) ) ) |
26 |
|
coscl |
⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ ) |
27 |
26
|
adantr |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( cos ‘ 𝐴 ) ∈ ℂ ) |
28 |
|
subsq |
⊢ ( ( ( cos ‘ 𝐴 ) ∈ ℂ ∧ ( i · ( sin ‘ 𝐴 ) ) ∈ ℂ ) → ( ( ( cos ‘ 𝐴 ) ↑ 2 ) − ( ( i · ( sin ‘ 𝐴 ) ) ↑ 2 ) ) = ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) · ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) ) ) |
29 |
27 7 28
|
syl2anc |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( cos ‘ 𝐴 ) ↑ 2 ) − ( ( i · ( sin ‘ 𝐴 ) ) ↑ 2 ) ) = ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) · ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) ) ) |
30 |
|
sqmul |
⊢ ( ( i ∈ ℂ ∧ ( sin ‘ 𝐴 ) ∈ ℂ ) → ( ( i · ( sin ‘ 𝐴 ) ) ↑ 2 ) = ( ( i ↑ 2 ) · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) |
31 |
5 2 30
|
sylancr |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( i · ( sin ‘ 𝐴 ) ) ↑ 2 ) = ( ( i ↑ 2 ) · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) |
32 |
|
i2 |
⊢ ( i ↑ 2 ) = - 1 |
33 |
32
|
oveq1i |
⊢ ( ( i ↑ 2 ) · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) = ( - 1 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) |
34 |
16
|
mulm1d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( - 1 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) = - ( ( sin ‘ 𝐴 ) ↑ 2 ) ) |
35 |
33 34
|
syl5eq |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( i ↑ 2 ) · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) = - ( ( sin ‘ 𝐴 ) ↑ 2 ) ) |
36 |
31 35
|
eqtrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( i · ( sin ‘ 𝐴 ) ) ↑ 2 ) = - ( ( sin ‘ 𝐴 ) ↑ 2 ) ) |
37 |
36
|
oveq2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( cos ‘ 𝐴 ) ↑ 2 ) − ( ( i · ( sin ‘ 𝐴 ) ) ↑ 2 ) ) = ( ( ( cos ‘ 𝐴 ) ↑ 2 ) − - ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) |
38 |
27
|
sqcld |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( cos ‘ 𝐴 ) ↑ 2 ) ∈ ℂ ) |
39 |
38 16
|
subnegd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( cos ‘ 𝐴 ) ↑ 2 ) − - ( ( sin ‘ 𝐴 ) ↑ 2 ) ) = ( ( ( cos ‘ 𝐴 ) ↑ 2 ) + ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) |
40 |
38 16
|
addcomd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( cos ‘ 𝐴 ) ↑ 2 ) + ( ( sin ‘ 𝐴 ) ↑ 2 ) ) = ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ) |
41 |
37 39 40
|
3eqtrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( cos ‘ 𝐴 ) ↑ 2 ) − ( ( i · ( sin ‘ 𝐴 ) ) ↑ 2 ) ) = ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ) |
42 |
|
efival |
⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) = ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) ) |
43 |
42
|
adantr |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ ( i · 𝐴 ) ) = ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) ) |
44 |
7
|
2timesd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 2 · ( i · ( sin ‘ 𝐴 ) ) ) = ( ( i · ( sin ‘ 𝐴 ) ) + ( i · ( sin ‘ 𝐴 ) ) ) ) |
45 |
43 44
|
oveq12d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( exp ‘ ( i · 𝐴 ) ) − ( 2 · ( i · ( sin ‘ 𝐴 ) ) ) ) = ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) − ( ( i · ( sin ‘ 𝐴 ) ) + ( i · ( sin ‘ 𝐴 ) ) ) ) ) |
46 |
27 7 7
|
pnpcan2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) − ( ( i · ( sin ‘ 𝐴 ) ) + ( i · ( sin ‘ 𝐴 ) ) ) ) = ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) ) |
47 |
45 46
|
eqtrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( exp ‘ ( i · 𝐴 ) ) − ( 2 · ( i · ( sin ‘ 𝐴 ) ) ) ) = ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) ) |
48 |
43 47
|
oveq12d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( exp ‘ ( i · 𝐴 ) ) · ( ( exp ‘ ( i · 𝐴 ) ) − ( 2 · ( i · ( sin ‘ 𝐴 ) ) ) ) ) = ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) · ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) ) ) |
49 |
|
mulcl |
⊢ ( ( 2 ∈ ℂ ∧ ( i · ( sin ‘ 𝐴 ) ) ∈ ℂ ) → ( 2 · ( i · ( sin ‘ 𝐴 ) ) ) ∈ ℂ ) |
50 |
22 7 49
|
sylancr |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 2 · ( i · ( sin ‘ 𝐴 ) ) ) ∈ ℂ ) |
51 |
12 12 50
|
subdid |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( exp ‘ ( i · 𝐴 ) ) · ( ( exp ‘ ( i · 𝐴 ) ) − ( 2 · ( i · ( sin ‘ 𝐴 ) ) ) ) ) = ( ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) − ( ( exp ‘ ( i · 𝐴 ) ) · ( 2 · ( i · ( sin ‘ 𝐴 ) ) ) ) ) ) |
52 |
48 51
|
eqtr3d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) · ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) ) = ( ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) − ( ( exp ‘ ( i · 𝐴 ) ) · ( 2 · ( i · ( sin ‘ 𝐴 ) ) ) ) ) ) |
53 |
29 41 52
|
3eqtr3d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = ( ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) − ( ( exp ‘ ( i · 𝐴 ) ) · ( 2 · ( i · ( sin ‘ 𝐴 ) ) ) ) ) ) |
54 |
|
sincossq |
⊢ ( 𝐴 ∈ ℂ → ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = 1 ) |
55 |
54
|
adantr |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = 1 ) |
56 |
25 53 55
|
3eqtr2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( exp ‘ ( i · 𝐴 ) ) ↑ 2 ) − ( 2 · ( ( exp ‘ ( i · 𝐴 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) = 1 ) |
57 |
56 36
|
oveq12d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( ( exp ‘ ( i · 𝐴 ) ) ↑ 2 ) − ( 2 · ( ( exp ‘ ( i · 𝐴 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) + ( ( i · ( sin ‘ 𝐴 ) ) ↑ 2 ) ) = ( 1 + - ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) |
58 |
|
negsub |
⊢ ( ( 1 ∈ ℂ ∧ ( ( sin ‘ 𝐴 ) ↑ 2 ) ∈ ℂ ) → ( 1 + - ( ( sin ‘ 𝐴 ) ↑ 2 ) ) = ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) |
59 |
15 16 58
|
sylancr |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 1 + - ( ( sin ‘ 𝐴 ) ↑ 2 ) ) = ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) |
60 |
20 57 59
|
3eqtrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( exp ‘ ( i · 𝐴 ) ) − ( i · ( sin ‘ 𝐴 ) ) ) ↑ 2 ) = ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) |
61 |
|
halfre |
⊢ ( 1 / 2 ) ∈ ℝ |
62 |
61
|
a1i |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 1 / 2 ) ∈ ℝ ) |
63 |
|
negicn |
⊢ - i ∈ ℂ |
64 |
|
mulcl |
⊢ ( ( - i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · 𝐴 ) ∈ ℂ ) |
65 |
63 8 64
|
sylancr |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( - i · 𝐴 ) ∈ ℂ ) |
66 |
|
efcl |
⊢ ( ( - i · 𝐴 ) ∈ ℂ → ( exp ‘ ( - i · 𝐴 ) ) ∈ ℂ ) |
67 |
65 66
|
syl |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ ( - i · 𝐴 ) ) ∈ ℂ ) |
68 |
12 67
|
addcld |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ ) |
69 |
68
|
recld |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ∈ ℝ ) |
70 |
|
halfgt0 |
⊢ 0 < ( 1 / 2 ) |
71 |
70
|
a1i |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < ( 1 / 2 ) ) |
72 |
12
|
recld |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( exp ‘ ( i · 𝐴 ) ) ) ∈ ℝ ) |
73 |
67
|
recld |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℝ ) |
74 |
|
asinsinlem |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < ( ℜ ‘ ( exp ‘ ( i · 𝐴 ) ) ) ) |
75 |
|
negcl |
⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ ) |
76 |
75
|
adantr |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - 𝐴 ∈ ℂ ) |
77 |
|
reneg |
⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ - 𝐴 ) = - ( ℜ ‘ 𝐴 ) ) |
78 |
77
|
adantr |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ - 𝐴 ) = - ( ℜ ‘ 𝐴 ) ) |
79 |
|
halfpire |
⊢ ( π / 2 ) ∈ ℝ |
80 |
79
|
renegcli |
⊢ - ( π / 2 ) ∈ ℝ |
81 |
|
recl |
⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℝ ) |
82 |
|
iooneg |
⊢ ( ( - ( π / 2 ) ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ∧ ( ℜ ‘ 𝐴 ) ∈ ℝ ) → ( ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ↔ - ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) - - ( π / 2 ) ) ) ) |
83 |
80 79 81 82
|
mp3an12i |
⊢ ( 𝐴 ∈ ℂ → ( ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ↔ - ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) - - ( π / 2 ) ) ) ) |
84 |
83
|
biimpa |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) - - ( π / 2 ) ) ) |
85 |
79
|
recni |
⊢ ( π / 2 ) ∈ ℂ |
86 |
85
|
negnegi |
⊢ - - ( π / 2 ) = ( π / 2 ) |
87 |
86
|
oveq2i |
⊢ ( - ( π / 2 ) (,) - - ( π / 2 ) ) = ( - ( π / 2 ) (,) ( π / 2 ) ) |
88 |
84 87
|
eleqtrdi |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) |
89 |
78 88
|
eqeltrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ - 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) |
90 |
|
asinsinlem |
⊢ ( ( - 𝐴 ∈ ℂ ∧ ( ℜ ‘ - 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < ( ℜ ‘ ( exp ‘ ( i · - 𝐴 ) ) ) ) |
91 |
76 89 90
|
syl2anc |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < ( ℜ ‘ ( exp ‘ ( i · - 𝐴 ) ) ) ) |
92 |
|
mulneg12 |
⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · 𝐴 ) = ( i · - 𝐴 ) ) |
93 |
5 8 92
|
sylancr |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( - i · 𝐴 ) = ( i · - 𝐴 ) ) |
94 |
93
|
fveq2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ ( - i · 𝐴 ) ) = ( exp ‘ ( i · - 𝐴 ) ) ) |
95 |
94
|
fveq2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( exp ‘ ( - i · 𝐴 ) ) ) = ( ℜ ‘ ( exp ‘ ( i · - 𝐴 ) ) ) ) |
96 |
91 95
|
breqtrrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < ( ℜ ‘ ( exp ‘ ( - i · 𝐴 ) ) ) ) |
97 |
72 73 74 96
|
addgt0d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < ( ( ℜ ‘ ( exp ‘ ( i · 𝐴 ) ) ) + ( ℜ ‘ ( exp ‘ ( - i · 𝐴 ) ) ) ) ) |
98 |
12 67
|
readdd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) = ( ( ℜ ‘ ( exp ‘ ( i · 𝐴 ) ) ) + ( ℜ ‘ ( exp ‘ ( - i · 𝐴 ) ) ) ) ) |
99 |
97 98
|
breqtrrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < ( ℜ ‘ ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) |
100 |
62 69 71 99
|
mulgt0d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < ( ( 1 / 2 ) · ( ℜ ‘ ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) ) |
101 |
|
cosval |
⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) ) |
102 |
101
|
adantr |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( cos ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) ) |
103 |
|
2ne0 |
⊢ 2 ≠ 0 |
104 |
103
|
a1i |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 2 ≠ 0 ) |
105 |
68 23 104
|
divrec2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) = ( ( 1 / 2 ) · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) |
106 |
102 105
|
eqtrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( cos ‘ 𝐴 ) = ( ( 1 / 2 ) · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) |
107 |
106
|
fveq2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( cos ‘ 𝐴 ) ) = ( ℜ ‘ ( ( 1 / 2 ) · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) ) |
108 |
|
remul2 |
⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ ) → ( ℜ ‘ ( ( 1 / 2 ) · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) = ( ( 1 / 2 ) · ( ℜ ‘ ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) ) |
109 |
61 68 108
|
sylancr |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( ( 1 / 2 ) · ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) = ( ( 1 / 2 ) · ( ℜ ‘ ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) ) |
110 |
107 109
|
eqtrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( cos ‘ 𝐴 ) ) = ( ( 1 / 2 ) · ( ℜ ‘ ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) ) ) ) |
111 |
100 110
|
breqtrrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < ( ℜ ‘ ( cos ‘ 𝐴 ) ) ) |
112 |
27 7 43
|
mvrraddd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( exp ‘ ( i · 𝐴 ) ) − ( i · ( sin ‘ 𝐴 ) ) ) = ( cos ‘ 𝐴 ) ) |
113 |
112
|
fveq2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( ( exp ‘ ( i · 𝐴 ) ) − ( i · ( sin ‘ 𝐴 ) ) ) ) = ( ℜ ‘ ( cos ‘ 𝐴 ) ) ) |
114 |
111 113
|
breqtrrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < ( ℜ ‘ ( ( exp ‘ ( i · 𝐴 ) ) − ( i · ( sin ‘ 𝐴 ) ) ) ) ) |
115 |
14 18 60 114
|
eqsqrt2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( exp ‘ ( i · 𝐴 ) ) − ( i · ( sin ‘ 𝐴 ) ) ) = ( √ ‘ ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) ) |
116 |
115
|
oveq2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( i · ( sin ‘ 𝐴 ) ) + ( ( exp ‘ ( i · 𝐴 ) ) − ( i · ( sin ‘ 𝐴 ) ) ) ) = ( ( i · ( sin ‘ 𝐴 ) ) + ( √ ‘ ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) ) ) |
117 |
13 116
|
eqtr3d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ ( i · 𝐴 ) ) = ( ( i · ( sin ‘ 𝐴 ) ) + ( √ ‘ ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) ) ) |
118 |
117
|
fveq2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( log ‘ ( exp ‘ ( i · 𝐴 ) ) ) = ( log ‘ ( ( i · ( sin ‘ 𝐴 ) ) + ( √ ‘ ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) ) ) ) |
119 |
|
pire |
⊢ π ∈ ℝ |
120 |
119
|
renegcli |
⊢ - π ∈ ℝ |
121 |
120
|
a1i |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - π ∈ ℝ ) |
122 |
80
|
a1i |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - ( π / 2 ) ∈ ℝ ) |
123 |
|
elioore |
⊢ ( ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( ℜ ‘ 𝐴 ) ∈ ℝ ) |
124 |
123
|
adantl |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ 𝐴 ) ∈ ℝ ) |
125 |
|
pirp |
⊢ π ∈ ℝ+ |
126 |
|
rphalflt |
⊢ ( π ∈ ℝ+ → ( π / 2 ) < π ) |
127 |
125 126
|
ax-mp |
⊢ ( π / 2 ) < π |
128 |
79 119
|
ltnegi |
⊢ ( ( π / 2 ) < π ↔ - π < - ( π / 2 ) ) |
129 |
127 128
|
mpbi |
⊢ - π < - ( π / 2 ) |
130 |
129
|
a1i |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - π < - ( π / 2 ) ) |
131 |
|
eliooord |
⊢ ( ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( - ( π / 2 ) < ( ℜ ‘ 𝐴 ) ∧ ( ℜ ‘ 𝐴 ) < ( π / 2 ) ) ) |
132 |
131
|
adantl |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( - ( π / 2 ) < ( ℜ ‘ 𝐴 ) ∧ ( ℜ ‘ 𝐴 ) < ( π / 2 ) ) ) |
133 |
132
|
simpld |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - ( π / 2 ) < ( ℜ ‘ 𝐴 ) ) |
134 |
121 122 124 130 133
|
lttrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - π < ( ℜ ‘ 𝐴 ) ) |
135 |
|
imre |
⊢ ( ( i · 𝐴 ) ∈ ℂ → ( ℑ ‘ ( i · 𝐴 ) ) = ( ℜ ‘ ( - i · ( i · 𝐴 ) ) ) ) |
136 |
10 135
|
syl |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℑ ‘ ( i · 𝐴 ) ) = ( ℜ ‘ ( - i · ( i · 𝐴 ) ) ) ) |
137 |
5 5
|
mulneg1i |
⊢ ( - i · i ) = - ( i · i ) |
138 |
|
ixi |
⊢ ( i · i ) = - 1 |
139 |
138
|
negeqi |
⊢ - ( i · i ) = - - 1 |
140 |
15
|
negnegi |
⊢ - - 1 = 1 |
141 |
137 139 140
|
3eqtri |
⊢ ( - i · i ) = 1 |
142 |
141
|
oveq1i |
⊢ ( ( - i · i ) · 𝐴 ) = ( 1 · 𝐴 ) |
143 |
63
|
a1i |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - i ∈ ℂ ) |
144 |
5
|
a1i |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → i ∈ ℂ ) |
145 |
143 144 8
|
mulassd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( - i · i ) · 𝐴 ) = ( - i · ( i · 𝐴 ) ) ) |
146 |
|
mulid2 |
⊢ ( 𝐴 ∈ ℂ → ( 1 · 𝐴 ) = 𝐴 ) |
147 |
146
|
adantr |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 1 · 𝐴 ) = 𝐴 ) |
148 |
142 145 147
|
3eqtr3a |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( - i · ( i · 𝐴 ) ) = 𝐴 ) |
149 |
148
|
fveq2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( - i · ( i · 𝐴 ) ) ) = ( ℜ ‘ 𝐴 ) ) |
150 |
136 149
|
eqtrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℑ ‘ ( i · 𝐴 ) ) = ( ℜ ‘ 𝐴 ) ) |
151 |
134 150
|
breqtrrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - π < ( ℑ ‘ ( i · 𝐴 ) ) ) |
152 |
119
|
a1i |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → π ∈ ℝ ) |
153 |
79
|
a1i |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( π / 2 ) ∈ ℝ ) |
154 |
132
|
simprd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ 𝐴 ) < ( π / 2 ) ) |
155 |
127
|
a1i |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( π / 2 ) < π ) |
156 |
124 153 152 154 155
|
lttrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ 𝐴 ) < π ) |
157 |
124 152 156
|
ltled |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ 𝐴 ) ≤ π ) |
158 |
150 157
|
eqbrtrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℑ ‘ ( i · 𝐴 ) ) ≤ π ) |
159 |
|
ellogrn |
⊢ ( ( i · 𝐴 ) ∈ ran log ↔ ( ( i · 𝐴 ) ∈ ℂ ∧ - π < ( ℑ ‘ ( i · 𝐴 ) ) ∧ ( ℑ ‘ ( i · 𝐴 ) ) ≤ π ) ) |
160 |
10 151 158 159
|
syl3anbrc |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( i · 𝐴 ) ∈ ran log ) |
161 |
|
logef |
⊢ ( ( i · 𝐴 ) ∈ ran log → ( log ‘ ( exp ‘ ( i · 𝐴 ) ) ) = ( i · 𝐴 ) ) |
162 |
160 161
|
syl |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( log ‘ ( exp ‘ ( i · 𝐴 ) ) ) = ( i · 𝐴 ) ) |
163 |
118 162
|
eqtr3d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( log ‘ ( ( i · ( sin ‘ 𝐴 ) ) + ( √ ‘ ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) ) ) = ( i · 𝐴 ) ) |
164 |
163
|
oveq2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( - i · ( log ‘ ( ( i · ( sin ‘ 𝐴 ) ) + ( √ ‘ ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) ) ) ) = ( - i · ( i · 𝐴 ) ) ) |
165 |
4 164 148
|
3eqtrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( arcsin ‘ ( sin ‘ 𝐴 ) ) = 𝐴 ) |