Proof of Theorem dirkertrigeqlem3
Step | Hyp | Ref
| Expression |
1 | | dirkertrigeqlem3.a |
. . . . . . . . . . . . 13
⊢ 𝐴 = (((2 · 𝐾) + 1) ·
π) |
2 | 1 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝐴 = (((2 · 𝐾) + 1) · π)) |
3 | 2 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 · 𝐴) = (𝑛 · (((2 · 𝐾) + 1) · π))) |
4 | | elfzelz 12213 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℤ) |
5 | 4 | zcnd 11359 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ) |
6 | 5 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℂ) |
7 | | 2cnd 10970 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 2 ∈ ℂ) |
8 | | dirkertrigeqlem3.k |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐾 ∈ ℤ) |
9 | 8 | zcnd 11359 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐾 ∈ ℂ) |
10 | 9 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝐾 ∈ ℂ) |
11 | 7, 10 | mulcld 9939 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (2 · 𝐾) ∈ ℂ) |
12 | | 1cnd 9935 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 1 ∈ ℂ) |
13 | 11, 12 | addcld 9938 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((2 · 𝐾) + 1) ∈ ℂ) |
14 | | picn 24015 |
. . . . . . . . . . . . . 14
⊢ π
∈ ℂ |
15 | 14 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → π ∈
ℂ) |
16 | 13, 15 | mulcld 9939 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((2 · 𝐾) + 1) · π) ∈
ℂ) |
17 | 6, 16 | mulcomd 9940 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 · (((2 · 𝐾) + 1) · π)) = ((((2 ·
𝐾) + 1) · π)
· 𝑛)) |
18 | 13, 15, 6 | mulassd 9942 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((((2 · 𝐾) + 1) · π) · 𝑛) = (((2 · 𝐾) + 1) · (π ·
𝑛))) |
19 | 15, 6 | mulcld 9939 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (π · 𝑛) ∈ ℂ) |
20 | 11, 12, 19 | adddird 9944 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((2 · 𝐾) + 1) · (π · 𝑛)) = (((2 · 𝐾) · (π · 𝑛)) + (1 · (π ·
𝑛)))) |
21 | 11, 19 | mulcld 9939 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((2 · 𝐾) · (π · 𝑛)) ∈ ℂ) |
22 | 12, 19 | mulcld 9939 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (1 · (π · 𝑛)) ∈
ℂ) |
23 | 21, 22 | addcomd 10117 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((2 · 𝐾) · (π · 𝑛)) + (1 · (π · 𝑛))) = ((1 · (π
· 𝑛)) + ((2 ·
𝐾) · (π ·
𝑛)))) |
24 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (1...𝑁) → π ∈
ℂ) |
25 | 24, 5 | mulcld 9939 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (1...𝑁) → (π · 𝑛) ∈ ℂ) |
26 | 25 | mulid2d 9937 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (1...𝑁) → (1 · (π · 𝑛)) = (π · 𝑛)) |
27 | 26 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (1 · (π · 𝑛)) = (π · 𝑛)) |
28 | 7, 10, 15, 6 | mul4d 10127 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((2 · 𝐾) · (π · 𝑛)) = ((2 · π) · (𝐾 · 𝑛))) |
29 | 7, 15 | mulcld 9939 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (2 · π) ∈
ℂ) |
30 | 10, 6 | mulcld 9939 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐾 · 𝑛) ∈ ℂ) |
31 | 29, 30 | mulcomd 9940 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((2 · π) · (𝐾 · 𝑛)) = ((𝐾 · 𝑛) · (2 ·
π))) |
32 | 28, 31 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((2 · 𝐾) · (π · 𝑛)) = ((𝐾 · 𝑛) · (2 ·
π))) |
33 | 27, 32 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1 · (π · 𝑛)) + ((2 · 𝐾) · (π · 𝑛))) = ((π · 𝑛) + ((𝐾 · 𝑛) · (2 ·
π)))) |
34 | 23, 33 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((2 · 𝐾) · (π · 𝑛)) + (1 · (π · 𝑛))) = ((π · 𝑛) + ((𝐾 · 𝑛) · (2 ·
π)))) |
35 | 18, 20, 34 | 3eqtrd 2648 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((((2 · 𝐾) + 1) · π) · 𝑛) = ((π · 𝑛) + ((𝐾 · 𝑛) · (2 ·
π)))) |
36 | 3, 17, 35 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 · 𝐴) = ((π · 𝑛) + ((𝐾 · 𝑛) · (2 ·
π)))) |
37 | 36 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝐴)) = (cos‘((π · 𝑛) + ((𝐾 · 𝑛) · (2 ·
π))))) |
38 | 8 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝐾 ∈ ℤ) |
39 | 4 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℤ) |
40 | 38, 39 | zmulcld 11364 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐾 · 𝑛) ∈ ℤ) |
41 | | cosper 24038 |
. . . . . . . . . 10
⊢ (((π
· 𝑛) ∈ ℂ
∧ (𝐾 · 𝑛) ∈ ℤ) →
(cos‘((π · 𝑛) + ((𝐾 · 𝑛) · (2 · π)))) =
(cos‘(π · 𝑛))) |
42 | 19, 40, 41 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (cos‘((π · 𝑛) + ((𝐾 · 𝑛) · (2 · π)))) =
(cos‘(π · 𝑛))) |
43 | 37, 42 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝐴)) = (cos‘(π · 𝑛))) |
44 | 43 | sumeq2dv 14281 |
. . . . . . 7
⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) = Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛))) |
45 | 44 | oveq2d 6565 |
. . . . . 6
⊢ (𝜑 → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛)))) |
46 | 45 | oveq1d 6564 |
. . . . 5
⊢ (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛))) / π)) |
47 | 46 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛))) / π)) |
48 | | dirkertrigeqlem3.n |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℕ) |
49 | 48 | nncnd 10913 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℂ) |
50 | | 2cnd 10970 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 2 ∈
ℂ) |
51 | | 2ne0 10990 |
. . . . . . . . . . . . . 14
⊢ 2 ≠
0 |
52 | 51 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 2 ≠ 0) |
53 | 49, 50, 52 | divcan2d 10682 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 · (𝑁 / 2)) = 𝑁) |
54 | 53 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 = (2 · (𝑁 / 2))) |
55 | 54 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝜑 → (1...𝑁) = (1...(2 · (𝑁 / 2)))) |
56 | 55 | sumeq1d 14279 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛)) = Σ𝑛 ∈ (1...(2 · (𝑁 / 2)))(cos‘(π · 𝑛))) |
57 | 56 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛)) = Σ𝑛 ∈ (1...(2 · (𝑁 / 2)))(cos‘(π · 𝑛))) |
58 | 14 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (1...(2 · (𝑁 / 2))) → π ∈
ℂ) |
59 | | elfzelz 12213 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (1...(2 · (𝑁 / 2))) → 𝑛 ∈
ℤ) |
60 | 59 | zcnd 11359 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (1...(2 · (𝑁 / 2))) → 𝑛 ∈
ℂ) |
61 | 58, 60 | mulcomd 9940 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (1...(2 · (𝑁 / 2))) → (π ·
𝑛) = (𝑛 · π)) |
62 | 61 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (1...(2 · (𝑁 / 2))) → (cos‘(π
· 𝑛)) =
(cos‘(𝑛 ·
π))) |
63 | 62 | rgen 2906 |
. . . . . . . . . 10
⊢
∀𝑛 ∈
(1...(2 · (𝑁 /
2)))(cos‘(π · 𝑛)) = (cos‘(𝑛 · π)) |
64 | 63 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → ∀𝑛 ∈ (1...(2 · (𝑁 / 2)))(cos‘(π ·
𝑛)) = (cos‘(𝑛 ·
π))) |
65 | 64 | sumeq2d 14280 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → Σ𝑛 ∈ (1...(2 · (𝑁 / 2)))(cos‘(π ·
𝑛)) = Σ𝑛 ∈ (1...(2 · (𝑁 / 2)))(cos‘(𝑛 ·
π))) |
66 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (𝑁 mod 2) = 0) |
67 | 48 | nnred 10912 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℝ) |
68 | 67 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → 𝑁 ∈ ℝ) |
69 | | 2rp 11713 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ+ |
70 | | mod0 12537 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 2 ∈
ℝ+) → ((𝑁 mod 2) = 0 ↔ (𝑁 / 2) ∈ ℤ)) |
71 | 68, 69, 70 | sylancl 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → ((𝑁 mod 2) = 0 ↔ (𝑁 / 2) ∈ ℤ)) |
72 | 66, 71 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (𝑁 / 2) ∈ ℤ) |
73 | | 2re 10967 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
74 | 73 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ∈
ℝ) |
75 | 48 | nngt0d 10941 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 𝑁) |
76 | | 2pos 10989 |
. . . . . . . . . . . . 13
⊢ 0 <
2 |
77 | 76 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 2) |
78 | 67, 74, 75, 77 | divgt0d 10838 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < (𝑁 / 2)) |
79 | 78 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → 0 < (𝑁 / 2)) |
80 | | elnnz 11264 |
. . . . . . . . . 10
⊢ ((𝑁 / 2) ∈ ℕ ↔
((𝑁 / 2) ∈ ℤ
∧ 0 < (𝑁 /
2))) |
81 | 72, 79, 80 | sylanbrc 695 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (𝑁 / 2) ∈ ℕ) |
82 | | dirkertrigeqlem1 38991 |
. . . . . . . . 9
⊢ ((𝑁 / 2) ∈ ℕ →
Σ𝑛 ∈ (1...(2
· (𝑁 /
2)))(cos‘(𝑛 ·
π)) = 0) |
83 | 81, 82 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → Σ𝑛 ∈ (1...(2 · (𝑁 / 2)))(cos‘(𝑛 · π)) =
0) |
84 | 57, 65, 83 | 3eqtrd 2648 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛)) = 0) |
85 | 84 | oveq2d 6565 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛))) = ((1 / 2) +
0)) |
86 | | halfcn 11124 |
. . . . . . 7
⊢ (1 / 2)
∈ ℂ |
87 | 86 | addid1i 10102 |
. . . . . 6
⊢ ((1 / 2)
+ 0) = (1 / 2) |
88 | 85, 87 | syl6eq 2660 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛))) = (1 / 2)) |
89 | 88 | oveq1d 6564 |
. . . 4
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛))) / π) = ((1 / 2) /
π)) |
90 | | ax-1cn 9873 |
. . . . . 6
⊢ 1 ∈
ℂ |
91 | | 2cnne0 11119 |
. . . . . 6
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
92 | | pire 24014 |
. . . . . . . 8
⊢ π
∈ ℝ |
93 | | pipos 24016 |
. . . . . . . 8
⊢ 0 <
π |
94 | 92, 93 | gt0ne0ii 10443 |
. . . . . . 7
⊢ π ≠
0 |
95 | 14, 94 | pm3.2i 470 |
. . . . . 6
⊢ (π
∈ ℂ ∧ π ≠ 0) |
96 | | divdiv1 10615 |
. . . . . 6
⊢ ((1
∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (π ∈
ℂ ∧ π ≠ 0)) → ((1 / 2) / π) = (1 / (2 ·
π))) |
97 | 90, 91, 95, 96 | mp3an 1416 |
. . . . 5
⊢ ((1 / 2)
/ π) = (1 / (2 · π)) |
98 | 97 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → ((1 / 2) / π) = (1 /
(2 · π))) |
99 | 47, 89, 98 | 3eqtrd 2648 |
. . 3
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = (1 / (2 ·
π))) |
100 | 1 | oveq2i 6560 |
. . . . . . . . . 10
⊢ ((𝑁 + (1 / 2)) · 𝐴) = ((𝑁 + (1 / 2)) · (((2 · 𝐾) + 1) ·
π)) |
101 | 100 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝐴) = ((𝑁 + (1 / 2)) · (((2 · 𝐾) + 1) ·
π))) |
102 | 86 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 / 2) ∈
ℂ) |
103 | 49, 102 | addcld 9938 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 + (1 / 2)) ∈ ℂ) |
104 | 50, 9 | mulcld 9939 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · 𝐾) ∈
ℂ) |
105 | | peano2cn 10087 |
. . . . . . . . . . 11
⊢ ((2
· 𝐾) ∈ ℂ
→ ((2 · 𝐾) + 1)
∈ ℂ) |
106 | 104, 105 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((2 · 𝐾) + 1) ∈
ℂ) |
107 | 14 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → π ∈
ℂ) |
108 | 103, 106,
107 | mulassd 9942 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑁 + (1 / 2)) · ((2 · 𝐾) + 1)) · π) = ((𝑁 + (1 / 2)) · (((2
· 𝐾) + 1) ·
π))) |
109 | | 1cnd 9935 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ∈
ℂ) |
110 | 49, 102, 104, 109 | muladdd 10368 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑁 + (1 / 2)) · ((2 · 𝐾) + 1)) = (((𝑁 · (2 · 𝐾)) + (1 · (1 / 2))) + ((𝑁 · 1) + ((2 ·
𝐾) · (1 /
2))))) |
111 | 49, 50, 9 | mul12d 10124 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 · (2 · 𝐾)) = (2 · (𝑁 · 𝐾))) |
112 | 102 | mulid2d 9937 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 · (1 / 2)) = (1
/ 2)) |
113 | 111, 112 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 · (2 · 𝐾)) + (1 · (1 / 2))) = ((2 ·
(𝑁 · 𝐾)) + (1 / 2))) |
114 | 49 | mulid1d 9936 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 · 1) = 𝑁) |
115 | 50, 9 | mulcomd 9940 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 · 𝐾) = (𝐾 · 2)) |
116 | 115 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2 · 𝐾) · (1 / 2)) = ((𝐾 · 2) · (1 /
2))) |
117 | 9, 50, 102 | mulassd 9942 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐾 · 2) · (1 / 2)) = (𝐾 · (2 · (1 /
2)))) |
118 | | 2cn 10968 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℂ |
119 | 118, 51 | recidi 10635 |
. . . . . . . . . . . . . . . . . 18
⊢ (2
· (1 / 2)) = 1 |
120 | 119 | oveq2i 6560 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 · (2 · (1 / 2)))
= (𝐾 ·
1) |
121 | 9 | mulid1d 9936 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐾 · 1) = 𝐾) |
122 | 120, 121 | syl5eq 2656 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐾 · (2 · (1 / 2))) = 𝐾) |
123 | 116, 117,
122 | 3eqtrd 2648 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2 · 𝐾) · (1 / 2)) = 𝐾) |
124 | 114, 123 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 · 1) + ((2 · 𝐾) · (1 / 2))) = (𝑁 + 𝐾)) |
125 | 113, 124 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑁 · (2 · 𝐾)) + (1 · (1 / 2))) + ((𝑁 · 1) + ((2 ·
𝐾) · (1 / 2)))) =
(((2 · (𝑁 ·
𝐾)) + (1 / 2)) + (𝑁 + 𝐾))) |
126 | 49, 9 | mulcld 9939 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 · 𝐾) ∈ ℂ) |
127 | 50, 126 | mulcld 9939 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (2 · (𝑁 · 𝐾)) ∈ ℂ) |
128 | 49, 9 | addcld 9938 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 + 𝐾) ∈ ℂ) |
129 | 127, 102,
128 | addassd 9941 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((2 · (𝑁 · 𝐾)) + (1 / 2)) + (𝑁 + 𝐾)) = ((2 · (𝑁 · 𝐾)) + ((1 / 2) + (𝑁 + 𝐾)))) |
130 | 110, 125,
129 | 3eqtrd 2648 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁 + (1 / 2)) · ((2 · 𝐾) + 1)) = ((2 · (𝑁 · 𝐾)) + ((1 / 2) + (𝑁 + 𝐾)))) |
131 | 102, 128 | addcld 9938 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((1 / 2) + (𝑁 + 𝐾)) ∈ ℂ) |
132 | 127, 131 | addcomd 10117 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · (𝑁 · 𝐾)) + ((1 / 2) + (𝑁 + 𝐾))) = (((1 / 2) + (𝑁 + 𝐾)) + (2 · (𝑁 · 𝐾)))) |
133 | 50, 126 | mulcomd 9940 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 · (𝑁 · 𝐾)) = ((𝑁 · 𝐾) · 2)) |
134 | 133 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((1 / 2) + (𝑁 + 𝐾)) + (2 · (𝑁 · 𝐾))) = (((1 / 2) + (𝑁 + 𝐾)) + ((𝑁 · 𝐾) · 2))) |
135 | 130, 132,
134 | 3eqtrd 2648 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 + (1 / 2)) · ((2 · 𝐾) + 1)) = (((1 / 2) + (𝑁 + 𝐾)) + ((𝑁 · 𝐾) · 2))) |
136 | 135 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑁 + (1 / 2)) · ((2 · 𝐾) + 1)) · π) = ((((1 /
2) + (𝑁 + 𝐾)) + ((𝑁 · 𝐾) · 2)) ·
π)) |
137 | 126, 50 | mulcld 9939 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 · 𝐾) · 2) ∈
ℂ) |
138 | 131, 137,
107 | adddird 9944 |
. . . . . . . . . 10
⊢ (𝜑 → ((((1 / 2) + (𝑁 + 𝐾)) + ((𝑁 · 𝐾) · 2)) · π) = ((((1 / 2) +
(𝑁 + 𝐾)) · π) + (((𝑁 · 𝐾) · 2) ·
π))) |
139 | 126, 50, 107 | mulassd 9942 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑁 · 𝐾) · 2) · π) = ((𝑁 · 𝐾) · (2 ·
π))) |
140 | 139 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝜑 → ((((1 / 2) + (𝑁 + 𝐾)) · π) + (((𝑁 · 𝐾) · 2) · π)) = ((((1 / 2) +
(𝑁 + 𝐾)) · π) + ((𝑁 · 𝐾) · (2 ·
π)))) |
141 | 136, 138,
140 | 3eqtrd 2648 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑁 + (1 / 2)) · ((2 · 𝐾) + 1)) · π) = ((((1 /
2) + (𝑁 + 𝐾)) · π) + ((𝑁 · 𝐾) · (2 ·
π)))) |
142 | 101, 108,
141 | 3eqtr2d 2650 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝐴) = ((((1 / 2) + (𝑁 + 𝐾)) · π) + ((𝑁 · 𝐾) · (2 ·
π)))) |
143 | 142 | fveq2d 6107 |
. . . . . . 7
⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝐴)) = (sin‘((((1 / 2) +
(𝑁 + 𝐾)) · π) + ((𝑁 · 𝐾) · (2 ·
π))))) |
144 | 131, 107 | mulcld 9939 |
. . . . . . . 8
⊢ (𝜑 → (((1 / 2) + (𝑁 + 𝐾)) · π) ∈
ℂ) |
145 | 48 | nnzd 11357 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℤ) |
146 | 145, 8 | zmulcld 11364 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 · 𝐾) ∈ ℤ) |
147 | | sinper 24037 |
. . . . . . . 8
⊢ (((((1 /
2) + (𝑁 + 𝐾)) · π) ∈ ℂ ∧
(𝑁 · 𝐾) ∈ ℤ) →
(sin‘((((1 / 2) + (𝑁
+ 𝐾)) · π) +
((𝑁 · 𝐾) · (2 · π))))
= (sin‘(((1 / 2) + (𝑁
+ 𝐾)) ·
π))) |
148 | 144, 146,
147 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (sin‘((((1 / 2) +
(𝑁 + 𝐾)) · π) + ((𝑁 · 𝐾) · (2 · π)))) =
(sin‘(((1 / 2) + (𝑁 +
𝐾)) ·
π))) |
149 | 102, 128 | addcomd 10117 |
. . . . . . . . . 10
⊢ (𝜑 → ((1 / 2) + (𝑁 + 𝐾)) = ((𝑁 + 𝐾) + (1 / 2))) |
150 | 49, 9, 102 | addassd 9941 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁 + 𝐾) + (1 / 2)) = (𝑁 + (𝐾 + (1 / 2)))) |
151 | 9, 102 | addcld 9938 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾 + (1 / 2)) ∈ ℂ) |
152 | 49, 151 | addcomd 10117 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 + (𝐾 + (1 / 2))) = ((𝐾 + (1 / 2)) + 𝑁)) |
153 | 149, 150,
152 | 3eqtrd 2648 |
. . . . . . . . 9
⊢ (𝜑 → ((1 / 2) + (𝑁 + 𝐾)) = ((𝐾 + (1 / 2)) + 𝑁)) |
154 | 153 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝜑 → (((1 / 2) + (𝑁 + 𝐾)) · π) = (((𝐾 + (1 / 2)) + 𝑁) · π)) |
155 | 154 | fveq2d 6107 |
. . . . . . 7
⊢ (𝜑 → (sin‘(((1 / 2) +
(𝑁 + 𝐾)) · π)) = (sin‘(((𝐾 + (1 / 2)) + 𝑁) · π))) |
156 | 143, 148,
155 | 3eqtrd 2648 |
. . . . . 6
⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝐴)) = (sin‘(((𝐾 + (1 / 2)) + 𝑁) · π))) |
157 | 1 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 = (((2 · 𝐾) + 1) · π)) |
158 | 157 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 / 2) = ((((2 · 𝐾) + 1) · π) / 2)) |
159 | 106, 107,
50, 52 | div23d 10717 |
. . . . . . . . 9
⊢ (𝜑 → ((((2 · 𝐾) + 1) · π) / 2) =
((((2 · 𝐾) + 1) / 2)
· π)) |
160 | 104, 109,
50, 52 | divdird 10718 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2 · 𝐾) + 1) / 2) = (((2 ·
𝐾) / 2) + (1 /
2))) |
161 | 9, 50, 52 | divcan3d 10685 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · 𝐾) / 2) = 𝐾) |
162 | 161 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2 · 𝐾) / 2) + (1 / 2)) = (𝐾 + (1 / 2))) |
163 | 160, 162 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝜑 → (((2 · 𝐾) + 1) / 2) = (𝐾 + (1 / 2))) |
164 | 163 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝜑 → ((((2 · 𝐾) + 1) / 2) · π) =
((𝐾 + (1 / 2)) ·
π)) |
165 | 158, 159,
164 | 3eqtrd 2648 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 / 2) = ((𝐾 + (1 / 2)) · π)) |
166 | 165 | fveq2d 6107 |
. . . . . . 7
⊢ (𝜑 → (sin‘(𝐴 / 2)) = (sin‘((𝐾 + (1 / 2)) ·
π))) |
167 | 166 | oveq2d 6565 |
. . . . . 6
⊢ (𝜑 → ((2 · π)
· (sin‘(𝐴 /
2))) = ((2 · π) · (sin‘((𝐾 + (1 / 2)) ·
π)))) |
168 | 156, 167 | oveq12d 6567 |
. . . . 5
⊢ (𝜑 → ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) ·
(sin‘(𝐴 / 2)))) =
((sin‘(((𝐾 + (1 / 2))
+ 𝑁) · π)) / ((2
· π) · (sin‘((𝐾 + (1 / 2)) ·
π))))) |
169 | 168 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) ·
(sin‘(𝐴 / 2)))) =
((sin‘(((𝐾 + (1 / 2))
+ 𝑁) · π)) / ((2
· π) · (sin‘((𝐾 + (1 / 2)) ·
π))))) |
170 | 151, 49, 107 | adddird 9944 |
. . . . . . 7
⊢ (𝜑 → (((𝐾 + (1 / 2)) + 𝑁) · π) = (((𝐾 + (1 / 2)) · π) + (𝑁 ·
π))) |
171 | 170 | fveq2d 6107 |
. . . . . 6
⊢ (𝜑 → (sin‘(((𝐾 + (1 / 2)) + 𝑁) · π)) = (sin‘(((𝐾 + (1 / 2)) · π) +
(𝑁 ·
π)))) |
172 | 171 | oveq1d 6564 |
. . . . 5
⊢ (𝜑 → ((sin‘(((𝐾 + (1 / 2)) + 𝑁) · π)) / ((2 · π)
· (sin‘((𝐾 +
(1 / 2)) · π)))) = ((sin‘(((𝐾 + (1 / 2)) · π) + (𝑁 · π))) / ((2 ·
π) · (sin‘((𝐾 + (1 / 2)) ·
π))))) |
173 | 172 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → ((sin‘(((𝐾 + (1 / 2)) + 𝑁) · π)) / ((2 · π)
· (sin‘((𝐾 +
(1 / 2)) · π)))) = ((sin‘(((𝐾 + (1 / 2)) · π) + (𝑁 · π))) / ((2 ·
π) · (sin‘((𝐾 + (1 / 2)) ·
π))))) |
174 | 49 | halfcld 11154 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 / 2) ∈ ℂ) |
175 | 50, 174 | mulcomd 9940 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 · (𝑁 / 2)) = ((𝑁 / 2) · 2)) |
176 | 53, 175 | eqtr3d 2646 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 = ((𝑁 / 2) · 2)) |
177 | 176 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 · π) = (((𝑁 / 2) · 2) ·
π)) |
178 | 174, 50, 107 | mulassd 9942 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑁 / 2) · 2) · π) = ((𝑁 / 2) · (2 ·
π))) |
179 | 177, 178 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 · π) = ((𝑁 / 2) · (2 ·
π))) |
180 | 179 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐾 + (1 / 2)) · π) + (𝑁 · π)) = (((𝐾 + (1 / 2)) · π) +
((𝑁 / 2) · (2
· π)))) |
181 | 180 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝜑 → (sin‘(((𝐾 + (1 / 2)) · π) +
(𝑁 · π))) =
(sin‘(((𝐾 + (1 / 2))
· π) + ((𝑁 / 2)
· (2 · π))))) |
182 | 181 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (sin‘(((𝐾 + (1 / 2)) · π) +
(𝑁 · π))) =
(sin‘(((𝐾 + (1 / 2))
· π) + ((𝑁 / 2)
· (2 · π))))) |
183 | 9 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → 𝐾 ∈ ℂ) |
184 | | 1cnd 9935 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → 1 ∈
ℂ) |
185 | 184 | halfcld 11154 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (1 / 2) ∈
ℂ) |
186 | 183, 185 | addcld 9938 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (𝐾 + (1 / 2)) ∈ ℂ) |
187 | 14 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → π ∈
ℂ) |
188 | 186, 187 | mulcld 9939 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → ((𝐾 + (1 / 2)) · π) ∈
ℂ) |
189 | | sinper 24037 |
. . . . . . . 8
⊢ ((((𝐾 + (1 / 2)) · π)
∈ ℂ ∧ (𝑁 /
2) ∈ ℤ) → (sin‘(((𝐾 + (1 / 2)) · π) + ((𝑁 / 2) · (2 ·
π)))) = (sin‘((𝐾 +
(1 / 2)) · π))) |
190 | 188, 72, 189 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (sin‘(((𝐾 + (1 / 2)) · π) +
((𝑁 / 2) · (2
· π)))) = (sin‘((𝐾 + (1 / 2)) ·
π))) |
191 | 182, 190 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (sin‘(((𝐾 + (1 / 2)) · π) +
(𝑁 · π))) =
(sin‘((𝐾 + (1 / 2))
· π))) |
192 | 50, 107 | mulcld 9939 |
. . . . . . . 8
⊢ (𝜑 → (2 · π) ∈
ℂ) |
193 | 151, 107 | mulcld 9939 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐾 + (1 / 2)) · π) ∈
ℂ) |
194 | 193 | sincld 14699 |
. . . . . . . 8
⊢ (𝜑 → (sin‘((𝐾 + (1 / 2)) · π))
∈ ℂ) |
195 | 192, 194 | mulcomd 9940 |
. . . . . . 7
⊢ (𝜑 → ((2 · π)
· (sin‘((𝐾 +
(1 / 2)) · π))) = ((sin‘((𝐾 + (1 / 2)) · π)) · (2
· π))) |
196 | 195 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → ((2 · π)
· (sin‘((𝐾 +
(1 / 2)) · π))) = ((sin‘((𝐾 + (1 / 2)) · π)) · (2
· π))) |
197 | 191, 196 | oveq12d 6567 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → ((sin‘(((𝐾 + (1 / 2)) · π) +
(𝑁 · π))) / ((2
· π) · (sin‘((𝐾 + (1 / 2)) · π)))) =
((sin‘((𝐾 + (1 / 2))
· π)) / ((sin‘((𝐾 + (1 / 2)) · π)) · (2
· π)))) |
198 | 94 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → π ≠
0) |
199 | 151, 107,
198 | divcan4d 10686 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐾 + (1 / 2)) · π) / π) = (𝐾 + (1 / 2))) |
200 | 8 | zred 11358 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ ℝ) |
201 | 69 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ∈
ℝ+) |
202 | 201 | rpreccld 11758 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 / 2) ∈
ℝ+) |
203 | 200, 202 | ltaddrpd 11781 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 < (𝐾 + (1 / 2))) |
204 | | 1red 9934 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ∈
ℝ) |
205 | 204 | rehalfcld 11156 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 / 2) ∈
ℝ) |
206 | | halflt1 11127 |
. . . . . . . . . . . . . 14
⊢ (1 / 2)
< 1 |
207 | 206 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 / 2) <
1) |
208 | 205, 204,
200, 207 | ltadd2dd 10075 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐾 + (1 / 2)) < (𝐾 + 1)) |
209 | | btwnnz 11329 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℤ ∧ 𝐾 < (𝐾 + (1 / 2)) ∧ (𝐾 + (1 / 2)) < (𝐾 + 1)) → ¬ (𝐾 + (1 / 2)) ∈ ℤ) |
210 | 8, 203, 208, 209 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ (𝐾 + (1 / 2)) ∈ ℤ) |
211 | 199, 210 | eqneltrd 2707 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ (((𝐾 + (1 / 2)) · π) / π) ∈
ℤ) |
212 | | sineq0 24077 |
. . . . . . . . . . 11
⊢ (((𝐾 + (1 / 2)) · π)
∈ ℂ → ((sin‘((𝐾 + (1 / 2)) · π)) = 0 ↔
(((𝐾 + (1 / 2)) ·
π) / π) ∈ ℤ)) |
213 | 193, 212 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((sin‘((𝐾 + (1 / 2)) · π)) = 0
↔ (((𝐾 + (1 / 2))
· π) / π) ∈ ℤ)) |
214 | 211, 213 | mtbird 314 |
. . . . . . . . 9
⊢ (𝜑 → ¬ (sin‘((𝐾 + (1 / 2)) · π)) =
0) |
215 | 214 | neqned 2789 |
. . . . . . . 8
⊢ (𝜑 → (sin‘((𝐾 + (1 / 2)) · π)) ≠
0) |
216 | 50, 107, 52, 198 | mulne0d 10558 |
. . . . . . . 8
⊢ (𝜑 → (2 · π) ≠
0) |
217 | 194, 194,
192, 215, 216 | divdiv1d 10711 |
. . . . . . 7
⊢ (𝜑 → (((sin‘((𝐾 + (1 / 2)) · π)) /
(sin‘((𝐾 + (1 / 2))
· π))) / (2 · π)) = ((sin‘((𝐾 + (1 / 2)) · π)) /
((sin‘((𝐾 + (1 / 2))
· π)) · (2 · π)))) |
218 | 194, 215 | dividd 10678 |
. . . . . . . 8
⊢ (𝜑 → ((sin‘((𝐾 + (1 / 2)) · π)) /
(sin‘((𝐾 + (1 / 2))
· π))) = 1) |
219 | 218 | oveq1d 6564 |
. . . . . . 7
⊢ (𝜑 → (((sin‘((𝐾 + (1 / 2)) · π)) /
(sin‘((𝐾 + (1 / 2))
· π))) / (2 · π)) = (1 / (2 ·
π))) |
220 | 217, 219 | eqtr3d 2646 |
. . . . . 6
⊢ (𝜑 → ((sin‘((𝐾 + (1 / 2)) · π)) /
((sin‘((𝐾 + (1 / 2))
· π)) · (2 · π))) = (1 / (2 ·
π))) |
221 | 220 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → ((sin‘((𝐾 + (1 / 2)) · π)) /
((sin‘((𝐾 + (1 / 2))
· π)) · (2 · π))) = (1 / (2 ·
π))) |
222 | 197, 221 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → ((sin‘(((𝐾 + (1 / 2)) · π) +
(𝑁 · π))) / ((2
· π) · (sin‘((𝐾 + (1 / 2)) · π)))) = (1 / (2
· π))) |
223 | 169, 173,
222 | 3eqtrrd 2649 |
. . 3
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (1 / (2 · π))
= ((sin‘((𝑁 + (1 /
2)) · 𝐴)) / ((2
· π) · (sin‘(𝐴 / 2))))) |
224 | 99, 223 | eqtrd 2644 |
. 2
⊢ ((𝜑 ∧ (𝑁 mod 2) = 0) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) ·
(sin‘(𝐴 /
2))))) |
225 | 46 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛))) / π)) |
226 | 145 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → 𝑁 ∈ ℤ) |
227 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → ¬ (𝑁 mod 2) = 0) |
228 | 227 | neqned 2789 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (𝑁 mod 2) ≠ 0) |
229 | | oddfl 38430 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ (𝑁 mod 2) ≠ 0) → 𝑁 = ((2 ·
(⌊‘(𝑁 / 2))) +
1)) |
230 | 226, 228,
229 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → 𝑁 = ((2 · (⌊‘(𝑁 / 2))) + 1)) |
231 | 230 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (1...𝑁) = (1...((2 · (⌊‘(𝑁 / 2))) + 1))) |
232 | 231 | sumeq1d 14279 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛)) = Σ𝑛 ∈ (1...((2 ·
(⌊‘(𝑁 / 2))) +
1))(cos‘(π · 𝑛))) |
233 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 = 1 → (𝑁 / 2) = (1 / 2)) |
234 | 233 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 = 1 →
(⌊‘(𝑁 / 2)) =
(⌊‘(1 / 2))) |
235 | | halffl 38451 |
. . . . . . . . . . . . . . . . 17
⊢
(⌊‘(1 / 2)) = 0 |
236 | 234, 235 | syl6eq 2660 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 = 1 →
(⌊‘(𝑁 / 2)) =
0) |
237 | 236 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 = 1 → (2 ·
(⌊‘(𝑁 / 2))) =
(2 · 0)) |
238 | | 2t0e0 11060 |
. . . . . . . . . . . . . . 15
⊢ (2
· 0) = 0 |
239 | 237, 238 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ (𝑁 = 1 → (2 ·
(⌊‘(𝑁 / 2))) =
0) |
240 | 239 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑁 = 1 → ((2 ·
(⌊‘(𝑁 / 2))) +
1) = (0 + 1)) |
241 | 90 | addid2i 10103 |
. . . . . . . . . . . . 13
⊢ (0 + 1) =
1 |
242 | 240, 241 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (𝑁 = 1 → ((2 ·
(⌊‘(𝑁 / 2))) +
1) = 1) |
243 | 242 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑁 = 1 → (1...((2 ·
(⌊‘(𝑁 / 2))) +
1)) = (1...1)) |
244 | 243 | sumeq1d 14279 |
. . . . . . . . . 10
⊢ (𝑁 = 1 → Σ𝑛 ∈ (1...((2 ·
(⌊‘(𝑁 / 2))) +
1))(cos‘(π · 𝑛)) = Σ𝑛 ∈ (1...1)(cos‘(π ·
𝑛))) |
245 | | 1z 11284 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
246 | | coscl 14696 |
. . . . . . . . . . . . 13
⊢ (π
∈ ℂ → (cos‘π) ∈ ℂ) |
247 | 14, 246 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(cos‘π) ∈ ℂ |
248 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 1 → (π · 𝑛) = (π ·
1)) |
249 | 14 | mulid1i 9921 |
. . . . . . . . . . . . . . 15
⊢ (π
· 1) = π |
250 | 248, 249 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 1 → (π · 𝑛) = π) |
251 | 250 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 1 → (cos‘(π
· 𝑛)) =
(cos‘π)) |
252 | 251 | fsum1 14320 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℤ ∧ (cos‘π) ∈ ℂ) → Σ𝑛 ∈ (1...1)(cos‘(π
· 𝑛)) =
(cos‘π)) |
253 | 245, 247,
252 | mp2an 704 |
. . . . . . . . . . 11
⊢
Σ𝑛 ∈
(1...1)(cos‘(π · 𝑛)) = (cos‘π) |
254 | 253 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 = 1 → Σ𝑛 ∈ (1...1)(cos‘(π
· 𝑛)) =
(cos‘π)) |
255 | | cospi 24028 |
. . . . . . . . . . 11
⊢
(cos‘π) = -1 |
256 | 255 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 = 1 → (cos‘π) =
-1) |
257 | 244, 254,
256 | 3eqtrd 2648 |
. . . . . . . . 9
⊢ (𝑁 = 1 → Σ𝑛 ∈ (1...((2 ·
(⌊‘(𝑁 / 2))) +
1))(cos‘(π · 𝑛)) = -1) |
258 | 257 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 = 1) → Σ𝑛 ∈ (1...((2 ·
(⌊‘(𝑁 / 2))) +
1))(cos‘(π · 𝑛)) = -1) |
259 | | 2nn 11062 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ |
260 | 259 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → 2 ∈
ℕ) |
261 | 67 | rehalfcld 11156 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 / 2) ∈ ℝ) |
262 | 261 | flcld 12461 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (⌊‘(𝑁 / 2)) ∈
ℤ) |
263 | 262 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → (⌊‘(𝑁 / 2)) ∈
ℤ) |
264 | | 2div2e1 11027 |
. . . . . . . . . . . . . . 15
⊢ (2 / 2) =
1 |
265 | 73 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → 2 ∈
ℝ) |
266 | 67 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → 𝑁 ∈ ℝ) |
267 | 69 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → 2 ∈
ℝ+) |
268 | | neqne 2790 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑁 = 1 → 𝑁 ≠ 1) |
269 | | nnne1ge2 38445 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 ≠ 1) → 2 ≤ 𝑁) |
270 | 48, 268, 269 | syl2an 493 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → 2 ≤ 𝑁) |
271 | 265, 266,
267, 270 | lediv1dd 11806 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → (2 / 2) ≤ (𝑁 / 2)) |
272 | 264, 271 | syl5eqbrr 4619 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → 1 ≤ (𝑁 / 2)) |
273 | 261 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → (𝑁 / 2) ∈ ℝ) |
274 | | flge 12468 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 / 2) ∈ ℝ ∧ 1
∈ ℤ) → (1 ≤ (𝑁 / 2) ↔ 1 ≤ (⌊‘(𝑁 / 2)))) |
275 | 273, 245,
274 | sylancl 693 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → (1 ≤ (𝑁 / 2) ↔ 1 ≤ (⌊‘(𝑁 / 2)))) |
276 | 272, 275 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → 1 ≤ (⌊‘(𝑁 / 2))) |
277 | | elnnz1 11280 |
. . . . . . . . . . . . 13
⊢
((⌊‘(𝑁 /
2)) ∈ ℕ ↔ ((⌊‘(𝑁 / 2)) ∈ ℤ ∧ 1 ≤
(⌊‘(𝑁 /
2)))) |
278 | 263, 276,
277 | sylanbrc 695 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → (⌊‘(𝑁 / 2)) ∈
ℕ) |
279 | 260, 278 | nnmulcld 10945 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → (2 ·
(⌊‘(𝑁 / 2)))
∈ ℕ) |
280 | | nnuz 11599 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
281 | 279, 280 | syl6eleq 2698 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → (2 ·
(⌊‘(𝑁 / 2)))
∈ (ℤ≥‘1)) |
282 | 14 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ 𝑁 = 1) ∧ 𝑛 ∈ (1...((2 ·
(⌊‘(𝑁 / 2))) +
1))) → π ∈ ℂ) |
283 | | elfzelz 12213 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (1...((2 ·
(⌊‘(𝑁 / 2))) +
1)) → 𝑛 ∈
ℤ) |
284 | 283 | zcnd 11359 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (1...((2 ·
(⌊‘(𝑁 / 2))) +
1)) → 𝑛 ∈
ℂ) |
285 | 284 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ 𝑁 = 1) ∧ 𝑛 ∈ (1...((2 ·
(⌊‘(𝑁 / 2))) +
1))) → 𝑛 ∈
ℂ) |
286 | 282, 285 | mulcld 9939 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ 𝑁 = 1) ∧ 𝑛 ∈ (1...((2 ·
(⌊‘(𝑁 / 2))) +
1))) → (π · 𝑛) ∈ ℂ) |
287 | 286 | coscld 14700 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ 𝑁 = 1) ∧ 𝑛 ∈ (1...((2 ·
(⌊‘(𝑁 / 2))) +
1))) → (cos‘(π · 𝑛)) ∈ ℂ) |
288 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑛 = ((2 ·
(⌊‘(𝑁 / 2))) +
1) → (π · 𝑛)
= (π · ((2 · (⌊‘(𝑁 / 2))) + 1))) |
289 | 288 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑛 = ((2 ·
(⌊‘(𝑁 / 2))) +
1) → (cos‘(π · 𝑛)) = (cos‘(π · ((2 ·
(⌊‘(𝑁 / 2))) +
1)))) |
290 | 281, 287,
289 | fsump1 14329 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → Σ𝑛 ∈ (1...((2 ·
(⌊‘(𝑁 / 2))) +
1))(cos‘(π · 𝑛)) = (Σ𝑛 ∈ (1...(2 ·
(⌊‘(𝑁 /
2))))(cos‘(π · 𝑛)) + (cos‘(π · ((2 ·
(⌊‘(𝑁 / 2))) +
1))))) |
291 | 14 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (1...(2 ·
(⌊‘(𝑁 / 2))))
→ π ∈ ℂ) |
292 | | elfzelz 12213 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (1...(2 ·
(⌊‘(𝑁 / 2))))
→ 𝑛 ∈
ℤ) |
293 | 292 | zcnd 11359 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (1...(2 ·
(⌊‘(𝑁 / 2))))
→ 𝑛 ∈
ℂ) |
294 | 291, 293 | mulcomd 9940 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (1...(2 ·
(⌊‘(𝑁 / 2))))
→ (π · 𝑛) =
(𝑛 ·
π)) |
295 | 294 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (1...(2 ·
(⌊‘(𝑁 / 2))))
→ (cos‘(π · 𝑛)) = (cos‘(𝑛 · π))) |
296 | 295 | sumeq2i 14277 |
. . . . . . . . . . 11
⊢
Σ𝑛 ∈
(1...(2 · (⌊‘(𝑁 / 2))))(cos‘(π · 𝑛)) = Σ𝑛 ∈ (1...(2 ·
(⌊‘(𝑁 /
2))))(cos‘(𝑛 ·
π)) |
297 | | dirkertrigeqlem1 38991 |
. . . . . . . . . . . 12
⊢
((⌊‘(𝑁 /
2)) ∈ ℕ → Σ𝑛 ∈ (1...(2 ·
(⌊‘(𝑁 /
2))))(cos‘(𝑛 ·
π)) = 0) |
298 | 278, 297 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → Σ𝑛 ∈ (1...(2 ·
(⌊‘(𝑁 /
2))))(cos‘(𝑛 ·
π)) = 0) |
299 | 296, 298 | syl5eq 2656 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → Σ𝑛 ∈ (1...(2 ·
(⌊‘(𝑁 /
2))))(cos‘(π · 𝑛)) = 0) |
300 | 262 | zcnd 11359 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (⌊‘(𝑁 / 2)) ∈
ℂ) |
301 | 50, 300 | mulcld 9939 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2 ·
(⌊‘(𝑁 / 2)))
∈ ℂ) |
302 | 107, 301,
109 | adddid 9943 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (π · ((2
· (⌊‘(𝑁
/ 2))) + 1)) = ((π · (2 · (⌊‘(𝑁 / 2)))) + (π ·
1))) |
303 | 107, 50, 300 | mul13d 38432 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (π · (2 ·
(⌊‘(𝑁 / 2)))) =
((⌊‘(𝑁 / 2))
· (2 · π))) |
304 | 249 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (π · 1) =
π) |
305 | 303, 304 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((π · (2
· (⌊‘(𝑁
/ 2)))) + (π · 1)) = (((⌊‘(𝑁 / 2)) · (2 · π)) +
π)) |
306 | 300, 192 | mulcld 9939 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((⌊‘(𝑁 / 2)) · (2 ·
π)) ∈ ℂ) |
307 | 306, 107 | addcomd 10117 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((⌊‘(𝑁 / 2)) · (2 ·
π)) + π) = (π + ((⌊‘(𝑁 / 2)) · (2 ·
π)))) |
308 | 302, 305,
307 | 3eqtrd 2648 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (π · ((2
· (⌊‘(𝑁
/ 2))) + 1)) = (π + ((⌊‘(𝑁 / 2)) · (2 ·
π)))) |
309 | 308 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝜑 → (cos‘(π ·
((2 · (⌊‘(𝑁 / 2))) + 1))) = (cos‘(π +
((⌊‘(𝑁 / 2))
· (2 · π))))) |
310 | | cosper 24038 |
. . . . . . . . . . . . 13
⊢ ((π
∈ ℂ ∧ (⌊‘(𝑁 / 2)) ∈ ℤ) →
(cos‘(π + ((⌊‘(𝑁 / 2)) · (2 · π)))) =
(cos‘π)) |
311 | 107, 262,
310 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → (cos‘(π +
((⌊‘(𝑁 / 2))
· (2 · π)))) = (cos‘π)) |
312 | 255 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (cos‘π) =
-1) |
313 | 309, 311,
312 | 3eqtrd 2648 |
. . . . . . . . . . 11
⊢ (𝜑 → (cos‘(π ·
((2 · (⌊‘(𝑁 / 2))) + 1))) = -1) |
314 | 313 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → (cos‘(π · ((2
· (⌊‘(𝑁
/ 2))) + 1))) = -1) |
315 | 299, 314 | oveq12d 6567 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → (Σ𝑛 ∈ (1...(2 ·
(⌊‘(𝑁 /
2))))(cos‘(π · 𝑛)) + (cos‘(π · ((2 ·
(⌊‘(𝑁 / 2))) +
1)))) = (0 + -1)) |
316 | | neg1cn 11001 |
. . . . . . . . . . 11
⊢ -1 ∈
ℂ |
317 | 316 | addid2i 10103 |
. . . . . . . . . 10
⊢ (0 + -1)
= -1 |
318 | 317 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → (0 + -1) = -1) |
319 | 290, 315,
318 | 3eqtrd 2648 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑁 = 1) → Σ𝑛 ∈ (1...((2 ·
(⌊‘(𝑁 / 2))) +
1))(cos‘(π · 𝑛)) = -1) |
320 | 258, 319 | pm2.61dan 828 |
. . . . . . 7
⊢ (𝜑 → Σ𝑛 ∈ (1...((2 ·
(⌊‘(𝑁 / 2))) +
1))(cos‘(π · 𝑛)) = -1) |
321 | 320 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → Σ𝑛 ∈ (1...((2 ·
(⌊‘(𝑁 / 2))) +
1))(cos‘(π · 𝑛)) = -1) |
322 | 232, 321 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛)) = -1) |
323 | 322 | oveq2d 6565 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛))) = ((1 / 2) +
-1)) |
324 | 323 | oveq1d 6564 |
. . 3
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(π · 𝑛))) / π) = (((1 / 2) + -1) /
π)) |
325 | 168, 172 | eqtrd 2644 |
. . . . 5
⊢ (𝜑 → ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) ·
(sin‘(𝐴 / 2)))) =
((sin‘(((𝐾 + (1 / 2))
· π) + (𝑁
· π))) / ((2 · π) · (sin‘((𝐾 + (1 / 2)) ·
π))))) |
326 | 325 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) ·
(sin‘(𝐴 / 2)))) =
((sin‘(((𝐾 + (1 / 2))
· π) + (𝑁
· π))) / ((2 · π) · (sin‘((𝐾 + (1 / 2)) ·
π))))) |
327 | 230 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (𝑁 · π) = (((2 ·
(⌊‘(𝑁 / 2))) +
1) · π)) |
328 | 301, 109,
107 | adddird 9944 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2 ·
(⌊‘(𝑁 / 2))) +
1) · π) = (((2 · (⌊‘(𝑁 / 2))) · π) + (1 ·
π))) |
329 | 107 | mulid2d 9937 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 · π) =
π) |
330 | 329 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2 ·
(⌊‘(𝑁 / 2)))
· π) + (1 · π)) = (((2 · (⌊‘(𝑁 / 2))) · π) +
π)) |
331 | 301, 107 | mulcld 9939 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 ·
(⌊‘(𝑁 / 2)))
· π) ∈ ℂ) |
332 | 331, 107 | addcomd 10117 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2 ·
(⌊‘(𝑁 / 2)))
· π) + π) = (π + ((2 · (⌊‘(𝑁 / 2))) · π))) |
333 | 328, 330,
332 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ (𝜑 → (((2 ·
(⌊‘(𝑁 / 2))) +
1) · π) = (π + ((2 · (⌊‘(𝑁 / 2))) · π))) |
334 | 333 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (((2 ·
(⌊‘(𝑁 / 2))) +
1) · π) = (π + ((2 · (⌊‘(𝑁 / 2))) · π))) |
335 | 50, 300 | mulcomd 9940 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 ·
(⌊‘(𝑁 / 2))) =
((⌊‘(𝑁 / 2))
· 2)) |
336 | 335 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 ·
(⌊‘(𝑁 / 2)))
· π) = (((⌊‘(𝑁 / 2)) · 2) ·
π)) |
337 | 300, 50, 107 | mulassd 9942 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((⌊‘(𝑁 / 2)) · 2) ·
π) = ((⌊‘(𝑁
/ 2)) · (2 · π))) |
338 | 336, 337 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 ·
(⌊‘(𝑁 / 2)))
· π) = ((⌊‘(𝑁 / 2)) · (2 ·
π))) |
339 | 338 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝜑 → (π + ((2 ·
(⌊‘(𝑁 / 2)))
· π)) = (π + ((⌊‘(𝑁 / 2)) · (2 ·
π)))) |
340 | 339 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (π + ((2 ·
(⌊‘(𝑁 / 2)))
· π)) = (π + ((⌊‘(𝑁 / 2)) · (2 ·
π)))) |
341 | 327, 334,
340 | 3eqtrd 2648 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (𝑁 · π) = (π +
((⌊‘(𝑁 / 2))
· (2 · π)))) |
342 | 341 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (((𝐾 + (1 / 2)) · π) + (𝑁 · π)) = (((𝐾 + (1 / 2)) · π) +
(π + ((⌊‘(𝑁
/ 2)) · (2 · π))))) |
343 | 193 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → ((𝐾 + (1 / 2)) · π) ∈
ℂ) |
344 | 14 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → π ∈
ℂ) |
345 | 306 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → ((⌊‘(𝑁 / 2)) · (2 ·
π)) ∈ ℂ) |
346 | 343, 344,
345 | addassd 9941 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → ((((𝐾 + (1 / 2)) · π) + π) +
((⌊‘(𝑁 / 2))
· (2 · π))) = (((𝐾 + (1 / 2)) · π) + (π +
((⌊‘(𝑁 / 2))
· (2 · π))))) |
347 | 342, 346 | eqtr4d 2647 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (((𝐾 + (1 / 2)) · π) + (𝑁 · π)) = ((((𝐾 + (1 / 2)) · π) +
π) + ((⌊‘(𝑁
/ 2)) · (2 · π)))) |
348 | 347 | fveq2d 6107 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (sin‘(((𝐾 + (1 / 2)) · π) +
(𝑁 · π))) =
(sin‘((((𝐾 + (1 / 2))
· π) + π) + ((⌊‘(𝑁 / 2)) · (2 ·
π))))) |
349 | 348 | oveq1d 6564 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → ((sin‘(((𝐾 + (1 / 2)) · π) +
(𝑁 · π))) / ((2
· π) · (sin‘((𝐾 + (1 / 2)) · π)))) =
((sin‘((((𝐾 + (1 /
2)) · π) + π) + ((⌊‘(𝑁 / 2)) · (2 · π)))) / ((2
· π) · (sin‘((𝐾 + (1 / 2)) ·
π))))) |
350 | 193, 107 | addcld 9938 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐾 + (1 / 2)) · π) + π) ∈
ℂ) |
351 | | sinper 24037 |
. . . . . . . . 9
⊢
(((((𝐾 + (1 / 2))
· π) + π) ∈ ℂ ∧ (⌊‘(𝑁 / 2)) ∈ ℤ) →
(sin‘((((𝐾 + (1 / 2))
· π) + π) + ((⌊‘(𝑁 / 2)) · (2 · π)))) =
(sin‘(((𝐾 + (1 / 2))
· π) + π))) |
352 | 350, 262,
351 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (sin‘((((𝐾 + (1 / 2)) · π) +
π) + ((⌊‘(𝑁
/ 2)) · (2 · π)))) = (sin‘(((𝐾 + (1 / 2)) · π) +
π))) |
353 | | sinppi 24045 |
. . . . . . . . 9
⊢ (((𝐾 + (1 / 2)) · π)
∈ ℂ → (sin‘(((𝐾 + (1 / 2)) · π) + π)) =
-(sin‘((𝐾 + (1 / 2))
· π))) |
354 | 193, 353 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (sin‘(((𝐾 + (1 / 2)) · π) +
π)) = -(sin‘((𝐾 +
(1 / 2)) · π))) |
355 | 352, 354 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → (sin‘((((𝐾 + (1 / 2)) · π) +
π) + ((⌊‘(𝑁
/ 2)) · (2 · π)))) = -(sin‘((𝐾 + (1 / 2)) ·
π))) |
356 | 355 | oveq1d 6564 |
. . . . . 6
⊢ (𝜑 → ((sin‘((((𝐾 + (1 / 2)) · π) +
π) + ((⌊‘(𝑁
/ 2)) · (2 · π)))) / ((2 · π) ·
(sin‘((𝐾 + (1 / 2))
· π)))) = (-(sin‘((𝐾 + (1 / 2)) · π)) / ((2 ·
π) · (sin‘((𝐾 + (1 / 2)) ·
π))))) |
357 | 195 | oveq2d 6565 |
. . . . . 6
⊢ (𝜑 → (-(sin‘((𝐾 + (1 / 2)) · π)) /
((2 · π) · (sin‘((𝐾 + (1 / 2)) · π)))) =
(-(sin‘((𝐾 + (1 / 2))
· π)) / ((sin‘((𝐾 + (1 / 2)) · π)) · (2
· π)))) |
358 | 194, 194,
215 | divnegd 10693 |
. . . . . . . . 9
⊢ (𝜑 → -((sin‘((𝐾 + (1 / 2)) · π)) /
(sin‘((𝐾 + (1 / 2))
· π))) = (-(sin‘((𝐾 + (1 / 2)) · π)) /
(sin‘((𝐾 + (1 / 2))
· π)))) |
359 | 218 | negeqd 10154 |
. . . . . . . . 9
⊢ (𝜑 → -((sin‘((𝐾 + (1 / 2)) · π)) /
(sin‘((𝐾 + (1 / 2))
· π))) = -1) |
360 | 358, 359 | eqtr3d 2646 |
. . . . . . . 8
⊢ (𝜑 → (-(sin‘((𝐾 + (1 / 2)) · π)) /
(sin‘((𝐾 + (1 / 2))
· π))) = -1) |
361 | 360 | oveq1d 6564 |
. . . . . . 7
⊢ (𝜑 → ((-(sin‘((𝐾 + (1 / 2)) · π)) /
(sin‘((𝐾 + (1 / 2))
· π))) / (2 · π)) = (-1 / (2 ·
π))) |
362 | 194 | negcld 10258 |
. . . . . . . 8
⊢ (𝜑 → -(sin‘((𝐾 + (1 / 2)) · π))
∈ ℂ) |
363 | 362, 194,
192, 215, 216 | divdiv1d 10711 |
. . . . . . 7
⊢ (𝜑 → ((-(sin‘((𝐾 + (1 / 2)) · π)) /
(sin‘((𝐾 + (1 / 2))
· π))) / (2 · π)) = (-(sin‘((𝐾 + (1 / 2)) · π)) /
((sin‘((𝐾 + (1 / 2))
· π)) · (2 · π)))) |
364 | 86, 90 | negsubi 10238 |
. . . . . . . . . . 11
⊢ ((1 / 2)
+ -1) = ((1 / 2) − 1) |
365 | 90, 86 | negsubdi2i 10246 |
. . . . . . . . . . 11
⊢ -(1
− (1 / 2)) = ((1 / 2) − 1) |
366 | | 1mhlfehlf 11128 |
. . . . . . . . . . . . 13
⊢ (1
− (1 / 2)) = (1 / 2) |
367 | 366 | negeqi 10153 |
. . . . . . . . . . . 12
⊢ -(1
− (1 / 2)) = -(1 / 2) |
368 | | divneg 10598 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → -(1 / 2) = (-1 /
2)) |
369 | 90, 118, 51, 368 | mp3an 1416 |
. . . . . . . . . . . 12
⊢ -(1 / 2)
= (-1 / 2) |
370 | 367, 369 | eqtri 2632 |
. . . . . . . . . . 11
⊢ -(1
− (1 / 2)) = (-1 / 2) |
371 | 364, 365,
370 | 3eqtr2i 2638 |
. . . . . . . . . 10
⊢ ((1 / 2)
+ -1) = (-1 / 2) |
372 | 371 | oveq1i 6559 |
. . . . . . . . 9
⊢ (((1 / 2)
+ -1) / π) = ((-1 / 2) / π) |
373 | | divdiv1 10615 |
. . . . . . . . . 10
⊢ ((-1
∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (π ∈
ℂ ∧ π ≠ 0)) → ((-1 / 2) / π) = (-1 / (2 ·
π))) |
374 | 316, 91, 95, 373 | mp3an 1416 |
. . . . . . . . 9
⊢ ((-1 / 2)
/ π) = (-1 / (2 · π)) |
375 | 372, 374 | eqtr2i 2633 |
. . . . . . . 8
⊢ (-1 / (2
· π)) = (((1 / 2) + -1) / π) |
376 | 375 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (-1 / (2 · π)) =
(((1 / 2) + -1) / π)) |
377 | 361, 363,
376 | 3eqtr3d 2652 |
. . . . . 6
⊢ (𝜑 → (-(sin‘((𝐾 + (1 / 2)) · π)) /
((sin‘((𝐾 + (1 / 2))
· π)) · (2 · π))) = (((1 / 2) + -1) /
π)) |
378 | 356, 357,
377 | 3eqtrd 2648 |
. . . . 5
⊢ (𝜑 → ((sin‘((((𝐾 + (1 / 2)) · π) +
π) + ((⌊‘(𝑁
/ 2)) · (2 · π)))) / ((2 · π) ·
(sin‘((𝐾 + (1 / 2))
· π)))) = (((1 / 2) + -1) / π)) |
379 | 378 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → ((sin‘((((𝐾 + (1 / 2)) · π) +
π) + ((⌊‘(𝑁
/ 2)) · (2 · π)))) / ((2 · π) ·
(sin‘((𝐾 + (1 / 2))
· π)))) = (((1 / 2) + -1) / π)) |
380 | 326, 349,
379 | 3eqtrrd 2649 |
. . 3
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (((1 / 2) + -1) / π)
= ((sin‘((𝑁 + (1 /
2)) · 𝐴)) / ((2
· π) · (sin‘(𝐴 / 2))))) |
381 | 225, 324,
380 | 3eqtrd 2648 |
. 2
⊢ ((𝜑 ∧ ¬ (𝑁 mod 2) = 0) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) ·
(sin‘(𝐴 /
2))))) |
382 | 224, 381 | pm2.61dan 828 |
1
⊢ (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) ·
(sin‘(𝐴 /
2))))) |