Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dirkertrigeqlem1 Structured version   Visualization version   GIF version

Theorem dirkertrigeqlem1 41252
Description: Sum of an even number of alternating cos values. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Assertion
Ref Expression
dirkertrigeqlem1 (𝐾 ∈ ℕ → Σ𝑛 ∈ (1...(2 · 𝐾))(cos‘(𝑛 · π)) = 0)
Distinct variable group:   𝑛,𝐾

Proof of Theorem dirkertrigeqlem1
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 6932 . . . . 5 (𝑥 = 1 → (2 · 𝑥) = (2 · 1))
21oveq2d 6940 . . . 4 (𝑥 = 1 → (1...(2 · 𝑥)) = (1...(2 · 1)))
32sumeq1d 14843 . . 3 (𝑥 = 1 → Σ𝑛 ∈ (1...(2 · 𝑥))(cos‘(𝑛 · π)) = Σ𝑛 ∈ (1...(2 · 1))(cos‘(𝑛 · π)))
43eqeq1d 2780 . 2 (𝑥 = 1 → (Σ𝑛 ∈ (1...(2 · 𝑥))(cos‘(𝑛 · π)) = 0 ↔ Σ𝑛 ∈ (1...(2 · 1))(cos‘(𝑛 · π)) = 0))
5 oveq2 6932 . . . . 5 (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦))
65oveq2d 6940 . . . 4 (𝑥 = 𝑦 → (1...(2 · 𝑥)) = (1...(2 · 𝑦)))
76sumeq1d 14843 . . 3 (𝑥 = 𝑦 → Σ𝑛 ∈ (1...(2 · 𝑥))(cos‘(𝑛 · π)) = Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)))
87eqeq1d 2780 . 2 (𝑥 = 𝑦 → (Σ𝑛 ∈ (1...(2 · 𝑥))(cos‘(𝑛 · π)) = 0 ↔ Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) = 0))
9 oveq2 6932 . . . . 5 (𝑥 = (𝑦 + 1) → (2 · 𝑥) = (2 · (𝑦 + 1)))
109oveq2d 6940 . . . 4 (𝑥 = (𝑦 + 1) → (1...(2 · 𝑥)) = (1...(2 · (𝑦 + 1))))
1110sumeq1d 14843 . . 3 (𝑥 = (𝑦 + 1) → Σ𝑛 ∈ (1...(2 · 𝑥))(cos‘(𝑛 · π)) = Σ𝑛 ∈ (1...(2 · (𝑦 + 1)))(cos‘(𝑛 · π)))
1211eqeq1d 2780 . 2 (𝑥 = (𝑦 + 1) → (Σ𝑛 ∈ (1...(2 · 𝑥))(cos‘(𝑛 · π)) = 0 ↔ Σ𝑛 ∈ (1...(2 · (𝑦 + 1)))(cos‘(𝑛 · π)) = 0))
13 oveq2 6932 . . . . 5 (𝑥 = 𝐾 → (2 · 𝑥) = (2 · 𝐾))
1413oveq2d 6940 . . . 4 (𝑥 = 𝐾 → (1...(2 · 𝑥)) = (1...(2 · 𝐾)))
1514sumeq1d 14843 . . 3 (𝑥 = 𝐾 → Σ𝑛 ∈ (1...(2 · 𝑥))(cos‘(𝑛 · π)) = Σ𝑛 ∈ (1...(2 · 𝐾))(cos‘(𝑛 · π)))
1615eqeq1d 2780 . 2 (𝑥 = 𝐾 → (Σ𝑛 ∈ (1...(2 · 𝑥))(cos‘(𝑛 · π)) = 0 ↔ Σ𝑛 ∈ (1...(2 · 𝐾))(cos‘(𝑛 · π)) = 0))
17 ax-1cn 10332 . . . . . 6 1 ∈ ℂ
18172timesi 11524 . . . . 5 (2 · 1) = (1 + 1)
1918oveq2i 6935 . . . 4 (1...(2 · 1)) = (1...(1 + 1))
2019sumeq1i 14840 . . 3 Σ𝑛 ∈ (1...(2 · 1))(cos‘(𝑛 · π)) = Σ𝑛 ∈ (1...(1 + 1))(cos‘(𝑛 · π))
21 1z 11763 . . . . . . . 8 1 ∈ ℤ
22 uzid 12011 . . . . . . . 8 (1 ∈ ℤ → 1 ∈ (ℤ‘1))
2321, 22ax-mp 5 . . . . . . 7 1 ∈ (ℤ‘1)
2423a1i 11 . . . . . 6 (⊤ → 1 ∈ (ℤ‘1))
25 elfzelz 12663 . . . . . . . . . 10 (𝑛 ∈ (1...(1 + 1)) → 𝑛 ∈ ℤ)
2625zcnd 11839 . . . . . . . . 9 (𝑛 ∈ (1...(1 + 1)) → 𝑛 ∈ ℂ)
2726adantl 475 . . . . . . . 8 ((⊤ ∧ 𝑛 ∈ (1...(1 + 1))) → 𝑛 ∈ ℂ)
28 picn 24653 . . . . . . . . 9 π ∈ ℂ
2928a1i 11 . . . . . . . 8 ((⊤ ∧ 𝑛 ∈ (1...(1 + 1))) → π ∈ ℂ)
3027, 29mulcld 10399 . . . . . . 7 ((⊤ ∧ 𝑛 ∈ (1...(1 + 1))) → (𝑛 · π) ∈ ℂ)
3130coscld 15267 . . . . . 6 ((⊤ ∧ 𝑛 ∈ (1...(1 + 1))) → (cos‘(𝑛 · π)) ∈ ℂ)
32 id 22 . . . . . . . 8 (𝑛 = (1 + 1) → 𝑛 = (1 + 1))
33 1p1e2 11511 . . . . . . . 8 (1 + 1) = 2
3432, 33syl6eq 2830 . . . . . . 7 (𝑛 = (1 + 1) → 𝑛 = 2)
3534fvoveq1d 6946 . . . . . 6 (𝑛 = (1 + 1) → (cos‘(𝑛 · π)) = (cos‘(2 · π)))
3624, 31, 35fsump1 14896 . . . . 5 (⊤ → Σ𝑛 ∈ (1...(1 + 1))(cos‘(𝑛 · π)) = (Σ𝑛 ∈ (1...1)(cos‘(𝑛 · π)) + (cos‘(2 · π))))
3736mptru 1609 . . . 4 Σ𝑛 ∈ (1...(1 + 1))(cos‘(𝑛 · π)) = (Σ𝑛 ∈ (1...1)(cos‘(𝑛 · π)) + (cos‘(2 · π)))
38 coscl 15263 . . . . . . . 8 (π ∈ ℂ → (cos‘π) ∈ ℂ)
3928, 38ax-mp 5 . . . . . . 7 (cos‘π) ∈ ℂ
40 oveq1 6931 . . . . . . . . . 10 (𝑛 = 1 → (𝑛 · π) = (1 · π))
4128mulid2i 10384 . . . . . . . . . 10 (1 · π) = π
4240, 41syl6eq 2830 . . . . . . . . 9 (𝑛 = 1 → (𝑛 · π) = π)
4342fveq2d 6452 . . . . . . . 8 (𝑛 = 1 → (cos‘(𝑛 · π)) = (cos‘π))
4443fsum1 14887 . . . . . . 7 ((1 ∈ ℤ ∧ (cos‘π) ∈ ℂ) → Σ𝑛 ∈ (1...1)(cos‘(𝑛 · π)) = (cos‘π))
4521, 39, 44mp2an 682 . . . . . 6 Σ𝑛 ∈ (1...1)(cos‘(𝑛 · π)) = (cos‘π)
46 cospi 24666 . . . . . 6 (cos‘π) = -1
4745, 46eqtri 2802 . . . . 5 Σ𝑛 ∈ (1...1)(cos‘(𝑛 · π)) = -1
48 cos2pi 24670 . . . . 5 (cos‘(2 · π)) = 1
4947, 48oveq12i 6936 . . . 4 𝑛 ∈ (1...1)(cos‘(𝑛 · π)) + (cos‘(2 · π))) = (-1 + 1)
50 neg1cn 11500 . . . . 5 -1 ∈ ℂ
51 1pneg1e0 11505 . . . . 5 (1 + -1) = 0
5217, 50, 51addcomli 10570 . . . 4 (-1 + 1) = 0
5337, 49, 523eqtri 2806 . . 3 Σ𝑛 ∈ (1...(1 + 1))(cos‘(𝑛 · π)) = 0
5420, 53eqtri 2802 . 2 Σ𝑛 ∈ (1...(2 · 1))(cos‘(𝑛 · π)) = 0
5518oveq2i 6935 . . . . . . . 8 ((2 · 𝑦) + (2 · 1)) = ((2 · 𝑦) + (1 + 1))
56 2cnd 11457 . . . . . . . . 9 (𝑦 ∈ ℕ → 2 ∈ ℂ)
57 nncn 11387 . . . . . . . . 9 (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
5817a1i 11 . . . . . . . . 9 (𝑦 ∈ ℕ → 1 ∈ ℂ)
5956, 57, 58adddid 10403 . . . . . . . 8 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = ((2 · 𝑦) + (2 · 1)))
6056, 57mulcld 10399 . . . . . . . . 9 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℂ)
6160, 58, 58addassd 10401 . . . . . . . 8 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) + 1) = ((2 · 𝑦) + (1 + 1)))
6255, 59, 613eqtr4a 2840 . . . . . . 7 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) = (((2 · 𝑦) + 1) + 1))
6362oveq2d 6940 . . . . . 6 (𝑦 ∈ ℕ → (1...(2 · (𝑦 + 1))) = (1...(((2 · 𝑦) + 1) + 1)))
6463sumeq1d 14843 . . . . 5 (𝑦 ∈ ℕ → Σ𝑛 ∈ (1...(2 · (𝑦 + 1)))(cos‘(𝑛 · π)) = Σ𝑛 ∈ (1...(((2 · 𝑦) + 1) + 1))(cos‘(𝑛 · π)))
6564adantr 474 . . . 4 ((𝑦 ∈ ℕ ∧ Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) = 0) → Σ𝑛 ∈ (1...(2 · (𝑦 + 1)))(cos‘(𝑛 · π)) = Σ𝑛 ∈ (1...(((2 · 𝑦) + 1) + 1))(cos‘(𝑛 · π)))
66 1red 10379 . . . . . . . 8 (𝑦 ∈ ℕ → 1 ∈ ℝ)
67 2re 11453 . . . . . . . . . . 11 2 ∈ ℝ
6867a1i 11 . . . . . . . . . 10 (𝑦 ∈ ℕ → 2 ∈ ℝ)
69 nnre 11386 . . . . . . . . . 10 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
7068, 69remulcld 10409 . . . . . . . . 9 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℝ)
7170, 66readdcld 10408 . . . . . . . 8 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℝ)
72 2rp 12146 . . . . . . . . . . 11 2 ∈ ℝ+
7372a1i 11 . . . . . . . . . 10 (𝑦 ∈ ℕ → 2 ∈ ℝ+)
74 nnrp 12154 . . . . . . . . . 10 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ+)
7573, 74rpmulcld 12201 . . . . . . . . 9 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℝ+)
7666, 75ltaddrp2d 12219 . . . . . . . 8 (𝑦 ∈ ℕ → 1 < ((2 · 𝑦) + 1))
7766, 71, 76ltled 10526 . . . . . . 7 (𝑦 ∈ ℕ → 1 ≤ ((2 · 𝑦) + 1))
78 2z 11765 . . . . . . . . . . 11 2 ∈ ℤ
7978a1i 11 . . . . . . . . . 10 (𝑦 ∈ ℕ → 2 ∈ ℤ)
80 nnz 11755 . . . . . . . . . 10 (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
8179, 80zmulcld 11844 . . . . . . . . 9 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ ℤ)
8281peano2zd 11841 . . . . . . . 8 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ ℤ)
83 eluz 12010 . . . . . . . 8 ((1 ∈ ℤ ∧ ((2 · 𝑦) + 1) ∈ ℤ) → (((2 · 𝑦) + 1) ∈ (ℤ‘1) ↔ 1 ≤ ((2 · 𝑦) + 1)))
8421, 82, 83sylancr 581 . . . . . . 7 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) ∈ (ℤ‘1) ↔ 1 ≤ ((2 · 𝑦) + 1)))
8577, 84mpbird 249 . . . . . 6 (𝑦 ∈ ℕ → ((2 · 𝑦) + 1) ∈ (ℤ‘1))
86 elfzelz 12663 . . . . . . . . . 10 (𝑛 ∈ (1...(((2 · 𝑦) + 1) + 1)) → 𝑛 ∈ ℤ)
8786zcnd 11839 . . . . . . . . 9 (𝑛 ∈ (1...(((2 · 𝑦) + 1) + 1)) → 𝑛 ∈ ℂ)
8828a1i 11 . . . . . . . . 9 (𝑛 ∈ (1...(((2 · 𝑦) + 1) + 1)) → π ∈ ℂ)
8987, 88mulcld 10399 . . . . . . . 8 (𝑛 ∈ (1...(((2 · 𝑦) + 1) + 1)) → (𝑛 · π) ∈ ℂ)
9089coscld 15267 . . . . . . 7 (𝑛 ∈ (1...(((2 · 𝑦) + 1) + 1)) → (cos‘(𝑛 · π)) ∈ ℂ)
9190adantl 475 . . . . . 6 ((𝑦 ∈ ℕ ∧ 𝑛 ∈ (1...(((2 · 𝑦) + 1) + 1))) → (cos‘(𝑛 · π)) ∈ ℂ)
92 fvoveq1 6947 . . . . . 6 (𝑛 = (((2 · 𝑦) + 1) + 1) → (cos‘(𝑛 · π)) = (cos‘((((2 · 𝑦) + 1) + 1) · π)))
9385, 91, 92fsump1 14896 . . . . 5 (𝑦 ∈ ℕ → Σ𝑛 ∈ (1...(((2 · 𝑦) + 1) + 1))(cos‘(𝑛 · π)) = (Σ𝑛 ∈ (1...((2 · 𝑦) + 1))(cos‘(𝑛 · π)) + (cos‘((((2 · 𝑦) + 1) + 1) · π))))
9493adantr 474 . . . 4 ((𝑦 ∈ ℕ ∧ Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) = 0) → Σ𝑛 ∈ (1...(((2 · 𝑦) + 1) + 1))(cos‘(𝑛 · π)) = (Σ𝑛 ∈ (1...((2 · 𝑦) + 1))(cos‘(𝑛 · π)) + (cos‘((((2 · 𝑦) + 1) + 1) · π))))
95 1lt2 11557 . . . . . . . . . . . 12 1 < 2
9695a1i 11 . . . . . . . . . . 11 (𝑦 ∈ ℕ → 1 < 2)
97 2t1e2 11549 . . . . . . . . . . . 12 (2 · 1) = 2
98 nnge1 11408 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → 1 ≤ 𝑦)
9966, 69, 73lemul2d 12229 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (1 ≤ 𝑦 ↔ (2 · 1) ≤ (2 · 𝑦)))
10098, 99mpbid 224 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (2 · 1) ≤ (2 · 𝑦))
10197, 100syl5eqbrr 4924 . . . . . . . . . . 11 (𝑦 ∈ ℕ → 2 ≤ (2 · 𝑦))
10266, 68, 70, 96, 101ltletrd 10538 . . . . . . . . . 10 (𝑦 ∈ ℕ → 1 < (2 · 𝑦))
10366, 70, 102ltled 10526 . . . . . . . . 9 (𝑦 ∈ ℕ → 1 ≤ (2 · 𝑦))
104 eluz 12010 . . . . . . . . . 10 ((1 ∈ ℤ ∧ (2 · 𝑦) ∈ ℤ) → ((2 · 𝑦) ∈ (ℤ‘1) ↔ 1 ≤ (2 · 𝑦)))
10521, 81, 104sylancr 581 . . . . . . . . 9 (𝑦 ∈ ℕ → ((2 · 𝑦) ∈ (ℤ‘1) ↔ 1 ≤ (2 · 𝑦)))
106103, 105mpbird 249 . . . . . . . 8 (𝑦 ∈ ℕ → (2 · 𝑦) ∈ (ℤ‘1))
107 elfzelz 12663 . . . . . . . . . . . 12 (𝑛 ∈ (1...((2 · 𝑦) + 1)) → 𝑛 ∈ ℤ)
108107zcnd 11839 . . . . . . . . . . 11 (𝑛 ∈ (1...((2 · 𝑦) + 1)) → 𝑛 ∈ ℂ)
10928a1i 11 . . . . . . . . . . 11 (𝑛 ∈ (1...((2 · 𝑦) + 1)) → π ∈ ℂ)
110108, 109mulcld 10399 . . . . . . . . . 10 (𝑛 ∈ (1...((2 · 𝑦) + 1)) → (𝑛 · π) ∈ ℂ)
111110coscld 15267 . . . . . . . . 9 (𝑛 ∈ (1...((2 · 𝑦) + 1)) → (cos‘(𝑛 · π)) ∈ ℂ)
112111adantl 475 . . . . . . . 8 ((𝑦 ∈ ℕ ∧ 𝑛 ∈ (1...((2 · 𝑦) + 1))) → (cos‘(𝑛 · π)) ∈ ℂ)
113 fvoveq1 6947 . . . . . . . 8 (𝑛 = ((2 · 𝑦) + 1) → (cos‘(𝑛 · π)) = (cos‘(((2 · 𝑦) + 1) · π)))
114106, 112, 113fsump1 14896 . . . . . . 7 (𝑦 ∈ ℕ → Σ𝑛 ∈ (1...((2 · 𝑦) + 1))(cos‘(𝑛 · π)) = (Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) + (cos‘(((2 · 𝑦) + 1) · π))))
11533, 97eqtr4i 2805 . . . . . . . . . . . 12 (1 + 1) = (2 · 1)
116115a1i 11 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (1 + 1) = (2 · 1))
117116oveq2d 6940 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · 𝑦) + (1 + 1)) = ((2 · 𝑦) + (2 · 1)))
118117, 61, 593eqtr4d 2824 . . . . . . . . 9 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) + 1) = (2 · (𝑦 + 1)))
119118fvoveq1d 6946 . . . . . . . 8 (𝑦 ∈ ℕ → (cos‘((((2 · 𝑦) + 1) + 1) · π)) = (cos‘((2 · (𝑦 + 1)) · π)))
12057, 58addcld 10398 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℂ)
12128a1i 11 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → π ∈ ℂ)
12256, 120, 121mulassd 10402 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · π) = (2 · ((𝑦 + 1) · π)))
123122oveq1d 6939 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · π) / (2 · π)) = ((2 · ((𝑦 + 1) · π)) / (2 · π)))
124120, 121mulcld 10399 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((𝑦 + 1) · π) ∈ ℂ)
125 0re 10380 . . . . . . . . . . . . . 14 0 ∈ ℝ
126 pipos 24654 . . . . . . . . . . . . . 14 0 < π
127125, 126gtneii 10490 . . . . . . . . . . . . 13 π ≠ 0
128127a1i 11 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → π ≠ 0)
12973rpne0d 12190 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 2 ≠ 0)
130124, 121, 56, 128, 129divcan5d 11179 . . . . . . . . . . 11 (𝑦 ∈ ℕ → ((2 · ((𝑦 + 1) · π)) / (2 · π)) = (((𝑦 + 1) · π) / π))
131120, 121, 128divcan4d 11159 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((𝑦 + 1) · π) / π) = (𝑦 + 1))
132123, 130, 1313eqtrd 2818 . . . . . . . . . 10 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · π) / (2 · π)) = (𝑦 + 1))
13380peano2zd 11841 . . . . . . . . . 10 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℤ)
134132, 133eqeltrd 2859 . . . . . . . . 9 (𝑦 ∈ ℕ → (((2 · (𝑦 + 1)) · π) / (2 · π)) ∈ ℤ)
135 peano2cn 10550 . . . . . . . . . . . . 13 (𝑦 ∈ ℂ → (𝑦 + 1) ∈ ℂ)
13657, 135syl 17 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℂ)
13756, 136mulcld 10399 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (2 · (𝑦 + 1)) ∈ ℂ)
138137, 121mulcld 10399 . . . . . . . . . 10 (𝑦 ∈ ℕ → ((2 · (𝑦 + 1)) · π) ∈ ℂ)
139 coseq1 24716 . . . . . . . . . 10 (((2 · (𝑦 + 1)) · π) ∈ ℂ → ((cos‘((2 · (𝑦 + 1)) · π)) = 1 ↔ (((2 · (𝑦 + 1)) · π) / (2 · π)) ∈ ℤ))
140138, 139syl 17 . . . . . . . . 9 (𝑦 ∈ ℕ → ((cos‘((2 · (𝑦 + 1)) · π)) = 1 ↔ (((2 · (𝑦 + 1)) · π) / (2 · π)) ∈ ℤ))
141134, 140mpbird 249 . . . . . . . 8 (𝑦 ∈ ℕ → (cos‘((2 · (𝑦 + 1)) · π)) = 1)
142119, 141eqtrd 2814 . . . . . . 7 (𝑦 ∈ ℕ → (cos‘((((2 · 𝑦) + 1) + 1) · π)) = 1)
143114, 142oveq12d 6942 . . . . . 6 (𝑦 ∈ ℕ → (Σ𝑛 ∈ (1...((2 · 𝑦) + 1))(cos‘(𝑛 · π)) + (cos‘((((2 · 𝑦) + 1) + 1) · π))) = ((Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) + (cos‘(((2 · 𝑦) + 1) · π))) + 1))
144143adantr 474 . . . . 5 ((𝑦 ∈ ℕ ∧ Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) = 0) → (Σ𝑛 ∈ (1...((2 · 𝑦) + 1))(cos‘(𝑛 · π)) + (cos‘((((2 · 𝑦) + 1) + 1) · π))) = ((Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) + (cos‘(((2 · 𝑦) + 1) · π))) + 1))
145 simpr 479 . . . . . . . 8 ((𝑦 ∈ ℕ ∧ Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) = 0) → Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) = 0)
14660, 58, 121adddird 10404 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · π) = (((2 · 𝑦) · π) + (1 · π)))
14760, 121mulcld 10399 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · 𝑦) · π) ∈ ℂ)
14841, 121syl5eqel 2863 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (1 · π) ∈ ℂ)
149147, 148addcomd 10580 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (((2 · 𝑦) · π) + (1 · π)) = ((1 · π) + ((2 · 𝑦) · π)))
15041a1i 11 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (1 · π) = π)
15156, 57mulcomd 10400 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (2 · 𝑦) = (𝑦 · 2))
152151oveq1d 6939 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((2 · 𝑦) · π) = ((𝑦 · 2) · π))
15357, 56, 121mulassd 10402 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → ((𝑦 · 2) · π) = (𝑦 · (2 · π)))
154152, 153eqtrd 2814 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((2 · 𝑦) · π) = (𝑦 · (2 · π)))
155150, 154oveq12d 6942 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → ((1 · π) + ((2 · 𝑦) · π)) = (π + (𝑦 · (2 · π))))
156146, 149, 1553eqtrd 2818 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (((2 · 𝑦) + 1) · π) = (π + (𝑦 · (2 · π))))
157156fveq2d 6452 . . . . . . . . . 10 (𝑦 ∈ ℕ → (cos‘(((2 · 𝑦) + 1) · π)) = (cos‘(π + (𝑦 · (2 · π)))))
158 cosper 24676 . . . . . . . . . . 11 ((π ∈ ℂ ∧ 𝑦 ∈ ℤ) → (cos‘(π + (𝑦 · (2 · π)))) = (cos‘π))
15928, 80, 158sylancr 581 . . . . . . . . . 10 (𝑦 ∈ ℕ → (cos‘(π + (𝑦 · (2 · π)))) = (cos‘π))
16046a1i 11 . . . . . . . . . 10 (𝑦 ∈ ℕ → (cos‘π) = -1)
161157, 159, 1603eqtrd 2818 . . . . . . . . 9 (𝑦 ∈ ℕ → (cos‘(((2 · 𝑦) + 1) · π)) = -1)
162161adantr 474 . . . . . . . 8 ((𝑦 ∈ ℕ ∧ Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) = 0) → (cos‘(((2 · 𝑦) + 1) · π)) = -1)
163145, 162oveq12d 6942 . . . . . . 7 ((𝑦 ∈ ℕ ∧ Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) = 0) → (Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) + (cos‘(((2 · 𝑦) + 1) · π))) = (0 + -1))
164163oveq1d 6939 . . . . . 6 ((𝑦 ∈ ℕ ∧ Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) = 0) → ((Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) + (cos‘(((2 · 𝑦) + 1) · π))) + 1) = ((0 + -1) + 1))
16550addid2i 10566 . . . . . . . 8 (0 + -1) = -1
166165oveq1i 6934 . . . . . . 7 ((0 + -1) + 1) = (-1 + 1)
167166, 52eqtri 2802 . . . . . 6 ((0 + -1) + 1) = 0
168164, 167syl6eq 2830 . . . . 5 ((𝑦 ∈ ℕ ∧ Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) = 0) → ((Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) + (cos‘(((2 · 𝑦) + 1) · π))) + 1) = 0)
169144, 168eqtrd 2814 . . . 4 ((𝑦 ∈ ℕ ∧ Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) = 0) → (Σ𝑛 ∈ (1...((2 · 𝑦) + 1))(cos‘(𝑛 · π)) + (cos‘((((2 · 𝑦) + 1) + 1) · π))) = 0)
17065, 94, 1693eqtrd 2818 . . 3 ((𝑦 ∈ ℕ ∧ Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) = 0) → Σ𝑛 ∈ (1...(2 · (𝑦 + 1)))(cos‘(𝑛 · π)) = 0)
171170ex 403 . 2 (𝑦 ∈ ℕ → (Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) = 0 → Σ𝑛 ∈ (1...(2 · (𝑦 + 1)))(cos‘(𝑛 · π)) = 0))
1724, 8, 12, 16, 54, 171nnind 11398 1 (𝐾 ∈ ℕ → Σ𝑛 ∈ (1...(2 · 𝐾))(cos‘(𝑛 · π)) = 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386   = wceq 1601  wtru 1602  wcel 2107  wne 2969   class class class wbr 4888  cfv 6137  (class class class)co 6924  cc 10272  cr 10273  0cc0 10274  1c1 10275   + caddc 10277   · cmul 10279   < clt 10413  cle 10414  -cneg 10609   / cdiv 11034  cn 11378  2c2 11434  cz 11732  cuz 11996  +crp 12141  ...cfz 12647  Σcsu 14828  cosccos 15201  πcpi 15203
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5008  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-inf2 8837  ax-cnex 10330  ax-resscn 10331  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-mulcom 10338  ax-addass 10339  ax-mulass 10340  ax-distr 10341  ax-i2m1 10342  ax-1ne0 10343  ax-1rid 10344  ax-rnegex 10345  ax-rrecex 10346  ax-cnre 10347  ax-pre-lttri 10348  ax-pre-lttrn 10349  ax-pre-ltadd 10350  ax-pre-mulgt0 10351  ax-pre-sup 10352  ax-addf 10353  ax-mulf 10354
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-fal 1615  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-int 4713  df-iun 4757  df-iin 4758  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-se 5317  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-isom 6146  df-riota 6885  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-of 7176  df-om 7346  df-1st 7447  df-2nd 7448  df-supp 7579  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-1o 7845  df-2o 7846  df-oadd 7849  df-er 8028  df-map 8144  df-pm 8145  df-ixp 8197  df-en 8244  df-dom 8245  df-sdom 8246  df-fin 8247  df-fsupp 8566  df-fi 8607  df-sup 8638  df-inf 8639  df-oi 8706  df-card 9100  df-cda 9327  df-pnf 10415  df-mnf 10416  df-xr 10417  df-ltxr 10418  df-le 10419  df-sub 10610  df-neg 10611  df-div 11035  df-nn 11379  df-2 11442  df-3 11443  df-4 11444  df-5 11445  df-6 11446  df-7 11447  df-8 11448  df-9 11449  df-n0 11647  df-z 11733  df-dec 11850  df-uz 11997  df-q 12100  df-rp 12142  df-xneg 12261  df-xadd 12262  df-xmul 12263  df-ioo 12495  df-ioc 12496  df-ico 12497  df-icc 12498  df-fz 12648  df-fzo 12789  df-fl 12916  df-mod 12992  df-seq 13124  df-exp 13183  df-fac 13383  df-bc 13412  df-hash 13440  df-shft 14218  df-cj 14250  df-re 14251  df-im 14252  df-sqrt 14386  df-abs 14387  df-limsup 14614  df-clim 14631  df-rlim 14632  df-sum 14829  df-ef 15204  df-sin 15206  df-cos 15207  df-pi 15209  df-struct 16261  df-ndx 16262  df-slot 16263  df-base 16265  df-sets 16266  df-ress 16267  df-plusg 16355  df-mulr 16356  df-starv 16357  df-sca 16358  df-vsca 16359  df-ip 16360  df-tset 16361  df-ple 16362  df-ds 16364  df-unif 16365  df-hom 16366  df-cco 16367  df-rest 16473  df-topn 16474  df-0g 16492  df-gsum 16493  df-topgen 16494  df-pt 16495  df-prds 16498  df-xrs 16552  df-qtop 16557  df-imas 16558  df-xps 16560  df-mre 16636  df-mrc 16637  df-acs 16639  df-mgm 17632  df-sgrp 17674  df-mnd 17685  df-submnd 17726  df-mulg 17932  df-cntz 18137  df-cmn 18585  df-psmet 20138  df-xmet 20139  df-met 20140  df-bl 20141  df-mopn 20142  df-fbas 20143  df-fg 20144  df-cnfld 20147  df-top 21110  df-topon 21127  df-topsp 21149  df-bases 21162  df-cld 21235  df-ntr 21236  df-cls 21237  df-nei 21314  df-lp 21352  df-perf 21353  df-cn 21443  df-cnp 21444  df-haus 21531  df-tx 21778  df-hmeo 21971  df-fil 22062  df-fm 22154  df-flim 22155  df-flf 22156  df-xms 22537  df-ms 22538  df-tms 22539  df-cncf 23093  df-limc 24071  df-dv 24072
This theorem is referenced by:  dirkertrigeqlem3  41254
  Copyright terms: Public domain W3C validator