| Step | Hyp | Ref
| Expression |
| 1 | | 1cnd 11256 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℂ) |
| 2 | 1 | halfcld 12511 |
. . . . . . . 8
⊢ (𝜑 → (1 / 2) ∈
ℂ) |
| 3 | | fzfid 14014 |
. . . . . . . . 9
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
| 4 | | elfzelz 13564 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℤ) |
| 5 | 4 | zcnd 12723 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ) |
| 6 | 5 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℂ) |
| 7 | | dirkertrigeqlem2.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 8 | 7 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 9 | 8 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝐴 ∈ ℂ) |
| 10 | 6, 9 | mulcld 11281 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 · 𝐴) ∈ ℂ) |
| 11 | 10 | coscld 16167 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝐴)) ∈ ℂ) |
| 12 | 3, 11 | fsumcl 15769 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) ∈ ℂ) |
| 13 | 2, 12 | addcld 11280 |
. . . . . . 7
⊢ (𝜑 → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) ∈ ℂ) |
| 14 | 8 | sincld 16166 |
. . . . . . 7
⊢ (𝜑 → (sin‘𝐴) ∈
ℂ) |
| 15 | | dirkertrigeqlem2.sinne0 |
. . . . . . 7
⊢ (𝜑 → (sin‘𝐴) ≠ 0) |
| 16 | 13, 14, 15 | divcan4d 12049 |
. . . . . 6
⊢ (𝜑 → ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) · (sin‘𝐴)) / (sin‘𝐴)) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)))) |
| 17 | 16 | eqcomd 2743 |
. . . . 5
⊢ (𝜑 → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) = ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) · (sin‘𝐴)) / (sin‘𝐴))) |
| 18 | 3, 14, 11 | fsummulc1 15821 |
. . . . . . . . 9
⊢ (𝜑 → (Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) · (sin‘𝐴)) = Σ𝑛 ∈ (1...𝑁)((cos‘(𝑛 · 𝐴)) · (sin‘𝐴))) |
| 19 | 14 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘𝐴) ∈ ℂ) |
| 20 | 11, 19 | mulcomd 11282 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝐴)) · (sin‘𝐴)) = ((sin‘𝐴) · (cos‘(𝑛 · 𝐴)))) |
| 21 | | sinmulcos 45880 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ (𝑛 · 𝐴) ∈ ℂ) → ((sin‘𝐴) · (cos‘(𝑛 · 𝐴))) = (((sin‘(𝐴 + (𝑛 · 𝐴))) + (sin‘(𝐴 − (𝑛 · 𝐴)))) / 2)) |
| 22 | 9, 10, 21 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘𝐴) · (cos‘(𝑛 · 𝐴))) = (((sin‘(𝐴 + (𝑛 · 𝐴))) + (sin‘(𝐴 − (𝑛 · 𝐴)))) / 2)) |
| 23 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 1 ∈ ℂ) |
| 24 | 6, 23, 9 | adddird 11286 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑛 + 1) · 𝐴) = ((𝑛 · 𝐴) + (1 · 𝐴))) |
| 25 | 23, 9 | mulcld 11281 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (1 · 𝐴) ∈ ℂ) |
| 26 | 10, 25 | addcomd 11463 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑛 · 𝐴) + (1 · 𝐴)) = ((1 · 𝐴) + (𝑛 · 𝐴))) |
| 27 | 8 | mullidd 11279 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1 · 𝐴) = 𝐴) |
| 28 | 27 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1 · 𝐴) + (𝑛 · 𝐴)) = (𝐴 + (𝑛 · 𝐴))) |
| 29 | 28 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((1 · 𝐴) + (𝑛 · 𝐴)) = (𝐴 + (𝑛 · 𝐴))) |
| 30 | 24, 26, 29 | 3eqtrrd 2782 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐴 + (𝑛 · 𝐴)) = ((𝑛 + 1) · 𝐴)) |
| 31 | 30 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘(𝐴 + (𝑛 · 𝐴))) = (sin‘((𝑛 + 1) · 𝐴))) |
| 32 | 10, 9 | negsubdi2d 11636 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → -((𝑛 · 𝐴) − 𝐴) = (𝐴 − (𝑛 · 𝐴))) |
| 33 | 32 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐴 − (𝑛 · 𝐴)) = -((𝑛 · 𝐴) − 𝐴)) |
| 34 | 33 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘(𝐴 − (𝑛 · 𝐴))) = (sin‘-((𝑛 · 𝐴) − 𝐴))) |
| 35 | 10, 9 | subcld 11620 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑛 · 𝐴) − 𝐴) ∈ ℂ) |
| 36 | | sinneg 16182 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 · 𝐴) − 𝐴) ∈ ℂ → (sin‘-((𝑛 · 𝐴) − 𝐴)) = -(sin‘((𝑛 · 𝐴) − 𝐴))) |
| 37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘-((𝑛 · 𝐴) − 𝐴)) = -(sin‘((𝑛 · 𝐴) − 𝐴))) |
| 38 | 34, 37 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘(𝐴 − (𝑛 · 𝐴))) = -(sin‘((𝑛 · 𝐴) − 𝐴))) |
| 39 | 31, 38 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘(𝐴 + (𝑛 · 𝐴))) + (sin‘(𝐴 − (𝑛 · 𝐴)))) = ((sin‘((𝑛 + 1) · 𝐴)) + -(sin‘((𝑛 · 𝐴) − 𝐴)))) |
| 40 | 9, 10 | addcld 11280 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐴 + (𝑛 · 𝐴)) ∈ ℂ) |
| 41 | 40 | sincld 16166 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘(𝐴 + (𝑛 · 𝐴))) ∈ ℂ) |
| 42 | 31, 41 | eqeltrrd 2842 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘((𝑛 + 1) · 𝐴)) ∈ ℂ) |
| 43 | 35 | sincld 16166 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘((𝑛 · 𝐴) − 𝐴)) ∈ ℂ) |
| 44 | 42, 43 | negsubd 11626 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘((𝑛 + 1) · 𝐴)) + -(sin‘((𝑛 · 𝐴) − 𝐴))) = ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 · 𝐴) − 𝐴)))) |
| 45 | 6, 9 | mulsubfacd 11724 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑛 · 𝐴) − 𝐴) = ((𝑛 − 1) · 𝐴)) |
| 46 | 45 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘((𝑛 · 𝐴) − 𝐴)) = (sin‘((𝑛 − 1) · 𝐴))) |
| 47 | 46 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 · 𝐴) − 𝐴))) = ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) |
| 48 | 39, 44, 47 | 3eqtrd 2781 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘(𝐴 + (𝑛 · 𝐴))) + (sin‘(𝐴 − (𝑛 · 𝐴)))) = ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) |
| 49 | 48 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((sin‘(𝐴 + (𝑛 · 𝐴))) + (sin‘(𝐴 − (𝑛 · 𝐴)))) / 2) = (((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2)) |
| 50 | 20, 22, 49 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝐴)) · (sin‘𝐴)) = (((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2)) |
| 51 | 50 | sumeq2dv 15738 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)((cos‘(𝑛 · 𝐴)) · (sin‘𝐴)) = Σ𝑛 ∈ (1...𝑁)(((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2)) |
| 52 | | 2cnd 12344 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℂ) |
| 53 | | peano2cnm 11575 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℂ → (𝑛 − 1) ∈
ℂ) |
| 54 | 6, 53 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 − 1) ∈ ℂ) |
| 55 | 54, 9 | mulcld 11281 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑛 − 1) · 𝐴) ∈ ℂ) |
| 56 | 55 | sincld 16166 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘((𝑛 − 1) · 𝐴)) ∈ ℂ) |
| 57 | 42, 56 | subcld 11620 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) ∈ ℂ) |
| 58 | | 2ne0 12370 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
| 59 | 58 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ≠ 0) |
| 60 | 3, 52, 57, 59 | fsumdivc 15822 |
. . . . . . . . . 10
⊢ (𝜑 → (Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2) = Σ𝑛 ∈ (1...𝑁)(((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2)) |
| 61 | 3, 57 | fsumcl 15769 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) ∈ ℂ) |
| 62 | 61, 52, 59 | divrec2d 12047 |
. . . . . . . . . 10
⊢ (𝜑 → (Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2) = ((1 / 2) · Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) |
| 63 | 60, 62 | eqtr3d 2779 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)(((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2) = ((1 / 2) · Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) |
| 64 | 18, 51, 63 | 3eqtrd 2781 |
. . . . . . . 8
⊢ (𝜑 → (Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) · (sin‘𝐴)) = ((1 / 2) · Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) |
| 65 | 64 | oveq2d 7447 |
. . . . . . 7
⊢ (𝜑 → (((1 / 2) ·
(sin‘𝐴)) +
(Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) · (sin‘𝐴))) = (((1 / 2) · (sin‘𝐴)) + ((1 / 2) ·
Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))))) |
| 66 | 2, 12, 14 | adddird 11286 |
. . . . . . 7
⊢ (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) · (sin‘𝐴)) = (((1 / 2) · (sin‘𝐴)) + (Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) · (sin‘𝐴)))) |
| 67 | 2, 14, 61 | adddid 11285 |
. . . . . . 7
⊢ (𝜑 → ((1 / 2) ·
((sin‘𝐴) +
Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) = (((1 / 2) · (sin‘𝐴)) + ((1 / 2) ·
Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))))) |
| 68 | 65, 66, 67 | 3eqtr4d 2787 |
. . . . . 6
⊢ (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) · (sin‘𝐴)) = ((1 / 2) · ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))))) |
| 69 | 68 | oveq1d 7446 |
. . . . 5
⊢ (𝜑 → ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) · (sin‘𝐴)) / (sin‘𝐴)) = (((1 / 2) · ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) / (sin‘𝐴))) |
| 70 | 10 | sincld 16166 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝐴)) ∈ ℂ) |
| 71 | 42, 70, 56 | npncand 11644 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) = ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) |
| 72 | 71 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = (((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) |
| 73 | 72 | sumeq2dv 15738 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = Σ𝑛 ∈ (1...𝑁)(((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) |
| 74 | 42, 70 | subcld 11620 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) ∈ ℂ) |
| 75 | 70, 56 | subcld 11620 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) ∈ ℂ) |
| 76 | 3, 74, 75 | fsumadd 15776 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)(((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) = (Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + Σ𝑛 ∈ (1...𝑁)((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) |
| 77 | | fvoveq1 7454 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑛 → (sin‘(𝑗 · 𝐴)) = (sin‘(𝑛 · 𝐴))) |
| 78 | | fvoveq1 7454 |
. . . . . . . . . . . 12
⊢ (𝑗 = (𝑛 + 1) → (sin‘(𝑗 · 𝐴)) = (sin‘((𝑛 + 1) · 𝐴))) |
| 79 | | fvoveq1 7454 |
. . . . . . . . . . . 12
⊢ (𝑗 = 1 → (sin‘(𝑗 · 𝐴)) = (sin‘(1 · 𝐴))) |
| 80 | | fvoveq1 7454 |
. . . . . . . . . . . 12
⊢ (𝑗 = (𝑁 + 1) → (sin‘(𝑗 · 𝐴)) = (sin‘((𝑁 + 1) · 𝐴))) |
| 81 | | dirkertrigeqlem2.n |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 82 | 81 | nnzd 12640 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 83 | | nnuz 12921 |
. . . . . . . . . . . . . 14
⊢ ℕ =
(ℤ≥‘1) |
| 84 | 81, 83 | eleqtrdi 2851 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
| 85 | | peano2uz 12943 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘1) → (𝑁 + 1) ∈
(ℤ≥‘1)) |
| 86 | 84, 85 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘1)) |
| 87 | | elfzelz 13564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℤ) |
| 88 | 87 | zcnd 12723 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℂ) |
| 89 | 88 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (1...(𝑁 + 1))) → 𝑗 ∈ ℂ) |
| 90 | 8 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (1...(𝑁 + 1))) → 𝐴 ∈ ℂ) |
| 91 | 89, 90 | mulcld 11281 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...(𝑁 + 1))) → (𝑗 · 𝐴) ∈ ℂ) |
| 92 | 91 | sincld 16166 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...(𝑁 + 1))) → (sin‘(𝑗 · 𝐴)) ∈ ℂ) |
| 93 | 77, 78, 79, 80, 82, 86, 92 | telfsum2 15841 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) = ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴)))) |
| 94 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (1...𝑁) → 1 ∈ ℂ) |
| 95 | 5, 94 | pncand 11621 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (1...𝑁) → ((𝑛 + 1) − 1) = 𝑛) |
| 96 | 95 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 = ((𝑛 + 1) − 1)) |
| 97 | 96 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 = ((𝑛 + 1) − 1)) |
| 98 | 97 | fvoveq1d 7453 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝐴)) = (sin‘(((𝑛 + 1) − 1) · 𝐴))) |
| 99 | 98 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = ((sin‘(((𝑛 + 1) − 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) |
| 100 | 99 | sumeq2dv 15738 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = Σ𝑛 ∈ (1...𝑁)((sin‘(((𝑛 + 1) − 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) |
| 101 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑛 → (𝑗 − 1) = (𝑛 − 1)) |
| 102 | 101 | fvoveq1d 7453 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑛 → (sin‘((𝑗 − 1) · 𝐴)) = (sin‘((𝑛 − 1) · 𝐴))) |
| 103 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = (𝑛 + 1) → (𝑗 − 1) = ((𝑛 + 1) − 1)) |
| 104 | 103 | fvoveq1d 7453 |
. . . . . . . . . . . . 13
⊢ (𝑗 = (𝑛 + 1) → (sin‘((𝑗 − 1) · 𝐴)) = (sin‘(((𝑛 + 1) − 1) · 𝐴))) |
| 105 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 1 → (𝑗 − 1) = (1 − 1)) |
| 106 | 105 | fvoveq1d 7453 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 1 → (sin‘((𝑗 − 1) · 𝐴)) = (sin‘((1 − 1)
· 𝐴))) |
| 107 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = (𝑁 + 1) → (𝑗 − 1) = ((𝑁 + 1) − 1)) |
| 108 | 107 | fvoveq1d 7453 |
. . . . . . . . . . . . 13
⊢ (𝑗 = (𝑁 + 1) → (sin‘((𝑗 − 1) · 𝐴)) = (sin‘(((𝑁 + 1) − 1) · 𝐴))) |
| 109 | | 1cnd 11256 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (1...(𝑁 + 1))) → 1 ∈
ℂ) |
| 110 | 89, 109 | subcld 11620 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (1...(𝑁 + 1))) → (𝑗 − 1) ∈ ℂ) |
| 111 | 110, 90 | mulcld 11281 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (1...(𝑁 + 1))) → ((𝑗 − 1) · 𝐴) ∈ ℂ) |
| 112 | 111 | sincld 16166 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...(𝑁 + 1))) → (sin‘((𝑗 − 1) · 𝐴)) ∈
ℂ) |
| 113 | 102, 104,
106, 108, 82, 86, 112 | telfsum2 15841 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘(((𝑛 + 1) − 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = ((sin‘(((𝑁 + 1) − 1) · 𝐴)) − (sin‘((1 − 1)
· 𝐴)))) |
| 114 | 81 | nnred 12281 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 115 | 114 | recnd 11289 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 116 | 115, 1 | pncand 11621 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁) |
| 117 | 116 | fvoveq1d 7453 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (sin‘(((𝑁 + 1) − 1) · 𝐴)) = (sin‘(𝑁 · 𝐴))) |
| 118 | 1 | subidd 11608 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1 − 1) =
0) |
| 119 | 118 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1 − 1) ·
𝐴) = (0 · 𝐴)) |
| 120 | 8 | mul02d 11459 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (0 · 𝐴) = 0) |
| 121 | 119, 120 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((1 − 1) ·
𝐴) = 0) |
| 122 | 121 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (sin‘((1 − 1)
· 𝐴)) =
(sin‘0)) |
| 123 | | sin0 16185 |
. . . . . . . . . . . . . . 15
⊢
(sin‘0) = 0 |
| 124 | 123 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (sin‘0) =
0) |
| 125 | 122, 124 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (sin‘((1 − 1)
· 𝐴)) =
0) |
| 126 | 117, 125 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((sin‘(((𝑁 + 1) − 1) · 𝐴)) − (sin‘((1
− 1) · 𝐴))) =
((sin‘(𝑁 ·
𝐴)) −
0)) |
| 127 | 100, 113,
126 | 3eqtrd 2781 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = ((sin‘(𝑁 · 𝐴)) − 0)) |
| 128 | 93, 127 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝜑 → (Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + Σ𝑛 ∈ (1...𝑁)((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) = (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0))) |
| 129 | 73, 76, 128 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0))) |
| 130 | 129 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝜑 → ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) = ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)))) |
| 131 | 27 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝜑 → (sin‘(1 ·
𝐴)) = (sin‘𝐴)) |
| 132 | 131 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝜑 → ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) = ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) |
| 133 | 132 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝜑 → (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)) = (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)) + ((sin‘(𝑁 · 𝐴)) − 0))) |
| 134 | 133 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0))) = ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)) + ((sin‘(𝑁 · 𝐴)) − 0)))) |
| 135 | 115, 1 | addcld 11280 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 + 1) ∈ ℂ) |
| 136 | 135, 8 | mulcld 11281 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑁 + 1) · 𝐴) ∈ ℂ) |
| 137 | 136 | sincld 16166 |
. . . . . . . . . . . 12
⊢ (𝜑 → (sin‘((𝑁 + 1) · 𝐴)) ∈ ℂ) |
| 138 | 137, 14 | subcld 11620 |
. . . . . . . . . . 11
⊢ (𝜑 → ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)) ∈ ℂ) |
| 139 | 115, 8 | mulcld 11281 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 · 𝐴) ∈ ℂ) |
| 140 | 139 | sincld 16166 |
. . . . . . . . . . . 12
⊢ (𝜑 → (sin‘(𝑁 · 𝐴)) ∈ ℂ) |
| 141 | | 0cnd 11254 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈
ℂ) |
| 142 | 140, 141 | subcld 11620 |
. . . . . . . . . . 11
⊢ (𝜑 → ((sin‘(𝑁 · 𝐴)) − 0) ∈
ℂ) |
| 143 | 14, 138, 142 | addassd 11283 |
. . . . . . . . . 10
⊢ (𝜑 → (((sin‘𝐴) + ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)) = ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)) + ((sin‘(𝑁 · 𝐴)) − 0)))) |
| 144 | 143 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝜑 → ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)) + ((sin‘(𝑁 · 𝐴)) − 0))) = (((sin‘𝐴) + ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0))) |
| 145 | 14, 137 | pncan3d 11623 |
. . . . . . . . . . 11
⊢ (𝜑 → ((sin‘𝐴) + ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) = (sin‘((𝑁 + 1) · 𝐴))) |
| 146 | 140 | subid1d 11609 |
. . . . . . . . . . 11
⊢ (𝜑 → ((sin‘(𝑁 · 𝐴)) − 0) = (sin‘(𝑁 · 𝐴))) |
| 147 | 145, 146 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝜑 → (((sin‘𝐴) + ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)) = ((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴)))) |
| 148 | 137, 140 | addcomd 11463 |
. . . . . . . . . 10
⊢ (𝜑 → ((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))) = ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) |
| 149 | 147, 148 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → (((sin‘𝐴) + ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)) = ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) |
| 150 | 134, 144,
149 | 3eqtrd 2781 |
. . . . . . . 8
⊢ (𝜑 → ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0))) = ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) |
| 151 | 130, 150 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) = ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) |
| 152 | 151 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → ((1 / 2) ·
((sin‘𝐴) +
Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) = ((1 / 2) · ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))))) |
| 153 | 152 | oveq1d 7446 |
. . . . 5
⊢ (𝜑 → (((1 / 2) ·
((sin‘𝐴) +
Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) / (sin‘𝐴)) = (((1 / 2) · ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) / (sin‘𝐴))) |
| 154 | 17, 69, 153 | 3eqtrd 2781 |
. . . 4
⊢ (𝜑 → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) = (((1 / 2) · ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) / (sin‘𝐴))) |
| 155 | | halfre 12480 |
. . . . . . . . . . . 12
⊢ (1 / 2)
∈ ℝ |
| 156 | 155 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 / 2) ∈
ℝ) |
| 157 | 114, 156 | readdcld 11290 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 + (1 / 2)) ∈ ℝ) |
| 158 | 157, 7 | remulcld 11291 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝐴) ∈ ℝ) |
| 159 | 158 | recnd 11289 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝐴) ∈ ℂ) |
| 160 | 2, 8 | mulcld 11281 |
. . . . . . . 8
⊢ (𝜑 → ((1 / 2) · 𝐴) ∈
ℂ) |
| 161 | | sinmulcos 45880 |
. . . . . . . 8
⊢ ((((𝑁 + (1 / 2)) · 𝐴) ∈ ℂ ∧ ((1 / 2)
· 𝐴) ∈ ℂ)
→ ((sin‘((𝑁 + (1
/ 2)) · 𝐴)) ·
(cos‘((1 / 2) · 𝐴))) = (((sin‘(((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴))) + (sin‘(((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴)))) / 2)) |
| 162 | 159, 160,
161 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2)
· 𝐴))) =
(((sin‘(((𝑁 + (1 /
2)) · 𝐴) + ((1 / 2)
· 𝐴))) +
(sin‘(((𝑁 + (1 / 2))
· 𝐴) − ((1 /
2) · 𝐴)))) /
2)) |
| 163 | 115, 2, 8 | adddird 11286 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁 + (1 / 2)) · 𝐴) = ((𝑁 · 𝐴) + ((1 / 2) · 𝐴))) |
| 164 | 163 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴)) = (((𝑁 · 𝐴) + ((1 / 2) · 𝐴)) + ((1 / 2) · 𝐴))) |
| 165 | 139, 160,
160 | addassd 11283 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑁 · 𝐴) + ((1 / 2) · 𝐴)) + ((1 / 2) · 𝐴)) = ((𝑁 · 𝐴) + (((1 / 2) · 𝐴) + ((1 / 2) · 𝐴)))) |
| 166 | 2, 2, 8 | adddird 11286 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((1 / 2) + (1 / 2))
· 𝐴) = (((1 / 2)
· 𝐴) + ((1 / 2)
· 𝐴))) |
| 167 | 1 | 2halvesd 12512 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((1 / 2) + (1 / 2)) =
1) |
| 168 | 167 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((1 / 2) + (1 / 2))
· 𝐴) = (1 ·
𝐴)) |
| 169 | 166, 168 | eqtr3d 2779 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((1 / 2) · 𝐴) + ((1 / 2) · 𝐴)) = (1 · 𝐴)) |
| 170 | 169 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁 · 𝐴) + (((1 / 2) · 𝐴) + ((1 / 2) · 𝐴))) = ((𝑁 · 𝐴) + (1 · 𝐴))) |
| 171 | 115, 1, 8 | adddird 11286 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁 + 1) · 𝐴) = ((𝑁 · 𝐴) + (1 · 𝐴))) |
| 172 | 170, 171 | eqtr4d 2780 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 · 𝐴) + (((1 / 2) · 𝐴) + ((1 / 2) · 𝐴))) = ((𝑁 + 1) · 𝐴)) |
| 173 | 164, 165,
172 | 3eqtrrd 2782 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁 + 1) · 𝐴) = (((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴))) |
| 174 | 173 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝜑 → (sin‘((𝑁 + 1) · 𝐴)) = (sin‘(((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴)))) |
| 175 | 163 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴)) = (((𝑁 · 𝐴) + ((1 / 2) · 𝐴)) − ((1 / 2) · 𝐴))) |
| 176 | 139, 160 | pncand 11621 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑁 · 𝐴) + ((1 / 2) · 𝐴)) − ((1 / 2) · 𝐴)) = (𝑁 · 𝐴)) |
| 177 | 175, 176 | eqtr2d 2778 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 · 𝐴) = (((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴))) |
| 178 | 177 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝜑 → (sin‘(𝑁 · 𝐴)) = (sin‘(((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴)))) |
| 179 | 174, 178 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝜑 → ((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))) = ((sin‘(((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴))) + (sin‘(((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴))))) |
| 180 | 179 | oveq1d 7446 |
. . . . . . 7
⊢ (𝜑 → (((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))) / 2) = (((sin‘(((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴))) + (sin‘(((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴)))) / 2)) |
| 181 | 162, 180 | eqtr4d 2780 |
. . . . . 6
⊢ (𝜑 → ((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2)
· 𝐴))) =
(((sin‘((𝑁 + 1)
· 𝐴)) +
(sin‘(𝑁 ·
𝐴))) / 2)) |
| 182 | 148 | oveq1d 7446 |
. . . . . 6
⊢ (𝜑 → (((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))) / 2) = (((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))) / 2)) |
| 183 | 140, 137 | addcld 11280 |
. . . . . . 7
⊢ (𝜑 → ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))) ∈ ℂ) |
| 184 | 183, 52, 59 | divrec2d 12047 |
. . . . . 6
⊢ (𝜑 → (((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))) / 2) = ((1 / 2) ·
((sin‘(𝑁 ·
𝐴)) + (sin‘((𝑁 + 1) · 𝐴))))) |
| 185 | 181, 182,
184 | 3eqtrrd 2782 |
. . . . 5
⊢ (𝜑 → ((1 / 2) ·
((sin‘(𝑁 ·
𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) ·
𝐴)))) |
| 186 | 185 | oveq1d 7446 |
. . . 4
⊢ (𝜑 → (((1 / 2) ·
((sin‘(𝑁 ·
𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) / (sin‘𝐴)) = (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) ·
𝐴))) / (sin‘𝐴))) |
| 187 | 8, 52, 59 | divcan2d 12045 |
. . . . . . . . 9
⊢ (𝜑 → (2 · (𝐴 / 2)) = 𝐴) |
| 188 | 187 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 = (2 · (𝐴 / 2))) |
| 189 | 188 | fveq2d 6910 |
. . . . . . 7
⊢ (𝜑 → (sin‘𝐴) = (sin‘(2 ·
(𝐴 / 2)))) |
| 190 | 8 | halfcld 12511 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 / 2) ∈ ℂ) |
| 191 | | sin2t 16213 |
. . . . . . . 8
⊢ ((𝐴 / 2) ∈ ℂ →
(sin‘(2 · (𝐴 /
2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))))) |
| 192 | 190, 191 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (sin‘(2 ·
(𝐴 / 2))) = (2 ·
((sin‘(𝐴 / 2))
· (cos‘(𝐴 /
2))))) |
| 193 | 189, 192 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → (sin‘𝐴) = (2 ·
((sin‘(𝐴 / 2))
· (cos‘(𝐴 /
2))))) |
| 194 | 193 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2)
· 𝐴))) /
(sin‘𝐴)) =
(((sin‘((𝑁 + (1 / 2))
· 𝐴)) ·
(cos‘((1 / 2) · 𝐴))) / (2 · ((sin‘(𝐴 / 2)) ·
(cos‘(𝐴 /
2)))))) |
| 195 | 190 | sincld 16166 |
. . . . . . . 8
⊢ (𝜑 → (sin‘(𝐴 / 2)) ∈
ℂ) |
| 196 | 190 | coscld 16167 |
. . . . . . . 8
⊢ (𝜑 → (cos‘(𝐴 / 2)) ∈
ℂ) |
| 197 | 52, 195, 196 | mulassd 11284 |
. . . . . . 7
⊢ (𝜑 → ((2 ·
(sin‘(𝐴 / 2)))
· (cos‘(𝐴 /
2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))))) |
| 198 | 8, 52, 59 | divrec2d 12047 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 / 2) = ((1 / 2) · 𝐴)) |
| 199 | 198 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝜑 → (cos‘(𝐴 / 2)) = (cos‘((1 / 2)
· 𝐴))) |
| 200 | 199 | oveq2d 7447 |
. . . . . . 7
⊢ (𝜑 → ((2 ·
(sin‘(𝐴 / 2)))
· (cos‘(𝐴 /
2))) = ((2 · (sin‘(𝐴 / 2))) · (cos‘((1 / 2)
· 𝐴)))) |
| 201 | 197, 200 | eqtr3d 2779 |
. . . . . 6
⊢ (𝜑 → (2 ·
((sin‘(𝐴 / 2))
· (cos‘(𝐴 /
2)))) = ((2 · (sin‘(𝐴 / 2))) · (cos‘((1 / 2)
· 𝐴)))) |
| 202 | 201 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2)
· 𝐴))) / (2 ·
((sin‘(𝐴 / 2))
· (cos‘(𝐴 /
2))))) = (((sin‘((𝑁 +
(1 / 2)) · 𝐴))
· (cos‘((1 / 2) · 𝐴))) / ((2 · (sin‘(𝐴 / 2))) · (cos‘((1
/ 2) · 𝐴))))) |
| 203 | 159 | sincld 16166 |
. . . . . 6
⊢ (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝐴)) ∈
ℂ) |
| 204 | 52, 195 | mulcld 11281 |
. . . . . 6
⊢ (𝜑 → (2 ·
(sin‘(𝐴 / 2))) ∈
ℂ) |
| 205 | 160 | coscld 16167 |
. . . . . 6
⊢ (𝜑 → (cos‘((1 / 2)
· 𝐴)) ∈
ℂ) |
| 206 | 195, 196 | mulcld 11281 |
. . . . . . . . 9
⊢ (𝜑 → ((sin‘(𝐴 / 2)) ·
(cos‘(𝐴 / 2))) ∈
ℂ) |
| 207 | 193, 15 | eqnetrrd 3009 |
. . . . . . . . 9
⊢ (𝜑 → (2 ·
((sin‘(𝐴 / 2))
· (cos‘(𝐴 /
2)))) ≠ 0) |
| 208 | 52, 206, 207 | mulne0bbd 11919 |
. . . . . . . 8
⊢ (𝜑 → ((sin‘(𝐴 / 2)) ·
(cos‘(𝐴 / 2))) ≠
0) |
| 209 | 195, 196,
208 | mulne0bad 11918 |
. . . . . . 7
⊢ (𝜑 → (sin‘(𝐴 / 2)) ≠ 0) |
| 210 | 52, 195, 59, 209 | mulne0d 11915 |
. . . . . 6
⊢ (𝜑 → (2 ·
(sin‘(𝐴 / 2))) ≠
0) |
| 211 | 195, 196,
208 | mulne0bbd 11919 |
. . . . . . 7
⊢ (𝜑 → (cos‘(𝐴 / 2)) ≠ 0) |
| 212 | 199, 211 | eqnetrrd 3009 |
. . . . . 6
⊢ (𝜑 → (cos‘((1 / 2)
· 𝐴)) ≠
0) |
| 213 | 203, 204,
205, 210, 212 | divcan5rd 12070 |
. . . . 5
⊢ (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2)
· 𝐴))) / ((2
· (sin‘(𝐴 /
2))) · (cos‘((1 / 2) · 𝐴)))) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (2 · (sin‘(𝐴 / 2))))) |
| 214 | 194, 202,
213 | 3eqtrd 2781 |
. . . 4
⊢ (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2)
· 𝐴))) /
(sin‘𝐴)) =
((sin‘((𝑁 + (1 / 2))
· 𝐴)) / (2 ·
(sin‘(𝐴 /
2))))) |
| 215 | 154, 186,
214 | 3eqtrd 2781 |
. . 3
⊢ (𝜑 → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (2 · (sin‘(𝐴 / 2))))) |
| 216 | 215 | oveq1d 7446 |
. 2
⊢ (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = (((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (2 ·
(sin‘(𝐴 / 2)))) /
π)) |
| 217 | | picn 26501 |
. . . 4
⊢ π
∈ ℂ |
| 218 | 217 | a1i 11 |
. . 3
⊢ (𝜑 → π ∈
ℂ) |
| 219 | | pire 26500 |
. . . . 5
⊢ π
∈ ℝ |
| 220 | | pipos 26502 |
. . . . 5
⊢ 0 <
π |
| 221 | 219, 220 | gt0ne0ii 11799 |
. . . 4
⊢ π ≠
0 |
| 222 | 221 | a1i 11 |
. . 3
⊢ (𝜑 → π ≠
0) |
| 223 | 203, 204,
218, 210, 222 | divdiv32d 12068 |
. 2
⊢ (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (2 ·
(sin‘(𝐴 / 2)))) /
π) = (((sin‘((𝑁 +
(1 / 2)) · 𝐴)) /
π) / (2 · (sin‘(𝐴 / 2))))) |
| 224 | 203, 218,
204, 222, 210 | divdiv1d 12074 |
. . 3
⊢ (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) / π) / (2 ·
(sin‘(𝐴 / 2)))) =
((sin‘((𝑁 + (1 / 2))
· 𝐴)) / (π
· (2 · (sin‘(𝐴 / 2)))))) |
| 225 | 218, 52, 195 | mulassd 11284 |
. . . . 5
⊢ (𝜑 → ((π · 2)
· (sin‘(𝐴 /
2))) = (π · (2 · (sin‘(𝐴 / 2))))) |
| 226 | 218, 52 | mulcomd 11282 |
. . . . . 6
⊢ (𝜑 → (π · 2) = (2
· π)) |
| 227 | 226 | oveq1d 7446 |
. . . . 5
⊢ (𝜑 → ((π · 2)
· (sin‘(𝐴 /
2))) = ((2 · π) · (sin‘(𝐴 / 2)))) |
| 228 | 225, 227 | eqtr3d 2779 |
. . . 4
⊢ (𝜑 → (π · (2 ·
(sin‘(𝐴 / 2)))) = ((2
· π) · (sin‘(𝐴 / 2)))) |
| 229 | 228 | oveq2d 7447 |
. . 3
⊢ (𝜑 → ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (π · (2 ·
(sin‘(𝐴 / 2))))) =
((sin‘((𝑁 + (1 / 2))
· 𝐴)) / ((2 ·
π) · (sin‘(𝐴 / 2))))) |
| 230 | 224, 229 | eqtrd 2777 |
. 2
⊢ (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) / π) / (2 ·
(sin‘(𝐴 / 2)))) =
((sin‘((𝑁 + (1 / 2))
· 𝐴)) / ((2 ·
π) · (sin‘(𝐴 / 2))))) |
| 231 | 216, 223,
230 | 3eqtrd 2781 |
1
⊢ (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) ·
(sin‘(𝐴 /
2))))) |