# Metamath Proof Explorer

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
`|- ( ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 ) ) ) )`
` |-  ( ( A e. CC /\ B e. CC ) -> ( cos ` ( A + B ) ) = ( ( ( cos ` A ) x. ( cos ` B ) ) - ( ( sin ` A ) x. ( sin ` B ) ) ) )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( ( 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 ) )`