Step |
Hyp |
Ref |
Expression |
1 |
|
negcl |
|- ( A e. CC -> -u A e. CC ) |
2 |
|
cosadd |
|- ( ( A e. CC /\ -u A e. CC ) -> ( cos ` ( A + -u A ) ) = ( ( ( cos ` A ) x. ( cos ` -u A ) ) - ( ( sin ` A ) x. ( sin ` -u A ) ) ) ) |
3 |
1 2
|
mpdan |
|- ( A e. CC -> ( cos ` ( A + -u A ) ) = ( ( ( cos ` A ) x. ( cos ` -u A ) ) - ( ( sin ` A ) x. ( sin ` -u A ) ) ) ) |
4 |
|
negid |
|- ( A e. CC -> ( A + -u A ) = 0 ) |
5 |
4
|
fveq2d |
|- ( A e. CC -> ( cos ` ( A + -u A ) ) = ( cos ` 0 ) ) |
6 |
|
cos0 |
|- ( cos ` 0 ) = 1 |
7 |
5 6
|
eqtrdi |
|- ( A e. CC -> ( cos ` ( A + -u A ) ) = 1 ) |
8 |
|
sincl |
|- ( A e. CC -> ( sin ` A ) e. CC ) |
9 |
8
|
sqcld |
|- ( A e. CC -> ( ( sin ` A ) ^ 2 ) e. CC ) |
10 |
|
coscl |
|- ( A e. CC -> ( cos ` A ) e. CC ) |
11 |
10
|
sqcld |
|- ( A e. CC -> ( ( cos ` A ) ^ 2 ) e. CC ) |
12 |
9 11
|
addcomd |
|- ( A e. CC -> ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) = ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) ) |
13 |
10
|
sqvald |
|- ( A e. CC -> ( ( cos ` A ) ^ 2 ) = ( ( cos ` A ) x. ( cos ` A ) ) ) |
14 |
|
cosneg |
|- ( A e. CC -> ( cos ` -u A ) = ( cos ` A ) ) |
15 |
14
|
oveq2d |
|- ( A e. CC -> ( ( cos ` A ) x. ( cos ` -u A ) ) = ( ( cos ` A ) x. ( cos ` A ) ) ) |
16 |
13 15
|
eqtr4d |
|- ( A e. CC -> ( ( cos ` A ) ^ 2 ) = ( ( cos ` A ) x. ( cos ` -u A ) ) ) |
17 |
8
|
sqvald |
|- ( A e. CC -> ( ( sin ` A ) ^ 2 ) = ( ( sin ` A ) x. ( sin ` A ) ) ) |
18 |
|
sinneg |
|- ( A e. CC -> ( sin ` -u A ) = -u ( sin ` A ) ) |
19 |
18
|
negeqd |
|- ( A e. CC -> -u ( sin ` -u A ) = -u -u ( sin ` A ) ) |
20 |
8
|
negnegd |
|- ( A e. CC -> -u -u ( sin ` A ) = ( sin ` A ) ) |
21 |
19 20
|
eqtrd |
|- ( A e. CC -> -u ( sin ` -u A ) = ( sin ` A ) ) |
22 |
21
|
oveq2d |
|- ( A e. CC -> ( ( sin ` A ) x. -u ( sin ` -u A ) ) = ( ( sin ` A ) x. ( sin ` A ) ) ) |
23 |
17 22
|
eqtr4d |
|- ( A e. CC -> ( ( sin ` A ) ^ 2 ) = ( ( sin ` A ) x. -u ( sin ` -u A ) ) ) |
24 |
1
|
sincld |
|- ( A e. CC -> ( sin ` -u A ) e. CC ) |
25 |
8 24
|
mulneg2d |
|- ( A e. CC -> ( ( sin ` A ) x. -u ( sin ` -u A ) ) = -u ( ( sin ` A ) x. ( sin ` -u A ) ) ) |
26 |
23 25
|
eqtrd |
|- ( A e. CC -> ( ( sin ` A ) ^ 2 ) = -u ( ( sin ` A ) x. ( sin ` -u A ) ) ) |
27 |
16 26
|
oveq12d |
|- ( A e. CC -> ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) = ( ( ( cos ` A ) x. ( cos ` -u A ) ) + -u ( ( sin ` A ) x. ( sin ` -u A ) ) ) ) |
28 |
1
|
coscld |
|- ( A e. CC -> ( cos ` -u A ) e. CC ) |
29 |
10 28
|
mulcld |
|- ( A e. CC -> ( ( cos ` A ) x. ( cos ` -u A ) ) e. CC ) |
30 |
8 24
|
mulcld |
|- ( A e. CC -> ( ( sin ` A ) x. ( sin ` -u A ) ) e. CC ) |
31 |
29 30
|
negsubd |
|- ( A e. CC -> ( ( ( cos ` A ) x. ( cos ` -u A ) ) + -u ( ( sin ` A ) x. ( sin ` -u A ) ) ) = ( ( ( cos ` A ) x. ( cos ` -u A ) ) - ( ( sin ` A ) x. ( sin ` -u A ) ) ) ) |
32 |
12 27 31
|
3eqtrrd |
|- ( A e. CC -> ( ( ( cos ` A ) x. ( cos ` -u A ) ) - ( ( sin ` A ) x. ( sin ` -u A ) ) ) = ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) ) |
33 |
3 7 32
|
3eqtr3rd |
|- ( A e. CC -> ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) = 1 ) |