Metamath Proof Explorer

Theorem dirkertrigeqlem1

Description: Sum of an even number of alternating cos values. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion dirkertrigeqlem1 
|- ( K e. NN -> sum_ n e. ( 1 ... ( 2 x. K ) ) ( cos ` ( n x. _pi ) ) = 0 )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = 1 -> ( 2 x. x ) = ( 2 x. 1 ) )
2 1 oveq2d 
 |-  ( x = 1 -> ( 1 ... ( 2 x. x ) ) = ( 1 ... ( 2 x. 1 ) ) )
3 2 sumeq1d 
 |-  ( x = 1 -> sum_ n e. ( 1 ... ( 2 x. x ) ) ( cos ` ( n x. _pi ) ) = sum_ n e. ( 1 ... ( 2 x. 1 ) ) ( cos ` ( n x. _pi ) ) )
4 3 eqeq1d 
 |-  ( x = 1 -> ( sum_ n e. ( 1 ... ( 2 x. x ) ) ( cos ` ( n x. _pi ) ) = 0 <-> sum_ n e. ( 1 ... ( 2 x. 1 ) ) ( cos ` ( n x. _pi ) ) = 0 ) )
5 oveq2 
 |-  ( x = y -> ( 2 x. x ) = ( 2 x. y ) )
6 5 oveq2d 
 |-  ( x = y -> ( 1 ... ( 2 x. x ) ) = ( 1 ... ( 2 x. y ) ) )
7 6 sumeq1d 
 |-  ( x = y -> sum_ n e. ( 1 ... ( 2 x. x ) ) ( cos ` ( n x. _pi ) ) = sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. _pi ) ) )
8 7 eqeq1d 
 |-  ( x = y -> ( sum_ n e. ( 1 ... ( 2 x. x ) ) ( cos ` ( n x. _pi ) ) = 0 <-> sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. _pi ) ) = 0 ) )
9 oveq2 
 |-  ( x = ( y + 1 ) -> ( 2 x. x ) = ( 2 x. ( y + 1 ) ) )
10 9 oveq2d 
 |-  ( x = ( y + 1 ) -> ( 1 ... ( 2 x. x ) ) = ( 1 ... ( 2 x. ( y + 1 ) ) ) )
11 10 sumeq1d 
 |-  ( x = ( y + 1 ) -> sum_ n e. ( 1 ... ( 2 x. x ) ) ( cos ` ( n x. _pi ) ) = sum_ n e. ( 1 ... ( 2 x. ( y + 1 ) ) ) ( cos ` ( n x. _pi ) ) )
12 11 eqeq1d 
 |-  ( x = ( y + 1 ) -> ( sum_ n e. ( 1 ... ( 2 x. x ) ) ( cos ` ( n x. _pi ) ) = 0 <-> sum_ n e. ( 1 ... ( 2 x. ( y + 1 ) ) ) ( cos ` ( n x. _pi ) ) = 0 ) )
13 oveq2 
 |-  ( x = K -> ( 2 x. x ) = ( 2 x. K ) )
14 13 oveq2d 
 |-  ( x = K -> ( 1 ... ( 2 x. x ) ) = ( 1 ... ( 2 x. K ) ) )
15 14 sumeq1d 
 |-  ( x = K -> sum_ n e. ( 1 ... ( 2 x. x ) ) ( cos ` ( n x. _pi ) ) = sum_ n e. ( 1 ... ( 2 x. K ) ) ( cos ` ( n x. _pi ) ) )
16 15 eqeq1d 
 |-  ( x = K -> ( sum_ n e. ( 1 ... ( 2 x. x ) ) ( cos ` ( n x. _pi ) ) = 0 <-> sum_ n e. ( 1 ... ( 2 x. K ) ) ( cos ` ( n x. _pi ) ) = 0 ) )
17 ax-1cn 
 |-  1 e. CC
18 17 2timesi 
 |-  ( 2 x. 1 ) = ( 1 + 1 )
19 18 oveq2i 
 |-  ( 1 ... ( 2 x. 1 ) ) = ( 1 ... ( 1 + 1 ) )
20 19 sumeq1i 
 |-  sum_ n e. ( 1 ... ( 2 x. 1 ) ) ( cos ` ( n x. _pi ) ) = sum_ n e. ( 1 ... ( 1 + 1 ) ) ( cos ` ( n x. _pi ) )
21 1z 
 |-  1 e. ZZ
22 uzid 
 |-  ( 1 e. ZZ -> 1 e. ( ZZ>= ` 1 ) )
23 21 22 ax-mp 
 |-  1 e. ( ZZ>= ` 1 )
24 23 a1i 
 |-  ( T. -> 1 e. ( ZZ>= ` 1 ) )
25 elfzelz 
 |-  ( n e. ( 1 ... ( 1 + 1 ) ) -> n e. ZZ )
26 25 zcnd 
 |-  ( n e. ( 1 ... ( 1 + 1 ) ) -> n e. CC )
27 26 adantl 
 |-  ( ( T. /\ n e. ( 1 ... ( 1 + 1 ) ) ) -> n e. CC )
28 picn 
 |-  _pi e. CC
29 28 a1i 
 |-  ( ( T. /\ n e. ( 1 ... ( 1 + 1 ) ) ) -> _pi e. CC )
30 27 29 mulcld 
 |-  ( ( T. /\ n e. ( 1 ... ( 1 + 1 ) ) ) -> ( n x. _pi ) e. CC )
31 30 coscld 
 |-  ( ( T. /\ n e. ( 1 ... ( 1 + 1 ) ) ) -> ( cos ` ( n x. _pi ) ) e. CC )
32 id 
 |-  ( n = ( 1 + 1 ) -> n = ( 1 + 1 ) )
33 1p1e2 
 |-  ( 1 + 1 ) = 2
34 32 33 eqtrdi 
 |-  ( n = ( 1 + 1 ) -> n = 2 )
35 34 fvoveq1d 
 |-  ( n = ( 1 + 1 ) -> ( cos ` ( n x. _pi ) ) = ( cos ` ( 2 x. _pi ) ) )
36 24 31 35 fsump1 
 |-  ( T. -> sum_ n e. ( 1 ... ( 1 + 1 ) ) ( cos ` ( n x. _pi ) ) = ( sum_ n e. ( 1 ... 1 ) ( cos ` ( n x. _pi ) ) + ( cos ` ( 2 x. _pi ) ) ) )
37 36 mptru 
 |-  sum_ n e. ( 1 ... ( 1 + 1 ) ) ( cos ` ( n x. _pi ) ) = ( sum_ n e. ( 1 ... 1 ) ( cos ` ( n x. _pi ) ) + ( cos ` ( 2 x. _pi ) ) )
38 coscl 
 |-  ( _pi e. CC -> ( cos ` _pi ) e. CC )
39 28 38 ax-mp 
 |-  ( cos ` _pi ) e. CC
40 oveq1 
 |-  ( n = 1 -> ( n x. _pi ) = ( 1 x. _pi ) )
41 28 mulid2i 
 |-  ( 1 x. _pi ) = _pi
42 40 41 eqtrdi 
 |-  ( n = 1 -> ( n x. _pi ) = _pi )
43 42 fveq2d 
 |-  ( n = 1 -> ( cos ` ( n x. _pi ) ) = ( cos ` _pi ) )
44 43 fsum1 
 |-  ( ( 1 e. ZZ /\ ( cos ` _pi ) e. CC ) -> sum_ n e. ( 1 ... 1 ) ( cos ` ( n x. _pi ) ) = ( cos ` _pi ) )
45 21 39 44 mp2an 
 |-  sum_ n e. ( 1 ... 1 ) ( cos ` ( n x. _pi ) ) = ( cos ` _pi )
46 cospi 
 |-  ( cos ` _pi ) = -u 1
47 45 46 eqtri 
 |-  sum_ n e. ( 1 ... 1 ) ( cos ` ( n x. _pi ) ) = -u 1
48 cos2pi 
 |-  ( cos ` ( 2 x. _pi ) ) = 1
49 47 48 oveq12i 
 |-  ( sum_ n e. ( 1 ... 1 ) ( cos ` ( n x. _pi ) ) + ( cos ` ( 2 x. _pi ) ) ) = ( -u 1 + 1 )
50 neg1cn 
 |-  -u 1 e. CC
51 1pneg1e0 
 |-  ( 1 + -u 1 ) = 0
52 17 50 51 addcomli 
 |-  ( -u 1 + 1 ) = 0
53 37 49 52 3eqtri 
 |-  sum_ n e. ( 1 ... ( 1 + 1 ) ) ( cos ` ( n x. _pi ) ) = 0
54 20 53 eqtri 
 |-  sum_ n e. ( 1 ... ( 2 x. 1 ) ) ( cos ` ( n x. _pi ) ) = 0
55 18 oveq2i 
 |-  ( ( 2 x. y ) + ( 2 x. 1 ) ) = ( ( 2 x. y ) + ( 1 + 1 ) )
56 2cnd 
 |-  ( y e. NN -> 2 e. CC )
57 nncn 
 |-  ( y e. NN -> y e. CC )
58 17 a1i 
 |-  ( y e. NN -> 1 e. CC )
59 56 57 58 adddid 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) = ( ( 2 x. y ) + ( 2 x. 1 ) ) )
60 56 57 mulcld 
 |-  ( y e. NN -> ( 2 x. y ) e. CC )
61 60 58 58 addassd 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 1 ) + 1 ) = ( ( 2 x. y ) + ( 1 + 1 ) ) )
62 55 59 61 3eqtr4a 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) = ( ( ( 2 x. y ) + 1 ) + 1 ) )
63 62 oveq2d 
 |-  ( y e. NN -> ( 1 ... ( 2 x. ( y + 1 ) ) ) = ( 1 ... ( ( ( 2 x. y ) + 1 ) + 1 ) ) )
64 63 sumeq1d 
 |-  ( y e. NN -> sum_ n e. ( 1 ... ( 2 x. ( y + 1 ) ) ) ( cos ` ( n x. _pi ) ) = sum_ n e. ( 1 ... ( ( ( 2 x. y ) + 1 ) + 1 ) ) ( cos ` ( n x. _pi ) ) )
65 64 adantr 
 |-  ( ( y e. NN /\ sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. _pi ) ) = 0 ) -> sum_ n e. ( 1 ... ( 2 x. ( y + 1 ) ) ) ( cos ` ( n x. _pi ) ) = sum_ n e. ( 1 ... ( ( ( 2 x. y ) + 1 ) + 1 ) ) ( cos ` ( n x. _pi ) ) )
66 1red 
 |-  ( y e. NN -> 1 e. RR )
67 2re 
 |-  2 e. RR
68 67 a1i 
 |-  ( y e. NN -> 2 e. RR )
69 nnre 
 |-  ( y e. NN -> y e. RR )
70 68 69 remulcld 
 |-  ( y e. NN -> ( 2 x. y ) e. RR )
71 70 66 readdcld 
 |-  ( y e. NN -> ( ( 2 x. y ) + 1 ) e. RR )
72 2rp 
 |-  2 e. RR+
73 72 a1i 
 |-  ( y e. NN -> 2 e. RR+ )
74 nnrp 
 |-  ( y e. NN -> y e. RR+ )
75 73 74 rpmulcld 
 |-  ( y e. NN -> ( 2 x. y ) e. RR+ )
76 66 75 ltaddrp2d 
 |-  ( y e. NN -> 1 < ( ( 2 x. y ) + 1 ) )
77 66 71 76 ltled 
 |-  ( y e. NN -> 1 <_ ( ( 2 x. y ) + 1 ) )
78 2z 
 |-  2 e. ZZ
79 78 a1i 
 |-  ( y e. NN -> 2 e. ZZ )
80 nnz 
 |-  ( y e. NN -> y e. ZZ )
81 79 80 zmulcld 
 |-  ( y e. NN -> ( 2 x. y ) e. ZZ )
82 81 peano2zd 
 |-  ( y e. NN -> ( ( 2 x. y ) + 1 ) e. ZZ )
83 eluz 
 |-  ( ( 1 e. ZZ /\ ( ( 2 x. y ) + 1 ) e. ZZ ) -> ( ( ( 2 x. y ) + 1 ) e. ( ZZ>= ` 1 ) <-> 1 <_ ( ( 2 x. y ) + 1 ) ) )
84 21 82 83 sylancr 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 1 ) e. ( ZZ>= ` 1 ) <-> 1 <_ ( ( 2 x. y ) + 1 ) ) )
85 77 84 mpbird 
 |-  ( y e. NN -> ( ( 2 x. y ) + 1 ) e. ( ZZ>= ` 1 ) )
86 elfzelz 
 |-  ( n e. ( 1 ... ( ( ( 2 x. y ) + 1 ) + 1 ) ) -> n e. ZZ )
87 86 zcnd 
 |-  ( n e. ( 1 ... ( ( ( 2 x. y ) + 1 ) + 1 ) ) -> n e. CC )
88 28 a1i 
 |-  ( n e. ( 1 ... ( ( ( 2 x. y ) + 1 ) + 1 ) ) -> _pi e. CC )
89 87 88 mulcld 
 |-  ( n e. ( 1 ... ( ( ( 2 x. y ) + 1 ) + 1 ) ) -> ( n x. _pi ) e. CC )
90 89 coscld 
 |-  ( n e. ( 1 ... ( ( ( 2 x. y ) + 1 ) + 1 ) ) -> ( cos ` ( n x. _pi ) ) e. CC )
91 90 adantl 
 |-  ( ( y e. NN /\ n e. ( 1 ... ( ( ( 2 x. y ) + 1 ) + 1 ) ) ) -> ( cos ` ( n x. _pi ) ) e. CC )
92 fvoveq1 
 |-  ( n = ( ( ( 2 x. y ) + 1 ) + 1 ) -> ( cos ` ( n x. _pi ) ) = ( cos ` ( ( ( ( 2 x. y ) + 1 ) + 1 ) x. _pi ) ) )
93 85 91 92 fsump1 
 |-  ( y e. NN -> sum_ n e. ( 1 ... ( ( ( 2 x. y ) + 1 ) + 1 ) ) ( cos ` ( n x. _pi ) ) = ( sum_ n e. ( 1 ... ( ( 2 x. y ) + 1 ) ) ( cos ` ( n x. _pi ) ) + ( cos ` ( ( ( ( 2 x. y ) + 1 ) + 1 ) x. _pi ) ) ) )
94 93 adantr 
 |-  ( ( y e. NN /\ sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. _pi ) ) = 0 ) -> sum_ n e. ( 1 ... ( ( ( 2 x. y ) + 1 ) + 1 ) ) ( cos ` ( n x. _pi ) ) = ( sum_ n e. ( 1 ... ( ( 2 x. y ) + 1 ) ) ( cos ` ( n x. _pi ) ) + ( cos ` ( ( ( ( 2 x. y ) + 1 ) + 1 ) x. _pi ) ) ) )
95 1lt2 
 |-  1 < 2
96 95 a1i 
 |-  ( y e. NN -> 1 < 2 )
97 2t1e2 
 |-  ( 2 x. 1 ) = 2
98 nnge1 
 |-  ( y e. NN -> 1 <_ y )
99 66 69 73 lemul2d 
 |-  ( y e. NN -> ( 1 <_ y <-> ( 2 x. 1 ) <_ ( 2 x. y ) ) )
100 98 99 mpbid 
 |-  ( y e. NN -> ( 2 x. 1 ) <_ ( 2 x. y ) )
101 97 100 eqbrtrrid 
 |-  ( y e. NN -> 2 <_ ( 2 x. y ) )
102 66 68 70 96 101 ltletrd 
 |-  ( y e. NN -> 1 < ( 2 x. y ) )
103 66 70 102 ltled 
 |-  ( y e. NN -> 1 <_ ( 2 x. y ) )
104 eluz 
 |-  ( ( 1 e. ZZ /\ ( 2 x. y ) e. ZZ ) -> ( ( 2 x. y ) e. ( ZZ>= ` 1 ) <-> 1 <_ ( 2 x. y ) ) )
105 21 81 104 sylancr 
 |-  ( y e. NN -> ( ( 2 x. y ) e. ( ZZ>= ` 1 ) <-> 1 <_ ( 2 x. y ) ) )
106 103 105 mpbird 
 |-  ( y e. NN -> ( 2 x. y ) e. ( ZZ>= ` 1 ) )
107 elfzelz 
 |-  ( n e. ( 1 ... ( ( 2 x. y ) + 1 ) ) -> n e. ZZ )
108 107 zcnd 
 |-  ( n e. ( 1 ... ( ( 2 x. y ) + 1 ) ) -> n e. CC )
109 28 a1i 
 |-  ( n e. ( 1 ... ( ( 2 x. y ) + 1 ) ) -> _pi e. CC )
110 108 109 mulcld 
 |-  ( n e. ( 1 ... ( ( 2 x. y ) + 1 ) ) -> ( n x. _pi ) e. CC )
111 110 coscld 
 |-  ( n e. ( 1 ... ( ( 2 x. y ) + 1 ) ) -> ( cos ` ( n x. _pi ) ) e. CC )
112 111 adantl 
 |-  ( ( y e. NN /\ n e. ( 1 ... ( ( 2 x. y ) + 1 ) ) ) -> ( cos ` ( n x. _pi ) ) e. CC )
113 fvoveq1 
 |-  ( n = ( ( 2 x. y ) + 1 ) -> ( cos ` ( n x. _pi ) ) = ( cos ` ( ( ( 2 x. y ) + 1 ) x. _pi ) ) )
114 106 112 113 fsump1 
 |-  ( y e. NN -> sum_ n e. ( 1 ... ( ( 2 x. y ) + 1 ) ) ( cos ` ( n x. _pi ) ) = ( sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. _pi ) ) + ( cos ` ( ( ( 2 x. y ) + 1 ) x. _pi ) ) ) )
115 33 97 eqtr4i 
 |-  ( 1 + 1 ) = ( 2 x. 1 )
116 115 a1i 
 |-  ( y e. NN -> ( 1 + 1 ) = ( 2 x. 1 ) )
117 116 oveq2d 
 |-  ( y e. NN -> ( ( 2 x. y ) + ( 1 + 1 ) ) = ( ( 2 x. y ) + ( 2 x. 1 ) ) )
118 117 61 59 3eqtr4d 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 1 ) + 1 ) = ( 2 x. ( y + 1 ) ) )
119 118 fvoveq1d 
 |-  ( y e. NN -> ( cos ` ( ( ( ( 2 x. y ) + 1 ) + 1 ) x. _pi ) ) = ( cos ` ( ( 2 x. ( y + 1 ) ) x. _pi ) ) )
120 57 58 addcld 
 |-  ( y e. NN -> ( y + 1 ) e. CC )
121 28 a1i 
 |-  ( y e. NN -> _pi e. CC )
122 56 120 121 mulassd 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) x. _pi ) = ( 2 x. ( ( y + 1 ) x. _pi ) ) )
123 122 oveq1d 
 |-  ( y e. NN -> ( ( ( 2 x. ( y + 1 ) ) x. _pi ) / ( 2 x. _pi ) ) = ( ( 2 x. ( ( y + 1 ) x. _pi ) ) / ( 2 x. _pi ) ) )
124 120 121 mulcld 
 |-  ( y e. NN -> ( ( y + 1 ) x. _pi ) e. CC )
125 0re 
 |-  0 e. RR
126 pipos 
 |-  0 < _pi
127 125 126 gtneii 
 |-  _pi =/= 0
128 127 a1i 
 |-  ( y e. NN -> _pi =/= 0 )
129 73 rpne0d 
 |-  ( y e. NN -> 2 =/= 0 )
130 124 121 56 128 129 divcan5d 
 |-  ( y e. NN -> ( ( 2 x. ( ( y + 1 ) x. _pi ) ) / ( 2 x. _pi ) ) = ( ( ( y + 1 ) x. _pi ) / _pi ) )
131 120 121 128 divcan4d 
 |-  ( y e. NN -> ( ( ( y + 1 ) x. _pi ) / _pi ) = ( y + 1 ) )
132 123 130 131 3eqtrd 
 |-  ( y e. NN -> ( ( ( 2 x. ( y + 1 ) ) x. _pi ) / ( 2 x. _pi ) ) = ( y + 1 ) )
133 80 peano2zd 
 |-  ( y e. NN -> ( y + 1 ) e. ZZ )
134 132 133 eqeltrd 
 |-  ( y e. NN -> ( ( ( 2 x. ( y + 1 ) ) x. _pi ) / ( 2 x. _pi ) ) e. ZZ )
135 peano2cn 
 |-  ( y e. CC -> ( y + 1 ) e. CC )
136 57 135 syl 
 |-  ( y e. NN -> ( y + 1 ) e. CC )
137 56 136 mulcld 
 |-  ( y e. NN -> ( 2 x. ( y + 1 ) ) e. CC )
138 137 121 mulcld 
 |-  ( y e. NN -> ( ( 2 x. ( y + 1 ) ) x. _pi ) e. CC )
139 coseq1 
 |-  ( ( ( 2 x. ( y + 1 ) ) x. _pi ) e. CC -> ( ( cos ` ( ( 2 x. ( y + 1 ) ) x. _pi ) ) = 1 <-> ( ( ( 2 x. ( y + 1 ) ) x. _pi ) / ( 2 x. _pi ) ) e. ZZ ) )
140 138 139 syl 
 |-  ( y e. NN -> ( ( cos ` ( ( 2 x. ( y + 1 ) ) x. _pi ) ) = 1 <-> ( ( ( 2 x. ( y + 1 ) ) x. _pi ) / ( 2 x. _pi ) ) e. ZZ ) )
141 134 140 mpbird 
 |-  ( y e. NN -> ( cos ` ( ( 2 x. ( y + 1 ) ) x. _pi ) ) = 1 )
142 119 141 eqtrd 
 |-  ( y e. NN -> ( cos ` ( ( ( ( 2 x. y ) + 1 ) + 1 ) x. _pi ) ) = 1 )
143 114 142 oveq12d 
 |-  ( y e. NN -> ( sum_ n e. ( 1 ... ( ( 2 x. y ) + 1 ) ) ( cos ` ( n x. _pi ) ) + ( cos ` ( ( ( ( 2 x. y ) + 1 ) + 1 ) x. _pi ) ) ) = ( ( sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. _pi ) ) + ( cos ` ( ( ( 2 x. y ) + 1 ) x. _pi ) ) ) + 1 ) )
144 143 adantr 
 |-  ( ( y e. NN /\ sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. _pi ) ) = 0 ) -> ( sum_ n e. ( 1 ... ( ( 2 x. y ) + 1 ) ) ( cos ` ( n x. _pi ) ) + ( cos ` ( ( ( ( 2 x. y ) + 1 ) + 1 ) x. _pi ) ) ) = ( ( sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. _pi ) ) + ( cos ` ( ( ( 2 x. y ) + 1 ) x. _pi ) ) ) + 1 ) )
145 simpr 
 |-  ( ( y e. NN /\ sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. _pi ) ) = 0 ) -> sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. _pi ) ) = 0 )
146 60 58 121 adddird 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 1 ) x. _pi ) = ( ( ( 2 x. y ) x. _pi ) + ( 1 x. _pi ) ) )
147 60 121 mulcld 
 |-  ( y e. NN -> ( ( 2 x. y ) x. _pi ) e. CC )
148 41 121 eqeltrid 
 |-  ( y e. NN -> ( 1 x. _pi ) e. CC )
149 147 148 addcomd 
 |-  ( y e. NN -> ( ( ( 2 x. y ) x. _pi ) + ( 1 x. _pi ) ) = ( ( 1 x. _pi ) + ( ( 2 x. y ) x. _pi ) ) )
150 41 a1i 
 |-  ( y e. NN -> ( 1 x. _pi ) = _pi )
151 56 57 mulcomd 
 |-  ( y e. NN -> ( 2 x. y ) = ( y x. 2 ) )
152 151 oveq1d 
 |-  ( y e. NN -> ( ( 2 x. y ) x. _pi ) = ( ( y x. 2 ) x. _pi ) )
153 57 56 121 mulassd 
 |-  ( y e. NN -> ( ( y x. 2 ) x. _pi ) = ( y x. ( 2 x. _pi ) ) )
154 152 153 eqtrd 
 |-  ( y e. NN -> ( ( 2 x. y ) x. _pi ) = ( y x. ( 2 x. _pi ) ) )
155 150 154 oveq12d 
 |-  ( y e. NN -> ( ( 1 x. _pi ) + ( ( 2 x. y ) x. _pi ) ) = ( _pi + ( y x. ( 2 x. _pi ) ) ) )
156 146 149 155 3eqtrd 
 |-  ( y e. NN -> ( ( ( 2 x. y ) + 1 ) x. _pi ) = ( _pi + ( y x. ( 2 x. _pi ) ) ) )
157 156 fveq2d 
 |-  ( y e. NN -> ( cos ` ( ( ( 2 x. y ) + 1 ) x. _pi ) ) = ( cos ` ( _pi + ( y x. ( 2 x. _pi ) ) ) ) )
158 cosper 
 |-  ( ( _pi e. CC /\ y e. ZZ ) -> ( cos ` ( _pi + ( y x. ( 2 x. _pi ) ) ) ) = ( cos ` _pi ) )
159 28 80 158 sylancr 
 |-  ( y e. NN -> ( cos ` ( _pi + ( y x. ( 2 x. _pi ) ) ) ) = ( cos ` _pi ) )
160 46 a1i 
 |-  ( y e. NN -> ( cos ` _pi ) = -u 1 )
161 157 159 160 3eqtrd 
 |-  ( y e. NN -> ( cos ` ( ( ( 2 x. y ) + 1 ) x. _pi ) ) = -u 1 )
162 161 adantr 
 |-  ( ( y e. NN /\ sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. _pi ) ) = 0 ) -> ( cos ` ( ( ( 2 x. y ) + 1 ) x. _pi ) ) = -u 1 )
163 145 162 oveq12d 
 |-  ( ( y e. NN /\ sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. _pi ) ) = 0 ) -> ( sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. _pi ) ) + ( cos ` ( ( ( 2 x. y ) + 1 ) x. _pi ) ) ) = ( 0 + -u 1 ) )
164 163 oveq1d 
 |-  ( ( y e. NN /\ sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. _pi ) ) = 0 ) -> ( ( sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. _pi ) ) + ( cos ` ( ( ( 2 x. y ) + 1 ) x. _pi ) ) ) + 1 ) = ( ( 0 + -u 1 ) + 1 ) )
165 50 addid2i 
 |-  ( 0 + -u 1 ) = -u 1
166 165 oveq1i 
 |-  ( ( 0 + -u 1 ) + 1 ) = ( -u 1 + 1 )
167 166 52 eqtri 
 |-  ( ( 0 + -u 1 ) + 1 ) = 0
168 164 167 eqtrdi 
 |-  ( ( y e. NN /\ sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. _pi ) ) = 0 ) -> ( ( sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. _pi ) ) + ( cos ` ( ( ( 2 x. y ) + 1 ) x. _pi ) ) ) + 1 ) = 0 )
169 144 168 eqtrd 
 |-  ( ( y e. NN /\ sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. _pi ) ) = 0 ) -> ( sum_ n e. ( 1 ... ( ( 2 x. y ) + 1 ) ) ( cos ` ( n x. _pi ) ) + ( cos ` ( ( ( ( 2 x. y ) + 1 ) + 1 ) x. _pi ) ) ) = 0 )
170 65 94 169 3eqtrd 
 |-  ( ( y e. NN /\ sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. _pi ) ) = 0 ) -> sum_ n e. ( 1 ... ( 2 x. ( y + 1 ) ) ) ( cos ` ( n x. _pi ) ) = 0 )
171 170 ex 
 |-  ( y e. NN -> ( sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. _pi ) ) = 0 -> sum_ n e. ( 1 ... ( 2 x. ( y + 1 ) ) ) ( cos ` ( n x. _pi ) ) = 0 ) )
172 4 8 12 16 54 171 nnind 
 |-  ( K e. NN -> sum_ n e. ( 1 ... ( 2 x. K ) ) ( cos ` ( n x. _pi ) ) = 0 )