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 ( 𝐾 ∈ ℕ → Σ 𝑛 ∈ ( 1 ... ( 2 · 𝐾 ) ) ( cos ‘ ( 𝑛 · π ) ) = 0 )

Proof

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