Description: The Dirichlet Kernel at any point evaluates to a real. (Contributed by Glauco Siliprandi, 11-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Hypothesis | dirkerre.1 | |
|
Assertion | dirkerre | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dirkerre.1 | |
|
2 | 1 | dirkerval2 | |
3 | 2re | |
|
4 | 3 | a1i | |
5 | nnre | |
|
6 | 4 5 | remulcld | |
7 | 1red | |
|
8 | 6 7 | readdcld | |
9 | pire | |
|
10 | 9 | a1i | |
11 | 4 10 | remulcld | |
12 | 2cnd | |
|
13 | 10 | recnd | |
14 | 2ne0 | |
|
15 | 14 | a1i | |
16 | 0re | |
|
17 | pipos | |
|
18 | 16 17 | gtneii | |
19 | 18 | a1i | |
20 | 12 13 15 19 | mulne0d | |
21 | 8 11 20 | redivcld | |
22 | 21 | ad2antrr | |
23 | dirker2re | |
|
24 | 22 23 | ifclda | |
25 | 2 24 | eqeltrd | |