Metamath Proof Explorer

Theorem tanneg

Description: The tangent of a negative is the negative of the tangent. (Contributed by David A. Wheeler, 23-Mar-2014)

Ref Expression
Assertion tanneg ⊢A∈ℂ∧cos⁡A≠0→tan⁡−A=−tan⁡A

Proof

Step Hyp Ref Expression
1 coscl ⊢A∈ℂ→cos⁡A∈ℂ
2 sincl ⊢A∈ℂ→sin⁡A∈ℂ
3 divneg ⊢sin⁡A∈ℂ∧cos⁡A∈ℂ∧cos⁡A≠0→−sin⁡Acos⁡A=−sin⁡Acos⁡A
4 2 3 syl3an1 ⊢A∈ℂ∧cos⁡A∈ℂ∧cos⁡A≠0→−sin⁡Acos⁡A=−sin⁡Acos⁡A
5 1 4 syl3an2 ⊢A∈ℂ∧A∈ℂ∧cos⁡A≠0→−sin⁡Acos⁡A=−sin⁡Acos⁡A
6 5 3anidm12 ⊢A∈ℂ∧cos⁡A≠0→−sin⁡Acos⁡A=−sin⁡Acos⁡A
7 tanval ⊢A∈ℂ∧cos⁡A≠0→tan⁡A=sin⁡Acos⁡A
8 7 negeqd ⊢A∈ℂ∧cos⁡A≠0→−tan⁡A=−sin⁡Acos⁡A
9 negcl ⊢A∈ℂ→−A∈ℂ
10 cosneg ⊢A∈ℂ→cos⁡−A=cos⁡A
11 10 adantr ⊢A∈ℂ∧cos⁡A≠0→cos⁡−A=cos⁡A
12 simpr ⊢A∈ℂ∧cos⁡A≠0→cos⁡A≠0
13 11 12 eqnetrd ⊢A∈ℂ∧cos⁡A≠0→cos⁡−A≠0
14 tanval ⊢−A∈ℂ∧cos⁡−A≠0→tan⁡−A=sin⁡−Acos⁡−A
15 9 13 14 syl2an2r ⊢A∈ℂ∧cos⁡A≠0→tan⁡−A=sin⁡−Acos⁡−A
16 sinneg ⊢A∈ℂ→sin⁡−A=−sin⁡A
17 16 10 oveq12d ⊢A∈ℂ→sin⁡−Acos⁡−A=−sin⁡Acos⁡A
18 17 adantr ⊢A∈ℂ∧cos⁡A≠0→sin⁡−Acos⁡−A=−sin⁡Acos⁡A
19 15 18 eqtrd ⊢A∈ℂ∧cos⁡A≠0→tan⁡−A=−sin⁡Acos⁡A
20 6 8 19 3eqtr4rd ⊢A∈ℂ∧cos⁡A≠0→tan⁡−A=−tan⁡A