tanval2

Description: Express the tangent function directly in terms of exp . (Contributed by Mario Carneiro, 25-Feb-2015)

		Ref	Expression
	Assertion	tanval2	$⊢ (A \in ℂ \land \cos A \neq 0) \to \tan A = \frac{e^{i A} - e^{(- i) A}}{i (e^{i A} + e^{(- i) A})}$

Proof

Step	Hyp	Ref	Expression
1		tanval	$⊢ (A \in ℂ \land \cos A \neq 0) \to \tan A = \frac{\sin A}{\cos A}$
2		2cn	$⊢ 2 \in ℂ$
3		ax-icn	$⊢ i \in ℂ$
4	2 3	mulcomi	$⊢ 2 i = i \cdot 2$
5	4	oveq2i	$⊢ \frac{e^{i A} - e^{(- i) A}}{2 i} = \frac{e^{i A} - e^{(- i) A}}{i \cdot 2}$
6		sinval	$⊢ A \in ℂ \to \sin A = \frac{e^{i A} - e^{(- i) A}}{2 i}$
7	6	adantr	$⊢ (A \in ℂ \land \cos A \neq 0) \to \sin A = \frac{e^{i A} - e^{(- i) A}}{2 i}$
8		simpl	$⊢ (A \in ℂ \land \cos A \neq 0) \to A \in ℂ$
9		mulcl	$⊢ (i \in ℂ \land A \in ℂ) \to i A \in ℂ$
10	3 8 9	sylancr	$⊢ (A \in ℂ \land \cos A \neq 0) \to i A \in ℂ$
11		efcl	$⊢ i A \in ℂ \to e^{i A} \in ℂ$
12	10 11	syl	$⊢ (A \in ℂ \land \cos A \neq 0) \to e^{i A} \in ℂ$
13		negicn	$⊢ - i \in ℂ$
14		mulcl	$⊢ (- i \in ℂ \land A \in ℂ) \to (- i) A \in ℂ$
15	13 8 14	sylancr	$⊢ (A \in ℂ \land \cos A \neq 0) \to (- i) A \in ℂ$
16		efcl	$⊢ (- i) A \in ℂ \to e^{(- i) A} \in ℂ$
17	15 16	syl	$⊢ (A \in ℂ \land \cos A \neq 0) \to e^{(- i) A} \in ℂ$
18	12 17	subcld	$⊢ (A \in ℂ \land \cos A \neq 0) \to e^{i A} - e^{(- i) A} \in ℂ$
19	3	a1i	$⊢ (A \in ℂ \land \cos A \neq 0) \to i \in ℂ$
20	2	a1i	$⊢ (A \in ℂ \land \cos A \neq 0) \to 2 \in ℂ$
21		ine0	$⊢ i \neq 0$
22	21	a1i	$⊢ (A \in ℂ \land \cos A \neq 0) \to i \neq 0$
23		2ne0	$⊢ 2 \neq 0$
24	23	a1i	$⊢ (A \in ℂ \land \cos A \neq 0) \to 2 \neq 0$
25	18 19 20 22 24	divdiv1d	$⊢ (A \in ℂ \land \cos A \neq 0) \to \frac{\frac{e^{i A} - e^{(- i) A}}{i}}{2} = \frac{e^{i A} - e^{(- i) A}}{i \cdot 2}$
26	5 7 25	3eqtr4a	$⊢ (A \in ℂ \land \cos A \neq 0) \to \sin A = \frac{\frac{e^{i A} - e^{(- i) A}}{i}}{2}$
27		cosval	$⊢ A \in ℂ \to \cos A = \frac{e^{i A} + e^{(- i) A}}{2}$
28	27	adantr	$⊢ (A \in ℂ \land \cos A \neq 0) \to \cos A = \frac{e^{i A} + e^{(- i) A}}{2}$
29	26 28	oveq12d	$⊢ (A \in ℂ \land \cos A \neq 0) \to \frac{\sin A}{\cos A} = \frac{\frac{\frac{e^{i A} - e^{(- i) A}}{i}}{2}}{\frac{e^{i A} + e^{(- i) A}}{2}}$
30	1 29	eqtrd	$⊢ (A \in ℂ \land \cos A \neq 0) \to \tan A = \frac{\frac{\frac{e^{i A} - e^{(- i) A}}{i}}{2}}{\frac{e^{i A} + e^{(- i) A}}{2}}$
31	18 19 22	divcld	$⊢ (A \in ℂ \land \cos A \neq 0) \to \frac{e^{i A} - e^{(- i) A}}{i} \in ℂ$
32	12 17	addcld	$⊢ (A \in ℂ \land \cos A \neq 0) \to e^{i A} + e^{(- i) A} \in ℂ$
33		simpr	$⊢ (A \in ℂ \land \cos A \neq 0) \to \cos A \neq 0$
34	28 33	eqnetrrd	$⊢ (A \in ℂ \land \cos A \neq 0) \to \frac{e^{i A} + e^{(- i) A}}{2} \neq 0$
35	32 20 24	diveq0ad	$⊢ (A \in ℂ \land \cos A \neq 0) \to (\frac{e^{i A} + e^{(- i) A}}{2} = 0 \leftrightarrow e^{i A} + e^{(- i) A} = 0)$
36	35	necon3bid	$⊢ (A \in ℂ \land \cos A \neq 0) \to (\frac{e^{i A} + e^{(- i) A}}{2} \neq 0 \leftrightarrow e^{i A} + e^{(- i) A} \neq 0)$
37	34 36	mpbid	$⊢ (A \in ℂ \land \cos A \neq 0) \to e^{i A} + e^{(- i) A} \neq 0$
38	31 32 20 37 24	divcan7d	$⊢ (A \in ℂ \land \cos A \neq 0) \to \frac{\frac{\frac{e^{i A} - e^{(- i) A}}{i}}{2}}{\frac{e^{i A} + e^{(- i) A}}{2}} = \frac{\frac{e^{i A} - e^{(- i) A}}{i}}{e^{i A} + e^{(- i) A}}$
39	18 19 32 22 37	divdiv1d	$⊢ (A \in ℂ \land \cos A \neq 0) \to \frac{\frac{e^{i A} - e^{(- i) A}}{i}}{e^{i A} + e^{(- i) A}} = \frac{e^{i A} - e^{(- i) A}}{i (e^{i A} + e^{(- i) A})}$
40	30 38 39	3eqtrd	$⊢ (A \in ℂ \land \cos A \neq 0) \to \tan A = \frac{e^{i A} - e^{(- i) A}}{i (e^{i A} + e^{(- i) A})}$

Metamath Proof Explorer

Theorem tanval2

Proof