Proof of Theorem cosadd
Step | Hyp | Ref
| Expression |
1 | | addcl 10937 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
2 | | cosval 15813 |
. . 3
⊢ ((𝐴 + 𝐵) ∈ ℂ → (cos‘(𝐴 + 𝐵)) = (((exp‘(i · (𝐴 + 𝐵))) + (exp‘(-i · (𝐴 + 𝐵)))) / 2)) |
3 | 1, 2 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(cos‘(𝐴 + 𝐵)) = (((exp‘(i ·
(𝐴 + 𝐵))) + (exp‘(-i · (𝐴 + 𝐵)))) / 2)) |
4 | | coscl 15817 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(cos‘𝐴) ∈
ℂ) |
5 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(cos‘𝐴) ∈
ℂ) |
6 | | coscl 15817 |
. . . . . . . 8
⊢ (𝐵 ∈ ℂ →
(cos‘𝐵) ∈
ℂ) |
7 | 6 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(cos‘𝐵) ∈
ℂ) |
8 | 5, 7 | mulcld 10979 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((cos‘𝐴) ·
(cos‘𝐵)) ∈
ℂ) |
9 | | ax-icn 10914 |
. . . . . . . 8
⊢ i ∈
ℂ |
10 | | sincl 15816 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℂ →
(sin‘𝐵) ∈
ℂ) |
11 | 10 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(sin‘𝐵) ∈
ℂ) |
12 | | mulcl 10939 |
. . . . . . . 8
⊢ ((i
∈ ℂ ∧ (sin‘𝐵) ∈ ℂ) → (i ·
(sin‘𝐵)) ∈
ℂ) |
13 | 9, 11, 12 | sylancr 586 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· (sin‘𝐵))
∈ ℂ) |
14 | | sincl 15816 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(sin‘𝐴) ∈
ℂ) |
15 | 14 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(sin‘𝐴) ∈
ℂ) |
16 | | mulcl 10939 |
. . . . . . . 8
⊢ ((i
∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i ·
(sin‘𝐴)) ∈
ℂ) |
17 | 9, 15, 16 | sylancr 586 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· (sin‘𝐴))
∈ ℂ) |
18 | 13, 17 | mulcld 10979 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((i
· (sin‘𝐵))
· (i · (sin‘𝐴))) ∈ ℂ) |
19 | 8, 18 | addcld 10978 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((cos‘𝐴) ·
(cos‘𝐵)) + ((i
· (sin‘𝐵))
· (i · (sin‘𝐴)))) ∈ ℂ) |
20 | 5, 13 | mulcld 10979 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((cos‘𝐴) · (i
· (sin‘𝐵)))
∈ ℂ) |
21 | 7, 17 | mulcld 10979 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((cos‘𝐵) · (i
· (sin‘𝐴)))
∈ ℂ) |
22 | 20, 21 | addcld 10978 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((cos‘𝐴) · (i
· (sin‘𝐵))) +
((cos‘𝐵) · (i
· (sin‘𝐴))))
∈ ℂ) |
23 | 19, 22, 19 | ppncand 11355 |
. . . 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 10944 |
. . . . . . . 8
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ ∧ 𝐵
∈ ℂ) → (i · (𝐴 + 𝐵)) = ((i · 𝐴) + (i · 𝐵))) |
25 | 9, 24 | mp3an1 1446 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· (𝐴 + 𝐵)) = ((i · 𝐴) + (i · 𝐵))) |
26 | 25 | fveq2d 6772 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(exp‘(i · (𝐴 +
𝐵))) = (exp‘((i
· 𝐴) + (i ·
𝐵)))) |
27 | | simpl 482 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐴 ∈
ℂ) |
28 | | mulcl 10939 |
. . . . . . . 8
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
29 | 9, 27, 28 | sylancr 586 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· 𝐴) ∈
ℂ) |
30 | | simpr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈
ℂ) |
31 | | mulcl 10939 |
. . . . . . . 8
⊢ ((i
∈ ℂ ∧ 𝐵
∈ ℂ) → (i · 𝐵) ∈ ℂ) |
32 | 9, 30, 31 | sylancr 586 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· 𝐵) ∈
ℂ) |
33 | | efadd 15784 |
. . . . . . 7
⊢ (((i
· 𝐴) ∈ ℂ
∧ (i · 𝐵) ∈
ℂ) → (exp‘((i · 𝐴) + (i · 𝐵))) = ((exp‘(i · 𝐴)) · (exp‘(i
· 𝐵)))) |
34 | 29, 32, 33 | syl2anc 583 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(exp‘((i · 𝐴)
+ (i · 𝐵))) =
((exp‘(i · 𝐴))
· (exp‘(i · 𝐵)))) |
35 | | efival 15842 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(exp‘(i · 𝐴))
= ((cos‘𝐴) + (i
· (sin‘𝐴)))) |
36 | | efival 15842 |
. . . . . . . 8
⊢ (𝐵 ∈ ℂ →
(exp‘(i · 𝐵))
= ((cos‘𝐵) + (i
· (sin‘𝐵)))) |
37 | 35, 36 | oveqan12d 7287 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((exp‘(i · 𝐴))
· (exp‘(i · 𝐵))) = (((cos‘𝐴) + (i · (sin‘𝐴))) · ((cos‘𝐵) + (i · (sin‘𝐵))))) |
38 | 5, 17, 7, 13 | muladdd 11416 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((cos‘𝐴) + (i
· (sin‘𝐴)))
· ((cos‘𝐵) +
(i · (sin‘𝐵)))) = ((((cos‘𝐴) · (cos‘𝐵)) + ((i · (sin‘𝐵)) · (i ·
(sin‘𝐴)))) +
(((cos‘𝐴) · (i
· (sin‘𝐵))) +
((cos‘𝐵) · (i
· (sin‘𝐴)))))) |
39 | 37, 38 | eqtrd 2779 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((exp‘(i · 𝐴))
· (exp‘(i · 𝐵))) = ((((cos‘𝐴) · (cos‘𝐵)) + ((i · (sin‘𝐵)) · (i ·
(sin‘𝐴)))) +
(((cos‘𝐴) · (i
· (sin‘𝐵))) +
((cos‘𝐵) · (i
· (sin‘𝐴)))))) |
40 | 26, 34, 39 | 3eqtrd 2783 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(exp‘(i · (𝐴 +
𝐵))) = ((((cos‘𝐴) · (cos‘𝐵)) + ((i ·
(sin‘𝐵)) · (i
· (sin‘𝐴)))) +
(((cos‘𝐴) · (i
· (sin‘𝐵))) +
((cos‘𝐵) · (i
· (sin‘𝐴)))))) |
41 | | negicn 11205 |
. . . . . . . 8
⊢ -i ∈
ℂ |
42 | | adddi 10944 |
. . . . . . . 8
⊢ ((-i
∈ ℂ ∧ 𝐴
∈ ℂ ∧ 𝐵
∈ ℂ) → (-i · (𝐴 + 𝐵)) = ((-i · 𝐴) + (-i · 𝐵))) |
43 | 41, 42 | mp3an1 1446 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-i
· (𝐴 + 𝐵)) = ((-i · 𝐴) + (-i · 𝐵))) |
44 | 43 | fveq2d 6772 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(exp‘(-i · (𝐴
+ 𝐵))) = (exp‘((-i
· 𝐴) + (-i ·
𝐵)))) |
45 | | mulcl 10939 |
. . . . . . . 8
⊢ ((-i
∈ ℂ ∧ 𝐴
∈ ℂ) → (-i · 𝐴) ∈ ℂ) |
46 | 41, 27, 45 | sylancr 586 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-i
· 𝐴) ∈
ℂ) |
47 | | mulcl 10939 |
. . . . . . . 8
⊢ ((-i
∈ ℂ ∧ 𝐵
∈ ℂ) → (-i · 𝐵) ∈ ℂ) |
48 | 41, 30, 47 | sylancr 586 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-i
· 𝐵) ∈
ℂ) |
49 | | efadd 15784 |
. . . . . . 7
⊢ (((-i
· 𝐴) ∈ ℂ
∧ (-i · 𝐵)
∈ ℂ) → (exp‘((-i · 𝐴) + (-i · 𝐵))) = ((exp‘(-i · 𝐴)) · (exp‘(-i
· 𝐵)))) |
50 | 46, 48, 49 | syl2anc 583 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(exp‘((-i · 𝐴)
+ (-i · 𝐵))) =
((exp‘(-i · 𝐴)) · (exp‘(-i · 𝐵)))) |
51 | | efmival 15843 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(exp‘(-i · 𝐴))
= ((cos‘𝐴) − (i
· (sin‘𝐴)))) |
52 | | efmival 15843 |
. . . . . . . 8
⊢ (𝐵 ∈ ℂ →
(exp‘(-i · 𝐵))
= ((cos‘𝐵) − (i
· (sin‘𝐵)))) |
53 | 51, 52 | oveqan12d 7287 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((exp‘(-i · 𝐴)) · (exp‘(-i · 𝐵))) = (((cos‘𝐴) − (i ·
(sin‘𝐴))) ·
((cos‘𝐵) − (i
· (sin‘𝐵))))) |
54 | 5, 17, 7, 13 | mulsubd 11417 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((cos‘𝐴) − (i
· (sin‘𝐴)))
· ((cos‘𝐵)
− (i · (sin‘𝐵)))) = ((((cos‘𝐴) · (cos‘𝐵)) + ((i · (sin‘𝐵)) · (i ·
(sin‘𝐴)))) −
(((cos‘𝐴) · (i
· (sin‘𝐵))) +
((cos‘𝐵) · (i
· (sin‘𝐴)))))) |
55 | 53, 54 | eqtrd 2779 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((exp‘(-i · 𝐴)) · (exp‘(-i · 𝐵))) = ((((cos‘𝐴) · (cos‘𝐵)) + ((i ·
(sin‘𝐵)) · (i
· (sin‘𝐴))))
− (((cos‘𝐴)
· (i · (sin‘𝐵))) + ((cos‘𝐵) · (i · (sin‘𝐴)))))) |
56 | 44, 50, 55 | 3eqtrd 2783 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(exp‘(-i · (𝐴
+ 𝐵))) =
((((cos‘𝐴) ·
(cos‘𝐵)) + ((i
· (sin‘𝐵))
· (i · (sin‘𝐴)))) − (((cos‘𝐴) · (i · (sin‘𝐵))) + ((cos‘𝐵) · (i ·
(sin‘𝐴)))))) |
57 | 40, 56 | oveq12d 7286 |
. . . 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 12199 |
. . . 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 2789 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((exp‘(i · (𝐴
+ 𝐵))) + (exp‘(-i
· (𝐴 + 𝐵)))) = (2 ·
(((cos‘𝐴) ·
(cos‘𝐵)) + ((i
· (sin‘𝐵))
· (i · (sin‘𝐴)))))) |
60 | 59 | oveq1d 7283 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((exp‘(i · (𝐴
+ 𝐵))) + (exp‘(-i
· (𝐴 + 𝐵)))) / 2) = ((2 ·
(((cos‘𝐴) ·
(cos‘𝐵)) + ((i
· (sin‘𝐵))
· (i · (sin‘𝐴))))) / 2)) |
61 | | 2cn 12031 |
. . . . 5
⊢ 2 ∈
ℂ |
62 | | 2ne0 12060 |
. . . . 5
⊢ 2 ≠
0 |
63 | | divcan3 11642 |
. . . . 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 1451 |
. . . 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 11170 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((i
· (sin‘𝐵))
· (i · (sin‘𝐴))) = ((i · i) ·
((sin‘𝐵) ·
(sin‘𝐴)))) |
68 | | ixi 11587 |
. . . . . . 7
⊢ (i
· i) = -1 |
69 | 68 | oveq1i 7278 |
. . . . . 6
⊢ ((i
· i) · ((sin‘𝐵) · (sin‘𝐴))) = (-1 · ((sin‘𝐵) · (sin‘𝐴))) |
70 | 11, 15 | mulcomd 10980 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((sin‘𝐵) ·
(sin‘𝐴)) =
((sin‘𝐴) ·
(sin‘𝐵))) |
71 | 70 | oveq2d 7284 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-1
· ((sin‘𝐵)
· (sin‘𝐴))) =
(-1 · ((sin‘𝐴)
· (sin‘𝐵)))) |
72 | 69, 71 | eqtrid 2791 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((i
· i) · ((sin‘𝐵) · (sin‘𝐴))) = (-1 · ((sin‘𝐴) · (sin‘𝐵)))) |
73 | 15, 11 | mulcld 10979 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((sin‘𝐴) ·
(sin‘𝐵)) ∈
ℂ) |
74 | 73 | mulm1d 11410 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-1
· ((sin‘𝐴)
· (sin‘𝐵))) =
-((sin‘𝐴) ·
(sin‘𝐵))) |
75 | 67, 72, 74 | 3eqtrd 2783 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((i
· (sin‘𝐵))
· (i · (sin‘𝐴))) = -((sin‘𝐴) · (sin‘𝐵))) |
76 | 75 | oveq2d 7284 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((cos‘𝐴) ·
(cos‘𝐵)) + ((i
· (sin‘𝐵))
· (i · (sin‘𝐴)))) = (((cos‘𝐴) · (cos‘𝐵)) + -((sin‘𝐴) · (sin‘𝐵)))) |
77 | 8, 73 | negsubd 11321 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((cos‘𝐴) ·
(cos‘𝐵)) +
-((sin‘𝐴) ·
(sin‘𝐵))) =
(((cos‘𝐴) ·
(cos‘𝐵)) −
((sin‘𝐴) ·
(sin‘𝐵)))) |
78 | 65, 76, 77 | 3eqtrd 2783 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((2
· (((cos‘𝐴)
· (cos‘𝐵)) +
((i · (sin‘𝐵))
· (i · (sin‘𝐴))))) / 2) = (((cos‘𝐴) · (cos‘𝐵)) − ((sin‘𝐴) · (sin‘𝐵)))) |
79 | 3, 60, 78 | 3eqtrd 2783 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(cos‘(𝐴 + 𝐵)) = (((cos‘𝐴) · (cos‘𝐵)) − ((sin‘𝐴) · (sin‘𝐵)))) |