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 ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( tan ‘ - 𝐴 ) = - ( tan ‘ 𝐴 ) )

Proof

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