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 = e i ⁢ − A − e − i ⁢ − A 2 ⁢ i
3 1 2 syl ⊢ A ∈ ℂ → sin ⁡ − A = e i ⁢ − A − e − i ⁢ − A 2 ⁢ i
4 sinval ⊢ A ∈ ℂ → sin ⁡ A = e i ⁢ A − e − i ⁢ A 2 ⁢ i
5 4 negeqd ⊢ A ∈ ℂ → − sin ⁡ A = − e i ⁢ A − e − i ⁢ A 2 ⁢ i
6 ax-icn ⊢ i ∈ ℂ
7 mulcl ⊢ i ∈ ℂ ∧ A ∈ ℂ → i ⁢ A ∈ ℂ
8 6 7 mpan ⊢ A ∈ ℂ → i ⁢ A ∈ ℂ
9 efcl ⊢ i ⁢ A ∈ ℂ → e i ⁢ A ∈ ℂ
10 8 9 syl ⊢ A ∈ ℂ → e i ⁢ 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 ∈ ℂ → e i ⁢ A − e − i ⁢ A ∈ ℂ
17 2mulicn ⊢ 2 ⁢ i ∈ ℂ
18 2muline0 ⊢ 2 ⁢ i ≠ 0
19 divneg ⊢ e i ⁢ A − e − i ⁢ A ∈ ℂ ∧ 2 ⁢ i ∈ ℂ ∧ 2 ⁢ i ≠ 0 → − e i ⁢ A − e − i ⁢ A 2 ⁢ i = − e i ⁢ A − e − i ⁢ A 2 ⁢ i
20 17 18 19 mp3an23 ⊢ e i ⁢ A − e − i ⁢ A ∈ ℂ → − e i ⁢ A − e − i ⁢ A 2 ⁢ i = − e i ⁢ A − e − i ⁢ A 2 ⁢ i
21 16 20 syl ⊢ A ∈ ℂ → − e i ⁢ A − e − i ⁢ A 2 ⁢ i = − e i ⁢ A − e − i ⁢ A 2 ⁢ i
22 5 21 eqtrd ⊢ A ∈ ℂ → − sin ⁡ A = − e i ⁢ A − e − i ⁢ A 2 ⁢ 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 ∈ ℂ → e i ⁢ − 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 = e i ⁢ A
30 26 29 oveq12d ⊢ A ∈ ℂ → e i ⁢ − A − e − i ⁢ − A = e − i ⁢ A − e i ⁢ A
31 10 15 negsubdi2d ⊢ A ∈ ℂ → − e i ⁢ A − e − i ⁢ A = e − i ⁢ A − e i ⁢ A
32 30 31 eqtr4d ⊢ A ∈ ℂ → e i ⁢ − A − e − i ⁢ − A = − e i ⁢ A − e − i ⁢ A
33 32 oveq1d ⊢ A ∈ ℂ → e i ⁢ − A − e − i ⁢ − A 2 ⁢ i = − e i ⁢ A − e − i ⁢ A 2 ⁢ i
34 22 33 eqtr4d ⊢ A ∈ ℂ → − sin ⁡ A = e i ⁢ − A − e − i ⁢ − A 2 ⁢ i
35 3 34 eqtr4d ⊢ A ∈ ℂ → sin ⁡ − A = − sin ⁡ A