This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ ℂ → ( cos ‘ - 𝐴 ) = ( cos ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 negicn ⊢ - i ∈ ℂ
2 mulcl ⊢ ( ( - i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · 𝐴 ) ∈ ℂ )
3 1 2 mpan ⊢ ( 𝐴 ∈ ℂ → ( - i · 𝐴 ) ∈ ℂ )
4 efcl ⊢ ( ( - i · 𝐴 ) ∈ ℂ → ( exp ‘ ( - i · 𝐴 ) ) ∈ ℂ )
5 3 4 syl ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( - i · 𝐴 ) ) ∈ ℂ )
6 ax-icn ⊢ i ∈ ℂ
7 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
8 6 7 mpan ⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ∈ ℂ )
9 efcl ⊢ ( ( i · 𝐴 ) ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ )
10 8 9 syl ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ )
11 mulneg12 ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · 𝐴 ) = ( i · - 𝐴 ) )
12 6 11 mpan ⊢ ( 𝐴 ∈ ℂ → ( - i · 𝐴 ) = ( i · - 𝐴 ) )
13 12 eqcomd ⊢ ( 𝐴 ∈ ℂ → ( i · - 𝐴 ) = ( - i · 𝐴 ) )
14 13 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · - 𝐴 ) ) = ( exp ‘ ( - i · 𝐴 ) ) )
15 mul2neg ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · - 𝐴 ) = ( i · 𝐴 ) )
16 6 15 mpan ⊢ ( 𝐴 ∈ ℂ → ( - i · - 𝐴 ) = ( i · 𝐴 ) )
17 16 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( - i · - 𝐴 ) ) = ( exp ‘ ( i · 𝐴 ) ) )
18 14 17 oveq12d ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · - 𝐴 ) ) + ( exp ‘ ( - i · - 𝐴 ) ) ) = ( ( exp ‘ ( - i · 𝐴 ) ) + ( exp ‘ ( i · 𝐴 ) ) ) )
19 5 10 18 comraddd ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · - 𝐴 ) ) + ( exp ‘ ( - i · - 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) )
20 19 oveq1d ⊢ ( 𝐴 ∈ ℂ → ( ( ( exp ‘ ( i · - 𝐴 ) ) + ( exp ‘ ( - i · - 𝐴 ) ) ) / 2 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) )
21 negcl ⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
22 cosval ⊢ ( - 𝐴 ∈ ℂ → ( cos ‘ - 𝐴 ) = ( ( ( exp ‘ ( i · - 𝐴 ) ) + ( exp ‘ ( - i · - 𝐴 ) ) ) / 2 ) )
23 21 22 syl ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ - 𝐴 ) = ( ( ( exp ‘ ( i · - 𝐴 ) ) + ( exp ‘ ( - i · - 𝐴 ) ) ) / 2 ) )
24 cosval ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) + ( exp ‘ ( - i · 𝐴 ) ) ) / 2 ) )
25 20 23 24 3eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ - 𝐴 ) = ( cos ‘ 𝐴 ) )