demoivreALT

Description: Alternate proof of demoivre . It is longer but does not use the exponential function. This is Metamath 100 proof #17. (Contributed by Steve Rodriguez, 10-Nov-2006) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	demoivreALT	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to {(\cos A + i \sin A)}^{N} = \cos N A + i \sin N A$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = 0 \to {(\cos A + i \sin A)}^{x} = {(\cos A + i \sin A)}^{0}$
2		oveq1	$⊢ x = 0 \to x A = 0 \cdot A$
3	2	fveq2d	$⊢ x = 0 \to \cos x A = \cos 0 \cdot A$
4	2	fveq2d	$⊢ x = 0 \to \sin x A = \sin 0 \cdot A$
5	4	oveq2d	$⊢ x = 0 \to i \sin x A = i \sin 0 \cdot A$
6	3 5	oveq12d	$⊢ x = 0 \to \cos x A + i \sin x A = \cos 0 \cdot A + i \sin 0 \cdot A$
7	1 6	eqeq12d	$⊢ x = 0 \to ({(\cos A + i \sin A)}^{x} = \cos x A + i \sin x A \leftrightarrow {(\cos A + i \sin A)}^{0} = \cos 0 \cdot A + i \sin 0 \cdot A)$
8	7	imbi2d	$⊢ x = 0 \to ((A \in ℂ \to {(\cos A + i \sin A)}^{x} = \cos x A + i \sin x A) \leftrightarrow (A \in ℂ \to {(\cos A + i \sin A)}^{0} = \cos 0 \cdot A + i \sin 0 \cdot A))$
9		oveq2	$⊢ x = k \to {(\cos A + i \sin A)}^{x} = {(\cos A + i \sin A)}^{k}$
10		oveq1	$⊢ x = k \to x A = k A$
11	10	fveq2d	$⊢ x = k \to \cos x A = \cos k A$
12	10	fveq2d	$⊢ x = k \to \sin x A = \sin k A$
13	12	oveq2d	$⊢ x = k \to i \sin x A = i \sin k A$
14	11 13	oveq12d	$⊢ x = k \to \cos x A + i \sin x A = \cos k A + i \sin k A$
15	9 14	eqeq12d	$⊢ x = k \to ({(\cos A + i \sin A)}^{x} = \cos x A + i \sin x A \leftrightarrow {(\cos A + i \sin A)}^{k} = \cos k A + i \sin k A)$
16	15	imbi2d	$⊢ x = k \to ((A \in ℂ \to {(\cos A + i \sin A)}^{x} = \cos x A + i \sin x A) \leftrightarrow (A \in ℂ \to {(\cos A + i \sin A)}^{k} = \cos k A + i \sin k A))$
17		oveq2	$⊢ x = k + 1 \to {(\cos A + i \sin A)}^{x} = {(\cos A + i \sin A)}^{k + 1}$
18		oveq1	$⊢ x = k + 1 \to x A = (k + 1) A$
19	18	fveq2d	$⊢ x = k + 1 \to \cos x A = \cos (k + 1) A$
20	18	fveq2d	$⊢ x = k + 1 \to \sin x A = \sin (k + 1) A$
21	20	oveq2d	$⊢ x = k + 1 \to i \sin x A = i \sin (k + 1) A$
22	19 21	oveq12d	$⊢ x = k + 1 \to \cos x A + i \sin x A = \cos (k + 1) A + i \sin (k + 1) A$
23	17 22	eqeq12d	$⊢ x = k + 1 \to ({(\cos A + i \sin A)}^{x} = \cos x A + i \sin x A \leftrightarrow {(\cos A + i \sin A)}^{k + 1} = \cos (k + 1) A + i \sin (k + 1) A)$
24	23	imbi2d	$⊢ x = k + 1 \to ((A \in ℂ \to {(\cos A + i \sin A)}^{x} = \cos x A + i \sin x A) \leftrightarrow (A \in ℂ \to {(\cos A + i \sin A)}^{k + 1} = \cos (k + 1) A + i \sin (k + 1) A))$
25		oveq2	$⊢ x = N \to {(\cos A + i \sin A)}^{x} = {(\cos A + i \sin A)}^{N}$
26		oveq1	$⊢ x = N \to x A = N A$
27	26	fveq2d	$⊢ x = N \to \cos x A = \cos N A$
28	26	fveq2d	$⊢ x = N \to \sin x A = \sin N A$
29	28	oveq2d	$⊢ x = N \to i \sin x A = i \sin N A$
30	27 29	oveq12d	$⊢ x = N \to \cos x A + i \sin x A = \cos N A + i \sin N A$
31	25 30	eqeq12d	$⊢ x = N \to ({(\cos A + i \sin A)}^{x} = \cos x A + i \sin x A \leftrightarrow {(\cos A + i \sin A)}^{N} = \cos N A + i \sin N A)$
32	31	imbi2d	$⊢ x = N \to ((A \in ℂ \to {(\cos A + i \sin A)}^{x} = \cos x A + i \sin x A) \leftrightarrow (A \in ℂ \to {(\cos A + i \sin A)}^{N} = \cos N A + i \sin N A))$
33		coscl	$⊢ A \in ℂ \to \cos A \in ℂ$
34		ax-icn	$⊢ i \in ℂ$
35		sincl	$⊢ A \in ℂ \to \sin A \in ℂ$
36		mulcl	$⊢ (i \in ℂ \land \sin A \in ℂ) \to i \sin A \in ℂ$
37	34 35 36	sylancr	$⊢ A \in ℂ \to i \sin A \in ℂ$
38		addcl	$⊢ (\cos A \in ℂ \land i \sin A \in ℂ) \to \cos A + i \sin A \in ℂ$
39	33 37 38	syl2anc	$⊢ A \in ℂ \to \cos A + i \sin A \in ℂ$
40		exp0	$⊢ \cos A + i \sin A \in ℂ \to {(\cos A + i \sin A)}^{0} = 1$
41	39 40	syl	$⊢ A \in ℂ \to {(\cos A + i \sin A)}^{0} = 1$
42		mul02	$⊢ A \in ℂ \to 0 \cdot A = 0$
43	42	fveq2d	$⊢ A \in ℂ \to \cos 0 \cdot A = \cos 0$
44		cos0	$⊢ \cos 0 = 1$
45	43 44	eqtrdi	$⊢ A \in ℂ \to \cos 0 \cdot A = 1$
46	42	fveq2d	$⊢ A \in ℂ \to \sin 0 \cdot A = \sin 0$
47		sin0	$⊢ \sin 0 = 0$
48	46 47	eqtrdi	$⊢ A \in ℂ \to \sin 0 \cdot A = 0$
49	48	oveq2d	$⊢ A \in ℂ \to i \sin 0 \cdot A = i \cdot 0$
50	34	mul01i	$⊢ i \cdot 0 = 0$
51	49 50	eqtrdi	$⊢ A \in ℂ \to i \sin 0 \cdot A = 0$
52	45 51	oveq12d	$⊢ A \in ℂ \to \cos 0 \cdot A + i \sin 0 \cdot A = 1 + 0$
53		ax-1cn	$⊢ 1 \in ℂ$
54	53	addridi	$⊢ 1 + 0 = 1$
55	52 54	eqtrdi	$⊢ A \in ℂ \to \cos 0 \cdot A + i \sin 0 \cdot A = 1$
56	41 55	eqtr4d	$⊢ A \in ℂ \to {(\cos A + i \sin A)}^{0} = \cos 0 \cdot A + i \sin 0 \cdot A$
57		expp1	$⊢ (\cos A + i \sin A \in ℂ \land k \in ℕ_{0}) \to {(\cos A + i \sin A)}^{k + 1} = {(\cos A + i \sin A)}^{k} (\cos A + i \sin A)$
58	39 57	sylan	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to {(\cos A + i \sin A)}^{k + 1} = {(\cos A + i \sin A)}^{k} (\cos A + i \sin A)$
59	58	ancoms	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to {(\cos A + i \sin A)}^{k + 1} = {(\cos A + i \sin A)}^{k} (\cos A + i \sin A)$
60	59	adantr	$⊢ ((k \in ℕ_{0} \land A \in ℂ) \land {(\cos A + i \sin A)}^{k} = \cos k A + i \sin k A) \to {(\cos A + i \sin A)}^{k + 1} = {(\cos A + i \sin A)}^{k} (\cos A + i \sin A)$
61		oveq1	$⊢ {(\cos A + i \sin A)}^{k} = \cos k A + i \sin k A \to {(\cos A + i \sin A)}^{k} (\cos A + i \sin A) = (\cos k A + i \sin k A) (\cos A + i \sin A)$
62	61	adantl	$⊢ ((k \in ℕ_{0} \land A \in ℂ) \land {(\cos A + i \sin A)}^{k} = \cos k A + i \sin k A) \to {(\cos A + i \sin A)}^{k} (\cos A + i \sin A) = (\cos k A + i \sin k A) (\cos A + i \sin A)$
63		nn0cn	$⊢ k \in ℕ_{0} \to k \in ℂ$
64		mulcl	$⊢ (k \in ℂ \land A \in ℂ) \to k A \in ℂ$
65	63 64	sylan	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to k A \in ℂ$
66		sinadd	$⊢ (k A \in ℂ \land A \in ℂ) \to \sin (k A + A) = \sin k A \cos A + \cos k A \sin A$
67	65 66	sylancom	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \sin (k A + A) = \sin k A \cos A + \cos k A \sin A$
68	33	adantl	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos A \in ℂ$
69		sincl	$⊢ k A \in ℂ \to \sin k A \in ℂ$
70	65 69	syl	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \sin k A \in ℂ$
71		mulcom	$⊢ (\cos A \in ℂ \land \sin k A \in ℂ) \to \cos A \sin k A = \sin k A \cos A$
72	68 70 71	syl2anc	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos A \sin k A = \sin k A \cos A$
73	72	oveq1d	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos A \sin k A + \cos k A \sin A = \sin k A \cos A + \cos k A \sin A$
74		mulcl	$⊢ (\cos A \in ℂ \land \sin k A \in ℂ) \to \cos A \sin k A \in ℂ$
75	68 70 74	syl2anc	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos A \sin k A \in ℂ$
76		coscl	$⊢ k A \in ℂ \to \cos k A \in ℂ$
77	65 76	syl	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos k A \in ℂ$
78	35	adantl	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \sin A \in ℂ$
79		mulcl	$⊢ (\cos k A \in ℂ \land \sin A \in ℂ) \to \cos k A \sin A \in ℂ$
80	77 78 79	syl2anc	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos k A \sin A \in ℂ$
81		addcom	$⊢ (\cos A \sin k A \in ℂ \land \cos k A \sin A \in ℂ) \to \cos A \sin k A + \cos k A \sin A = \cos k A \sin A + \cos A \sin k A$
82	75 80 81	syl2anc	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos A \sin k A + \cos k A \sin A = \cos k A \sin A + \cos A \sin k A$
83	67 73 82	3eqtr2d	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \sin (k A + A) = \cos k A \sin A + \cos A \sin k A$
84	83	oveq2d	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to i \sin (k A + A) = i (\cos k A \sin A + \cos A \sin k A)$
85	84	oveq2d	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos (k A + A) + i \sin (k A + A) = \cos (k A + A) + i (\cos k A \sin A + \cos A \sin k A)$
86		adddir	$⊢ (k \in ℂ \land 1 \in ℂ \land A \in ℂ) \to (k + 1) A = k A + 1 A$
87		mullid	$⊢ A \in ℂ \to 1 A = A$
88	87	oveq2d	$⊢ A \in ℂ \to k A + 1 A = k A + A$
89	88	3ad2ant3	$⊢ (k \in ℂ \land 1 \in ℂ \land A \in ℂ) \to k A + 1 A = k A + A$
90	86 89	eqtrd	$⊢ (k \in ℂ \land 1 \in ℂ \land A \in ℂ) \to (k + 1) A = k A + A$
91	63 90	syl3an1	$⊢ (k \in ℕ_{0} \land 1 \in ℂ \land A \in ℂ) \to (k + 1) A = k A + A$
92	53 91	mp3an2	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to (k + 1) A = k A + A$
93	92	fveq2d	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos (k + 1) A = \cos (k A + A)$
94	92	fveq2d	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \sin (k + 1) A = \sin (k A + A)$
95	94	oveq2d	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to i \sin (k + 1) A = i \sin (k A + A)$
96	93 95	oveq12d	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos (k + 1) A + i \sin (k + 1) A = \cos (k A + A) + i \sin (k A + A)$
97		mulcl	$⊢ (i \in ℂ \land \sin k A \in ℂ) \to i \sin k A \in ℂ$
98	34 97	mpan	$⊢ \sin k A \in ℂ \to i \sin k A \in ℂ$
99	65 69 98	3syl	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to i \sin k A \in ℂ$
100	33 37	jca	$⊢ A \in ℂ \to (\cos A \in ℂ \land i \sin A \in ℂ)$
101	100	adantl	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to (\cos A \in ℂ \land i \sin A \in ℂ)$
102		muladd	$⊢ ((\cos k A \in ℂ \land i \sin k A \in ℂ) \land (\cos A \in ℂ \land i \sin A \in ℂ)) \to (\cos k A + i \sin k A) (\cos A + i \sin A) = \cos k A \cos A + i \sin A i \sin k A + \cos k A i \sin A + \cos A i \sin k A$
103	77 99 101 102	syl21anc	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to (\cos k A + i \sin k A) (\cos A + i \sin A) = \cos k A \cos A + i \sin A i \sin k A + \cos k A i \sin A + \cos A i \sin k A$
104	78 34	jctil	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to (i \in ℂ \land \sin A \in ℂ)$
105	70 34	jctil	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to (i \in ℂ \land \sin k A \in ℂ)$
106		mul4	$⊢ ((i \in ℂ \land \sin A \in ℂ) \land (i \in ℂ \land \sin k A \in ℂ)) \to i \sin A i \sin k A = i i \sin A \sin k A$
107		ixi	$⊢ i i = - 1$
108	107	oveq1i	$⊢ i i \sin A \sin k A = -1 \sin A \sin k A$
109	106 108	eqtrdi	$⊢ ((i \in ℂ \land \sin A \in ℂ) \land (i \in ℂ \land \sin k A \in ℂ)) \to i \sin A i \sin k A = -1 \sin A \sin k A$
110	104 105 109	syl2anc	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to i \sin A i \sin k A = -1 \sin A \sin k A$
111	110	oveq2d	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos k A \cos A + i \sin A i \sin k A = \cos k A \cos A + -1 \sin A \sin k A$
112	111	oveq1d	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos k A \cos A + i \sin A i \sin k A + \cos k A i \sin A + \cos A i \sin k A = \cos k A \cos A + -1 \sin A \sin k A + \cos k A i \sin A + \cos A i \sin k A$
113		mul12	$⊢ (\cos k A \in ℂ \land i \in ℂ \land \sin A \in ℂ) \to \cos k A i \sin A = i \cos k A \sin A$
114	34 113	mp3an2	$⊢ (\cos k A \in ℂ \land \sin A \in ℂ) \to \cos k A i \sin A = i \cos k A \sin A$
115	77 78 114	syl2anc	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos k A i \sin A = i \cos k A \sin A$
116		mul12	$⊢ (\cos A \in ℂ \land i \in ℂ \land \sin k A \in ℂ) \to \cos A i \sin k A = i \cos A \sin k A$
117	34 116	mp3an2	$⊢ (\cos A \in ℂ \land \sin k A \in ℂ) \to \cos A i \sin k A = i \cos A \sin k A$
118	68 70 117	syl2anc	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos A i \sin k A = i \cos A \sin k A$
119	115 118	oveq12d	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos k A i \sin A + \cos A i \sin k A = i \cos k A \sin A + i \cos A \sin k A$
120		adddi	$⊢ (i \in ℂ \land \cos k A \sin A \in ℂ \land \cos A \sin k A \in ℂ) \to i (\cos k A \sin A + \cos A \sin k A) = i \cos k A \sin A + i \cos A \sin k A$
121	34 120	mp3an1	$⊢ (\cos k A \sin A \in ℂ \land \cos A \sin k A \in ℂ) \to i (\cos k A \sin A + \cos A \sin k A) = i \cos k A \sin A + i \cos A \sin k A$
122	80 75 121	syl2anc	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to i (\cos k A \sin A + \cos A \sin k A) = i \cos k A \sin A + i \cos A \sin k A$
123	119 122	eqtr4d	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos k A i \sin A + \cos A i \sin k A = i (\cos k A \sin A + \cos A \sin k A)$
124	123	oveq2d	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos k A \cos A + -1 \sin A \sin k A + \cos k A i \sin A + \cos A i \sin k A = \cos k A \cos A + -1 \sin A \sin k A + i (\cos k A \sin A + \cos A \sin k A)$
125	103 112 124	3eqtrd	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to (\cos k A + i \sin k A) (\cos A + i \sin A) = \cos k A \cos A + -1 \sin A \sin k A + i (\cos k A \sin A + \cos A \sin k A)$
126		mulcl	$⊢ (\sin A \in ℂ \land \sin k A \in ℂ) \to \sin A \sin k A \in ℂ$
127	78 70 126	syl2anc	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \sin A \sin k A \in ℂ$
128		mulm1	$⊢ \sin A \sin k A \in ℂ \to -1 \sin A \sin k A = - \sin A \sin k A$
129	127 128	syl	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to -1 \sin A \sin k A = - \sin A \sin k A$
130	129	oveq2d	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos k A \cos A + -1 \sin A \sin k A = \cos k A \cos A + (- \sin A \sin k A)$
131	130	oveq1d	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos k A \cos A + -1 \sin A \sin k A + i (\cos k A \sin A + \cos A \sin k A) = \cos k A \cos A + (- \sin A \sin k A) + i (\cos k A \sin A + \cos A \sin k A)$
132		mulcl	$⊢ (\cos k A \in ℂ \land \cos A \in ℂ) \to \cos k A \cos A \in ℂ$
133	77 68 132	syl2anc	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos k A \cos A \in ℂ$
134		negsub	$⊢ (\cos k A \cos A \in ℂ \land \sin A \sin k A \in ℂ) \to \cos k A \cos A + (- \sin A \sin k A) = \cos k A \cos A - \sin A \sin k A$
135	133 127 134	syl2anc	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos k A \cos A + (- \sin A \sin k A) = \cos k A \cos A - \sin A \sin k A$
136	135	oveq1d	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos k A \cos A + (- \sin A \sin k A) + i (\cos k A \sin A + \cos A \sin k A) = \cos k A \cos A - \sin A \sin k A + i (\cos k A \sin A + \cos A \sin k A)$
137	125 131 136	3eqtrd	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to (\cos k A + i \sin k A) (\cos A + i \sin A) = \cos k A \cos A - \sin A \sin k A + i (\cos k A \sin A + \cos A \sin k A)$
138		cosadd	$⊢ (k A \in ℂ \land A \in ℂ) \to \cos (k A + A) = \cos k A \cos A - \sin k A \sin A$
139	65 138	sylancom	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos (k A + A) = \cos k A \cos A - \sin k A \sin A$
140		mulcom	$⊢ (\sin k A \in ℂ \land \sin A \in ℂ) \to \sin k A \sin A = \sin A \sin k A$
141	70 78 140	syl2anc	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \sin k A \sin A = \sin A \sin k A$
142	141	oveq2d	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos k A \cos A - \sin k A \sin A = \cos k A \cos A - \sin A \sin k A$
143	139 142	eqtrd	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos (k A + A) = \cos k A \cos A - \sin A \sin k A$
144	143	oveq1d	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to \cos (k A + A) + i (\cos k A \sin A + \cos A \sin k A) = \cos k A \cos A - \sin A \sin k A + i (\cos k A \sin A + \cos A \sin k A)$
145	137 144	eqtr4d	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to (\cos k A + i \sin k A) (\cos A + i \sin A) = \cos (k A + A) + i (\cos k A \sin A + \cos A \sin k A)$
146	85 96 145	3eqtr4rd	$⊢ (k \in ℕ_{0} \land A \in ℂ) \to (\cos k A + i \sin k A) (\cos A + i \sin A) = \cos (k + 1) A + i \sin (k + 1) A$
147	146	adantr	$⊢ ((k \in ℕ_{0} \land A \in ℂ) \land {(\cos A + i \sin A)}^{k} = \cos k A + i \sin k A) \to (\cos k A + i \sin k A) (\cos A + i \sin A) = \cos (k + 1) A + i \sin (k + 1) A$
148	60 62 147	3eqtrd	$⊢ ((k \in ℕ_{0} \land A \in ℂ) \land {(\cos A + i \sin A)}^{k} = \cos k A + i \sin k A) \to {(\cos A + i \sin A)}^{k + 1} = \cos (k + 1) A + i \sin (k + 1) A$
149	148	exp31	$⊢ k \in ℕ_{0} \to (A \in ℂ \to ({(\cos A + i \sin A)}^{k} = \cos k A + i \sin k A \to {(\cos A + i \sin A)}^{k + 1} = \cos (k + 1) A + i \sin (k + 1) A))$
150	149	a2d	$⊢ k \in ℕ_{0} \to ((A \in ℂ \to {(\cos A + i \sin A)}^{k} = \cos k A + i \sin k A) \to (A \in ℂ \to {(\cos A + i \sin A)}^{k + 1} = \cos (k + 1) A + i \sin (k + 1) A))$
151	8 16 24 32 56 150	nn0ind	$⊢ N \in ℕ_{0} \to (A \in ℂ \to {(\cos A + i \sin A)}^{N} = \cos N A + i \sin N A)$
152	151	impcom	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to {(\cos A + i \sin A)}^{N} = \cos N A + i \sin N A$

Metamath Proof Explorer

Theorem demoivreALT

Proof