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

Theorem demoivreALT 11911
Description: Alternate proof of demoivre 11910. 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 5922 . . . . 5 (𝑥 = 0 → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = (((cos‘𝐴) + (i · (sin‘𝐴)))↑0))
2 oveq1 5921 . . . . . . 7 (𝑥 = 0 → (𝑥 · 𝐴) = (0 · 𝐴))
32fveq2d 5554 . . . . . 6 (𝑥 = 0 → (cos‘(𝑥 · 𝐴)) = (cos‘(0 · 𝐴)))
42fveq2d 5554 . . . . . . 7 (𝑥 = 0 → (sin‘(𝑥 · 𝐴)) = (sin‘(0 · 𝐴)))
54oveq2d 5930 . . . . . 6 (𝑥 = 0 → (i · (sin‘(𝑥 · 𝐴))) = (i · (sin‘(0 · 𝐴))))
63, 5oveq12d 5932 . . . . 5 (𝑥 = 0 → ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴)))) = ((cos‘(0 · 𝐴)) + (i · (sin‘(0 · 𝐴)))))
71, 6eqeq12d 2208 . . . 4 (𝑥 = 0 → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴)))) ↔ (((cos‘𝐴) + (i · (sin‘𝐴)))↑0) = ((cos‘(0 · 𝐴)) + (i · (sin‘(0 · 𝐴))))))
87imbi2d 230 . . 3 (𝑥 = 0 → ((𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴))))) ↔ (𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑0) = ((cos‘(0 · 𝐴)) + (i · (sin‘(0 · 𝐴)))))))
9 oveq2 5922 . . . . 5 (𝑥 = 𝑘 → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘))
10 oveq1 5921 . . . . . . 7 (𝑥 = 𝑘 → (𝑥 · 𝐴) = (𝑘 · 𝐴))
1110fveq2d 5554 . . . . . 6 (𝑥 = 𝑘 → (cos‘(𝑥 · 𝐴)) = (cos‘(𝑘 · 𝐴)))
1210fveq2d 5554 . . . . . . 7 (𝑥 = 𝑘 → (sin‘(𝑥 · 𝐴)) = (sin‘(𝑘 · 𝐴)))
1312oveq2d 5930 . . . . . 6 (𝑥 = 𝑘 → (i · (sin‘(𝑥 · 𝐴))) = (i · (sin‘(𝑘 · 𝐴))))
1411, 13oveq12d 5932 . . . . 5 (𝑥 = 𝑘 → ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴)))) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))))
159, 14eqeq12d 2208 . . . 4 (𝑥 = 𝑘 → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴)))) ↔ (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴))))))
1615imbi2d 230 . . 3 (𝑥 = 𝑘 → ((𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴))))) ↔ (𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))))))
17 oveq2 5922 . . . . 5 (𝑥 = (𝑘 + 1) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)))
18 oveq1 5921 . . . . . . 7 (𝑥 = (𝑘 + 1) → (𝑥 · 𝐴) = ((𝑘 + 1) · 𝐴))
1918fveq2d 5554 . . . . . 6 (𝑥 = (𝑘 + 1) → (cos‘(𝑥 · 𝐴)) = (cos‘((𝑘 + 1) · 𝐴)))
2018fveq2d 5554 . . . . . . 7 (𝑥 = (𝑘 + 1) → (sin‘(𝑥 · 𝐴)) = (sin‘((𝑘 + 1) · 𝐴)))
2120oveq2d 5930 . . . . . 6 (𝑥 = (𝑘 + 1) → (i · (sin‘(𝑥 · 𝐴))) = (i · (sin‘((𝑘 + 1) · 𝐴))))
2219, 21oveq12d 5932 . . . . 5 (𝑥 = (𝑘 + 1) → ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴)))) = ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴)))))
2317, 22eqeq12d 2208 . . . 4 (𝑥 = (𝑘 + 1) → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴)))) ↔ (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴))))))
2423imbi2d 230 . . 3 (𝑥 = (𝑘 + 1) → ((𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴))))) ↔ (𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴)))))))
25 oveq2 5922 . . . . 5 (𝑥 = 𝑁 → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁))
26 oveq1 5921 . . . . . . 7 (𝑥 = 𝑁 → (𝑥 · 𝐴) = (𝑁 · 𝐴))
2726fveq2d 5554 . . . . . 6 (𝑥 = 𝑁 → (cos‘(𝑥 · 𝐴)) = (cos‘(𝑁 · 𝐴)))
2826fveq2d 5554 . . . . . . 7 (𝑥 = 𝑁 → (sin‘(𝑥 · 𝐴)) = (sin‘(𝑁 · 𝐴)))
2928oveq2d 5930 . . . . . 6 (𝑥 = 𝑁 → (i · (sin‘(𝑥 · 𝐴))) = (i · (sin‘(𝑁 · 𝐴))))
3027, 29oveq12d 5932 . . . . 5 (𝑥 = 𝑁 → ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴)))) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))
3125, 30eqeq12d 2208 . . . 4 (𝑥 = 𝑁 → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴)))) ↔ (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴))))))
3231imbi2d 230 . . 3 (𝑥 = 𝑁 → ((𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑥) = ((cos‘(𝑥 · 𝐴)) + (i · (sin‘(𝑥 · 𝐴))))) ↔ (𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))))
33 coscl 11844 . . . . . 6 (𝐴 ∈ ℂ → (cos‘𝐴) ∈ ℂ)
34 ax-icn 7961 . . . . . . 7 i ∈ ℂ
35 sincl 11843 . . . . . . 7 (𝐴 ∈ ℂ → (sin‘𝐴) ∈ ℂ)
36 mulcl 7993 . . . . . . 7 ((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i · (sin‘𝐴)) ∈ ℂ)
3734, 35, 36sylancr 414 . . . . . 6 (𝐴 ∈ ℂ → (i · (sin‘𝐴)) ∈ ℂ)
38 addcl 7991 . . . . . 6 (((cos‘𝐴) ∈ ℂ ∧ (i · (sin‘𝐴)) ∈ ℂ) → ((cos‘𝐴) + (i · (sin‘𝐴))) ∈ ℂ)
3933, 37, 38syl2anc 411 . . . . 5 (𝐴 ∈ ℂ → ((cos‘𝐴) + (i · (sin‘𝐴))) ∈ ℂ)
40 exp0 10608 . . . . 5 (((cos‘𝐴) + (i · (sin‘𝐴))) ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑0) = 1)
4139, 40syl 14 . . . 4 (𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑0) = 1)
42 mul02 8400 . . . . . . . 8 (𝐴 ∈ ℂ → (0 · 𝐴) = 0)
4342fveq2d 5554 . . . . . . 7 (𝐴 ∈ ℂ → (cos‘(0 · 𝐴)) = (cos‘0))
44 cos0 11867 . . . . . . 7 (cos‘0) = 1
4543, 44eqtrdi 2242 . . . . . 6 (𝐴 ∈ ℂ → (cos‘(0 · 𝐴)) = 1)
4642fveq2d 5554 . . . . . . . . 9 (𝐴 ∈ ℂ → (sin‘(0 · 𝐴)) = (sin‘0))
47 sin0 11866 . . . . . . . . 9 (sin‘0) = 0
4846, 47eqtrdi 2242 . . . . . . . 8 (𝐴 ∈ ℂ → (sin‘(0 · 𝐴)) = 0)
4948oveq2d 5930 . . . . . . 7 (𝐴 ∈ ℂ → (i · (sin‘(0 · 𝐴))) = (i · 0))
5034mul01i 8404 . . . . . . 7 (i · 0) = 0
5149, 50eqtrdi 2242 . . . . . 6 (𝐴 ∈ ℂ → (i · (sin‘(0 · 𝐴))) = 0)
5245, 51oveq12d 5932 . . . . 5 (𝐴 ∈ ℂ → ((cos‘(0 · 𝐴)) + (i · (sin‘(0 · 𝐴)))) = (1 + 0))
53 ax-1cn 7959 . . . . . 6 1 ∈ ℂ
5453addid1i 8155 . . . . 5 (1 + 0) = 1
5552, 54eqtrdi 2242 . . . 4 (𝐴 ∈ ℂ → ((cos‘(0 · 𝐴)) + (i · (sin‘(0 · 𝐴)))) = 1)
5641, 55eqtr4d 2229 . . 3 (𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑0) = ((cos‘(0 · 𝐴)) + (i · (sin‘(0 · 𝐴)))))
57 expp1 10611 . . . . . . . . 9 ((((cos‘𝐴) + (i · (sin‘𝐴))) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) · ((cos‘𝐴) + (i · (sin‘𝐴)))))
5839, 57sylan 283 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) · ((cos‘𝐴) + (i · (sin‘𝐴)))))
5958ancoms 268 . . . . . . 7 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) · ((cos‘𝐴) + (i · (sin‘𝐴)))))
6059adantr 276 . . . . . 6 (((𝑘 ∈ ℕ0𝐴 ∈ ℂ) ∧ (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴))))) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) · ((cos‘𝐴) + (i · (sin‘𝐴)))))
61 oveq1 5921 . . . . . . 7 ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) · ((cos‘𝐴) + (i · (sin‘𝐴)))) = (((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) · ((cos‘𝐴) + (i · (sin‘𝐴)))))
6261adantl 277 . . . . . 6 (((𝑘 ∈ ℕ0𝐴 ∈ ℂ) ∧ (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴))))) → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) · ((cos‘𝐴) + (i · (sin‘𝐴)))) = (((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) · ((cos‘𝐴) + (i · (sin‘𝐴)))))
63 nn0cn 9244 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
64 mulcl 7993 . . . . . . . . . . . . 13 ((𝑘 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝑘 · 𝐴) ∈ ℂ)
6563, 64sylan 283 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (𝑘 · 𝐴) ∈ ℂ)
66 sinadd 11873 . . . . . . . . . . . 12 (((𝑘 · 𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (sin‘((𝑘 · 𝐴) + 𝐴)) = (((sin‘(𝑘 · 𝐴)) · (cos‘𝐴)) + ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))))
6765, 66sylancom 420 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (sin‘((𝑘 · 𝐴) + 𝐴)) = (((sin‘(𝑘 · 𝐴)) · (cos‘𝐴)) + ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))))
6833adantl 277 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (cos‘𝐴) ∈ ℂ)
69 sincl 11843 . . . . . . . . . . . . . 14 ((𝑘 · 𝐴) ∈ ℂ → (sin‘(𝑘 · 𝐴)) ∈ ℂ)
7065, 69syl 14 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (sin‘(𝑘 · 𝐴)) ∈ ℂ)
71 mulcom 7995 . . . . . . . . . . . . 13 (((cos‘𝐴) ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ) → ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) = ((sin‘(𝑘 · 𝐴)) · (cos‘𝐴)))
7268, 70, 71syl2anc 411 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) = ((sin‘(𝑘 · 𝐴)) · (cos‘𝐴)))
7372oveq1d 5929 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) + ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))) = (((sin‘(𝑘 · 𝐴)) · (cos‘𝐴)) + ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))))
74 mulcl 7993 . . . . . . . . . . . . 13 (((cos‘𝐴) ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ) → ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ)
7568, 70, 74syl2anc 411 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ)
76 coscl 11844 . . . . . . . . . . . . . 14 ((𝑘 · 𝐴) ∈ ℂ → (cos‘(𝑘 · 𝐴)) ∈ ℂ)
7765, 76syl 14 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (cos‘(𝑘 · 𝐴)) ∈ ℂ)
7835adantl 277 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (sin‘𝐴) ∈ ℂ)
79 mulcl 7993 . . . . . . . . . . . . 13 (((cos‘(𝑘 · 𝐴)) ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) ∈ ℂ)
8077, 78, 79syl2anc 411 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) ∈ ℂ)
81 addcom 8150 . . . . . . . . . . . 12 ((((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ ∧ ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) ∈ ℂ) → (((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) + ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))) = (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))
8275, 80, 81syl2anc 411 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) + ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))) = (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))
8367, 73, 823eqtr2d 2232 . . . . . . . . . 10 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (sin‘((𝑘 · 𝐴) + 𝐴)) = (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))
8483oveq2d 5930 . . . . . . . . 9 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (i · (sin‘((𝑘 · 𝐴) + 𝐴))) = (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))))
8584oveq2d 5930 . . . . . . . 8 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((cos‘((𝑘 · 𝐴) + 𝐴)) + (i · (sin‘((𝑘 · 𝐴) + 𝐴)))) = ((cos‘((𝑘 · 𝐴) + 𝐴)) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))))
86 adddir 8004 . . . . . . . . . . . . 13 ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑘 + 1) · 𝐴) = ((𝑘 · 𝐴) + (1 · 𝐴)))
87 mullid 8011 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
8887oveq2d 5930 . . . . . . . . . . . . . 14 (𝐴 ∈ ℂ → ((𝑘 · 𝐴) + (1 · 𝐴)) = ((𝑘 · 𝐴) + 𝐴))
89883ad2ant3 1022 . . . . . . . . . . . . 13 ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑘 · 𝐴) + (1 · 𝐴)) = ((𝑘 · 𝐴) + 𝐴))
9086, 89eqtrd 2226 . . . . . . . . . . . 12 ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑘 + 1) · 𝐴) = ((𝑘 · 𝐴) + 𝐴))
9163, 90syl3an1 1282 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0 ∧ 1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑘 + 1) · 𝐴) = ((𝑘 · 𝐴) + 𝐴))
9253, 91mp3an2 1336 . . . . . . . . . 10 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((𝑘 + 1) · 𝐴) = ((𝑘 · 𝐴) + 𝐴))
9392fveq2d 5554 . . . . . . . . 9 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (cos‘((𝑘 + 1) · 𝐴)) = (cos‘((𝑘 · 𝐴) + 𝐴)))
9492fveq2d 5554 . . . . . . . . . 10 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (sin‘((𝑘 + 1) · 𝐴)) = (sin‘((𝑘 · 𝐴) + 𝐴)))
9594oveq2d 5930 . . . . . . . . 9 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (i · (sin‘((𝑘 + 1) · 𝐴))) = (i · (sin‘((𝑘 · 𝐴) + 𝐴))))
9693, 95oveq12d 5932 . . . . . . . 8 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴)))) = ((cos‘((𝑘 · 𝐴) + 𝐴)) + (i · (sin‘((𝑘 · 𝐴) + 𝐴)))))
97 mulcl 7993 . . . . . . . . . . . . . 14 ((i ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ) → (i · (sin‘(𝑘 · 𝐴))) ∈ ℂ)
9834, 97mpan 424 . . . . . . . . . . . . 13 ((sin‘(𝑘 · 𝐴)) ∈ ℂ → (i · (sin‘(𝑘 · 𝐴))) ∈ ℂ)
9965, 69, 983syl 17 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (i · (sin‘(𝑘 · 𝐴))) ∈ ℂ)
10033, 37jca 306 . . . . . . . . . . . . 13 (𝐴 ∈ ℂ → ((cos‘𝐴) ∈ ℂ ∧ (i · (sin‘𝐴)) ∈ ℂ))
101100adantl 277 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((cos‘𝐴) ∈ ℂ ∧ (i · (sin‘𝐴)) ∈ ℂ))
102 muladd 8397 . . . . . . . . . . . 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 1248 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) · ((cos‘𝐴) + (i · (sin‘𝐴)))) = ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + ((i · (sin‘𝐴)) · (i · (sin‘(𝑘 · 𝐴))))) + (((cos‘(𝑘 · 𝐴)) · (i · (sin‘𝐴))) + ((cos‘𝐴) · (i · (sin‘(𝑘 · 𝐴)))))))
10478, 34jctil 312 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ))
10570, 34jctil 312 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (i ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ))
106 mul4 8145 . . . . . . . . . . . . . . 15 (((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) ∧ (i ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ)) → ((i · (sin‘𝐴)) · (i · (sin‘(𝑘 · 𝐴)))) = ((i · i) · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))))
107 ixi 8596 . . . . . . . . . . . . . . . 16 (i · i) = -1
108107oveq1i 5924 . . . . . . . . . . . . . . 15 ((i · i) · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) = (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))
109106, 108eqtrdi 2242 . . . . . . . . . . . . . 14 (((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) ∧ (i ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ)) → ((i · (sin‘𝐴)) · (i · (sin‘(𝑘 · 𝐴)))) = (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))))
110104, 105, 109syl2anc 411 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((i · (sin‘𝐴)) · (i · (sin‘(𝑘 · 𝐴)))) = (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))))
111110oveq2d 5930 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + ((i · (sin‘𝐴)) · (i · (sin‘(𝑘 · 𝐴))))) = (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))))
112111oveq1d 5929 . . . . . . . . . . 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 8142 . . . . . . . . . . . . . . . 16 (((cos‘(𝑘 · 𝐴)) ∈ ℂ ∧ i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → ((cos‘(𝑘 · 𝐴)) · (i · (sin‘𝐴))) = (i · ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))))
11434, 113mp3an2 1336 . . . . . . . . . . . . . . 15 (((cos‘(𝑘 · 𝐴)) ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → ((cos‘(𝑘 · 𝐴)) · (i · (sin‘𝐴))) = (i · ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))))
11577, 78, 114syl2anc 411 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((cos‘(𝑘 · 𝐴)) · (i · (sin‘𝐴))) = (i · ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))))
116 mul12 8142 . . . . . . . . . . . . . . . 16 (((cos‘𝐴) ∈ ℂ ∧ i ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ) → ((cos‘𝐴) · (i · (sin‘(𝑘 · 𝐴)))) = (i · ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))
11734, 116mp3an2 1336 . . . . . . . . . . . . . . 15 (((cos‘𝐴) ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ) → ((cos‘𝐴) · (i · (sin‘(𝑘 · 𝐴)))) = (i · ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))
11868, 70, 117syl2anc 411 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((cos‘𝐴) · (i · (sin‘(𝑘 · 𝐴)))) = (i · ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))
119115, 118oveq12d 5932 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) · (i · (sin‘𝐴))) + ((cos‘𝐴) · (i · (sin‘(𝑘 · 𝐴))))) = ((i · ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))) + (i · ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))))
120 adddi 7998 . . . . . . . . . . . . . . 15 ((i ∈ ℂ ∧ ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) ∈ ℂ ∧ ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ) → (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))) = ((i · ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))) + (i · ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))))
12134, 120mp3an1 1335 . . . . . . . . . . . . . 14 ((((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) ∈ ℂ ∧ ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ) → (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))) = ((i · ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))) + (i · ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))))
12280, 75, 121syl2anc 411 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))) = ((i · ((cos‘(𝑘 · 𝐴)) · (sin‘𝐴))) + (i · ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))))
123119, 122eqtr4d 2229 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) · (i · (sin‘𝐴))) + ((cos‘𝐴) · (i · (sin‘(𝑘 · 𝐴))))) = (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴))))))
124123oveq2d 5930 . . . . . . . . . . 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 2230 . . . . . . . . . 10 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) · ((cos‘𝐴) + (i · (sin‘𝐴)))) = ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))))
126 mulcl 7993 . . . . . . . . . . . . . 14 (((sin‘𝐴) ∈ ℂ ∧ (sin‘(𝑘 · 𝐴)) ∈ ℂ) → ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ)
12778, 70, 126syl2anc 411 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ)
128 mulm1 8413 . . . . . . . . . . . . 13 (((sin‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ → (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) = -((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))
129127, 128syl 14 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) = -((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))
130129oveq2d 5930 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))) = (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + -((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))))
131130oveq1d 5929 . . . . . . . . . 10 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + (-1 · ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))) = ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + -((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))))
132 mulcl 7993 . . . . . . . . . . . . 13 (((cos‘(𝑘 · 𝐴)) ∈ ℂ ∧ (cos‘𝐴) ∈ ℂ) → ((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) ∈ ℂ)
13377, 68, 132syl2anc 411 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) ∈ ℂ)
134 negsub 8261 . . . . . . . . . . . 12 ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) ∈ ℂ ∧ ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))) ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + -((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) = (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))))
135133, 127, 134syl2anc 411 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + -((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) = (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))))
136135oveq1d 5929 . . . . . . . . . 10 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) + -((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))) = ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))))
137125, 131, 1363eqtrd 2230 . . . . . . . . 9 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) · ((cos‘𝐴) + (i · (sin‘𝐴)))) = ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))))
138 cosadd 11874 . . . . . . . . . . . 12 (((𝑘 · 𝐴) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (cos‘((𝑘 · 𝐴) + 𝐴)) = (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘(𝑘 · 𝐴)) · (sin‘𝐴))))
13965, 138sylancom 420 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (cos‘((𝑘 · 𝐴) + 𝐴)) = (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘(𝑘 · 𝐴)) · (sin‘𝐴))))
140 mulcom 7995 . . . . . . . . . . . . 13 (((sin‘(𝑘 · 𝐴)) ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → ((sin‘(𝑘 · 𝐴)) · (sin‘𝐴)) = ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))
14170, 78, 140syl2anc 411 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((sin‘(𝑘 · 𝐴)) · (sin‘𝐴)) = ((sin‘𝐴) · (sin‘(𝑘 · 𝐴))))
142141oveq2d 5930 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘(𝑘 · 𝐴)) · (sin‘𝐴))) = (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))))
143139, 142eqtrd 2226 . . . . . . . . . 10 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (cos‘((𝑘 · 𝐴) + 𝐴)) = (((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))))
144143oveq1d 5929 . . . . . . . . 9 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → ((cos‘((𝑘 · 𝐴) + 𝐴)) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))) = ((((cos‘(𝑘 · 𝐴)) · (cos‘𝐴)) − ((sin‘𝐴) · (sin‘(𝑘 · 𝐴)))) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))))
145137, 144eqtr4d 2229 . . . . . . . 8 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) · ((cos‘𝐴) + (i · (sin‘𝐴)))) = ((cos‘((𝑘 · 𝐴) + 𝐴)) + (i · (((cos‘(𝑘 · 𝐴)) · (sin‘𝐴)) + ((cos‘𝐴) · (sin‘(𝑘 · 𝐴)))))))
14685, 96, 1453eqtr4rd 2237 . . . . . . 7 ((𝑘 ∈ ℕ0𝐴 ∈ ℂ) → (((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) · ((cos‘𝐴) + (i · (sin‘𝐴)))) = ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴)))))
147146adantr 276 . . . . . 6 (((𝑘 ∈ ℕ0𝐴 ∈ ℂ) ∧ (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴))))) → (((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) · ((cos‘𝐴) + (i · (sin‘𝐴)))) = ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴)))))
14860, 62, 1473eqtrd 2230 . . . . 5 (((𝑘 ∈ ℕ0𝐴 ∈ ℂ) ∧ (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴))))) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴)))))
149148exp31 364 . . . 4 (𝑘 ∈ ℕ0 → (𝐴 ∈ ℂ → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴)))) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴)))))))
150149a2d 26 . . 3 (𝑘 ∈ ℕ0 → ((𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑘) = ((cos‘(𝑘 · 𝐴)) + (i · (sin‘(𝑘 · 𝐴))))) → (𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑(𝑘 + 1)) = ((cos‘((𝑘 + 1) · 𝐴)) + (i · (sin‘((𝑘 + 1) · 𝐴)))))))
1518, 16, 24, 32, 56, 150nn0ind 9425 . 2 (𝑁 ∈ ℕ0 → (𝐴 ∈ ℂ → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴))))))
152151impcom 125 1 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  w3a 980   = wceq 1364  wcel 2164  cfv 5250  (class class class)co 5914  cc 7864  0cc0 7866  1c1 7867  ici 7868   + caddc 7869   · cmul 7871  cmin 8184  -cneg 8185  0cn0 9234  cexp 10603  sincsin 11781  cosccos 11782
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 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-coll 4144  ax-sep 4147  ax-nul 4155  ax-pow 4203  ax-pr 4238  ax-un 4462  ax-setind 4567  ax-iinf 4618  ax-cnex 7957  ax-resscn 7958  ax-1cn 7959  ax-1re 7960  ax-icn 7961  ax-addcl 7962  ax-addrcl 7963  ax-mulcl 7964  ax-mulrcl 7965  ax-addcom 7966  ax-mulcom 7967  ax-addass 7968  ax-mulass 7969  ax-distr 7970  ax-i2m1 7971  ax-0lt1 7972  ax-1rid 7973  ax-0id 7974  ax-rnegex 7975  ax-precex 7976  ax-cnre 7977  ax-pre-ltirr 7978  ax-pre-ltwlin 7979  ax-pre-lttrn 7980  ax-pre-apti 7981  ax-pre-ltadd 7982  ax-pre-mulgt0 7983  ax-pre-mulext 7984  ax-arch 7985  ax-caucvg 7986
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rmo 2480  df-rab 2481  df-v 2762  df-sbc 2986  df-csb 3081  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3447  df-if 3558  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-int 3871  df-iun 3914  df-disj 4007  df-br 4030  df-opab 4091  df-mpt 4092  df-tr 4128  df-id 4322  df-po 4325  df-iso 4326  df-iord 4395  df-on 4397  df-ilim 4398  df-suc 4400  df-iom 4621  df-xp 4663  df-rel 4664  df-cnv 4665  df-co 4666  df-dm 4667  df-rn 4668  df-res 4669  df-ima 4670  df-iota 5211  df-fun 5252  df-fn 5253  df-f 5254  df-f1 5255  df-fo 5256  df-f1o 5257  df-fv 5258  df-isom 5259  df-riota 5869  df-ov 5917  df-oprab 5918  df-mpo 5919  df-1st 6188  df-2nd 6189  df-recs 6353  df-irdg 6418  df-frec 6439  df-1o 6464  df-oadd 6468  df-er 6582  df-en 6790  df-dom 6791  df-fin 6792  df-sup 7037  df-pnf 8050  df-mnf 8051  df-xr 8052  df-ltxr 8053  df-le 8054  df-sub 8186  df-neg 8187  df-reap 8588  df-ap 8595  df-div 8686  df-inn 8977  df-2 9035  df-3 9036  df-4 9037  df-n0 9235  df-z 9312  df-uz 9587  df-q 9679  df-rp 9714  df-ico 9954  df-fz 10069  df-fzo 10203  df-seqfrec 10513  df-exp 10604  df-fac 10791  df-bc 10813  df-ihash 10841  df-cj 10980  df-re 10981  df-im 10982  df-rsqrt 11136  df-abs 11137  df-clim 11416  df-sumdc 11491  df-ef 11785  df-sin 11787  df-cos 11788
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator