Metamath Proof Explorer

Theorem cosneg

Description: The cosines of a number and its negative are the same. (Contributed by NM, 30-Apr-2005)

Ref Expression
Assertion cosneg 
|- ( A e. CC -> ( cos ` -u A ) = ( cos ` A ) )

Proof

Step Hyp Ref Expression
1 negicn 
 |-  -u _i e. CC
2 mulcl 
 |-  ( ( -u _i e. CC /\ A e. CC ) -> ( -u _i x. A ) e. CC )
3 1 2 mpan 
 |-  ( A e. CC -> ( -u _i x. A ) e. CC )
4 efcl 
 |-  ( ( -u _i x. A ) e. CC -> ( exp ` ( -u _i x. A ) ) e. CC )
5 3 4 syl 
 |-  ( A e. CC -> ( exp ` ( -u _i x. A ) ) e. CC )
6 ax-icn 
 |-  _i e. CC
7 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
8 6 7 mpan 
 |-  ( A e. CC -> ( _i x. A ) e. CC )
9 efcl 
 |-  ( ( _i x. A ) e. CC -> ( exp ` ( _i x. A ) ) e. CC )
10 8 9 syl 
 |-  ( A e. CC -> ( exp ` ( _i x. A ) ) e. CC )
11 mulneg12 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( -u _i x. A ) = ( _i x. -u A ) )
12 6 11 mpan 
 |-  ( A e. CC -> ( -u _i x. A ) = ( _i x. -u A ) )
13 12 eqcomd 
 |-  ( A e. CC -> ( _i x. -u A ) = ( -u _i x. A ) )
14 13 fveq2d 
 |-  ( A e. CC -> ( exp ` ( _i x. -u A ) ) = ( exp ` ( -u _i x. A ) ) )
15 mul2neg 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( -u _i x. -u A ) = ( _i x. A ) )
16 6 15 mpan 
 |-  ( A e. CC -> ( -u _i x. -u A ) = ( _i x. A ) )
17 16 fveq2d 
 |-  ( A e. CC -> ( exp ` ( -u _i x. -u A ) ) = ( exp ` ( _i x. A ) ) )
18 14 17 oveq12d 
 |-  ( A e. CC -> ( ( exp ` ( _i x. -u A ) ) + ( exp ` ( -u _i x. -u A ) ) ) = ( ( exp ` ( -u _i x. A ) ) + ( exp ` ( _i x. A ) ) ) )
19 5 10 18 comraddd 
 |-  ( A e. CC -> ( ( exp ` ( _i x. -u A ) ) + ( exp ` ( -u _i x. -u A ) ) ) = ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) )
20 19 oveq1d 
 |-  ( A e. CC -> ( ( ( exp ` ( _i x. -u A ) ) + ( exp ` ( -u _i x. -u A ) ) ) / 2 ) = ( ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) / 2 ) )
21 negcl 
 |-  ( A e. CC -> -u A e. CC )
22 cosval 
 |-  ( -u A e. CC -> ( cos ` -u A ) = ( ( ( exp ` ( _i x. -u A ) ) + ( exp ` ( -u _i x. -u A ) ) ) / 2 ) )
23 21 22 syl 
 |-  ( A e. CC -> ( cos ` -u A ) = ( ( ( exp ` ( _i x. -u A ) ) + ( exp ` ( -u _i x. -u A ) ) ) / 2 ) )
24 cosval 
 |-  ( A e. CC -> ( cos ` A ) = ( ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) / 2 ) )
25 20 23 24 3eqtr4d 
 |-  ( A e. CC -> ( cos ` -u A ) = ( cos ` A ) )