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 ⁡ A cos ⁡ A = − sin ⁡ A cos ⁡ A
4 2 3 syl3an1 ⊢ A ∈ ℂ ∧ cos ⁡ A ∈ ℂ ∧ cos ⁡ A ≠ 0 → − sin ⁡ A cos ⁡ A = − sin ⁡ A cos ⁡ A
5 1 4 syl3an2 ⊢ A ∈ ℂ ∧ A ∈ ℂ ∧ cos ⁡ A ≠ 0 → − sin ⁡ A cos ⁡ A = − sin ⁡ A cos ⁡ A
6 5 3anidm12 ⊢ A ∈ ℂ ∧ cos ⁡ A ≠ 0 → − sin ⁡ A cos ⁡ A = − sin ⁡ A cos ⁡ A
7 tanval ⊢ A ∈ ℂ ∧ cos ⁡ A ≠ 0 → tan ⁡ A = sin ⁡ A cos ⁡ A
8 7 negeqd ⊢ A ∈ ℂ ∧ cos ⁡ A ≠ 0 → − tan ⁡ A = − sin ⁡ A cos ⁡ 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 ⁡ − A cos ⁡ − A
15 9 13 14 syl2an2r ⊢ A ∈ ℂ ∧ cos ⁡ A ≠ 0 → tan ⁡ − A = sin ⁡ − A cos ⁡ − A
16 sinneg ⊢ A ∈ ℂ → sin ⁡ − A = − sin ⁡ A
17 16 10 oveq12d ⊢ A ∈ ℂ → sin ⁡ − A cos ⁡ − A = − sin ⁡ A cos ⁡ A
18 17 adantr ⊢ A ∈ ℂ ∧ cos ⁡ A ≠ 0 → sin ⁡ − A cos ⁡ − A = − sin ⁡ A cos ⁡ A
19 15 18 eqtrd ⊢ A ∈ ℂ ∧ cos ⁡ A ≠ 0 → tan ⁡ − A = − sin ⁡ A cos ⁡ A
20 6 8 19 3eqtr4rd ⊢ A ∈ ℂ ∧ cos ⁡ A ≠ 0 → tan ⁡ − A = − tan ⁡ A