Metamath Proof Explorer

Theorem 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 addid1i 
 |-  ( 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 mulid2 
 |-  ( 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 ) ) ) ) )