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