Metamath Proof Explorer

Theorem dirkertrigeqlem3

Description: Trigonometric equality lemma for the Dirichlet kernel trigonometric equality. Here we handle the case for an angle that's an odd multiple of _pi . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dirkertrigeqlem3.n 
|- ( ph -> N e. NN )
dirkertrigeqlem3.k 
|- ( ph -> K e. ZZ )
dirkertrigeqlem3.a 
|- A = ( ( ( 2 x. K ) + 1 ) x. _pi )
Assertion dirkertrigeqlem3 
|- ( ph -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) / _pi ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( ( 2 x. _pi ) x. ( sin ` ( A / 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dirkertrigeqlem3.n 
 |-  ( ph -> N e. NN )
2 dirkertrigeqlem3.k 
 |-  ( ph -> K e. ZZ )
3 dirkertrigeqlem3.a 
 |-  A = ( ( ( 2 x. K ) + 1 ) x. _pi )
4 3 a1i 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> A = ( ( ( 2 x. K ) + 1 ) x. _pi ) )
5 4 oveq2d 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( n x. A ) = ( n x. ( ( ( 2 x. K ) + 1 ) x. _pi ) ) )
6 elfzelz 
 |-  ( n e. ( 1 ... N ) -> n e. ZZ )
7 6 zcnd 
 |-  ( n e. ( 1 ... N ) -> n e. CC )
8 7 adantl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> n e. CC )
9 2cnd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> 2 e. CC )
10 2 zcnd 
 |-  ( ph -> K e. CC )
11 10 adantr 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> K e. CC )
12 9 11 mulcld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( 2 x. K ) e. CC )
13 1cnd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> 1 e. CC )
14 12 13 addcld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 2 x. K ) + 1 ) e. CC )
15 picn 
 |-  _pi e. CC
16 15 a1i 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> _pi e. CC )
17 14 16 mulcld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( 2 x. K ) + 1 ) x. _pi ) e. CC )
18 8 17 mulcomd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( n x. ( ( ( 2 x. K ) + 1 ) x. _pi ) ) = ( ( ( ( 2 x. K ) + 1 ) x. _pi ) x. n ) )
19 14 16 8 mulassd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( ( 2 x. K ) + 1 ) x. _pi ) x. n ) = ( ( ( 2 x. K ) + 1 ) x. ( _pi x. n ) ) )
20 16 8 mulcld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( _pi x. n ) e. CC )
21 12 13 20 adddird 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( 2 x. K ) + 1 ) x. ( _pi x. n ) ) = ( ( ( 2 x. K ) x. ( _pi x. n ) ) + ( 1 x. ( _pi x. n ) ) ) )
22 12 20 mulcld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 2 x. K ) x. ( _pi x. n ) ) e. CC )
23 13 20 mulcld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( 1 x. ( _pi x. n ) ) e. CC )
24 22 23 addcomd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( 2 x. K ) x. ( _pi x. n ) ) + ( 1 x. ( _pi x. n ) ) ) = ( ( 1 x. ( _pi x. n ) ) + ( ( 2 x. K ) x. ( _pi x. n ) ) ) )
25 15 a1i 
 |-  ( n e. ( 1 ... N ) -> _pi e. CC )
26 25 7 mulcld 
 |-  ( n e. ( 1 ... N ) -> ( _pi x. n ) e. CC )
27 26 mullidd 
 |-  ( n e. ( 1 ... N ) -> ( 1 x. ( _pi x. n ) ) = ( _pi x. n ) )
28 27 adantl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( 1 x. ( _pi x. n ) ) = ( _pi x. n ) )
29 9 11 16 8 mul4d 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 2 x. K ) x. ( _pi x. n ) ) = ( ( 2 x. _pi ) x. ( K x. n ) ) )
30 9 16 mulcld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( 2 x. _pi ) e. CC )
31 11 8 mulcld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( K x. n ) e. CC )
32 30 31 mulcomd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 2 x. _pi ) x. ( K x. n ) ) = ( ( K x. n ) x. ( 2 x. _pi ) ) )
33 29 32 eqtrd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 2 x. K ) x. ( _pi x. n ) ) = ( ( K x. n ) x. ( 2 x. _pi ) ) )
34 28 33 oveq12d 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 1 x. ( _pi x. n ) ) + ( ( 2 x. K ) x. ( _pi x. n ) ) ) = ( ( _pi x. n ) + ( ( K x. n ) x. ( 2 x. _pi ) ) ) )
35 24 34 eqtrd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( 2 x. K ) x. ( _pi x. n ) ) + ( 1 x. ( _pi x. n ) ) ) = ( ( _pi x. n ) + ( ( K x. n ) x. ( 2 x. _pi ) ) ) )
36 19 21 35 3eqtrd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( ( 2 x. K ) + 1 ) x. _pi ) x. n ) = ( ( _pi x. n ) + ( ( K x. n ) x. ( 2 x. _pi ) ) ) )
37 5 18 36 3eqtrd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( n x. A ) = ( ( _pi x. n ) + ( ( K x. n ) x. ( 2 x. _pi ) ) ) )
38 37 fveq2d 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( cos ` ( n x. A ) ) = ( cos ` ( ( _pi x. n ) + ( ( K x. n ) x. ( 2 x. _pi ) ) ) ) )
39 2 adantr 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> K e. ZZ )
40 6 adantl 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> n e. ZZ )
41 39 40 zmulcld 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( K x. n ) e. ZZ )
42 cosper 
 |-  ( ( ( _pi x. n ) e. CC /\ ( K x. n ) e. ZZ ) -> ( cos ` ( ( _pi x. n ) + ( ( K x. n ) x. ( 2 x. _pi ) ) ) ) = ( cos ` ( _pi x. n ) ) )
43 20 41 42 syl2anc 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( cos ` ( ( _pi x. n ) + ( ( K x. n ) x. ( 2 x. _pi ) ) ) ) = ( cos ` ( _pi x. n ) ) )
44 38 43 eqtrd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( cos ` ( n x. A ) ) = ( cos ` ( _pi x. n ) ) )
45 44 sumeq2dv 
 |-  ( ph -> sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) = sum_ n e. ( 1 ... N ) ( cos ` ( _pi x. n ) ) )
46 45 oveq2d 
 |-  ( ph -> ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) = ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( _pi x. n ) ) ) )
47 46 oveq1d 
 |-  ( ph -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) / _pi ) = ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( _pi x. n ) ) ) / _pi ) )
48 47 adantr 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) / _pi ) = ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( _pi x. n ) ) ) / _pi ) )
49 1 nncnd 
 |-  ( ph -> N e. CC )
50 2cnd 
 |-  ( ph -> 2 e. CC )
51 2ne0 
 |-  2 =/= 0
52 51 a1i 
 |-  ( ph -> 2 =/= 0 )
53 49 50 52 divcan2d 
 |-  ( ph -> ( 2 x. ( N / 2 ) ) = N )
54 53 eqcomd 
 |-  ( ph -> N = ( 2 x. ( N / 2 ) ) )
55 54 oveq2d 
 |-  ( ph -> ( 1 ... N ) = ( 1 ... ( 2 x. ( N / 2 ) ) ) )
56 55 sumeq1d 
 |-  ( ph -> sum_ n e. ( 1 ... N ) ( cos ` ( _pi x. n ) ) = sum_ n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) ( cos ` ( _pi x. n ) ) )
57 56 adantr 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> sum_ n e. ( 1 ... N ) ( cos ` ( _pi x. n ) ) = sum_ n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) ( cos ` ( _pi x. n ) ) )
58 15 a1i 
 |-  ( n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) -> _pi e. CC )
59 elfzelz 
 |-  ( n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) -> n e. ZZ )
60 59 zcnd 
 |-  ( n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) -> n e. CC )
61 58 60 mulcomd 
 |-  ( n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) -> ( _pi x. n ) = ( n x. _pi ) )
62 61 fveq2d 
 |-  ( n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) -> ( cos ` ( _pi x. n ) ) = ( cos ` ( n x. _pi ) ) )
63 62 rgen 
 |-  A. n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) ( cos ` ( _pi x. n ) ) = ( cos ` ( n x. _pi ) )
64 63 a1i 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> A. n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) ( cos ` ( _pi x. n ) ) = ( cos ` ( n x. _pi ) ) )
65 64 sumeq2d 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> sum_ n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) ( cos ` ( _pi x. n ) ) = sum_ n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) ( cos ` ( n x. _pi ) ) )
66 simpr 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( N mod 2 ) = 0 )
67 1 nnred 
 |-  ( ph -> N e. RR )
68 67 adantr 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> N e. RR )
69 2rp 
 |-  2 e. RR+
70 mod0 
 |-  ( ( N e. RR /\ 2 e. RR+ ) -> ( ( N mod 2 ) = 0 <-> ( N / 2 ) e. ZZ ) )
71 68 69 70 sylancl 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( N mod 2 ) = 0 <-> ( N / 2 ) e. ZZ ) )
72 66 71 mpbid 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( N / 2 ) e. ZZ )
73 2re 
 |-  2 e. RR
74 73 a1i 
 |-  ( ph -> 2 e. RR )
75 1 nngt0d 
 |-  ( ph -> 0 < N )
76 2pos 
 |-  0 < 2
77 76 a1i 
 |-  ( ph -> 0 < 2 )
78 67 74 75 77 divgt0d 
 |-  ( ph -> 0 < ( N / 2 ) )
79 78 adantr 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> 0 < ( N / 2 ) )
80 elnnz 
 |-  ( ( N / 2 ) e. NN <-> ( ( N / 2 ) e. ZZ /\ 0 < ( N / 2 ) ) )
81 72 79 80 sylanbrc 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( N / 2 ) e. NN )
82 dirkertrigeqlem1 
 |-  ( ( N / 2 ) e. NN -> sum_ n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) ( cos ` ( n x. _pi ) ) = 0 )
83 81 82 syl 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> sum_ n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) ( cos ` ( n x. _pi ) ) = 0 )
84 57 65 83 3eqtrd 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> sum_ n e. ( 1 ... N ) ( cos ` ( _pi x. n ) ) = 0 )
85 84 oveq2d 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( _pi x. n ) ) ) = ( ( 1 / 2 ) + 0 ) )
86 halfcn 
 |-  ( 1 / 2 ) e. CC
87 86 addridi 
 |-  ( ( 1 / 2 ) + 0 ) = ( 1 / 2 )
88 85 87 eqtrdi 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( _pi x. n ) ) ) = ( 1 / 2 ) )
89 88 oveq1d 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( _pi x. n ) ) ) / _pi ) = ( ( 1 / 2 ) / _pi ) )
90 ax-1cn 
 |-  1 e. CC
91 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
92 pire 
 |-  _pi e. RR
93 pipos 
 |-  0 < _pi
94 92 93 gt0ne0ii 
 |-  _pi =/= 0
95 15 94 pm3.2i 
 |-  ( _pi e. CC /\ _pi =/= 0 )
96 divdiv1 
 |-  ( ( 1 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( _pi e. CC /\ _pi =/= 0 ) ) -> ( ( 1 / 2 ) / _pi ) = ( 1 / ( 2 x. _pi ) ) )
97 90 91 95 96 mp3an 
 |-  ( ( 1 / 2 ) / _pi ) = ( 1 / ( 2 x. _pi ) )
98 97 a1i 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( 1 / 2 ) / _pi ) = ( 1 / ( 2 x. _pi ) ) )
99 48 89 98 3eqtrd 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) / _pi ) = ( 1 / ( 2 x. _pi ) ) )
100 3 oveq2i 
 |-  ( ( N + ( 1 / 2 ) ) x. A ) = ( ( N + ( 1 / 2 ) ) x. ( ( ( 2 x. K ) + 1 ) x. _pi ) )
101 100 a1i 
 |-  ( ph -> ( ( N + ( 1 / 2 ) ) x. A ) = ( ( N + ( 1 / 2 ) ) x. ( ( ( 2 x. K ) + 1 ) x. _pi ) ) )
102 86 a1i 
 |-  ( ph -> ( 1 / 2 ) e. CC )
103 49 102 addcld 
 |-  ( ph -> ( N + ( 1 / 2 ) ) e. CC )
104 50 10 mulcld 
 |-  ( ph -> ( 2 x. K ) e. CC )
105 peano2cn 
 |-  ( ( 2 x. K ) e. CC -> ( ( 2 x. K ) + 1 ) e. CC )
106 104 105 syl 
 |-  ( ph -> ( ( 2 x. K ) + 1 ) e. CC )
107 15 a1i 
 |-  ( ph -> _pi e. CC )
108 103 106 107 mulassd 
 |-  ( ph -> ( ( ( N + ( 1 / 2 ) ) x. ( ( 2 x. K ) + 1 ) ) x. _pi ) = ( ( N + ( 1 / 2 ) ) x. ( ( ( 2 x. K ) + 1 ) x. _pi ) ) )
109 1cnd 
 |-  ( ph -> 1 e. CC )
110 49 102 104 109 muladdd 
 |-  ( ph -> ( ( N + ( 1 / 2 ) ) x. ( ( 2 x. K ) + 1 ) ) = ( ( ( N x. ( 2 x. K ) ) + ( 1 x. ( 1 / 2 ) ) ) + ( ( N x. 1 ) + ( ( 2 x. K ) x. ( 1 / 2 ) ) ) ) )
111 49 50 10 mul12d 
 |-  ( ph -> ( N x. ( 2 x. K ) ) = ( 2 x. ( N x. K ) ) )
112 102 mullidd 
 |-  ( ph -> ( 1 x. ( 1 / 2 ) ) = ( 1 / 2 ) )
113 111 112 oveq12d 
 |-  ( ph -> ( ( N x. ( 2 x. K ) ) + ( 1 x. ( 1 / 2 ) ) ) = ( ( 2 x. ( N x. K ) ) + ( 1 / 2 ) ) )
114 49 mulridd 
 |-  ( ph -> ( N x. 1 ) = N )
115 50 10 mulcomd 
 |-  ( ph -> ( 2 x. K ) = ( K x. 2 ) )
116 115 oveq1d 
 |-  ( ph -> ( ( 2 x. K ) x. ( 1 / 2 ) ) = ( ( K x. 2 ) x. ( 1 / 2 ) ) )
117 10 50 102 mulassd 
 |-  ( ph -> ( ( K x. 2 ) x. ( 1 / 2 ) ) = ( K x. ( 2 x. ( 1 / 2 ) ) ) )
118 2thalfe1 
 |-  ( 2 x. ( 1 / 2 ) ) = 1
119 118 oveq2i 
 |-  ( K x. ( 2 x. ( 1 / 2 ) ) ) = ( K x. 1 )
120 10 mulridd 
 |-  ( ph -> ( K x. 1 ) = K )
121 119 120 eqtrid 
 |-  ( ph -> ( K x. ( 2 x. ( 1 / 2 ) ) ) = K )
122 116 117 121 3eqtrd 
 |-  ( ph -> ( ( 2 x. K ) x. ( 1 / 2 ) ) = K )
123 114 122 oveq12d 
 |-  ( ph -> ( ( N x. 1 ) + ( ( 2 x. K ) x. ( 1 / 2 ) ) ) = ( N + K ) )
124 113 123 oveq12d 
 |-  ( ph -> ( ( ( N x. ( 2 x. K ) ) + ( 1 x. ( 1 / 2 ) ) ) + ( ( N x. 1 ) + ( ( 2 x. K ) x. ( 1 / 2 ) ) ) ) = ( ( ( 2 x. ( N x. K ) ) + ( 1 / 2 ) ) + ( N + K ) ) )
125 49 10 mulcld 
 |-  ( ph -> ( N x. K ) e. CC )
126 50 125 mulcld 
 |-  ( ph -> ( 2 x. ( N x. K ) ) e. CC )
127 49 10 addcld 
 |-  ( ph -> ( N + K ) e. CC )
128 126 102 127 addassd 
 |-  ( ph -> ( ( ( 2 x. ( N x. K ) ) + ( 1 / 2 ) ) + ( N + K ) ) = ( ( 2 x. ( N x. K ) ) + ( ( 1 / 2 ) + ( N + K ) ) ) )
129 110 124 128 3eqtrd 
 |-  ( ph -> ( ( N + ( 1 / 2 ) ) x. ( ( 2 x. K ) + 1 ) ) = ( ( 2 x. ( N x. K ) ) + ( ( 1 / 2 ) + ( N + K ) ) ) )
130 102 127 addcld 
 |-  ( ph -> ( ( 1 / 2 ) + ( N + K ) ) e. CC )
131 126 130 addcomd 
 |-  ( ph -> ( ( 2 x. ( N x. K ) ) + ( ( 1 / 2 ) + ( N + K ) ) ) = ( ( ( 1 / 2 ) + ( N + K ) ) + ( 2 x. ( N x. K ) ) ) )
132 50 125 mulcomd 
 |-  ( ph -> ( 2 x. ( N x. K ) ) = ( ( N x. K ) x. 2 ) )
133 132 oveq2d 
 |-  ( ph -> ( ( ( 1 / 2 ) + ( N + K ) ) + ( 2 x. ( N x. K ) ) ) = ( ( ( 1 / 2 ) + ( N + K ) ) + ( ( N x. K ) x. 2 ) ) )
134 129 131 133 3eqtrd 
 |-  ( ph -> ( ( N + ( 1 / 2 ) ) x. ( ( 2 x. K ) + 1 ) ) = ( ( ( 1 / 2 ) + ( N + K ) ) + ( ( N x. K ) x. 2 ) ) )
135 134 oveq1d 
 |-  ( ph -> ( ( ( N + ( 1 / 2 ) ) x. ( ( 2 x. K ) + 1 ) ) x. _pi ) = ( ( ( ( 1 / 2 ) + ( N + K ) ) + ( ( N x. K ) x. 2 ) ) x. _pi ) )
136 125 50 mulcld 
 |-  ( ph -> ( ( N x. K ) x. 2 ) e. CC )
137 130 136 107 adddird 
 |-  ( ph -> ( ( ( ( 1 / 2 ) + ( N + K ) ) + ( ( N x. K ) x. 2 ) ) x. _pi ) = ( ( ( ( 1 / 2 ) + ( N + K ) ) x. _pi ) + ( ( ( N x. K ) x. 2 ) x. _pi ) ) )
138 125 50 107 mulassd 
 |-  ( ph -> ( ( ( N x. K ) x. 2 ) x. _pi ) = ( ( N x. K ) x. ( 2 x. _pi ) ) )
139 138 oveq2d 
 |-  ( ph -> ( ( ( ( 1 / 2 ) + ( N + K ) ) x. _pi ) + ( ( ( N x. K ) x. 2 ) x. _pi ) ) = ( ( ( ( 1 / 2 ) + ( N + K ) ) x. _pi ) + ( ( N x. K ) x. ( 2 x. _pi ) ) ) )
140 135 137 139 3eqtrd 
 |-  ( ph -> ( ( ( N + ( 1 / 2 ) ) x. ( ( 2 x. K ) + 1 ) ) x. _pi ) = ( ( ( ( 1 / 2 ) + ( N + K ) ) x. _pi ) + ( ( N x. K ) x. ( 2 x. _pi ) ) ) )
141 101 108 140 3eqtr2d 
 |-  ( ph -> ( ( N + ( 1 / 2 ) ) x. A ) = ( ( ( ( 1 / 2 ) + ( N + K ) ) x. _pi ) + ( ( N x. K ) x. ( 2 x. _pi ) ) ) )
142 141 fveq2d 
 |-  ( ph -> ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) = ( sin ` ( ( ( ( 1 / 2 ) + ( N + K ) ) x. _pi ) + ( ( N x. K ) x. ( 2 x. _pi ) ) ) ) )
143 130 107 mulcld 
 |-  ( ph -> ( ( ( 1 / 2 ) + ( N + K ) ) x. _pi ) e. CC )
144 1 nnzd 
 |-  ( ph -> N e. ZZ )
145 144 2 zmulcld 
 |-  ( ph -> ( N x. K ) e. ZZ )
146 sinper 
 |-  ( ( ( ( ( 1 / 2 ) + ( N + K ) ) x. _pi ) e. CC /\ ( N x. K ) e. ZZ ) -> ( sin ` ( ( ( ( 1 / 2 ) + ( N + K ) ) x. _pi ) + ( ( N x. K ) x. ( 2 x. _pi ) ) ) ) = ( sin ` ( ( ( 1 / 2 ) + ( N + K ) ) x. _pi ) ) )
147 143 145 146 syl2anc 
 |-  ( ph -> ( sin ` ( ( ( ( 1 / 2 ) + ( N + K ) ) x. _pi ) + ( ( N x. K ) x. ( 2 x. _pi ) ) ) ) = ( sin ` ( ( ( 1 / 2 ) + ( N + K ) ) x. _pi ) ) )
148 102 127 addcomd 
 |-  ( ph -> ( ( 1 / 2 ) + ( N + K ) ) = ( ( N + K ) + ( 1 / 2 ) ) )
149 49 10 102 addassd 
 |-  ( ph -> ( ( N + K ) + ( 1 / 2 ) ) = ( N + ( K + ( 1 / 2 ) ) ) )
150 10 102 addcld 
 |-  ( ph -> ( K + ( 1 / 2 ) ) e. CC )
151 49 150 addcomd 
 |-  ( ph -> ( N + ( K + ( 1 / 2 ) ) ) = ( ( K + ( 1 / 2 ) ) + N ) )
152 148 149 151 3eqtrd 
 |-  ( ph -> ( ( 1 / 2 ) + ( N + K ) ) = ( ( K + ( 1 / 2 ) ) + N ) )
153 152 oveq1d 
 |-  ( ph -> ( ( ( 1 / 2 ) + ( N + K ) ) x. _pi ) = ( ( ( K + ( 1 / 2 ) ) + N ) x. _pi ) )
154 153 fveq2d 
 |-  ( ph -> ( sin ` ( ( ( 1 / 2 ) + ( N + K ) ) x. _pi ) ) = ( sin ` ( ( ( K + ( 1 / 2 ) ) + N ) x. _pi ) ) )
155 142 147 154 3eqtrd 
 |-  ( ph -> ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) = ( sin ` ( ( ( K + ( 1 / 2 ) ) + N ) x. _pi ) ) )
156 3 a1i 
 |-  ( ph -> A = ( ( ( 2 x. K ) + 1 ) x. _pi ) )
157 156 oveq1d 
 |-  ( ph -> ( A / 2 ) = ( ( ( ( 2 x. K ) + 1 ) x. _pi ) / 2 ) )
158 106 107 50 52 div23d 
 |-  ( ph -> ( ( ( ( 2 x. K ) + 1 ) x. _pi ) / 2 ) = ( ( ( ( 2 x. K ) + 1 ) / 2 ) x. _pi ) )
159 104 109 50 52 divdird 
 |-  ( ph -> ( ( ( 2 x. K ) + 1 ) / 2 ) = ( ( ( 2 x. K ) / 2 ) + ( 1 / 2 ) ) )
160 10 50 52 divcan3d 
 |-  ( ph -> ( ( 2 x. K ) / 2 ) = K )
161 160 oveq1d 
 |-  ( ph -> ( ( ( 2 x. K ) / 2 ) + ( 1 / 2 ) ) = ( K + ( 1 / 2 ) ) )
162 159 161 eqtrd 
 |-  ( ph -> ( ( ( 2 x. K ) + 1 ) / 2 ) = ( K + ( 1 / 2 ) ) )
163 162 oveq1d 
 |-  ( ph -> ( ( ( ( 2 x. K ) + 1 ) / 2 ) x. _pi ) = ( ( K + ( 1 / 2 ) ) x. _pi ) )
164 157 158 163 3eqtrd 
 |-  ( ph -> ( A / 2 ) = ( ( K + ( 1 / 2 ) ) x. _pi ) )
165 164 fveq2d 
 |-  ( ph -> ( sin ` ( A / 2 ) ) = ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) )
166 165 oveq2d 
 |-  ( ph -> ( ( 2 x. _pi ) x. ( sin ` ( A / 2 ) ) ) = ( ( 2 x. _pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) )
167 155 166 oveq12d 
 |-  ( ph -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( ( 2 x. _pi ) x. ( sin ` ( A / 2 ) ) ) ) = ( ( sin ` ( ( ( K + ( 1 / 2 ) ) + N ) x. _pi ) ) / ( ( 2 x. _pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) ) )
168 167 adantr 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( ( 2 x. _pi ) x. ( sin ` ( A / 2 ) ) ) ) = ( ( sin ` ( ( ( K + ( 1 / 2 ) ) + N ) x. _pi ) ) / ( ( 2 x. _pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) ) )
169 150 49 107 adddird 
 |-  ( ph -> ( ( ( K + ( 1 / 2 ) ) + N ) x. _pi ) = ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( N x. _pi ) ) )
170 169 fveq2d 
 |-  ( ph -> ( sin ` ( ( ( K + ( 1 / 2 ) ) + N ) x. _pi ) ) = ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( N x. _pi ) ) ) )
171 170 oveq1d 
 |-  ( ph -> ( ( sin ` ( ( ( K + ( 1 / 2 ) ) + N ) x. _pi ) ) / ( ( 2 x. _pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) ) = ( ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( N x. _pi ) ) ) / ( ( 2 x. _pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) ) )
172 171 adantr 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( sin ` ( ( ( K + ( 1 / 2 ) ) + N ) x. _pi ) ) / ( ( 2 x. _pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) ) = ( ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( N x. _pi ) ) ) / ( ( 2 x. _pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) ) )
173 49 halfcld 
 |-  ( ph -> ( N / 2 ) e. CC )
174 50 173 mulcomd 
 |-  ( ph -> ( 2 x. ( N / 2 ) ) = ( ( N / 2 ) x. 2 ) )
175 53 174 eqtr3d 
 |-  ( ph -> N = ( ( N / 2 ) x. 2 ) )
176 175 oveq1d 
 |-  ( ph -> ( N x. _pi ) = ( ( ( N / 2 ) x. 2 ) x. _pi ) )
177 173 50 107 mulassd 
 |-  ( ph -> ( ( ( N / 2 ) x. 2 ) x. _pi ) = ( ( N / 2 ) x. ( 2 x. _pi ) ) )
178 176 177 eqtrd 
 |-  ( ph -> ( N x. _pi ) = ( ( N / 2 ) x. ( 2 x. _pi ) ) )
179 178 oveq2d 
 |-  ( ph -> ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( N x. _pi ) ) = ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( ( N / 2 ) x. ( 2 x. _pi ) ) ) )
180 179 fveq2d 
 |-  ( ph -> ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( N x. _pi ) ) ) = ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( ( N / 2 ) x. ( 2 x. _pi ) ) ) ) )
181 180 adantr 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( N x. _pi ) ) ) = ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( ( N / 2 ) x. ( 2 x. _pi ) ) ) ) )
182 10 adantr 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> K e. CC )
183 1cnd 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> 1 e. CC )
184 183 halfcld 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( 1 / 2 ) e. CC )
185 182 184 addcld 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( K + ( 1 / 2 ) ) e. CC )
186 15 a1i 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> _pi e. CC )
187 185 186 mulcld 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( K + ( 1 / 2 ) ) x. _pi ) e. CC )
188 sinper 
 |-  ( ( ( ( K + ( 1 / 2 ) ) x. _pi ) e. CC /\ ( N / 2 ) e. ZZ ) -> ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( ( N / 2 ) x. ( 2 x. _pi ) ) ) ) = ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) )
189 187 72 188 syl2anc 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( ( N / 2 ) x. ( 2 x. _pi ) ) ) ) = ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) )
190 181 189 eqtrd 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( N x. _pi ) ) ) = ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) )
191 50 107 mulcld 
 |-  ( ph -> ( 2 x. _pi ) e. CC )
192 150 107 mulcld 
 |-  ( ph -> ( ( K + ( 1 / 2 ) ) x. _pi ) e. CC )
193 192 sincld 
 |-  ( ph -> ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) e. CC )
194 191 193 mulcomd 
 |-  ( ph -> ( ( 2 x. _pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) = ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) x. ( 2 x. _pi ) ) )
195 194 adantr 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( 2 x. _pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) = ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) x. ( 2 x. _pi ) ) )
196 190 195 oveq12d 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( N x. _pi ) ) ) / ( ( 2 x. _pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) ) = ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) / ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) x. ( 2 x. _pi ) ) ) )
197 94 a1i 
 |-  ( ph -> _pi =/= 0 )
198 150 107 197 divcan4d 
 |-  ( ph -> ( ( ( K + ( 1 / 2 ) ) x. _pi ) / _pi ) = ( K + ( 1 / 2 ) ) )
199 2 zred 
 |-  ( ph -> K e. RR )
200 69 a1i 
 |-  ( ph -> 2 e. RR+ )
201 200 rpreccld 
 |-  ( ph -> ( 1 / 2 ) e. RR+ )
202 199 201 ltaddrpd 
 |-  ( ph -> K < ( K + ( 1 / 2 ) ) )
203 1red 
 |-  ( ph -> 1 e. RR )
204 203 rehalfcld 
 |-  ( ph -> ( 1 / 2 ) e. RR )
205 halflt1 
 |-  ( 1 / 2 ) < 1
206 205 a1i 
 |-  ( ph -> ( 1 / 2 ) < 1 )
207 204 203 199 206 ltadd2dd 
 |-  ( ph -> ( K + ( 1 / 2 ) ) < ( K + 1 ) )
208 btwnnz 
 |-  ( ( K e. ZZ /\ K < ( K + ( 1 / 2 ) ) /\ ( K + ( 1 / 2 ) ) < ( K + 1 ) ) -> -. ( K + ( 1 / 2 ) ) e. ZZ )
209 2 202 207 208 syl3anc 
 |-  ( ph -> -. ( K + ( 1 / 2 ) ) e. ZZ )
210 198 209 eqneltrd 
 |-  ( ph -> -. ( ( ( K + ( 1 / 2 ) ) x. _pi ) / _pi ) e. ZZ )
211 sineq0 
 |-  ( ( ( K + ( 1 / 2 ) ) x. _pi ) e. CC -> ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) = 0 <-> ( ( ( K + ( 1 / 2 ) ) x. _pi ) / _pi ) e. ZZ ) )
212 192 211 syl 
 |-  ( ph -> ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) = 0 <-> ( ( ( K + ( 1 / 2 ) ) x. _pi ) / _pi ) e. ZZ ) )
213 210 212 mtbird 
 |-  ( ph -> -. ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) = 0 )
214 213 neqned 
 |-  ( ph -> ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) =/= 0 )
215 50 107 52 197 mulne0d 
 |-  ( ph -> ( 2 x. _pi ) =/= 0 )
216 193 193 191 214 215 divdiv1d 
 |-  ( ph -> ( ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) / ( 2 x. _pi ) ) = ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) / ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) x. ( 2 x. _pi ) ) ) )
217 193 214 dividd 
 |-  ( ph -> ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) = 1 )
218 217 oveq1d 
 |-  ( ph -> ( ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) / ( 2 x. _pi ) ) = ( 1 / ( 2 x. _pi ) ) )
219 216 218 eqtr3d 
 |-  ( ph -> ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) / ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) x. ( 2 x. _pi ) ) ) = ( 1 / ( 2 x. _pi ) ) )
220 219 adantr 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) / ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) x. ( 2 x. _pi ) ) ) = ( 1 / ( 2 x. _pi ) ) )
221 196 220 eqtrd 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( N x. _pi ) ) ) / ( ( 2 x. _pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) ) = ( 1 / ( 2 x. _pi ) ) )
222 168 172 221 3eqtrrd 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( 1 / ( 2 x. _pi ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( ( 2 x. _pi ) x. ( sin ` ( A / 2 ) ) ) ) )
223 99 222 eqtrd 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) / _pi ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( ( 2 x. _pi ) x. ( sin ` ( A / 2 ) ) ) ) )
224 47 adantr 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) / _pi ) = ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( _pi x. n ) ) ) / _pi ) )
225 144 adantr 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> N e. ZZ )
226 simpr 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> -. ( N mod 2 ) = 0 )
227 226 neqned 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( N mod 2 ) =/= 0 )
228 oddfl 
 |-  ( ( N e. ZZ /\ ( N mod 2 ) =/= 0 ) -> N = ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) )
229 225 227 228 syl2anc 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> N = ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) )
230 229 oveq2d 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( 1 ... N ) = ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) )
231 230 sumeq1d 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> sum_ n e. ( 1 ... N ) ( cos ` ( _pi x. n ) ) = sum_ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ( cos ` ( _pi x. n ) ) )
232 fvoveq1 
 |-  ( N = 1 -> ( |_ ` ( N / 2 ) ) = ( |_ ` ( 1 / 2 ) ) )
233 halffl 
 |-  ( |_ ` ( 1 / 2 ) ) = 0
234 232 233 eqtrdi 
 |-  ( N = 1 -> ( |_ ` ( N / 2 ) ) = 0 )
235 234 oveq2d 
 |-  ( N = 1 -> ( 2 x. ( |_ ` ( N / 2 ) ) ) = ( 2 x. 0 ) )
236 2t0e0 
 |-  ( 2 x. 0 ) = 0
237 235 236 eqtrdi 
 |-  ( N = 1 -> ( 2 x. ( |_ ` ( N / 2 ) ) ) = 0 )
238 237 oveq1d 
 |-  ( N = 1 -> ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) = ( 0 + 1 ) )
239 90 addlidi 
 |-  ( 0 + 1 ) = 1
240 238 239 eqtrdi 
 |-  ( N = 1 -> ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) = 1 )
241 240 oveq2d 
 |-  ( N = 1 -> ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) = ( 1 ... 1 ) )
242 241 sumeq1d 
 |-  ( N = 1 -> sum_ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ( cos ` ( _pi x. n ) ) = sum_ n e. ( 1 ... 1 ) ( cos ` ( _pi x. n ) ) )
243 1z 
 |-  1 e. ZZ
244 coscl 
 |-  ( _pi e. CC -> ( cos ` _pi ) e. CC )
245 15 244 ax-mp 
 |-  ( cos ` _pi ) e. CC
246 oveq2 
 |-  ( n = 1 -> ( _pi x. n ) = ( _pi x. 1 ) )
247 15 mulridi 
 |-  ( _pi x. 1 ) = _pi
248 246 247 eqtrdi 
 |-  ( n = 1 -> ( _pi x. n ) = _pi )
249 248 fveq2d 
 |-  ( n = 1 -> ( cos ` ( _pi x. n ) ) = ( cos ` _pi ) )
250 249 fsum1 
 |-  ( ( 1 e. ZZ /\ ( cos ` _pi ) e. CC ) -> sum_ n e. ( 1 ... 1 ) ( cos ` ( _pi x. n ) ) = ( cos ` _pi ) )
251 243 245 250 mp2an 
 |-  sum_ n e. ( 1 ... 1 ) ( cos ` ( _pi x. n ) ) = ( cos ` _pi )
252 251 a1i 
 |-  ( N = 1 -> sum_ n e. ( 1 ... 1 ) ( cos ` ( _pi x. n ) ) = ( cos ` _pi ) )
253 cospi 
 |-  ( cos ` _pi ) = -u 1
254 253 a1i 
 |-  ( N = 1 -> ( cos ` _pi ) = -u 1 )
255 242 252 254 3eqtrd 
 |-  ( N = 1 -> sum_ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ( cos ` ( _pi x. n ) ) = -u 1 )
256 255 adantl 
 |-  ( ( ph /\ N = 1 ) -> sum_ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ( cos ` ( _pi x. n ) ) = -u 1 )
257 2nn 
 |-  2 e. NN
258 257 a1i 
 |-  ( ( ph /\ -. N = 1 ) -> 2 e. NN )
259 67 rehalfcld 
 |-  ( ph -> ( N / 2 ) e. RR )
260 259 flcld 
 |-  ( ph -> ( |_ ` ( N / 2 ) ) e. ZZ )
261 260 adantr 
 |-  ( ( ph /\ -. N = 1 ) -> ( |_ ` ( N / 2 ) ) e. ZZ )
262 2div2e1 
 |-  ( 2 / 2 ) = 1
263 73 a1i 
 |-  ( ( ph /\ -. N = 1 ) -> 2 e. RR )
264 67 adantr 
 |-  ( ( ph /\ -. N = 1 ) -> N e. RR )
265 69 a1i 
 |-  ( ( ph /\ -. N = 1 ) -> 2 e. RR+ )
266 neqne 
 |-  ( -. N = 1 -> N =/= 1 )
267 nnne1ge2 
 |-  ( ( N e. NN /\ N =/= 1 ) -> 2 <_ N )
268 1 266 267 syl2an 
 |-  ( ( ph /\ -. N = 1 ) -> 2 <_ N )
269 263 264 265 268 lediv1dd 
 |-  ( ( ph /\ -. N = 1 ) -> ( 2 / 2 ) <_ ( N / 2 ) )
270 262 269 eqbrtrrid 
 |-  ( ( ph /\ -. N = 1 ) -> 1 <_ ( N / 2 ) )
271 259 adantr 
 |-  ( ( ph /\ -. N = 1 ) -> ( N / 2 ) e. RR )
272 flge 
 |-  ( ( ( N / 2 ) e. RR /\ 1 e. ZZ ) -> ( 1 <_ ( N / 2 ) <-> 1 <_ ( |_ ` ( N / 2 ) ) ) )
273 271 243 272 sylancl 
 |-  ( ( ph /\ -. N = 1 ) -> ( 1 <_ ( N / 2 ) <-> 1 <_ ( |_ ` ( N / 2 ) ) ) )
274 270 273 mpbid 
 |-  ( ( ph /\ -. N = 1 ) -> 1 <_ ( |_ ` ( N / 2 ) ) )
275 elnnz1 
 |-  ( ( |_ ` ( N / 2 ) ) e. NN <-> ( ( |_ ` ( N / 2 ) ) e. ZZ /\ 1 <_ ( |_ ` ( N / 2 ) ) ) )
276 261 274 275 sylanbrc 
 |-  ( ( ph /\ -. N = 1 ) -> ( |_ ` ( N / 2 ) ) e. NN )
277 258 276 nnmulcld 
 |-  ( ( ph /\ -. N = 1 ) -> ( 2 x. ( |_ ` ( N / 2 ) ) ) e. NN )
278 nnuz 
 |-  NN = ( ZZ>= ` 1 )
279 277 278 eleqtrdi 
 |-  ( ( ph /\ -. N = 1 ) -> ( 2 x. ( |_ ` ( N / 2 ) ) ) e. ( ZZ>= ` 1 ) )
280 15 a1i 
 |-  ( ( ( ph /\ -. N = 1 ) /\ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) -> _pi e. CC )
281 elfzelz 
 |-  ( n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) -> n e. ZZ )
282 281 zcnd 
 |-  ( n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) -> n e. CC )
283 282 adantl 
 |-  ( ( ( ph /\ -. N = 1 ) /\ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) -> n e. CC )
284 280 283 mulcld 
 |-  ( ( ( ph /\ -. N = 1 ) /\ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) -> ( _pi x. n ) e. CC )
285 284 coscld 
 |-  ( ( ( ph /\ -. N = 1 ) /\ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) -> ( cos ` ( _pi x. n ) ) e. CC )
286 oveq2 
 |-  ( n = ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) -> ( _pi x. n ) = ( _pi x. ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) )
287 286 fveq2d 
 |-  ( n = ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) -> ( cos ` ( _pi x. n ) ) = ( cos ` ( _pi x. ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) )
288 279 285 287 fsump1 
 |-  ( ( ph /\ -. N = 1 ) -> sum_ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ( cos ` ( _pi x. n ) ) = ( sum_ n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) ( cos ` ( _pi x. n ) ) + ( cos ` ( _pi x. ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) ) )
289 15 a1i 
 |-  ( n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) -> _pi e. CC )
290 elfzelz 
 |-  ( n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) -> n e. ZZ )
291 290 zcnd 
 |-  ( n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) -> n e. CC )
292 289 291 mulcomd 
 |-  ( n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) -> ( _pi x. n ) = ( n x. _pi ) )
293 292 fveq2d 
 |-  ( n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) -> ( cos ` ( _pi x. n ) ) = ( cos ` ( n x. _pi ) ) )
294 293 sumeq2i 
 |-  sum_ n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) ( cos ` ( _pi x. n ) ) = sum_ n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) ( cos ` ( n x. _pi ) )
295 dirkertrigeqlem1 
 |-  ( ( |_ ` ( N / 2 ) ) e. NN -> sum_ n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) ( cos ` ( n x. _pi ) ) = 0 )
296 276 295 syl 
 |-  ( ( ph /\ -. N = 1 ) -> sum_ n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) ( cos ` ( n x. _pi ) ) = 0 )
297 294 296 eqtrid 
 |-  ( ( ph /\ -. N = 1 ) -> sum_ n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) ( cos ` ( _pi x. n ) ) = 0 )
298 260 zcnd 
 |-  ( ph -> ( |_ ` ( N / 2 ) ) e. CC )
299 50 298 mulcld 
 |-  ( ph -> ( 2 x. ( |_ ` ( N / 2 ) ) ) e. CC )
300 107 299 109 adddid 
 |-  ( ph -> ( _pi x. ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) = ( ( _pi x. ( 2 x. ( |_ ` ( N / 2 ) ) ) ) + ( _pi x. 1 ) ) )
301 107 50 298 mul13d 
 |-  ( ph -> ( _pi x. ( 2 x. ( |_ ` ( N / 2 ) ) ) ) = ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) )
302 247 a1i 
 |-  ( ph -> ( _pi x. 1 ) = _pi )
303 301 302 oveq12d 
 |-  ( ph -> ( ( _pi x. ( 2 x. ( |_ ` ( N / 2 ) ) ) ) + ( _pi x. 1 ) ) = ( ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) + _pi ) )
304 298 191 mulcld 
 |-  ( ph -> ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) e. CC )
305 304 107 addcomd 
 |-  ( ph -> ( ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) + _pi ) = ( _pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) )
306 300 303 305 3eqtrd 
 |-  ( ph -> ( _pi x. ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) = ( _pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) )
307 306 fveq2d 
 |-  ( ph -> ( cos ` ( _pi x. ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) = ( cos ` ( _pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) ) )
308 cosper 
 |-  ( ( _pi e. CC /\ ( |_ ` ( N / 2 ) ) e. ZZ ) -> ( cos ` ( _pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) ) = ( cos ` _pi ) )
309 107 260 308 syl2anc 
 |-  ( ph -> ( cos ` ( _pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) ) = ( cos ` _pi ) )
310 253 a1i 
 |-  ( ph -> ( cos ` _pi ) = -u 1 )
311 307 309 310 3eqtrd 
 |-  ( ph -> ( cos ` ( _pi x. ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) = -u 1 )
312 311 adantr 
 |-  ( ( ph /\ -. N = 1 ) -> ( cos ` ( _pi x. ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) = -u 1 )
313 297 312 oveq12d 
 |-  ( ( ph /\ -. N = 1 ) -> ( sum_ n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) ( cos ` ( _pi x. n ) ) + ( cos ` ( _pi x. ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) ) = ( 0 + -u 1 ) )
314 neg1cn 
 |-  -u 1 e. CC
315 314 addlidi 
 |-  ( 0 + -u 1 ) = -u 1
316 315 a1i 
 |-  ( ( ph /\ -. N = 1 ) -> ( 0 + -u 1 ) = -u 1 )
317 288 313 316 3eqtrd 
 |-  ( ( ph /\ -. N = 1 ) -> sum_ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ( cos ` ( _pi x. n ) ) = -u 1 )
318 256 317 pm2.61dan 
 |-  ( ph -> sum_ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ( cos ` ( _pi x. n ) ) = -u 1 )
319 318 adantr 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> sum_ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ( cos ` ( _pi x. n ) ) = -u 1 )
320 231 319 eqtrd 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> sum_ n e. ( 1 ... N ) ( cos ` ( _pi x. n ) ) = -u 1 )
321 320 oveq2d 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( _pi x. n ) ) ) = ( ( 1 / 2 ) + -u 1 ) )
322 321 oveq1d 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( _pi x. n ) ) ) / _pi ) = ( ( ( 1 / 2 ) + -u 1 ) / _pi ) )
323 167 171 eqtrd 
 |-  ( ph -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( ( 2 x. _pi ) x. ( sin ` ( A / 2 ) ) ) ) = ( ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( N x. _pi ) ) ) / ( ( 2 x. _pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) ) )
324 323 adantr 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( ( 2 x. _pi ) x. ( sin ` ( A / 2 ) ) ) ) = ( ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( N x. _pi ) ) ) / ( ( 2 x. _pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) ) )
325 229 oveq1d 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( N x. _pi ) = ( ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) x. _pi ) )
326 299 109 107 adddird 
 |-  ( ph -> ( ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) x. _pi ) = ( ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. _pi ) + ( 1 x. _pi ) ) )
327 107 mullidd 
 |-  ( ph -> ( 1 x. _pi ) = _pi )
328 327 oveq2d 
 |-  ( ph -> ( ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. _pi ) + ( 1 x. _pi ) ) = ( ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. _pi ) + _pi ) )
329 299 107 mulcld 
 |-  ( ph -> ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. _pi ) e. CC )
330 329 107 addcomd 
 |-  ( ph -> ( ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. _pi ) + _pi ) = ( _pi + ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. _pi ) ) )
331 326 328 330 3eqtrd 
 |-  ( ph -> ( ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) x. _pi ) = ( _pi + ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. _pi ) ) )
332 331 adantr 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) x. _pi ) = ( _pi + ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. _pi ) ) )
333 50 298 mulcomd 
 |-  ( ph -> ( 2 x. ( |_ ` ( N / 2 ) ) ) = ( ( |_ ` ( N / 2 ) ) x. 2 ) )
334 333 oveq1d 
 |-  ( ph -> ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. _pi ) = ( ( ( |_ ` ( N / 2 ) ) x. 2 ) x. _pi ) )
335 298 50 107 mulassd 
 |-  ( ph -> ( ( ( |_ ` ( N / 2 ) ) x. 2 ) x. _pi ) = ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) )
336 334 335 eqtrd 
 |-  ( ph -> ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. _pi ) = ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) )
337 336 oveq2d 
 |-  ( ph -> ( _pi + ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. _pi ) ) = ( _pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) )
338 337 adantr 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( _pi + ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. _pi ) ) = ( _pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) )
339 325 332 338 3eqtrd 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( N x. _pi ) = ( _pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) )
340 339 oveq2d 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( N x. _pi ) ) = ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( _pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) ) )
341 192 adantr 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( K + ( 1 / 2 ) ) x. _pi ) e. CC )
342 15 a1i 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> _pi e. CC )
343 304 adantr 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) e. CC )
344 341 342 343 addassd 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( ( ( K + ( 1 / 2 ) ) x. _pi ) + _pi ) + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) = ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( _pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) ) )
345 340 344 eqtr4d 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( N x. _pi ) ) = ( ( ( ( K + ( 1 / 2 ) ) x. _pi ) + _pi ) + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) )
346 345 fveq2d 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( N x. _pi ) ) ) = ( sin ` ( ( ( ( K + ( 1 / 2 ) ) x. _pi ) + _pi ) + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) ) )
347 346 oveq1d 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( N x. _pi ) ) ) / ( ( 2 x. _pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) ) = ( ( sin ` ( ( ( ( K + ( 1 / 2 ) ) x. _pi ) + _pi ) + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) ) / ( ( 2 x. _pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) ) )
348 192 107 addcld 
 |-  ( ph -> ( ( ( K + ( 1 / 2 ) ) x. _pi ) + _pi ) e. CC )
349 sinper 
 |-  ( ( ( ( ( K + ( 1 / 2 ) ) x. _pi ) + _pi ) e. CC /\ ( |_ ` ( N / 2 ) ) e. ZZ ) -> ( sin ` ( ( ( ( K + ( 1 / 2 ) ) x. _pi ) + _pi ) + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) ) = ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + _pi ) ) )
350 348 260 349 syl2anc 
 |-  ( ph -> ( sin ` ( ( ( ( K + ( 1 / 2 ) ) x. _pi ) + _pi ) + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) ) = ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + _pi ) ) )
351 sinppi 
 |-  ( ( ( K + ( 1 / 2 ) ) x. _pi ) e. CC -> ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + _pi ) ) = -u ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) )
352 192 351 syl 
 |-  ( ph -> ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + _pi ) ) = -u ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) )
353 350 352 eqtrd 
 |-  ( ph -> ( sin ` ( ( ( ( K + ( 1 / 2 ) ) x. _pi ) + _pi ) + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) ) = -u ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) )
354 353 oveq1d 
 |-  ( ph -> ( ( sin ` ( ( ( ( K + ( 1 / 2 ) ) x. _pi ) + _pi ) + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) ) / ( ( 2 x. _pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) ) = ( -u ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) / ( ( 2 x. _pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) ) )
355 194 oveq2d 
 |-  ( ph -> ( -u ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) / ( ( 2 x. _pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) ) = ( -u ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) / ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) x. ( 2 x. _pi ) ) ) )
356 193 193 214 divnegd 
 |-  ( ph -> -u ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) = ( -u ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) )
357 217 negeqd 
 |-  ( ph -> -u ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) = -u 1 )
358 356 357 eqtr3d 
 |-  ( ph -> ( -u ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) = -u 1 )
359 358 oveq1d 
 |-  ( ph -> ( ( -u ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) / ( 2 x. _pi ) ) = ( -u 1 / ( 2 x. _pi ) ) )
360 193 negcld 
 |-  ( ph -> -u ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) e. CC )
361 360 193 191 214 215 divdiv1d 
 |-  ( ph -> ( ( -u ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) / ( 2 x. _pi ) ) = ( -u ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) / ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) x. ( 2 x. _pi ) ) ) )
362 86 90 negsubi 
 |-  ( ( 1 / 2 ) + -u 1 ) = ( ( 1 / 2 ) - 1 )
363 90 86 negsubdi2i 
 |-  -u ( 1 - ( 1 / 2 ) ) = ( ( 1 / 2 ) - 1 )
364 1mhlfehlf 
 |-  ( 1 - ( 1 / 2 ) ) = ( 1 / 2 )
365 364 negeqi 
 |-  -u ( 1 - ( 1 / 2 ) ) = -u ( 1 / 2 )
366 2cn 
 |-  2 e. CC
367 divneg 
 |-  ( ( 1 e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> -u ( 1 / 2 ) = ( -u 1 / 2 ) )
368 90 366 51 367 mp3an 
 |-  -u ( 1 / 2 ) = ( -u 1 / 2 )
369 365 368 eqtri 
 |-  -u ( 1 - ( 1 / 2 ) ) = ( -u 1 / 2 )
370 362 363 369 3eqtr2i 
 |-  ( ( 1 / 2 ) + -u 1 ) = ( -u 1 / 2 )
371 370 oveq1i 
 |-  ( ( ( 1 / 2 ) + -u 1 ) / _pi ) = ( ( -u 1 / 2 ) / _pi )
372 divdiv1 
 |-  ( ( -u 1 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( _pi e. CC /\ _pi =/= 0 ) ) -> ( ( -u 1 / 2 ) / _pi ) = ( -u 1 / ( 2 x. _pi ) ) )
373 314 91 95 372 mp3an 
 |-  ( ( -u 1 / 2 ) / _pi ) = ( -u 1 / ( 2 x. _pi ) )
374 371 373 eqtr2i 
 |-  ( -u 1 / ( 2 x. _pi ) ) = ( ( ( 1 / 2 ) + -u 1 ) / _pi )
375 374 a1i 
 |-  ( ph -> ( -u 1 / ( 2 x. _pi ) ) = ( ( ( 1 / 2 ) + -u 1 ) / _pi ) )
376 359 361 375 3eqtr3d 
 |-  ( ph -> ( -u ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) / ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) x. ( 2 x. _pi ) ) ) = ( ( ( 1 / 2 ) + -u 1 ) / _pi ) )
377 354 355 376 3eqtrd 
 |-  ( ph -> ( ( sin ` ( ( ( ( K + ( 1 / 2 ) ) x. _pi ) + _pi ) + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) ) / ( ( 2 x. _pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) ) = ( ( ( 1 / 2 ) + -u 1 ) / _pi ) )
378 377 adantr 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( sin ` ( ( ( ( K + ( 1 / 2 ) ) x. _pi ) + _pi ) + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) ) / ( ( 2 x. _pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) ) = ( ( ( 1 / 2 ) + -u 1 ) / _pi ) )
379 324 347 378 3eqtrrd 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( ( 1 / 2 ) + -u 1 ) / _pi ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( ( 2 x. _pi ) x. ( sin ` ( A / 2 ) ) ) ) )
380 224 322 379 3eqtrd 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) / _pi ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( ( 2 x. _pi ) x. ( sin ` ( A / 2 ) ) ) ) )
381 223 380 pm2.61dan 
 |-  ( ph -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) / _pi ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( ( 2 x. _pi ) x. ( sin ` ( A / 2 ) ) ) ) )