Theorem demoivre 7443

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. (Contributed by Steve Rodriguez, 10-Nov-2006.) Warning: The HTML proof page is 0.6 megabyte in size.

Assertion

Ref	Expression
demoivre	|- ((A e. CC /\ N e. NN0) -> (((cos` A) + (i x. (sin` A)))^N) = ((cos` (N x. A)) + (i x. (sin` (N x. A)))))

Proof of Theorem demoivre

Step	Hyp	Ref	Expression
1		opreq2 3964	. . . . 5 |- (x = 0 -> (((cos` A) + (i x. (sin` A)))^x) = (((cos` A) + (i x. (sin` A)))^0))
2		opreq1 3963	. . . . . . 7 |- (x = 0 -> (x x. A) = (0 x. A))
3	2	fveq2d 3723	. . . . . 6 |- (x = 0 -> (cos` (x x. A)) = (cos` (0 x. A)))
4	2	fveq2d 3723	. . . . . . 7 |- (x = 0 -> (sin` (x x. A)) = (sin` (0 x. A)))
5	4	opreq2d 3971	. . . . . 6 |- (x = 0 -> (i x. (sin` (x x. A))) = (i x. (sin` (0 x. A))))
6	3, 5	opreq12d 3973	. . . . 5 |- (x = 0 -> ((cos` (x x. A)) + (i x. (sin` (x x. A)))) = ((cos` (0 x. A)) + (i x. (sin` (0 x. A)))))
7	1, 6	eqeq12d 1487	. . . 4 |- (x = 0 -> ((((cos` A) + (i x. (sin` A)))^x) = ((cos` (x x. A)) + (i x. (sin` (x x. A)))) <-> (((cos` A) + (i x. (sin` A)))^0) = ((cos` (0 x. A)) + (i x. (sin` (0 x. A))))))
8	7	imbi2d 611	. . 3 |- (x = 0 -> ((A e. CC -> (((cos` A) + (i x. (sin` A)))^x) = ((cos` (x x. A)) + (i x. (sin` (x x. A))))) <-> (A e. CC -> (((cos` A) + (i x. (sin` A)))^0) = ((cos` (0 x. A)) + (i x. (sin` (0 x. A)))))))
9		opreq2 3964	. . . . 5 |- (x = k -> (((cos` A) + (i x. (sin` A)))^x) = (((cos` A) + (i x. (sin` A)))^k))
10		opreq1 3963	. . . . . . 7 |- (x = k -> (x x. A) = (k x. A))
11	10	fveq2d 3723	. . . . . 6 |- (x = k -> (cos` (x x. A)) = (cos` (k x. A)))
12	10	fveq2d 3723	. . . . . . 7 |- (x = k -> (sin` (x x. A)) = (sin` (k x. A)))
13	12	opreq2d 3971	. . . . . 6 |- (x = k -> (i x. (sin` (x x. A))) = (i x. (sin` (k x. A))))
14	11, 13	opreq12d 3973	. . . . 5 |- (x = k -> ((cos` (x x. A)) + (i x. (sin` (x x. A)))) = ((cos` (k x. A)) + (i x. (sin` (k x. A)))))
15	9, 14	eqeq12d 1487	. . . 4 |- (x = k -> ((((cos` A) + (i x. (sin` A)))^x) = ((cos` (x x. A)) + (i x. (sin` (x x. A)))) <-> (((cos` A) + (i x. (sin` A)))^k) = ((cos` (k x. A)) + (i x. (sin` (k x. A))))))
16	15	imbi2d 611	. . 3 |- (x = k -> ((A e. CC -> (((cos` A) + (i x. (sin` A)))^x) = ((cos` (x x. A)) + (i x. (sin` (x x. A))))) <-> (A e. CC -> (((cos` A) + (i x. (sin` A)))^k) = ((cos` (k x. A)) + (i x. (sin` (k x. A)))))))
17		opreq2 3964	. . . . 5 |- (x = (k + 1) -> (((cos` A) + (i x. (sin` A)))^x) = (((cos` A) + (i x. (sin` A)))^(k + 1)))
18		opreq1 3963	. . . . . . 7 |- (x = (k + 1) -> (x x. A) = ((k + 1) x. A))
19	18	fveq2d 3723	. . . . . 6 |- (x = (k + 1) -> (cos` (x x. A)) = (cos` ((k + 1) x. A)))
20	18	fveq2d 3723	. . . . . . 7 |- (x = (k + 1) -> (sin` (x x. A)) = (sin` ((k + 1) x. A)))
21	20	opreq2d 3971	. . . . . 6 |- (x = (k + 1) -> (i x. (sin` (x x. A))) = (i x. (sin` ((k + 1) x. A))))
22	19, 21	opreq12d 3973	. . . . 5 |- (x = (k + 1) -> ((cos` (x x. A)) + (i x. (sin` (x x. A)))) = ((cos` ((k + 1) x. A)) + (i x. (sin` ((k + 1) x. A)))))
23	17, 22	eqeq12d 1487	. . . 4 |- (x = (k + 1) -> ((((cos` A) + (i x. (sin` A)))^x) = ((cos` (x x. A)) + (i x. (sin` (x x. A)))) <-> (((cos` A) + (i x. (sin` A)))^(k + 1)) = ((cos` ((k + 1) x. A)) + (i x. (sin` ((k + 1) x. A))))))
24	23	imbi2d 611	. . 3 |- (x = (k + 1) -> ((A e. CC -> (((cos` A) + (i x. (sin` A)))^x) = ((cos` (x x. A)) + (i x. (sin` (x x. A))))) <-> (A e. CC -> (((cos` A) + (i x. (sin` A)))^(k + 1)) = ((cos` ((k + 1) x. A)) + (i x. (sin` ((k + 1) x. A)))))))
25		opreq2 3964	. . . . 5 |- (x = N -> (((cos` A) + (i x. (sin` A)))^x) = (((cos` A) + (i x. (sin` A)))^N))
26		opreq1 3963	. . . . . . 7 |- (x = N -> (x x. A) = (N x. A))
27	26	fveq2d 3723	. . . . . 6 |- (x = N -> (cos` (x x. A)) = (cos` (N x. A)))
28	26	fveq2d 3723	. . . . . . 7 |- (x = N -> (sin` (x x. A)) = (sin` (N x. A)))
29	28	opreq2d 3971	. . . . . 6 |- (x = N -> (i x. (sin` (x x. A))) = (i x. (sin` (N x. A))))
30	27, 29	opreq12d 3973	. . . . 5 |- (x = N -> ((cos` (x x. A)) + (i x. (sin` (x x. A)))) = ((cos` (N x. A)) + (i x. (sin` (N x. A)))))
31	25, 30	eqeq12d 1487	. . . 4 |- (x = N -> ((((cos` A) + (i x. (sin` A)))^x) = ((cos` (x x. A)) + (i x. (sin` (x x. A)))) <-> (((cos` A) + (i x. (sin` A)))^N) = ((cos` (N x. A)) + (i x. (sin` (N x. A))))))
32	31	imbi2d 611	. . 3 |- (x = N -> ((A e. CC -> (((cos` A) + (i x. (sin` A)))^x) = ((cos` (x x. A)) + (i x. (sin` (x x. A))))) <-> (A e. CC -> (((cos` A) + (i x. (sin` A)))^N) = ((cos` (N x. A)) + (i x. (sin` (N x. A)))))))
33		axaddcl 5254	. . . . . 6 |- (((cos` A) e. CC /\ (i x. (sin` A)) e. CC) -> ((cos` A) + (i x. (sin` A))) e. CC)
34		cosclt 7391	. . . . . 6 |- (A e. CC -> (cos` A) e. CC)
35		sinclt 7390	. . . . . . 7 |- (A e. CC -> (sin` A) e. CC)
36		axicn 5253	. . . . . . . 8 |- i e. CC
37		axmulcl 5256	. . . . . . . 8 |- ((i e. CC /\ (sin` A) e. CC) -> (i x. (sin` A)) e. CC)
38	36, 37	mpan 694	. . . . . . 7 |- ((sin` A) e. CC -> (i x. (sin` A)) e. CC)
39	35, 38	syl 10	. . . . . 6 |- (A e. CC -> (i x. (sin` A)) e. CC)
40	33, 34, 39	sylanc 471	. . . . 5 |- (A e. CC -> ((cos` A) + (i x. (sin` A))) e. CC)
41		exp0t 6516	. . . . 5 |- (((cos` A) + (i x. (sin` A))) e. CC -> (((cos` A) + (i x. (sin` A)))^0) = 1)
42	40, 41	syl 10	. . . 4 |- (A e. CC -> (((cos` A) + (i x.