Metamath Proof Explorer

Theorem sinneg

Description: The sine of a negative is the negative of the sine. (Contributed by NM, 30-Apr-2005)

Ref Expression
Assertion sinneg ( 𝐴 ∈ ℂ → ( sin ‘ - 𝐴 ) = - ( sin ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 negcl ⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
2 sinval ⊢ ( - 𝐴 ∈ ℂ → ( sin ‘ - 𝐴 ) = ( ( ( exp ‘ ( i · - 𝐴 ) ) − ( exp ‘ ( - i · - 𝐴 ) ) ) / ( 2 · i ) ) )
3 1 2 syl ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ - 𝐴 ) = ( ( ( exp ‘ ( i · - 𝐴 ) ) − ( exp ‘ ( - i · - 𝐴 ) ) ) / ( 2 · i ) ) )
4 sinval ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) )
5 4 negeqd ⊢ ( 𝐴 ∈ ℂ → - ( sin ‘ 𝐴 ) = - ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · 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 negicn ⊢ - i ∈ ℂ
12 mulcl ⊢ ( ( - i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · 𝐴 ) ∈ ℂ )
13 11 12 mpan ⊢ ( 𝐴 ∈ ℂ → ( - i · 𝐴 ) ∈ ℂ )
14 efcl ⊢ ( ( - i · 𝐴 ) ∈ ℂ → ( exp ‘ ( - i · 𝐴 ) ) ∈ ℂ )
15 13 14 syl ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( - i · 𝐴 ) ) ∈ ℂ )
16 10 15 subcld ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ )
17 2mulicn ⊢ ( 2 · i ) ∈ ℂ
18 2muline0 ⊢ ( 2 · i ) ≠ 0
19 divneg ⊢ ( ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ ∧ ( 2 · i ) ∈ ℂ ∧ ( 2 · i ) ≠ 0 ) → - ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) = ( - ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) )
20 17 18 19 mp3an23 ⊢ ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ → - ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) = ( - ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) )
21 16 20 syl ⊢ ( 𝐴 ∈ ℂ → - ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) = ( - ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) )
22 5 21 eqtrd ⊢ ( 𝐴 ∈ ℂ → - ( sin ‘ 𝐴 ) = ( - ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) )
23 mulneg12 ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · 𝐴 ) = ( i · - 𝐴 ) )
24 6 23 mpan ⊢ ( 𝐴 ∈ ℂ → ( - i · 𝐴 ) = ( i · - 𝐴 ) )
25 24 eqcomd ⊢ ( 𝐴 ∈ ℂ → ( i · - 𝐴 ) = ( - i · 𝐴 ) )
26 25 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · - 𝐴 ) ) = ( exp ‘ ( - i · 𝐴 ) ) )
27 mul2neg ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · - 𝐴 ) = ( i · 𝐴 ) )
28 6 27 mpan ⊢ ( 𝐴 ∈ ℂ → ( - i · - 𝐴 ) = ( i · 𝐴 ) )
29 28 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( - i · - 𝐴 ) ) = ( exp ‘ ( i · 𝐴 ) ) )
30 26 29 oveq12d ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · - 𝐴 ) ) − ( exp ‘ ( - i · - 𝐴 ) ) ) = ( ( exp ‘ ( - i · 𝐴 ) ) − ( exp ‘ ( i · 𝐴 ) ) ) )
31 10 15 negsubdi2d ⊢ ( 𝐴 ∈ ℂ → - ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) = ( ( exp ‘ ( - i · 𝐴 ) ) − ( exp ‘ ( i · 𝐴 ) ) ) )
32 30 31 eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · - 𝐴 ) ) − ( exp ‘ ( - i · - 𝐴 ) ) ) = - ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) )
33 32 oveq1d ⊢ ( 𝐴 ∈ ℂ → ( ( ( exp ‘ ( i · - 𝐴 ) ) − ( exp ‘ ( - i · - 𝐴 ) ) ) / ( 2 · i ) ) = ( - ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) )
34 22 33 eqtr4d ⊢ ( 𝐴 ∈ ℂ → - ( sin ‘ 𝐴 ) = ( ( ( exp ‘ ( i · - 𝐴 ) ) − ( exp ‘ ( - i · - 𝐴 ) ) ) / ( 2 · i ) ) )
35 3 34 eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ - 𝐴 ) = - ( sin ‘ 𝐴 ) )