# 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}\in ℂ\to {F}\left({A}\right)=\frac{{\mathrm{e}}^{\mathrm{i}{A}}{O}{\mathrm{e}}^{\left(-\mathrm{i}\right){A}}}{{D}}$
sinperlem.2 ${⊢}{A}+{K}2\mathrm{\pi }\in ℂ\to {F}\left({A}+{K}2\mathrm{\pi }\right)=\frac{{\mathrm{e}}^{\mathrm{i}\left({A}+{K}2\mathrm{\pi }\right)}{O}{\mathrm{e}}^{\left(-\mathrm{i}\right)\left({A}+{K}2\mathrm{\pi }\right)}}{{D}}$
Assertion sinperlem ${⊢}\left({A}\in ℂ\wedge {K}\in ℤ\right)\to {F}\left({A}+{K}2\mathrm{\pi }\right)={F}\left({A}\right)$

### Proof

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