This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. NN |-> ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
dirkerper.2 
|- T = ( 2 x. _pi )
Assertion dirkerper 
|- ( ( N e. NN /\ x e. RR ) -> ( ( D ` N ) ` ( x + T ) ) = ( ( D ` N ) ` x ) )

Proof

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