resinval

Description: The sine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005)

		Ref	Expression
	Assertion	resinval	$⊢ A \in ℝ \to \sin A = ℑ (e^{i A})$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$⊢ i \in ℂ$
2		recn	$⊢ A \in ℝ \to A \in ℂ$
3		cjmul	$⊢ (i \in ℂ \land A \in ℂ) \to \overline{i A} = \overline{i} \overline{A}$
4	1 2 3	sylancr	$⊢ A \in ℝ \to \overline{i A} = \overline{i} \overline{A}$
5		cji	$⊢ \overline{i} = - i$
6	5	oveq1i	$⊢ \overline{i} \overline{A} = (- i) \overline{A}$
7		cjre	$⊢ A \in ℝ \to \overline{A} = A$
8	7	oveq2d	$⊢ A \in ℝ \to (- i) \overline{A} = (- i) A$
9	6 8	syl5eq	$⊢ A \in ℝ \to \overline{i} \overline{A} = (- i) A$
10	4 9	eqtrd	$⊢ A \in ℝ \to \overline{i A} = (- i) A$
11	10	fveq2d	$⊢ A \in ℝ \to e^{\overline{i A}} = e^{(- i) A}$
12		mulcl	$⊢ (i \in ℂ \land A \in ℂ) \to i A \in ℂ$
13	1 2 12	sylancr	$⊢ A \in ℝ \to i A \in ℂ$
14		efcj	$⊢ i A \in ℂ \to e^{\overline{i A}} = \overline{e^{i A}}$
15	13 14	syl	$⊢ A \in ℝ \to e^{\overline{i A}} = \overline{e^{i A}}$
16	11 15	eqtr3d	$⊢ A \in ℝ \to e^{(- i) A} = \overline{e^{i A}}$
17	16	oveq2d	$⊢ A \in ℝ \to e^{i A} - e^{(- i) A} = e^{i A} - \overline{e^{i A}}$
18	17	oveq1d	$⊢ A \in ℝ \to \frac{e^{i A} - e^{(- i) A}}{2 i} = \frac{e^{i A} - \overline{e^{i A}}}{2 i}$
19		sinval	$⊢ A \in ℂ \to \sin A = \frac{e^{i A} - e^{(- i) A}}{2 i}$
20	2 19	syl	$⊢ A \in ℝ \to \sin A = \frac{e^{i A} - e^{(- i) A}}{2 i}$
21		efcl	$⊢ i A \in ℂ \to e^{i A} \in ℂ$
22		imval2	$⊢ e^{i A} \in ℂ \to ℑ (e^{i A}) = \frac{e^{i A} - \overline{e^{i A}}}{2 i}$
23	13 21 22	3syl	$⊢ A \in ℝ \to ℑ (e^{i A}) = \frac{e^{i A} - \overline{e^{i A}}}{2 i}$
24	18 20 23	3eqtr4d	$⊢ A \in ℝ \to \sin A = ℑ (e^{i A})$

Metamath Proof Explorer

Theorem resinval

Proof