Proof of Theorem asinsin
| Step | Hyp | Ref
| Expression |
| 1 | | sincl 16162 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(sin‘𝐴) ∈
ℂ) |
| 2 | 1 | adantr 480 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (sin‘𝐴) ∈ ℂ) |
| 3 | | asinval 26925 |
. . 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 11214 |
. . . . . . . 8
⊢ i ∈
ℂ |
| 6 | | mulcl 11239 |
. . . . . . . 8
⊢ ((i
∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i ·
(sin‘𝐴)) ∈
ℂ) |
| 7 | 5, 2, 6 | sylancr 587 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · (sin‘𝐴)) ∈ ℂ) |
| 8 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 𝐴 ∈ ℂ) |
| 9 | | mulcl 11239 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
| 10 | 5, 8, 9 | sylancr 587 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · 𝐴) ∈ ℂ) |
| 11 | | efcl 16118 |
. . . . . . . 8
⊢ ((i
· 𝐴) ∈ ℂ
→ (exp‘(i · 𝐴)) ∈ ℂ) |
| 12 | 10, 11 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(i · 𝐴)) ∈ ℂ) |
| 13 | 7, 12 | pncan3d 11623 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i · (sin‘𝐴)) + ((exp‘(i · 𝐴)) − (i ·
(sin‘𝐴)))) =
(exp‘(i · 𝐴))) |
| 14 | 12, 7 | subcld 11620 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) − (i · (sin‘𝐴))) ∈
ℂ) |
| 15 | | ax-1cn 11213 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
| 16 | 2 | sqcld 14184 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((sin‘𝐴)↑2) ∈ ℂ) |
| 17 | | subcl 11507 |
. . . . . . . . 9
⊢ ((1
∈ ℂ ∧ ((sin‘𝐴)↑2) ∈ ℂ) → (1 −
((sin‘𝐴)↑2))
∈ ℂ) |
| 18 | 15, 16, 17 | sylancr 587 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (1 − ((sin‘𝐴)↑2)) ∈ ℂ) |
| 19 | | binom2sub 14259 |
. . . . . . . . . 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 584 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) − (i · (sin‘𝐴)))↑2) = ((((exp‘(i
· 𝐴))↑2)
− (2 · ((exp‘(i · 𝐴)) · (i · (sin‘𝐴))))) + ((i ·
(sin‘𝐴))↑2))) |
| 21 | 12 | sqvald 14183 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴))↑2) = ((exp‘(i · 𝐴)) · (exp‘(i
· 𝐴)))) |
| 22 | | 2cn 12341 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ |
| 23 | 22 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 2 ∈ ℂ) |
| 24 | 23, 12, 7 | mul12d 11470 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (2 · ((exp‘(i · 𝐴)) · (i ·
(sin‘𝐴)))) =
((exp‘(i · 𝐴))
· (2 · (i · (sin‘𝐴))))) |
| 25 | 21, 24 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴))↑2) − (2 ·
((exp‘(i · 𝐴))
· (i · (sin‘𝐴))))) = (((exp‘(i · 𝐴)) · (exp‘(i
· 𝐴))) −
((exp‘(i · 𝐴))
· (2 · (i · (sin‘𝐴)))))) |
| 26 | | coscl 16163 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(cos‘𝐴) ∈
ℂ) |
| 27 | 26 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘𝐴) ∈ ℂ) |
| 28 | | subsq 14249 |
. . . . . . . . . . . . 13
⊢
(((cos‘𝐴)
∈ ℂ ∧ (i · (sin‘𝐴)) ∈ ℂ) → (((cos‘𝐴)↑2) − ((i ·
(sin‘𝐴))↑2)) =
(((cos‘𝐴) + (i
· (sin‘𝐴)))
· ((cos‘𝐴)
− (i · (sin‘𝐴))))) |
| 29 | 27, 7, 28 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴)↑2) − ((i ·
(sin‘𝐴))↑2)) =
(((cos‘𝐴) + (i
· (sin‘𝐴)))
· ((cos‘𝐴)
− (i · (sin‘𝐴))))) |
| 30 | | sqmul 14159 |
. . . . . . . . . . . . . . . 16
⊢ ((i
∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → ((i ·
(sin‘𝐴))↑2) =
((i↑2) · ((sin‘𝐴)↑2))) |
| 31 | 5, 2, 30 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i · (sin‘𝐴))↑2) = ((i↑2) ·
((sin‘𝐴)↑2))) |
| 32 | | i2 14241 |
. . . . . . . . . . . . . . . . 17
⊢
(i↑2) = -1 |
| 33 | 32 | oveq1i 7441 |
. . . . . . . . . . . . . . . 16
⊢
((i↑2) · ((sin‘𝐴)↑2)) = (-1 · ((sin‘𝐴)↑2)) |
| 34 | 16 | mulm1d 11715 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (-1 · ((sin‘𝐴)↑2)) = -((sin‘𝐴)↑2)) |
| 35 | 33, 34 | eqtrid 2789 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i↑2) · ((sin‘𝐴)↑2)) = -((sin‘𝐴)↑2)) |
| 36 | 31, 35 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i · (sin‘𝐴))↑2) = -((sin‘𝐴)↑2)) |
| 37 | 36 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴)↑2) − ((i ·
(sin‘𝐴))↑2)) =
(((cos‘𝐴)↑2)
− -((sin‘𝐴)↑2))) |
| 38 | 27 | sqcld 14184 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((cos‘𝐴)↑2) ∈ ℂ) |
| 39 | 38, 16 | subnegd 11627 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴)↑2) − -((sin‘𝐴)↑2)) = (((cos‘𝐴)↑2) + ((sin‘𝐴)↑2))) |
| 40 | 38, 16 | addcomd 11463 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴)↑2) + ((sin‘𝐴)↑2)) = (((sin‘𝐴)↑2) + ((cos‘𝐴)↑2))) |
| 41 | 37, 39, 40 | 3eqtrd 2781 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴)↑2) − ((i ·
(sin‘𝐴))↑2)) =
(((sin‘𝐴)↑2) +
((cos‘𝐴)↑2))) |
| 42 | | efival 16188 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
(exp‘(i · 𝐴))
= ((cos‘𝐴) + (i
· (sin‘𝐴)))) |
| 43 | 42 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(i · 𝐴)) = ((cos‘𝐴) + (i · (sin‘𝐴)))) |
| 44 | 7 | 2timesd 12509 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (2 · (i · (sin‘𝐴))) = ((i ·
(sin‘𝐴)) + (i
· (sin‘𝐴)))) |
| 45 | 43, 44 | oveq12d 7449 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) − (2 · (i ·
(sin‘𝐴)))) =
(((cos‘𝐴) + (i
· (sin‘𝐴)))
− ((i · (sin‘𝐴)) + (i · (sin‘𝐴))))) |
| 46 | 27, 7, 7 | pnpcan2d 11658 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) − ((i · (sin‘𝐴)) + (i ·
(sin‘𝐴)))) =
((cos‘𝐴) − (i
· (sin‘𝐴)))) |
| 47 | 45, 46 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) − (2 · (i ·
(sin‘𝐴)))) =
((cos‘𝐴) − (i
· (sin‘𝐴)))) |
| 48 | 43, 47 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) · ((exp‘(i · 𝐴)) − (2 · (i
· (sin‘𝐴)))))
= (((cos‘𝐴) + (i
· (sin‘𝐴)))
· ((cos‘𝐴)
− (i · (sin‘𝐴))))) |
| 49 | | mulcl 11239 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℂ ∧ (i · (sin‘𝐴)) ∈ ℂ) → (2 · (i
· (sin‘𝐴)))
∈ ℂ) |
| 50 | 22, 7, 49 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (2 · (i · (sin‘𝐴))) ∈
ℂ) |
| 51 | 12, 12, 50 | subdid 11719 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) · ((exp‘(i · 𝐴)) − (2 · (i
· (sin‘𝐴)))))
= (((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) − ((exp‘(i
· 𝐴)) · (2
· (i · (sin‘𝐴)))))) |
| 52 | 48, 51 | eqtr3d 2779 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) · ((cos‘𝐴) − (i · (sin‘𝐴)))) = (((exp‘(i ·
𝐴)) · (exp‘(i
· 𝐴))) −
((exp‘(i · 𝐴))
· (2 · (i · (sin‘𝐴)))))) |
| 53 | 29, 41, 52 | 3eqtr3d 2785 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((sin‘𝐴)↑2) + ((cos‘𝐴)↑2)) = (((exp‘(i · 𝐴)) · (exp‘(i
· 𝐴))) −
((exp‘(i · 𝐴))
· (2 · (i · (sin‘𝐴)))))) |
| 54 | | sincossq 16212 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
(((sin‘𝐴)↑2) +
((cos‘𝐴)↑2)) =
1) |
| 55 | 54 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((sin‘𝐴)↑2) + ((cos‘𝐴)↑2)) = 1) |
| 56 | 25, 53, 55 | 3eqtr2d 2783 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴))↑2) − (2 ·
((exp‘(i · 𝐴))
· (i · (sin‘𝐴))))) = 1) |
| 57 | 56, 36 | oveq12d 7449 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((((exp‘(i · 𝐴))↑2) − (2 ·
((exp‘(i · 𝐴))
· (i · (sin‘𝐴))))) + ((i · (sin‘𝐴))↑2)) = (1 +
-((sin‘𝐴)↑2))) |
| 58 | | negsub 11557 |
. . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ ((sin‘𝐴)↑2) ∈ ℂ) → (1 +
-((sin‘𝐴)↑2)) =
(1 − ((sin‘𝐴)↑2))) |
| 59 | 15, 16, 58 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (1 + -((sin‘𝐴)↑2)) = (1 − ((sin‘𝐴)↑2))) |
| 60 | 20, 57, 59 | 3eqtrd 2781 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) − (i · (sin‘𝐴)))↑2) = (1 −
((sin‘𝐴)↑2))) |
| 61 | | halfre 12480 |
. . . . . . . . . . . 12
⊢ (1 / 2)
∈ ℝ |
| 62 | 61 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (1 / 2) ∈ ℝ) |
| 63 | | negicn 11509 |
. . . . . . . . . . . . . . 15
⊢ -i ∈
ℂ |
| 64 | | mulcl 11239 |
. . . . . . . . . . . . . . 15
⊢ ((-i
∈ ℂ ∧ 𝐴
∈ ℂ) → (-i · 𝐴) ∈ ℂ) |
| 65 | 63, 8, 64 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (-i · 𝐴) ∈ ℂ) |
| 66 | | efcl 16118 |
. . . . . . . . . . . . . 14
⊢ ((-i
· 𝐴) ∈ ℂ
→ (exp‘(-i · 𝐴)) ∈ ℂ) |
| 67 | 65, 66 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(-i · 𝐴)) ∈ ℂ) |
| 68 | 12, 67 | addcld 11280 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) ∈
ℂ) |
| 69 | 68 | recld 15233 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘((exp‘(i · 𝐴)) + (exp‘(-i ·
𝐴)))) ∈
ℝ) |
| 70 | | halfgt0 12482 |
. . . . . . . . . . . 12
⊢ 0 < (1
/ 2) |
| 71 | 70 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < (1 / 2)) |
| 72 | 12 | recld 15233 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(exp‘(i · 𝐴))) ∈
ℝ) |
| 73 | 67 | recld 15233 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(exp‘(-i · 𝐴))) ∈
ℝ) |
| 74 | | asinsinlem 26934 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < (ℜ‘(exp‘(i ·
𝐴)))) |
| 75 | | negcl 11508 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → -𝐴 ∈
ℂ) |
| 76 | 75 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -𝐴 ∈ ℂ) |
| 77 | | reneg 15164 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ →
(ℜ‘-𝐴) =
-(ℜ‘𝐴)) |
| 78 | 77 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘-𝐴) = -(ℜ‘𝐴)) |
| 79 | | halfpire 26506 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (π /
2) ∈ ℝ |
| 80 | 79 | renegcli 11570 |
. . . . . . . . . . . . . . . . . . 19
⊢ -(π /
2) ∈ ℝ |
| 81 | | recl 15149 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℝ) |
| 82 | | iooneg 13511 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((-(π
/ 2) ∈ ℝ ∧ (π / 2) ∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ) →
((ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2)) ↔ -(ℜ‘𝐴) ∈ (-(π / 2)(,)--(π /
2)))) |
| 83 | 80, 79, 81, 82 | mp3an12i 1467 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ →
((ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2)) ↔ -(ℜ‘𝐴) ∈ (-(π / 2)(,)--(π /
2)))) |
| 84 | 83 | biimpa 476 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -(ℜ‘𝐴) ∈ (-(π / 2)(,)--(π /
2))) |
| 85 | 79 | recni 11275 |
. . . . . . . . . . . . . . . . . . 19
⊢ (π /
2) ∈ ℂ |
| 86 | 85 | negnegi 11579 |
. . . . . . . . . . . . . . . . . 18
⊢ --(π /
2) = (π / 2) |
| 87 | 86 | oveq2i 7442 |
. . . . . . . . . . . . . . . . 17
⊢ (-(π /
2)(,)--(π / 2)) = (-(π / 2)(,)(π / 2)) |
| 88 | 84, 87 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -(ℜ‘𝐴) ∈ (-(π / 2)(,)(π /
2))) |
| 89 | 78, 88 | eqeltrd 2841 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘-𝐴) ∈ (-(π / 2)(,)(π /
2))) |
| 90 | | asinsinlem 26934 |
. . . . . . . . . . . . . . 15
⊢ ((-𝐴 ∈ ℂ ∧
(ℜ‘-𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < (ℜ‘(exp‘(i ·
-𝐴)))) |
| 91 | 76, 89, 90 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < (ℜ‘(exp‘(i ·
-𝐴)))) |
| 92 | | mulneg12 11701 |
. . . . . . . . . . . . . . . . 17
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (-i · 𝐴) = (i · -𝐴)) |
| 93 | 5, 8, 92 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (-i · 𝐴) = (i · -𝐴)) |
| 94 | 93 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(-i · 𝐴)) = (exp‘(i · -𝐴))) |
| 95 | 94 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(exp‘(-i · 𝐴))) =
(ℜ‘(exp‘(i · -𝐴)))) |
| 96 | 91, 95 | breqtrrd 5171 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < (ℜ‘(exp‘(-i ·
𝐴)))) |
| 97 | 72, 73, 74, 96 | addgt0d 11838 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < ((ℜ‘(exp‘(i ·
𝐴))) +
(ℜ‘(exp‘(-i · 𝐴))))) |
| 98 | 12, 67 | readdd 15253 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘((exp‘(i · 𝐴)) + (exp‘(-i ·
𝐴)))) =
((ℜ‘(exp‘(i · 𝐴))) + (ℜ‘(exp‘(-i ·
𝐴))))) |
| 99 | 97, 98 | breqtrrd 5171 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < (ℜ‘((exp‘(i ·
𝐴)) + (exp‘(-i
· 𝐴))))) |
| 100 | 62, 69, 71, 99 | mulgt0d 11416 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < ((1 / 2) ·
(ℜ‘((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴)))))) |
| 101 | | cosval 16159 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(cos‘𝐴) =
(((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2)) |
| 102 | 101 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘𝐴) = (((exp‘(i · 𝐴)) + (exp‘(-i ·
𝐴))) / 2)) |
| 103 | | 2ne0 12370 |
. . . . . . . . . . . . . . 15
⊢ 2 ≠
0 |
| 104 | 103 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 2 ≠ 0) |
| 105 | 68, 23, 104 | divrec2d 12047 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) / 2) = ((1 / 2) ·
((exp‘(i · 𝐴))
+ (exp‘(-i · 𝐴))))) |
| 106 | 102, 105 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (cos‘𝐴) = ((1 / 2) · ((exp‘(i
· 𝐴)) +
(exp‘(-i · 𝐴))))) |
| 107 | 106 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(cos‘𝐴)) = (ℜ‘((1 / 2) ·
((exp‘(i · 𝐴))
+ (exp‘(-i · 𝐴)))))) |
| 108 | | remul2 15169 |
. . . . . . . . . . . 12
⊢ (((1 / 2)
∈ ℝ ∧ ((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))) ∈ ℂ) →
(ℜ‘((1 / 2) · ((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴))))) = ((1 / 2) ·
(ℜ‘((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴)))))) |
| 109 | 61, 68, 108 | sylancr 587 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘((1 / 2) ·
((exp‘(i · 𝐴))
+ (exp‘(-i · 𝐴))))) = ((1 / 2) ·
(ℜ‘((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴)))))) |
| 110 | 107, 109 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(cos‘𝐴)) = ((1 / 2) ·
(ℜ‘((exp‘(i · 𝐴)) + (exp‘(-i · 𝐴)))))) |
| 111 | 100, 110 | breqtrrd 5171 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < (ℜ‘(cos‘𝐴))) |
| 112 | 27, 7, 43 | mvrraddd 11675 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) − (i · (sin‘𝐴))) = (cos‘𝐴)) |
| 113 | 112 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘((exp‘(i · 𝐴)) − (i ·
(sin‘𝐴)))) =
(ℜ‘(cos‘𝐴))) |
| 114 | 111, 113 | breqtrrd 5171 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → 0 < (ℜ‘((exp‘(i ·
𝐴)) − (i ·
(sin‘𝐴))))) |
| 115 | 14, 18, 60, 114 | eqsqrt2d 15407 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((exp‘(i · 𝐴)) − (i · (sin‘𝐴))) = (√‘(1 −
((sin‘𝐴)↑2)))) |
| 116 | 115 | oveq2d 7447 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((i · (sin‘𝐴)) + ((exp‘(i · 𝐴)) − (i ·
(sin‘𝐴)))) = ((i
· (sin‘𝐴)) +
(√‘(1 − ((sin‘𝐴)↑2))))) |
| 117 | 13, 116 | eqtr3d 2779 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (exp‘(i · 𝐴)) = ((i · (sin‘𝐴)) + (√‘(1 −
((sin‘𝐴)↑2))))) |
| 118 | 117 | fveq2d 6910 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (log‘(exp‘(i · 𝐴))) = (log‘((i ·
(sin‘𝐴)) +
(√‘(1 − ((sin‘𝐴)↑2)))))) |
| 119 | | pire 26500 |
. . . . . . . . . 10
⊢ π
∈ ℝ |
| 120 | 119 | renegcli 11570 |
. . . . . . . . 9
⊢ -π
∈ ℝ |
| 121 | 120 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -π ∈ ℝ) |
| 122 | 80 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -(π / 2) ∈ ℝ) |
| 123 | | elioore 13417 |
. . . . . . . . 9
⊢
((ℜ‘𝐴)
∈ (-(π / 2)(,)(π / 2)) → (ℜ‘𝐴) ∈ ℝ) |
| 124 | 123 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) ∈ ℝ) |
| 125 | | pirp 26503 |
. . . . . . . . . . 11
⊢ π
∈ ℝ+ |
| 126 | | rphalflt 13064 |
. . . . . . . . . . 11
⊢ (π
∈ ℝ+ → (π / 2) < π) |
| 127 | 125, 126 | ax-mp 5 |
. . . . . . . . . 10
⊢ (π /
2) < π |
| 128 | 79, 119 | ltnegi 11807 |
. . . . . . . . . 10
⊢ ((π /
2) < π ↔ -π < -(π / 2)) |
| 129 | 127, 128 | mpbi 230 |
. . . . . . . . 9
⊢ -π
< -(π / 2) |
| 130 | 129 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -π < -(π / 2)) |
| 131 | | eliooord 13446 |
. . . . . . . . . 10
⊢
((ℜ‘𝐴)
∈ (-(π / 2)(,)(π / 2)) → (-(π / 2) < (ℜ‘𝐴) ∧ (ℜ‘𝐴) < (π /
2))) |
| 132 | 131 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (-(π / 2) < (ℜ‘𝐴) ∧ (ℜ‘𝐴) < (π /
2))) |
| 133 | 132 | simpld 494 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -(π / 2) < (ℜ‘𝐴)) |
| 134 | 121, 122,
124, 130, 133 | lttrd 11422 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -π < (ℜ‘𝐴)) |
| 135 | | imre 15147 |
. . . . . . . . 9
⊢ ((i
· 𝐴) ∈ ℂ
→ (ℑ‘(i · 𝐴)) = (ℜ‘(-i · (i ·
𝐴)))) |
| 136 | 10, 135 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℑ‘(i · 𝐴)) = (ℜ‘(-i · (i ·
𝐴)))) |
| 137 | 5, 5 | mulneg1i 11709 |
. . . . . . . . . . . 12
⊢ (-i
· i) = -(i · i) |
| 138 | | ixi 11892 |
. . . . . . . . . . . . 13
⊢ (i
· i) = -1 |
| 139 | 138 | negeqi 11501 |
. . . . . . . . . . . 12
⊢ -(i
· i) = --1 |
| 140 | 15 | negnegi 11579 |
. . . . . . . . . . . 12
⊢ --1 =
1 |
| 141 | 137, 139,
140 | 3eqtri 2769 |
. . . . . . . . . . 11
⊢ (-i
· i) = 1 |
| 142 | 141 | oveq1i 7441 |
. . . . . . . . . 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 11284 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → ((-i · i) · 𝐴) = (-i · (i · 𝐴))) |
| 146 | | mullid 11260 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (1
· 𝐴) = 𝐴) |
| 147 | 146 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (1 · 𝐴) = 𝐴) |
| 148 | 142, 145,
147 | 3eqtr3a 2801 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (-i · (i · 𝐴)) = 𝐴) |
| 149 | 148 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘(-i · (i · 𝐴))) = (ℜ‘𝐴)) |
| 150 | 136, 149 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℑ‘(i · 𝐴)) = (ℜ‘𝐴)) |
| 151 | 134, 150 | breqtrrd 5171 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → -π < (ℑ‘(i · 𝐴))) |
| 152 | 119 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → π ∈ ℝ) |
| 153 | 79 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (π / 2) ∈ ℝ) |
| 154 | 132 | simprd 495 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) < (π / 2)) |
| 155 | 127 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (π / 2) < π) |
| 156 | 124, 153,
152, 154, 155 | lttrd 11422 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) < π) |
| 157 | 124, 152,
156 | ltled 11409 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℜ‘𝐴) ≤ π) |
| 158 | 150, 157 | eqbrtrd 5165 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (ℑ‘(i · 𝐴)) ≤ π) |
| 159 | | ellogrn 26601 |
. . . . . 6
⊢ ((i
· 𝐴) ∈ ran log
↔ ((i · 𝐴)
∈ ℂ ∧ -π < (ℑ‘(i · 𝐴)) ∧ (ℑ‘(i · 𝐴)) ≤ π)) |
| 160 | 10, 151, 158, 159 | syl3anbrc 1344 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (i · 𝐴) ∈ ran log) |
| 161 | | logef 26623 |
. . . . 5
⊢ ((i
· 𝐴) ∈ ran log
→ (log‘(exp‘(i · 𝐴))) = (i · 𝐴)) |
| 162 | 160, 161 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (log‘(exp‘(i · 𝐴))) = (i · 𝐴)) |
| 163 | 118, 162 | eqtr3d 2779 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (log‘((i · (sin‘𝐴)) + (√‘(1 −
((sin‘𝐴)↑2)))))
= (i · 𝐴)) |
| 164 | 163 | oveq2d 7447 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (-i · (log‘((i ·
(sin‘𝐴)) +
(√‘(1 − ((sin‘𝐴)↑2)))))) = (-i · (i ·
𝐴))) |
| 165 | 4, 164, 148 | 3eqtrd 2781 |
1
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
(-(π / 2)(,)(π / 2))) → (arcsin‘(sin‘𝐴)) = 𝐴) |