Proof of Theorem sinadd
| Step | Hyp | Ref
| Expression |
| 1 | | addcl 11237 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
| 2 | | sinval 16158 |
. . 3
⊢ ((𝐴 + 𝐵) ∈ ℂ → (sin‘(𝐴 + 𝐵)) = (((exp‘(i · (𝐴 + 𝐵))) − (exp‘(-i · (𝐴 + 𝐵)))) / (2 · i))) |
| 3 | 1, 2 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(sin‘(𝐴 + 𝐵)) = (((exp‘(i ·
(𝐴 + 𝐵))) − (exp‘(-i · (𝐴 + 𝐵)))) / (2 · i))) |
| 4 | | 2cn 12341 |
. . . . . . 7
⊢ 2 ∈
ℂ |
| 5 | 4 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 2 ∈
ℂ) |
| 6 | | ax-icn 11214 |
. . . . . . 7
⊢ i ∈
ℂ |
| 7 | 6 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → i ∈
ℂ) |
| 8 | | coscl 16163 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(cos‘𝐴) ∈
ℂ) |
| 9 | 8 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(cos‘𝐴) ∈
ℂ) |
| 10 | | sincl 16162 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℂ →
(sin‘𝐵) ∈
ℂ) |
| 11 | 10 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(sin‘𝐵) ∈
ℂ) |
| 12 | 9, 11 | mulcld 11281 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((cos‘𝐴) ·
(sin‘𝐵)) ∈
ℂ) |
| 13 | | sincl 16162 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(sin‘𝐴) ∈
ℂ) |
| 14 | 13 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(sin‘𝐴) ∈
ℂ) |
| 15 | | coscl 16163 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℂ →
(cos‘𝐵) ∈
ℂ) |
| 16 | 15 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(cos‘𝐵) ∈
ℂ) |
| 17 | 14, 16 | mulcld 11281 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((sin‘𝐴) ·
(cos‘𝐵)) ∈
ℂ) |
| 18 | 12, 17 | addcld 11280 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((cos‘𝐴) ·
(sin‘𝐵)) +
((sin‘𝐴) ·
(cos‘𝐵))) ∈
ℂ) |
| 19 | 5, 7, 18 | mulassd 11284 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((2
· i) · (((cos‘𝐴) · (sin‘𝐵)) + ((sin‘𝐴) · (cos‘𝐵)))) = (2 · (i ·
(((cos‘𝐴) ·
(sin‘𝐵)) +
((sin‘𝐴) ·
(cos‘𝐵)))))) |
| 20 | 7, 12, 17 | adddid 11285 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· (((cos‘𝐴)
· (sin‘𝐵)) +
((sin‘𝐴) ·
(cos‘𝐵)))) = ((i
· ((cos‘𝐴)
· (sin‘𝐵))) +
(i · ((sin‘𝐴)
· (cos‘𝐵))))) |
| 21 | 7, 9, 11 | mul12d 11470 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· ((cos‘𝐴)
· (sin‘𝐵))) =
((cos‘𝐴) · (i
· (sin‘𝐵)))) |
| 22 | 14, 16 | mulcomd 11282 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((sin‘𝐴) ·
(cos‘𝐵)) =
((cos‘𝐵) ·
(sin‘𝐴))) |
| 23 | 22 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· ((sin‘𝐴)
· (cos‘𝐵))) =
(i · ((cos‘𝐵)
· (sin‘𝐴)))) |
| 24 | 7, 16, 14 | mul12d 11470 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· ((cos‘𝐵)
· (sin‘𝐴))) =
((cos‘𝐵) · (i
· (sin‘𝐴)))) |
| 25 | 23, 24 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· ((sin‘𝐴)
· (cos‘𝐵))) =
((cos‘𝐵) · (i
· (sin‘𝐴)))) |
| 26 | 21, 25 | oveq12d 7449 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((i
· ((cos‘𝐴)
· (sin‘𝐵))) +
(i · ((sin‘𝐴)
· (cos‘𝐵)))) =
(((cos‘𝐴) · (i
· (sin‘𝐵))) +
((cos‘𝐵) · (i
· (sin‘𝐴))))) |
| 27 | 20, 26 | eqtrd 2777 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· (((cos‘𝐴)
· (sin‘𝐵)) +
((sin‘𝐴) ·
(cos‘𝐵)))) =
(((cos‘𝐴) · (i
· (sin‘𝐵))) +
((cos‘𝐵) · (i
· (sin‘𝐴))))) |
| 28 | 27 | oveq2d 7447 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2
· (i · (((cos‘𝐴) · (sin‘𝐵)) + ((sin‘𝐴) · (cos‘𝐵))))) = (2 · (((cos‘𝐴) · (i ·
(sin‘𝐵))) +
((cos‘𝐵) · (i
· (sin‘𝐴)))))) |
| 29 | 19, 28 | eqtrd 2777 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((2
· i) · (((cos‘𝐴) · (sin‘𝐵)) + ((sin‘𝐴) · (cos‘𝐵)))) = (2 · (((cos‘𝐴) · (i ·
(sin‘𝐵))) +
((cos‘𝐵) · (i
· (sin‘𝐴)))))) |
| 30 | | mulcl 11239 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ (sin‘𝐵) ∈ ℂ) → (i ·
(sin‘𝐵)) ∈
ℂ) |
| 31 | 6, 11, 30 | sylancr 587 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· (sin‘𝐵))
∈ ℂ) |
| 32 | 9, 31 | mulcld 11281 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((cos‘𝐴) · (i
· (sin‘𝐵)))
∈ ℂ) |
| 33 | | mulcl 11239 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i ·
(sin‘𝐴)) ∈
ℂ) |
| 34 | 6, 14, 33 | sylancr 587 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· (sin‘𝐴))
∈ ℂ) |
| 35 | 16, 34 | mulcld 11281 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((cos‘𝐵) · (i
· (sin‘𝐴)))
∈ ℂ) |
| 36 | 32, 35 | addcld 11280 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((cos‘𝐴) · (i
· (sin‘𝐵))) +
((cos‘𝐵) · (i
· (sin‘𝐴))))
∈ ℂ) |
| 37 | | mulcl 11239 |
. . . . . 6
⊢ ((2
∈ ℂ ∧ (((cos‘𝐴) · (i · (sin‘𝐵))) + ((cos‘𝐵) · (i ·
(sin‘𝐴)))) ∈
ℂ) → (2 · (((cos‘𝐴) · (i · (sin‘𝐵))) + ((cos‘𝐵) · (i ·
(sin‘𝐴))))) ∈
ℂ) |
| 38 | 4, 36, 37 | sylancr 587 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2
· (((cos‘𝐴)
· (i · (sin‘𝐵))) + ((cos‘𝐵) · (i · (sin‘𝐴))))) ∈
ℂ) |
| 39 | | 2mulicn 12489 |
. . . . . 6
⊢ (2
· i) ∈ ℂ |
| 40 | 39 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2
· i) ∈ ℂ) |
| 41 | | 2muline0 12490 |
. . . . . 6
⊢ (2
· i) ≠ 0 |
| 42 | 41 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2
· i) ≠ 0) |
| 43 | 38, 40, 18, 42 | divmuld 12065 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((2
· (((cos‘𝐴)
· (i · (sin‘𝐵))) + ((cos‘𝐵) · (i · (sin‘𝐴))))) / (2 · i)) =
(((cos‘𝐴) ·
(sin‘𝐵)) +
((sin‘𝐴) ·
(cos‘𝐵))) ↔ ((2
· i) · (((cos‘𝐴) · (sin‘𝐵)) + ((sin‘𝐴) · (cos‘𝐵)))) = (2 · (((cos‘𝐴) · (i ·
(sin‘𝐵))) +
((cos‘𝐵) · (i
· (sin‘𝐴))))))) |
| 44 | 29, 43 | mpbird 257 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((2
· (((cos‘𝐴)
· (i · (sin‘𝐵))) + ((cos‘𝐵) · (i · (sin‘𝐴))))) / (2 · i)) =
(((cos‘𝐴) ·
(sin‘𝐵)) +
((sin‘𝐴) ·
(cos‘𝐵)))) |
| 45 | 9, 16 | mulcld 11281 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((cos‘𝐴) ·
(cos‘𝐵)) ∈
ℂ) |
| 46 | 31, 34 | mulcld 11281 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((i
· (sin‘𝐵))
· (i · (sin‘𝐴))) ∈ ℂ) |
| 47 | 45, 46 | addcld 11280 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((cos‘𝐴) ·
(cos‘𝐵)) + ((i
· (sin‘𝐵))
· (i · (sin‘𝐴)))) ∈ ℂ) |
| 48 | 47, 36, 36 | pnncand 11659 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((((cos‘𝐴) ·
(cos‘𝐵)) + ((i
· (sin‘𝐵))
· (i · (sin‘𝐴)))) + (((cos‘𝐴) · (i · (sin‘𝐵))) + ((cos‘𝐵) · (i ·
(sin‘𝐴))))) −
((((cos‘𝐴) ·
(cos‘𝐵)) + ((i
· (sin‘𝐵))
· (i · (sin‘𝐴)))) − (((cos‘𝐴) · (i · (sin‘𝐵))) + ((cos‘𝐵) · (i ·
(sin‘𝐴)))))) =
((((cos‘𝐴) ·
(i · (sin‘𝐵)))
+ ((cos‘𝐵) ·
(i · (sin‘𝐴)))) + (((cos‘𝐴) · (i · (sin‘𝐵))) + ((cos‘𝐵) · (i ·
(sin‘𝐴)))))) |
| 49 | | adddi 11244 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ ∧ 𝐵
∈ ℂ) → (i · (𝐴 + 𝐵)) = ((i · 𝐴) + (i · 𝐵))) |
| 50 | 6, 49 | mp3an1 1450 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· (𝐴 + 𝐵)) = ((i · 𝐴) + (i · 𝐵))) |
| 51 | 50 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(exp‘(i · (𝐴 +
𝐵))) = (exp‘((i
· 𝐴) + (i ·
𝐵)))) |
| 52 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈
ℂ) |
| 53 | | mulcl 11239 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
| 54 | 6, 52, 53 | sylancr 587 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· 𝐴) ∈
ℂ) |
| 55 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈
ℂ) |
| 56 | | mulcl 11239 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ 𝐵
∈ ℂ) → (i · 𝐵) ∈ ℂ) |
| 57 | 6, 55, 56 | sylancr 587 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· 𝐵) ∈
ℂ) |
| 58 | | efadd 16130 |
. . . . . . . 8
⊢ (((i
· 𝐴) ∈ ℂ
∧ (i · 𝐵) ∈
ℂ) → (exp‘((i · 𝐴) + (i · 𝐵))) = ((exp‘(i · 𝐴)) · (exp‘(i
· 𝐵)))) |
| 59 | 54, 57, 58 | syl2anc 584 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(exp‘((i · 𝐴)
+ (i · 𝐵))) =
((exp‘(i · 𝐴))
· (exp‘(i · 𝐵)))) |
| 60 | | efival 16188 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(exp‘(i · 𝐴))
= ((cos‘𝐴) + (i
· (sin‘𝐴)))) |
| 61 | | efival 16188 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℂ →
(exp‘(i · 𝐵))
= ((cos‘𝐵) + (i
· (sin‘𝐵)))) |
| 62 | 60, 61 | oveqan12d 7450 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((exp‘(i · 𝐴))
· (exp‘(i · 𝐵))) = (((cos‘𝐴) + (i · (sin‘𝐴))) · ((cos‘𝐵) + (i · (sin‘𝐵))))) |
| 63 | 9, 34, 16, 31 | muladdd 11721 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((cos‘𝐴) + (i
· (sin‘𝐴)))
· ((cos‘𝐵) +
(i · (sin‘𝐵)))) = ((((cos‘𝐴) · (cos‘𝐵)) + ((i · (sin‘𝐵)) · (i ·
(sin‘𝐴)))) +
(((cos‘𝐴) · (i
· (sin‘𝐵))) +
((cos‘𝐵) · (i
· (sin‘𝐴)))))) |
| 64 | 62, 63 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((exp‘(i · 𝐴))
· (exp‘(i · 𝐵))) = ((((cos‘𝐴) · (cos‘𝐵)) + ((i · (sin‘𝐵)) · (i ·
(sin‘𝐴)))) +
(((cos‘𝐴) · (i
· (sin‘𝐵))) +
((cos‘𝐵) · (i
· (sin‘𝐴)))))) |
| 65 | 51, 59, 64 | 3eqtrd 2781 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(exp‘(i · (𝐴 +
𝐵))) = ((((cos‘𝐴) · (cos‘𝐵)) + ((i ·
(sin‘𝐵)) · (i
· (sin‘𝐴)))) +
(((cos‘𝐴) · (i
· (sin‘𝐵))) +
((cos‘𝐵) · (i
· (sin‘𝐴)))))) |
| 66 | | negicn 11509 |
. . . . . . . . 9
⊢ -i ∈
ℂ |
| 67 | | adddi 11244 |
. . . . . . . . 9
⊢ ((-i
∈ ℂ ∧ 𝐴
∈ ℂ ∧ 𝐵
∈ ℂ) → (-i · (𝐴 + 𝐵)) = ((-i · 𝐴) + (-i · 𝐵))) |
| 68 | 66, 67 | mp3an1 1450 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-i
· (𝐴 + 𝐵)) = ((-i · 𝐴) + (-i · 𝐵))) |
| 69 | 68 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(exp‘(-i · (𝐴
+ 𝐵))) = (exp‘((-i
· 𝐴) + (-i ·
𝐵)))) |
| 70 | | mulcl 11239 |
. . . . . . . . 9
⊢ ((-i
∈ ℂ ∧ 𝐴
∈ ℂ) → (-i · 𝐴) ∈ ℂ) |
| 71 | 66, 52, 70 | sylancr 587 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-i
· 𝐴) ∈
ℂ) |
| 72 | | mulcl 11239 |
. . . . . . . . 9
⊢ ((-i
∈ ℂ ∧ 𝐵
∈ ℂ) → (-i · 𝐵) ∈ ℂ) |
| 73 | 66, 55, 72 | sylancr 587 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-i
· 𝐵) ∈
ℂ) |
| 74 | | efadd 16130 |
. . . . . . . 8
⊢ (((-i
· 𝐴) ∈ ℂ
∧ (-i · 𝐵)
∈ ℂ) → (exp‘((-i · 𝐴) + (-i · 𝐵))) = ((exp‘(-i · 𝐴)) · (exp‘(-i
· 𝐵)))) |
| 75 | 71, 73, 74 | syl2anc 584 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(exp‘((-i · 𝐴)
+ (-i · 𝐵))) =
((exp‘(-i · 𝐴)) · (exp‘(-i · 𝐵)))) |
| 76 | | efmival 16189 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(exp‘(-i · 𝐴))
= ((cos‘𝐴) − (i
· (sin‘𝐴)))) |
| 77 | | efmival 16189 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℂ →
(exp‘(-i · 𝐵))
= ((cos‘𝐵) − (i
· (sin‘𝐵)))) |
| 78 | 76, 77 | oveqan12d 7450 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((exp‘(-i · 𝐴)) · (exp‘(-i · 𝐵))) = (((cos‘𝐴) − (i ·
(sin‘𝐴))) ·
((cos‘𝐵) − (i
· (sin‘𝐵))))) |
| 79 | 9, 34, 16, 31 | mulsubd 11722 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((cos‘𝐴) − (i
· (sin‘𝐴)))
· ((cos‘𝐵)
− (i · (sin‘𝐵)))) = ((((cos‘𝐴) · (cos‘𝐵)) + ((i · (sin‘𝐵)) · (i ·
(sin‘𝐴)))) −
(((cos‘𝐴) · (i
· (sin‘𝐵))) +
((cos‘𝐵) · (i
· (sin‘𝐴)))))) |
| 80 | 78, 79 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((exp‘(-i · 𝐴)) · (exp‘(-i · 𝐵))) = ((((cos‘𝐴) · (cos‘𝐵)) + ((i ·
(sin‘𝐵)) · (i
· (sin‘𝐴))))
− (((cos‘𝐴)
· (i · (sin‘𝐵))) + ((cos‘𝐵) · (i · (sin‘𝐴)))))) |
| 81 | 69, 75, 80 | 3eqtrd 2781 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(exp‘(-i · (𝐴
+ 𝐵))) =
((((cos‘𝐴) ·
(cos‘𝐵)) + ((i
· (sin‘𝐵))
· (i · (sin‘𝐴)))) − (((cos‘𝐴) · (i · (sin‘𝐵))) + ((cos‘𝐵) · (i ·
(sin‘𝐴)))))) |
| 82 | 65, 81 | oveq12d 7449 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((exp‘(i · (𝐴
+ 𝐵))) −
(exp‘(-i · (𝐴
+ 𝐵)))) =
(((((cos‘𝐴) ·
(cos‘𝐵)) + ((i
· (sin‘𝐵))
· (i · (sin‘𝐴)))) + (((cos‘𝐴) · (i · (sin‘𝐵))) + ((cos‘𝐵) · (i ·
(sin‘𝐴))))) −
((((cos‘𝐴) ·
(cos‘𝐵)) + ((i
· (sin‘𝐵))
· (i · (sin‘𝐴)))) − (((cos‘𝐴) · (i · (sin‘𝐵))) + ((cos‘𝐵) · (i ·
(sin‘𝐴))))))) |
| 83 | 36 | 2timesd 12509 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2
· (((cos‘𝐴)
· (i · (sin‘𝐵))) + ((cos‘𝐵) · (i · (sin‘𝐴))))) = ((((cos‘𝐴) · (i ·
(sin‘𝐵))) +
((cos‘𝐵) · (i
· (sin‘𝐴)))) +
(((cos‘𝐴) · (i
· (sin‘𝐵))) +
((cos‘𝐵) · (i
· (sin‘𝐴)))))) |
| 84 | 48, 82, 83 | 3eqtr4d 2787 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((exp‘(i · (𝐴
+ 𝐵))) −
(exp‘(-i · (𝐴
+ 𝐵)))) = (2 ·
(((cos‘𝐴) · (i
· (sin‘𝐵))) +
((cos‘𝐵) · (i
· (sin‘𝐴)))))) |
| 85 | 84 | oveq1d 7446 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((exp‘(i · (𝐴
+ 𝐵))) −
(exp‘(-i · (𝐴
+ 𝐵)))) / (2 · i)) =
((2 · (((cos‘𝐴) · (i · (sin‘𝐵))) + ((cos‘𝐵) · (i ·
(sin‘𝐴))))) / (2
· i))) |
| 86 | 17, 12 | addcomd 11463 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((sin‘𝐴) ·
(cos‘𝐵)) +
((cos‘𝐴) ·
(sin‘𝐵))) =
(((cos‘𝐴) ·
(sin‘𝐵)) +
((sin‘𝐴) ·
(cos‘𝐵)))) |
| 87 | 44, 85, 86 | 3eqtr4d 2787 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((exp‘(i · (𝐴
+ 𝐵))) −
(exp‘(-i · (𝐴
+ 𝐵)))) / (2 · i)) =
(((sin‘𝐴) ·
(cos‘𝐵)) +
((cos‘𝐴) ·
(sin‘𝐵)))) |
| 88 | 3, 87 | eqtrd 2777 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(sin‘(𝐴 + 𝐵)) = (((sin‘𝐴) · (cos‘𝐵)) + ((cos‘𝐴) · (sin‘𝐵)))) |