This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem asinneg

Description: The arcsine function is odd. (Contributed by Mario Carneiro, 1-Apr-2015)

Ref Expression
Assertion asinneg ( 𝐴 ∈ ℂ → ( arcsin ‘ - 𝐴 ) = - ( arcsin ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ax-icn ⊢ i ∈ ℂ
2 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
3 1 2 mpan ⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ∈ ℂ )
4 ax-1cn ⊢ 1 ∈ ℂ
5 sqcl ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) ∈ ℂ )
6 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ) → ( 1 − ( 𝐴 ↑ 2 ) ) ∈ ℂ )
7 4 5 6 sylancr ⊢ ( 𝐴 ∈ ℂ → ( 1 − ( 𝐴 ↑ 2 ) ) ∈ ℂ )
8 7 sqrtcld ⊢ ( 𝐴 ∈ ℂ → ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ∈ ℂ )
9 3 8 addcld ⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ∈ ℂ )
10 asinlem ⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ≠ 0 )
11 9 10 logcld ⊢ ( 𝐴 ∈ ℂ → ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ∈ ℂ )
12 efneg ⊢ ( ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ∈ ℂ → ( exp ‘ - ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) = ( 1 / ( exp ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ) )
13 11 12 syl ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ - ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) = ( 1 / ( exp ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ) )
14 eflog ⊢ ( ( ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ∈ ℂ ∧ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ≠ 0 ) → ( exp ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) = ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) )
15 9 10 14 syl2anc ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) = ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) )
16 15 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( 1 / ( exp ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ) = ( 1 / ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) )
17 asinlem2 ⊢ ( 𝐴 ∈ ℂ → ( ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) · ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) = 1 )
18 4 a1i ⊢ ( 𝐴 ∈ ℂ → 1 ∈ ℂ )
19 negcl ⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
20 mulcl ⊢ ( ( i ∈ ℂ ∧ - 𝐴 ∈ ℂ ) → ( i · - 𝐴 ) ∈ ℂ )
21 1 19 20 sylancr ⊢ ( 𝐴 ∈ ℂ → ( i · - 𝐴 ) ∈ ℂ )
22 19 sqcld ⊢ ( 𝐴 ∈ ℂ → ( - 𝐴 ↑ 2 ) ∈ ℂ )
23 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( - 𝐴 ↑ 2 ) ∈ ℂ ) → ( 1 − ( - 𝐴 ↑ 2 ) ) ∈ ℂ )
24 4 22 23 sylancr ⊢ ( 𝐴 ∈ ℂ → ( 1 − ( - 𝐴 ↑ 2 ) ) ∈ ℂ )
25 24 sqrtcld ⊢ ( 𝐴 ∈ ℂ → ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ∈ ℂ )
26 21 25 addcld ⊢ ( 𝐴 ∈ ℂ → ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ∈ ℂ )
27 18 9 26 10 divmuld ⊢ ( 𝐴 ∈ ℂ → ( ( 1 / ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) = ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ↔ ( ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) · ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) = 1 ) )
28 17 27 mpbird ⊢ ( 𝐴 ∈ ℂ → ( 1 / ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) = ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) )
29 13 16 28 3eqtrd ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ - ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) = ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) )
30 asinlem ⊢ ( - 𝐴 ∈ ℂ → ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ≠ 0 )
31 19 30 syl ⊢ ( 𝐴 ∈ ℂ → ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ≠ 0 )
32 11 negcld ⊢ ( 𝐴 ∈ ℂ → - ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ∈ ℂ )
33 11 imnegd ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ - ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) = - ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) )
34 11 imcld ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ∈ ℝ )
35 34 renegcld ⊢ ( 𝐴 ∈ ℂ → - ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ∈ ℝ )
36 pire ⊢ π ∈ ℝ
37 36 a1i ⊢ ( 𝐴 ∈ ℂ → π ∈ ℝ )
38 9 10 logimcld ⊢ ( 𝐴 ∈ ℂ → ( - π < ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ∧ ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ≤ π ) )
39 38 simprd ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ≤ π )
40 9 renegd ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ - ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) = - ( ℜ ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) )
41 asinlem3 ⊢ ( 𝐴 ∈ ℂ → 0 ≤ ( ℜ ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) )
42 9 recld ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ∈ ℝ )
43 42 le0neg2d ⊢ ( 𝐴 ∈ ℂ → ( 0 ≤ ( ℜ ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ↔ - ( ℜ ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ≤ 0 ) )
44 41 43 mpbid ⊢ ( 𝐴 ∈ ℂ → - ( ℜ ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ≤ 0 )
45 40 44 eqbrtrd ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ - ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ≤ 0 )
46 9 negcld ⊢ ( 𝐴 ∈ ℂ → - ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ∈ ℂ )
47 46 recld ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ - ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ∈ ℝ )
48 0re ⊢ 0 ∈ ℝ
49 lenlt ⊢ ( ( ( ℜ ‘ - ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ℜ ‘ - ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ≤ 0 ↔ ¬ 0 < ( ℜ ‘ - ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) )
50 47 48 49 sylancl ⊢ ( 𝐴 ∈ ℂ → ( ( ℜ ‘ - ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ≤ 0 ↔ ¬ 0 < ( ℜ ‘ - ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) )
51 45 50 mpbid ⊢ ( 𝐴 ∈ ℂ → ¬ 0 < ( ℜ ‘ - ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) )
52 lognegb ⊢ ( ( ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ∈ ℂ ∧ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ≠ 0 ) → ( - ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) = π ) )
53 9 10 52 syl2anc ⊢ ( 𝐴 ∈ ℂ → ( - ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) = π ) )
54 rpgt0 ⊢ ( - ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ∈ ℝ+ → 0 < - ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) )
55 rpre ⊢ ( - ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ∈ ℝ+ → - ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ∈ ℝ )
56 55 rered ⊢ ( - ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ∈ ℝ+ → ( ℜ ‘ - ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) = - ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) )
57 54 56 breqtrrd ⊢ ( - ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ∈ ℝ+ → 0 < ( ℜ ‘ - ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) )
58 53 57 biimtrrdi ⊢ ( 𝐴 ∈ ℂ → ( ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) = π → 0 < ( ℜ ‘ - ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) )
59 58 necon3bd ⊢ ( 𝐴 ∈ ℂ → ( ¬ 0 < ( ℜ ‘ - ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) → ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ≠ π ) )
60 51 59 mpd ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ≠ π )
61 60 necomd ⊢ ( 𝐴 ∈ ℂ → π ≠ ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) )
62 34 37 39 61 leneltd ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) < π )
63 ltneg ⊢ ( ( ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ∈ ℝ ∧ π ∈ ℝ ) → ( ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) < π ↔ - π < - ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ) )
64 34 36 63 sylancl ⊢ ( 𝐴 ∈ ℂ → ( ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) < π ↔ - π < - ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ) )
65 62 64 mpbid ⊢ ( 𝐴 ∈ ℂ → - π < - ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) )
66 38 simpld ⊢ ( 𝐴 ∈ ℂ → - π < ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) )
67 36 renegcli ⊢ - π ∈ ℝ
68 ltle ⊢ ( ( - π ∈ ℝ ∧ ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ∈ ℝ ) → ( - π < ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) → - π ≤ ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ) )
69 67 34 68 sylancr ⊢ ( 𝐴 ∈ ℂ → ( - π < ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) → - π ≤ ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ) )
70 66 69 mpd ⊢ ( 𝐴 ∈ ℂ → - π ≤ ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) )
71 lenegcon1 ⊢ ( ( π ∈ ℝ ∧ ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ∈ ℝ ) → ( - π ≤ ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ↔ - ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ≤ π ) )
72 36 34 71 sylancr ⊢ ( 𝐴 ∈ ℂ → ( - π ≤ ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ↔ - ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ≤ π ) )
73 70 72 mpbid ⊢ ( 𝐴 ∈ ℂ → - ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ≤ π )
74 67 rexri ⊢ - π ∈ ℝ*
75 elioc2 ⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ ) → ( - ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ∈ ( - π (,] π ) ↔ ( - ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ∈ ℝ ∧ - π < - ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ∧ - ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ≤ π ) ) )
76 74 36 75 mp2an ⊢ ( - ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ∈ ( - π (,] π ) ↔ ( - ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ∈ ℝ ∧ - π < - ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ∧ - ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ≤ π ) )
77 35 65 73 76 syl3anbrc ⊢ ( 𝐴 ∈ ℂ → - ( ℑ ‘ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ∈ ( - π (,] π ) )
78 33 77 eqeltrd ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ - ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ∈ ( - π (,] π ) )
79 imf ⊢ ℑ : ℂ ⟶ ℝ
80 ffn ⊢ ( ℑ : ℂ ⟶ ℝ → ℑ Fn ℂ )
81 elpreima ⊢ ( ℑ Fn ℂ → ( - ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ∈ ( ◡ ℑ “ ( - π (,] π ) ) ↔ ( - ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ∈ ℂ ∧ ( ℑ ‘ - ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ∈ ( - π (,] π ) ) ) )
82 79 80 81 mp2b ⊢ ( - ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ∈ ( ◡ ℑ “ ( - π (,] π ) ) ↔ ( - ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ∈ ℂ ∧ ( ℑ ‘ - ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) ∈ ( - π (,] π ) ) )
83 32 78 82 sylanbrc ⊢ ( 𝐴 ∈ ℂ → - ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ∈ ( ◡ ℑ “ ( - π (,] π ) ) )
84 logrn ⊢ ran log = ( ◡ ℑ “ ( - π (,] π ) )
85 83 84 eleqtrrdi ⊢ ( 𝐴 ∈ ℂ → - ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ∈ ran log )
86 logeftb ⊢ ( ( ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ∈ ℂ ∧ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ≠ 0 ∧ - ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ∈ ran log ) → ( ( log ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) = - ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ↔ ( exp ‘ - ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) = ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) )
87 26 31 85 86 syl3anc ⊢ ( 𝐴 ∈ ℂ → ( ( log ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) = - ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ↔ ( exp ‘ - ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) = ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) )
88 29 87 mpbird ⊢ ( 𝐴 ∈ ℂ → ( log ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) = - ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) )
89 88 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( - i · ( log ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ) = ( - i · - ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) )
90 negicn ⊢ - i ∈ ℂ
91 mulneg2 ⊢ ( ( - i ∈ ℂ ∧ ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ∈ ℂ ) → ( - i · - ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) = - ( - i · ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) )
92 90 11 91 sylancr ⊢ ( 𝐴 ∈ ℂ → ( - i · - ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) = - ( - i · ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) )
93 89 92 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( - i · ( log ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ) = - ( - i · ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) )
94 asinval ⊢ ( - 𝐴 ∈ ℂ → ( arcsin ‘ - 𝐴 ) = ( - i · ( log ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ) )
95 19 94 syl ⊢ ( 𝐴 ∈ ℂ → ( arcsin ‘ - 𝐴 ) = ( - i · ( log ‘ ( ( i · - 𝐴 ) + ( √ ‘ ( 1 − ( - 𝐴 ↑ 2 ) ) ) ) ) ) )
96 asinval ⊢ ( 𝐴 ∈ ℂ → ( arcsin ‘ 𝐴 ) = ( - i · ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) )
97 96 negeqd ⊢ ( 𝐴 ∈ ℂ → - ( arcsin ‘ 𝐴 ) = - ( - i · ( log ‘ ( ( i · 𝐴 ) + ( √ ‘ ( 1 − ( 𝐴 ↑ 2 ) ) ) ) ) ) )
98 93 95 97 3eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( arcsin ‘ - 𝐴 ) = - ( arcsin ‘ 𝐴 ) )