Step |
Hyp |
Ref |
Expression |
1 |
|
addcl |
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC ) |
2 |
|
cosval |
|- ( ( A + B ) e. CC -> ( cos ` ( A + B ) ) = ( ( ( exp ` ( _i x. ( A + B ) ) ) + ( exp ` ( -u _i x. ( A + B ) ) ) ) / 2 ) ) |
3 |
1 2
|
syl |
|- ( ( A e. CC /\ B e. CC ) -> ( cos ` ( A + B ) ) = ( ( ( exp ` ( _i x. ( A + B ) ) ) + ( exp ` ( -u _i x. ( A + B ) ) ) ) / 2 ) ) |
4 |
|
coscl |
|- ( A e. CC -> ( cos ` A ) e. CC ) |
5 |
4
|
adantr |
|- ( ( A e. CC /\ B e. CC ) -> ( cos ` A ) e. CC ) |
6 |
|
coscl |
|- ( B e. CC -> ( cos ` B ) e. CC ) |
7 |
6
|
adantl |
|- ( ( A e. CC /\ B e. CC ) -> ( cos ` B ) e. CC ) |
8 |
5 7
|
mulcld |
|- ( ( A e. CC /\ B e. CC ) -> ( ( cos ` A ) x. ( cos ` B ) ) e. CC ) |
9 |
|
ax-icn |
|- _i e. CC |
10 |
|
sincl |
|- ( B e. CC -> ( sin ` B ) e. CC ) |
11 |
10
|
adantl |
|- ( ( A e. CC /\ B e. CC ) -> ( sin ` B ) e. CC ) |
12 |
|
mulcl |
|- ( ( _i e. CC /\ ( sin ` B ) e. CC ) -> ( _i x. ( sin ` B ) ) e. CC ) |
13 |
9 11 12
|
sylancr |
|- ( ( A e. CC /\ B e. CC ) -> ( _i x. ( sin ` B ) ) e. CC ) |
14 |
|
sincl |
|- ( A e. CC -> ( sin ` A ) e. CC ) |
15 |
14
|
adantr |
|- ( ( A e. CC /\ B e. CC ) -> ( sin ` A ) e. CC ) |
16 |
|
mulcl |
|- ( ( _i e. CC /\ ( sin ` A ) e. CC ) -> ( _i x. ( sin ` A ) ) e. CC ) |
17 |
9 15 16
|
sylancr |
|- ( ( A e. CC /\ B e. CC ) -> ( _i x. ( sin ` A ) ) e. CC ) |
18 |
13 17
|
mulcld |
|- ( ( A e. CC /\ B e. CC ) -> ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) e. CC ) |
19 |
8 18
|
addcld |
|- ( ( A e. CC /\ B e. CC ) -> ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) e. CC ) |
20 |
5 13
|
mulcld |
|- ( ( A e. CC /\ B e. CC ) -> ( ( cos ` A ) x. ( _i x. ( sin ` B ) ) ) e. CC ) |
21 |
7 17
|
mulcld |
|- ( ( A e. CC /\ B e. CC ) -> ( ( cos ` B ) x. ( _i x. ( sin ` A ) ) ) e. CC ) |
22 |
20 21
|
addcld |
|- ( ( A e. CC /\ B e. CC ) -> ( ( ( cos ` A ) x. ( _i x. ( sin ` B ) ) ) + ( ( cos ` B ) x. ( _i x. ( sin ` A ) ) ) ) e. CC ) |
23 |
19 22 19
|
ppncand |
|- ( ( A e. CC /\ B e. CC ) -> ( ( ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) + ( ( ( cos ` A ) x. ( _i x. ( sin ` B ) ) ) + ( ( cos ` B ) x. ( _i x. ( sin ` A ) ) ) ) ) + ( ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) - ( ( ( cos ` A ) x. ( _i x. ( sin ` B ) ) ) + ( ( cos ` B ) x. ( _i x. ( sin ` A ) ) ) ) ) ) = ( ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) + ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) ) ) |
24 |
|
adddi |
|- ( ( _i e. CC /\ A e. CC /\ B e. CC ) -> ( _i x. ( A + B ) ) = ( ( _i x. A ) + ( _i x. B ) ) ) |
25 |
9 24
|
mp3an1 |
|- ( ( A e. CC /\ B e. CC ) -> ( _i x. ( A + B ) ) = ( ( _i x. A ) + ( _i x. B ) ) ) |
26 |
25
|
fveq2d |
|- ( ( A e. CC /\ B e. CC ) -> ( exp ` ( _i x. ( A + B ) ) ) = ( exp ` ( ( _i x. A ) + ( _i x. B ) ) ) ) |
27 |
|
simpl |
|- ( ( A e. CC /\ B e. CC ) -> A e. CC ) |
28 |
|
mulcl |
|- ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC ) |
29 |
9 27 28
|
sylancr |
|- ( ( A e. CC /\ B e. CC ) -> ( _i x. A ) e. CC ) |
30 |
|
simpr |
|- ( ( A e. CC /\ B e. CC ) -> B e. CC ) |
31 |
|
mulcl |
|- ( ( _i e. CC /\ B e. CC ) -> ( _i x. B ) e. CC ) |
32 |
9 30 31
|
sylancr |
|- ( ( A e. CC /\ B e. CC ) -> ( _i x. B ) e. CC ) |
33 |
|
efadd |
|- ( ( ( _i x. A ) e. CC /\ ( _i x. B ) e. CC ) -> ( exp ` ( ( _i x. A ) + ( _i x. B ) ) ) = ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. B ) ) ) ) |
34 |
29 32 33
|
syl2anc |
|- ( ( A e. CC /\ B e. CC ) -> ( exp ` ( ( _i x. A ) + ( _i x. B ) ) ) = ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. B ) ) ) ) |
35 |
|
efival |
|- ( A e. CC -> ( exp ` ( _i x. A ) ) = ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) ) |
36 |
|
efival |
|- ( B e. CC -> ( exp ` ( _i x. B ) ) = ( ( cos ` B ) + ( _i x. ( sin ` B ) ) ) ) |
37 |
35 36
|
oveqan12d |
|- ( ( A e. CC /\ B e. CC ) -> ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. B ) ) ) = ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) x. ( ( cos ` B ) + ( _i x. ( sin ` B ) ) ) ) ) |
38 |
5 17 7 13
|
muladdd |
|- ( ( A e. CC /\ B e. CC ) -> ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) x. ( ( cos ` B ) + ( _i x. ( sin ` B ) ) ) ) = ( ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) + ( ( ( cos ` A ) x. ( _i x. ( sin ` B ) ) ) + ( ( cos ` B ) x. ( _i x. ( sin ` A ) ) ) ) ) ) |
39 |
37 38
|
eqtrd |
|- ( ( A e. CC /\ B e. CC ) -> ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. B ) ) ) = ( ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) + ( ( ( cos ` A ) x. ( _i x. ( sin ` B ) ) ) + ( ( cos ` B ) x. ( _i x. ( sin ` A ) ) ) ) ) ) |
40 |
26 34 39
|
3eqtrd |
|- ( ( A e. CC /\ B e. CC ) -> ( exp ` ( _i x. ( A + B ) ) ) = ( ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) + ( ( ( cos ` A ) x. ( _i x. ( sin ` B ) ) ) + ( ( cos ` B ) x. ( _i x. ( sin ` A ) ) ) ) ) ) |
41 |
|
negicn |
|- -u _i e. CC |
42 |
|
adddi |
|- ( ( -u _i e. CC /\ A e. CC /\ B e. CC ) -> ( -u _i x. ( A + B ) ) = ( ( -u _i x. A ) + ( -u _i x. B ) ) ) |
43 |
41 42
|
mp3an1 |
|- ( ( A e. CC /\ B e. CC ) -> ( -u _i x. ( A + B ) ) = ( ( -u _i x. A ) + ( -u _i x. B ) ) ) |
44 |
43
|
fveq2d |
|- ( ( A e. CC /\ B e. CC ) -> ( exp ` ( -u _i x. ( A + B ) ) ) = ( exp ` ( ( -u _i x. A ) + ( -u _i x. B ) ) ) ) |
45 |
|
mulcl |
|- ( ( -u _i e. CC /\ A e. CC ) -> ( -u _i x. A ) e. CC ) |
46 |
41 27 45
|
sylancr |
|- ( ( A e. CC /\ B e. CC ) -> ( -u _i x. A ) e. CC ) |
47 |
|
mulcl |
|- ( ( -u _i e. CC /\ B e. CC ) -> ( -u _i x. B ) e. CC ) |
48 |
41 30 47
|
sylancr |
|- ( ( A e. CC /\ B e. CC ) -> ( -u _i x. B ) e. CC ) |
49 |
|
efadd |
|- ( ( ( -u _i x. A ) e. CC /\ ( -u _i x. B ) e. CC ) -> ( exp ` ( ( -u _i x. A ) + ( -u _i x. B ) ) ) = ( ( exp ` ( -u _i x. A ) ) x. ( exp ` ( -u _i x. B ) ) ) ) |
50 |
46 48 49
|
syl2anc |
|- ( ( A e. CC /\ B e. CC ) -> ( exp ` ( ( -u _i x. A ) + ( -u _i x. B ) ) ) = ( ( exp ` ( -u _i x. A ) ) x. ( exp ` ( -u _i x. B ) ) ) ) |
51 |
|
efmival |
|- ( A e. CC -> ( exp ` ( -u _i x. A ) ) = ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) ) |
52 |
|
efmival |
|- ( B e. CC -> ( exp ` ( -u _i x. B ) ) = ( ( cos ` B ) - ( _i x. ( sin ` B ) ) ) ) |
53 |
51 52
|
oveqan12d |
|- ( ( A e. CC /\ B e. CC ) -> ( ( exp ` ( -u _i x. A ) ) x. ( exp ` ( -u _i x. B ) ) ) = ( ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) x. ( ( cos ` B ) - ( _i x. ( sin ` B ) ) ) ) ) |
54 |
5 17 7 13
|
mulsubd |
|- ( ( A e. CC /\ B e. CC ) -> ( ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) x. ( ( cos ` B ) - ( _i x. ( sin ` B ) ) ) ) = ( ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) - ( ( ( cos ` A ) x. ( _i x. ( sin ` B ) ) ) + ( ( cos ` B ) x. ( _i x. ( sin ` A ) ) ) ) ) ) |
55 |
53 54
|
eqtrd |
|- ( ( A e. CC /\ B e. CC ) -> ( ( exp ` ( -u _i x. A ) ) x. ( exp ` ( -u _i x. B ) ) ) = ( ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) - ( ( ( cos ` A ) x. ( _i x. ( sin ` B ) ) ) + ( ( cos ` B ) x. ( _i x. ( sin ` A ) ) ) ) ) ) |
56 |
44 50 55
|
3eqtrd |
|- ( ( A e. CC /\ B e. CC ) -> ( exp ` ( -u _i x. ( A + B ) ) ) = ( ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) - ( ( ( cos ` A ) x. ( _i x. ( sin ` B ) ) ) + ( ( cos ` B ) x. ( _i x. ( sin ` A ) ) ) ) ) ) |
57 |
40 56
|
oveq12d |
|- ( ( A e. CC /\ B e. CC ) -> ( ( exp ` ( _i x. ( A + B ) ) ) + ( exp ` ( -u _i x. ( A + B ) ) ) ) = ( ( ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) + ( ( ( cos ` A ) x. ( _i x. ( sin ` B ) ) ) + ( ( cos ` B ) x. ( _i x. ( sin ` A ) ) ) ) ) + ( ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) - ( ( ( cos ` A ) x. ( _i x. ( sin ` B ) ) ) + ( ( cos ` B ) x. ( _i x. ( sin ` A ) ) ) ) ) ) ) |
58 |
19
|
2timesd |
|- ( ( A e. CC /\ B e. CC ) -> ( 2 x. ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) ) = ( ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) + ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) ) ) |
59 |
23 57 58
|
3eqtr4d |
|- ( ( A e. CC /\ B e. CC ) -> ( ( exp ` ( _i x. ( A + B ) ) ) + ( exp ` ( -u _i x. ( A + B ) ) ) ) = ( 2 x. ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) ) ) |
60 |
59
|
oveq1d |
|- ( ( A e. CC /\ B e. CC ) -> ( ( ( exp ` ( _i x. ( A + B ) ) ) + ( exp ` ( -u _i x. ( A + B ) ) ) ) / 2 ) = ( ( 2 x. ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) ) / 2 ) ) |
61 |
|
2cn |
|- 2 e. CC |
62 |
|
2ne0 |
|- 2 =/= 0 |
63 |
|
divcan3 |
|- ( ( ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( 2 x. ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) ) / 2 ) = ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) ) |
64 |
61 62 63
|
mp3an23 |
|- ( ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) e. CC -> ( ( 2 x. ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) ) / 2 ) = ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) ) |
65 |
19 64
|
syl |
|- ( ( A e. CC /\ B e. CC ) -> ( ( 2 x. ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) ) / 2 ) = ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) ) |
66 |
9
|
a1i |
|- ( ( A e. CC /\ B e. CC ) -> _i e. CC ) |
67 |
66 11 66 15
|
mul4d |
|- ( ( A e. CC /\ B e. CC ) -> ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) = ( ( _i x. _i ) x. ( ( sin ` B ) x. ( sin ` A ) ) ) ) |
68 |
|
ixi |
|- ( _i x. _i ) = -u 1 |
69 |
68
|
oveq1i |
|- ( ( _i x. _i ) x. ( ( sin ` B ) x. ( sin ` A ) ) ) = ( -u 1 x. ( ( sin ` B ) x. ( sin ` A ) ) ) |
70 |
11 15
|
mulcomd |
|- ( ( A e. CC /\ B e. CC ) -> ( ( sin ` B ) x. ( sin ` A ) ) = ( ( sin ` A ) x. ( sin ` B ) ) ) |
71 |
70
|
oveq2d |
|- ( ( A e. CC /\ B e. CC ) -> ( -u 1 x. ( ( sin ` B ) x. ( sin ` A ) ) ) = ( -u 1 x. ( ( sin ` A ) x. ( sin ` B ) ) ) ) |
72 |
69 71
|
eqtrid |
|- ( ( A e. CC /\ B e. CC ) -> ( ( _i x. _i ) x. ( ( sin ` B ) x. ( sin ` A ) ) ) = ( -u 1 x. ( ( sin ` A ) x. ( sin ` B ) ) ) ) |
73 |
15 11
|
mulcld |
|- ( ( A e. CC /\ B e. CC ) -> ( ( sin ` A ) x. ( sin ` B ) ) e. CC ) |
74 |
73
|
mulm1d |
|- ( ( A e. CC /\ B e. CC ) -> ( -u 1 x. ( ( sin ` A ) x. ( sin ` B ) ) ) = -u ( ( sin ` A ) x. ( sin ` B ) ) ) |
75 |
67 72 74
|
3eqtrd |
|- ( ( A e. CC /\ B e. CC ) -> ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) = -u ( ( sin ` A ) x. ( sin ` B ) ) ) |
76 |
75
|
oveq2d |
|- ( ( A e. CC /\ B e. CC ) -> ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) = ( ( ( cos ` A ) x. ( cos ` B ) ) + -u ( ( sin ` A ) x. ( sin ` B ) ) ) ) |
77 |
8 73
|
negsubd |
|- ( ( A e. CC /\ B e. CC ) -> ( ( ( cos ` A ) x. ( cos ` B ) ) + -u ( ( sin ` A ) x. ( sin ` B ) ) ) = ( ( ( cos ` A ) x. ( cos ` B ) ) - ( ( sin ` A ) x. ( sin ` B ) ) ) ) |
78 |
65 76 77
|
3eqtrd |
|- ( ( A e. CC /\ B e. CC ) -> ( ( 2 x. ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( _i x. ( sin ` B ) ) x. ( _i x. ( sin ` A ) ) ) ) ) / 2 ) = ( ( ( cos ` A ) x. ( cos ` B ) ) - ( ( sin ` A ) x. ( sin ` B ) ) ) ) |
79 |
3 60 78
|
3eqtrd |
|- ( ( A e. CC /\ B e. CC ) -> ( cos ` ( A + B ) ) = ( ( ( cos ` A ) x. ( cos ` B ) ) - ( ( sin ` A ) x. ( sin ` B ) ) ) ) |