Metamath Proof Explorer

Theorem sinperlem

Description: Lemma for sinper and cosper . (Contributed by Paul Chapman, 23-Jan-2008) (Revised by Mario Carneiro, 10-May-2014)

Ref Expression
Hypotheses sinperlem.1 ⊢ A ∈ ℂ → F ⁡ A = e i ⁢ A O e − i ⁢ A D
sinperlem.2 ⊢ A + K ⁢ 2 ⁢ π ∈ ℂ → F ⁡ A + K ⁢ 2 ⁢ π = e i ⁢ A + K ⁢ 2 ⁢ π O e − i ⁢ A + K ⁢ 2 ⁢ π D
Assertion sinperlem ⊢ A ∈ ℂ ∧ K ∈ ℤ → F ⁡ A + K ⁢ 2 ⁢ π = F ⁡ A

Proof

Step Hyp Ref Expression
1 sinperlem.1 ⊢ A ∈ ℂ → F ⁡ A = e i ⁢ A O e − i ⁢ A D
2 sinperlem.2 ⊢ A + K ⁢ 2 ⁢ π ∈ ℂ → F ⁡ A + K ⁢ 2 ⁢ π = e i ⁢ A + K ⁢ 2 ⁢ π O e − i ⁢ A + K ⁢ 2 ⁢ π D
3 zcn ⊢ K ∈ ℤ → K ∈ ℂ
4 2cn ⊢ 2 ∈ ℂ
5 picn ⊢ π ∈ ℂ
6 4 5 mulcli ⊢ 2 ⁢ π ∈ ℂ
7 mulcl ⊢ K ∈ ℂ ∧ 2 ⁢ π ∈ ℂ → K ⁢ 2 ⁢ π ∈ ℂ
8 3 6 7 sylancl ⊢ K ∈ ℤ → K ⁢ 2 ⁢ π ∈ ℂ
9 ax-icn ⊢ i ∈ ℂ
10 adddi ⊢ i ∈ ℂ ∧ A ∈ ℂ ∧ K ⁢ 2 ⁢ π ∈ ℂ → i ⁢ A + K ⁢ 2 ⁢ π = i ⁢ A + i ⁢ K ⁢ 2 ⁢ π
11 9 10 mp3an1 ⊢ A ∈ ℂ ∧ K ⁢ 2 ⁢ π ∈ ℂ → i ⁢ A + K ⁢ 2 ⁢ π = i ⁢ A + i ⁢ K ⁢ 2 ⁢ π
12 8 11 sylan2 ⊢ A ∈ ℂ ∧ K ∈ ℤ → i ⁢ A + K ⁢ 2 ⁢ π = i ⁢ A + i ⁢ K ⁢ 2 ⁢ π
13 mul12 ⊢ i ∈ ℂ ∧ K ∈ ℂ ∧ 2 ⁢ π ∈ ℂ → i ⁢ K ⁢ 2 ⁢ π = K ⁢ i ⁢ 2 ⁢ π
14 9 6 13 mp3an13 ⊢ K ∈ ℂ → i ⁢ K ⁢ 2 ⁢ π = K ⁢ i ⁢ 2 ⁢ π
15 3 14 syl ⊢ K ∈ ℤ → i ⁢ K ⁢ 2 ⁢ π = K ⁢ i ⁢ 2 ⁢ π
16 9 6 mulcli ⊢ i ⁢ 2 ⁢ π ∈ ℂ
17 mulcom ⊢ K ∈ ℂ ∧ i ⁢ 2 ⁢ π ∈ ℂ → K ⁢ i ⁢ 2 ⁢ π = i ⁢ 2 ⁢ π ⁢ K
18 3 16 17 sylancl ⊢ K ∈ ℤ → K ⁢ i ⁢ 2 ⁢ π = i ⁢ 2 ⁢ π ⁢ K
19 15 18 eqtrd ⊢ K ∈ ℤ → i ⁢ K ⁢ 2 ⁢ π = i ⁢ 2 ⁢ π ⁢ K
20 19 adantl ⊢ A ∈ ℂ ∧ K ∈ ℤ → i ⁢ K ⁢ 2 ⁢ π = i ⁢ 2 ⁢ π ⁢ K
21 20 oveq2d ⊢ A ∈ ℂ ∧ K ∈ ℤ → i ⁢ A + i ⁢ K ⁢ 2 ⁢ π = i ⁢ A + i ⁢ 2 ⁢ π ⁢ K
22 12 21 eqtrd ⊢ A ∈ ℂ ∧ K ∈ ℤ → i ⁢ A + K ⁢ 2 ⁢ π = i ⁢ A + i ⁢ 2 ⁢ π ⁢ K
23 22 fveq2d ⊢ A ∈ ℂ ∧ K ∈ ℤ → e i ⁢ A + K ⁢ 2 ⁢ π = e i ⁢ A + i ⁢ 2 ⁢ π ⁢ K
24 mulcl ⊢ i ∈ ℂ ∧ A ∈ ℂ → i ⁢ A ∈ ℂ
25 9 24 mpan ⊢ A ∈ ℂ → i ⁢ A ∈ ℂ
26 efper ⊢ i ⁢ A ∈ ℂ ∧ K ∈ ℤ → e i ⁢ A + i ⁢ 2 ⁢ π ⁢ K = e i ⁢ A
27 25 26 sylan ⊢ A ∈ ℂ ∧ K ∈ ℤ → e i ⁢ A + i ⁢ 2 ⁢ π ⁢ K = e i ⁢ A
28 23 27 eqtrd ⊢ A ∈ ℂ ∧ K ∈ ℤ → e i ⁢ A + K ⁢ 2 ⁢ π = e i ⁢ A
29 negicn ⊢ − i ∈ ℂ
30 adddi ⊢ − i ∈ ℂ ∧ A ∈ ℂ ∧ K ⁢ 2 ⁢ π ∈ ℂ → − i ⁢ A + K ⁢ 2 ⁢ π = − i ⁢ A + − i ⁢ K ⁢ 2 ⁢ π
31 29 30 mp3an1 ⊢ A ∈ ℂ ∧ K ⁢ 2 ⁢ π ∈ ℂ → − i ⁢ A + K ⁢ 2 ⁢ π = − i ⁢ A + − i ⁢ K ⁢ 2 ⁢ π
32 8 31 sylan2 ⊢ A ∈ ℂ ∧ K ∈ ℤ → − i ⁢ A + K ⁢ 2 ⁢ π = − i ⁢ A + − i ⁢ K ⁢ 2 ⁢ π
33 19 negeqd ⊢ K ∈ ℤ → − i ⁢ K ⁢ 2 ⁢ π = − i ⁢ 2 ⁢ π ⁢ K
34 mulneg1 ⊢ i ∈ ℂ ∧ K ⁢ 2 ⁢ π ∈ ℂ → − i ⁢ K ⁢ 2 ⁢ π = − i ⁢ K ⁢ 2 ⁢ π
35 9 8 34 sylancr ⊢ K ∈ ℤ → − i ⁢ K ⁢ 2 ⁢ π = − i ⁢ K ⁢ 2 ⁢ π
36 mulneg2 ⊢ i ⁢ 2 ⁢ π ∈ ℂ ∧ K ∈ ℂ → i ⁢ 2 ⁢ π ⁢ − K = − i ⁢ 2 ⁢ π ⁢ K
37 16 3 36 sylancr ⊢ K ∈ ℤ → i ⁢ 2 ⁢ π ⁢ − K = − i ⁢ 2 ⁢ π ⁢ K
38 33 35 37 3eqtr4d ⊢ K ∈ ℤ → − i ⁢ K ⁢ 2 ⁢ π = i ⁢ 2 ⁢ π ⁢ − K
39 38 adantl ⊢ A ∈ ℂ ∧ K ∈ ℤ → − i ⁢ K ⁢ 2 ⁢ π = i ⁢ 2 ⁢ π ⁢ − K
40 39 oveq2d ⊢ A ∈ ℂ ∧ K ∈ ℤ → − i ⁢ A + − i ⁢ K ⁢ 2 ⁢ π = − i ⁢ A + i ⁢ 2 ⁢ π ⁢ − K
41 32 40 eqtrd ⊢ A ∈ ℂ ∧ K ∈ ℤ → − i ⁢ A + K ⁢ 2 ⁢ π = − i ⁢ A + i ⁢ 2 ⁢ π ⁢ − K
42 41 fveq2d ⊢ A ∈ ℂ ∧ K ∈ ℤ → e − i ⁢ A + K ⁢ 2 ⁢ π = e − i ⁢ A + i ⁢ 2 ⁢ π ⁢ − K
43 mulcl ⊢ − i ∈ ℂ ∧ A ∈ ℂ → − i ⁢ A ∈ ℂ
44 29 43 mpan ⊢ A ∈ ℂ → − i ⁢ A ∈ ℂ
45 znegcl ⊢ K ∈ ℤ → − K ∈ ℤ
46 efper ⊢ − i ⁢ A ∈ ℂ ∧ − K ∈ ℤ → e − i ⁢ A + i ⁢ 2 ⁢ π ⁢ − K = e − i ⁢ A
47 44 45 46 syl2an ⊢ A ∈ ℂ ∧ K ∈ ℤ → e − i ⁢ A + i ⁢ 2 ⁢ π ⁢ − K = e − i ⁢ A
48 42 47 eqtrd ⊢ A ∈ ℂ ∧ K ∈ ℤ → e − i ⁢ A + K ⁢ 2 ⁢ π = e − i ⁢ A
49 28 48 oveq12d ⊢ A ∈ ℂ ∧ K ∈ ℤ → e i ⁢ A + K ⁢ 2 ⁢ π O e − i ⁢ A + K ⁢ 2 ⁢ π = e i ⁢ A O e − i ⁢ A
50 49 oveq1d ⊢ A ∈ ℂ ∧ K ∈ ℤ → e i ⁢ A + K ⁢ 2 ⁢ π O e − i ⁢ A + K ⁢ 2 ⁢ π D = e i ⁢ A O e − i ⁢ A D
51 addcl ⊢ A ∈ ℂ ∧ K ⁢ 2 ⁢ π ∈ ℂ → A + K ⁢ 2 ⁢ π ∈ ℂ
52 8 51 sylan2 ⊢ A ∈ ℂ ∧ K ∈ ℤ → A + K ⁢ 2 ⁢ π ∈ ℂ
53 52 2 syl ⊢ A ∈ ℂ ∧ K ∈ ℤ → F ⁡ A + K ⁢ 2 ⁢ π = e i ⁢ A + K ⁢ 2 ⁢ π O e − i ⁢ A + K ⁢ 2 ⁢ π D
54 1 adantr ⊢ A ∈ ℂ ∧ K ∈ ℤ → F ⁡ A = e i ⁢ A O e − i ⁢ A D
55 50 53 54 3eqtr4d ⊢ A ∈ ℂ ∧ K ∈ ℤ → F ⁡ A + K ⁢ 2 ⁢ π = F ⁡ A