efimpi

Description: The exponential function at _i times a real number less _pi . (Contributed by Paul Chapman, 15-Mar-2008)

		Ref	Expression
	Assertion	efimpi	$⊢ A \in ℂ \to e^{i (A - π)} = - e^{i A}$

Step	Hyp	Ref	Expression
1		picn	$⊢ π \in ℂ$
2		subcl	$⊢ (A \in ℂ \land π \in ℂ) \to A - π \in ℂ$
3	1 2	mpan2	$⊢ A \in ℂ \to A - π \in ℂ$
4		efival	$⊢ A - π \in ℂ \to e^{i (A - π)} = \cos (A - π) + i \sin (A - π)$
5	3 4	syl	$⊢ A \in ℂ \to e^{i (A - π)} = \cos (A - π) + i \sin (A - π)$
6		coscl	$⊢ A \in ℂ \to \cos A \in ℂ$
7		ax-icn	$⊢ i \in ℂ$
8		sincl	$⊢ A \in ℂ \to \sin A \in ℂ$
9		mulcl	$⊢ (i \in ℂ \land \sin A \in ℂ) \to i \sin A \in ℂ$
10	7 8 9	sylancr	$⊢ A \in ℂ \to i \sin A \in ℂ$
11	6 10	negdid	$⊢ A \in ℂ \to - (\cos A + i \sin A) = - \cos A + (- i \sin A)$
12		cosmpi	$⊢ A \in ℂ \to \cos (A - π) = - \cos A$
13		sinmpi	$⊢ A \in ℂ \to \sin (A - π) = - \sin A$
14	13	oveq2d	$⊢ A \in ℂ \to i \sin (A - π) = i (- \sin A)$
15		mulneg2	$⊢ (i \in ℂ \land \sin A \in ℂ) \to i (- \sin A) = - i \sin A$
16	7 8 15	sylancr	$⊢ A \in ℂ \to i (- \sin A) = - i \sin A$
17	14 16	eqtrd	$⊢ A \in ℂ \to i \sin (A - π) = - i \sin A$
18	12 17	oveq12d	$⊢ A \in ℂ \to \cos (A - π) + i \sin (A - π) = - \cos A + (- i \sin A)$
19	11 18	eqtr4d	$⊢ A \in ℂ \to - (\cos A + i \sin A) = \cos (A - π) + i \sin (A - π)$
20	5 19	eqtr4d	$⊢ A \in ℂ \to e^{i (A - π)} = - (\cos A + i \sin A)$
21		efival	$⊢ A \in ℂ \to e^{i A} = \cos A + i \sin A$
22	21	negeqd	$⊢ A \in ℂ \to - e^{i A} = - (\cos A + i \sin A)$
23	20 22	eqtr4d	$⊢ A \in ℂ \to e^{i (A - π)} = - e^{i A}$

Metamath Proof Explorer