demoivre

Description: De Moivre's Formula. Proof by induction given at http://en.wikipedia.org/wiki/De_Moivre's_formula , but restricted to nonnegative integer powers. See also demoivreALT for an alternate longer proof not using the exponential function. (Contributed by NM, 24-Jul-2007)

		Ref	Expression
	Assertion	demoivre	$⊢ (A \in ℂ \land N \in ℤ) \to {(\cos A + i \sin A)}^{N} = \cos N A + i \sin N A$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$⊢ i \in ℂ$
2		mulcl	$⊢ (i \in ℂ \land A \in ℂ) \to i A \in ℂ$
3	1 2	mpan	$⊢ A \in ℂ \to i A \in ℂ$
4		efexp	$⊢ (i A \in ℂ \land N \in ℤ) \to e^{N i A} = {e^{i A}}^{N}$
5	3 4	sylan	$⊢ (A \in ℂ \land N \in ℤ) \to e^{N i A} = {e^{i A}}^{N}$
6		zcn	$⊢ N \in ℤ \to N \in ℂ$
7		mul12	$⊢ (N \in ℂ \land i \in ℂ \land A \in ℂ) \to N i A = i N A$
8	1 7	mp3an2	$⊢ (N \in ℂ \land A \in ℂ) \to N i A = i N A$
9	8	fveq2d	$⊢ (N \in ℂ \land A \in ℂ) \to e^{N i A} = e^{i N A}$
10		mulcl	$⊢ (N \in ℂ \land A \in ℂ) \to N A \in ℂ$
11		efival	$⊢ N A \in ℂ \to e^{i N A} = \cos N A + i \sin N A$
12	10 11	syl	$⊢ (N \in ℂ \land A \in ℂ) \to e^{i N A} = \cos N A + i \sin N A$
13	9 12	eqtrd	$⊢ (N \in ℂ \land A \in ℂ) \to e^{N i A} = \cos N A + i \sin N A$
14	13	ancoms	$⊢ (A \in ℂ \land N \in ℂ) \to e^{N i A} = \cos N A + i \sin N A$
15	6 14	sylan2	$⊢ (A \in ℂ \land N \in ℤ) \to e^{N i A} = \cos N A + i \sin N A$
16		efival	$⊢ A \in ℂ \to e^{i A} = \cos A + i \sin A$
17	16	oveq1d	$⊢ A \in ℂ \to {e^{i A}}^{N} = {(\cos A + i \sin A)}^{N}$
18	17	adantr	$⊢ (A \in ℂ \land N \in ℤ) \to {e^{i A}}^{N} = {(\cos A + i \sin A)}^{N}$
19	5 15 18	3eqtr3rd	$⊢ (A \in ℂ \land N \in ℤ) \to {(\cos A + i \sin A)}^{N} = \cos N A + i \sin N A$

Metamath Proof Explorer

Theorem demoivre

Proof