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 e. CC /\ N e. NN0 ) -> ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) ^ N ) = ( ( cos ` ( N x. A ) ) + ( _i x. ( sin ` ( N x. A ) ) ) ) )

Proof

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

Metamath Proof Explorer

Theorem demoivreALT

Proof