Metamath Proof Explorer


Theorem dirkerre

Description: The Dirichlet Kernel at any point evaluates to a real. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypothesis dirkerre.1 D=nsifsmod2π=02n+12πsinn+12s2πsins2
Assertion dirkerre NSDNS

Proof

Step Hyp Ref Expression
1 dirkerre.1 D=nsifsmod2π=02n+12πsinn+12s2πsins2
2 1 dirkerval2 NSDNS=ifSmod2π=02 N+12πsinN+12S2πsinS2
3 2re 2
4 3 a1i N2
5 nnre NN
6 4 5 remulcld N2 N
7 1red N1
8 6 7 readdcld N2 N+1
9 pire π
10 9 a1i Nπ
11 4 10 remulcld N2π
12 2cnd N2
13 10 recnd Nπ
14 2ne0 20
15 14 a1i N20
16 0re 0
17 pipos 0<π
18 16 17 gtneii π0
19 18 a1i Nπ0
20 12 13 15 19 mulne0d N2π0
21 8 11 20 redivcld N2 N+12π
22 21 ad2antrr NSSmod2π=02 N+12π
23 dirker2re NS¬Smod2π=0sinN+12S2πsinS2
24 22 23 ifclda NSifSmod2π=02 N+12πsinN+12S2πsinS2
25 2 24 eqeltrd NSDNS