Theorem tanadd

Description: Addition formula for tangent. (Contributed by Mario Carneiro, 4-Apr-2015)

	Ref	Expression
Assertion	tanadd	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \tan \left(A+B\right)=\frac{\tan A+\tan B}{1-\tan A\tan B}$$

Proof

Step	Hyp	Ref	Expression
1		addcl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+B\in ℂ$$
2	1	adantr	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to A+B\in ℂ$$
3		simpr3	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos \left(A+B\right)\ne 0$$
4		tanval	$$⊢\left(A+B\in ℂ\wedge \cos \left(A+B\right)\ne 0\right)\to \tan \left(A+B\right)=\frac{\sin \left(A+B\right)}{\cos \left(A+B\right)}$$
5	2 3 4	syl2anc	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \tan \left(A+B\right)=\frac{\sin \left(A+B\right)}{\cos \left(A+B\right)}$$
6		sinadd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \sin \left(A+B\right)=\sin A\cos B+\cos A\sin B$$
7	6	adantr	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \sin \left(A+B\right)=\sin A\cos B+\cos A\sin B$$
8		cosadd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \cos \left(A+B\right)=\cos A\cos B-\sin A\sin B$$
9	8	adantr	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos \left(A+B\right)=\cos A\cos B-\sin A\sin B$$
10	7 9	oveq12d	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \frac{\sin \left(A+B\right)}{\cos \left(A+B\right)}=\frac{\sin A\cos B+\cos A\sin B}{\cos A\cos B-\sin A\sin B}$$
11		simpll	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to A\in ℂ$$
12	11	coscld	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos A\in ℂ$$
13		simplr	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to B\in ℂ$$
14	13	coscld	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos B\in ℂ$$
15	12 14	mulcld	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos A\cos B\in ℂ$$
16		simpr1	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos A\ne 0$$
17	11 16	tancld	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \tan A\in ℂ$$
18		simpr2	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos B\ne 0$$
19	13 18	tancld	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \tan B\in ℂ$$
20	15 17 19	adddid	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos A\cos B\left(\tan A+\tan B\right)=\cos A\cos B\tan A+\cos A\cos B\tan B$$
21	12 14 17	mul32d	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos A\cos B\tan A=\cos A\tan A\cos B$$
22		tanval	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \tan A=\frac{\sin A}{\cos A}$$
23	11 16 22	syl2anc	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \tan A=\frac{\sin A}{\cos A}$$
24	23	oveq2d	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos A\tan A=\cos A\left(\frac{\sin A}{\cos A}\right)$$
25	11	sincld	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \sin A\in ℂ$$
26	25 12 16	divcan2d	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos A\left(\frac{\sin A}{\cos A}\right)=\sin A$$
27	24 26	eqtrd	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos A\tan A=\sin A$$
28	27	oveq1d	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos A\tan A\cos B=\sin A\cos B$$
29	21 28	eqtrd	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos A\cos B\tan A=\sin A\cos B$$
30	12 14 19	mulassd	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos A\cos B\tan B=\cos A\cos B\tan B$$
31		tanval	$$⊢\left(B\in ℂ\wedge \cos B\ne 0\right)\to \tan B=\frac{\sin B}{\cos B}$$
32	13 18 31	syl2anc	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \tan B=\frac{\sin B}{\cos B}$$
33	32	oveq2d	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos B\tan B=\cos B\left(\frac{\sin B}{\cos B}\right)$$
34	13	sincld	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \sin B\in ℂ$$
35	34 14 18	divcan2d	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos B\left(\frac{\sin B}{\cos B}\right)=\sin B$$
36	33 35	eqtrd	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos B\tan B=\sin B$$
37	36	oveq2d	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos A\cos B\tan B=\cos A\sin B$$
38	30 37	eqtrd	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos A\cos B\tan B=\cos A\sin B$$
39	29 38	oveq12d	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos A\cos B\tan A+\cos A\cos B\tan B=\sin A\cos B+\cos A\sin B$$
40	20 39	eqtrd	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos A\cos B\left(\tan A+\tan B\right)=\sin A\cos B+\cos A\sin B$$
41		1cnd	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to 1\in ℂ$$
42	17 19	mulcld	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \tan A\tan B\in ℂ$$
43	15 41 42	subdid	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos A\cos B\left(1-\tan A\tan B\right)=\cos A\cos B\cdot 1-\cos A\cos B\tan A\tan B$$
44	15	mulid1d	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos A\cos B\cdot 1=\cos A\cos B$$
45	12 14 17 19	mul4d	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos A\cos B\tan A\tan B=\cos A\tan A\cos B\tan B$$
46	27 36	oveq12d	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos A\tan A\cos B\tan B=\sin A\sin B$$
47	45 46	eqtrd	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos A\cos B\tan A\tan B=\sin A\sin B$$
48	44 47	oveq12d	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos A\cos B\cdot 1-\cos A\cos B\tan A\tan B=\cos A\cos B-\sin A\sin B$$
49	43 48	eqtrd	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos A\cos B\left(1-\tan A\tan B\right)=\cos A\cos B-\sin A\sin B$$
50	40 49	oveq12d	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \frac{\cos A\cos B\left(\tan A+\tan B\right)}{\cos A\cos B\left(1-\tan A\tan B\right)}=\frac{\sin A\cos B+\cos A\sin B}{\cos A\cos B-\sin A\sin B}$$
51	17 19	addcld	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \tan A+\tan B\in ℂ$$
52		ax-1cn	$$⊢1\in ℂ$$
53		subcl	$$⊢\left(1\in ℂ\wedge \tan A\tan B\in ℂ\right)\to 1-\tan A\tan B\in ℂ$$
54	52 42 53	sylancr	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to 1-\tan A\tan B\in ℂ$$
55		tanaddlem	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\right)\right)\to \left(\cos \left(A+B\right)\ne 0\leftrightarrow \tan A\tan B\ne 1\right)$$
56	55	3adantr3	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \left(\cos \left(A+B\right)\ne 0\leftrightarrow \tan A\tan B\ne 1\right)$$
57	3 56	mpbid	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \tan A\tan B\ne 1$$
58	57	necomd	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to 1\ne \tan A\tan B$$
59		subeq0	$$⊢\left(1\in ℂ\wedge \tan A\tan B\in ℂ\right)\to \left(1-\tan A\tan B=0\leftrightarrow 1=\tan A\tan B\right)$$
60	59	necon3bid	$$⊢\left(1\in ℂ\wedge \tan A\tan B\in ℂ\right)\to \left(1-\tan A\tan B\ne 0\leftrightarrow 1\ne \tan A\tan B\right)$$
61	52 42 60	sylancr	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \left(1-\tan A\tan B\ne 0\leftrightarrow 1\ne \tan A\tan B\right)$$
62	58 61	mpbird	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to 1-\tan A\tan B\ne 0$$
63	12 14 16 18	mulne0d	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \cos A\cos B\ne 0$$
64	51 54 15 62 63	divcan5d	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \frac{\cos A\cos B\left(\tan A+\tan B\right)}{\cos A\cos B\left(1-\tan A\tan B\right)}=\frac{\tan A+\tan B}{1-\tan A\tan B}$$
65	10 50 64	3eqtr2rd	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \frac{\tan A+\tan B}{1-\tan A\tan B}=\frac{\sin \left(A+B\right)}{\cos \left(A+B\right)}$$
66	5 65	eqtr4d	$$⊢\left(\left(A\in ℂ\wedge B\in ℂ\right)\wedge \left(\cos A\ne 0\wedge \cos B\ne 0\wedge \cos \left(A+B\right)\ne 0\right)\right)\to \tan \left(A+B\right)=\frac{\tan A+\tan B}{1-\tan A\tan B}$$