Proof of Theorem asinneg
Step | Hyp | Ref
| Expression |
1 | | ax-icn 9995 |
. . . . . . . . . 10
⊢ i ∈
ℂ |
2 | | mulcl 10020 |
. . . . . . . . . 10
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
3 | 1, 2 | mpan 706 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (i
· 𝐴) ∈
ℂ) |
4 | | ax-1cn 9994 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
5 | | sqcl 12925 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (𝐴↑2) ∈
ℂ) |
6 | | subcl 10280 |
. . . . . . . . . . 11
⊢ ((1
∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → (1 −
(𝐴↑2)) ∈
ℂ) |
7 | 4, 5, 6 | sylancr 695 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (1
− (𝐴↑2)) ∈
ℂ) |
8 | 7 | sqrtcld 14176 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(√‘(1 − (𝐴↑2))) ∈ ℂ) |
9 | 3, 8 | addcld 10059 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((i
· 𝐴) +
(√‘(1 − (𝐴↑2)))) ∈ ℂ) |
10 | | asinlem 24595 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((i
· 𝐴) +
(√‘(1 − (𝐴↑2)))) ≠ 0) |
11 | 9, 10 | logcld 24317 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
(log‘((i · 𝐴)
+ (√‘(1 − (𝐴↑2))))) ∈
ℂ) |
12 | | efneg 14828 |
. . . . . . 7
⊢
((log‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))) ∈ ℂ
→ (exp‘-(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) = (1 /
(exp‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))))) |
13 | 11, 12 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(exp‘-(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) = (1 /
(exp‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))))) |
14 | | eflog 24323 |
. . . . . . . 8
⊢ ((((i
· 𝐴) +
(√‘(1 − (𝐴↑2)))) ∈ ℂ ∧ ((i
· 𝐴) +
(√‘(1 − (𝐴↑2)))) ≠ 0) →
(exp‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) = ((i ·
𝐴) + (√‘(1
− (𝐴↑2))))) |
15 | 9, 10, 14 | syl2anc 693 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
(exp‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) = ((i ·
𝐴) + (√‘(1
− (𝐴↑2))))) |
16 | 15 | oveq2d 6666 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (1 /
(exp‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))))) = (1 / ((i
· 𝐴) +
(√‘(1 − (𝐴↑2)))))) |
17 | | asinlem2 24596 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (((i
· 𝐴) +
(√‘(1 − (𝐴↑2)))) · ((i · -𝐴) + (√‘(1 −
(-𝐴↑2))))) =
1) |
18 | 4 | a1i 11 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → 1 ∈
ℂ) |
19 | | negcl 10281 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → -𝐴 ∈
ℂ) |
20 | | mulcl 10020 |
. . . . . . . . . 10
⊢ ((i
∈ ℂ ∧ -𝐴
∈ ℂ) → (i · -𝐴) ∈ ℂ) |
21 | 1, 19, 20 | sylancr 695 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (i
· -𝐴) ∈
ℂ) |
22 | 19 | sqcld 13006 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (-𝐴↑2) ∈
ℂ) |
23 | | subcl 10280 |
. . . . . . . . . . 11
⊢ ((1
∈ ℂ ∧ (-𝐴↑2) ∈ ℂ) → (1 −
(-𝐴↑2)) ∈
ℂ) |
24 | 4, 22, 23 | sylancr 695 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (1
− (-𝐴↑2)) ∈
ℂ) |
25 | 24 | sqrtcld 14176 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(√‘(1 − (-𝐴↑2))) ∈ ℂ) |
26 | 21, 25 | addcld 10059 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((i
· -𝐴) +
(√‘(1 − (-𝐴↑2)))) ∈ ℂ) |
27 | 18, 9, 26, 10 | divmuld 10823 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → ((1 / ((i
· 𝐴) +
(√‘(1 − (𝐴↑2))))) = ((i · -𝐴) + (√‘(1 −
(-𝐴↑2)))) ↔ (((i
· 𝐴) +
(√‘(1 − (𝐴↑2)))) · ((i · -𝐴) + (√‘(1 −
(-𝐴↑2))))) =
1)) |
28 | 17, 27 | mpbird 247 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (1 / ((i
· 𝐴) +
(√‘(1 − (𝐴↑2))))) = ((i · -𝐴) + (√‘(1 −
(-𝐴↑2))))) |
29 | 13, 16, 28 | 3eqtrd 2660 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(exp‘-(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) = ((i ·
-𝐴) + (√‘(1
− (-𝐴↑2))))) |
30 | | asinlem 24595 |
. . . . . . 7
⊢ (-𝐴 ∈ ℂ → ((i
· -𝐴) +
(√‘(1 − (-𝐴↑2)))) ≠ 0) |
31 | 19, 30 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → ((i
· -𝐴) +
(√‘(1 − (-𝐴↑2)))) ≠ 0) |
32 | 11 | negcld 10379 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
-(log‘((i · 𝐴)
+ (√‘(1 − (𝐴↑2))))) ∈
ℂ) |
33 | 11 | imnegd 13950 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(ℑ‘-(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) =
-(ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))))) |
34 | 11 | imcld 13935 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
(ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) ∈
ℝ) |
35 | 34 | renegcld 10457 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
-(ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) ∈
ℝ) |
36 | 9 | renegd 13949 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ →
(ℜ‘-((i · 𝐴) + (√‘(1 − (𝐴↑2))))) =
-(ℜ‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) |
37 | | asinlem3 24598 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ → 0 ≤
(ℜ‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) |
38 | 9 | recld 13934 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ →
(ℜ‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))) ∈
ℝ) |
39 | 38 | le0neg2d 10600 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ → (0 ≤
(ℜ‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))) ↔
-(ℜ‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))) ≤
0)) |
40 | 37, 39 | mpbid 222 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ →
-(ℜ‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))) ≤
0) |
41 | 36, 40 | eqbrtrd 4675 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
(ℜ‘-((i · 𝐴) + (√‘(1 − (𝐴↑2))))) ≤
0) |
42 | 9 | negcld 10379 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ → -((i
· 𝐴) +
(√‘(1 − (𝐴↑2)))) ∈ ℂ) |
43 | 42 | recld 13934 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ →
(ℜ‘-((i · 𝐴) + (√‘(1 − (𝐴↑2))))) ∈
ℝ) |
44 | | 0re 10040 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ |
45 | | lenlt 10116 |
. . . . . . . . . . . . . . . 16
⊢
(((ℜ‘-((i · 𝐴) + (√‘(1 − (𝐴↑2))))) ∈ ℝ
∧ 0 ∈ ℝ) → ((ℜ‘-((i · 𝐴) + (√‘(1 − (𝐴↑2))))) ≤ 0 ↔ ¬
0 < (ℜ‘-((i · 𝐴) + (√‘(1 − (𝐴↑2))))))) |
46 | 43, 44, 45 | sylancl 694 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
((ℜ‘-((i · 𝐴) + (√‘(1 − (𝐴↑2))))) ≤ 0 ↔ ¬
0 < (ℜ‘-((i · 𝐴) + (√‘(1 − (𝐴↑2))))))) |
47 | 41, 46 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ → ¬ 0
< (ℜ‘-((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) |
48 | | lognegb 24336 |
. . . . . . . . . . . . . . . . 17
⊢ ((((i
· 𝐴) +
(√‘(1 − (𝐴↑2)))) ∈ ℂ ∧ ((i
· 𝐴) +
(√‘(1 − (𝐴↑2)))) ≠ 0) → (-((i ·
𝐴) + (√‘(1
− (𝐴↑2))))
∈ ℝ+ ↔ (ℑ‘(log‘((i · 𝐴) + (√‘(1 −
(𝐴↑2)))))) =
π)) |
49 | 9, 10, 48 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → (-((i
· 𝐴) +
(√‘(1 − (𝐴↑2)))) ∈ ℝ+
↔ (ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) =
π)) |
50 | | rpgt0 11844 |
. . . . . . . . . . . . . . . . 17
⊢ (-((i
· 𝐴) +
(√‘(1 − (𝐴↑2)))) ∈ ℝ+
→ 0 < -((i · 𝐴) + (√‘(1 − (𝐴↑2))))) |
51 | | rpre 11839 |
. . . . . . . . . . . . . . . . . 18
⊢ (-((i
· 𝐴) +
(√‘(1 − (𝐴↑2)))) ∈ ℝ+
→ -((i · 𝐴) +
(√‘(1 − (𝐴↑2)))) ∈ ℝ) |
52 | 51 | rered 13964 |
. . . . . . . . . . . . . . . . 17
⊢ (-((i
· 𝐴) +
(√‘(1 − (𝐴↑2)))) ∈ ℝ+
→ (ℜ‘-((i · 𝐴) + (√‘(1 − (𝐴↑2))))) = -((i ·
𝐴) + (√‘(1
− (𝐴↑2))))) |
53 | 50, 52 | breqtrrd 4681 |
. . . . . . . . . . . . . . . 16
⊢ (-((i
· 𝐴) +
(√‘(1 − (𝐴↑2)))) ∈ ℝ+
→ 0 < (ℜ‘-((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) |
54 | 49, 53 | syl6bir 244 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
((ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) = π → 0
< (ℜ‘-((i · 𝐴) + (√‘(1 − (𝐴↑2))))))) |
55 | 54 | necon3bd 2808 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ → (¬ 0
< (ℜ‘-((i · 𝐴) + (√‘(1 − (𝐴↑2))))) →
(ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) ≠
π)) |
56 | 47, 55 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ →
(ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) ≠
π) |
57 | 56 | necomd 2849 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → π ≠
(ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))))) |
58 | | pire 24210 |
. . . . . . . . . . . . . 14
⊢ π
∈ ℝ |
59 | 58 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → π
∈ ℝ) |
60 | 9, 10 | logimcld 24318 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ → (-π
< (ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) ∧
(ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) ≤
π)) |
61 | 60 | simprd 479 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ →
(ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) ≤
π) |
62 | 34, 59, 61 | leltned 10190 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
((ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) < π ↔
π ≠ (ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))))) |
63 | 57, 62 | mpbird 247 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
(ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) <
π) |
64 | | ltneg 10528 |
. . . . . . . . . . . 12
⊢
(((ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) ∈ ℝ
∧ π ∈ ℝ) → ((ℑ‘(log‘((i · 𝐴) + (√‘(1 −
(𝐴↑2)))))) < π
↔ -π < -(ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))))) |
65 | 34, 58, 64 | sylancl 694 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
((ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) < π ↔
-π < -(ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))))) |
66 | 63, 65 | mpbid 222 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → -π
< -(ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))))) |
67 | 60 | simpld 475 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → -π
< (ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))))) |
68 | 58 | renegcli 10342 |
. . . . . . . . . . . . 13
⊢ -π
∈ ℝ |
69 | | ltle 10126 |
. . . . . . . . . . . . 13
⊢ ((-π
∈ ℝ ∧ (ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) ∈ ℝ)
→ (-π < (ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) → -π ≤
(ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))))) |
70 | 68, 34, 69 | sylancr 695 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → (-π
< (ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) → -π ≤
(ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))))) |
71 | 67, 70 | mpd 15 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → -π
≤ (ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))))) |
72 | | lenegcon1 10532 |
. . . . . . . . . . . 12
⊢ ((π
∈ ℝ ∧ (ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) ∈ ℝ)
→ (-π ≤ (ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) ↔
-(ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) ≤
π)) |
73 | 58, 34, 72 | sylancr 695 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (-π
≤ (ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) ↔
-(ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) ≤
π)) |
74 | 71, 73 | mpbid 222 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
-(ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) ≤
π) |
75 | 68 | rexri 10097 |
. . . . . . . . . . 11
⊢ -π
∈ ℝ* |
76 | | elioc2 12236 |
. . . . . . . . . . 11
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ) →
(-(ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) ∈
(-π(,]π) ↔ (-(ℑ‘(log‘((i · 𝐴) + (√‘(1 −
(𝐴↑2)))))) ∈
ℝ ∧ -π < -(ℑ‘(log‘((i · 𝐴) + (√‘(1 −
(𝐴↑2)))))) ∧
-(ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) ≤
π))) |
77 | 75, 58, 76 | mp2an 708 |
. . . . . . . . . 10
⊢
(-(ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) ∈
(-π(,]π) ↔ (-(ℑ‘(log‘((i · 𝐴) + (√‘(1 −
(𝐴↑2)))))) ∈
ℝ ∧ -π < -(ℑ‘(log‘((i · 𝐴) + (√‘(1 −
(𝐴↑2)))))) ∧
-(ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) ≤
π)) |
78 | 35, 66, 74, 77 | syl3anbrc 1246 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
-(ℑ‘(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) ∈
(-π(,]π)) |
79 | 33, 78 | eqeltrd 2701 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(ℑ‘-(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) ∈
(-π(,]π)) |
80 | | imf 13853 |
. . . . . . . . 9
⊢
ℑ:ℂ⟶ℝ |
81 | | ffn 6045 |
. . . . . . . . 9
⊢
(ℑ:ℂ⟶ℝ → ℑ Fn
ℂ) |
82 | | elpreima 6337 |
. . . . . . . . 9
⊢ (ℑ
Fn ℂ → (-(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))) ∈ (◡ℑ “ (-π(,]π)) ↔
(-(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))) ∈ ℂ
∧ (ℑ‘-(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) ∈
(-π(,]π)))) |
83 | 80, 81, 82 | mp2b 10 |
. . . . . . . 8
⊢
(-(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))) ∈ (◡ℑ “ (-π(,]π)) ↔
(-(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))) ∈ ℂ
∧ (ℑ‘-(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) ∈
(-π(,]π))) |
84 | 32, 79, 83 | sylanbrc 698 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
-(log‘((i · 𝐴)
+ (√‘(1 − (𝐴↑2))))) ∈ (◡ℑ “
(-π(,]π))) |
85 | | logrn 24305 |
. . . . . . 7
⊢ ran log =
(◡ℑ “
(-π(,]π)) |
86 | 84, 85 | syl6eleqr 2712 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
-(log‘((i · 𝐴)
+ (√‘(1 − (𝐴↑2))))) ∈ ran
log) |
87 | | logeftb 24330 |
. . . . . 6
⊢ ((((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)))))) |
88 | 26, 31, 86, 87 | syl3anc 1326 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
((log‘((i · -𝐴) + (√‘(1 − (-𝐴↑2))))) = -(log‘((i
· 𝐴) +
(√‘(1 − (𝐴↑2))))) ↔
(exp‘-(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) = ((i ·
-𝐴) + (√‘(1
− (-𝐴↑2)))))) |
89 | 29, 88 | mpbird 247 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(log‘((i · -𝐴)
+ (√‘(1 − (-𝐴↑2))))) = -(log‘((i ·
𝐴) + (√‘(1
− (𝐴↑2)))))) |
90 | 89 | oveq2d 6666 |
. . 3
⊢ (𝐴 ∈ ℂ → (-i
· (log‘((i · -𝐴) + (√‘(1 − (-𝐴↑2)))))) = (-i ·
-(log‘((i · 𝐴)
+ (√‘(1 − (𝐴↑2))))))) |
91 | | negicn 10282 |
. . . 4
⊢ -i ∈
ℂ |
92 | | mulneg2 10467 |
. . . 4
⊢ ((-i
∈ ℂ ∧ (log‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))) ∈ ℂ)
→ (-i · -(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) = -(-i ·
(log‘((i · 𝐴)
+ (√‘(1 − (𝐴↑2))))))) |
93 | 91, 11, 92 | sylancr 695 |
. . 3
⊢ (𝐴 ∈ ℂ → (-i
· -(log‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) = -(-i ·
(log‘((i · 𝐴)
+ (√‘(1 − (𝐴↑2))))))) |
94 | 90, 93 | eqtrd 2656 |
. 2
⊢ (𝐴 ∈ ℂ → (-i
· (log‘((i · -𝐴) + (√‘(1 − (-𝐴↑2)))))) = -(-i ·
(log‘((i · 𝐴)
+ (√‘(1 − (𝐴↑2))))))) |
95 | | asinval 24609 |
. . 3
⊢ (-𝐴 ∈ ℂ →
(arcsin‘-𝐴) = (-i
· (log‘((i · -𝐴) + (√‘(1 − (-𝐴↑2))))))) |
96 | 19, 95 | syl 17 |
. 2
⊢ (𝐴 ∈ ℂ →
(arcsin‘-𝐴) = (-i
· (log‘((i · -𝐴) + (√‘(1 − (-𝐴↑2))))))) |
97 | | asinval 24609 |
. . 3
⊢ (𝐴 ∈ ℂ →
(arcsin‘𝐴) = (-i
· (log‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))))) |
98 | 97 | negeqd 10275 |
. 2
⊢ (𝐴 ∈ ℂ →
-(arcsin‘𝐴) = -(-i
· (log‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))))) |
99 | 94, 96, 98 | 3eqtr4d 2666 |
1
⊢ (𝐴 ∈ ℂ →
(arcsin‘-𝐴) =
-(arcsin‘𝐴)) |