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 mulid2d 
 |-  ( 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 addid1i 
 |-  ( ( 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 mulid2d 
 |-  ( 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 mulid1d 
 |-  ( 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 2cn 
 |-  2 e. CC
119 118 51 recidi 
 |-  ( 2 x. ( 1 / 2 ) ) = 1
120 119 oveq2i 
 |-  ( K x. ( 2 x. ( 1 / 2 ) ) ) = ( K x. 1 )
121 10 mulid1d 
 |-  ( ph -> ( K x. 1 ) = K )
122 120 121 syl5eq 
 |-  ( ph -> ( K x. ( 2 x. ( 1 / 2 ) ) ) = K )
123 116 117 122 3eqtrd 
 |-  ( ph -> ( ( 2 x. K ) x. ( 1 / 2 ) ) = K )
124 114 123 oveq12d 
 |-  ( ph -> ( ( N x. 1 ) + ( ( 2 x. K ) x. ( 1 / 2 ) ) ) = ( N + K ) )
125 113 124 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 ) ) )
126 49 10 mulcld 
 |-  ( ph -> ( N x. K ) e. CC )
127 50 126 mulcld 
 |-  ( ph -> ( 2 x. ( N x. K ) ) e. CC )
128 49 10 addcld 
 |-  ( ph -> ( N + K ) e. CC )
129 127 102 128 addassd 
 |-  ( ph -> ( ( ( 2 x. ( N x. K ) ) + ( 1 / 2 ) ) + ( N + K ) ) = ( ( 2 x. ( N x. K ) ) + ( ( 1 / 2 ) + ( N + K ) ) ) )
130 110 125 129 3eqtrd 
 |-  ( ph -> ( ( N + ( 1 / 2 ) ) x. ( ( 2 x. K ) + 1 ) ) = ( ( 2 x. ( N x. K ) ) + ( ( 1 / 2 ) + ( N + K ) ) ) )
131 102 128 addcld 
 |-  ( ph -> ( ( 1 / 2 ) + ( N + K ) ) e. CC )
132 127 131 addcomd 
 |-  ( ph -> ( ( 2 x. ( N x. K ) ) + ( ( 1 / 2 ) + ( N + K ) ) ) = ( ( ( 1 / 2 ) + ( N + K ) ) + ( 2 x. ( N x. K ) ) ) )
133 50 126 mulcomd 
 |-  ( ph -> ( 2 x. ( N x. K ) ) = ( ( N x. K ) x. 2 ) )
134 133 oveq2d 
 |-  ( ph -> ( ( ( 1 / 2 ) + ( N + K ) ) + ( 2 x. ( N x. K ) ) ) = ( ( ( 1 / 2 ) + ( N + K ) ) + ( ( N x. K ) x. 2 ) ) )
135 130 132 134 3eqtrd 
 |-  ( ph -> ( ( N + ( 1 / 2 ) ) x. ( ( 2 x. K ) + 1 ) ) = ( ( ( 1 / 2 ) + ( N + K ) ) + ( ( N x. K ) x. 2 ) ) )
136 135 oveq1d 
 |-  ( ph -> ( ( ( N + ( 1 / 2 ) ) x. ( ( 2 x. K ) + 1 ) ) x. _pi ) = ( ( ( ( 1 / 2 ) + ( N + K ) ) + ( ( N x. K ) x. 2 ) ) x. _pi ) )
137 126 50 mulcld 
 |-  ( ph -> ( ( N x. K ) x. 2 ) e. CC )
138 131 137 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 ) ) )
139 126 50 107 mulassd 
 |-  ( ph -> ( ( ( N x. K ) x. 2 ) x. _pi ) = ( ( N x. K ) x. ( 2 x. _pi ) ) )
140 139 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 ) ) ) )
141 136 138 140 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 ) ) ) )
142 101 108 141 3eqtr2d 
 |-  ( ph -> ( ( N + ( 1 / 2 ) ) x. A ) = ( ( ( ( 1 / 2 ) + ( N + K ) ) x. _pi ) + ( ( N x. K ) x. ( 2 x. _pi ) ) ) )
143 142 fveq2d 
 |-  ( ph -> ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) = ( sin ` ( ( ( ( 1 / 2 ) + ( N + K ) ) x. _pi ) + ( ( N x. K ) x. ( 2 x. _pi ) ) ) ) )
144 131 107 mulcld 
 |-  ( ph -> ( ( ( 1 / 2 ) + ( N + K ) ) x. _pi ) e. CC )
145 1 nnzd 
 |-  ( ph -> N e. ZZ )
146 145 2 zmulcld 
 |-  ( ph -> ( N x. K ) e. ZZ )
147 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 ) ) )
148 144 146 147 syl2anc 
 |-  ( ph -> ( sin ` ( ( ( ( 1 / 2 ) + ( N + K ) ) x. _pi ) + ( ( N x. K ) x. ( 2 x. _pi ) ) ) ) = ( sin ` ( ( ( 1 / 2 ) + ( N + K ) ) x. _pi ) ) )
149 102 128 addcomd 
 |-  ( ph -> ( ( 1 / 2 ) + ( N + K ) ) = ( ( N + K ) + ( 1 / 2 ) ) )
150 49 10 102 addassd 
 |-  ( ph -> ( ( N + K ) + ( 1 / 2 ) ) = ( N + ( K + ( 1 / 2 ) ) ) )
151 10 102 addcld 
 |-  ( ph -> ( K + ( 1 / 2 ) ) e. CC )
152 49 151 addcomd 
 |-  ( ph -> ( N + ( K + ( 1 / 2 ) ) ) = ( ( K + ( 1 / 2 ) ) + N ) )
153 149 150 152 3eqtrd 
 |-  ( ph -> ( ( 1 / 2 ) + ( N + K ) ) = ( ( K + ( 1 / 2 ) ) + N ) )
154 153 oveq1d 
 |-  ( ph -> ( ( ( 1 / 2 ) + ( N + K ) ) x. _pi ) = ( ( ( K + ( 1 / 2 ) ) + N ) x. _pi ) )
155 154 fveq2d 
 |-  ( ph -> ( sin ` ( ( ( 1 / 2 ) + ( N + K ) ) x. _pi ) ) = ( sin ` ( ( ( K + ( 1 / 2 ) ) + N ) x. _pi ) ) )
156 143 148 155 3eqtrd 
 |-  ( ph -> ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) = ( sin ` ( ( ( K + ( 1 / 2 ) ) + N ) x. _pi ) ) )
157 3 a1i 
 |-  ( ph -> A = ( ( ( 2 x. K ) + 1 ) x. _pi ) )
158 157 oveq1d 
 |-  ( ph -> ( A / 2 ) = ( ( ( ( 2 x. K ) + 1 ) x. _pi ) / 2 ) )
159 106 107 50 52 div23d 
 |-  ( ph -> ( ( ( ( 2 x. K ) + 1 ) x. _pi ) / 2 ) = ( ( ( ( 2 x. K ) + 1 ) / 2 ) x. _pi ) )
160 104 109 50 52 divdird 
 |-  ( ph -> ( ( ( 2 x. K ) + 1 ) / 2 ) = ( ( ( 2 x. K ) / 2 ) + ( 1 / 2 ) ) )
161 10 50 52 divcan3d 
 |-  ( ph -> ( ( 2 x. K ) / 2 ) = K )
162 161 oveq1d 
 |-  ( ph -> ( ( ( 2 x. K ) / 2 ) + ( 1 / 2 ) ) = ( K + ( 1 / 2 ) ) )
163 160 162 eqtrd 
 |-  ( ph -> ( ( ( 2 x. K ) + 1 ) / 2 ) = ( K + ( 1 / 2 ) ) )
164 163 oveq1d 
 |-  ( ph -> ( ( ( ( 2 x. K ) + 1 ) / 2 ) x. _pi ) = ( ( K + ( 1 / 2 ) ) x. _pi ) )
165 158 159 164 3eqtrd 
 |-  ( ph -> ( A / 2 ) = ( ( K + ( 1 / 2 ) ) x. _pi ) )
166 165 fveq2d 
 |-  ( ph -> ( sin ` ( A / 2 ) ) = ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) )
167 166 oveq2d 
 |-  ( ph -> ( ( 2 x. _pi ) x. ( sin ` ( A / 2 ) ) ) = ( ( 2 x. _pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) )
168 156 167 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 ) ) ) ) )
169 168 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 ) ) ) ) )
170 151 49 107 adddird 
 |-  ( ph -> ( ( ( K + ( 1 / 2 ) ) + N ) x. _pi ) = ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( N x. _pi ) ) )
171 170 fveq2d 
 |-  ( ph -> ( sin ` ( ( ( K + ( 1 / 2 ) ) + N ) x. _pi ) ) = ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( N x. _pi ) ) ) )
172 171 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 ) ) ) ) )
173 172 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 ) ) ) ) )
174 49 halfcld 
 |-  ( ph -> ( N / 2 ) e. CC )
175 50 174 mulcomd 
 |-  ( ph -> ( 2 x. ( N / 2 ) ) = ( ( N / 2 ) x. 2 ) )
176 53 175 eqtr3d 
 |-  ( ph -> N = ( ( N / 2 ) x. 2 ) )
177 176 oveq1d 
 |-  ( ph -> ( N x. _pi ) = ( ( ( N / 2 ) x. 2 ) x. _pi ) )
178 174 50 107 mulassd 
 |-  ( ph -> ( ( ( N / 2 ) x. 2 ) x. _pi ) = ( ( N / 2 ) x. ( 2 x. _pi ) ) )
179 177 178 eqtrd 
 |-  ( ph -> ( N x. _pi ) = ( ( N / 2 ) x. ( 2 x. _pi ) ) )
180 179 oveq2d 
 |-  ( ph -> ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( N x. _pi ) ) = ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( ( N / 2 ) x. ( 2 x. _pi ) ) ) )
181 180 fveq2d 
 |-  ( ph -> ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( N x. _pi ) ) ) = ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( ( N / 2 ) x. ( 2 x. _pi ) ) ) ) )
182 181 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 ) ) ) ) )
183 10 adantr 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> K e. CC )
184 1cnd 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> 1 e. CC )
185 184 halfcld 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( 1 / 2 ) e. CC )
186 183 185 addcld 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( K + ( 1 / 2 ) ) e. CC )
187 15 a1i 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> _pi e. CC )
188 186 187 mulcld 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( K + ( 1 / 2 ) ) x. _pi ) e. CC )
189 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 ) ) )
190 188 72 189 syl2anc 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( ( N / 2 ) x. ( 2 x. _pi ) ) ) ) = ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) )
191 182 190 eqtrd 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + ( N x. _pi ) ) ) = ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) )
192 50 107 mulcld 
 |-  ( ph -> ( 2 x. _pi ) e. CC )
193 151 107 mulcld 
 |-  ( ph -> ( ( K + ( 1 / 2 ) ) x. _pi ) e. CC )
194 193 sincld 
 |-  ( ph -> ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) e. CC )
195 192 194 mulcomd 
 |-  ( ph -> ( ( 2 x. _pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) = ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) x. ( 2 x. _pi ) ) )
196 195 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 ) ) )
197 191 196 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 ) ) ) )
198 94 a1i 
 |-  ( ph -> _pi =/= 0 )
199 151 107 198 divcan4d 
 |-  ( ph -> ( ( ( K + ( 1 / 2 ) ) x. _pi ) / _pi ) = ( K + ( 1 / 2 ) ) )
200 2 zred 
 |-  ( ph -> K e. RR )
201 69 a1i 
 |-  ( ph -> 2 e. RR+ )
202 201 rpreccld 
 |-  ( ph -> ( 1 / 2 ) e. RR+ )
203 200 202 ltaddrpd 
 |-  ( ph -> K < ( K + ( 1 / 2 ) ) )
204 1red 
 |-  ( ph -> 1 e. RR )
205 204 rehalfcld 
 |-  ( ph -> ( 1 / 2 ) e. RR )
206 halflt1 
 |-  ( 1 / 2 ) < 1
207 206 a1i 
 |-  ( ph -> ( 1 / 2 ) < 1 )
208 205 204 200 207 ltadd2dd 
 |-  ( ph -> ( K + ( 1 / 2 ) ) < ( K + 1 ) )
209 btwnnz 
 |-  ( ( K e. ZZ /\ K < ( K + ( 1 / 2 ) ) /\ ( K + ( 1 / 2 ) ) < ( K + 1 ) ) -> -. ( K + ( 1 / 2 ) ) e. ZZ )
210 2 203 208 209 syl3anc 
 |-  ( ph -> -. ( K + ( 1 / 2 ) ) e. ZZ )
211 199 210 eqneltrd 
 |-  ( ph -> -. ( ( ( K + ( 1 / 2 ) ) x. _pi ) / _pi ) e. ZZ )
212 sineq0 
 |-  ( ( ( K + ( 1 / 2 ) ) x. _pi ) e. CC -> ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) = 0 <-> ( ( ( K + ( 1 / 2 ) ) x. _pi ) / _pi ) e. ZZ ) )
213 193 212 syl 
 |-  ( ph -> ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) = 0 <-> ( ( ( K + ( 1 / 2 ) ) x. _pi ) / _pi ) e. ZZ ) )
214 211 213 mtbird 
 |-  ( ph -> -. ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) = 0 )
215 214 neqned 
 |-  ( ph -> ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) =/= 0 )
216 50 107 52 198 mulne0d 
 |-  ( ph -> ( 2 x. _pi ) =/= 0 )
217 194 194 192 215 216 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 ) ) ) )
218 194 215 dividd 
 |-  ( ph -> ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) = 1 )
219 218 oveq1d 
 |-  ( ph -> ( ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) / ( 2 x. _pi ) ) = ( 1 / ( 2 x. _pi ) ) )
220 217 219 eqtr3d 
 |-  ( ph -> ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) / ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) x. ( 2 x. _pi ) ) ) = ( 1 / ( 2 x. _pi ) ) )
221 220 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 ) ) )
222 197 221 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 ) ) )
223 169 173 222 3eqtrrd 
 |-  ( ( ph /\ ( N mod 2 ) = 0 ) -> ( 1 / ( 2 x. _pi ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( ( 2 x. _pi ) x. ( sin ` ( A / 2 ) ) ) ) )
224 99 223 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 ) ) ) ) )
225 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 ) )
226 145 adantr 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> N e. ZZ )
227 simpr 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> -. ( N mod 2 ) = 0 )
228 227 neqned 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( N mod 2 ) =/= 0 )
229 oddfl 
 |-  ( ( N e. ZZ /\ ( N mod 2 ) =/= 0 ) -> N = ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) )
230 226 228 229 syl2anc 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> N = ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) )
231 230 oveq2d 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( 1 ... N ) = ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) )
232 231 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 ) ) )
233 fvoveq1 
 |-  ( N = 1 -> ( |_ ` ( N / 2 ) ) = ( |_ ` ( 1 / 2 ) ) )
234 halffl 
 |-  ( |_ ` ( 1 / 2 ) ) = 0
235 233 234 eqtrdi 
 |-  ( N = 1 -> ( |_ ` ( N / 2 ) ) = 0 )
236 235 oveq2d 
 |-  ( N = 1 -> ( 2 x. ( |_ ` ( N / 2 ) ) ) = ( 2 x. 0 ) )
237 2t0e0 
 |-  ( 2 x. 0 ) = 0
238 236 237 eqtrdi 
 |-  ( N = 1 -> ( 2 x. ( |_ ` ( N / 2 ) ) ) = 0 )
239 238 oveq1d 
 |-  ( N = 1 -> ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) = ( 0 + 1 ) )
240 90 addid2i 
 |-  ( 0 + 1 ) = 1
241 239 240 eqtrdi 
 |-  ( N = 1 -> ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) = 1 )
242 241 oveq2d 
 |-  ( N = 1 -> ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) = ( 1 ... 1 ) )
243 242 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 ) ) )
244 1z 
 |-  1 e. ZZ
245 coscl 
 |-  ( _pi e. CC -> ( cos ` _pi ) e. CC )
246 15 245 ax-mp 
 |-  ( cos ` _pi ) e. CC
247 oveq2 
 |-  ( n = 1 -> ( _pi x. n ) = ( _pi x. 1 ) )
248 15 mulid1i 
 |-  ( _pi x. 1 ) = _pi
249 247 248 eqtrdi 
 |-  ( n = 1 -> ( _pi x. n ) = _pi )
250 249 fveq2d 
 |-  ( n = 1 -> ( cos ` ( _pi x. n ) ) = ( cos ` _pi ) )
251 250 fsum1 
 |-  ( ( 1 e. ZZ /\ ( cos ` _pi ) e. CC ) -> sum_ n e. ( 1 ... 1 ) ( cos ` ( _pi x. n ) ) = ( cos ` _pi ) )
252 244 246 251 mp2an 
 |-  sum_ n e. ( 1 ... 1 ) ( cos ` ( _pi x. n ) ) = ( cos ` _pi )
253 252 a1i 
 |-  ( N = 1 -> sum_ n e. ( 1 ... 1 ) ( cos ` ( _pi x. n ) ) = ( cos ` _pi ) )
254 cospi 
 |-  ( cos ` _pi ) = -u 1
255 254 a1i 
 |-  ( N = 1 -> ( cos ` _pi ) = -u 1 )
256 243 253 255 3eqtrd 
 |-  ( N = 1 -> sum_ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ( cos ` ( _pi x. n ) ) = -u 1 )
257 256 adantl 
 |-  ( ( ph /\ N = 1 ) -> sum_ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ( cos ` ( _pi x. n ) ) = -u 1 )
258 2nn 
 |-  2 e. NN
259 258 a1i 
 |-  ( ( ph /\ -. N = 1 ) -> 2 e. NN )
260 67 rehalfcld 
 |-  ( ph -> ( N / 2 ) e. RR )
261 260 flcld 
 |-  ( ph -> ( |_ ` ( N / 2 ) ) e. ZZ )
262 261 adantr 
 |-  ( ( ph /\ -. N = 1 ) -> ( |_ ` ( N / 2 ) ) e. ZZ )
263 2div2e1 
 |-  ( 2 / 2 ) = 1
264 73 a1i 
 |-  ( ( ph /\ -. N = 1 ) -> 2 e. RR )
265 67 adantr 
 |-  ( ( ph /\ -. N = 1 ) -> N e. RR )
266 69 a1i 
 |-  ( ( ph /\ -. N = 1 ) -> 2 e. RR+ )
267 neqne 
 |-  ( -. N = 1 -> N =/= 1 )
268 nnne1ge2 
 |-  ( ( N e. NN /\ N =/= 1 ) -> 2 <_ N )
269 1 267 268 syl2an 
 |-  ( ( ph /\ -. N = 1 ) -> 2 <_ N )
270 264 265 266 269 lediv1dd 
 |-  ( ( ph /\ -. N = 1 ) -> ( 2 / 2 ) <_ ( N / 2 ) )
271 263 270 eqbrtrrid 
 |-  ( ( ph /\ -. N = 1 ) -> 1 <_ ( N / 2 ) )
272 260 adantr 
 |-  ( ( ph /\ -. N = 1 ) -> ( N / 2 ) e. RR )
273 flge 
 |-  ( ( ( N / 2 ) e. RR /\ 1 e. ZZ ) -> ( 1 <_ ( N / 2 ) <-> 1 <_ ( |_ ` ( N / 2 ) ) ) )
274 272 244 273 sylancl 
 |-  ( ( ph /\ -. N = 1 ) -> ( 1 <_ ( N / 2 ) <-> 1 <_ ( |_ ` ( N / 2 ) ) ) )
275 271 274 mpbid 
 |-  ( ( ph /\ -. N = 1 ) -> 1 <_ ( |_ ` ( N / 2 ) ) )
276 elnnz1 
 |-  ( ( |_ ` ( N / 2 ) ) e. NN <-> ( ( |_ ` ( N / 2 ) ) e. ZZ /\ 1 <_ ( |_ ` ( N / 2 ) ) ) )
277 262 275 276 sylanbrc 
 |-  ( ( ph /\ -. N = 1 ) -> ( |_ ` ( N / 2 ) ) e. NN )
278 259 277 nnmulcld 
 |-  ( ( ph /\ -. N = 1 ) -> ( 2 x. ( |_ ` ( N / 2 ) ) ) e. NN )
279 nnuz 
 |-  NN = ( ZZ>= ` 1 )
280 278 279 eleqtrdi 
 |-  ( ( ph /\ -. N = 1 ) -> ( 2 x. ( |_ ` ( N / 2 ) ) ) e. ( ZZ>= ` 1 ) )
281 15 a1i 
 |-  ( ( ( ph /\ -. N = 1 ) /\ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) -> _pi e. CC )
282 elfzelz 
 |-  ( n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) -> n e. ZZ )
283 282 zcnd 
 |-  ( n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) -> n e. CC )
284 283 adantl 
 |-  ( ( ( ph /\ -. N = 1 ) /\ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) -> n e. CC )
285 281 284 mulcld 
 |-  ( ( ( ph /\ -. N = 1 ) /\ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) -> ( _pi x. n ) e. CC )
286 285 coscld 
 |-  ( ( ( ph /\ -. N = 1 ) /\ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) -> ( cos ` ( _pi x. n ) ) e. CC )
287 oveq2 
 |-  ( n = ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) -> ( _pi x. n ) = ( _pi x. ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) )
288 287 fveq2d 
 |-  ( n = ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) -> ( cos ` ( _pi x. n ) ) = ( cos ` ( _pi x. ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) )
289 280 286 288 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 ) ) ) ) )
290 15 a1i 
 |-  ( n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) -> _pi e. CC )
291 elfzelz 
 |-  ( n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) -> n e. ZZ )
292 291 zcnd 
 |-  ( n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) -> n e. CC )
293 290 292 mulcomd 
 |-  ( n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) -> ( _pi x. n ) = ( n x. _pi ) )
294 293 fveq2d 
 |-  ( n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) -> ( cos ` ( _pi x. n ) ) = ( cos ` ( n x. _pi ) ) )
295 294 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 ) )
296 dirkertrigeqlem1 
 |-  ( ( |_ ` ( N / 2 ) ) e. NN -> sum_ n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) ( cos ` ( n x. _pi ) ) = 0 )
297 277 296 syl 
 |-  ( ( ph /\ -. N = 1 ) -> sum_ n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) ( cos ` ( n x. _pi ) ) = 0 )
298 295 297 syl5eq 
 |-  ( ( ph /\ -. N = 1 ) -> sum_ n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) ( cos ` ( _pi x. n ) ) = 0 )
299 261 zcnd 
 |-  ( ph -> ( |_ ` ( N / 2 ) ) e. CC )
300 50 299 mulcld 
 |-  ( ph -> ( 2 x. ( |_ ` ( N / 2 ) ) ) e. CC )
301 107 300 109 adddid 
 |-  ( ph -> ( _pi x. ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) = ( ( _pi x. ( 2 x. ( |_ ` ( N / 2 ) ) ) ) + ( _pi x. 1 ) ) )
302 107 50 299 mul13d 
 |-  ( ph -> ( _pi x. ( 2 x. ( |_ ` ( N / 2 ) ) ) ) = ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) )
303 248 a1i 
 |-  ( ph -> ( _pi x. 1 ) = _pi )
304 302 303 oveq12d 
 |-  ( ph -> ( ( _pi x. ( 2 x. ( |_ ` ( N / 2 ) ) ) ) + ( _pi x. 1 ) ) = ( ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) + _pi ) )
305 299 192 mulcld 
 |-  ( ph -> ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) e. CC )
306 305 107 addcomd 
 |-  ( ph -> ( ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) + _pi ) = ( _pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) )
307 301 304 306 3eqtrd 
 |-  ( ph -> ( _pi x. ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) = ( _pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) )
308 307 fveq2d 
 |-  ( ph -> ( cos ` ( _pi x. ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) = ( cos ` ( _pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) ) )
309 cosper 
 |-  ( ( _pi e. CC /\ ( |_ ` ( N / 2 ) ) e. ZZ ) -> ( cos ` ( _pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) ) = ( cos ` _pi ) )
310 107 261 309 syl2anc 
 |-  ( ph -> ( cos ` ( _pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) ) = ( cos ` _pi ) )
311 254 a1i 
 |-  ( ph -> ( cos ` _pi ) = -u 1 )
312 308 310 311 3eqtrd 
 |-  ( ph -> ( cos ` ( _pi x. ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) = -u 1 )
313 312 adantr 
 |-  ( ( ph /\ -. N = 1 ) -> ( cos ` ( _pi x. ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) = -u 1 )
314 298 313 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 ) )
315 neg1cn 
 |-  -u 1 e. CC
316 315 addid2i 
 |-  ( 0 + -u 1 ) = -u 1
317 316 a1i 
 |-  ( ( ph /\ -. N = 1 ) -> ( 0 + -u 1 ) = -u 1 )
318 289 314 317 3eqtrd 
 |-  ( ( ph /\ -. N = 1 ) -> sum_ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ( cos ` ( _pi x. n ) ) = -u 1 )
319 257 318 pm2.61dan 
 |-  ( ph -> sum_ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ( cos ` ( _pi x. n ) ) = -u 1 )
320 319 adantr 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> sum_ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ( cos ` ( _pi x. n ) ) = -u 1 )
321 232 320 eqtrd 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> sum_ n e. ( 1 ... N ) ( cos ` ( _pi x. n ) ) = -u 1 )
322 321 oveq2d 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( _pi x. n ) ) ) = ( ( 1 / 2 ) + -u 1 ) )
323 322 oveq1d 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( _pi x. n ) ) ) / _pi ) = ( ( ( 1 / 2 ) + -u 1 ) / _pi ) )
324 168 172 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 ) ) ) ) )
325 324 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 ) ) ) ) )
326 230 oveq1d 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( N x. _pi ) = ( ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) x. _pi ) )
327 300 109 107 adddird 
 |-  ( ph -> ( ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) x. _pi ) = ( ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. _pi ) + ( 1 x. _pi ) ) )
328 107 mulid2d 
 |-  ( ph -> ( 1 x. _pi ) = _pi )
329 328 oveq2d 
 |-  ( ph -> ( ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. _pi ) + ( 1 x. _pi ) ) = ( ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. _pi ) + _pi ) )
330 300 107 mulcld 
 |-  ( ph -> ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. _pi ) e. CC )
331 330 107 addcomd 
 |-  ( ph -> ( ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. _pi ) + _pi ) = ( _pi + ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. _pi ) ) )
332 327 329 331 3eqtrd 
 |-  ( ph -> ( ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) x. _pi ) = ( _pi + ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. _pi ) ) )
333 332 adantr 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) x. _pi ) = ( _pi + ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. _pi ) ) )
334 50 299 mulcomd 
 |-  ( ph -> ( 2 x. ( |_ ` ( N / 2 ) ) ) = ( ( |_ ` ( N / 2 ) ) x. 2 ) )
335 334 oveq1d 
 |-  ( ph -> ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. _pi ) = ( ( ( |_ ` ( N / 2 ) ) x. 2 ) x. _pi ) )
336 299 50 107 mulassd 
 |-  ( ph -> ( ( ( |_ ` ( N / 2 ) ) x. 2 ) x. _pi ) = ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) )
337 335 336 eqtrd 
 |-  ( ph -> ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. _pi ) = ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) )
338 337 oveq2d 
 |-  ( ph -> ( _pi + ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. _pi ) ) = ( _pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) )
339 338 adantr 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( _pi + ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. _pi ) ) = ( _pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) )
340 326 333 339 3eqtrd 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( N x. _pi ) = ( _pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) )
341 340 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 ) ) ) ) )
342 193 adantr 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( K + ( 1 / 2 ) ) x. _pi ) e. CC )
343 15 a1i 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> _pi e. CC )
344 305 adantr 
 |-  ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) e. CC )
345 342 343 344 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 ) ) ) ) )
346 341 345 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 ) ) ) )
347 346 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 ) ) ) ) )
348 347 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 ) ) ) ) )
349 193 107 addcld 
 |-  ( ph -> ( ( ( K + ( 1 / 2 ) ) x. _pi ) + _pi ) e. CC )
350 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 ) ) )
351 349 261 350 syl2anc 
 |-  ( ph -> ( sin ` ( ( ( ( K + ( 1 / 2 ) ) x. _pi ) + _pi ) + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) ) = ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + _pi ) ) )
352 sinppi 
 |-  ( ( ( K + ( 1 / 2 ) ) x. _pi ) e. CC -> ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + _pi ) ) = -u ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) )
353 193 352 syl 
 |-  ( ph -> ( sin ` ( ( ( K + ( 1 / 2 ) ) x. _pi ) + _pi ) ) = -u ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) )
354 351 353 eqtrd 
 |-  ( ph -> ( sin ` ( ( ( ( K + ( 1 / 2 ) ) x. _pi ) + _pi ) + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. _pi ) ) ) ) = -u ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) )
355 354 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 ) ) ) ) )
356 195 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 ) ) ) )
357 194 194 215 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 ) ) ) )
358 218 negeqd 
 |-  ( ph -> -u ( ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) = -u 1 )
359 357 358 eqtr3d 
 |-  ( ph -> ( -u ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) = -u 1 )
360 359 oveq1d 
 |-  ( ph -> ( ( -u ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) ) / ( 2 x. _pi ) ) = ( -u 1 / ( 2 x. _pi ) ) )
361 194 negcld 
 |-  ( ph -> -u ( sin ` ( ( K + ( 1 / 2 ) ) x. _pi ) ) e. CC )
362 361 194 192 215 216 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 ) ) ) )
363 86 90 negsubi 
 |-  ( ( 1 / 2 ) + -u 1 ) = ( ( 1 / 2 ) - 1 )
364 90 86 negsubdi2i 
 |-  -u ( 1 - ( 1 / 2 ) ) = ( ( 1 / 2 ) - 1 )
365 1mhlfehlf 
 |-  ( 1 - ( 1 / 2 ) ) = ( 1 / 2 )
366 365 negeqi 
 |-  -u ( 1 - ( 1 / 2 ) ) = -u ( 1 / 2 )
367 divneg 
 |-  ( ( 1 e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> -u ( 1 / 2 ) = ( -u 1 / 2 ) )
368 90 118 51 367 mp3an 
 |-  -u ( 1 / 2 ) = ( -u 1 / 2 )
369 366 368 eqtri 
 |-  -u ( 1 - ( 1 / 2 ) ) = ( -u 1 / 2 )
370 363 364 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 315 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 360 362 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 355 356 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 325 348 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 225 323 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 224 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 ) ) ) ) )