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 mulridd 
 |-  ( ( ( 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 ) ) ) ) )