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	addridi	⊢ ( 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		mullid	⊢ ( 𝐴 ∈ ℂ → ( 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 ‘ ( 𝑁 · 𝐴 ) ) ) ) )