Proof of Theorem sinhval
| Step | Hyp | Ref
| Expression |
| 1 | | ixi 11892 |
. . . . . . . . 9
⊢ (i
· i) = -1 |
| 2 | 1 | oveq1i 7441 |
. . . . . . . 8
⊢ ((i
· i) · 𝐴) =
(-1 · 𝐴) |
| 3 | | ax-icn 11214 |
. . . . . . . . 9
⊢ i ∈
ℂ |
| 4 | | mulass 11243 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ i ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((i · i)
· 𝐴) = (i ·
(i · 𝐴))) |
| 5 | 3, 3, 4 | mp3an12 1453 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((i
· i) · 𝐴) =
(i · (i · 𝐴))) |
| 6 | | mulm1 11704 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (-1
· 𝐴) = -𝐴) |
| 7 | 2, 5, 6 | 3eqtr3a 2801 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (i
· (i · 𝐴)) =
-𝐴) |
| 8 | 7 | fveq2d 6910 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(exp‘(i · (i · 𝐴))) = (exp‘-𝐴)) |
| 9 | 3, 3 | mulneg1i 11709 |
. . . . . . . . . 10
⊢ (-i
· i) = -(i · i) |
| 10 | 1 | negeqi 11501 |
. . . . . . . . . . 11
⊢ -(i
· i) = --1 |
| 11 | | negneg1e1 12384 |
. . . . . . . . . . 11
⊢ --1 =
1 |
| 12 | 10, 11 | eqtri 2765 |
. . . . . . . . . 10
⊢ -(i
· i) = 1 |
| 13 | 9, 12 | eqtri 2765 |
. . . . . . . . 9
⊢ (-i
· i) = 1 |
| 14 | 13 | oveq1i 7441 |
. . . . . . . 8
⊢ ((-i
· i) · 𝐴) =
(1 · 𝐴) |
| 15 | | negicn 11509 |
. . . . . . . . 9
⊢ -i ∈
ℂ |
| 16 | | mulass 11243 |
. . . . . . . . 9
⊢ ((-i
∈ ℂ ∧ i ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((-i · i)
· 𝐴) = (-i ·
(i · 𝐴))) |
| 17 | 15, 3, 16 | mp3an12 1453 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((-i
· i) · 𝐴) =
(-i · (i · 𝐴))) |
| 18 | | mullid 11260 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (1
· 𝐴) = 𝐴) |
| 19 | 14, 17, 18 | 3eqtr3a 2801 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (-i
· (i · 𝐴)) =
𝐴) |
| 20 | 19 | fveq2d 6910 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(exp‘(-i · (i · 𝐴))) = (exp‘𝐴)) |
| 21 | 8, 20 | oveq12d 7449 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
((exp‘(i · (i · 𝐴))) − (exp‘(-i · (i
· 𝐴)))) =
((exp‘-𝐴) −
(exp‘𝐴))) |
| 22 | 21 | oveq1d 7446 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(((exp‘(i · (i · 𝐴))) − (exp‘(-i · (i
· 𝐴)))) / (2
· i)) = (((exp‘-𝐴) − (exp‘𝐴)) / (2 · i))) |
| 23 | | mulcl 11239 |
. . . . . 6
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
| 24 | 3, 23 | mpan 690 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (i
· 𝐴) ∈
ℂ) |
| 25 | | sinval 16158 |
. . . . 5
⊢ ((i
· 𝐴) ∈ ℂ
→ (sin‘(i · 𝐴)) = (((exp‘(i · (i ·
𝐴))) − (exp‘(-i
· (i · 𝐴))))
/ (2 · i))) |
| 26 | 24, 25 | syl 17 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(sin‘(i · 𝐴))
= (((exp‘(i · (i · 𝐴))) − (exp‘(-i · (i
· 𝐴)))) / (2
· i))) |
| 27 | | irec 14240 |
. . . . . . . 8
⊢ (1 / i) =
-i |
| 28 | 27 | negeqi 11501 |
. . . . . . 7
⊢ -(1 / i)
= --i |
| 29 | 3 | negnegi 11579 |
. . . . . . 7
⊢ --i =
i |
| 30 | 28, 29 | eqtri 2765 |
. . . . . 6
⊢ -(1 / i)
= i |
| 31 | 30 | oveq1i 7441 |
. . . . 5
⊢ (-(1 / i)
· (((exp‘𝐴)
− (exp‘-𝐴)) /
2)) = (i · (((exp‘𝐴) − (exp‘-𝐴)) / 2)) |
| 32 | | ine0 11698 |
. . . . . . . 8
⊢ i ≠
0 |
| 33 | 3, 32 | reccli 11997 |
. . . . . . 7
⊢ (1 / i)
∈ ℂ |
| 34 | | efcl 16118 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(exp‘𝐴) ∈
ℂ) |
| 35 | | negcl 11508 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → -𝐴 ∈
ℂ) |
| 36 | | efcl 16118 |
. . . . . . . . . 10
⊢ (-𝐴 ∈ ℂ →
(exp‘-𝐴) ∈
ℂ) |
| 37 | 35, 36 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(exp‘-𝐴) ∈
ℂ) |
| 38 | 34, 37 | subcld 11620 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
((exp‘𝐴) −
(exp‘-𝐴)) ∈
ℂ) |
| 39 | 38 | halfcld 12511 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
(((exp‘𝐴) −
(exp‘-𝐴)) / 2) ∈
ℂ) |
| 40 | | mulneg12 11701 |
. . . . . . 7
⊢ (((1 / i)
∈ ℂ ∧ (((exp‘𝐴) − (exp‘-𝐴)) / 2) ∈ ℂ) → (-(1 / i)
· (((exp‘𝐴)
− (exp‘-𝐴)) /
2)) = ((1 / i) · -(((exp‘𝐴) − (exp‘-𝐴)) / 2))) |
| 41 | 33, 39, 40 | sylancr 587 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (-(1 / i)
· (((exp‘𝐴)
− (exp‘-𝐴)) /
2)) = ((1 / i) · -(((exp‘𝐴) − (exp‘-𝐴)) / 2))) |
| 42 | | 2cnd 12344 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → 2 ∈
ℂ) |
| 43 | | 2ne0 12370 |
. . . . . . . . . . 11
⊢ 2 ≠
0 |
| 44 | 43 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → 2 ≠
0) |
| 45 | 38, 42, 44 | divnegd 12056 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
-(((exp‘𝐴) −
(exp‘-𝐴)) / 2) =
(-((exp‘𝐴) −
(exp‘-𝐴)) /
2)) |
| 46 | 34, 37 | negsubdi2d 11636 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
-((exp‘𝐴) −
(exp‘-𝐴)) =
((exp‘-𝐴) −
(exp‘𝐴))) |
| 47 | 46 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(-((exp‘𝐴) −
(exp‘-𝐴)) / 2) =
(((exp‘-𝐴) −
(exp‘𝐴)) /
2)) |
| 48 | 45, 47 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
-(((exp‘𝐴) −
(exp‘-𝐴)) / 2) =
(((exp‘-𝐴) −
(exp‘𝐴)) /
2)) |
| 49 | 48 | oveq2d 7447 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → ((1 / i)
· -(((exp‘𝐴)
− (exp‘-𝐴)) /
2)) = ((1 / i) · (((exp‘-𝐴) − (exp‘𝐴)) / 2))) |
| 50 | 37, 34 | subcld 11620 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
((exp‘-𝐴) −
(exp‘𝐴)) ∈
ℂ) |
| 51 | 50 | halfcld 12511 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(((exp‘-𝐴) −
(exp‘𝐴)) / 2) ∈
ℂ) |
| 52 | 3 | a1i 11 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → i ∈
ℂ) |
| 53 | 32 | a1i 11 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → i ≠
0) |
| 54 | 51, 52, 53 | divrec2d 12047 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((((exp‘-𝐴) −
(exp‘𝐴)) / 2) / i) =
((1 / i) · (((exp‘-𝐴) − (exp‘𝐴)) / 2))) |
| 55 | 50, 42, 52, 44, 53 | divdiv1d 12074 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((((exp‘-𝐴) −
(exp‘𝐴)) / 2) / i) =
(((exp‘-𝐴) −
(exp‘𝐴)) / (2
· i))) |
| 56 | 49, 54, 55 | 3eqtr2d 2783 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → ((1 / i)
· -(((exp‘𝐴)
− (exp‘-𝐴)) /
2)) = (((exp‘-𝐴)
− (exp‘𝐴)) / (2
· i))) |
| 57 | 41, 56 | eqtrd 2777 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (-(1 / i)
· (((exp‘𝐴)
− (exp‘-𝐴)) /
2)) = (((exp‘-𝐴)
− (exp‘𝐴)) / (2
· i))) |
| 58 | 31, 57 | eqtr3id 2791 |
. . . 4
⊢ (𝐴 ∈ ℂ → (i
· (((exp‘𝐴)
− (exp‘-𝐴)) /
2)) = (((exp‘-𝐴)
− (exp‘𝐴)) / (2
· i))) |
| 59 | 22, 26, 58 | 3eqtr4d 2787 |
. . 3
⊢ (𝐴 ∈ ℂ →
(sin‘(i · 𝐴))
= (i · (((exp‘𝐴) − (exp‘-𝐴)) / 2))) |
| 60 | 59 | oveq1d 7446 |
. 2
⊢ (𝐴 ∈ ℂ →
((sin‘(i · 𝐴))
/ i) = ((i · (((exp‘𝐴) − (exp‘-𝐴)) / 2)) / i)) |
| 61 | 39, 52, 53 | divcan3d 12048 |
. 2
⊢ (𝐴 ∈ ℂ → ((i
· (((exp‘𝐴)
− (exp‘-𝐴)) /
2)) / i) = (((exp‘𝐴)
− (exp‘-𝐴)) /
2)) |
| 62 | 60, 61 | eqtrd 2777 |
1
⊢ (𝐴 ∈ ℂ →
((sin‘(i · 𝐴))
/ i) = (((exp‘𝐴)
− (exp‘-𝐴)) /
2)) |