Step | Hyp | Ref
| Expression |
1 | | 1cnd 10056 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℂ) |
2 | 1 | halfcld 11277 |
. . . . . . . 8
⊢ (𝜑 → (1 / 2) ∈
ℂ) |
3 | | fzfid 12772 |
. . . . . . . . 9
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
4 | | elfzelz 12342 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℤ) |
5 | 4 | zcnd 11483 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ) |
6 | 5 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℂ) |
7 | | dirkertrigeqlem2.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ ℝ) |
8 | 7 | recnd 10068 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℂ) |
9 | 8 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝐴 ∈ ℂ) |
10 | 6, 9 | mulcld 10060 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 · 𝐴) ∈ ℂ) |
11 | 10 | coscld 14861 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝐴)) ∈ ℂ) |
12 | 3, 11 | fsumcl 14464 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) ∈ ℂ) |
13 | 2, 12 | addcld 10059 |
. . . . . . 7
⊢ (𝜑 → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) ∈ ℂ) |
14 | 8 | sincld 14860 |
. . . . . . 7
⊢ (𝜑 → (sin‘𝐴) ∈
ℂ) |
15 | | dirkertrigeqlem2.sinne0 |
. . . . . . 7
⊢ (𝜑 → (sin‘𝐴) ≠ 0) |
16 | 13, 14, 15 | divcan4d 10807 |
. . . . . 6
⊢ (𝜑 → ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) · (sin‘𝐴)) / (sin‘𝐴)) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)))) |
17 | 16 | eqcomd 2628 |
. . . . 5
⊢ (𝜑 → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) = ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) · (sin‘𝐴)) / (sin‘𝐴))) |
18 | 3, 14, 11 | fsummulc1 14517 |
. . . . . . . . 9
⊢ (𝜑 → (Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) · (sin‘𝐴)) = Σ𝑛 ∈ (1...𝑁)((cos‘(𝑛 · 𝐴)) · (sin‘𝐴))) |
19 | 14 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘𝐴) ∈ ℂ) |
20 | 11, 19 | mulcomd 10061 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝐴)) · (sin‘𝐴)) = ((sin‘𝐴) · (cos‘(𝑛 · 𝐴)))) |
21 | | sinmulcos 40076 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ (𝑛 · 𝐴) ∈ ℂ) → ((sin‘𝐴) · (cos‘(𝑛 · 𝐴))) = (((sin‘(𝐴 + (𝑛 · 𝐴))) + (sin‘(𝐴 − (𝑛 · 𝐴)))) / 2)) |
22 | 9, 10, 21 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘𝐴) · (cos‘(𝑛 · 𝐴))) = (((sin‘(𝐴 + (𝑛 · 𝐴))) + (sin‘(𝐴 − (𝑛 · 𝐴)))) / 2)) |
23 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 1 ∈ ℂ) |
24 | 6, 23, 9 | adddird 10065 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑛 + 1) · 𝐴) = ((𝑛 · 𝐴) + (1 · 𝐴))) |
25 | 23, 9 | mulcld 10060 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (1 · 𝐴) ∈ ℂ) |
26 | 10, 25 | addcomd 10238 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑛 · 𝐴) + (1 · 𝐴)) = ((1 · 𝐴) + (𝑛 · 𝐴))) |
27 | 8 | mulid2d 10058 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1 · 𝐴) = 𝐴) |
28 | 27 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1 · 𝐴) + (𝑛 · 𝐴)) = (𝐴 + (𝑛 · 𝐴))) |
29 | 28 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1 · 𝐴) + (𝑛 · 𝐴)) = (𝐴 + (𝑛 · 𝐴))) |
30 | 24, 26, 29 | 3eqtrrd 2661 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐴 + (𝑛 · 𝐴)) = ((𝑛 + 1) · 𝐴)) |
31 | 30 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘(𝐴 + (𝑛 · 𝐴))) = (sin‘((𝑛 + 1) · 𝐴))) |
32 | 10, 9 | negsubdi2d 10408 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → -((𝑛 · 𝐴) − 𝐴) = (𝐴 − (𝑛 · 𝐴))) |
33 | 32 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐴 − (𝑛 · 𝐴)) = -((𝑛 · 𝐴) − 𝐴)) |
34 | 33 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘(𝐴 − (𝑛 · 𝐴))) = (sin‘-((𝑛 · 𝐴) − 𝐴))) |
35 | 10, 9 | subcld 10392 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑛 · 𝐴) − 𝐴) ∈ ℂ) |
36 | | sinneg 14876 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 · 𝐴) − 𝐴) ∈ ℂ → (sin‘-((𝑛 · 𝐴) − 𝐴)) = -(sin‘((𝑛 · 𝐴) − 𝐴))) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘-((𝑛 · 𝐴) − 𝐴)) = -(sin‘((𝑛 · 𝐴) − 𝐴))) |
38 | 34, 37 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘(𝐴 − (𝑛 · 𝐴))) = -(sin‘((𝑛 · 𝐴) − 𝐴))) |
39 | 31, 38 | oveq12d 6668 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘(𝐴 + (𝑛 · 𝐴))) + (sin‘(𝐴 − (𝑛 · 𝐴)))) = ((sin‘((𝑛 + 1) · 𝐴)) + -(sin‘((𝑛 · 𝐴) − 𝐴)))) |
40 | 9, 10 | addcld 10059 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐴 + (𝑛 · 𝐴)) ∈ ℂ) |
41 | 40 | sincld 14860 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘(𝐴 + (𝑛 · 𝐴))) ∈ ℂ) |
42 | 31, 41 | eqeltrrd 2702 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘((𝑛 + 1) · 𝐴)) ∈ ℂ) |
43 | 35 | sincld 14860 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘((𝑛 · 𝐴) − 𝐴)) ∈ ℂ) |
44 | 42, 43 | negsubd 10398 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘((𝑛 + 1) · 𝐴)) + -(sin‘((𝑛 · 𝐴) − 𝐴))) = ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 · 𝐴) − 𝐴)))) |
45 | 6, 9 | mulsubfacd 10492 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑛 · 𝐴) − 𝐴) = ((𝑛 − 1) · 𝐴)) |
46 | 45 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘((𝑛 · 𝐴) − 𝐴)) = (sin‘((𝑛 − 1) · 𝐴))) |
47 | 46 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 · 𝐴) − 𝐴))) = ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) |
48 | 39, 44, 47 | 3eqtrd 2660 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘(𝐴 + (𝑛 · 𝐴))) + (sin‘(𝐴 − (𝑛 · 𝐴)))) = ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) |
49 | 48 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((sin‘(𝐴 + (𝑛 · 𝐴))) + (sin‘(𝐴 − (𝑛 · 𝐴)))) / 2) = (((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2)) |
50 | 20, 22, 49 | 3eqtrd 2660 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝐴)) · (sin‘𝐴)) = (((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2)) |
51 | 50 | sumeq2dv 14433 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)((cos‘(𝑛 · 𝐴)) · (sin‘𝐴)) = Σ𝑛 ∈ (1...𝑁)(((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2)) |
52 | | 2cnd 11093 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℂ) |
53 | | peano2cnm 10347 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℂ → (𝑛 − 1) ∈
ℂ) |
54 | 6, 53 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 − 1) ∈ ℂ) |
55 | 54, 9 | mulcld 10060 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑛 − 1) · 𝐴) ∈ ℂ) |
56 | 55 | sincld 14860 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘((𝑛 − 1) · 𝐴)) ∈ ℂ) |
57 | 42, 56 | subcld 10392 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) ∈ ℂ) |
58 | | 2ne0 11113 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
59 | 58 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ≠ 0) |
60 | 3, 52, 57, 59 | fsumdivc 14518 |
. . . . . . . . . 10
⊢ (𝜑 → (Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2) = Σ𝑛 ∈ (1...𝑁)(((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2)) |
61 | 3, 57 | fsumcl 14464 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) ∈ ℂ) |
62 | 61, 52, 59 | divrec2d 10805 |
. . . . . . . . . 10
⊢ (𝜑 → (Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2) = ((1 / 2) · Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) |
63 | 60, 62 | eqtr3d 2658 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)(((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2) = ((1 / 2) · Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) |
64 | 18, 51, 63 | 3eqtrd 2660 |
. . . . . . . 8
⊢ (𝜑 → (Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) · (sin‘𝐴)) = ((1 / 2) · Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) |
65 | 64 | oveq2d 6666 |
. . . . . . 7
⊢ (𝜑 → (((1 / 2) ·
(sin‘𝐴)) +
(Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) · (sin‘𝐴))) = (((1 / 2) · (sin‘𝐴)) + ((1 / 2) ·
Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))))) |
66 | 2, 12, 14 | adddird 10065 |
. . . . . . 7
⊢ (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) · (sin‘𝐴)) = (((1 / 2) · (sin‘𝐴)) + (Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) · (sin‘𝐴)))) |
67 | 2, 14, 61 | adddid 10064 |
. . . . . . 7
⊢ (𝜑 → ((1 / 2) ·
((sin‘𝐴) +
Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) = (((1 / 2) · (sin‘𝐴)) + ((1 / 2) ·
Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))))) |
68 | 65, 66, 67 | 3eqtr4d 2666 |
. . . . . 6
⊢ (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) · (sin‘𝐴)) = ((1 / 2) · ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))))) |
69 | 68 | oveq1d 6665 |
. . . . 5
⊢ (𝜑 → ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) · (sin‘𝐴)) / (sin‘𝐴)) = (((1 / 2) · ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) / (sin‘𝐴))) |
70 | 10 | sincld 14860 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝐴)) ∈ ℂ) |
71 | 42, 70, 56 | npncand 10416 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) = ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) |
72 | 71 | eqcomd 2628 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = (((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) |
73 | 72 | sumeq2dv 14433 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = Σ𝑛 ∈ (1...𝑁)(((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) |
74 | 42, 70 | subcld 10392 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) ∈ ℂ) |
75 | 70, 56 | subcld 10392 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) ∈ ℂ) |
76 | 3, 74, 75 | fsumadd 14470 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)(((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) = (Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + Σ𝑛 ∈ (1...𝑁)((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) |
77 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑛 → (𝑗 · 𝐴) = (𝑛 · 𝐴)) |
78 | 77 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑛 → (sin‘(𝑗 · 𝐴)) = (sin‘(𝑛 · 𝐴))) |
79 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝑗 = (𝑛 + 1) → (𝑗 · 𝐴) = ((𝑛 + 1) · 𝐴)) |
80 | 79 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑗 = (𝑛 + 1) → (sin‘(𝑗 · 𝐴)) = (sin‘((𝑛 + 1) · 𝐴))) |
81 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 1 → (𝑗 · 𝐴) = (1 · 𝐴)) |
82 | 81 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑗 = 1 → (sin‘(𝑗 · 𝐴)) = (sin‘(1 · 𝐴))) |
83 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝑗 = (𝑁 + 1) → (𝑗 · 𝐴) = ((𝑁 + 1) · 𝐴)) |
84 | 83 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑗 = (𝑁 + 1) → (sin‘(𝑗 · 𝐴)) = (sin‘((𝑁 + 1) · 𝐴))) |
85 | | dirkertrigeqlem2.n |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℕ) |
86 | 85 | nnzd 11481 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℤ) |
87 | | nnuz 11723 |
. . . . . . . . . . . . . 14
⊢ ℕ =
(ℤ≥‘1) |
88 | 85, 87 | syl6eleq 2711 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
89 | | peano2uz 11741 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘1) → (𝑁 + 1) ∈
(ℤ≥‘1)) |
90 | 88, 89 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘1)) |
91 | | elfzelz 12342 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℤ) |
92 | 91 | zcnd 11483 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℂ) |
93 | 92 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (1...(𝑁 + 1))) → 𝑗 ∈ ℂ) |
94 | 8 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (1...(𝑁 + 1))) → 𝐴 ∈ ℂ) |
95 | 93, 94 | mulcld 10060 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...(𝑁 + 1))) → (𝑗 · 𝐴) ∈ ℂ) |
96 | 95 | sincld 14860 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...(𝑁 + 1))) → (sin‘(𝑗 · 𝐴)) ∈ ℂ) |
97 | 78, 80, 82, 84, 86, 90, 96 | telfsum2 14537 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) = ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴)))) |
98 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ (1...𝑁) → 1 ∈ ℂ) |
99 | 5, 98 | pncand 10393 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 + 1) − 1) = 𝑛) |
100 | 99 | eqcomd 2628 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 = ((𝑛 + 1) − 1)) |
101 | 100 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 = ((𝑛 + 1) − 1)) |
102 | 101 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 · 𝐴) = (((𝑛 + 1) − 1) · 𝐴)) |
103 | 102 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝐴)) = (sin‘(((𝑛 + 1) − 1) · 𝐴))) |
104 | 103 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = ((sin‘(((𝑛 + 1) − 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) |
105 | 104 | sumeq2dv 14433 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = Σ𝑛 ∈ (1...𝑁)((sin‘(((𝑛 + 1) − 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) |
106 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑛 → (𝑗 − 1) = (𝑛 − 1)) |
107 | 106 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑛 → ((𝑗 − 1) · 𝐴) = ((𝑛 − 1) · 𝐴)) |
108 | 107 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑛 → (sin‘((𝑗 − 1) · 𝐴)) = (sin‘((𝑛 − 1) · 𝐴))) |
109 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = (𝑛 + 1) → (𝑗 − 1) = ((𝑛 + 1) − 1)) |
110 | 109 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = (𝑛 + 1) → ((𝑗 − 1) · 𝐴) = (((𝑛 + 1) − 1) · 𝐴)) |
111 | 110 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑗 = (𝑛 + 1) → (sin‘((𝑗 − 1) · 𝐴)) = (sin‘(((𝑛 + 1) − 1) · 𝐴))) |
112 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 1 → (𝑗 − 1) = (1 − 1)) |
113 | 112 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 1 → ((𝑗 − 1) · 𝐴) = ((1 − 1) · 𝐴)) |
114 | 113 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 1 → (sin‘((𝑗 − 1) · 𝐴)) = (sin‘((1 − 1)
· 𝐴))) |
115 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = (𝑁 + 1) → (𝑗 − 1) = ((𝑁 + 1) − 1)) |
116 | 115 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = (𝑁 + 1) → ((𝑗 − 1) · 𝐴) = (((𝑁 + 1) − 1) · 𝐴)) |
117 | 116 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑗 = (𝑁 + 1) → (sin‘((𝑗 − 1) · 𝐴)) = (sin‘(((𝑁 + 1) − 1) · 𝐴))) |
118 | | 1cnd 10056 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (1...(𝑁 + 1))) → 1 ∈
ℂ) |
119 | 93, 118 | subcld 10392 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (1...(𝑁 + 1))) → (𝑗 − 1) ∈ ℂ) |
120 | 119, 94 | mulcld 10060 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (1...(𝑁 + 1))) → ((𝑗 − 1) · 𝐴) ∈ ℂ) |
121 | 120 | sincld 14860 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...(𝑁 + 1))) → (sin‘((𝑗 − 1) · 𝐴)) ∈
ℂ) |
122 | 108, 111,
114, 117, 86, 90, 121 | telfsum2 14537 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘(((𝑛 + 1) − 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = ((sin‘(((𝑁 + 1) − 1) · 𝐴)) − (sin‘((1 − 1)
· 𝐴)))) |
123 | 85 | nnred 11035 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ ℝ) |
124 | 123 | recnd 10068 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℂ) |
125 | 124, 1 | pncand 10393 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁) |
126 | 125 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑁 + 1) − 1) · 𝐴) = (𝑁 · 𝐴)) |
127 | 126 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (sin‘(((𝑁 + 1) − 1) · 𝐴)) = (sin‘(𝑁 · 𝐴))) |
128 | 1 | subidd 10380 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1 − 1) =
0) |
129 | 128 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1 − 1) ·
𝐴) = (0 · 𝐴)) |
130 | 8 | mul02d 10234 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (0 · 𝐴) = 0) |
131 | 129, 130 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((1 − 1) ·
𝐴) = 0) |
132 | 131 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (sin‘((1 − 1)
· 𝐴)) =
(sin‘0)) |
133 | | sin0 14879 |
. . . . . . . . . . . . . . 15
⊢
(sin‘0) = 0 |
134 | 133 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (sin‘0) =
0) |
135 | 132, 134 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (sin‘((1 − 1)
· 𝐴)) =
0) |
136 | 127, 135 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((sin‘(((𝑁 + 1) − 1) · 𝐴)) − (sin‘((1
− 1) · 𝐴))) =
((sin‘(𝑁 ·
𝐴)) −
0)) |
137 | 105, 122,
136 | 3eqtrd 2660 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = ((sin‘(𝑁 · 𝐴)) − 0)) |
138 | 97, 137 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝜑 → (Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + Σ𝑛 ∈ (1...𝑁)((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) = (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0))) |
139 | 73, 76, 138 | 3eqtrd 2660 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0))) |
140 | 139 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝜑 → ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) = ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)))) |
141 | 27 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝜑 → (sin‘(1 ·
𝐴)) = (sin‘𝐴)) |
142 | 141 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝜑 → ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) = ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) |
143 | 142 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝜑 → (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)) = (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)) + ((sin‘(𝑁 · 𝐴)) − 0))) |
144 | 143 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝜑 → ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0))) = ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)) + ((sin‘(𝑁 · 𝐴)) − 0)))) |
145 | 124, 1 | addcld 10059 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 + 1) ∈ ℂ) |
146 | 145, 8 | mulcld 10060 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑁 + 1) · 𝐴) ∈ ℂ) |
147 | 146 | sincld 14860 |
. . . . . . . . . . . 12
⊢ (𝜑 → (sin‘((𝑁 + 1) · 𝐴)) ∈ ℂ) |
148 | 147, 14 | subcld 10392 |
. . . . . . . . . . 11
⊢ (𝜑 → ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)) ∈ ℂ) |
149 | 124, 8 | mulcld 10060 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 · 𝐴) ∈ ℂ) |
150 | 149 | sincld 14860 |
. . . . . . . . . . . 12
⊢ (𝜑 → (sin‘(𝑁 · 𝐴)) ∈ ℂ) |
151 | | 0cnd 10033 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈
ℂ) |
152 | 150, 151 | subcld 10392 |
. . . . . . . . . . 11
⊢ (𝜑 → ((sin‘(𝑁 · 𝐴)) − 0) ∈
ℂ) |
153 | 14, 148, 152 | addassd 10062 |
. . . . . . . . . 10
⊢ (𝜑 → (((sin‘𝐴) + ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)) = ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)) + ((sin‘(𝑁 · 𝐴)) − 0)))) |
154 | 153 | eqcomd 2628 |
. . . . . . . . 9
⊢ (𝜑 → ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)) + ((sin‘(𝑁 · 𝐴)) − 0))) = (((sin‘𝐴) + ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0))) |
155 | 14, 147 | pncan3d 10395 |
. . . . . . . . . . 11
⊢ (𝜑 → ((sin‘𝐴) + ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) = (sin‘((𝑁 + 1) · 𝐴))) |
156 | 150 | subid1d 10381 |
. . . . . . . . . . 11
⊢ (𝜑 → ((sin‘(𝑁 · 𝐴)) − 0) = (sin‘(𝑁 · 𝐴))) |
157 | 155, 156 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝜑 → (((sin‘𝐴) + ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)) = ((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴)))) |
158 | 147, 150 | addcomd 10238 |
. . . . . . . . . 10
⊢ (𝜑 → ((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))) = ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) |
159 | 157, 158 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝜑 → (((sin‘𝐴) + ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)) = ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) |
160 | 144, 154,
159 | 3eqtrd 2660 |
. . . . . . . 8
⊢ (𝜑 → ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0))) = ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) |
161 | 140, 160 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) = ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) |
162 | 161 | oveq2d 6666 |
. . . . . 6
⊢ (𝜑 → ((1 / 2) ·
((sin‘𝐴) +
Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) = ((1 / 2) · ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))))) |
163 | 162 | oveq1d 6665 |
. . . . 5
⊢ (𝜑 → (((1 / 2) ·
((sin‘𝐴) +
Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) / (sin‘𝐴)) = (((1 / 2) · ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) / (sin‘𝐴))) |
164 | 17, 69, 163 | 3eqtrd 2660 |
. . . 4
⊢ (𝜑 → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) = (((1 / 2) · ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) / (sin‘𝐴))) |
165 | | halfre 11246 |
. . . . . . . . . . . 12
⊢ (1 / 2)
∈ ℝ |
166 | 165 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 / 2) ∈
ℝ) |
167 | 123, 166 | readdcld 10069 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 + (1 / 2)) ∈ ℝ) |
168 | 167, 7 | remulcld 10070 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝐴) ∈ ℝ) |
169 | 168 | recnd 10068 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝐴) ∈ ℂ) |
170 | 2, 8 | mulcld 10060 |
. . . . . . . 8
⊢ (𝜑 → ((1 / 2) · 𝐴) ∈
ℂ) |
171 | | sinmulcos 40076 |
. . . . . . . 8
⊢ ((((𝑁 + (1 / 2)) · 𝐴) ∈ ℂ ∧ ((1 / 2)
· 𝐴) ∈ ℂ)
→ ((sin‘((𝑁 + (1
/ 2)) · 𝐴)) ·
(cos‘((1 / 2) · 𝐴))) = (((sin‘(((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴))) + (sin‘(((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴)))) / 2)) |
172 | 169, 170,
171 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → ((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2)
· 𝐴))) =
(((sin‘(((𝑁 + (1 /
2)) · 𝐴) + ((1 / 2)
· 𝐴))) +
(sin‘(((𝑁 + (1 / 2))
· 𝐴) − ((1 /
2) · 𝐴)))) /
2)) |
173 | 124, 2, 8 | adddird 10065 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝐴) = ((𝑁 · 𝐴) + ((1 / 2) · 𝐴))) |
174 | 173 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴)) = (((𝑁 · 𝐴) + ((1 / 2) · 𝐴)) + ((1 / 2) · 𝐴))) |
175 | 149, 170,
170 | addassd 10062 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑁 · 𝐴) + ((1 / 2) · 𝐴)) + ((1 / 2) · 𝐴)) = ((𝑁 · 𝐴) + (((1 / 2) · 𝐴) + ((1 / 2) · 𝐴)))) |
176 | 2, 2, 8 | adddird 10065 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((1 / 2) + (1 / 2))
· 𝐴) = (((1 / 2)
· 𝐴) + ((1 / 2)
· 𝐴))) |
177 | 1 | 2halvesd 11278 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((1 / 2) + (1 / 2)) =
1) |
178 | 177 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((1 / 2) + (1 / 2))
· 𝐴) = (1 ·
𝐴)) |
179 | 176, 178 | eqtr3d 2658 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((1 / 2) · 𝐴) + ((1 / 2) · 𝐴)) = (1 · 𝐴)) |
180 | 179 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁 · 𝐴) + (((1 / 2) · 𝐴) + ((1 / 2) · 𝐴))) = ((𝑁 · 𝐴) + (1 · 𝐴))) |
181 | 124, 1, 8 | adddird 10065 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁 + 1) · 𝐴) = ((𝑁 · 𝐴) + (1 · 𝐴))) |
182 | 180, 181 | eqtr4d 2659 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 · 𝐴) + (((1 / 2) · 𝐴) + ((1 / 2) · 𝐴))) = ((𝑁 + 1) · 𝐴)) |
183 | 174, 175,
182 | 3eqtrrd 2661 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁 + 1) · 𝐴) = (((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴))) |
184 | 183 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝜑 → (sin‘((𝑁 + 1) · 𝐴)) = (sin‘(((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴)))) |
185 | 173 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴)) = (((𝑁 · 𝐴) + ((1 / 2) · 𝐴)) − ((1 / 2) · 𝐴))) |
186 | 149, 170 | pncand 10393 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑁 · 𝐴) + ((1 / 2) · 𝐴)) − ((1 / 2) · 𝐴)) = (𝑁 · 𝐴)) |
187 | 185, 186 | eqtr2d 2657 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 · 𝐴) = (((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴))) |
188 | 187 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝜑 → (sin‘(𝑁 · 𝐴)) = (sin‘(((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴)))) |
189 | 184, 188 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝜑 → ((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))) = ((sin‘(((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴))) + (sin‘(((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴))))) |
190 | 189 | oveq1d 6665 |
. . . . . . 7
⊢ (𝜑 → (((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))) / 2) = (((sin‘(((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴))) + (sin‘(((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴)))) / 2)) |
191 | 172, 190 | eqtr4d 2659 |
. . . . . 6
⊢ (𝜑 → ((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2)
· 𝐴))) =
(((sin‘((𝑁 + 1)
· 𝐴)) +
(sin‘(𝑁 ·
𝐴))) / 2)) |
192 | 158 | oveq1d 6665 |
. . . . . 6
⊢ (𝜑 → (((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))) / 2) = (((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))) / 2)) |
193 | 150, 147 | addcld 10059 |
. . . . . . 7
⊢ (𝜑 → ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))) ∈ ℂ) |
194 | 193, 52, 59 | divrec2d 10805 |
. . . . . 6
⊢ (𝜑 → (((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))) / 2) = ((1 / 2) ·
((sin‘(𝑁 ·
𝐴)) + (sin‘((𝑁 + 1) · 𝐴))))) |
195 | 191, 192,
194 | 3eqtrrd 2661 |
. . . . 5
⊢ (𝜑 → ((1 / 2) ·
((sin‘(𝑁 ·
𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) ·
𝐴)))) |
196 | 195 | oveq1d 6665 |
. . . 4
⊢ (𝜑 → (((1 / 2) ·
((sin‘(𝑁 ·
𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) / (sin‘𝐴)) = (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) ·
𝐴))) / (sin‘𝐴))) |
197 | 8, 52, 59 | divcan2d 10803 |
. . . . . . . . 9
⊢ (𝜑 → (2 · (𝐴 / 2)) = 𝐴) |
198 | 197 | eqcomd 2628 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 = (2 · (𝐴 / 2))) |
199 | 198 | fveq2d 6195 |
. . . . . . 7
⊢ (𝜑 → (sin‘𝐴) = (sin‘(2 ·
(𝐴 / 2)))) |
200 | 8 | halfcld 11277 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 / 2) ∈ ℂ) |
201 | | sin2t 14907 |
. . . . . . . 8
⊢ ((𝐴 / 2) ∈ ℂ →
(sin‘(2 · (𝐴 /
2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))))) |
202 | 200, 201 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (sin‘(2 ·
(𝐴 / 2))) = (2 ·
((sin‘(𝐴 / 2))
· (cos‘(𝐴 /
2))))) |
203 | 199, 202 | eqtrd 2656 |
. . . . . 6
⊢ (𝜑 → (sin‘𝐴) = (2 ·
((sin‘(𝐴 / 2))
· (cos‘(𝐴 /
2))))) |
204 | 203 | oveq2d 6666 |
. . . . 5
⊢ (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2)
· 𝐴))) /
(sin‘𝐴)) =
(((sin‘((𝑁 + (1 / 2))
· 𝐴)) ·
(cos‘((1 / 2) · 𝐴))) / (2 · ((sin‘(𝐴 / 2)) ·
(cos‘(𝐴 /
2)))))) |
205 | 200 | sincld 14860 |
. . . . . . . 8
⊢ (𝜑 → (sin‘(𝐴 / 2)) ∈
ℂ) |
206 | 200 | coscld 14861 |
. . . . . . . 8
⊢ (𝜑 → (cos‘(𝐴 / 2)) ∈
ℂ) |
207 | 52, 205, 206 | mulassd 10063 |
. . . . . . 7
⊢ (𝜑 → ((2 ·
(sin‘(𝐴 / 2)))
· (cos‘(𝐴 /
2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))))) |
208 | 8, 52, 59 | divrec2d 10805 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 / 2) = ((1 / 2) · 𝐴)) |
209 | 208 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝜑 → (cos‘(𝐴 / 2)) = (cos‘((1 / 2)
· 𝐴))) |
210 | 209 | oveq2d 6666 |
. . . . . . 7
⊢ (𝜑 → ((2 ·
(sin‘(𝐴 / 2)))
· (cos‘(𝐴 /
2))) = ((2 · (sin‘(𝐴 / 2))) · (cos‘((1 / 2)
· 𝐴)))) |
211 | 207, 210 | eqtr3d 2658 |
. . . . . 6
⊢ (𝜑 → (2 ·
((sin‘(𝐴 / 2))
· (cos‘(𝐴 /
2)))) = ((2 · (sin‘(𝐴 / 2))) · (cos‘((1 / 2)
· 𝐴)))) |
212 | 211 | oveq2d 6666 |
. . . . 5
⊢ (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2)
· 𝐴))) / (2 ·
((sin‘(𝐴 / 2))
· (cos‘(𝐴 /
2))))) = (((sin‘((𝑁 +
(1 / 2)) · 𝐴))
· (cos‘((1 / 2) · 𝐴))) / ((2 · (sin‘(𝐴 / 2))) · (cos‘((1
/ 2) · 𝐴))))) |
213 | 169 | sincld 14860 |
. . . . . 6
⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝐴)) ∈
ℂ) |
214 | 52, 205 | mulcld 10060 |
. . . . . 6
⊢ (𝜑 → (2 ·
(sin‘(𝐴 / 2))) ∈
ℂ) |
215 | 170 | coscld 14861 |
. . . . . 6
⊢ (𝜑 → (cos‘((1 / 2)
· 𝐴)) ∈
ℂ) |
216 | 205, 206 | mulcld 10060 |
. . . . . . . . 9
⊢ (𝜑 → ((sin‘(𝐴 / 2)) ·
(cos‘(𝐴 / 2))) ∈
ℂ) |
217 | 203, 15 | eqnetrrd 2862 |
. . . . . . . . 9
⊢ (𝜑 → (2 ·
((sin‘(𝐴 / 2))
· (cos‘(𝐴 /
2)))) ≠ 0) |
218 | 52, 216, 217 | mulne0bbd 10683 |
. . . . . . . 8
⊢ (𝜑 → ((sin‘(𝐴 / 2)) ·
(cos‘(𝐴 / 2))) ≠
0) |
219 | 205, 206,
218 | mulne0bad 10682 |
. . . . . . 7
⊢ (𝜑 → (sin‘(𝐴 / 2)) ≠ 0) |
220 | 52, 205, 59, 219 | mulne0d 10679 |
. . . . . 6
⊢ (𝜑 → (2 ·
(sin‘(𝐴 / 2))) ≠
0) |
221 | 205, 206,
218 | mulne0bbd 10683 |
. . . . . . 7
⊢ (𝜑 → (cos‘(𝐴 / 2)) ≠ 0) |
222 | 209, 221 | eqnetrrd 2862 |
. . . . . 6
⊢ (𝜑 → (cos‘((1 / 2)
· 𝐴)) ≠
0) |
223 | 213, 214,
215, 220, 222 | divcan5rd 10828 |
. . . . 5
⊢ (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2)
· 𝐴))) / ((2
· (sin‘(𝐴 /
2))) · (cos‘((1 / 2) · 𝐴)))) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (2 · (sin‘(𝐴 / 2))))) |
224 | 204, 212,
223 | 3eqtrd 2660 |
. . . 4
⊢ (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2)
· 𝐴))) /
(sin‘𝐴)) =
((sin‘((𝑁 + (1 / 2))
· 𝐴)) / (2 ·
(sin‘(𝐴 /
2))))) |
225 | 164, 196,
224 | 3eqtrd 2660 |
. . 3
⊢ (𝜑 → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (2 · (sin‘(𝐴 / 2))))) |
226 | 225 | oveq1d 6665 |
. 2
⊢ (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = (((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (2 ·
(sin‘(𝐴 / 2)))) /
π)) |
227 | | picn 24211 |
. . . 4
⊢ π
∈ ℂ |
228 | 227 | a1i 11 |
. . 3
⊢ (𝜑 → π ∈
ℂ) |
229 | | pire 24210 |
. . . . 5
⊢ π
∈ ℝ |
230 | | pipos 24212 |
. . . . 5
⊢ 0 <
π |
231 | 229, 230 | gt0ne0ii 10564 |
. . . 4
⊢ π ≠
0 |
232 | 231 | a1i 11 |
. . 3
⊢ (𝜑 → π ≠
0) |
233 | 213, 214,
228, 220, 232 | divdiv32d 10826 |
. 2
⊢ (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (2 ·
(sin‘(𝐴 / 2)))) /
π) = (((sin‘((𝑁 +
(1 / 2)) · 𝐴)) /
π) / (2 · (sin‘(𝐴 / 2))))) |
234 | 213, 228,
214, 232, 220 | divdiv1d 10832 |
. . 3
⊢ (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) / π) / (2 ·
(sin‘(𝐴 / 2)))) =
((sin‘((𝑁 + (1 / 2))
· 𝐴)) / (π
· (2 · (sin‘(𝐴 / 2)))))) |
235 | 228, 52, 205 | mulassd 10063 |
. . . . 5
⊢ (𝜑 → ((π · 2)
· (sin‘(𝐴 /
2))) = (π · (2 · (sin‘(𝐴 / 2))))) |
236 | 228, 52 | mulcomd 10061 |
. . . . . 6
⊢ (𝜑 → (π · 2) = (2
· π)) |
237 | 236 | oveq1d 6665 |
. . . . 5
⊢ (𝜑 → ((π · 2)
· (sin‘(𝐴 /
2))) = ((2 · π) · (sin‘(𝐴 / 2)))) |
238 | 235, 237 | eqtr3d 2658 |
. . . 4
⊢ (𝜑 → (π · (2 ·
(sin‘(𝐴 / 2)))) = ((2
· π) · (sin‘(𝐴 / 2)))) |
239 | 238 | oveq2d 6666 |
. . 3
⊢ (𝜑 → ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (π · (2 ·
(sin‘(𝐴 / 2))))) =
((sin‘((𝑁 + (1 / 2))
· 𝐴)) / ((2 ·
π) · (sin‘(𝐴 / 2))))) |
240 | 234, 239 | eqtrd 2656 |
. 2
⊢ (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) / π) / (2 ·
(sin‘(𝐴 / 2)))) =
((sin‘((𝑁 + (1 / 2))
· 𝐴)) / ((2 ·
π) · (sin‘(𝐴 / 2))))) |
241 | 226, 233,
240 | 3eqtrd 2660 |
1
⊢ (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) ·
(sin‘(𝐴 /
2))))) |