Proof of Theorem asinsin
Step | Hyp | Ref
| Expression |
1 | | sincl 15564 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(sin‘𝐴) ∈
ℂ) |
2 | 1 | adantr 484 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (sin‘𝐴) ∈ ℂ) |
3 | | asinval 25612 |
. . 3
⊢
((sin‘𝐴)
∈ ℂ → (arcsin‘(sin‘𝐴)) = (-i · (log‘((i ·
(sin‘𝐴)) +
(√‘(1 − ((sin‘𝐴)↑2))))))) |
4 | 2, 3 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (arcsin‘(sin‘𝐴)) = (-i · (log‘((i ·
(sin‘𝐴)) +
(√‘(1 − ((sin‘𝐴)↑2))))))) |
5 | | ax-icn 10667 |
. . . . . . . 8
⊢ i ∈
ℂ |
6 | | mulcl 10692 |
. . . . . . . 8
⊢ ((i
∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i ·
(sin‘𝐴)) ∈
ℂ) |
7 | 5, 2, 6 | sylancr 590 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · (sin‘𝐴)) ∈ ℂ) |
8 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 𝐴 ∈ ℂ) |
9 | | mulcl 10692 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
10 | 5, 8, 9 | sylancr 590 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · 𝐴) ∈ ℂ) |
11 | | efcl 15521 |
. . . . . . . 8
⊢ ((i
· 𝐴) ∈ ℂ
→ (exp‘(i · 𝐴)) ∈ ℂ) |
12 | 10, 11 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(i · 𝐴)) ∈ ℂ) |
13 | 7, 12 | pncan3d 11071 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i · (sin‘𝐴)) + ((exp‘(i · 𝐴)) − (i ·
(sin‘𝐴)))) =
(exp‘(i · 𝐴))) |
14 | 12, 7 | subcld 11068 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) − (i · (sin‘𝐴))) ∈
ℂ) |
15 | | ax-1cn 10666 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
16 | 2 | sqcld 13593 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((sin‘𝐴)↑2) ∈ ℂ) |
17 | | subcl 10956 |
. . . . . . . . 9
⊢ ((1
∈ ℂ ∧ ((sin‘𝐴)↑2) ∈ ℂ) → (1 −
((sin‘𝐴)↑2))
∈ ℂ) |
18 | 15, 16, 17 | sylancr 590 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (1 − ((sin‘𝐴)↑2)) ∈ ℂ) |
19 | | binom2sub 13666 |
. . . . . . . . . 10
⊢
(((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 587 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) − (i · (sin‘𝐴)))↑2) = ((((exp‘(i
· 𝐴))↑2)
− (2 · ((exp‘(i · 𝐴)) · (i · (sin‘𝐴))))) + ((i ·
(sin‘𝐴))↑2))) |
21 | 12 | sqvald 13592 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴))↑2) = ((exp‘(i · 𝐴)) · (exp‘(i
· 𝐴)))) |
22 | | 2cn 11784 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ |
23 | 22 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 2 ∈ ℂ) |
24 | 23, 12, 7 | mul12d 10920 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (2 · ((exp‘(i · 𝐴)) · (i ·
(sin‘𝐴)))) =
((exp‘(i · 𝐴))
· (2 · (i · (sin‘𝐴))))) |
25 | 21, 24 | oveq12d 7182 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴))↑2) − (2 ·
((exp‘(i · 𝐴))
· (i · (sin‘𝐴))))) = (((exp‘(i · 𝐴)) · (exp‘(i
· 𝐴))) −
((exp‘(i · 𝐴))
· (2 · (i · (sin‘𝐴)))))) |
26 | | coscl 15565 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(cos‘𝐴) ∈
ℂ) |
27 | 26 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘𝐴) ∈ ℂ) |
28 | | subsq 13657 |
. . . . . . . . . . . . 13
⊢
(((cos‘𝐴)
∈ ℂ ∧ (i · (sin‘𝐴)) ∈ ℂ) → (((cos‘𝐴)↑2) − ((i ·
(sin‘𝐴))↑2)) =
(((cos‘𝐴) + (i
· (sin‘𝐴)))
· ((cos‘𝐴)
− (i · (sin‘𝐴))))) |
29 | 27, 7, 28 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴)↑2) − ((i ·
(sin‘𝐴))↑2)) =
(((cos‘𝐴) + (i
· (sin‘𝐴)))
· ((cos‘𝐴)
− (i · (sin‘𝐴))))) |
30 | | sqmul 13570 |
. . . . . . . . . . . . . . . 16
⊢ ((i
∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → ((i ·
(sin‘𝐴))↑2) =
((i↑2) · ((sin‘𝐴)↑2))) |
31 | 5, 2, 30 | sylancr 590 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i · (sin‘𝐴))↑2) = ((i↑2) ·
((sin‘𝐴)↑2))) |
32 | | i2 13650 |
. . . . . . . . . . . . . . . . 17
⊢
(i↑2) = -1 |
33 | 32 | oveq1i 7174 |
. . . . . . . . . . . . . . . 16
⊢
((i↑2) · ((sin‘𝐴)↑2)) = (-1 · ((sin‘𝐴)↑2)) |
34 | 16 | mulm1d 11163 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (-1 · ((sin‘𝐴)↑2)) = -((sin‘𝐴)↑2)) |
35 | 33, 34 | syl5eq 2785 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i↑2) · ((sin‘𝐴)↑2)) = -((sin‘𝐴)↑2)) |
36 | 31, 35 | eqtrd 2773 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i · (sin‘𝐴))↑2) = -((sin‘𝐴)↑2)) |
37 | 36 | oveq2d 7180 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴)↑2) − ((i ·
(sin‘𝐴))↑2)) =
(((cos‘𝐴)↑2)
− -((sin‘𝐴)↑2))) |
38 | 27 | sqcld 13593 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((cos‘𝐴)↑2) ∈ ℂ) |
39 | 38, 16 | subnegd 11075 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴)↑2) − -((sin‘𝐴)↑2)) = (((cos‘𝐴)↑2) + ((sin‘𝐴)↑2))) |
40 | 38, 16 | addcomd 10913 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴)↑2) + ((sin‘𝐴)↑2)) = (((sin‘𝐴)↑2) + ((cos‘𝐴)↑2))) |
41 | 37, 39, 40 | 3eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴)↑2) − ((i ·
(sin‘𝐴))↑2)) =
(((sin‘𝐴)↑2) +
((cos‘𝐴)↑2))) |
42 | | efival 15590 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
(exp‘(i · 𝐴))
= ((cos‘𝐴) + (i
· (sin‘𝐴)))) |
43 | 42 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(i · 𝐴)) = ((cos‘𝐴) + (i · (sin‘𝐴)))) |
44 | 7 | 2timesd 11952 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (2 · (i · (sin‘𝐴))) = ((i ·
(sin‘𝐴)) + (i
· (sin‘𝐴)))) |
45 | 43, 44 | oveq12d 7182 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) − (2 · (i ·
(sin‘𝐴)))) =
(((cos‘𝐴) + (i
· (sin‘𝐴)))
− ((i · (sin‘𝐴)) + (i · (sin‘𝐴))))) |
46 | 27, 7, 7 | pnpcan2d 11106 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) − ((i · (sin‘𝐴)) + (i ·
(sin‘𝐴)))) =
((cos‘𝐴) − (i
· (sin‘𝐴)))) |
47 | 45, 46 | eqtrd 2773 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) − (2 · (i ·
(sin‘𝐴)))) =
((cos‘𝐴) − (i
· (sin‘𝐴)))) |
48 | 43, 47 | oveq12d 7182 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) · ((exp‘(i · 𝐴)) − (2 · (i
· (sin‘𝐴)))))
= (((cos‘𝐴) + (i
· (sin‘𝐴)))
· ((cos‘𝐴)
− (i · (sin‘𝐴))))) |
49 | | mulcl 10692 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℂ ∧ (i · (sin‘𝐴)) ∈ ℂ) → (2 · (i
· (sin‘𝐴)))
∈ ℂ) |
50 | 22, 7, 49 | sylancr 590 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (2 · (i · (sin‘𝐴))) ∈
ℂ) |
51 | 12, 12, 50 | subdid 11167 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) · ((exp‘(i · 𝐴)) − (2 · (i
· (sin‘𝐴)))))
= (((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) − ((exp‘(i
· 𝐴)) · (2
· (i · (sin‘𝐴)))))) |
52 | 48, 51 | eqtr3d 2775 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) · ((cos‘𝐴) − (i · (sin‘𝐴)))) = (((exp‘(i ·
𝐴)) · (exp‘(i
· 𝐴))) −
((exp‘(i · 𝐴))
· (2 · (i · (sin‘𝐴)))))) |
53 | 29, 41, 52 | 3eqtr3d 2781 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((sin‘𝐴)↑2) + ((cos‘𝐴)↑2)) = (((exp‘(i · 𝐴)) · (exp‘(i
· 𝐴))) −
((exp‘(i · 𝐴))
· (2 · (i · (sin‘𝐴)))))) |
54 | | sincossq 15614 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
(((sin‘𝐴)↑2) +
((cos‘𝐴)↑2)) =
1) |
55 | 54 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((sin‘𝐴)↑2) + ((cos‘𝐴)↑2)) = 1) |
56 | 25, 53, 55 | 3eqtr2d 2779 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴))↑2) − (2 ·
((exp‘(i · 𝐴))
· (i · (sin‘𝐴))))) = 1) |
57 | 56, 36 | oveq12d 7182 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((((exp‘(i · 𝐴))↑2) − (2 ·
((exp‘(i · 𝐴))
· (i · (sin‘𝐴))))) + ((i · (sin‘𝐴))↑2)) = (1 +
-((sin‘𝐴)↑2))) |
58 | | negsub 11005 |
. . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ ((sin‘𝐴)↑2) ∈ ℂ) → (1 +
-((sin‘𝐴)↑2)) =
(1 − ((sin‘𝐴)↑2))) |
59 | 15, 16, 58 | sylancr 590 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (1 + -((sin‘𝐴)↑2)) = (1 − ((sin‘𝐴)↑2))) |
60 | 20, 57, 59 | 3eqtrd 2777 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) − (i · (sin‘𝐴)))↑2) = (1 −
((sin‘𝐴)↑2))) |
61 | | halfre 11923 |
. . . . . . . . . . . 12
⊢ (1 / 2)
∈ ℝ |
62 | 61 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (1 / 2) ∈ ℝ) |
63 | | negicn 10958 |
. . . . . . . . . . . . . . 15
⊢ -i ∈
ℂ |
64 | | mulcl 10692 |
. . . . . . . . . . . . . . 15
⊢ ((-i
∈ ℂ ∧ 𝐴
∈ ℂ) → (-i · 𝐴) ∈ ℂ) |
65 | 63, 8, 64 | sylancr 590 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (-i · 𝐴) ∈ ℂ) |
66 | | efcl 15521 |
. . . . . . . . . . . . . 14
⊢ ((-i
· 𝐴) ∈ ℂ
→ (exp‘(-i · 𝐴)) ∈ ℂ) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(-i · 𝐴)) ∈ ℂ) |
68 | 12, 67 | addcld 10731 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) ∈
ℂ) |
69 | 68 | recld 14636 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘((exp‘(i · 𝐴)) + (exp‘(-i ·
𝐴)))) ∈
ℝ) |
70 | | halfgt0 11925 |
. . . . . . . . . . . 12
⊢ 0 < (1
/ 2) |
71 | 70 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < (1 / 2)) |
72 | 12 | recld 14636 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(exp‘(i · 𝐴))) ∈
ℝ) |
73 | 67 | recld 14636 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(exp‘(-i · 𝐴))) ∈
ℝ) |
74 | | asinsinlem 25621 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < (ℜ‘(exp‘(i ·
𝐴)))) |
75 | | negcl 10957 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → -𝐴 ∈
ℂ) |
76 | 75 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -𝐴 ∈ ℂ) |
77 | | reneg 14567 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ →
(ℜ‘-𝐴) =
-(ℜ‘𝐴)) |
78 | 77 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘-𝐴) = -(ℜ‘𝐴)) |
79 | | halfpire 25201 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (π /
2) ∈ ℝ |
80 | 79 | renegcli 11018 |
. . . . . . . . . . . . . . . . . . 19
⊢ -(π /
2) ∈ ℝ |
81 | | recl 14552 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℝ) |
82 | | iooneg 12938 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((-(π
/ 2) ∈ ℝ ∧ (π / 2) ∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ) →
((ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2)) ↔ -(ℜ‘𝐴) ∈ (-(π / 2)(,)--(π /
2)))) |
83 | 80, 79, 81, 82 | mp3an12i 1466 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ →
((ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2)) ↔ -(ℜ‘𝐴) ∈ (-(π / 2)(,)--(π /
2)))) |
84 | 83 | biimpa 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -(ℜ‘𝐴) ∈ (-(π / 2)(,)--(π /
2))) |
85 | 79 | recni 10726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (π /
2) ∈ ℂ |
86 | 85 | negnegi 11027 |
. . . . . . . . . . . . . . . . . 18
⊢ --(π /
2) = (π / 2) |
87 | 86 | oveq2i 7175 |
. . . . . . . . . . . . . . . . 17
⊢ (-(π /
2)(,)--(π / 2)) = (-(π / 2)(,)(π / 2)) |
88 | 84, 87 | eleqtrdi 2843 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -(ℜ‘𝐴) ∈ (-(π / 2)(,)(π /
2))) |
89 | 78, 88 | eqeltrd 2833 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘-𝐴) ∈ (-(π / 2)(,)(π /
2))) |
90 | | asinsinlem 25621 |
. . . . . . . . . . . . . . 15
⊢ ((-𝐴 ∈ ℂ ∧
(ℜ‘-𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < (ℜ‘(exp‘(i ·
-𝐴)))) |
91 | 76, 89, 90 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < (ℜ‘(exp‘(i ·
-𝐴)))) |
92 | | mulneg12 11149 |
. . . . . . . . . . . . . . . . 17
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (-i · 𝐴) = (i · -𝐴)) |
93 | 5, 8, 92 | sylancr 590 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (-i · 𝐴) = (i · -𝐴)) |
94 | 93 | fveq2d 6672 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(-i · 𝐴)) = (exp‘(i · -𝐴))) |
95 | 94 | fveq2d 6672 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(exp‘(-i · 𝐴))) =
(ℜ‘(exp‘(i · -𝐴)))) |
96 | 91, 95 | breqtrrd 5055 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < (ℜ‘(exp‘(-i ·
𝐴)))) |
97 | 72, 73, 74, 96 | addgt0d 11286 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < ((ℜ‘(exp‘(i ·
𝐴))) +
(ℜ‘(exp‘(-i · 𝐴))))) |
98 | 12, 67 | readdd 14656 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘((exp‘(i · 𝐴)) + (exp‘(-i ·
𝐴)))) =
((ℜ‘(exp‘(i · 𝐴))) + (ℜ‘(exp‘(-i ·
𝐴))))) |
99 | 97, 98 | breqtrrd 5055 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < (ℜ‘((exp‘(i ·
𝐴)) + (exp‘(-i
· 𝐴))))) |
100 | 62, 69, 71, 99 | mulgt0d 10866 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < ((1 / 2) ·
(ℜ‘((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴)))))) |
101 | | cosval 15561 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(cos‘𝐴) =
(((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2)) |
102 | 101 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘𝐴) = (((exp‘(i · 𝐴)) + (exp‘(-i ·
𝐴))) / 2)) |
103 | | 2ne0 11813 |
. . . . . . . . . . . . . . 15
⊢ 2 ≠
0 |
104 | 103 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 2 ≠ 0) |
105 | 68, 23, 104 | divrec2d 11491 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2) = ((1 / 2) ·
((exp‘(i · 𝐴))
+ (exp‘(-i · 𝐴))))) |
106 | 102, 105 | eqtrd 2773 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘𝐴) = ((1 / 2) · ((exp‘(i
· 𝐴)) +
(exp‘(-i · 𝐴))))) |
107 | 106 | fveq2d 6672 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(cos‘𝐴)) = (ℜ‘((1 / 2) ·
((exp‘(i · 𝐴))
+ (exp‘(-i · 𝐴)))))) |
108 | | remul2 14572 |
. . . . . . . . . . . 12
⊢ (((1 / 2)
∈ ℝ ∧ ((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) ∈ ℂ) →
(ℜ‘((1 / 2) · ((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))))) = ((1 / 2) ·
(ℜ‘((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴)))))) |
109 | 61, 68, 108 | sylancr 590 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘((1 / 2) ·
((exp‘(i · 𝐴))
+ (exp‘(-i · 𝐴))))) = ((1 / 2) ·
(ℜ‘((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴)))))) |
110 | 107, 109 | eqtrd 2773 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(cos‘𝐴)) = ((1 / 2) ·
(ℜ‘((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴)))))) |
111 | 100, 110 | breqtrrd 5055 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < (ℜ‘(cos‘𝐴))) |
112 | 27, 7, 43 | mvrraddd 11123 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) − (i · (sin‘𝐴))) = (cos‘𝐴)) |
113 | 112 | fveq2d 6672 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘((exp‘(i · 𝐴)) − (i ·
(sin‘𝐴)))) =
(ℜ‘(cos‘𝐴))) |
114 | 111, 113 | breqtrrd 5055 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < (ℜ‘((exp‘(i ·
𝐴)) − (i ·
(sin‘𝐴))))) |
115 | 14, 18, 60, 114 | eqsqrt2d 14811 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) − (i · (sin‘𝐴))) = (√‘(1 −
((sin‘𝐴)↑2)))) |
116 | 115 | oveq2d 7180 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i · (sin‘𝐴)) + ((exp‘(i · 𝐴)) − (i ·
(sin‘𝐴)))) = ((i
· (sin‘𝐴)) +
(√‘(1 − ((sin‘𝐴)↑2))))) |
117 | 13, 116 | eqtr3d 2775 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(i · 𝐴)) = ((i · (sin‘𝐴)) + (√‘(1 −
((sin‘𝐴)↑2))))) |
118 | 117 | fveq2d 6672 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (log‘(exp‘(i · 𝐴))) = (log‘((i ·
(sin‘𝐴)) +
(√‘(1 − ((sin‘𝐴)↑2)))))) |
119 | | pire 25195 |
. . . . . . . . . 10
⊢ π
∈ ℝ |
120 | 119 | renegcli 11018 |
. . . . . . . . 9
⊢ -π
∈ ℝ |
121 | 120 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -π ∈ ℝ) |
122 | 80 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -(π / 2) ∈ ℝ) |
123 | | elioore 12844 |
. . . . . . . . 9
⊢
((ℜ‘𝐴)
∈ (-(π / 2)(,)(π / 2)) → (ℜ‘𝐴) ∈ ℝ) |
124 | 123 | adantl 485 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) ∈ ℝ) |
125 | | pirp 25198 |
. . . . . . . . . . 11
⊢ π
∈ ℝ+ |
126 | | rphalflt 12494 |
. . . . . . . . . . 11
⊢ (π
∈ ℝ+ → (π / 2) < π) |
127 | 125, 126 | ax-mp 5 |
. . . . . . . . . 10
⊢ (π /
2) < π |
128 | 79, 119 | ltnegi 11255 |
. . . . . . . . . 10
⊢ ((π /
2) < π ↔ -π < -(π / 2)) |
129 | 127, 128 | mpbi 233 |
. . . . . . . . 9
⊢ -π
< -(π / 2) |
130 | 129 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -π < -(π / 2)) |
131 | | eliooord 12873 |
. . . . . . . . . 10
⊢
((ℜ‘𝐴)
∈ (-(π / 2)(,)(π / 2)) → (-(π / 2) < (ℜ‘𝐴) ∧ (ℜ‘𝐴) < (π /
2))) |
132 | 131 | adantl 485 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (-(π / 2) < (ℜ‘𝐴) ∧ (ℜ‘𝐴) < (π /
2))) |
133 | 132 | simpld 498 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -(π / 2) < (ℜ‘𝐴)) |
134 | 121, 122,
124, 130, 133 | lttrd 10872 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -π < (ℜ‘𝐴)) |
135 | | imre 14550 |
. . . . . . . . 9
⊢ ((i
· 𝐴) ∈ ℂ
→ (ℑ‘(i · 𝐴)) = (ℜ‘(-i · (i ·
𝐴)))) |
136 | 10, 135 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℑ‘(i · 𝐴)) = (ℜ‘(-i · (i ·
𝐴)))) |
137 | 5, 5 | mulneg1i 11157 |
. . . . . . . . . . . 12
⊢ (-i
· i) = -(i · i) |
138 | | ixi 11340 |
. . . . . . . . . . . . 13
⊢ (i
· i) = -1 |
139 | 138 | negeqi 10950 |
. . . . . . . . . . . 12
⊢ -(i
· i) = --1 |
140 | 15 | negnegi 11027 |
. . . . . . . . . . . 12
⊢ --1 =
1 |
141 | 137, 139,
140 | 3eqtri 2765 |
. . . . . . . . . . 11
⊢ (-i
· i) = 1 |
142 | 141 | oveq1i 7174 |
. . . . . . . . . 10
⊢ ((-i
· i) · 𝐴) =
(1 · 𝐴) |
143 | 63 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -i ∈ ℂ) |
144 | 5 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → i ∈ ℂ) |
145 | 143, 144,
8 | mulassd 10735 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((-i · i) · 𝐴) = (-i · (i · 𝐴))) |
146 | | mulid2 10711 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (1
· 𝐴) = 𝐴) |
147 | 146 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (1 · 𝐴) = 𝐴) |
148 | 142, 145,
147 | 3eqtr3a 2797 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (-i · (i · 𝐴)) = 𝐴) |
149 | 148 | fveq2d 6672 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(-i · (i · 𝐴))) = (ℜ‘𝐴)) |
150 | 136, 149 | eqtrd 2773 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℑ‘(i · 𝐴)) = (ℜ‘𝐴)) |
151 | 134, 150 | breqtrrd 5055 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -π < (ℑ‘(i · 𝐴))) |
152 | 119 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → π ∈ ℝ) |
153 | 79 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (π / 2) ∈ ℝ) |
154 | 132 | simprd 499 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) < (π / 2)) |
155 | 127 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (π / 2) < π) |
156 | 124, 153,
152, 154, 155 | lttrd 10872 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) < π) |
157 | 124, 152,
156 | ltled 10859 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) ≤ π) |
158 | 150, 157 | eqbrtrd 5049 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℑ‘(i · 𝐴)) ≤ π) |
159 | | ellogrn 25295 |
. . . . . 6
⊢ ((i
· 𝐴) ∈ ran log
↔ ((i · 𝐴)
∈ ℂ ∧ -π < (ℑ‘(i · 𝐴)) ∧ (ℑ‘(i · 𝐴)) ≤ π)) |
160 | 10, 151, 158, 159 | syl3anbrc 1344 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · 𝐴) ∈ ran log) |
161 | | logef 25317 |
. . . . 5
⊢ ((i
· 𝐴) ∈ ran log
→ (log‘(exp‘(i · 𝐴))) = (i · 𝐴)) |
162 | 160, 161 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (log‘(exp‘(i · 𝐴))) = (i · 𝐴)) |
163 | 118, 162 | eqtr3d 2775 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (log‘((i · (sin‘𝐴)) + (√‘(1 −
((sin‘𝐴)↑2)))))
= (i · 𝐴)) |
164 | 163 | oveq2d 7180 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (-i · (log‘((i ·
(sin‘𝐴)) +
(√‘(1 − ((sin‘𝐴)↑2)))))) = (-i · (i ·
𝐴))) |
165 | 4, 164, 148 | 3eqtrd 2777 |
1
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (arcsin‘(sin‘𝐴)) = 𝐴) |