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 \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to (\cos (A + B) \neq 0 \leftrightarrow \tan A \tan B \neq 1)$

Proof

Step	Hyp	Ref	Expression
1		coscl	$⊢ A \in ℂ \to \cos A \in ℂ$
2	1	ad2antrr	$⊢ ((A \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to \cos A \in ℂ$
3		coscl	$⊢ B \in ℂ \to \cos B \in ℂ$
4	3	ad2antlr	$⊢ ((A \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to \cos B \in ℂ$
5	2 4	mulcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to \cos A \cos B \in ℂ$
6		sincl	$⊢ A \in ℂ \to \sin A \in ℂ$
7	6	ad2antrr	$⊢ ((A \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to \sin A \in ℂ$
8		sincl	$⊢ B \in ℂ \to \sin B \in ℂ$
9	8	ad2antlr	$⊢ ((A \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to \sin B \in ℂ$
10	7 9	mulcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to \sin A \sin B \in ℂ$
11	5 10	subeq0ad	$⊢ ((A \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to (\cos A \cos B - \sin A \sin B = 0 \leftrightarrow \cos A \cos B = \sin A \sin B)$
12		cosadd	$⊢ (A \in ℂ \land B \in ℂ) \to \cos (A + B) = \cos A \cos B - \sin A \sin B$
13	12	adantr	$⊢ ((A \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to \cos (A + B) = \cos A \cos B - \sin A \sin B$
14	13	eqeq1d	$⊢ ((A \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to (\cos (A + B) = 0 \leftrightarrow \cos A \cos B - \sin A \sin B = 0)$
15		tanval	$⊢ (A \in ℂ \land \cos A \neq 0) \to \tan A = \frac{\sin A}{\cos A}$
16	15	ad2ant2r	$⊢ ((A \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to \tan A = \frac{\sin A}{\cos A}$
17		tanval	$⊢ (B \in ℂ \land \cos B \neq 0) \to \tan B = \frac{\sin B}{\cos B}$
18	17	ad2ant2l	$⊢ ((A \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to \tan B = \frac{\sin B}{\cos B}$
19	16 18	oveq12d	$⊢ ((A \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to \tan A \tan B = (\frac{\sin A}{\cos A}) (\frac{\sin B}{\cos B})$
20		simprl	$⊢ ((A \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to \cos A \neq 0$
21		simprr	$⊢ ((A \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to \cos B \neq 0$
22	7 2 9 4 20 21	divmuldivd	$⊢ ((A \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to (\frac{\sin A}{\cos A}) (\frac{\sin B}{\cos B}) = \frac{\sin A \sin B}{\cos A \cos B}$
23	19 22	eqtrd	$⊢ ((A \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to \tan A \tan B = \frac{\sin A \sin B}{\cos A \cos B}$
24	23	eqeq1d	$⊢ ((A \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to (\tan A \tan B = 1 \leftrightarrow \frac{\sin A \sin B}{\cos A \cos B} = 1)$
25		1cnd	$⊢ ((A \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to 1 \in ℂ$
26	2 4 20 21	mulne0d	$⊢ ((A \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to \cos A \cos B \neq 0$
27	10 5 25 26	divmuld	$⊢ ((A \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to (\frac{\sin A \sin B}{\cos A \cos B} = 1 \leftrightarrow \cos A \cos B \cdot 1 = \sin A \sin B)$
28	5	mulridd	$⊢ ((A \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to \cos A \cos B \cdot 1 = \cos A \cos B$
29	28	eqeq1d	$⊢ ((A \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to (\cos A \cos B \cdot 1 = \sin A \sin B \leftrightarrow \cos A \cos B = \sin A \sin B)$
30	24 27 29	3bitrd	$⊢ ((A \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to (\tan A \tan B = 1 \leftrightarrow \cos A \cos B = \sin A \sin B)$
31	11 14 30	3bitr4d	$⊢ ((A \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to (\cos (A + B) = 0 \leftrightarrow \tan A \tan B = 1)$
32	31	necon3bid	$⊢ ((A \in ℂ \land B \in ℂ) \land (\cos A \neq 0 \land \cos B \neq 0)) \to (\cos (A + B) \neq 0 \leftrightarrow \tan A \tan B \neq 1)$

Metamath Proof Explorer

Theorem tanaddlem

Proof