demoivreALT - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > demoivreALT		GIF version

Theorem demoivreALT 12271

Description: Alternate proof of demoivre 12270. 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.)

**Assertion**
Ref	Expression
demoivreALT	⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))

Proof of Theorem demoivreALT Dummy variables 𝑥 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 6002	. . . . 5 ⊢ (𝑥 = 0 → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = (((cos‘𝐴) + (i · (sin‘𝐴)))↑0))
2		oveq1 6001	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 · 𝐴) = (0 · 𝐴))
3	2	fveq2d 5627	. . . . . 6 ⊢ (𝑥 = 0 → (cos‘(𝑥 · 𝐴)) = (cos‘(0 · 𝐴)))
4	2	fveq2d 5627	. . . . . . 7 ⊢ (𝑥 = 0 → (sin‘(𝑥 · 𝐴)) = (sin‘(0 · 𝐴)))
5	4	oveq2d 6010	. . . . . 6 ⊢ (𝑥 = 0 → (i · (sin‘(𝑥 · 𝐴))) = (i · (sin‘(0 · 𝐴))))
6	3, 5	oveq12d 6012	. . . . 5 ⊢ (𝑥 = 0 → ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴)))) = ((cos‘(0 · 𝐴)) + (i · (sin‘(0 · 𝐴)))))
7	1, 6	eqeq12d 2244	. . . 4 ⊢ (𝑥 = 0 → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴)))) ↔ (((cos‘𝐴) + (i · (sin‘𝐴)))↑0) = ((cos‘(0 · 𝐴)) + (i · (sin‘(0 · 𝐴))))))
8	7	imbi2d 230	. . 3 ⊢ (𝑥 = 0 → ((𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴))))) ↔ (𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑0) = ((cos‘(0 · 𝐴)) + (i · (sin‘(0 · 𝐴)))))))
9		oveq2 6002	. . . . 5 ⊢ (𝑥 = 𝑘 → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘))
10		oveq1 6001	. . . . . . 7 ⊢ (𝑥 = 𝑘 → (𝑥 · 𝐴) = (𝑘 · 𝐴))
11	10	fveq2d 5627	. . . . . 6 ⊢ (𝑥 = 𝑘 → (cos‘(𝑥 · 𝐴)) = (cos‘(𝑘 · 𝐴)))
12	10	fveq2d 5627	. . . . . . 7 ⊢ (𝑥 = 𝑘 → (sin‘(𝑥 · 𝐴)) = (sin‘(𝑘 · 𝐴)))
13	12	oveq2d 6010	. . . . . 6 ⊢ (𝑥 = 𝑘 → (i · (sin‘(𝑥 · 𝐴))) = (i · (sin‘(𝑘 · 𝐴))))
14	11, 13	oveq12d 6012	. . . . 5 ⊢ (𝑥 = 𝑘 → ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴)))) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))))
15	9, 14	eqeq12d 2244	. . . 4 ⊢ (𝑥 = 𝑘 → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴)))) ↔ (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴))))))
16	15	imbi2d 230	. . 3 ⊢ (𝑥 = 𝑘 → ((𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴))))) ↔ (𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))))))
17		oveq2 6002	. . . . 5 ⊢ (𝑥 = (𝑘 + 1) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)))
18		oveq1 6001	. . . . . . 7 ⊢ (𝑥 = (𝑘 + 1) → (𝑥 · 𝐴) = ((𝑘 + 1) · 𝐴))
19	18	fveq2d 5627	. . . . . 6 ⊢ (𝑥 = (𝑘 + 1) → (cos‘(𝑥 · 𝐴)) = (cos‘((𝑘 + 1) · 𝐴)))
20	18	fveq2d 5627	. . . . . . 7 ⊢ (𝑥 = (𝑘 + 1) → (sin‘(𝑥 · 𝐴)) = (sin‘((𝑘 + 1) · 𝐴)))
21	20	oveq2d 6010	. . . . . 6 ⊢ (𝑥 = (𝑘 + 1) → (i · (sin‘(𝑥 · 𝐴))) = (i · (sin‘((𝑘 + 1) · 𝐴))))
22	19, 21	oveq12d 6012	. . . . 5 ⊢ (𝑥 = (𝑘 + 1) → ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴)))) = ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴)))))
23	17, 22	eqeq12d 2244	. . . 4 ⊢ (𝑥 = (𝑘 + 1) → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴)))) ↔ (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴))))))
24	23	imbi2d 230	. . 3 ⊢ (𝑥 = (𝑘 + 1) → ((𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴))))) ↔ (𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴)))))))
25		oveq2 6002	. . . . 5 ⊢ (𝑥 = 𝑁 → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁))
26		oveq1 6001	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (𝑥 · 𝐴) = (𝑁 · 𝐴))
27	26	fveq2d 5627	. . . . . 6 ⊢ (𝑥 = 𝑁 → (cos‘(𝑥 · 𝐴)) = (cos‘(𝑁 · 𝐴)))
28	26	fveq2d 5627	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (sin‘(𝑥 · 𝐴)) = (sin‘(𝑁 · 𝐴)))
29	28	oveq2d 6010	. . . . . 6 ⊢ (𝑥 = 𝑁 → (i · (sin‘(𝑥 · 𝐴))) = (i · (sin‘(𝑁 · 𝐴))))
30	27, 29	oveq12d 6012	. . . . 5 ⊢ (𝑥 = 𝑁 → ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴)))) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))
31	25, 30	eqeq12d 2244	. . . 4 ⊢ (𝑥 = 𝑁 → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴)))) ↔ (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴))))))
32	31	imbi2d 230	. . 3 ⊢ (𝑥 = 𝑁 → ((𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴))))) ↔ (𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))))
33		coscl 12204	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (cos‘𝐴) ∈ ℂ)
34		ax-icn 8082	. . . . . . 7 ⊢ i ∈ ℂ
35		sincl 12203	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (sin‘𝐴) ∈ ℂ)
36		mulcl 8114	. . . . . . 7 ⊢ ((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i · (sin‘𝐴)) ∈ ℂ)
37	34, 35, 36	sylancr 414	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (i · (sin‘𝐴)) ∈ ℂ)
38		addcl 8112	. . . . . 6 ⊢ (((cos‘𝐴) ∈ ℂ ∧ (i · (sin‘𝐴)) ∈ ℂ) → ((cos‘𝐴) + (i · (sin‘𝐴))) ∈ ℂ)
39	33, 37, 38	syl2anc 411	. . . . 5 ⊢ (𝐴 ∈ ℂ → ((cos‘𝐴) + (i · (sin‘𝐴))) ∈ ℂ)
40		exp0 10752	. . . . 5 ⊢ (((cos‘𝐴) + (i · (sin‘𝐴))) ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑0) = 1)
41	39, 40	syl 14	. . . 4 ⊢ (𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑0) = 1)
42		mul02 8521	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (0 · 𝐴) = 0)
43	42	fveq2d 5627	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (cos‘(0 · 𝐴)) = (cos‘0))
44		cos0 12227	. . . . . . 7 ⊢ (cos‘0) = 1
45	43, 44	eqtrdi 2278	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (cos‘(0 · 𝐴)) = 1)
46	42	fveq2d 5627	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (sin‘(0 · 𝐴)) = (sin‘0))
47		sin0 12226	. . . . . . . . 9 ⊢ (sin‘0) = 0
48	46, 47	eqtrdi 2278	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (sin‘(0 · 𝐴)) = 0)
49	48	oveq2d 6010	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (i · (sin‘(0 · 𝐴))) = (i · 0))
50	34	mul01i 8525	. . . . . . 7 ⊢ (i · 0) = 0
51	49, 50	eqtrdi 2278	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (i · (sin‘(0 · 𝐴))) = 0)
52	45, 51	oveq12d 6012	. . . . 5 ⊢ (𝐴 ∈ ℂ → ((cos‘(0 · 𝐴)) + (i · (sin‘(0 · 𝐴)))) = (1 + 0))
53		ax-1cn 8080	. . . . . 6 ⊢ 1 ∈ ℂ
54	53	addridi 8276	. . . . 5 ⊢ (1 + 0) = 1
55	52, 54	eqtrdi 2278	. . . 4 ⊢ (𝐴 ∈ ℂ → ((cos‘(0 · 𝐴)) + (i · (sin‘(0 · 𝐴)))) = 1)
56	41, 55	eqtr4d 2265	. . 3 ⊢ (𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑0) = ((cos‘(0 · 𝐴)) + (i · (sin‘(0 · 𝐴)))))
57		expp1 10755	. . . . . . . . 9 ⊢ ((((cos‘𝐴) + (i · (sin‘𝐴))) ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) · ((cos‘𝐴) + (i · (sin‘𝐴)))))
58	39, 57	sylan 283	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) · ((cos‘𝐴) + (i · (sin‘𝐴)))))
59	58	ancoms 268	. . . . . . 7 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) · ((cos‘𝐴) + (i · (sin‘𝐴)))))
60	59	adantr 276	. . . . . 6 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) ∧ (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴))))) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) · ((cos‘𝐴) + (i · (sin‘𝐴)))))
61		oveq1 6001	. . . . . . 7 ⊢ ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) · ((cos‘𝐴) + (i · (sin‘𝐴)))) = (((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) · ((cos‘𝐴) + (i · (sin‘𝐴)))))
62	61	adantl 277	. . . . . 6 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) ∧ (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴))))) → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) · ((cos‘𝐴) + (i · (sin‘𝐴)))) = (((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) · ((cos‘𝐴) + (i · (sin‘𝐴)))))
63		nn0cn 9367	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ₀ → 𝑘 ∈ ℂ)
64		mulcl 8114	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝑘 · 𝐴) ∈ ℂ)
65	63, 64	sylan 283	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (𝑘 · 𝐴) ∈ ℂ)
66		sinadd 12233	. . . . . . . . . . . 12 ⊢ (((𝑘 · 𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (sin‘((𝑘 · 𝐴) + 𝐴)) = (((sin‘(𝑘 · 𝐴)) · (cos‘𝐴)) + ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))))
67	65, 66	sylancom 420	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (sin‘((𝑘 · 𝐴) + 𝐴)) = (((sin‘(𝑘 · 𝐴)) · (cos‘𝐴)) + ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))))
68	33	adantl 277	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (cos‘𝐴) ∈ ℂ)
69		sincl 12203	. . . . . . . . . . . . . 14 ⊢ ((𝑘 · 𝐴) ∈ ℂ → (sin‘(𝑘 · 𝐴)) ∈ ℂ)
70	65, 69	syl 14	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (sin‘(𝑘 · 𝐴)) ∈ ℂ)
71		mulcom 8116	. . . . . . . . . . . . 13 ⊢ (((cos‘𝐴) ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ) → ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) = ((sin‘(𝑘 · 𝐴)) · (cos‘𝐴)))
72	68, 70, 71	syl2anc 411	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) = ((sin‘(𝑘 · 𝐴)) · (cos‘𝐴)))
73	72	oveq1d 6009	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) + ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))) = (((sin‘(𝑘 · 𝐴)) · (cos‘𝐴)) + ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))))
74		mulcl 8114	. . . . . . . . . . . . 13 ⊢ (((cos‘𝐴) ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ) → ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ)
75	68, 70, 74	syl2anc 411	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ)
76		coscl 12204	. . . . . . . . . . . . . 14 ⊢ ((𝑘 · 𝐴) ∈ ℂ → (cos‘(𝑘 · 𝐴)) ∈ ℂ)
77	65, 76	syl 14	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (cos‘(𝑘 · 𝐴)) ∈ ℂ)
78	35	adantl 277	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (sin‘𝐴) ∈ ℂ)
79		mulcl 8114	. . . . . . . . . . . . 13 ⊢ (((cos‘(𝑘 · 𝐴)) ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) ∈ ℂ)
80	77, 78, 79	syl2anc 411	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) ∈ ℂ)
81		addcom 8271	. . . . . . . . . . . 12 ⊢ ((((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ ∧ ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) ∈ ℂ) → (((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) + ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))) = (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))
82	75, 80, 81	syl2anc 411	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) + ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))) = (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))
83	67, 73, 82	3eqtr2d 2268	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (sin‘((𝑘 · 𝐴) + 𝐴)) = (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))
84	83	oveq2d 6010	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (i · (sin‘((𝑘 · 𝐴) + 𝐴))) = (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))))
85	84	oveq2d 6010	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → ((cos‘((𝑘 · 𝐴) + 𝐴)) + (i · (sin‘((𝑘 · 𝐴) + 𝐴)))) = ((cos‘((𝑘 · 𝐴) + 𝐴)) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))))
86		adddir 8125	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑘 + 1) · 𝐴) = ((𝑘 · 𝐴) + (1 · 𝐴)))
87		mullid 8132	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
88	87	oveq2d 6010	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → ((𝑘 · 𝐴) + (1 · 𝐴)) = ((𝑘 · 𝐴) + 𝐴))
89	88	3ad2ant3 1044	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑘 · 𝐴) + (1 · 𝐴)) = ((𝑘 · 𝐴) + 𝐴))
90	86, 89	eqtrd 2262	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑘 + 1) · 𝐴) = ((𝑘 · 𝐴) + 𝐴))
91	63, 90	syl3an1 1304	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ₀ ∧ 1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑘 + 1) · 𝐴) = ((𝑘 · 𝐴) + 𝐴))
92	53, 91	mp3an2 1359	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → ((𝑘 + 1) · 𝐴) = ((𝑘 · 𝐴) + 𝐴))
93	92	fveq2d 5627	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (cos‘((𝑘 + 1) · 𝐴)) = (cos‘((𝑘 · 𝐴) + 𝐴)))
94	92	fveq2d 5627	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (sin‘((𝑘 + 1) · 𝐴)) = (sin‘((𝑘 · 𝐴) + 𝐴)))
95	94	oveq2d 6010	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (i · (sin‘((𝑘 + 1) · 𝐴))) = (i · (sin‘((𝑘 · 𝐴) + 𝐴))))
96	93, 95	oveq12d 6012	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴)))) = ((cos‘((𝑘 · 𝐴) + 𝐴)) + (i · (sin‘((𝑘 · 𝐴) + 𝐴)))))
97		mulcl 8114	. . . . . . . . . . . . . 14 ⊢ ((i ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ) → (i · (sin‘(𝑘 · 𝐴))) ∈ ℂ)
98	34, 97	mpan 424	. . . . . . . . . . . . 13 ⊢ ((sin‘(𝑘 · 𝐴)) ∈ ℂ → (i · (sin‘(𝑘 · 𝐴))) ∈ ℂ)
99	65, 69, 98	3syl 17	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (i · (sin‘(𝑘 · 𝐴))) ∈ ℂ)
100	33, 37	jca 306	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → ((cos‘𝐴) ∈ ℂ ∧ (i · (sin‘𝐴)) ∈ ℂ))
101	100	adantl 277	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → ((cos‘𝐴) ∈ ℂ ∧ (i · (sin‘𝐴)) ∈ ℂ))
102		muladd 8518	. . . . . . . . . . . 12 ⊢ ((((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 1270	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) · ((cos‘𝐴) + (i · (sin‘𝐴)))) = ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + ((i · (sin‘𝐴)) · (i · (sin‘(𝑘 · 𝐴))))) + (((cos‘(𝑘 · 𝐴)) · (i · (sin‘𝐴))) + ((cos‘𝐴) · (i · (sin‘(𝑘 · 𝐴)))))))
104	78, 34	jctil 312	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ))
105	70, 34	jctil 312	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (i ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ))
106		mul4 8266	. . . . . . . . . . . . . . 15 ⊢ (((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) ∧ (i ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ)) → ((i · (sin‘𝐴)) · (i · (sin‘(𝑘 · 𝐴)))) = ((i · i) · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))))
107		ixi 8718	. . . . . . . . . . . . . . . 16 ⊢ (i · i) = -1
108	107	oveq1i 6004	. . . . . . . . . . . . . . 15 ⊢ ((i · i) · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) = (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))
109	106, 108	eqtrdi 2278	. . . . . . . . . . . . . 14 ⊢ (((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) ∧ (i ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ)) → ((i · (sin‘𝐴)) · (i · (sin‘(𝑘 · 𝐴)))) = (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))))
110	104, 105, 109	syl2anc 411	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → ((i · (sin‘𝐴)) · (i · (sin‘(𝑘 · 𝐴)))) = (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))))
111	110	oveq2d 6010	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + ((i · (sin‘𝐴)) · (i · (sin‘(𝑘 · 𝐴))))) = (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))))
112	111	oveq1d 6009	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → ((((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 8263	. . . . . . . . . . . . . . . 16 ⊢ (((cos‘(𝑘 · 𝐴)) ∈ ℂ ∧ i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → ((cos‘(𝑘 · 𝐴)) · (i · (sin‘𝐴))) = (i · ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))))
114	34, 113	mp3an2 1359	. . . . . . . . . . . . . . 15 ⊢ (((cos‘(𝑘 · 𝐴)) ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → ((cos‘(𝑘 · 𝐴)) · (i · (sin‘𝐴))) = (i · ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))))
115	77, 78, 114	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → ((cos‘(𝑘 · 𝐴)) · (i · (sin‘𝐴))) = (i · ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))))
116		mul12 8263	. . . . . . . . . . . . . . . 16 ⊢ (((cos‘𝐴) ∈ ℂ ∧ i ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ) → ((cos‘𝐴) · (i · (sin‘(𝑘 · 𝐴)))) = (i · ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))
117	34, 116	mp3an2 1359	. . . . . . . . . . . . . . 15 ⊢ (((cos‘𝐴) ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ) → ((cos‘𝐴) · (i · (sin‘(𝑘 · 𝐴)))) = (i · ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))
118	68, 70, 117	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → ((cos‘𝐴) · (i · (sin‘(𝑘 · 𝐴)))) = (i · ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))
119	115, 118	oveq12d 6012	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) · (i · (sin‘𝐴))) + ((cos‘𝐴) · (i · (sin‘(𝑘 · 𝐴))))) = ((i · ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))) + (i · ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))))
120		adddi 8119	. . . . . . . . . . . . . . 15 ⊢ ((i ∈ ℂ ∧ ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) ∈ ℂ ∧ ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ) → (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))) = ((i · ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))) + (i · ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))))
121	34, 120	mp3an1 1358	. . . . . . . . . . . . . 14 ⊢ ((((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) ∈ ℂ ∧ ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ) → (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))) = ((i · ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))) + (i · ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))))
122	80, 75, 121	syl2anc 411	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))) = ((i · ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))) + (i · ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))))
123	119, 122	eqtr4d 2265	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) · (i · (sin‘𝐴))) + ((cos‘𝐴) · (i · (sin‘(𝑘 · 𝐴))))) = (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))))
124	123	oveq2d 6010	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → ((((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 2266	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) · ((cos‘𝐴) + (i · (sin‘𝐴)))) = ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))))
126		mulcl 8114	. . . . . . . . . . . . . 14 ⊢ (((sin‘𝐴) ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ) → ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ)
127	78, 70, 126	syl2anc 411	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ)
128		mulm1 8534	. . . . . . . . . . . . 13 ⊢ (((sin‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ → (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) = -((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))
129	127, 128	syl 14	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) = -((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))
130	129	oveq2d 6010	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))) = (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + -((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))))
131	130	oveq1d 6009	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))) = ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + -((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))))
132		mulcl 8114	. . . . . . . . . . . . 13 ⊢ (((cos‘(𝑘 · 𝐴)) ∈ ℂ ∧ (cos‘𝐴) ∈ ℂ) → ((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) ∈ ℂ)
133	77, 68, 132	syl2anc 411	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → ((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) ∈ ℂ)
134		negsub 8382	. . . . . . . . . . . 12 ⊢ ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) ∈ ℂ ∧ ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + -((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) = (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))))
135	133, 127, 134	syl2anc 411	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + -((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) = (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))))
136	135	oveq1d 6009	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + -((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))) = ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))))
137	125, 131, 136	3eqtrd 2266	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) · ((cos‘𝐴) + (i · (sin‘𝐴)))) = ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))))
138		cosadd 12234	. . . . . . . . . . . 12 ⊢ (((𝑘 · 𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (cos‘((𝑘 · 𝐴) + 𝐴)) = (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘(𝑘 · 𝐴)) · (sin‘𝐴))))
139	65, 138	sylancom 420	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (cos‘((𝑘 · 𝐴) + 𝐴)) = (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘(𝑘 · 𝐴)) · (sin‘𝐴))))
140		mulcom 8116	. . . . . . . . . . . . 13 ⊢ (((sin‘(𝑘 · 𝐴)) ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → ((sin‘(𝑘 · 𝐴)) · (sin‘𝐴)) = ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))
141	70, 78, 140	syl2anc 411	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → ((sin‘(𝑘 · 𝐴)) · (sin‘𝐴)) = ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))
142	141	oveq2d 6010	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘(𝑘 · 𝐴)) · (sin‘𝐴))) = (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))))
143	139, 142	eqtrd 2262	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (cos‘((𝑘 · 𝐴) + 𝐴)) = (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))))
144	143	oveq1d 6009	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → ((cos‘((𝑘 · 𝐴) + 𝐴)) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))) = ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))))
145	137, 144	eqtr4d 2265	. . . . . . . 8 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) · ((cos‘𝐴) + (i · (sin‘𝐴)))) = ((cos‘((𝑘 · 𝐴) + 𝐴)) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))))
146	85, 96, 145	3eqtr4rd 2273	. . . . . . 7 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) · ((cos‘𝐴) + (i · (sin‘𝐴)))) = ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴)))))
147	146	adantr 276	. . . . . 6 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) ∧ (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴))))) → (((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) · ((cos‘𝐴) + (i · (sin‘𝐴)))) = ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴)))))
148	60, 62, 147	3eqtrd 2266	. . . . 5 ⊢ (((𝑘 ∈ ℕ₀ ∧ 𝐴 ∈ ℂ) ∧ (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴))))) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴)))))
149	148	exp31 364	. . . 4 ⊢ (𝑘 ∈ ℕ₀ → (𝐴 ∈ ℂ → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴)))))))
150	149	a2d 26	. . 3 ⊢ (𝑘 ∈ ℕ₀ → ((𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴))))) → (𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴)))))))
151	8, 16, 24, 32, 56, 150	nn0ind 9549	. 2 ⊢ (𝑁 ∈ ℕ₀ → (𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴))))))
152	151	impcom 125	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 1002 = wceq 1395 ∈ wcel 2200 ‘cfv 5314 (class class class)co 5994 ℂcc 7985 0cc0 7987 1c1 7988 ici 7989 + caddc 7990 · cmul 7992 − cmin 8305 -cneg 8306 ℕ₀cn0 9357 ↑cexp 10747 sincsin 12141 cosccos 12142

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4198 ax-sep 4201 ax-nul 4209 ax-pow 4257 ax-pr 4292 ax-un 4521 ax-setind 4626 ax-iinf 4677 ax-cnex 8078 ax-resscn 8079 ax-1cn 8080 ax-1re 8081 ax-icn 8082 ax-addcl 8083 ax-addrcl 8084 ax-mulcl 8085 ax-mulrcl 8086 ax-addcom 8087 ax-mulcom 8088 ax-addass 8089 ax-mulass 8090 ax-distr 8091 ax-i2m1 8092 ax-0lt1 8093 ax-1rid 8094 ax-0id 8095 ax-rnegex 8096 ax-precex 8097 ax-cnre 8098 ax-pre-ltirr 8099 ax-pre-ltwlin 8100 ax-pre-lttrn 8101 ax-pre-apti 8102 ax-pre-ltadd 8103 ax-pre-mulgt0 8104 ax-pre-mulext 8105 ax-arch 8106 ax-caucvg 8107

This theorem depends on definitions: df-bi 117 df-dc 840 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-nel 2496 df-ral 2513 df-rex 2514 df-reu 2515 df-rmo 2516 df-rab 2517 df-v 2801 df-sbc 3029 df-csb 3125 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-nul 3492 df-if 3603 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3888 df-int 3923 df-iun 3966 df-disj 4059 df-br 4083 df-opab 4145 df-mpt 4146 df-tr 4182 df-id 4381 df-po 4384 df-iso 4385 df-iord 4454 df-on 4456 df-ilim 4457 df-suc 4459 df-iom 4680 df-xp 4722 df-rel 4723 df-cnv 4724 df-co 4725 df-dm 4726 df-rn 4727 df-res 4728 df-ima 4729 df-iota 5274 df-fun 5316 df-fn 5317 df-f 5318 df-f1 5319 df-fo 5320 df-f1o 5321 df-fv 5322 df-isom 5323 df-riota 5947 df-ov 5997 df-oprab 5998 df-mpo 5999 df-1st 6276 df-2nd 6277 df-recs 6441 df-irdg 6506 df-frec 6527 df-1o 6552 df-oadd 6556 df-er 6670 df-en 6878 df-dom 6879 df-fin 6880 df-sup 7139 df-pnf 8171 df-mnf 8172 df-xr 8173 df-ltxr 8174 df-le 8175 df-sub 8307 df-neg 8308 df-reap 8710 df-ap 8717 df-div 8808 df-inn 9099 df-2 9157 df-3 9158 df-4 9159 df-n0 9358 df-z 9435 df-uz 9711 df-q 9803 df-rp 9838 df-ico 10078 df-fz 10193 df-fzo 10327 df-seqfrec 10657 df-exp 10748 df-fac 10935 df-bc 10957 df-ihash 10985 df-cj 11339 df-re 11340 df-im 11341 df-rsqrt 11495 df-abs 11496 df-clim 11776 df-sumdc 11851 df-ef 12145 df-sin 12147 df-cos 12148

This theorem is referenced by: (None)

W3C validator