Metamath Proof Explorer

Theorem dirkertrigeq

Description: Trigonometric equality for the Dirichlet kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dirkertrigeq.d 
|- D = ( n e. NN |-> ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )
dirkertrigeq.n 
|- ( ph -> N e. NN )
dirkertrigeq.f 
|- F = ( D ` N )
dirkertrigeq.h 
|- H = ( s e. RR |-> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) )
Assertion dirkertrigeq 
|- ( ph -> F = H )

Proof

Step Hyp Ref Expression
1 dirkertrigeq.d 
 |-  D = ( n e. NN |-> ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )
2 dirkertrigeq.n 
 |-  ( ph -> N e. NN )
3 dirkertrigeq.f 
 |-  F = ( D ` N )
4 dirkertrigeq.h 
 |-  H = ( s e. RR |-> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) )
5 3 a1i 
 |-  ( ph -> F = ( D ` N ) )
6 1 dirkerval 
 |-  ( N e. NN -> ( D ` N ) = ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )
7 2 6 syl 
 |-  ( ph -> ( D ` N ) = ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )
8 2cnd 
 |-  ( ph -> 2 e. CC )
9 2 nncnd 
 |-  ( ph -> N e. CC )
10 8 9 mulcld 
 |-  ( ph -> ( 2 x. N ) e. CC )
11 peano2cn 
 |-  ( ( 2 x. N ) e. CC -> ( ( 2 x. N ) + 1 ) e. CC )
12 10 11 syl 
 |-  ( ph -> ( ( 2 x. N ) + 1 ) e. CC )
13 picn 
 |-  _pi e. CC
14 13 a1i 
 |-  ( ph -> _pi e. CC )
15 2ne0 
 |-  2 =/= 0
16 15 a1i 
 |-  ( ph -> 2 =/= 0 )
17 pire 
 |-  _pi e. RR
18 pipos 
 |-  0 < _pi
19 17 18 gt0ne0ii 
 |-  _pi =/= 0
20 19 a1i 
 |-  ( ph -> _pi =/= 0 )
21 12 8 14 16 20 divdiv1d 
 |-  ( ph -> ( ( ( ( 2 x. N ) + 1 ) / 2 ) / _pi ) = ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) )
22 21 eqcomd 
 |-  ( ph -> ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) = ( ( ( ( 2 x. N ) + 1 ) / 2 ) / _pi ) )
23 22 ad2antrr 
 |-  ( ( ( ph /\ s e. RR ) /\ ( s mod ( 2 x. _pi ) ) = 0 ) -> ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) = ( ( ( ( 2 x. N ) + 1 ) / 2 ) / _pi ) )
24 iftrue 
 |-  ( ( s mod ( 2 x. _pi ) ) = 0 -> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) = ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) )
25 24 adantl 
 |-  ( ( ( ph /\ s e. RR ) /\ ( s mod ( 2 x. _pi ) ) = 0 ) -> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) = ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) )
26 elfzelz 
 |-  ( k e. ( 1 ... N ) -> k e. ZZ )
27 26 zcnd 
 |-  ( k e. ( 1 ... N ) -> k e. CC )
28 27 adantl 
 |-  ( ( ( s e. RR /\ ( s mod ( 2 x. _pi ) ) = 0 ) /\ k e. ( 1 ... N ) ) -> k e. CC )
29 recn 
 |-  ( s e. RR -> s e. CC )
30 29 ad2antrr 
 |-  ( ( ( s e. RR /\ ( s mod ( 2 x. _pi ) ) = 0 ) /\ k e. ( 1 ... N ) ) -> s e. CC )
31 2cn 
 |-  2 e. CC
32 31 13 mulcli 
 |-  ( 2 x. _pi ) e. CC
33 32 a1i 
 |-  ( ( ( s e. RR /\ ( s mod ( 2 x. _pi ) ) = 0 ) /\ k e. ( 1 ... N ) ) -> ( 2 x. _pi ) e. CC )
34 31 13 15 19 mulne0i 
 |-  ( 2 x. _pi ) =/= 0
35 34 a1i 
 |-  ( ( ( s e. RR /\ ( s mod ( 2 x. _pi ) ) = 0 ) /\ k e. ( 1 ... N ) ) -> ( 2 x. _pi ) =/= 0 )
36 28 30 33 35 divassd 
 |-  ( ( ( s e. RR /\ ( s mod ( 2 x. _pi ) ) = 0 ) /\ k e. ( 1 ... N ) ) -> ( ( k x. s ) / ( 2 x. _pi ) ) = ( k x. ( s / ( 2 x. _pi ) ) ) )
37 26 adantl 
 |-  ( ( ( s e. RR /\ ( s mod ( 2 x. _pi ) ) = 0 ) /\ k e. ( 1 ... N ) ) -> k e. ZZ )
38 simpr 
 |-  ( ( s e. RR /\ ( s mod ( 2 x. _pi ) ) = 0 ) -> ( s mod ( 2 x. _pi ) ) = 0 )
39 simpl 
 |-  ( ( s e. RR /\ ( s mod ( 2 x. _pi ) ) = 0 ) -> s e. RR )
40 2rp 
 |-  2 e. RR+
41 pirp 
 |-  _pi e. RR+
42 rpmulcl 
 |-  ( ( 2 e. RR+ /\ _pi e. RR+ ) -> ( 2 x. _pi ) e. RR+ )
43 40 41 42 mp2an 
 |-  ( 2 x. _pi ) e. RR+
44 mod0 
 |-  ( ( s e. RR /\ ( 2 x. _pi ) e. RR+ ) -> ( ( s mod ( 2 x. _pi ) ) = 0 <-> ( s / ( 2 x. _pi ) ) e. ZZ ) )
45 39 43 44 sylancl 
 |-  ( ( s e. RR /\ ( s mod ( 2 x. _pi ) ) = 0 ) -> ( ( s mod ( 2 x. _pi ) ) = 0 <-> ( s / ( 2 x. _pi ) ) e. ZZ ) )
46 38 45 mpbid 
 |-  ( ( s e. RR /\ ( s mod ( 2 x. _pi ) ) = 0 ) -> ( s / ( 2 x. _pi ) ) e. ZZ )
47 46 adantr 
 |-  ( ( ( s e. RR /\ ( s mod ( 2 x. _pi ) ) = 0 ) /\ k e. ( 1 ... N ) ) -> ( s / ( 2 x. _pi ) ) e. ZZ )
48 37 47 zmulcld 
 |-  ( ( ( s e. RR /\ ( s mod ( 2 x. _pi ) ) = 0 ) /\ k e. ( 1 ... N ) ) -> ( k x. ( s / ( 2 x. _pi ) ) ) e. ZZ )
49 36 48 eqeltrd 
 |-  ( ( ( s e. RR /\ ( s mod ( 2 x. _pi ) ) = 0 ) /\ k e. ( 1 ... N ) ) -> ( ( k x. s ) / ( 2 x. _pi ) ) e. ZZ )
50 27 adantl 
 |-  ( ( s e. RR /\ k e. ( 1 ... N ) ) -> k e. CC )
51 29 adantr 
 |-  ( ( s e. RR /\ k e. ( 1 ... N ) ) -> s e. CC )
52 50 51 mulcld 
 |-  ( ( s e. RR /\ k e. ( 1 ... N ) ) -> ( k x. s ) e. CC )
53 coseq1 
 |-  ( ( k x. s ) e. CC -> ( ( cos ` ( k x. s ) ) = 1 <-> ( ( k x. s ) / ( 2 x. _pi ) ) e. ZZ ) )
54 52 53 syl 
 |-  ( ( s e. RR /\ k e. ( 1 ... N ) ) -> ( ( cos ` ( k x. s ) ) = 1 <-> ( ( k x. s ) / ( 2 x. _pi ) ) e. ZZ ) )
55 54 adantlr 
 |-  ( ( ( s e. RR /\ ( s mod ( 2 x. _pi ) ) = 0 ) /\ k e. ( 1 ... N ) ) -> ( ( cos ` ( k x. s ) ) = 1 <-> ( ( k x. s ) / ( 2 x. _pi ) ) e. ZZ ) )
56 49 55 mpbird 
 |-  ( ( ( s e. RR /\ ( s mod ( 2 x. _pi ) ) = 0 ) /\ k e. ( 1 ... N ) ) -> ( cos ` ( k x. s ) ) = 1 )
57 56 ralrimiva 
 |-  ( ( s e. RR /\ ( s mod ( 2 x. _pi ) ) = 0 ) -> A. k e. ( 1 ... N ) ( cos ` ( k x. s ) ) = 1 )
58 57 adantll 
 |-  ( ( ( ph /\ s e. RR ) /\ ( s mod ( 2 x. _pi ) ) = 0 ) -> A. k e. ( 1 ... N ) ( cos ` ( k x. s ) ) = 1 )
59 58 sumeq2d 
 |-  ( ( ( ph /\ s e. RR ) /\ ( s mod ( 2 x. _pi ) ) = 0 ) -> sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) = sum_ k e. ( 1 ... N ) 1 )
60 fzfid 
 |-  ( ( ( ph /\ s e. RR ) /\ ( s mod ( 2 x. _pi ) ) = 0 ) -> ( 1 ... N ) e. Fin )
61 1cnd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( s mod ( 2 x. _pi ) ) = 0 ) -> 1 e. CC )
62 fsumconst 
 |-  ( ( ( 1 ... N ) e. Fin /\ 1 e. CC ) -> sum_ k e. ( 1 ... N ) 1 = ( ( # ` ( 1 ... N ) ) x. 1 ) )
63 60 61 62 syl2anc 
 |-  ( ( ( ph /\ s e. RR ) /\ ( s mod ( 2 x. _pi ) ) = 0 ) -> sum_ k e. ( 1 ... N ) 1 = ( ( # ` ( 1 ... N ) ) x. 1 ) )
64 2 nnnn0d 
 |-  ( ph -> N e. NN0 )
65 hashfz1 
 |-  ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
66 64 65 syl 
 |-  ( ph -> ( # ` ( 1 ... N ) ) = N )
67 66 oveq1d 
 |-  ( ph -> ( ( # ` ( 1 ... N ) ) x. 1 ) = ( N x. 1 ) )
68 9 mulid1d 
 |-  ( ph -> ( N x. 1 ) = N )
69 67 68 eqtrd 
 |-  ( ph -> ( ( # ` ( 1 ... N ) ) x. 1 ) = N )
70 69 ad2antrr 
 |-  ( ( ( ph /\ s e. RR ) /\ ( s mod ( 2 x. _pi ) ) = 0 ) -> ( ( # ` ( 1 ... N ) ) x. 1 ) = N )
71 59 63 70 3eqtrd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( s mod ( 2 x. _pi ) ) = 0 ) -> sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) = N )
72 71 oveq2d 
 |-  ( ( ( ph /\ s e. RR ) /\ ( s mod ( 2 x. _pi ) ) = 0 ) -> ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) = ( ( 1 / 2 ) + N ) )
73 9 div1d 
 |-  ( ph -> ( N / 1 ) = N )
74 73 eqcomd 
 |-  ( ph -> N = ( N / 1 ) )
75 74 oveq2d 
 |-  ( ph -> ( ( 1 / 2 ) + N ) = ( ( 1 / 2 ) + ( N / 1 ) ) )
76 1cnd 
 |-  ( ph -> 1 e. CC )
77 ax-1ne0 
 |-  1 =/= 0
78 77 a1i 
 |-  ( ph -> 1 =/= 0 )
79 76 8 9 76 16 78 divadddivd 
 |-  ( ph -> ( ( 1 / 2 ) + ( N / 1 ) ) = ( ( ( 1 x. 1 ) + ( N x. 2 ) ) / ( 2 x. 1 ) ) )
80 76 76 mulcld 
 |-  ( ph -> ( 1 x. 1 ) e. CC )
81 9 8 mulcld 
 |-  ( ph -> ( N x. 2 ) e. CC )
82 80 81 addcomd 
 |-  ( ph -> ( ( 1 x. 1 ) + ( N x. 2 ) ) = ( ( N x. 2 ) + ( 1 x. 1 ) ) )
83 9 8 mulcomd 
 |-  ( ph -> ( N x. 2 ) = ( 2 x. N ) )
84 76 mulid1d 
 |-  ( ph -> ( 1 x. 1 ) = 1 )
85 83 84 oveq12d 
 |-  ( ph -> ( ( N x. 2 ) + ( 1 x. 1 ) ) = ( ( 2 x. N ) + 1 ) )
86 82 85 eqtrd 
 |-  ( ph -> ( ( 1 x. 1 ) + ( N x. 2 ) ) = ( ( 2 x. N ) + 1 ) )
87 8 mulid1d 
 |-  ( ph -> ( 2 x. 1 ) = 2 )
88 86 87 oveq12d 
 |-  ( ph -> ( ( ( 1 x. 1 ) + ( N x. 2 ) ) / ( 2 x. 1 ) ) = ( ( ( 2 x. N ) + 1 ) / 2 ) )
89 75 79 88 3eqtrd 
 |-  ( ph -> ( ( 1 / 2 ) + N ) = ( ( ( 2 x. N ) + 1 ) / 2 ) )
90 89 ad2antrr 
 |-  ( ( ( ph /\ s e. RR ) /\ ( s mod ( 2 x. _pi ) ) = 0 ) -> ( ( 1 / 2 ) + N ) = ( ( ( 2 x. N ) + 1 ) / 2 ) )
91 72 90 eqtrd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( s mod ( 2 x. _pi ) ) = 0 ) -> ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) = ( ( ( 2 x. N ) + 1 ) / 2 ) )
92 91 oveq1d 
 |-  ( ( ( ph /\ s e. RR ) /\ ( s mod ( 2 x. _pi ) ) = 0 ) -> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) = ( ( ( ( 2 x. N ) + 1 ) / 2 ) / _pi ) )
93 23 25 92 3eqtr4rd 
 |-  ( ( ( ph /\ s e. RR ) /\ ( s mod ( 2 x. _pi ) ) = 0 ) -> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) = if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) )
94 iffalse 
 |-  ( -. ( s mod ( 2 x. _pi ) ) = 0 -> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) )
95 94 adantl 
 |-  ( ( ( ph /\ s e. RR ) /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) -> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) )
96 13 a1i 
 |-  ( s e. RR -> _pi e. CC )
97 19 a1i 
 |-  ( s e. RR -> _pi =/= 0 )
98 29 96 97 divcan1d 
 |-  ( s e. RR -> ( ( s / _pi ) x. _pi ) = s )
99 98 eqcomd 
 |-  ( s e. RR -> s = ( ( s / _pi ) x. _pi ) )
100 99 ad2antrr 
 |-  ( ( ( s e. RR /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) /\ ( s mod _pi ) = 0 ) -> s = ( ( s / _pi ) x. _pi ) )
101 simpr 
 |-  ( ( s e. RR /\ ( s mod _pi ) = 0 ) -> ( s mod _pi ) = 0 )
102 simpl 
 |-  ( ( s e. RR /\ ( s mod _pi ) = 0 ) -> s e. RR )
103 mod0 
 |-  ( ( s e. RR /\ _pi e. RR+ ) -> ( ( s mod _pi ) = 0 <-> ( s / _pi ) e. ZZ ) )
104 102 41 103 sylancl 
 |-  ( ( s e. RR /\ ( s mod _pi ) = 0 ) -> ( ( s mod _pi ) = 0 <-> ( s / _pi ) e. ZZ ) )
105 101 104 mpbid 
 |-  ( ( s e. RR /\ ( s mod _pi ) = 0 ) -> ( s / _pi ) e. ZZ )
106 105 adantlr 
 |-  ( ( ( s e. RR /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) /\ ( s mod _pi ) = 0 ) -> ( s / _pi ) e. ZZ )
107 rpreccl 
 |-  ( _pi e. RR+ -> ( 1 / _pi ) e. RR+ )
108 41 107 ax-mp 
 |-  ( 1 / _pi ) e. RR+
109 moddi 
 |-  ( ( ( 1 / _pi ) e. RR+ /\ s e. RR /\ ( 2 x. _pi ) e. RR+ ) -> ( ( 1 / _pi ) x. ( s mod ( 2 x. _pi ) ) ) = ( ( ( 1 / _pi ) x. s ) mod ( ( 1 / _pi ) x. ( 2 x. _pi ) ) ) )
110 108 43 109 mp3an13 
 |-  ( s e. RR -> ( ( 1 / _pi ) x. ( s mod ( 2 x. _pi ) ) ) = ( ( ( 1 / _pi ) x. s ) mod ( ( 1 / _pi ) x. ( 2 x. _pi ) ) ) )
111 29 96 97 divrec2d 
 |-  ( s e. RR -> ( s / _pi ) = ( ( 1 / _pi ) x. s ) )
112 111 eqcomd 
 |-  ( s e. RR -> ( ( 1 / _pi ) x. s ) = ( s / _pi ) )
113 96 97 reccld 
 |-  ( s e. RR -> ( 1 / _pi ) e. CC )
114 32 a1i 
 |-  ( s e. RR -> ( 2 x. _pi ) e. CC )
115 113 114 mulcomd 
 |-  ( s e. RR -> ( ( 1 / _pi ) x. ( 2 x. _pi ) ) = ( ( 2 x. _pi ) x. ( 1 / _pi ) ) )
116 2cnd 
 |-  ( s e. RR -> 2 e. CC )
117 116 96 113 mulassd 
 |-  ( s e. RR -> ( ( 2 x. _pi ) x. ( 1 / _pi ) ) = ( 2 x. ( _pi x. ( 1 / _pi ) ) ) )
118 13 19 recidi 
 |-  ( _pi x. ( 1 / _pi ) ) = 1
119 118 oveq2i 
 |-  ( 2 x. ( _pi x. ( 1 / _pi ) ) ) = ( 2 x. 1 )
120 116 mulid1d 
 |-  ( s e. RR -> ( 2 x. 1 ) = 2 )
121 119 120 eqtrid 
 |-  ( s e. RR -> ( 2 x. ( _pi x. ( 1 / _pi ) ) ) = 2 )
122 115 117 121 3eqtrd 
 |-  ( s e. RR -> ( ( 1 / _pi ) x. ( 2 x. _pi ) ) = 2 )
123 112 122 oveq12d 
 |-  ( s e. RR -> ( ( ( 1 / _pi ) x. s ) mod ( ( 1 / _pi ) x. ( 2 x. _pi ) ) ) = ( ( s / _pi ) mod 2 ) )
124 110 123 eqtr2d 
 |-  ( s e. RR -> ( ( s / _pi ) mod 2 ) = ( ( 1 / _pi ) x. ( s mod ( 2 x. _pi ) ) ) )
125 124 adantr 
 |-  ( ( s e. RR /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) -> ( ( s / _pi ) mod 2 ) = ( ( 1 / _pi ) x. ( s mod ( 2 x. _pi ) ) ) )
126 113 adantr 
 |-  ( ( s e. RR /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) -> ( 1 / _pi ) e. CC )
127 id 
 |-  ( s e. RR -> s e. RR )
128 43 a1i 
 |-  ( s e. RR -> ( 2 x. _pi ) e. RR+ )
129 127 128 modcld 
 |-  ( s e. RR -> ( s mod ( 2 x. _pi ) ) e. RR )
130 129 recnd 
 |-  ( s e. RR -> ( s mod ( 2 x. _pi ) ) e. CC )
131 130 adantr 
 |-  ( ( s e. RR /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) -> ( s mod ( 2 x. _pi ) ) e. CC )
132 ax-1cn 
 |-  1 e. CC
133 132 13 77 19 divne0i 
 |-  ( 1 / _pi ) =/= 0
134 133 a1i 
 |-  ( ( s e. RR /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) -> ( 1 / _pi ) =/= 0 )
135 neqne 
 |-  ( -. ( s mod ( 2 x. _pi ) ) = 0 -> ( s mod ( 2 x. _pi ) ) =/= 0 )
136 135 adantl 
 |-  ( ( s e. RR /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) -> ( s mod ( 2 x. _pi ) ) =/= 0 )
137 126 131 134 136 mulne0d 
 |-  ( ( s e. RR /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) -> ( ( 1 / _pi ) x. ( s mod ( 2 x. _pi ) ) ) =/= 0 )
138 125 137 eqnetrd 
 |-  ( ( s e. RR /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) -> ( ( s / _pi ) mod 2 ) =/= 0 )
139 138 adantr 
 |-  ( ( ( s e. RR /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) /\ ( s mod _pi ) = 0 ) -> ( ( s / _pi ) mod 2 ) =/= 0 )
140 oddfl 
 |-  ( ( ( s / _pi ) e. ZZ /\ ( ( s / _pi ) mod 2 ) =/= 0 ) -> ( s / _pi ) = ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) )
141 106 139 140 syl2anc 
 |-  ( ( ( s e. RR /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) /\ ( s mod _pi ) = 0 ) -> ( s / _pi ) = ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) )
142 141 oveq1d 
 |-  ( ( ( s e. RR /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) /\ ( s mod _pi ) = 0 ) -> ( ( s / _pi ) x. _pi ) = ( ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) x. _pi ) )
143 100 142 eqtrd 
 |-  ( ( ( s e. RR /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) /\ ( s mod _pi ) = 0 ) -> s = ( ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) x. _pi ) )
144 143 oveq2d 
 |-  ( ( ( s e. RR /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) /\ ( s mod _pi ) = 0 ) -> ( k x. s ) = ( k x. ( ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) x. _pi ) ) )
145 144 fveq2d 
 |-  ( ( ( s e. RR /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) /\ ( s mod _pi ) = 0 ) -> ( cos ` ( k x. s ) ) = ( cos ` ( k x. ( ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) x. _pi ) ) ) )
146 145 sumeq2sdv 
 |-  ( ( ( s e. RR /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) /\ ( s mod _pi ) = 0 ) -> sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) = sum_ k e. ( 1 ... N ) ( cos ` ( k x. ( ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) x. _pi ) ) ) )
147 146 oveq2d 
 |-  ( ( ( s e. RR /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) /\ ( s mod _pi ) = 0 ) -> ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) = ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. ( ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) x. _pi ) ) ) ) )
148 147 oveq1d 
 |-  ( ( ( s e. RR /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) /\ ( s mod _pi ) = 0 ) -> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) = ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. ( ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) x. _pi ) ) ) ) / _pi ) )
149 148 adantlll 
 |-  ( ( ( ( ph /\ s e. RR ) /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) /\ ( s mod _pi ) = 0 ) -> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) = ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. ( ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) x. _pi ) ) ) ) / _pi ) )
150 2 ad2antrr 
 |-  ( ( ( ph /\ s e. RR ) /\ ( s mod _pi ) = 0 ) -> N e. NN )
151 17 a1i 
 |-  ( s e. RR -> _pi e. RR )
152 127 151 97 redivcld 
 |-  ( s e. RR -> ( s / _pi ) e. RR )
153 152 rehalfcld 
 |-  ( s e. RR -> ( ( s / _pi ) / 2 ) e. RR )
154 153 flcld 
 |-  ( s e. RR -> ( |_ ` ( ( s / _pi ) / 2 ) ) e. ZZ )
155 154 ad2antlr 
 |-  ( ( ( ph /\ s e. RR ) /\ ( s mod _pi ) = 0 ) -> ( |_ ` ( ( s / _pi ) / 2 ) ) e. ZZ )
156 eqid 
 |-  ( ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) x. _pi ) = ( ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) x. _pi )
157 150 155 156 dirkertrigeqlem3 
 |-  ( ( ( ph /\ s e. RR ) /\ ( s mod _pi ) = 0 ) -> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. ( ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) x. _pi ) ) ) ) / _pi ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) x. _pi ) ) ) / ( ( 2 x. _pi ) x. ( sin ` ( ( ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) x. _pi ) / 2 ) ) ) ) )
158 157 adantlr 
 |-  ( ( ( ( ph /\ s e. RR ) /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) /\ ( s mod _pi ) = 0 ) -> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. ( ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) x. _pi ) ) ) ) / _pi ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) x. _pi ) ) ) / ( ( 2 x. _pi ) x. ( sin ` ( ( ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) x. _pi ) / 2 ) ) ) ) )
159 141 adantlll 
 |-  ( ( ( ( ph /\ s e. RR ) /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) /\ ( s mod _pi ) = 0 ) -> ( s / _pi ) = ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) )
160 159 eqcomd 
 |-  ( ( ( ( ph /\ s e. RR ) /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) /\ ( s mod _pi ) = 0 ) -> ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) = ( s / _pi ) )
161 160 oveq1d 
 |-  ( ( ( ( ph /\ s e. RR ) /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) /\ ( s mod _pi ) = 0 ) -> ( ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) x. _pi ) = ( ( s / _pi ) x. _pi ) )
162 161 oveq2d 
 |-  ( ( ( ( ph /\ s e. RR ) /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) /\ ( s mod _pi ) = 0 ) -> ( ( N + ( 1 / 2 ) ) x. ( ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) x. _pi ) ) = ( ( N + ( 1 / 2 ) ) x. ( ( s / _pi ) x. _pi ) ) )
163 162 fveq2d 
 |-  ( ( ( ( ph /\ s e. RR ) /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) /\ ( s mod _pi ) = 0 ) -> ( sin ` ( ( N + ( 1 / 2 ) ) x. ( ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) x. _pi ) ) ) = ( sin ` ( ( N + ( 1 / 2 ) ) x. ( ( s / _pi ) x. _pi ) ) ) )
164 161 fvoveq1d 
 |-  ( ( ( ( ph /\ s e. RR ) /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) /\ ( s mod _pi ) = 0 ) -> ( sin ` ( ( ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) x. _pi ) / 2 ) ) = ( sin ` ( ( ( s / _pi ) x. _pi ) / 2 ) ) )
165 164 oveq2d 
 |-  ( ( ( ( ph /\ s e. RR ) /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) /\ ( s mod _pi ) = 0 ) -> ( ( 2 x. _pi ) x. ( sin ` ( ( ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) x. _pi ) / 2 ) ) ) = ( ( 2 x. _pi ) x. ( sin ` ( ( ( s / _pi ) x. _pi ) / 2 ) ) ) )
166 163 165 oveq12d 
 |-  ( ( ( ( ph /\ s e. RR ) /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) /\ ( s mod _pi ) = 0 ) -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) x. _pi ) ) ) / ( ( 2 x. _pi ) x. ( sin ` ( ( ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) x. _pi ) / 2 ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( ( s / _pi ) x. _pi ) ) ) / ( ( 2 x. _pi ) x. ( sin ` ( ( ( s / _pi ) x. _pi ) / 2 ) ) ) ) )
167 98 oveq2d 
 |-  ( s e. RR -> ( ( N + ( 1 / 2 ) ) x. ( ( s / _pi ) x. _pi ) ) = ( ( N + ( 1 / 2 ) ) x. s ) )
168 167 fveq2d 
 |-  ( s e. RR -> ( sin ` ( ( N + ( 1 / 2 ) ) x. ( ( s / _pi ) x. _pi ) ) ) = ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) )
169 98 fvoveq1d 
 |-  ( s e. RR -> ( sin ` ( ( ( s / _pi ) x. _pi ) / 2 ) ) = ( sin ` ( s / 2 ) ) )
170 169 oveq2d 
 |-  ( s e. RR -> ( ( 2 x. _pi ) x. ( sin ` ( ( ( s / _pi ) x. _pi ) / 2 ) ) ) = ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) )
171 168 170 oveq12d 
 |-  ( s e. RR -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( ( s / _pi ) x. _pi ) ) ) / ( ( 2 x. _pi ) x. ( sin ` ( ( ( s / _pi ) x. _pi ) / 2 ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) )
172 171 adantl 
 |-  ( ( ph /\ s e. RR ) -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( ( s / _pi ) x. _pi ) ) ) / ( ( 2 x. _pi ) x. ( sin ` ( ( ( s / _pi ) x. _pi ) / 2 ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) )
173 172 ad2antrr 
 |-  ( ( ( ( ph /\ s e. RR ) /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) /\ ( s mod _pi ) = 0 ) -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( ( s / _pi ) x. _pi ) ) ) / ( ( 2 x. _pi ) x. ( sin ` ( ( ( s / _pi ) x. _pi ) / 2 ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) )
174 166 173 eqtrd 
 |-  ( ( ( ( ph /\ s e. RR ) /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) /\ ( s mod _pi ) = 0 ) -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. ( ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) x. _pi ) ) ) / ( ( 2 x. _pi ) x. ( sin ` ( ( ( ( 2 x. ( |_ ` ( ( s / _pi ) / 2 ) ) ) + 1 ) x. _pi ) / 2 ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) )
175 149 158 174 3eqtrrd 
 |-  ( ( ( ( ph /\ s e. RR ) /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) /\ ( s mod _pi ) = 0 ) -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) = ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) )
176 simplr 
 |-  ( ( ( ph /\ s e. RR ) /\ -. ( s mod _pi ) = 0 ) -> s e. RR )
177 simpr 
 |-  ( ( ( ph /\ s e. RR ) /\ -. ( s mod _pi ) = 0 ) -> -. ( s mod _pi ) = 0 )
178 176 41 103 sylancl 
 |-  ( ( ( ph /\ s e. RR ) /\ -. ( s mod _pi ) = 0 ) -> ( ( s mod _pi ) = 0 <-> ( s / _pi ) e. ZZ ) )
179 177 178 mtbid 
 |-  ( ( ( ph /\ s e. RR ) /\ -. ( s mod _pi ) = 0 ) -> -. ( s / _pi ) e. ZZ )
180 176 recnd 
 |-  ( ( ( ph /\ s e. RR ) /\ -. ( s mod _pi ) = 0 ) -> s e. CC )
181 sineq0 
 |-  ( s e. CC -> ( ( sin ` s ) = 0 <-> ( s / _pi ) e. ZZ ) )
182 180 181 syl 
 |-  ( ( ( ph /\ s e. RR ) /\ -. ( s mod _pi ) = 0 ) -> ( ( sin ` s ) = 0 <-> ( s / _pi ) e. ZZ ) )
183 179 182 mtbird 
 |-  ( ( ( ph /\ s e. RR ) /\ -. ( s mod _pi ) = 0 ) -> -. ( sin ` s ) = 0 )
184 183 neqned 
 |-  ( ( ( ph /\ s e. RR ) /\ -. ( s mod _pi ) = 0 ) -> ( sin ` s ) =/= 0 )
185 2 ad2antrr 
 |-  ( ( ( ph /\ s e. RR ) /\ -. ( s mod _pi ) = 0 ) -> N e. NN )
186 176 184 185 dirkertrigeqlem2 
 |-  ( ( ( ph /\ s e. RR ) /\ -. ( s mod _pi ) = 0 ) -> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) )
187 186 eqcomd 
 |-  ( ( ( ph /\ s e. RR ) /\ -. ( s mod _pi ) = 0 ) -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) = ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) )
188 187 adantlr 
 |-  ( ( ( ( ph /\ s e. RR ) /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) /\ -. ( s mod _pi ) = 0 ) -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) = ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) )
189 175 188 pm2.61dan 
 |-  ( ( ( ph /\ s e. RR ) /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) = ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) )
190 95 189 eqtr2d 
 |-  ( ( ( ph /\ s e. RR ) /\ -. ( s mod ( 2 x. _pi ) ) = 0 ) -> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) = if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) )
191 93 190 pm2.61dan 
 |-  ( ( ph /\ s e. RR ) -> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) = if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) )
192 191 mpteq2dva 
 |-  ( ph -> ( s e. RR |-> ( ( ( 1 / 2 ) + sum_ k e. ( 1 ... N ) ( cos ` ( k x. s ) ) ) / _pi ) ) = ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )
193 4 192 eqtr2id 
 |-  ( ph -> ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) = H )
194 5 7 193 3eqtrd 
 |-  ( ph -> F = H )