Proof of Theorem addsin
Step | Hyp | Ref
| Expression |
1 | | addcl 7852 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
2 | 1 | halfcld 9072 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) / 2) ∈ ℂ) |
3 | 2 | sincld 11602 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(sin‘((𝐴 + 𝐵) / 2)) ∈
ℂ) |
4 | | subcl 8069 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ) |
5 | 4 | halfcld 9072 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) / 2) ∈ ℂ) |
6 | 5 | coscld 11603 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(cos‘((𝐴 −
𝐵) / 2)) ∈
ℂ) |
7 | 3, 6 | mulcld 7893 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((sin‘((𝐴 + 𝐵) / 2)) ·
(cos‘((𝐴 −
𝐵) / 2))) ∈
ℂ) |
8 | 7 | 2timesd 9070 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (2
· ((sin‘((𝐴 +
𝐵) / 2)) ·
(cos‘((𝐴 −
𝐵) / 2)))) =
(((sin‘((𝐴 + 𝐵) / 2)) ·
(cos‘((𝐴 −
𝐵) / 2))) +
((sin‘((𝐴 + 𝐵) / 2)) ·
(cos‘((𝐴 −
𝐵) /
2))))) |
9 | | sinadd 11628 |
. . . . 5
⊢ ((((𝐴 + 𝐵) / 2) ∈ ℂ ∧ ((𝐴 − 𝐵) / 2) ∈ ℂ) →
(sin‘(((𝐴 + 𝐵) / 2) + ((𝐴 − 𝐵) / 2))) = (((sin‘((𝐴 + 𝐵) / 2)) · (cos‘((𝐴 − 𝐵) / 2))) + ((cos‘((𝐴 + 𝐵) / 2)) · (sin‘((𝐴 − 𝐵) / 2))))) |
10 | 2, 5, 9 | syl2anc 409 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(sin‘(((𝐴 + 𝐵) / 2) + ((𝐴 − 𝐵) / 2))) = (((sin‘((𝐴 + 𝐵) / 2)) · (cos‘((𝐴 − 𝐵) / 2))) + ((cos‘((𝐴 + 𝐵) / 2)) · (sin‘((𝐴 − 𝐵) / 2))))) |
11 | | sinsub 11632 |
. . . . 5
⊢ ((((𝐴 + 𝐵) / 2) ∈ ℂ ∧ ((𝐴 − 𝐵) / 2) ∈ ℂ) →
(sin‘(((𝐴 + 𝐵) / 2) − ((𝐴 − 𝐵) / 2))) = (((sin‘((𝐴 + 𝐵) / 2)) · (cos‘((𝐴 − 𝐵) / 2))) − ((cos‘((𝐴 + 𝐵) / 2)) · (sin‘((𝐴 − 𝐵) / 2))))) |
12 | 2, 5, 11 | syl2anc 409 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(sin‘(((𝐴 + 𝐵) / 2) − ((𝐴 − 𝐵) / 2))) = (((sin‘((𝐴 + 𝐵) / 2)) · (cos‘((𝐴 − 𝐵) / 2))) − ((cos‘((𝐴 + 𝐵) / 2)) · (sin‘((𝐴 − 𝐵) / 2))))) |
13 | 10, 12 | oveq12d 5839 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((sin‘(((𝐴 + 𝐵) / 2) + ((𝐴 − 𝐵) / 2))) + (sin‘(((𝐴 + 𝐵) / 2) − ((𝐴 − 𝐵) / 2)))) = ((((sin‘((𝐴 + 𝐵) / 2)) · (cos‘((𝐴 − 𝐵) / 2))) + ((cos‘((𝐴 + 𝐵) / 2)) · (sin‘((𝐴 − 𝐵) / 2)))) + (((sin‘((𝐴 + 𝐵) / 2)) · (cos‘((𝐴 − 𝐵) / 2))) − ((cos‘((𝐴 + 𝐵) / 2)) · (sin‘((𝐴 − 𝐵) / 2)))))) |
14 | 2 | coscld 11603 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(cos‘((𝐴 + 𝐵) / 2)) ∈
ℂ) |
15 | 5 | sincld 11602 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(sin‘((𝐴 −
𝐵) / 2)) ∈
ℂ) |
16 | 14, 15 | mulcld 7893 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((cos‘((𝐴 + 𝐵) / 2)) ·
(sin‘((𝐴 −
𝐵) / 2))) ∈
ℂ) |
17 | 7, 16, 7 | ppncand 8221 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((((sin‘((𝐴 + 𝐵) / 2)) ·
(cos‘((𝐴 −
𝐵) / 2))) +
((cos‘((𝐴 + 𝐵) / 2)) ·
(sin‘((𝐴 −
𝐵) / 2)))) +
(((sin‘((𝐴 + 𝐵) / 2)) ·
(cos‘((𝐴 −
𝐵) / 2))) −
((cos‘((𝐴 + 𝐵) / 2)) ·
(sin‘((𝐴 −
𝐵) / 2))))) =
(((sin‘((𝐴 + 𝐵) / 2)) ·
(cos‘((𝐴 −
𝐵) / 2))) +
((sin‘((𝐴 + 𝐵) / 2)) ·
(cos‘((𝐴 −
𝐵) /
2))))) |
18 | 13, 17 | eqtrd 2190 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((sin‘(((𝐴 + 𝐵) / 2) + ((𝐴 − 𝐵) / 2))) + (sin‘(((𝐴 + 𝐵) / 2) − ((𝐴 − 𝐵) / 2)))) = (((sin‘((𝐴 + 𝐵) / 2)) · (cos‘((𝐴 − 𝐵) / 2))) + ((sin‘((𝐴 + 𝐵) / 2)) · (cos‘((𝐴 − 𝐵) / 2))))) |
19 | | halfaddsub 9062 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((((𝐴 + 𝐵) / 2) + ((𝐴 − 𝐵) / 2)) = 𝐴 ∧ (((𝐴 + 𝐵) / 2) − ((𝐴 − 𝐵) / 2)) = 𝐵)) |
20 | 19 | simpld 111 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵) / 2) + ((𝐴 − 𝐵) / 2)) = 𝐴) |
21 | 20 | fveq2d 5471 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(sin‘(((𝐴 + 𝐵) / 2) + ((𝐴 − 𝐵) / 2))) = (sin‘𝐴)) |
22 | 19 | simprd 113 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵) / 2) − ((𝐴 − 𝐵) / 2)) = 𝐵) |
23 | 22 | fveq2d 5471 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(sin‘(((𝐴 + 𝐵) / 2) − ((𝐴 − 𝐵) / 2))) = (sin‘𝐵)) |
24 | 21, 23 | oveq12d 5839 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((sin‘(((𝐴 + 𝐵) / 2) + ((𝐴 − 𝐵) / 2))) + (sin‘(((𝐴 + 𝐵) / 2) − ((𝐴 − 𝐵) / 2)))) = ((sin‘𝐴) + (sin‘𝐵))) |
25 | 8, 18, 24 | 3eqtr2rd 2197 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((sin‘𝐴) +
(sin‘𝐵)) = (2
· ((sin‘((𝐴 +
𝐵) / 2)) ·
(cos‘((𝐴 −
𝐵) /
2))))) |