MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  demoivreALT Structured version   Visualization version   GIF version

Theorem demoivreALT 15417
Description: Alternate proof of demoivre 15416. 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 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))

Proof of Theorem demoivreALT
Dummy variables 𝑥 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 6986 . . . . 5 (𝑥 = 0 → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = (((cos‘𝐴) + (i · (sin‘𝐴)))↑0))
2 oveq1 6985 . . . . . . 7 (𝑥 = 0 → (𝑥 · 𝐴) = (0 · 𝐴))
32fveq2d 6505 . . . . . 6 (𝑥 = 0 → (cos‘(𝑥 · 𝐴)) = (cos‘(0 · 𝐴)))
42fveq2d 6505 . . . . . . 7 (𝑥 = 0 → (sin‘(𝑥 · 𝐴)) = (sin‘(0 · 𝐴)))
54oveq2d 6994 . . . . . 6 (𝑥 = 0 → (i · (sin‘(𝑥 · 𝐴))) = (i · (sin‘(0 · 𝐴))))
63, 5oveq12d 6996 . . . . 5 (𝑥 = 0 → ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴)))) = ((cos‘(0 · 𝐴)) + (i · (sin‘(0 · 𝐴)))))
71, 6eqeq12d 2793 . . . 4 (𝑥 = 0 → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴)))) ↔ (((cos‘𝐴) + (i · (sin‘𝐴)))↑0) = ((cos‘(0 · 𝐴)) + (i · (sin‘(0 · 𝐴))))))
87imbi2d 333 . . 3 (𝑥 = 0 → ((𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴))))) ↔ (𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑0) = ((cos‘(0 · 𝐴)) + (i · (sin‘(0 · 𝐴)))))))
9 oveq2 6986 . . . . 5 (𝑥 = 𝑘 → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘))
10 oveq1 6985 . . . . . . 7 (𝑥 = 𝑘 → (𝑥 · 𝐴) = (𝑘 · 𝐴))
1110fveq2d 6505 . . . . . 6 (𝑥 = 𝑘 → (cos‘(𝑥 · 𝐴)) = (cos‘(𝑘 · 𝐴)))
1210fveq2d 6505 . . . . . . 7 (𝑥 = 𝑘 → (sin‘(𝑥 · 𝐴)) = (sin‘(𝑘 · 𝐴)))
1312oveq2d 6994 . . . . . 6 (𝑥 = 𝑘 → (i · (sin‘(𝑥 · 𝐴))) = (i · (sin‘(𝑘 · 𝐴))))
1411, 13oveq12d 6996 . . . . 5 (𝑥 = 𝑘 → ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴)))) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))))
159, 14eqeq12d 2793 . . . 4 (𝑥 = 𝑘 → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴)))) ↔ (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴))))))
1615imbi2d 333 . . 3 (𝑥 = 𝑘 → ((𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴))))) ↔ (𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))))))
17 oveq2 6986 . . . . 5 (𝑥 = (𝑘 + 1) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)))
18 oveq1 6985 . . . . . . 7 (𝑥 = (𝑘 + 1) → (𝑥 · 𝐴) = ((𝑘 + 1) · 𝐴))
1918fveq2d 6505 . . . . . 6 (𝑥 = (𝑘 + 1) → (cos‘(𝑥 · 𝐴)) = (cos‘((𝑘 + 1) · 𝐴)))
2018fveq2d 6505 . . . . . . 7 (𝑥 = (𝑘 + 1) → (sin‘(𝑥 · 𝐴)) = (sin‘((𝑘 + 1) · 𝐴)))
2120oveq2d 6994 . . . . . 6 (𝑥 = (𝑘 + 1) → (i · (sin‘(𝑥 · 𝐴))) = (i · (sin‘((𝑘 + 1) · 𝐴))))
2219, 21oveq12d 6996 . . . . 5 (𝑥 = (𝑘 + 1) → ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴)))) = ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴)))))
2317, 22eqeq12d 2793 . . . 4 (𝑥 = (𝑘 + 1) → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴)))) ↔ (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴))))))
2423imbi2d 333 . . 3 (𝑥 = (𝑘 + 1) → ((𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴))))) ↔ (𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴)))))))
25 oveq2 6986 . . . . 5 (𝑥 = 𝑁 → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁))
26 oveq1 6985 . . . . . . 7 (𝑥 = 𝑁 → (𝑥 · 𝐴) = (𝑁 · 𝐴))
2726fveq2d 6505 . . . . . 6 (𝑥 = 𝑁 → (cos‘(𝑥 · 𝐴)) = (cos‘(𝑁 · 𝐴)))
2826fveq2d 6505 . . . . . . 7 (𝑥 = 𝑁 → (sin‘(𝑥 · 𝐴)) = (sin‘(𝑁 · 𝐴)))
2928oveq2d 6994 . . . . . 6 (𝑥 = 𝑁 → (i · (sin‘(𝑥 · 𝐴))) = (i · (sin‘(𝑁 · 𝐴))))
3027, 29oveq12d 6996 . . . . 5 (𝑥 = 𝑁 → ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴)))) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))
3125, 30eqeq12d 2793 . . . 4 (𝑥 = 𝑁 → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴)))) ↔ (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴))))))
3231imbi2d 333 . . 3 (𝑥 = 𝑁 → ((𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴))))) ↔ (𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))))
33 coscl 15343 . . . . . 6 (𝐴 ∈ ℂ → (cos‘𝐴) ∈ ℂ)
34 ax-icn 10396 . . . . . . 7 i ∈ ℂ
35 sincl 15342 . . . . . . 7 (𝐴 ∈ ℂ → (sin‘𝐴) ∈ ℂ)
36 mulcl 10421 . . . . . . 7 ((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i · (sin‘𝐴)) ∈ ℂ)
3734, 35, 36sylancr 578 . . . . . 6 (𝐴 ∈ ℂ → (i · (sin‘𝐴)) ∈ ℂ)
38 addcl 10419 . . . . . 6 (((cos‘𝐴) ∈ ℂ ∧ (i · (sin‘𝐴)) ∈ ℂ) → ((cos‘𝐴) + (i · (sin‘𝐴))) ∈ ℂ)
3933, 37, 38syl2anc 576 . . . . 5 (𝐴 ∈ ℂ → ((cos‘𝐴) + (i · (sin‘𝐴))) ∈ ℂ)
40 exp0 13251 . . . . 5 (((cos‘𝐴) + (i · (sin‘𝐴))) ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑0) = 1)
4139, 40syl 17 . . . 4 (𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑0) = 1)
42 mul02 10620 . . . . . . . 8 (𝐴 ∈ ℂ → (0 · 𝐴) = 0)
4342fveq2d 6505 . . . . . . 7 (𝐴 ∈ ℂ → (cos‘(0 · 𝐴)) = (cos‘0))
44 cos0 15366 . . . . . . 7 (cos‘0) = 1
4543, 44syl6eq 2830 . . . . . 6 (𝐴 ∈ ℂ → (cos‘(0 · 𝐴)) = 1)
4642fveq2d 6505 . . . . . . . . 9 (𝐴 ∈ ℂ → (sin‘(0 · 𝐴)) = (sin‘0))
47 sin0 15365 . . . . . . . . 9 (sin‘0) = 0
4846, 47syl6eq 2830 . . . . . . . 8 (𝐴 ∈ ℂ → (sin‘(0 · 𝐴)) = 0)
4948oveq2d 6994 . . . . . . 7 (𝐴 ∈ ℂ → (i · (sin‘(0 · 𝐴))) = (i · 0))
5034mul01i 10632 . . . . . . 7 (i · 0) = 0
5149, 50syl6eq 2830 . . . . . 6 (𝐴 ∈ ℂ → (i · (sin‘(0 · 𝐴))) = 0)
5245, 51oveq12d 6996 . . . . 5 (𝐴 ∈ ℂ → ((cos‘(0 · 𝐴)) + (i · (sin‘(0 · 𝐴)))) = (1 + 0))
53 ax-1cn 10395 . . . . . 6 1 ∈ ℂ
5453addid1i 10629 . . . . 5 (1 + 0) = 1
5552, 54syl6eq 2830 . . . 4 (𝐴 ∈ ℂ → ((cos‘(0 · 𝐴)) + (i · (sin‘(0 · 𝐴)))) = 1)
5641, 55eqtr4d 2817 . . 3 (𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑0) = ((cos‘(0 · 𝐴)) + (i · (sin‘(0 · 𝐴)))))
57 expp1 13254 . . . . . . . . 9 ((((cos‘𝐴) + (i · (sin‘𝐴))) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) · ((cos‘𝐴) + (i · (sin‘𝐴)))))
5839, 57sylan 572 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) · ((cos‘𝐴) + (i · (sin‘𝐴)))))
5958ancoms 451 . . . . . . 7 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) · ((cos‘𝐴) + (i · (sin‘𝐴)))))
6059adantr 473 . . . . . 6 (((𝑘 ∈ ℕ0𝐴 ∈ ℂ) ∧ (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴))))) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) · ((cos‘𝐴) + (i · (sin‘𝐴)))))
61 oveq1 6985 . . . . . . 7 ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) · ((cos‘𝐴) + (i · (sin‘𝐴)))) = (((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) · ((cos‘𝐴) + (i · (sin‘𝐴)))))
6261adantl 474 . . . . . 6 (((𝑘 ∈ ℕ0𝐴 ∈ ℂ) ∧ (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴))))) → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) · ((cos‘𝐴) + (i · (sin‘𝐴)))) = (((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) · ((cos‘𝐴) + (i · (sin‘𝐴)))))
63 nn0cn 11721 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
64 mulcl 10421 . . . . . . . . . . . . 13 ((𝑘 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝑘 · 𝐴) ∈ ℂ)
6563, 64sylan 572 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (𝑘 · 𝐴) ∈ ℂ)
66 sinadd 15380 . . . . . . . . . . . 12 (((𝑘 · 𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (sin‘((𝑘 · 𝐴) + 𝐴)) = (((sin‘(𝑘 · 𝐴)) · (cos‘𝐴)) + ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))))
6765, 66sylancom 579 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (sin‘((𝑘 · 𝐴) + 𝐴)) = (((sin‘(𝑘 · 𝐴)) · (cos‘𝐴)) + ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))))
6833adantl 474 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (cos‘𝐴) ∈ ℂ)
69 sincl 15342 . . . . . . . . . . . . . 14 ((𝑘 · 𝐴) ∈ ℂ → (sin‘(𝑘 · 𝐴)) ∈ ℂ)
7065, 69syl 17 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (sin‘(𝑘 · 𝐴)) ∈ ℂ)
71 mulcom 10423 . . . . . . . . . . . . 13 (((cos‘𝐴) ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ) → ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) = ((sin‘(𝑘 · 𝐴)) · (cos‘𝐴)))
7268, 70, 71syl2anc 576 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) = ((sin‘(𝑘 · 𝐴)) · (cos‘𝐴)))
7372oveq1d 6993 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) + ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))) = (((sin‘(𝑘 · 𝐴)) · (cos‘𝐴)) + ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))))
74 mulcl 10421 . . . . . . . . . . . . 13 (((cos‘𝐴) ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ) → ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ)
7568, 70, 74syl2anc 576 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ)
76 coscl 15343 . . . . . . . . . . . . . 14 ((𝑘 · 𝐴) ∈ ℂ → (cos‘(𝑘 · 𝐴)) ∈ ℂ)
7765, 76syl 17 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (cos‘(𝑘 · 𝐴)) ∈ ℂ)
7835adantl 474 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (sin‘𝐴) ∈ ℂ)
79 mulcl 10421 . . . . . . . . . . . . 13 (((cos‘(𝑘 · 𝐴)) ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) ∈ ℂ)
8077, 78, 79syl2anc 576 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) ∈ ℂ)
81 addcom 10628 . . . . . . . . . . . 12 ((((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ ∧ ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) ∈ ℂ) → (((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) + ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))) = (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))
8275, 80, 81syl2anc 576 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) + ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))) = (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))
8367, 73, 823eqtr2d 2820 . . . . . . . . . 10 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (sin‘((𝑘 · 𝐴) + 𝐴)) = (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))
8483oveq2d 6994 . . . . . . . . 9 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (i · (sin‘((𝑘 · 𝐴) + 𝐴))) = (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))))
8584oveq2d 6994 . . . . . . . 8 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((cos‘((𝑘 · 𝐴) + 𝐴)) + (i · (sin‘((𝑘 · 𝐴) + 𝐴)))) = ((cos‘((𝑘 · 𝐴) + 𝐴)) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))))
86 adddir 10432 . . . . . . . . . . . . 13 ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑘 + 1) · 𝐴) = ((𝑘 · 𝐴) + (1 · 𝐴)))
87 mulid2 10440 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
8887oveq2d 6994 . . . . . . . . . . . . . 14 (𝐴 ∈ ℂ → ((𝑘 · 𝐴) + (1 · 𝐴)) = ((𝑘 · 𝐴) + 𝐴))
89883ad2ant3 1115 . . . . . . . . . . . . 13 ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑘 · 𝐴) + (1 · 𝐴)) = ((𝑘 · 𝐴) + 𝐴))
9086, 89eqtrd 2814 . . . . . . . . . . . 12 ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑘 + 1) · 𝐴) = ((𝑘 · 𝐴) + 𝐴))
9163, 90syl3an1 1143 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0 ∧ 1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑘 + 1) · 𝐴) = ((𝑘 · 𝐴) + 𝐴))
9253, 91mp3an2 1428 . . . . . . . . . 10 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((𝑘 + 1) · 𝐴) = ((𝑘 · 𝐴) + 𝐴))
9392fveq2d 6505 . . . . . . . . 9 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (cos‘((𝑘 + 1) · 𝐴)) = (cos‘((𝑘 · 𝐴) + 𝐴)))
9492fveq2d 6505 . . . . . . . . . 10 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (sin‘((𝑘 + 1) · 𝐴)) = (sin‘((𝑘 · 𝐴) + 𝐴)))
9594oveq2d 6994 . . . . . . . . 9 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (i · (sin‘((𝑘 + 1) · 𝐴))) = (i · (sin‘((𝑘 · 𝐴) + 𝐴))))
9693, 95oveq12d 6996 . . . . . . . 8 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴)))) = ((cos‘((𝑘 · 𝐴) + 𝐴)) + (i · (sin‘((𝑘 · 𝐴) + 𝐴)))))
97 mulcl 10421 . . . . . . . . . . . . . 14 ((i ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ) → (i · (sin‘(𝑘 · 𝐴))) ∈ ℂ)
9834, 97mpan 677 . . . . . . . . . . . . 13 ((sin‘(𝑘 · 𝐴)) ∈ ℂ → (i · (sin‘(𝑘 · 𝐴))) ∈ ℂ)
9965, 69, 983syl 18 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (i · (sin‘(𝑘 · 𝐴))) ∈ ℂ)
10033, 37jca 504 . . . . . . . . . . . . 13 (𝐴 ∈ ℂ → ((cos‘𝐴) ∈ ℂ ∧ (i · (sin‘𝐴)) ∈ ℂ))
101100adantl 474 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((cos‘𝐴) ∈ ℂ ∧ (i · (sin‘𝐴)) ∈ ℂ))
102 muladd 10875 . . . . . . . . . . . 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‘(𝑘 · 𝐴)))))))
10377, 99, 101, 102syl21anc 825 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) · ((cos‘𝐴) + (i · (sin‘𝐴)))) = ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + ((i · (sin‘𝐴)) · (i · (sin‘(𝑘 · 𝐴))))) + (((cos‘(𝑘 · 𝐴)) · (i · (sin‘𝐴))) + ((cos‘𝐴) · (i · (sin‘(𝑘 · 𝐴)))))))
10478, 34jctil 512 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ))
10570, 34jctil 512 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (i ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ))
106 mul4 10610 . . . . . . . . . . . . . . 15 (((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) ∧ (i ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ)) → ((i · (sin‘𝐴)) · (i · (sin‘(𝑘 · 𝐴)))) = ((i · i) · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))))
107 ixi 11072 . . . . . . . . . . . . . . . 16 (i · i) = -1
108107oveq1i 6988 . . . . . . . . . . . . . . 15 ((i · i) · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) = (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))
109106, 108syl6eq 2830 . . . . . . . . . . . . . 14 (((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) ∧ (i ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ)) → ((i · (sin‘𝐴)) · (i · (sin‘(𝑘 · 𝐴)))) = (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))))
110104, 105, 109syl2anc 576 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((i · (sin‘𝐴)) · (i · (sin‘(𝑘 · 𝐴)))) = (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))))
111110oveq2d 6994 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + ((i · (sin‘𝐴)) · (i · (sin‘(𝑘 · 𝐴))))) = (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))))
112111oveq1d 6993 . . . . . . . . . . 11 ((𝑘 ∈ ℕ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 10607 . . . . . . . . . . . . . . . 16 (((cos‘(𝑘 · 𝐴)) ∈ ℂ ∧ i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → ((cos‘(𝑘 · 𝐴)) · (i · (sin‘𝐴))) = (i · ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))))
11434, 113mp3an2 1428 . . . . . . . . . . . . . . 15 (((cos‘(𝑘 · 𝐴)) ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → ((cos‘(𝑘 · 𝐴)) · (i · (sin‘𝐴))) = (i · ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))))
11577, 78, 114syl2anc 576 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((cos‘(𝑘 · 𝐴)) · (i · (sin‘𝐴))) = (i · ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))))
116 mul12 10607 . . . . . . . . . . . . . . . 16 (((cos‘𝐴) ∈ ℂ ∧ i ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ) → ((cos‘𝐴) · (i · (sin‘(𝑘 · 𝐴)))) = (i · ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))
11734, 116mp3an2 1428 . . . . . . . . . . . . . . 15 (((cos‘𝐴) ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ) → ((cos‘𝐴) · (i · (sin‘(𝑘 · 𝐴)))) = (i · ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))
11868, 70, 117syl2anc 576 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((cos‘𝐴) · (i · (sin‘(𝑘 · 𝐴)))) = (i · ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))
119115, 118oveq12d 6996 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) · (i · (sin‘𝐴))) + ((cos‘𝐴) · (i · (sin‘(𝑘 · 𝐴))))) = ((i · ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))) + (i · ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))))
120 adddi 10426 . . . . . . . . . . . . . . 15 ((i ∈ ℂ ∧ ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) ∈ ℂ ∧ ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ) → (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))) = ((i · ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))) + (i · ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))))
12134, 120mp3an1 1427 . . . . . . . . . . . . . 14 ((((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) ∈ ℂ ∧ ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ) → (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))) = ((i · ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))) + (i · ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))))
12280, 75, 121syl2anc 576 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))) = ((i · ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))) + (i · ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))))
123119, 122eqtr4d 2817 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) · (i · (sin‘𝐴))) + ((cos‘𝐴) · (i · (sin‘(𝑘 · 𝐴))))) = (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))))
124123oveq2d 6994 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))) + (((cos‘(𝑘 · 𝐴)) · (i · (sin‘𝐴))) + ((cos‘𝐴) · (i · (sin‘(𝑘 · 𝐴)))))) = ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))))
125103, 112, 1243eqtrd 2818 . . . . . . . . . 10 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) · ((cos‘𝐴) + (i · (sin‘𝐴)))) = ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))))
126 mulcl 10421 . . . . . . . . . . . . . 14 (((sin‘𝐴) ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ) → ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ)
12778, 70, 126syl2anc 576 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ)
128 mulm1 10884 . . . . . . . . . . . . 13 (((sin‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ → (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) = -((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))
129127, 128syl 17 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) = -((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))
130129oveq2d 6994 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))) = (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + -((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))))
131130oveq1d 6993 . . . . . . . . . 10 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))) = ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + -((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))))
132 mulcl 10421 . . . . . . . . . . . . 13 (((cos‘(𝑘 · 𝐴)) ∈ ℂ ∧ (cos‘𝐴) ∈ ℂ) → ((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) ∈ ℂ)
13377, 68, 132syl2anc 576 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) ∈ ℂ)
134 negsub 10737 . . . . . . . . . . . 12 ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) ∈ ℂ ∧ ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + -((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) = (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))))
135133, 127, 134syl2anc 576 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + -((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) = (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))))
136135oveq1d 6993 . . . . . . . . . 10 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + -((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))) = ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))))
137125, 131, 1363eqtrd 2818 . . . . . . . . 9 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) · ((cos‘𝐴) + (i · (sin‘𝐴)))) = ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))))
138 cosadd 15381 . . . . . . . . . . . 12 (((𝑘 · 𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (cos‘((𝑘 · 𝐴) + 𝐴)) = (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘(𝑘 · 𝐴)) · (sin‘𝐴))))
13965, 138sylancom 579 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (cos‘((𝑘 · 𝐴) + 𝐴)) = (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘(𝑘 · 𝐴)) · (sin‘𝐴))))
140 mulcom 10423 . . . . . . . . . . . . 13 (((sin‘(𝑘 · 𝐴)) ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → ((sin‘(𝑘 · 𝐴)) · (sin‘𝐴)) = ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))
14170, 78, 140syl2anc 576 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((sin‘(𝑘 · 𝐴)) · (sin‘𝐴)) = ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))
142141oveq2d 6994 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘(𝑘 · 𝐴)) · (sin‘𝐴))) = (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))))
143139, 142eqtrd 2814 . . . . . . . . . 10 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (cos‘((𝑘 · 𝐴) + 𝐴)) = (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))))
144143oveq1d 6993 . . . . . . . . 9 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((cos‘((𝑘 · 𝐴) + 𝐴)) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))) = ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))))
145137, 144eqtr4d 2817 . . . . . . . 8 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) · ((cos‘𝐴) + (i · (sin‘𝐴)))) = ((cos‘((𝑘 · 𝐴) + 𝐴)) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))))
14685, 96, 1453eqtr4rd 2825 . . . . . . 7 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) · ((cos‘𝐴) + (i · (sin‘𝐴)))) = ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴)))))
147146adantr 473 . . . . . 6 (((𝑘 ∈ ℕ0𝐴 ∈ ℂ) ∧ (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴))))) → (((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) · ((cos‘𝐴) + (i · (sin‘𝐴)))) = ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴)))))
14860, 62, 1473eqtrd 2818 . . . . 5 (((𝑘 ∈ ℕ0𝐴 ∈ ℂ) ∧ (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴))))) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴)))))
149148exp31 412 . . . 4 (𝑘 ∈ ℕ0 → (𝐴 ∈ ℂ → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴)))))))
150149a2d 29 . . 3 (𝑘 ∈ ℕ0 → ((𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴))))) → (𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴)))))))
1518, 16, 24, 32, 56, 150nn0ind 11893 . 2 (𝑁 ∈ ℕ0 → (𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴))))))
152151impcom 399 1 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387  w3a 1068   = wceq 1507  wcel 2050  cfv 6190  (class class class)co 6978  cc 10335  0cc0 10337  1c1 10338  ici 10339   + caddc 10340   · cmul 10342  cmin 10672  -cneg 10673  0cn0 11710  cexp 13247  sincsin 15280  cosccos 15281
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-rep 5050  ax-sep 5061  ax-nul 5068  ax-pow 5120  ax-pr 5187  ax-un 7281  ax-inf2 8900  ax-cnex 10393  ax-resscn 10394  ax-1cn 10395  ax-icn 10396  ax-addcl 10397  ax-addrcl 10398  ax-mulcl 10399  ax-mulrcl 10400  ax-mulcom 10401  ax-addass 10402  ax-mulass 10403  ax-distr 10404  ax-i2m1 10405  ax-1ne0 10406  ax-1rid 10407  ax-rnegex 10408  ax-rrecex 10409  ax-cnre 10410  ax-pre-lttri 10411  ax-pre-lttrn 10412  ax-pre-ltadd 10413  ax-pre-mulgt0 10414  ax-pre-sup 10415  ax-addf 10416  ax-mulf 10417
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rmo 3096  df-rab 3097  df-v 3417  df-sbc 3684  df-csb 3789  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-pss 3847  df-nul 4181  df-if 4352  df-pw 4425  df-sn 4443  df-pr 4445  df-tp 4447  df-op 4449  df-uni 4714  df-int 4751  df-iun 4795  df-br 4931  df-opab 4993  df-mpt 5010  df-tr 5032  df-id 5313  df-eprel 5318  df-po 5327  df-so 5328  df-fr 5367  df-se 5368  df-we 5369  df-xp 5414  df-rel 5415  df-cnv 5416  df-co 5417  df-dm 5418  df-rn 5419  df-res 5420  df-ima 5421  df-pred 5988  df-ord 6034  df-on 6035  df-lim 6036  df-suc 6037  df-iota 6154  df-fun 6192  df-fn 6193  df-f 6194  df-f1 6195  df-fo 6196  df-f1o 6197  df-fv 6198  df-isom 6199  df-riota 6939  df-ov 6981  df-oprab 6982  df-mpo 6983  df-om 7399  df-1st 7503  df-2nd 7504  df-wrecs 7752  df-recs 7814  df-rdg 7852  df-1o 7907  df-oadd 7911  df-er 8091  df-pm 8211  df-en 8309  df-dom 8310  df-sdom 8311  df-fin 8312  df-sup 8703  df-inf 8704  df-oi 8771  df-card 9164  df-pnf 10478  df-mnf 10479  df-xr 10480  df-ltxr 10481  df-le 10482  df-sub 10674  df-neg 10675  df-div 11101  df-nn 11442  df-2 11506  df-3 11507  df-n0 11711  df-z 11797  df-uz 12062  df-rp 12208  df-ico 12563  df-fz 12712  df-fzo 12853  df-fl 12980  df-seq 13188  df-exp 13248  df-fac 13452  df-bc 13481  df-hash 13509  df-shft 14290  df-cj 14322  df-re 14323  df-im 14324  df-sqrt 14458  df-abs 14459  df-limsup 14692  df-clim 14709  df-rlim 14710  df-sum 14907  df-ef 15284  df-sin 15286  df-cos 15287
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator