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	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ↔ ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ≠ 1 ) )

Proof

Step	Hyp	Ref	Expression
1		coscl	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ )
2	1	ad2antrr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( cos ‘ 𝐴 ) ∈ ℂ )
3		coscl	⊢ ( 𝐵 ∈ ℂ → ( cos ‘ 𝐵 ) ∈ ℂ )
4	3	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( cos ‘ 𝐵 ) ∈ ℂ )
5	2 4	mulcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ∈ ℂ )
6		sincl	⊢ ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) ∈ ℂ )
7	6	ad2antrr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( sin ‘ 𝐴 ) ∈ ℂ )
8		sincl	⊢ ( 𝐵 ∈ ℂ → ( sin ‘ 𝐵 ) ∈ ℂ )
9	8	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( sin ‘ 𝐵 ) ∈ ℂ )
10	7 9	mulcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ∈ ℂ )
11	5 10	subeq0ad	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) = 0 ↔ ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) = ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
12		cosadd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( cos ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
13	12	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( cos ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
14	13	eqeq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( ( cos ‘ ( 𝐴 + 𝐵 ) ) = 0 ↔ ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) = 0 ) )
15		tanval	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( tan ‘ 𝐴 ) = ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) )
16	15	ad2ant2r	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( tan ‘ 𝐴 ) = ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) )
17		tanval	⊢ ( ( 𝐵 ∈ ℂ ∧ ( cos ‘ 𝐵 ) ≠ 0 ) → ( tan ‘ 𝐵 ) = ( ( sin ‘ 𝐵 ) / ( cos ‘ 𝐵 ) ) )
18	17	ad2ant2l	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( tan ‘ 𝐵 ) = ( ( sin ‘ 𝐵 ) / ( cos ‘ 𝐵 ) ) )
19	16 18	oveq12d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) = ( ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) · ( ( sin ‘ 𝐵 ) / ( cos ‘ 𝐵 ) ) ) )
20		simprl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( cos ‘ 𝐴 ) ≠ 0 )
21		simprr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( cos ‘ 𝐵 ) ≠ 0 )
22	7 2 9 4 20 21	divmuldivd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) · ( ( sin ‘ 𝐵 ) / ( cos ‘ 𝐵 ) ) ) = ( ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) / ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) )
23	19 22	eqtrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) = ( ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) / ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) )
24	23	eqeq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) = 1 ↔ ( ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) / ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) = 1 ) )
25		1cnd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → 1 ∈ ℂ )
26	2 4 20 21	mulne0d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ≠ 0 )
27	10 5 25 26	divmuld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( ( ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) / ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) = 1 ↔ ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · 1 ) = ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
28	5	mulid1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · 1 ) = ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) )
29	28	eqeq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) · 1 ) = ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ↔ ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) = ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
30	24 27 29	3bitrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) = 1 ↔ ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) = ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
31	11 14 30	3bitr4d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( ( cos ‘ ( 𝐴 + 𝐵 ) ) = 0 ↔ ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) = 1 ) )
32	31	necon3bid	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( cos ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐵 ) ≠ 0 ) ) → ( ( cos ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ↔ ( ( tan ‘ 𝐴 ) · ( tan ‘ 𝐵 ) ) ≠ 1 ) )