Metamath Proof Explorer


Theorem tanadd

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

Ref Expression
Assertion tanadd
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 /\ ( cos ` ( A + B ) ) =/= 0 ) ) -> ( tan ` ( A + B ) ) = ( ( ( tan ` A ) + ( tan ` B ) ) / ( 1 - ( ( tan ` A ) x. ( tan ` B ) ) ) ) )

Proof

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