Metamath Proof Explorer

Theorem tanaddlem

Description: A useful intermediate step in tanadd when showing that the addition of tangents is well-defined. (Contributed by Mario Carneiro, 4-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 coscl 
 |-  ( A e. CC -> ( cos ` A ) e. CC )
2 1 ad2antrr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 ) ) -> ( cos ` A ) e. CC )
3 coscl 
 |-  ( B e. CC -> ( cos ` B ) e. CC )
4 3 ad2antlr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 ) ) -> ( cos ` B ) e. CC )
5 2 4 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 ) ) -> ( ( cos ` A ) x. ( cos ` B ) ) e. CC )
6 sincl 
 |-  ( A e. CC -> ( sin ` A ) e. CC )
7 6 ad2antrr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 ) ) -> ( sin ` A ) e. CC )
8 sincl 
 |-  ( B e. CC -> ( sin ` B ) e. CC )
9 8 ad2antlr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 ) ) -> ( sin ` B ) e. CC )
10 7 9 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 ) ) -> ( ( sin ` A ) x. ( sin ` B ) ) e. CC )
11 5 10 subeq0ad 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 ) ) -> ( ( ( ( cos ` A ) x. ( cos ` B ) ) - ( ( sin ` A ) x. ( sin ` B ) ) ) = 0 <-> ( ( cos ` A ) x. ( cos ` B ) ) = ( ( sin ` A ) x. ( sin ` B ) ) ) )
12 cosadd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cos ` ( A + B ) ) = ( ( ( cos ` A ) x. ( cos ` B ) ) - ( ( sin ` A ) x. ( sin ` B ) ) ) )
13 12 adantr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 ) ) -> ( cos ` ( A + B ) ) = ( ( ( cos ` A ) x. ( cos ` B ) ) - ( ( sin ` A ) x. ( sin ` B ) ) ) )
14 13 eqeq1d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 ) ) -> ( ( cos ` ( A + B ) ) = 0 <-> ( ( ( cos ` A ) x. ( cos ` B ) ) - ( ( sin ` A ) x. ( sin ` B ) ) ) = 0 ) )
15 tanval 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( tan ` A ) = ( ( sin ` A ) / ( cos ` A ) ) )
16 15 ad2ant2r 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 ) ) -> ( tan ` A ) = ( ( sin ` A ) / ( cos ` A ) ) )
17 tanval 
 |-  ( ( B e. CC /\ ( cos ` B ) =/= 0 ) -> ( tan ` B ) = ( ( sin ` B ) / ( cos ` B ) ) )
18 17 ad2ant2l 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 ) ) -> ( tan ` B ) = ( ( sin ` B ) / ( cos ` B ) ) )
19 16 18 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 ) ) -> ( ( tan ` A ) x. ( tan ` B ) ) = ( ( ( sin ` A ) / ( cos ` A ) ) x. ( ( sin ` B ) / ( cos ` B ) ) ) )
20 simprl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 ) ) -> ( cos ` A ) =/= 0 )
21 simprr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 ) ) -> ( cos ` B ) =/= 0 )
22 7 2 9 4 20 21 divmuldivd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 ) ) -> ( ( ( sin ` A ) / ( cos ` A ) ) x. ( ( sin ` B ) / ( cos ` B ) ) ) = ( ( ( sin ` A ) x. ( sin ` B ) ) / ( ( cos ` A ) x. ( cos ` B ) ) ) )
23 19 22 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 ) ) -> ( ( tan ` A ) x. ( tan ` B ) ) = ( ( ( sin ` A ) x. ( sin ` B ) ) / ( ( cos ` A ) x. ( cos ` B ) ) ) )
24 23 eqeq1d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 ) ) -> ( ( ( tan ` A ) x. ( tan ` B ) ) = 1 <-> ( ( ( sin ` A ) x. ( sin ` B ) ) / ( ( cos ` A ) x. ( cos ` B ) ) ) = 1 ) )
25 1cnd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 ) ) -> 1 e. CC )
26 2 4 20 21 mulne0d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 ) ) -> ( ( cos ` A ) x. ( cos ` B ) ) =/= 0 )
27 10 5 25 26 divmuld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 ) ) -> ( ( ( ( sin ` A ) x. ( sin ` B ) ) / ( ( cos ` A ) x. ( cos ` B ) ) ) = 1 <-> ( ( ( cos ` A ) x. ( cos ` B ) ) x. 1 ) = ( ( sin ` A ) x. ( sin ` B ) ) ) )
28 5 mulid1d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 ) ) -> ( ( ( cos ` A ) x. ( cos ` B ) ) x. 1 ) = ( ( cos ` A ) x. ( cos ` B ) ) )
29 28 eqeq1d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 ) ) -> ( ( ( ( cos ` A ) x. ( cos ` B ) ) x. 1 ) = ( ( sin ` A ) x. ( sin ` B ) ) <-> ( ( cos ` A ) x. ( cos ` B ) ) = ( ( sin ` A ) x. ( sin ` B ) ) ) )
30 24 27 29 3bitrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 ) ) -> ( ( ( tan ` A ) x. ( tan ` B ) ) = 1 <-> ( ( cos ` A ) x. ( cos ` B ) ) = ( ( sin ` A ) x. ( sin ` B ) ) ) )
31 11 14 30 3bitr4d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 ) ) -> ( ( cos ` ( A + B ) ) = 0 <-> ( ( tan ` A ) x. ( tan ` B ) ) = 1 ) )
32 31 necon3bid 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) =/= 0 /\ ( cos ` B ) =/= 0 ) ) -> ( ( cos ` ( A + B ) ) =/= 0 <-> ( ( tan ` A ) x. ( tan ` B ) ) =/= 1 ) )