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 ⊢A∈ℂ→sin⁡−A=−sin⁡A

Proof

Step Hyp Ref Expression
1 negcl ⊢A∈ℂ→−A∈ℂ
2 sinval ⊢−A∈ℂ→sin⁡−A=ei⁢−A−e−i⁢−A2⁢i
3 1 2 syl ⊢A∈ℂ→sin⁡−A=ei⁢−A−e−i⁢−A2⁢i
4 sinval ⊢A∈ℂ→sin⁡A=ei⁢A−e−i⁢A2⁢i
5 4 negeqd ⊢A∈ℂ→−sin⁡A=−ei⁢A−e−i⁢A2⁢i
6 ax-icn ⊢i∈ℂ
7 mulcl ⊢i∈ℂ∧A∈ℂ→i⁢A∈ℂ
8 6 7 mpan ⊢A∈ℂ→i⁢A∈ℂ
9 efcl ⊢i⁢A∈ℂ→ei⁢A∈ℂ
10 8 9 syl ⊢A∈ℂ→ei⁢A∈ℂ
11 negicn ⊢−i∈ℂ
12 mulcl ⊢−i∈ℂ∧A∈ℂ→−i⁢A∈ℂ
13 11 12 mpan ⊢A∈ℂ→−i⁢A∈ℂ
14 efcl ⊢−i⁢A∈ℂ→e−i⁢A∈ℂ
15 13 14 syl ⊢A∈ℂ→e−i⁢A∈ℂ
16 10 15 subcld ⊢A∈ℂ→ei⁢A−e−i⁢A∈ℂ
17 2mulicn ⊢2⁢i∈ℂ
18 2muline0 ⊢2⁢i≠0
19 divneg ⊢ei⁢A−e−i⁢A∈ℂ∧2⁢i∈ℂ∧2⁢i≠0→−ei⁢A−e−i⁢A2⁢i=−ei⁢A−e−i⁢A2⁢i
20 17 18 19 mp3an23 ⊢ei⁢A−e−i⁢A∈ℂ→−ei⁢A−e−i⁢A2⁢i=−ei⁢A−e−i⁢A2⁢i
21 16 20 syl ⊢A∈ℂ→−ei⁢A−e−i⁢A2⁢i=−ei⁢A−e−i⁢A2⁢i
22 5 21 eqtrd ⊢A∈ℂ→−sin⁡A=−ei⁢A−e−i⁢A2⁢i
23 mulneg12 ⊢i∈ℂ∧A∈ℂ→−i⁢A=i⁢−A
24 6 23 mpan ⊢A∈ℂ→−i⁢A=i⁢−A
25 24 eqcomd ⊢A∈ℂ→i⁢−A=−i⁢A
26 25 fveq2d ⊢A∈ℂ→ei⁢−A=e−i⁢A
27 mul2neg ⊢i∈ℂ∧A∈ℂ→−i⁢−A=i⁢A
28 6 27 mpan ⊢A∈ℂ→−i⁢−A=i⁢A
29 28 fveq2d ⊢A∈ℂ→e−i⁢−A=ei⁢A
30 26 29 oveq12d ⊢A∈ℂ→ei⁢−A−e−i⁢−A=e−i⁢A−ei⁢A
31 10 15 negsubdi2d ⊢A∈ℂ→−ei⁢A−e−i⁢A=e−i⁢A−ei⁢A
32 30 31 eqtr4d ⊢A∈ℂ→ei⁢−A−e−i⁢−A=−ei⁢A−e−i⁢A
33 32 oveq1d ⊢A∈ℂ→ei⁢−A−e−i⁢−A2⁢i=−ei⁢A−e−i⁢A2⁢i
34 22 33 eqtr4d ⊢A∈ℂ→−sin⁡A=ei⁢−A−e−i⁢−A2⁢i
35 3 34 eqtr4d ⊢A∈ℂ→sin⁡−A=−sin⁡A