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