Proof of Theorem cosadd
| Step | Hyp | Ref
| Expression |
| 1 | | addcl 11237 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
| 2 | | cosval 16159 |
. . 3
⊢ ((𝐴 + 𝐵) ∈ ℂ → (cos‘(𝐴 + 𝐵)) = (((exp‘(i · (𝐴 + 𝐵))) + (exp‘(-i · (𝐴 + 𝐵)))) / 2)) |
| 3 | 1, 2 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(cos‘(𝐴 + 𝐵)) = (((exp‘(i ·
(𝐴 + 𝐵))) + (exp‘(-i · (𝐴 + 𝐵)))) / 2)) |
| 4 | | coscl 16163 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(cos‘𝐴) ∈
ℂ) |
| 5 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(cos‘𝐴) ∈
ℂ) |
| 6 | | coscl 16163 |
. . . . . . . 8
⊢ (𝐵 ∈ ℂ →
(cos‘𝐵) ∈
ℂ) |
| 7 | 6 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(cos‘𝐵) ∈
ℂ) |
| 8 | 5, 7 | mulcld 11281 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((cos‘𝐴) ·
(cos‘𝐵)) ∈
ℂ) |
| 9 | | ax-icn 11214 |
. . . . . . . 8
⊢ i ∈
ℂ |
| 10 | | sincl 16162 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℂ →
(sin‘𝐵) ∈
ℂ) |
| 11 | 10 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(sin‘𝐵) ∈
ℂ) |
| 12 | | mulcl 11239 |
. . . . . . . 8
⊢ ((i
∈ ℂ ∧ (sin‘𝐵) ∈ ℂ) → (i ·
(sin‘𝐵)) ∈
ℂ) |
| 13 | 9, 11, 12 | sylancr 587 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· (sin‘𝐵))
∈ ℂ) |
| 14 | | sincl 16162 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(sin‘𝐴) ∈
ℂ) |
| 15 | 14 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(sin‘𝐴) ∈
ℂ) |
| 16 | | mulcl 11239 |
. . . . . . . 8
⊢ ((i
∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i ·
(sin‘𝐴)) ∈
ℂ) |
| 17 | 9, 15, 16 | sylancr 587 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· (sin‘𝐴))
∈ ℂ) |
| 18 | 13, 17 | mulcld 11281 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((i
· (sin‘𝐵))
· (i · (sin‘𝐴))) ∈ ℂ) |
| 19 | 8, 18 | addcld 11280 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((cos‘𝐴) ·
(cos‘𝐵)) + ((i
· (sin‘𝐵))
· (i · (sin‘𝐴)))) ∈ ℂ) |
| 20 | 5, 13 | mulcld 11281 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((cos‘𝐴) · (i
· (sin‘𝐵)))
∈ ℂ) |
| 21 | 7, 17 | mulcld 11281 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((cos‘𝐵) · (i
· (sin‘𝐴)))
∈ ℂ) |
| 22 | 20, 21 | addcld 11280 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((cos‘𝐴) · (i
· (sin‘𝐵))) +
((cos‘𝐵) · (i
· (sin‘𝐴))))
∈ ℂ) |
| 23 | 19, 22, 19 | ppncand 11660 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((((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‘𝐴) ·
(cos‘𝐵)) + ((i
· (sin‘𝐵))
· (i · (sin‘𝐴)))) + (((cos‘𝐴) · (cos‘𝐵)) + ((i · (sin‘𝐵)) · (i ·
(sin‘𝐴)))))) |
| 24 | | adddi 11244 |
. . . . . . . 8
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ ∧ 𝐵
∈ ℂ) → (i · (𝐴 + 𝐵)) = ((i · 𝐴) + (i · 𝐵))) |
| 25 | 9, 24 | mp3an1 1450 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· (𝐴 + 𝐵)) = ((i · 𝐴) + (i · 𝐵))) |
| 26 | 25 | fveq2d 6910 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(exp‘(i · (𝐴 +
𝐵))) = (exp‘((i
· 𝐴) + (i ·
𝐵)))) |
| 27 | | simpl 482 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈
ℂ) |
| 28 | | mulcl 11239 |
. . . . . . . 8
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
| 29 | 9, 27, 28 | sylancr 587 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· 𝐴) ∈
ℂ) |
| 30 | | simpr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈
ℂ) |
| 31 | | mulcl 11239 |
. . . . . . . 8
⊢ ((i
∈ ℂ ∧ 𝐵
∈ ℂ) → (i · 𝐵) ∈ ℂ) |
| 32 | 9, 30, 31 | sylancr 587 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· 𝐵) ∈
ℂ) |
| 33 | | efadd 16130 |
. . . . . . 7
⊢ (((i
· 𝐴) ∈ ℂ
∧ (i · 𝐵) ∈
ℂ) → (exp‘((i · 𝐴) + (i · 𝐵))) = ((exp‘(i · 𝐴)) · (exp‘(i
· 𝐵)))) |
| 34 | 29, 32, 33 | syl2anc 584 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(exp‘((i · 𝐴)
+ (i · 𝐵))) =
((exp‘(i · 𝐴))
· (exp‘(i · 𝐵)))) |
| 35 | | efival 16188 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(exp‘(i · 𝐴))
= ((cos‘𝐴) + (i
· (sin‘𝐴)))) |
| 36 | | efival 16188 |
. . . . . . . 8
⊢ (𝐵 ∈ ℂ →
(exp‘(i · 𝐵))
= ((cos‘𝐵) + (i
· (sin‘𝐵)))) |
| 37 | 35, 36 | oveqan12d 7450 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((exp‘(i · 𝐴))
· (exp‘(i · 𝐵))) = (((cos‘𝐴) + (i · (sin‘𝐴))) · ((cos‘𝐵) + (i · (sin‘𝐵))))) |
| 38 | 5, 17, 7, 13 | muladdd 11721 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((cos‘𝐴) + (i
· (sin‘𝐴)))
· ((cos‘𝐵) +
(i · (sin‘𝐵)))) = ((((cos‘𝐴) · (cos‘𝐵)) + ((i · (sin‘𝐵)) · (i ·
(sin‘𝐴)))) +
(((cos‘𝐴) · (i
· (sin‘𝐵))) +
((cos‘𝐵) · (i
· (sin‘𝐴)))))) |
| 39 | 37, 38 | eqtrd 2777 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((exp‘(i · 𝐴))
· (exp‘(i · 𝐵))) = ((((cos‘𝐴) · (cos‘𝐵)) + ((i · (sin‘𝐵)) · (i ·
(sin‘𝐴)))) +
(((cos‘𝐴) · (i
· (sin‘𝐵))) +
((cos‘𝐵) · (i
· (sin‘𝐴)))))) |
| 40 | 26, 34, 39 | 3eqtrd 2781 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(exp‘(i · (𝐴 +
𝐵))) = ((((cos‘𝐴) · (cos‘𝐵)) + ((i ·
(sin‘𝐵)) · (i
· (sin‘𝐴)))) +
(((cos‘𝐴) · (i
· (sin‘𝐵))) +
((cos‘𝐵) · (i
· (sin‘𝐴)))))) |
| 41 | | negicn 11509 |
. . . . . . . 8
⊢ -i ∈
ℂ |
| 42 | | adddi 11244 |
. . . . . . . 8
⊢ ((-i
∈ ℂ ∧ 𝐴
∈ ℂ ∧ 𝐵
∈ ℂ) → (-i · (𝐴 + 𝐵)) = ((-i · 𝐴) + (-i · 𝐵))) |
| 43 | 41, 42 | mp3an1 1450 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-i
· (𝐴 + 𝐵)) = ((-i · 𝐴) + (-i · 𝐵))) |
| 44 | 43 | fveq2d 6910 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(exp‘(-i · (𝐴
+ 𝐵))) = (exp‘((-i
· 𝐴) + (-i ·
𝐵)))) |
| 45 | | mulcl 11239 |
. . . . . . . 8
⊢ ((-i
∈ ℂ ∧ 𝐴
∈ ℂ) → (-i · 𝐴) ∈ ℂ) |
| 46 | 41, 27, 45 | sylancr 587 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-i
· 𝐴) ∈
ℂ) |
| 47 | | mulcl 11239 |
. . . . . . . 8
⊢ ((-i
∈ ℂ ∧ 𝐵
∈ ℂ) → (-i · 𝐵) ∈ ℂ) |
| 48 | 41, 30, 47 | sylancr 587 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-i
· 𝐵) ∈
ℂ) |
| 49 | | efadd 16130 |
. . . . . . 7
⊢ (((-i
· 𝐴) ∈ ℂ
∧ (-i · 𝐵)
∈ ℂ) → (exp‘((-i · 𝐴) + (-i · 𝐵))) = ((exp‘(-i · 𝐴)) · (exp‘(-i
· 𝐵)))) |
| 50 | 46, 48, 49 | syl2anc 584 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(exp‘((-i · 𝐴)
+ (-i · 𝐵))) =
((exp‘(-i · 𝐴)) · (exp‘(-i · 𝐵)))) |
| 51 | | efmival 16189 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(exp‘(-i · 𝐴))
= ((cos‘𝐴) − (i
· (sin‘𝐴)))) |
| 52 | | efmival 16189 |
. . . . . . . 8
⊢ (𝐵 ∈ ℂ →
(exp‘(-i · 𝐵))
= ((cos‘𝐵) − (i
· (sin‘𝐵)))) |
| 53 | 51, 52 | oveqan12d 7450 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((exp‘(-i · 𝐴)) · (exp‘(-i · 𝐵))) = (((cos‘𝐴) − (i ·
(sin‘𝐴))) ·
((cos‘𝐵) − (i
· (sin‘𝐵))))) |
| 54 | 5, 17, 7, 13 | mulsubd 11722 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((cos‘𝐴) − (i
· (sin‘𝐴)))
· ((cos‘𝐵)
− (i · (sin‘𝐵)))) = ((((cos‘𝐴) · (cos‘𝐵)) + ((i · (sin‘𝐵)) · (i ·
(sin‘𝐴)))) −
(((cos‘𝐴) · (i
· (sin‘𝐵))) +
((cos‘𝐵) · (i
· (sin‘𝐴)))))) |
| 55 | 53, 54 | eqtrd 2777 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((exp‘(-i · 𝐴)) · (exp‘(-i · 𝐵))) = ((((cos‘𝐴) · (cos‘𝐵)) + ((i ·
(sin‘𝐵)) · (i
· (sin‘𝐴))))
− (((cos‘𝐴)
· (i · (sin‘𝐵))) + ((cos‘𝐵) · (i · (sin‘𝐴)))))) |
| 56 | 44, 50, 55 | 3eqtrd 2781 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(exp‘(-i · (𝐴
+ 𝐵))) =
((((cos‘𝐴) ·
(cos‘𝐵)) + ((i
· (sin‘𝐵))
· (i · (sin‘𝐴)))) − (((cos‘𝐴) · (i · (sin‘𝐵))) + ((cos‘𝐵) · (i ·
(sin‘𝐴)))))) |
| 57 | 40, 56 | oveq12d 7449 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((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‘𝐴))))))) |
| 58 | 19 | 2timesd 12509 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2
· (((cos‘𝐴)
· (cos‘𝐵)) +
((i · (sin‘𝐵))
· (i · (sin‘𝐴))))) = ((((cos‘𝐴) · (cos‘𝐵)) + ((i · (sin‘𝐵)) · (i ·
(sin‘𝐴)))) +
(((cos‘𝐴) ·
(cos‘𝐵)) + ((i
· (sin‘𝐵))
· (i · (sin‘𝐴)))))) |
| 59 | 23, 57, 58 | 3eqtr4d 2787 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((exp‘(i · (𝐴
+ 𝐵))) + (exp‘(-i
· (𝐴 + 𝐵)))) = (2 ·
(((cos‘𝐴) ·
(cos‘𝐵)) + ((i
· (sin‘𝐵))
· (i · (sin‘𝐴)))))) |
| 60 | 59 | oveq1d 7446 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((exp‘(i · (𝐴
+ 𝐵))) + (exp‘(-i
· (𝐴 + 𝐵)))) / 2) = ((2 ·
(((cos‘𝐴) ·
(cos‘𝐵)) + ((i
· (sin‘𝐵))
· (i · (sin‘𝐴))))) / 2)) |
| 61 | | 2cn 12341 |
. . . . 5
⊢ 2 ∈
ℂ |
| 62 | | 2ne0 12370 |
. . . . 5
⊢ 2 ≠
0 |
| 63 | | divcan3 11948 |
. . . . 5
⊢
(((((cos‘𝐴)
· (cos‘𝐵)) +
((i · (sin‘𝐵))
· (i · (sin‘𝐴)))) ∈ ℂ ∧ 2 ∈ ℂ
∧ 2 ≠ 0) → ((2 · (((cos‘𝐴) · (cos‘𝐵)) + ((i · (sin‘𝐵)) · (i ·
(sin‘𝐴))))) / 2) =
(((cos‘𝐴) ·
(cos‘𝐵)) + ((i
· (sin‘𝐵))
· (i · (sin‘𝐴))))) |
| 64 | 61, 62, 63 | mp3an23 1455 |
. . . 4
⊢
((((cos‘𝐴)
· (cos‘𝐵)) +
((i · (sin‘𝐵))
· (i · (sin‘𝐴)))) ∈ ℂ → ((2 ·
(((cos‘𝐴) ·
(cos‘𝐵)) + ((i
· (sin‘𝐵))
· (i · (sin‘𝐴))))) / 2) = (((cos‘𝐴) · (cos‘𝐵)) + ((i · (sin‘𝐵)) · (i ·
(sin‘𝐴))))) |
| 65 | 19, 64 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((2
· (((cos‘𝐴)
· (cos‘𝐵)) +
((i · (sin‘𝐵))
· (i · (sin‘𝐴))))) / 2) = (((cos‘𝐴) · (cos‘𝐵)) + ((i · (sin‘𝐵)) · (i ·
(sin‘𝐴))))) |
| 66 | 9 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → i ∈
ℂ) |
| 67 | 66, 11, 66, 15 | mul4d 11473 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((i
· (sin‘𝐵))
· (i · (sin‘𝐴))) = ((i · i) ·
((sin‘𝐵) ·
(sin‘𝐴)))) |
| 68 | | ixi 11892 |
. . . . . . 7
⊢ (i
· i) = -1 |
| 69 | 68 | oveq1i 7441 |
. . . . . 6
⊢ ((i
· i) · ((sin‘𝐵) · (sin‘𝐴))) = (-1 · ((sin‘𝐵) · (sin‘𝐴))) |
| 70 | 11, 15 | mulcomd 11282 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((sin‘𝐵) ·
(sin‘𝐴)) =
((sin‘𝐴) ·
(sin‘𝐵))) |
| 71 | 70 | oveq2d 7447 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-1
· ((sin‘𝐵)
· (sin‘𝐴))) =
(-1 · ((sin‘𝐴)
· (sin‘𝐵)))) |
| 72 | 69, 71 | eqtrid 2789 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((i
· i) · ((sin‘𝐵) · (sin‘𝐴))) = (-1 · ((sin‘𝐴) · (sin‘𝐵)))) |
| 73 | 15, 11 | mulcld 11281 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((sin‘𝐴) ·
(sin‘𝐵)) ∈
ℂ) |
| 74 | 73 | mulm1d 11715 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-1
· ((sin‘𝐴)
· (sin‘𝐵))) =
-((sin‘𝐴) ·
(sin‘𝐵))) |
| 75 | 67, 72, 74 | 3eqtrd 2781 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((i
· (sin‘𝐵))
· (i · (sin‘𝐴))) = -((sin‘𝐴) · (sin‘𝐵))) |
| 76 | 75 | oveq2d 7447 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((cos‘𝐴) ·
(cos‘𝐵)) + ((i
· (sin‘𝐵))
· (i · (sin‘𝐴)))) = (((cos‘𝐴) · (cos‘𝐵)) + -((sin‘𝐴) · (sin‘𝐵)))) |
| 77 | 8, 73 | negsubd 11626 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((cos‘𝐴) ·
(cos‘𝐵)) +
-((sin‘𝐴) ·
(sin‘𝐵))) =
(((cos‘𝐴) ·
(cos‘𝐵)) −
((sin‘𝐴) ·
(sin‘𝐵)))) |
| 78 | 65, 76, 77 | 3eqtrd 2781 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((2
· (((cos‘𝐴)
· (cos‘𝐵)) +
((i · (sin‘𝐵))
· (i · (sin‘𝐴))))) / 2) = (((cos‘𝐴) · (cos‘𝐵)) − ((sin‘𝐴) · (sin‘𝐵)))) |
| 79 | 3, 60, 78 | 3eqtrd 2781 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(cos‘(𝐴 + 𝐵)) = (((cos‘𝐴) · (cos‘𝐵)) − ((sin‘𝐴) · (sin‘𝐵)))) |