Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . 5
⊢ (𝑥 = 1 → (2 · 𝑥) = (2 ·
1)) |
2 | 1 | oveq2d 6666 |
. . . 4
⊢ (𝑥 = 1 → (1...(2 ·
𝑥)) = (1...(2 ·
1))) |
3 | 2 | sumeq1d 14431 |
. . 3
⊢ (𝑥 = 1 → Σ𝑛 ∈ (1...(2 · 𝑥))(cos‘(𝑛 · π)) = Σ𝑛 ∈ (1...(2 · 1))(cos‘(𝑛 ·
π))) |
4 | 3 | eqeq1d 2624 |
. 2
⊢ (𝑥 = 1 → (Σ𝑛 ∈ (1...(2 · 𝑥))(cos‘(𝑛 · π)) = 0 ↔ Σ𝑛 ∈ (1...(2 ·
1))(cos‘(𝑛 ·
π)) = 0)) |
5 | | oveq2 6658 |
. . . . 5
⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦)) |
6 | 5 | oveq2d 6666 |
. . . 4
⊢ (𝑥 = 𝑦 → (1...(2 · 𝑥)) = (1...(2 · 𝑦))) |
7 | 6 | sumeq1d 14431 |
. . 3
⊢ (𝑥 = 𝑦 → Σ𝑛 ∈ (1...(2 · 𝑥))(cos‘(𝑛 · π)) = Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π))) |
8 | 7 | eqeq1d 2624 |
. 2
⊢ (𝑥 = 𝑦 → (Σ𝑛 ∈ (1...(2 · 𝑥))(cos‘(𝑛 · π)) = 0 ↔ Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) = 0)) |
9 | | oveq2 6658 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (2 · 𝑥) = (2 · (𝑦 + 1))) |
10 | 9 | oveq2d 6666 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → (1...(2 · 𝑥)) = (1...(2 · (𝑦 + 1)))) |
11 | 10 | sumeq1d 14431 |
. . 3
⊢ (𝑥 = (𝑦 + 1) → Σ𝑛 ∈ (1...(2 · 𝑥))(cos‘(𝑛 · π)) = Σ𝑛 ∈ (1...(2 · (𝑦 + 1)))(cos‘(𝑛 · π))) |
12 | 11 | eqeq1d 2624 |
. 2
⊢ (𝑥 = (𝑦 + 1) → (Σ𝑛 ∈ (1...(2 · 𝑥))(cos‘(𝑛 · π)) = 0 ↔ Σ𝑛 ∈ (1...(2 · (𝑦 + 1)))(cos‘(𝑛 · π)) =
0)) |
13 | | oveq2 6658 |
. . . . 5
⊢ (𝑥 = 𝐾 → (2 · 𝑥) = (2 · 𝐾)) |
14 | 13 | oveq2d 6666 |
. . . 4
⊢ (𝑥 = 𝐾 → (1...(2 · 𝑥)) = (1...(2 · 𝐾))) |
15 | 14 | sumeq1d 14431 |
. . 3
⊢ (𝑥 = 𝐾 → Σ𝑛 ∈ (1...(2 · 𝑥))(cos‘(𝑛 · π)) = Σ𝑛 ∈ (1...(2 · 𝐾))(cos‘(𝑛 · π))) |
16 | 15 | eqeq1d 2624 |
. 2
⊢ (𝑥 = 𝐾 → (Σ𝑛 ∈ (1...(2 · 𝑥))(cos‘(𝑛 · π)) = 0 ↔ Σ𝑛 ∈ (1...(2 · 𝐾))(cos‘(𝑛 · π)) = 0)) |
17 | | ax-1cn 9994 |
. . . . . 6
⊢ 1 ∈
ℂ |
18 | 17 | 2timesi 11147 |
. . . . 5
⊢ (2
· 1) = (1 + 1) |
19 | 18 | oveq2i 6661 |
. . . 4
⊢ (1...(2
· 1)) = (1...(1 + 1)) |
20 | 19 | sumeq1i 14428 |
. . 3
⊢
Σ𝑛 ∈
(1...(2 · 1))(cos‘(𝑛 · π)) = Σ𝑛 ∈ (1...(1 + 1))(cos‘(𝑛 ·
π)) |
21 | | 1z 11407 |
. . . . . . . 8
⊢ 1 ∈
ℤ |
22 | | uzid 11702 |
. . . . . . . 8
⊢ (1 ∈
ℤ → 1 ∈ (ℤ≥‘1)) |
23 | 21, 22 | ax-mp 5 |
. . . . . . 7
⊢ 1 ∈
(ℤ≥‘1) |
24 | 23 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 1 ∈ (ℤ≥‘1)) |
25 | | elfzelz 12342 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (1...(1 + 1)) →
𝑛 ∈
ℤ) |
26 | 25 | zcnd 11483 |
. . . . . . . . 9
⊢ (𝑛 ∈ (1...(1 + 1)) →
𝑛 ∈
ℂ) |
27 | 26 | adantl 482 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑛
∈ (1...(1 + 1))) → 𝑛 ∈ ℂ) |
28 | | picn 24211 |
. . . . . . . . 9
⊢ π
∈ ℂ |
29 | 28 | a1i 11 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑛
∈ (1...(1 + 1))) → π ∈ ℂ) |
30 | 27, 29 | mulcld 10060 |
. . . . . . 7
⊢
((⊤ ∧ 𝑛
∈ (1...(1 + 1))) → (𝑛 · π) ∈
ℂ) |
31 | 30 | coscld 14861 |
. . . . . 6
⊢
((⊤ ∧ 𝑛
∈ (1...(1 + 1))) → (cos‘(𝑛 · π)) ∈
ℂ) |
32 | | id 22 |
. . . . . . . . 9
⊢ (𝑛 = (1 + 1) → 𝑛 = (1 + 1)) |
33 | | 1p1e2 11134 |
. . . . . . . . 9
⊢ (1 + 1) =
2 |
34 | 32, 33 | syl6eq 2672 |
. . . . . . . 8
⊢ (𝑛 = (1 + 1) → 𝑛 = 2) |
35 | 34 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑛 = (1 + 1) → (𝑛 · π) = (2 ·
π)) |
36 | 35 | fveq2d 6195 |
. . . . . 6
⊢ (𝑛 = (1 + 1) →
(cos‘(𝑛 ·
π)) = (cos‘(2 · π))) |
37 | 24, 31, 36 | fsump1 14487 |
. . . . 5
⊢ (⊤
→ Σ𝑛 ∈
(1...(1 + 1))(cos‘(𝑛
· π)) = (Σ𝑛
∈ (1...1)(cos‘(𝑛
· π)) + (cos‘(2 · π)))) |
38 | 37 | trud 1493 |
. . . 4
⊢
Σ𝑛 ∈
(1...(1 + 1))(cos‘(𝑛
· π)) = (Σ𝑛
∈ (1...1)(cos‘(𝑛
· π)) + (cos‘(2 · π))) |
39 | | coscl 14857 |
. . . . . . . 8
⊢ (π
∈ ℂ → (cos‘π) ∈ ℂ) |
40 | 28, 39 | ax-mp 5 |
. . . . . . 7
⊢
(cos‘π) ∈ ℂ |
41 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑛 = 1 → (𝑛 · π) = (1 ·
π)) |
42 | 28 | mulid2i 10043 |
. . . . . . . . . 10
⊢ (1
· π) = π |
43 | 41, 42 | syl6eq 2672 |
. . . . . . . . 9
⊢ (𝑛 = 1 → (𝑛 · π) = π) |
44 | 43 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑛 = 1 → (cos‘(𝑛 · π)) =
(cos‘π)) |
45 | 44 | fsum1 14476 |
. . . . . . 7
⊢ ((1
∈ ℤ ∧ (cos‘π) ∈ ℂ) → Σ𝑛 ∈ (1...1)(cos‘(𝑛 · π)) =
(cos‘π)) |
46 | 21, 40, 45 | mp2an 708 |
. . . . . 6
⊢
Σ𝑛 ∈
(1...1)(cos‘(𝑛
· π)) = (cos‘π) |
47 | | cospi 24224 |
. . . . . 6
⊢
(cos‘π) = -1 |
48 | 46, 47 | eqtri 2644 |
. . . . 5
⊢
Σ𝑛 ∈
(1...1)(cos‘(𝑛
· π)) = -1 |
49 | | cos2pi 24228 |
. . . . 5
⊢
(cos‘(2 · π)) = 1 |
50 | 48, 49 | oveq12i 6662 |
. . . 4
⊢
(Σ𝑛 ∈
(1...1)(cos‘(𝑛
· π)) + (cos‘(2 · π))) = (-1 + 1) |
51 | | neg1cn 11124 |
. . . . 5
⊢ -1 ∈
ℂ |
52 | | 1pneg1e0 11129 |
. . . . 5
⊢ (1 + -1)
= 0 |
53 | 17, 51, 52 | addcomli 10228 |
. . . 4
⊢ (-1 + 1)
= 0 |
54 | 38, 50, 53 | 3eqtri 2648 |
. . 3
⊢
Σ𝑛 ∈
(1...(1 + 1))(cos‘(𝑛
· π)) = 0 |
55 | 20, 54 | eqtri 2644 |
. 2
⊢
Σ𝑛 ∈
(1...(2 · 1))(cos‘(𝑛 · π)) = 0 |
56 | 18 | oveq2i 6661 |
. . . . . . . 8
⊢ ((2
· 𝑦) + (2 ·
1)) = ((2 · 𝑦) + (1
+ 1)) |
57 | | 2cnd 11093 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → 2 ∈
ℂ) |
58 | | nncn 11028 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
59 | 17 | a1i 11 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → 1 ∈
ℂ) |
60 | 57, 58, 59 | adddid 10064 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ → (2
· (𝑦 + 1)) = ((2
· 𝑦) + (2 ·
1))) |
61 | 57, 58 | mulcld 10060 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → (2
· 𝑦) ∈
ℂ) |
62 | 61, 59, 59 | addassd 10062 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ → (((2
· 𝑦) + 1) + 1) = ((2
· 𝑦) + (1 +
1))) |
63 | 56, 60, 62 | 3eqtr4a 2682 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → (2
· (𝑦 + 1)) = (((2
· 𝑦) + 1) +
1)) |
64 | 63 | oveq2d 6666 |
. . . . . 6
⊢ (𝑦 ∈ ℕ → (1...(2
· (𝑦 + 1))) =
(1...(((2 · 𝑦) + 1)
+ 1))) |
65 | 64 | sumeq1d 14431 |
. . . . 5
⊢ (𝑦 ∈ ℕ →
Σ𝑛 ∈ (1...(2
· (𝑦 +
1)))(cos‘(𝑛 ·
π)) = Σ𝑛 ∈
(1...(((2 · 𝑦) + 1)
+ 1))(cos‘(𝑛 ·
π))) |
66 | 65 | adantr 481 |
. . . 4
⊢ ((𝑦 ∈ ℕ ∧
Σ𝑛 ∈ (1...(2
· 𝑦))(cos‘(𝑛 · π)) = 0) → Σ𝑛 ∈ (1...(2 · (𝑦 + 1)))(cos‘(𝑛 · π)) = Σ𝑛 ∈ (1...(((2 · 𝑦) + 1) + 1))(cos‘(𝑛 ·
π))) |
67 | | 1red 10055 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ → 1 ∈
ℝ) |
68 | | 2re 11090 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
69 | 68 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → 2 ∈
ℝ) |
70 | | nnre 11027 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) |
71 | 69, 70 | remulcld 10070 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → (2
· 𝑦) ∈
ℝ) |
72 | 71, 67 | readdcld 10069 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + 1) ∈
ℝ) |
73 | | 2rp 11837 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ+ |
74 | 73 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → 2 ∈
ℝ+) |
75 | | nnrp 11842 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ+) |
76 | 74, 75 | rpmulcld 11888 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → (2
· 𝑦) ∈
ℝ+) |
77 | 67, 76 | ltaddrp2d 11906 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ → 1 <
((2 · 𝑦) +
1)) |
78 | 67, 72, 77 | ltled 10185 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → 1 ≤
((2 · 𝑦) +
1)) |
79 | | 2z 11409 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
80 | 79 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → 2 ∈
ℤ) |
81 | | nnz 11399 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
82 | 80, 81 | zmulcld 11488 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → (2
· 𝑦) ∈
ℤ) |
83 | 82 | peano2zd 11485 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + 1) ∈
ℤ) |
84 | | eluz 11701 |
. . . . . . . 8
⊢ ((1
∈ ℤ ∧ ((2 · 𝑦) + 1) ∈ ℤ) → (((2 ·
𝑦) + 1) ∈
(ℤ≥‘1) ↔ 1 ≤ ((2 · 𝑦) + 1))) |
85 | 21, 83, 84 | sylancr 695 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → (((2
· 𝑦) + 1) ∈
(ℤ≥‘1) ↔ 1 ≤ ((2 · 𝑦) + 1))) |
86 | 78, 85 | mpbird 247 |
. . . . . 6
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + 1) ∈
(ℤ≥‘1)) |
87 | | elfzelz 12342 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (1...(((2 · 𝑦) + 1) + 1)) → 𝑛 ∈
ℤ) |
88 | 87 | zcnd 11483 |
. . . . . . . . 9
⊢ (𝑛 ∈ (1...(((2 · 𝑦) + 1) + 1)) → 𝑛 ∈
ℂ) |
89 | 28 | a1i 11 |
. . . . . . . . 9
⊢ (𝑛 ∈ (1...(((2 · 𝑦) + 1) + 1)) → π ∈
ℂ) |
90 | 88, 89 | mulcld 10060 |
. . . . . . . 8
⊢ (𝑛 ∈ (1...(((2 · 𝑦) + 1) + 1)) → (𝑛 · π) ∈
ℂ) |
91 | 90 | coscld 14861 |
. . . . . . 7
⊢ (𝑛 ∈ (1...(((2 · 𝑦) + 1) + 1)) →
(cos‘(𝑛 ·
π)) ∈ ℂ) |
92 | 91 | adantl 482 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ ∧ 𝑛 ∈ (1...(((2 · 𝑦) + 1) + 1))) →
(cos‘(𝑛 ·
π)) ∈ ℂ) |
93 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑛 = (((2 · 𝑦) + 1) + 1) → (𝑛 · π) = ((((2 ·
𝑦) + 1) + 1) ·
π)) |
94 | 93 | fveq2d 6195 |
. . . . . 6
⊢ (𝑛 = (((2 · 𝑦) + 1) + 1) →
(cos‘(𝑛 ·
π)) = (cos‘((((2 · 𝑦) + 1) + 1) · π))) |
95 | 86, 92, 94 | fsump1 14487 |
. . . . 5
⊢ (𝑦 ∈ ℕ →
Σ𝑛 ∈ (1...(((2
· 𝑦) + 1) +
1))(cos‘(𝑛 ·
π)) = (Σ𝑛 ∈
(1...((2 · 𝑦) +
1))(cos‘(𝑛 ·
π)) + (cos‘((((2 · 𝑦) + 1) + 1) ·
π)))) |
96 | 95 | adantr 481 |
. . . 4
⊢ ((𝑦 ∈ ℕ ∧
Σ𝑛 ∈ (1...(2
· 𝑦))(cos‘(𝑛 · π)) = 0) → Σ𝑛 ∈ (1...(((2 · 𝑦) + 1) + 1))(cos‘(𝑛 · π)) = (Σ𝑛 ∈ (1...((2 · 𝑦) + 1))(cos‘(𝑛 · π)) +
(cos‘((((2 · 𝑦) + 1) + 1) ·
π)))) |
97 | | 1lt2 11194 |
. . . . . . . . . . . 12
⊢ 1 <
2 |
98 | 97 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → 1 <
2) |
99 | | 2t1e2 11176 |
. . . . . . . . . . . 12
⊢ (2
· 1) = 2 |
100 | | nnge1 11046 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → 1 ≤
𝑦) |
101 | 67, 70, 74 | lemul2d 11916 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → (1 ≤
𝑦 ↔ (2 · 1)
≤ (2 · 𝑦))) |
102 | 100, 101 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → (2
· 1) ≤ (2 · 𝑦)) |
103 | 99, 102 | syl5eqbrr 4689 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → 2 ≤ (2
· 𝑦)) |
104 | 67, 69, 71, 98, 103 | ltletrd 10197 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → 1 < (2
· 𝑦)) |
105 | 67, 71, 104 | ltled 10185 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → 1 ≤ (2
· 𝑦)) |
106 | | eluz 11701 |
. . . . . . . . . 10
⊢ ((1
∈ ℤ ∧ (2 · 𝑦) ∈ ℤ) → ((2 · 𝑦) ∈
(ℤ≥‘1) ↔ 1 ≤ (2 · 𝑦))) |
107 | 21, 82, 106 | sylancr 695 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) ∈
(ℤ≥‘1) ↔ 1 ≤ (2 · 𝑦))) |
108 | 105, 107 | mpbird 247 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ → (2
· 𝑦) ∈
(ℤ≥‘1)) |
109 | | elfzelz 12342 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (1...((2 · 𝑦) + 1)) → 𝑛 ∈
ℤ) |
110 | 109 | zcnd 11483 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (1...((2 · 𝑦) + 1)) → 𝑛 ∈
ℂ) |
111 | 28 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (1...((2 · 𝑦) + 1)) → π ∈
ℂ) |
112 | 110, 111 | mulcld 10060 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (1...((2 · 𝑦) + 1)) → (𝑛 · π) ∈
ℂ) |
113 | 112 | coscld 14861 |
. . . . . . . . 9
⊢ (𝑛 ∈ (1...((2 · 𝑦) + 1)) → (cos‘(𝑛 · π)) ∈
ℂ) |
114 | 113 | adantl 482 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧ 𝑛 ∈ (1...((2 · 𝑦) + 1))) →
(cos‘(𝑛 ·
π)) ∈ ℂ) |
115 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑛 = ((2 · 𝑦) + 1) → (𝑛 · π) = (((2 ·
𝑦) + 1) ·
π)) |
116 | 115 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑛 = ((2 · 𝑦) + 1) → (cos‘(𝑛 · π)) =
(cos‘(((2 · 𝑦)
+ 1) · π))) |
117 | 108, 114,
116 | fsump1 14487 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ →
Σ𝑛 ∈ (1...((2
· 𝑦) +
1))(cos‘(𝑛 ·
π)) = (Σ𝑛 ∈
(1...(2 · 𝑦))(cos‘(𝑛 · π)) + (cos‘(((2 ·
𝑦) + 1) ·
π)))) |
118 | 33, 99 | eqtr4i 2647 |
. . . . . . . . . . . . 13
⊢ (1 + 1) =
(2 · 1) |
119 | 118 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → (1 + 1) =
(2 · 1)) |
120 | 119 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) + (1 + 1)) =
((2 · 𝑦) + (2
· 1))) |
121 | 120, 62, 60 | 3eqtr4d 2666 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → (((2
· 𝑦) + 1) + 1) = (2
· (𝑦 +
1))) |
122 | 121 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → ((((2
· 𝑦) + 1) + 1)
· π) = ((2 · (𝑦 + 1)) · π)) |
123 | 122 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ →
(cos‘((((2 · 𝑦) + 1) + 1) · π)) = (cos‘((2
· (𝑦 + 1)) ·
π))) |
124 | 58, 59 | addcld 10059 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈
ℂ) |
125 | 28 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → π
∈ ℂ) |
126 | 57, 124, 125 | mulassd 10063 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) ·
π) = (2 · ((𝑦 +
1) · π))) |
127 | 126 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (((2
· (𝑦 + 1)) ·
π) / (2 · π)) = ((2 · ((𝑦 + 1) · π)) / (2 ·
π))) |
128 | 124, 125 | mulcld 10060 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → ((𝑦 + 1) · π) ∈
ℂ) |
129 | | 0re 10040 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
130 | | pipos 24212 |
. . . . . . . . . . . . . 14
⊢ 0 <
π |
131 | 129, 130 | gtneii 10149 |
. . . . . . . . . . . . 13
⊢ π ≠
0 |
132 | 131 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → π ≠
0) |
133 | 74 | rpne0d 11877 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → 2 ≠
0) |
134 | 128, 125,
57, 132, 133 | divcan5d 10827 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → ((2
· ((𝑦 + 1) ·
π)) / (2 · π)) = (((𝑦 + 1) · π) /
π)) |
135 | 124, 125,
132 | divcan4d 10807 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (((𝑦 + 1) · π) / π) =
(𝑦 + 1)) |
136 | 127, 134,
135 | 3eqtrd 2660 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → (((2
· (𝑦 + 1)) ·
π) / (2 · π)) = (𝑦 + 1)) |
137 | 81 | peano2zd 11485 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈
ℤ) |
138 | 136, 137 | eqeltrd 2701 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → (((2
· (𝑦 + 1)) ·
π) / (2 · π)) ∈ ℤ) |
139 | | peano2cn 10208 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℂ → (𝑦 + 1) ∈
ℂ) |
140 | 58, 139 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈
ℂ) |
141 | 57, 140 | mulcld 10060 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (2
· (𝑦 + 1)) ∈
ℂ) |
142 | 141, 125 | mulcld 10060 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → ((2
· (𝑦 + 1)) ·
π) ∈ ℂ) |
143 | | coseq1 24274 |
. . . . . . . . . 10
⊢ (((2
· (𝑦 + 1)) ·
π) ∈ ℂ → ((cos‘((2 · (𝑦 + 1)) · π)) = 1 ↔ (((2
· (𝑦 + 1)) ·
π) / (2 · π)) ∈ ℤ)) |
144 | 142, 143 | syl 17 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ →
((cos‘((2 · (𝑦
+ 1)) · π)) = 1 ↔ (((2 · (𝑦 + 1)) · π) / (2 · π))
∈ ℤ)) |
145 | 138, 144 | mpbird 247 |
. . . . . . . 8
⊢ (𝑦 ∈ ℕ →
(cos‘((2 · (𝑦
+ 1)) · π)) = 1) |
146 | 123, 145 | eqtrd 2656 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ →
(cos‘((((2 · 𝑦) + 1) + 1) · π)) =
1) |
147 | 117, 146 | oveq12d 6668 |
. . . . . 6
⊢ (𝑦 ∈ ℕ →
(Σ𝑛 ∈ (1...((2
· 𝑦) +
1))(cos‘(𝑛 ·
π)) + (cos‘((((2 · 𝑦) + 1) + 1) · π))) = ((Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) + (cos‘(((2 ·
𝑦) + 1) · π))) +
1)) |
148 | 147 | adantr 481 |
. . . . 5
⊢ ((𝑦 ∈ ℕ ∧
Σ𝑛 ∈ (1...(2
· 𝑦))(cos‘(𝑛 · π)) = 0) → (Σ𝑛 ∈ (1...((2 · 𝑦) + 1))(cos‘(𝑛 · π)) +
(cos‘((((2 · 𝑦) + 1) + 1) · π))) = ((Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) + (cos‘(((2 ·
𝑦) + 1) · π))) +
1)) |
149 | | simpr 477 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧
Σ𝑛 ∈ (1...(2
· 𝑦))(cos‘(𝑛 · π)) = 0) → Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) = 0) |
150 | 61, 59, 125 | adddird 10065 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → (((2
· 𝑦) + 1) ·
π) = (((2 · 𝑦)
· π) + (1 · π))) |
151 | 61, 125 | mulcld 10060 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) · π)
∈ ℂ) |
152 | 42, 125 | syl5eqel 2705 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → (1
· π) ∈ ℂ) |
153 | 151, 152 | addcomd 10238 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → (((2
· 𝑦) · π)
+ (1 · π)) = ((1 · π) + ((2 · 𝑦) · π))) |
154 | 42 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → (1
· π) = π) |
155 | 57, 58 | mulcomd 10061 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → (2
· 𝑦) = (𝑦 · 2)) |
156 | 155 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) · π)
= ((𝑦 · 2) ·
π)) |
157 | 58, 57, 125 | mulassd 10063 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → ((𝑦 · 2) · π) =
(𝑦 · (2 ·
π))) |
158 | 156, 157 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → ((2
· 𝑦) · π)
= (𝑦 · (2 ·
π))) |
159 | 154, 158 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → ((1
· π) + ((2 · 𝑦) · π)) = (π + (𝑦 · (2 ·
π)))) |
160 | 150, 153,
159 | 3eqtrd 2660 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (((2
· 𝑦) + 1) ·
π) = (π + (𝑦 ·
(2 · π)))) |
161 | 160 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ →
(cos‘(((2 · 𝑦)
+ 1) · π)) = (cos‘(π + (𝑦 · (2 ·
π))))) |
162 | | cosper 24234 |
. . . . . . . . . . 11
⊢ ((π
∈ ℂ ∧ 𝑦
∈ ℤ) → (cos‘(π + (𝑦 · (2 · π)))) =
(cos‘π)) |
163 | 28, 81, 162 | sylancr 695 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ →
(cos‘(π + (𝑦
· (2 · π)))) = (cos‘π)) |
164 | 47 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ →
(cos‘π) = -1) |
165 | 161, 163,
164 | 3eqtrd 2660 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ →
(cos‘(((2 · 𝑦)
+ 1) · π)) = -1) |
166 | 165 | adantr 481 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧
Σ𝑛 ∈ (1...(2
· 𝑦))(cos‘(𝑛 · π)) = 0) → (cos‘(((2
· 𝑦) + 1) ·
π)) = -1) |
167 | 149, 166 | oveq12d 6668 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧
Σ𝑛 ∈ (1...(2
· 𝑦))(cos‘(𝑛 · π)) = 0) → (Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) + (cos‘(((2 ·
𝑦) + 1) · π))) =
(0 + -1)) |
168 | 167 | oveq1d 6665 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ ∧
Σ𝑛 ∈ (1...(2
· 𝑦))(cos‘(𝑛 · π)) = 0) → ((Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) + (cos‘(((2 ·
𝑦) + 1) · π))) +
1) = ((0 + -1) + 1)) |
169 | 51 | addid2i 10224 |
. . . . . . . 8
⊢ (0 + -1)
= -1 |
170 | 169 | oveq1i 6660 |
. . . . . . 7
⊢ ((0 + -1)
+ 1) = (-1 + 1) |
171 | 170, 53 | eqtri 2644 |
. . . . . 6
⊢ ((0 + -1)
+ 1) = 0 |
172 | 168, 171 | syl6eq 2672 |
. . . . 5
⊢ ((𝑦 ∈ ℕ ∧
Σ𝑛 ∈ (1...(2
· 𝑦))(cos‘(𝑛 · π)) = 0) → ((Σ𝑛 ∈ (1...(2 · 𝑦))(cos‘(𝑛 · π)) + (cos‘(((2 ·
𝑦) + 1) · π))) +
1) = 0) |
173 | 148, 172 | eqtrd 2656 |
. . . 4
⊢ ((𝑦 ∈ ℕ ∧
Σ𝑛 ∈ (1...(2
· 𝑦))(cos‘(𝑛 · π)) = 0) → (Σ𝑛 ∈ (1...((2 · 𝑦) + 1))(cos‘(𝑛 · π)) +
(cos‘((((2 · 𝑦) + 1) + 1) · π))) =
0) |
174 | 66, 96, 173 | 3eqtrd 2660 |
. . 3
⊢ ((𝑦 ∈ ℕ ∧
Σ𝑛 ∈ (1...(2
· 𝑦))(cos‘(𝑛 · π)) = 0) → Σ𝑛 ∈ (1...(2 · (𝑦 + 1)))(cos‘(𝑛 · π)) =
0) |
175 | 174 | ex 450 |
. 2
⊢ (𝑦 ∈ ℕ →
(Σ𝑛 ∈ (1...(2
· 𝑦))(cos‘(𝑛 · π)) = 0 → Σ𝑛 ∈ (1...(2 · (𝑦 + 1)))(cos‘(𝑛 · π)) =
0)) |
176 | 4, 8, 12, 16, 55, 175 | nnind 11038 |
1
⊢ (𝐾 ∈ ℕ →
Σ𝑛 ∈ (1...(2
· 𝐾))(cos‘(𝑛 · π)) = 0) |