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 syl5eq
 |-  ( 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 )