Metamath Proof Explorer

Theorem tanadd

Description: Addition formula for tangent. (Contributed by Mario Carneiro, 4-Apr-2015)

Ref Expression
Assertion tanadd ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( tan ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( tan ‘ 𝐴 ) + ( tan ‘ 𝐵 ) ) / ( 1 − ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 addcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) ∈ ℂ )
2 1 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( 𝐴 + 𝐵 ) ∈ ℂ )
3 simpr3 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 )
4 tanval ⊢ ( ( ( 𝐴 + 𝐵 ) ∈ ℂ ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) → ( tan ‘ ( 𝐴 + 𝐵 ) ) = ( ( sin ‘ ( 𝐴 + 𝐵 ) ) / ( cos ‘ ( 𝐴 + 𝐵 ) ) ) )
5 2 3 4 syl2anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( tan ‘ ( 𝐴 + 𝐵 ) ) = ( ( sin ‘ ( 𝐴 + 𝐵 ) ) / ( cos ‘ ( 𝐴 + 𝐵 ) ) ) )
6 sinadd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sin ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
7 6 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( sin ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
8 cosadd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( cos ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
9 8 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( cos ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
10 7 9 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( sin ‘ ( 𝐴 + 𝐵 ) ) / ( cos ‘ ( 𝐴 + 𝐵 ) ) ) = ( ( ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) / ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) ) )
11 simpll ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → 𝐴 ∈ ℂ )
12 11 coscld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( cos ‘ 𝐴 ) ∈ ℂ )
13 simplr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → 𝐵 ∈ ℂ )
14 13 coscld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( cos ‘ 𝐵 ) ∈ ℂ )
15 12 14 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ∈ ℂ )
16 simpr1 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( cos ‘ 𝐴 ) ≠ 0 )
17 11 16 tancld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( tan ‘ 𝐴 ) ∈ ℂ )
18 simpr2 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( cos ‘ 𝐵 ) ≠ 0 )
19 13 18 tancld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( tan ‘ 𝐵 ) ∈ ℂ )
20 15 17 19 adddid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · ( ( tan ‘ 𝐴 ) + ( tan ‘ 𝐵 ) ) ) = ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · ( tan ‘ 𝐴 ) ) + ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · ( tan ‘ 𝐵 ) ) ) )
21 12 14 17 mul32d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · ( tan ‘ 𝐴 ) ) = ( ( ( cos ‘ 𝐴 ) · ( tan ‘ 𝐴 ) ) · ( cos ‘ 𝐵 ) ) )
22 tanval ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( tan ‘ 𝐴 ) = ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) )
23 11 16 22 syl2anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( tan ‘ 𝐴 ) = ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) )
24 23 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( cos ‘ 𝐴 ) · ( tan ‘ 𝐴 ) ) = ( ( cos ‘ 𝐴 ) · ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) ) )
25 11 sincld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( sin ‘ 𝐴 ) ∈ ℂ )
26 25 12 16 divcan2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( cos ‘ 𝐴 ) · ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) ) = ( sin ‘ 𝐴 ) )
27 24 26 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( cos ‘ 𝐴 ) · ( tan ‘ 𝐴 ) ) = ( sin ‘ 𝐴 ) )
28 27 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( cos ‘ 𝐴 ) · ( tan ‘ 𝐴 ) ) · ( cos ‘ 𝐵 ) ) = ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) )
29 21 28 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · ( tan ‘ 𝐴 ) ) = ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) )
30 12 14 19 mulassd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · ( tan ‘ 𝐵 ) ) = ( ( cos ‘ 𝐴 ) · ( ( cos ‘ 𝐵 ) · ( tan ‘ 𝐵 ) ) ) )
31 tanval ⊢ ( ( 𝐵 ∈ ℂ ∧ ( cos ‘ 𝐵 ) ≠ 0 ) → ( tan ‘ 𝐵 ) = ( ( sin ‘ 𝐵 ) / ( cos ‘ 𝐵 ) ) )
32 13 18 31 syl2anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( tan ‘ 𝐵 ) = ( ( sin ‘ 𝐵 ) / ( cos ‘ 𝐵 ) ) )
33 32 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( cos ‘ 𝐵 ) · ( tan ‘ 𝐵 ) ) = ( ( cos ‘ 𝐵 ) · ( ( sin ‘ 𝐵 ) / ( cos ‘ 𝐵 ) ) ) )
34 13 sincld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( sin ‘ 𝐵 ) ∈ ℂ )
35 34 14 18 divcan2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( cos ‘ 𝐵 ) · ( ( sin ‘ 𝐵 ) / ( cos ‘ 𝐵 ) ) ) = ( sin ‘ 𝐵 ) )
36 33 35 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( cos ‘ 𝐵 ) · ( tan ‘ 𝐵 ) ) = ( sin ‘ 𝐵 ) )
37 36 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( cos ‘ 𝐴 ) · ( ( cos ‘ 𝐵 ) · ( tan ‘ 𝐵 ) ) ) = ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) )
38 30 37 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · ( tan ‘ 𝐵 ) ) = ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) )
39 29 38 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · ( tan ‘ 𝐴 ) ) + ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · ( tan ‘ 𝐵 ) ) ) = ( ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
40 20 39 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · ( ( tan ‘ 𝐴 ) + ( tan ‘ 𝐵 ) ) ) = ( ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
41 1cnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → 1 ∈ ℂ )
42 17 19 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ∈ ℂ )
43 15 41 42 subdid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · ( 1 − ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ) ) = ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · 1 ) − ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ) ) )
44 15 mulridd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · 1 ) = ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) )
45 12 14 17 19 mul4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ) = ( ( ( cos ‘ 𝐴 ) · ( tan ‘ 𝐴 ) ) · ( ( cos ‘ 𝐵 ) · ( tan ‘ 𝐵 ) ) ) )
46 27 36 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( cos ‘ 𝐴 ) · ( tan ‘ 𝐴 ) ) · ( ( cos ‘ 𝐵 ) · ( tan ‘ 𝐵 ) ) ) = ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) )
47 45 46 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ) = ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) )
48 44 47 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · 1 ) − ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ) ) = ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
49 43 48 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · ( 1 − ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ) ) = ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
50 40 49 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · ( ( tan ‘ 𝐴 ) + ( tan ‘ 𝐵 ) ) ) / ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · ( 1 − ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ) ) ) = ( ( ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) / ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) ) )
51 17 19 addcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( tan ‘ 𝐴 ) + ( tan ‘ 𝐵 ) ) ∈ ℂ )
52 ax-1cn ⊢ 1 ∈ ℂ
53 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ∈ ℂ ) → ( 1 − ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ) ∈ ℂ )
54 52 42 53 sylancr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( 1 − ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ) ∈ ℂ )
55 tanaddlem ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ↔ ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ≠ 1 ) )
56 55 3adantr3 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ↔ ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ≠ 1 ) )
57 3 56 mpbid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ≠ 1 )
58 57 necomd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → 1 ≠ ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) )
59 subeq0 ⊢ ( ( 1 ∈ ℂ ∧ ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ∈ ℂ ) → ( ( 1 − ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ) = 0 ↔ 1 = ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ) )
60 59 necon3bid ⊢ ( ( 1 ∈ ℂ ∧ ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ∈ ℂ ) → ( ( 1 − ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ) ≠ 0 ↔ 1 ≠ ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ) )
61 52 42 60 sylancr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( 1 − ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ) ≠ 0 ↔ 1 ≠ ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ) )
62 58 61 mpbird ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( 1 − ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ) ≠ 0 )
63 12 14 16 18 mulne0d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ≠ 0 )
64 51 54 15 62 63 divcan5d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · ( ( tan ‘ 𝐴 ) + ( tan ‘ 𝐵 ) ) ) / ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · ( 1 − ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ) ) ) = ( ( ( tan ‘ 𝐴 ) + ( tan ‘ 𝐵 ) ) / ( 1 − ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ) ) )
65 10 50 64 3eqtr2rd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( tan ‘ 𝐴 ) + ( tan ‘ 𝐵 ) ) / ( 1 − ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ) ) = ( ( sin ‘ ( 𝐴 + 𝐵 ) ) / ( cos ‘ ( 𝐴 + 𝐵 ) ) ) )
66 5 65 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ∧ ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( tan ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( tan ‘ 𝐴 ) + ( tan ‘ 𝐵 ) ) / ( 1 − ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ) ) )