Metamath Proof Explorer

Theorem dirkerper

Description: the Dirichlet Kernel has period 2 _pi . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dirkerper.1 ⊢D=n∈ℕ⟼y∈ℝ⟼ifymod2⁢π=02⁢n+12⁢πsin⁡n+12⁢y2⁢π⁢sin⁡y2
dirkerper.2 ⊢T=2⁢π
Assertion dirkerper ⊢N∈ℕ∧x∈ℝ→D⁡N⁡x+T=D⁡N⁡x

Proof

Step Hyp Ref Expression
1 dirkerper.1 ⊢D=n∈ℕ⟼y∈ℝ⟼ifymod2⁢π=02⁢n+12⁢πsin⁡n+12⁢y2⁢π⁢sin⁡y2
2 dirkerper.2 ⊢T=2⁢π
3 2 eqcomi ⊢2⁢π=T
4 3 oveq2i ⊢1⁢2⁢π=1⁢T
5 2re ⊢2∈ℝ
6 pire ⊢π∈ℝ
7 5 6 remulcli ⊢2⁢π∈ℝ
8 2 7 eqeltri ⊢T∈ℝ
9 8 recni ⊢T∈ℂ
10 9 mullidi ⊢1⁢T=T
11 4 10 eqtri ⊢1⁢2⁢π=T
12 11 oveq2i ⊢x+1⁢2⁢π=x+T
13 12 eqcomi ⊢x+T=x+1⁢2⁢π
14 13 oveq1i ⊢x+Tmod2⁢π=x+1⁢2⁢πmod2⁢π
15 14 a1i ⊢N∈ℕ∧x∈ℝ∧xmod2⁢π=0→x+Tmod2⁢π=x+1⁢2⁢πmod2⁢π
16 id ⊢x∈ℝ→x∈ℝ
17 16 ad2antlr ⊢N∈ℕ∧x∈ℝ∧xmod2⁢π=0→x∈ℝ
18 2rp ⊢2∈ℝ+
19 pirp ⊢π∈ℝ+
20 rpmulcl ⊢2∈ℝ+∧π∈ℝ+→2⁢π∈ℝ+
21 18 19 20 mp2an ⊢2⁢π∈ℝ+
22 21 a1i ⊢N∈ℕ∧x∈ℝ∧xmod2⁢π=0→2⁢π∈ℝ+
23 1z ⊢1∈ℤ
24 23 a1i ⊢N∈ℕ∧x∈ℝ∧xmod2⁢π=0→1∈ℤ
25 modcyc ⊢x∈ℝ∧2⁢π∈ℝ+∧1∈ℤ→x+1⁢2⁢πmod2⁢π=xmod2⁢π
26 17 22 24 25 syl3anc ⊢N∈ℕ∧x∈ℝ∧xmod2⁢π=0→x+1⁢2⁢πmod2⁢π=xmod2⁢π
27 simpr ⊢N∈ℕ∧x∈ℝ∧xmod2⁢π=0→xmod2⁢π=0
28 15 26 27 3eqtrd ⊢N∈ℕ∧x∈ℝ∧xmod2⁢π=0→x+Tmod2⁢π=0
29 28 iftrued ⊢N∈ℕ∧x∈ℝ∧xmod2⁢π=0→ifx+Tmod2⁢π=02⋅ N+12⁢πsin⁡N+12⁢x+T2⁢π⁢sin⁡x+T2=2⋅ N+12⁢π
30 iftrue ⊢xmod2⁢π=0→ifxmod2⁢π=02⋅ N+12⁢πsin⁡N+12⁢x2⁢π⁢sin⁡x2=2⋅ N+12⁢π
31 30 adantl ⊢N∈ℕ∧x∈ℝ∧xmod2⁢π=0→ifxmod2⁢π=02⋅ N+12⁢πsin⁡N+12⁢x2⁢π⁢sin⁡x2=2⋅ N+12⁢π
32 29 31 eqtr4d ⊢N∈ℕ∧x∈ℝ∧xmod2⁢π=0→ifx+Tmod2⁢π=02⋅ N+12⁢πsin⁡N+12⁢x+T2⁢π⁢sin⁡x+T2=ifxmod2⁢π=02⋅ N+12⁢πsin⁡N+12⁢x2⁢π⁢sin⁡x2
33 iffalse ⊢¬xmod2⁢π=0→ifxmod2⁢π=02⋅ N+12⁢πsin⁡N+12⁢x2⁢π⁢sin⁡x2=sin⁡N+12⁢x2⁢π⁢sin⁡x2
34 33 adantl ⊢N∈ℕ∧x∈ℝ∧¬xmod2⁢π=0→ifxmod2⁢π=02⋅ N+12⁢πsin⁡N+12⁢x2⁢π⁢sin⁡x2=sin⁡N+12⁢x2⁢π⁢sin⁡x2
35 nncn ⊢N∈ℕ→N∈ℂ
36 halfcn ⊢12∈ℂ
37 36 a1i ⊢N∈ℕ→12∈ℂ
38 35 37 addcld ⊢N∈ℕ→N+12∈ℂ
39 38 adantr ⊢N∈ℕ∧x∈ℝ→N+12∈ℂ
40 recn ⊢x∈ℝ→x∈ℂ
41 40 adantl ⊢N∈ℕ∧x∈ℝ→x∈ℂ
42 39 41 mulcld ⊢N∈ℕ∧x∈ℝ→N+12⁢x∈ℂ
43 42 sincld ⊢N∈ℕ∧x∈ℝ→sin⁡N+12⁢x∈ℂ
44 43 adantr ⊢N∈ℕ∧x∈ℝ∧¬xmod2⁢π=0→sin⁡N+12⁢x∈ℂ
45 7 recni ⊢2⁢π∈ℂ
46 45 a1i ⊢N∈ℕ∧x∈ℝ→2⁢π∈ℂ
47 41 halfcld ⊢N∈ℕ∧x∈ℝ→x2∈ℂ
48 47 sincld ⊢N∈ℕ∧x∈ℝ→sin⁡x2∈ℂ
49 46 48 mulcld ⊢N∈ℕ∧x∈ℝ→2⁢π⁢sin⁡x2∈ℂ
50 49 adantr ⊢N∈ℕ∧x∈ℝ∧¬xmod2⁢π=0→2⁢π⁢sin⁡x2∈ℂ
51 dirkerdenne0 ⊢x∈ℝ∧¬xmod2⁢π=0→2⁢π⁢sin⁡x2≠0
52 51 adantll ⊢N∈ℕ∧x∈ℝ∧¬xmod2⁢π=0→2⁢π⁢sin⁡x2≠0
53 44 50 52 div2negd ⊢N∈ℕ∧x∈ℝ∧¬xmod2⁢π=0→−sin⁡N+12⁢x−2⁢π⁢sin⁡x2=sin⁡N+12⁢x2⁢π⁢sin⁡x2
54 14 a1i ⊢x∈ℝ→x+Tmod2⁢π=x+1⁢2⁢πmod2⁢π
55 21 23 25 mp3an23 ⊢x∈ℝ→x+1⁢2⁢πmod2⁢π=xmod2⁢π
56 54 55 eqtrd ⊢x∈ℝ→x+Tmod2⁢π=xmod2⁢π
57 56 adantr ⊢x∈ℝ∧¬xmod2⁢π=0→x+Tmod2⁢π=xmod2⁢π
58 simpr ⊢x∈ℝ∧¬xmod2⁢π=0→¬xmod2⁢π=0
59 58 neqned ⊢x∈ℝ∧¬xmod2⁢π=0→xmod2⁢π≠0
60 57 59 eqnetrd ⊢x∈ℝ∧¬xmod2⁢π=0→x+Tmod2⁢π≠0
61 60 neneqd ⊢x∈ℝ∧¬xmod2⁢π=0→¬x+Tmod2⁢π=0
62 iffalse ⊢¬x+Tmod2⁢π=0→ifx+Tmod2⁢π=02⋅ N+12⁢πsin⁡N+12⁢x+T2⁢π⁢sin⁡x+T2=sin⁡N+12⁢x+T2⁢π⁢sin⁡x+T2
63 2 oveq2i ⊢x+T=x+2⁢π
64 63 oveq2i ⊢N+12⁢x+T=N+12⁢x+2⁢π
65 64 fveq2i ⊢sin⁡N+12⁢x+T=sin⁡N+12⁢x+2⁢π
66 63 oveq1i ⊢x+T2=x+2⁢π2
67 66 fveq2i ⊢sin⁡x+T2=sin⁡x+2⁢π2
68 67 oveq2i ⊢2⁢π⁢sin⁡x+T2=2⁢π⁢sin⁡x+2⁢π2
69 65 68 oveq12i ⊢sin⁡N+12⁢x+T2⁢π⁢sin⁡x+T2=sin⁡N+12⁢x+2⁢π2⁢π⁢sin⁡x+2⁢π2
70 62 69 eqtrdi ⊢¬x+Tmod2⁢π=0→ifx+Tmod2⁢π=02⋅ N+12⁢πsin⁡N+12⁢x+T2⁢π⁢sin⁡x+T2=sin⁡N+12⁢x+2⁢π2⁢π⁢sin⁡x+2⁢π2
71 61 70 syl ⊢x∈ℝ∧¬xmod2⁢π=0→ifx+Tmod2⁢π=02⋅ N+12⁢πsin⁡N+12⁢x+T2⁢π⁢sin⁡x+T2=sin⁡N+12⁢x+2⁢π2⁢π⁢sin⁡x+2⁢π2
72 71 adantll ⊢N∈ℕ∧x∈ℝ∧¬xmod2⁢π=0→ifx+Tmod2⁢π=02⋅ N+12⁢πsin⁡N+12⁢x+T2⁢π⁢sin⁡x+T2=sin⁡N+12⁢x+2⁢π2⁢π⁢sin⁡x+2⁢π2
73 45 a1i ⊢N∈ℕ→2⁢π∈ℂ
74 35 37 73 adddird ⊢N∈ℕ→N+12⁢2⁢π=N⁢2⁢π+12⁢2⁢π
75 ax-1cn ⊢1∈ℂ
76 2cnne0 ⊢2∈ℂ∧2≠0
77 2cn ⊢2∈ℂ
78 picn ⊢π∈ℂ
79 77 78 mulcli ⊢2⁢π∈ℂ
80 div32 ⊢1∈ℂ∧2∈ℂ∧2≠0∧2⁢π∈ℂ→12⁢2⁢π=1⁢2⁢π2
81 75 76 79 80 mp3an ⊢12⁢2⁢π=1⁢2⁢π2
82 2ne0 ⊢2≠0
83 79 77 82 divcli ⊢2⁢π2∈ℂ
84 83 mullidi ⊢1⁢2⁢π2=2⁢π2
85 78 77 82 divcan3i ⊢2⁢π2=π
86 84 85 eqtri ⊢1⁢2⁢π2=π
87 81 86 eqtri ⊢12⁢2⁢π=π
88 87 oveq2i ⊢N⁢2⁢π+12⁢2⁢π=N⁢2⁢π+π
89 74 88 eqtrdi ⊢N∈ℕ→N+12⁢2⁢π=N⁢2⁢π+π
90 89 oveq2d ⊢N∈ℕ→N+12⁢x+N+12⁢2⁢π=N+12⁢x+N⁢2⁢π+π
91 90 adantr ⊢N∈ℕ∧x∈ℝ→N+12⁢x+N+12⁢2⁢π=N+12⁢x+N⁢2⁢π+π
92 39 41 46 adddid ⊢N∈ℕ∧x∈ℝ→N+12⁢x+2⁢π=N+12⁢x+N+12⁢2⁢π
93 35 73 mulcld ⊢N∈ℕ→N⁢2⁢π∈ℂ
94 93 adantr ⊢N∈ℕ∧x∈ℝ→N⁢2⁢π∈ℂ
95 78 a1i ⊢N∈ℕ∧x∈ℝ→π∈ℂ
96 42 94 95 addassd ⊢N∈ℕ∧x∈ℝ→N+12⁢x+N⁢2⁢π+π=N+12⁢x+N⁢2⁢π+π
97 91 92 96 3eqtr4d ⊢N∈ℕ∧x∈ℝ→N+12⁢x+2⁢π=N+12⁢x+N⁢2⁢π+π
98 97 fveq2d ⊢N∈ℕ∧x∈ℝ→sin⁡N+12⁢x+2⁢π=sin⁡N+12⁢x+N⁢2⁢π+π
99 42 94 addcld ⊢N∈ℕ∧x∈ℝ→N+12⁢x+N⁢2⁢π∈ℂ
100 sinppi ⊢N+12⁢x+N⁢2⁢π∈ℂ→sin⁡N+12⁢x+N⁢2⁢π+π=−sin⁡N+12⁢x+N⁢2⁢π
101 99 100 syl ⊢N∈ℕ∧x∈ℝ→sin⁡N+12⁢x+N⁢2⁢π+π=−sin⁡N+12⁢x+N⁢2⁢π
102 simpl ⊢N∈ℕ∧x∈ℝ→N∈ℕ
103 102 nnzd ⊢N∈ℕ∧x∈ℝ→N∈ℤ
104 sinper ⊢N+12⁢x∈ℂ∧N∈ℤ→sin⁡N+12⁢x+N⁢2⁢π=sin⁡N+12⁢x
105 42 103 104 syl2anc ⊢N∈ℕ∧x∈ℝ→sin⁡N+12⁢x+N⁢2⁢π=sin⁡N+12⁢x
106 105 negeqd ⊢N∈ℕ∧x∈ℝ→−sin⁡N+12⁢x+N⁢2⁢π=−sin⁡N+12⁢x
107 98 101 106 3eqtrd ⊢N∈ℕ∧x∈ℝ→sin⁡N+12⁢x+2⁢π=−sin⁡N+12⁢x
108 45 a1i ⊢x∈ℝ→2⁢π∈ℂ
109 77 a1i ⊢x∈ℝ→2∈ℂ
110 82 a1i ⊢x∈ℝ→2≠0
111 40 108 109 110 divdird ⊢x∈ℝ→x+2⁢π2=x2+2⁢π2
112 85 a1i ⊢x∈ℝ→2⁢π2=π
113 112 oveq2d ⊢x∈ℝ→x2+2⁢π2=x2+π
114 111 113 eqtrd ⊢x∈ℝ→x+2⁢π2=x2+π
115 114 fveq2d ⊢x∈ℝ→sin⁡x+2⁢π2=sin⁡x2+π
116 40 halfcld ⊢x∈ℝ→x2∈ℂ
117 sinppi ⊢x2∈ℂ→sin⁡x2+π=−sin⁡x2
118 116 117 syl ⊢x∈ℝ→sin⁡x2+π=−sin⁡x2
119 115 118 eqtrd ⊢x∈ℝ→sin⁡x+2⁢π2=−sin⁡x2
120 119 oveq2d ⊢x∈ℝ→2⁢π⁢sin⁡x+2⁢π2=2⁢π⁢−sin⁡x2
121 120 adantl ⊢N∈ℕ∧x∈ℝ→2⁢π⁢sin⁡x+2⁢π2=2⁢π⁢−sin⁡x2
122 107 121 oveq12d ⊢N∈ℕ∧x∈ℝ→sin⁡N+12⁢x+2⁢π2⁢π⁢sin⁡x+2⁢π2=−sin⁡N+12⁢x2⁢π⁢−sin⁡x2
123 122 adantr ⊢N∈ℕ∧x∈ℝ∧¬xmod2⁢π=0→sin⁡N+12⁢x+2⁢π2⁢π⁢sin⁡x+2⁢π2=−sin⁡N+12⁢x2⁢π⁢−sin⁡x2
124 116 sincld ⊢x∈ℝ→sin⁡x2∈ℂ
125 108 124 mulneg2d ⊢x∈ℝ→2⁢π⁢−sin⁡x2=−2⁢π⁢sin⁡x2
126 125 oveq2d ⊢x∈ℝ→−sin⁡N+12⁢x2⁢π⁢−sin⁡x2=−sin⁡N+12⁢x−2⁢π⁢sin⁡x2
127 126 ad2antlr ⊢N∈ℕ∧x∈ℝ∧¬xmod2⁢π=0→−sin⁡N+12⁢x2⁢π⁢−sin⁡x2=−sin⁡N+12⁢x−2⁢π⁢sin⁡x2
128 72 123 127 3eqtrrd ⊢N∈ℕ∧x∈ℝ∧¬xmod2⁢π=0→−sin⁡N+12⁢x−2⁢π⁢sin⁡x2=ifx+Tmod2⁢π=02⋅ N+12⁢πsin⁡N+12⁢x+T2⁢π⁢sin⁡x+T2
129 34 53 128 3eqtr2rd ⊢N∈ℕ∧x∈ℝ∧¬xmod2⁢π=0→ifx+Tmod2⁢π=02⋅ N+12⁢πsin⁡N+12⁢x+T2⁢π⁢sin⁡x+T2=ifxmod2⁢π=02⋅ N+12⁢πsin⁡N+12⁢x2⁢π⁢sin⁡x2
130 32 129 pm2.61dan ⊢N∈ℕ∧x∈ℝ→ifx+Tmod2⁢π=02⋅ N+12⁢πsin⁡N+12⁢x+T2⁢π⁢sin⁡x+T2=ifxmod2⁢π=02⋅ N+12⁢πsin⁡N+12⁢x2⁢π⁢sin⁡x2
131 8 a1i ⊢x∈ℝ→T∈ℝ
132 16 131 readdcld ⊢x∈ℝ→x+T∈ℝ
133 1 dirkerval2 ⊢N∈ℕ∧x+T∈ℝ→D⁡N⁡x+T=ifx+Tmod2⁢π=02⋅ N+12⁢πsin⁡N+12⁢x+T2⁢π⁢sin⁡x+T2
134 132 133 sylan2 ⊢N∈ℕ∧x∈ℝ→D⁡N⁡x+T=ifx+Tmod2⁢π=02⋅ N+12⁢πsin⁡N+12⁢x+T2⁢π⁢sin⁡x+T2
135 1 dirkerval2 ⊢N∈ℕ∧x∈ℝ→D⁡N⁡x=ifxmod2⁢π=02⋅ N+12⁢πsin⁡N+12⁢x2⁢π⁢sin⁡x2
136 130 134 135 3eqtr4d ⊢N∈ℕ∧x∈ℝ→D⁡N⁡x+T=D⁡N⁡x