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 ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) ↑ 𝑁 ) = ( ( cos ‘ ( 𝑁 · 𝐴 ) ) + ( i · ( sin ‘ ( 𝑁 · 𝐴 ) ) ) ) )

Proof

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