tanval3

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

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

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$⊢ i \in ℂ$
2		simpl	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to A \in ℂ$
3		mulcl	$⊢ (i \in ℂ \land A \in ℂ) \to i A \in ℂ$
4	1 2 3	sylancr	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to i A \in ℂ$
5		efcl	$⊢ i A \in ℂ \to e^{i A} \in ℂ$
6	4 5	syl	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to e^{i A} \in ℂ$
7		negicn	$⊢ - i \in ℂ$
8		mulcl	$⊢ (- i \in ℂ \land A \in ℂ) \to (- i) A \in ℂ$
9	7 2 8	sylancr	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to (- i) A \in ℂ$
10		efcl	$⊢ (- i) A \in ℂ \to e^{(- i) A} \in ℂ$
11	9 10	syl	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to e^{(- i) A} \in ℂ$
12	6 11	subcld	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to e^{i A} - e^{(- i) A} \in ℂ$
13	6 11	addcld	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to e^{i A} + e^{(- i) A} \in ℂ$
14		mulcl	$⊢ (i \in ℂ \land e^{i A} + e^{(- i) A} \in ℂ) \to i (e^{i A} + e^{(- i) A}) \in ℂ$
15	1 13 14	sylancr	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to i (e^{i A} + e^{(- i) A}) \in ℂ$
16		2z	$⊢ 2 \in ℤ$
17		efexp	$⊢ (i A \in ℂ \land 2 \in ℤ) \to e^{2 i A} = {e^{i A}}^{2}$
18	4 16 17	sylancl	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to e^{2 i A} = {e^{i A}}^{2}$
19	6	sqvald	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to {e^{i A}}^{2} = e^{i A} e^{i A}$
20	18 19	eqtrd	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to e^{2 i A} = e^{i A} e^{i A}$
21		mulneg1	$⊢ (i \in ℂ \land A \in ℂ) \to (- i) A = - i A$
22	1 2 21	sylancr	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to (- i) A = - i A$
23	22	fveq2d	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to e^{(- i) A} = e^{- i A}$
24	23	oveq2d	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to e^{i A} e^{(- i) A} = e^{i A} e^{- i A}$
25		efcan	$⊢ i A \in ℂ \to e^{i A} e^{- i A} = 1$
26	4 25	syl	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to e^{i A} e^{- i A} = 1$
27	24 26	eqtr2d	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to 1 = e^{i A} e^{(- i) A}$
28	20 27	oveq12d	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to e^{2 i A} + 1 = e^{i A} e^{i A} + e^{i A} e^{(- i) A}$
29	6 6 11	adddid	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to e^{i A} (e^{i A} + e^{(- i) A}) = e^{i A} e^{i A} + e^{i A} e^{(- i) A}$
30	28 29	eqtr4d	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to e^{2 i A} + 1 = e^{i A} (e^{i A} + e^{(- i) A})$
31	30	oveq2d	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to i (e^{2 i A} + 1) = i e^{i A} (e^{i A} + e^{(- i) A})$
32	1	a1i	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to i \in ℂ$
33	32 6 13	mul12d	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to i e^{i A} (e^{i A} + e^{(- i) A}) = e^{i A} i (e^{i A} + e^{(- i) A})$
34	31 33	eqtrd	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to i (e^{2 i A} + 1) = e^{i A} i (e^{i A} + e^{(- i) A})$
35		2cn	$⊢ 2 \in ℂ$
36		mulcl	$⊢ (2 \in ℂ \land i A \in ℂ) \to 2 i A \in ℂ$
37	35 4 36	sylancr	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to 2 i A \in ℂ$
38		efcl	$⊢ 2 i A \in ℂ \to e^{2 i A} \in ℂ$
39	37 38	syl	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to e^{2 i A} \in ℂ$
40		ax-1cn	$⊢ 1 \in ℂ$
41		addcl	$⊢ (e^{2 i A} \in ℂ \land 1 \in ℂ) \to e^{2 i A} + 1 \in ℂ$
42	39 40 41	sylancl	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to e^{2 i A} + 1 \in ℂ$
43		ine0	$⊢ i \neq 0$
44	43	a1i	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to i \neq 0$
45		simpr	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to e^{2 i A} + 1 \neq 0$
46	32 42 44 45	mulne0d	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to i (e^{2 i A} + 1) \neq 0$
47	34 46	eqnetrrd	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to e^{i A} i (e^{i A} + e^{(- i) A}) \neq 0$
48	6 15 47	mulne0bbd	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to i (e^{i A} + e^{(- i) A}) \neq 0$
49		efne0	$⊢ i A \in ℂ \to e^{i A} \neq 0$
50	4 49	syl	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to e^{i A} \neq 0$
51	12 15 6 48 50	divcan5d	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to \frac{e^{i A} (e^{i A} - 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})}$
52	20 27	oveq12d	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to e^{2 i A} - 1 = e^{i A} e^{i A} - e^{i A} e^{(- i) A}$
53	6 6 11	subdid	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to e^{i A} (e^{i A} - e^{(- i) A}) = e^{i A} e^{i A} - e^{i A} e^{(- i) A}$
54	52 53	eqtr4d	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to e^{2 i A} - 1 = e^{i A} (e^{i A} - e^{(- i) A})$
55	54 34	oveq12d	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to \frac{e^{2 i A} - 1}{i (e^{2 i A} + 1)} = \frac{e^{i A} (e^{i A} - e^{(- i) A})}{e^{i A} i (e^{i A} + e^{(- i) A})}$
56		cosval	$⊢ A \in ℂ \to \cos A = \frac{e^{i A} + e^{(- i) A}}{2}$
57	56	adantr	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to \cos A = \frac{e^{i A} + e^{(- i) A}}{2}$
58		2cnd	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to 2 \in ℂ$
59	32 13 48	mulne0bbd	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to e^{i A} + e^{(- i) A} \neq 0$
60		2ne0	$⊢ 2 \neq 0$
61	60	a1i	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to 2 \neq 0$
62	13 58 59 61	divne0d	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to \frac{e^{i A} + e^{(- i) A}}{2} \neq 0$
63	57 62	eqnetrd	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to \cos A \neq 0$
64		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})}$
65	63 64	syldan	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to \tan A = \frac{e^{i A} - e^{(- i) A}}{i (e^{i A} + e^{(- i) A})}$
66	51 55 65	3eqtr4rd	$⊢ (A \in ℂ \land e^{2 i A} + 1 \neq 0) \to \tan A = \frac{e^{2 i A} - 1}{i (e^{2 i A} + 1)}$

Metamath Proof Explorer

Theorem tanval3

Proof