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

Theorem dirkertrigeqlem2 40956
Description: Trigonomic equality lemma for the Dirichlet Kernel trigonomic equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
dirkertrigeqlem2.a (𝜑𝐴 ∈ ℝ)
dirkertrigeqlem2.sinne0 (𝜑 → (sin‘𝐴) ≠ 0)
dirkertrigeqlem2.n (𝜑𝑁 ∈ ℕ)
Assertion
Ref Expression
dirkertrigeqlem2 (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) · (sin‘(𝐴 / 2)))))
Distinct variable groups:   𝐴,𝑛   𝑛,𝑁   𝜑,𝑛

Proof of Theorem dirkertrigeqlem2
Dummy variable 𝑗 is distinct from all other variables.
StepHypRef Expression
1 1cnd 10290 . . . . . . . . 9 (𝜑 → 1 ∈ ℂ)
21halfcld 11525 . . . . . . . 8 (𝜑 → (1 / 2) ∈ ℂ)
3 fzfid 12983 . . . . . . . . 9 (𝜑 → (1...𝑁) ∈ Fin)
4 elfzelz 12552 . . . . . . . . . . . . 13 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℤ)
54zcnd 11733 . . . . . . . . . . . 12 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
65adantl 473 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℂ)
7 dirkertrigeqlem2.a . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℝ)
87recnd 10324 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℂ)
98adantr 472 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → 𝐴 ∈ ℂ)
106, 9mulcld 10316 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑛 · 𝐴) ∈ ℂ)
1110coscld 15146 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝐴)) ∈ ℂ)
123, 11fsumcl 14752 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) ∈ ℂ)
132, 12addcld 10315 . . . . . . 7 (𝜑 → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) ∈ ℂ)
148sincld 15145 . . . . . . 7 (𝜑 → (sin‘𝐴) ∈ ℂ)
15 dirkertrigeqlem2.sinne0 . . . . . . 7 (𝜑 → (sin‘𝐴) ≠ 0)
1613, 14, 15divcan4d 11063 . . . . . 6 (𝜑 → ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) · (sin‘𝐴)) / (sin‘𝐴)) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))))
1716eqcomd 2771 . . . . 5 (𝜑 → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) = ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) · (sin‘𝐴)) / (sin‘𝐴)))
183, 14, 11fsummulc1 14804 . . . . . . . . 9 (𝜑 → (Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) · (sin‘𝐴)) = Σ𝑛 ∈ (1...𝑁)((cos‘(𝑛 · 𝐴)) · (sin‘𝐴)))
1914adantr 472 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘𝐴) ∈ ℂ)
2011, 19mulcomd 10317 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝐴)) · (sin‘𝐴)) = ((sin‘𝐴) · (cos‘(𝑛 · 𝐴))))
21 sinmulcos 40717 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ (𝑛 · 𝐴) ∈ ℂ) → ((sin‘𝐴) · (cos‘(𝑛 · 𝐴))) = (((sin‘(𝐴 + (𝑛 · 𝐴))) + (sin‘(𝐴 − (𝑛 · 𝐴)))) / 2))
229, 10, 21syl2anc 579 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘𝐴) · (cos‘(𝑛 · 𝐴))) = (((sin‘(𝐴 + (𝑛 · 𝐴))) + (sin‘(𝐴 − (𝑛 · 𝐴)))) / 2))
23 1cnd 10290 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (1...𝑁)) → 1 ∈ ℂ)
246, 23, 9adddird 10321 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑛 + 1) · 𝐴) = ((𝑛 · 𝐴) + (1 · 𝐴)))
2523, 9mulcld 10316 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (1...𝑁)) → (1 · 𝐴) ∈ ℂ)
2610, 25addcomd 10494 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑛 · 𝐴) + (1 · 𝐴)) = ((1 · 𝐴) + (𝑛 · 𝐴)))
278mulid2d 10314 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1 · 𝐴) = 𝐴)
2827oveq1d 6859 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1 · 𝐴) + (𝑛 · 𝐴)) = (𝐴 + (𝑛 · 𝐴)))
2928adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...𝑁)) → ((1 · 𝐴) + (𝑛 · 𝐴)) = (𝐴 + (𝑛 · 𝐴)))
3024, 26, 293eqtrrd 2804 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...𝑁)) → (𝐴 + (𝑛 · 𝐴)) = ((𝑛 + 1) · 𝐴))
3130fveq2d 6381 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝐴 + (𝑛 · 𝐴))) = (sin‘((𝑛 + 1) · 𝐴)))
3210, 9negsubdi2d 10664 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (1...𝑁)) → -((𝑛 · 𝐴) − 𝐴) = (𝐴 − (𝑛 · 𝐴)))
3332eqcomd 2771 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...𝑁)) → (𝐴 − (𝑛 · 𝐴)) = -((𝑛 · 𝐴) − 𝐴))
3433fveq2d 6381 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝐴 − (𝑛 · 𝐴))) = (sin‘-((𝑛 · 𝐴) − 𝐴)))
3510, 9subcld 10648 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑛 · 𝐴) − 𝐴) ∈ ℂ)
36 sinneg 15161 . . . . . . . . . . . . . . . 16 (((𝑛 · 𝐴) − 𝐴) ∈ ℂ → (sin‘-((𝑛 · 𝐴) − 𝐴)) = -(sin‘((𝑛 · 𝐴) − 𝐴)))
3735, 36syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘-((𝑛 · 𝐴) − 𝐴)) = -(sin‘((𝑛 · 𝐴) − 𝐴)))
3834, 37eqtrd 2799 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝐴 − (𝑛 · 𝐴))) = -(sin‘((𝑛 · 𝐴) − 𝐴)))
3931, 38oveq12d 6862 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘(𝐴 + (𝑛 · 𝐴))) + (sin‘(𝐴 − (𝑛 · 𝐴)))) = ((sin‘((𝑛 + 1) · 𝐴)) + -(sin‘((𝑛 · 𝐴) − 𝐴))))
409, 10addcld 10315 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...𝑁)) → (𝐴 + (𝑛 · 𝐴)) ∈ ℂ)
4140sincld 15145 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝐴 + (𝑛 · 𝐴))) ∈ ℂ)
4231, 41eqeltrrd 2845 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘((𝑛 + 1) · 𝐴)) ∈ ℂ)
4335sincld 15145 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘((𝑛 · 𝐴) − 𝐴)) ∈ ℂ)
4442, 43negsubd 10654 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘((𝑛 + 1) · 𝐴)) + -(sin‘((𝑛 · 𝐴) − 𝐴))) = ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 · 𝐴) − 𝐴))))
456, 9mulsubfacd 10748 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑛 · 𝐴) − 𝐴) = ((𝑛 − 1) · 𝐴))
4645fveq2d 6381 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘((𝑛 · 𝐴) − 𝐴)) = (sin‘((𝑛 − 1) · 𝐴)))
4746oveq2d 6860 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 · 𝐴) − 𝐴))) = ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))
4839, 44, 473eqtrd 2803 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘(𝐴 + (𝑛 · 𝐴))) + (sin‘(𝐴 − (𝑛 · 𝐴)))) = ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))
4948oveq1d 6859 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → (((sin‘(𝐴 + (𝑛 · 𝐴))) + (sin‘(𝐴 − (𝑛 · 𝐴)))) / 2) = (((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2))
5020, 22, 493eqtrd 2803 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝐴)) · (sin‘𝐴)) = (((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2))
5150sumeq2dv 14721 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (1...𝑁)((cos‘(𝑛 · 𝐴)) · (sin‘𝐴)) = Σ𝑛 ∈ (1...𝑁)(((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2))
52 2cnd 11352 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℂ)
53 peano2cnm 10603 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℂ → (𝑛 − 1) ∈ ℂ)
546, 53syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑛 − 1) ∈ ℂ)
5554, 9mulcld 10316 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑛 − 1) · 𝐴) ∈ ℂ)
5655sincld 15145 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘((𝑛 − 1) · 𝐴)) ∈ ℂ)
5742, 56subcld 10648 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) ∈ ℂ)
58 2ne0 11385 . . . . . . . . . . . 12 2 ≠ 0
5958a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ≠ 0)
603, 52, 57, 59fsumdivc 14805 . . . . . . . . . 10 (𝜑 → (Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2) = Σ𝑛 ∈ (1...𝑁)(((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2))
613, 57fsumcl 14752 . . . . . . . . . . 11 (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) ∈ ℂ)
6261, 52, 59divrec2d 11061 . . . . . . . . . 10 (𝜑 → (Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2) = ((1 / 2) · Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))))
6360, 62eqtr3d 2801 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (1...𝑁)(((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2) = ((1 / 2) · Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))))
6418, 51, 633eqtrd 2803 . . . . . . . 8 (𝜑 → (Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) · (sin‘𝐴)) = ((1 / 2) · Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))))
6564oveq2d 6860 . . . . . . 7 (𝜑 → (((1 / 2) · (sin‘𝐴)) + (Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) · (sin‘𝐴))) = (((1 / 2) · (sin‘𝐴)) + ((1 / 2) · Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))))
662, 12, 14adddird 10321 . . . . . . 7 (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) · (sin‘𝐴)) = (((1 / 2) · (sin‘𝐴)) + (Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) · (sin‘𝐴))))
672, 14, 61adddid 10320 . . . . . . 7 (𝜑 → ((1 / 2) · ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) = (((1 / 2) · (sin‘𝐴)) + ((1 / 2) · Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))))
6865, 66, 673eqtr4d 2809 . . . . . 6 (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) · (sin‘𝐴)) = ((1 / 2) · ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))))
6968oveq1d 6859 . . . . 5 (𝜑 → ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) · (sin‘𝐴)) / (sin‘𝐴)) = (((1 / 2) · ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) / (sin‘𝐴)))
7010sincld 15145 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝐴)) ∈ ℂ)
7142, 70, 56npncand 10672 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) = ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))
7271eqcomd 2771 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = (((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))))
7372sumeq2dv 14721 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = Σ𝑛 ∈ (1...𝑁)(((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))))
7442, 70subcld 10648 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) ∈ ℂ)
7570, 56subcld 10648 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) ∈ ℂ)
763, 74, 75fsumadd 14758 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (1...𝑁)(((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) = (Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + Σ𝑛 ∈ (1...𝑁)((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))))
77 fvoveq1 6867 . . . . . . . . . . . 12 (𝑗 = 𝑛 → (sin‘(𝑗 · 𝐴)) = (sin‘(𝑛 · 𝐴)))
78 fvoveq1 6867 . . . . . . . . . . . 12 (𝑗 = (𝑛 + 1) → (sin‘(𝑗 · 𝐴)) = (sin‘((𝑛 + 1) · 𝐴)))
79 fvoveq1 6867 . . . . . . . . . . . 12 (𝑗 = 1 → (sin‘(𝑗 · 𝐴)) = (sin‘(1 · 𝐴)))
80 fvoveq1 6867 . . . . . . . . . . . 12 (𝑗 = (𝑁 + 1) → (sin‘(𝑗 · 𝐴)) = (sin‘((𝑁 + 1) · 𝐴)))
81 dirkertrigeqlem2.n . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℕ)
8281nnzd 11731 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℤ)
83 nnuz 11926 . . . . . . . . . . . . . 14 ℕ = (ℤ‘1)
8481, 83syl6eleq 2854 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ (ℤ‘1))
85 peano2uz 11944 . . . . . . . . . . . . 13 (𝑁 ∈ (ℤ‘1) → (𝑁 + 1) ∈ (ℤ‘1))
8684, 85syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑁 + 1) ∈ (ℤ‘1))
87 elfzelz 12552 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℤ)
8887zcnd 11733 . . . . . . . . . . . . . . 15 (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℂ)
8988adantl 473 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...(𝑁 + 1))) → 𝑗 ∈ ℂ)
908adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...(𝑁 + 1))) → 𝐴 ∈ ℂ)
9189, 90mulcld 10316 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...(𝑁 + 1))) → (𝑗 · 𝐴) ∈ ℂ)
9291sincld 15145 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...(𝑁 + 1))) → (sin‘(𝑗 · 𝐴)) ∈ ℂ)
9377, 78, 79, 80, 82, 86, 92telfsum2 14824 . . . . . . . . . . 11 (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) = ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))))
94 1cnd 10290 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) → 1 ∈ ℂ)
955, 94pncand 10649 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (1...𝑁) → ((𝑛 + 1) − 1) = 𝑛)
9695eqcomd 2771 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (1...𝑁) → 𝑛 = ((𝑛 + 1) − 1))
9796adantl 473 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 = ((𝑛 + 1) − 1))
9897fvoveq1d 6866 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝐴)) = (sin‘(((𝑛 + 1) − 1) · 𝐴)))
9998oveq1d 6859 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = ((sin‘(((𝑛 + 1) − 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))
10099sumeq2dv 14721 . . . . . . . . . . . 12 (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = Σ𝑛 ∈ (1...𝑁)((sin‘(((𝑛 + 1) − 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))
101 oveq1 6851 . . . . . . . . . . . . . 14 (𝑗 = 𝑛 → (𝑗 − 1) = (𝑛 − 1))
102101fvoveq1d 6866 . . . . . . . . . . . . 13 (𝑗 = 𝑛 → (sin‘((𝑗 − 1) · 𝐴)) = (sin‘((𝑛 − 1) · 𝐴)))
103 oveq1 6851 . . . . . . . . . . . . . 14 (𝑗 = (𝑛 + 1) → (𝑗 − 1) = ((𝑛 + 1) − 1))
104103fvoveq1d 6866 . . . . . . . . . . . . 13 (𝑗 = (𝑛 + 1) → (sin‘((𝑗 − 1) · 𝐴)) = (sin‘(((𝑛 + 1) − 1) · 𝐴)))
105 oveq1 6851 . . . . . . . . . . . . . 14 (𝑗 = 1 → (𝑗 − 1) = (1 − 1))
106105fvoveq1d 6866 . . . . . . . . . . . . 13 (𝑗 = 1 → (sin‘((𝑗 − 1) · 𝐴)) = (sin‘((1 − 1) · 𝐴)))
107 oveq1 6851 . . . . . . . . . . . . . 14 (𝑗 = (𝑁 + 1) → (𝑗 − 1) = ((𝑁 + 1) − 1))
108107fvoveq1d 6866 . . . . . . . . . . . . 13 (𝑗 = (𝑁 + 1) → (sin‘((𝑗 − 1) · 𝐴)) = (sin‘(((𝑁 + 1) − 1) · 𝐴)))
109 1cnd 10290 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (1...(𝑁 + 1))) → 1 ∈ ℂ)
11089, 109subcld 10648 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (1...(𝑁 + 1))) → (𝑗 − 1) ∈ ℂ)
111110, 90mulcld 10316 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...(𝑁 + 1))) → ((𝑗 − 1) · 𝐴) ∈ ℂ)
112111sincld 15145 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...(𝑁 + 1))) → (sin‘((𝑗 − 1) · 𝐴)) ∈ ℂ)
113102, 104, 106, 108, 82, 86, 112telfsum2 14824 . . . . . . . . . . . 12 (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘(((𝑛 + 1) − 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = ((sin‘(((𝑁 + 1) − 1) · 𝐴)) − (sin‘((1 − 1) · 𝐴))))
11481nnred 11293 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℝ)
115114recnd 10324 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℂ)
116115, 1pncand 10649 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
117116fvoveq1d 6866 . . . . . . . . . . . . 13 (𝜑 → (sin‘(((𝑁 + 1) − 1) · 𝐴)) = (sin‘(𝑁 · 𝐴)))
1181subidd 10636 . . . . . . . . . . . . . . . . 17 (𝜑 → (1 − 1) = 0)
119118oveq1d 6859 . . . . . . . . . . . . . . . 16 (𝜑 → ((1 − 1) · 𝐴) = (0 · 𝐴))
1208mul02d 10490 . . . . . . . . . . . . . . . 16 (𝜑 → (0 · 𝐴) = 0)
121119, 120eqtrd 2799 . . . . . . . . . . . . . . 15 (𝜑 → ((1 − 1) · 𝐴) = 0)
122121fveq2d 6381 . . . . . . . . . . . . . 14 (𝜑 → (sin‘((1 − 1) · 𝐴)) = (sin‘0))
123 sin0 15164 . . . . . . . . . . . . . . 15 (sin‘0) = 0
124123a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (sin‘0) = 0)
125122, 124eqtrd 2799 . . . . . . . . . . . . 13 (𝜑 → (sin‘((1 − 1) · 𝐴)) = 0)
126117, 125oveq12d 6862 . . . . . . . . . . . 12 (𝜑 → ((sin‘(((𝑁 + 1) − 1) · 𝐴)) − (sin‘((1 − 1) · 𝐴))) = ((sin‘(𝑁 · 𝐴)) − 0))
127100, 113, 1263eqtrd 2803 . . . . . . . . . . 11 (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = ((sin‘(𝑁 · 𝐴)) − 0))
12893, 127oveq12d 6862 . . . . . . . . . 10 (𝜑 → (Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + Σ𝑛 ∈ (1...𝑁)((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) = (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)))
12973, 76, 1283eqtrd 2803 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)))
130129oveq2d 6860 . . . . . . . 8 (𝜑 → ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) = ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0))))
13127fveq2d 6381 . . . . . . . . . . . 12 (𝜑 → (sin‘(1 · 𝐴)) = (sin‘𝐴))
132131oveq2d 6860 . . . . . . . . . . 11 (𝜑 → ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) = ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)))
133132oveq1d 6859 . . . . . . . . . 10 (𝜑 → (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)) = (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)) + ((sin‘(𝑁 · 𝐴)) − 0)))
134133oveq2d 6860 . . . . . . . . 9 (𝜑 → ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0))) = ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)) + ((sin‘(𝑁 · 𝐴)) − 0))))
135115, 1addcld 10315 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 + 1) ∈ ℂ)
136135, 8mulcld 10316 . . . . . . . . . . . . 13 (𝜑 → ((𝑁 + 1) · 𝐴) ∈ ℂ)
137136sincld 15145 . . . . . . . . . . . 12 (𝜑 → (sin‘((𝑁 + 1) · 𝐴)) ∈ ℂ)
138137, 14subcld 10648 . . . . . . . . . . 11 (𝜑 → ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)) ∈ ℂ)
139115, 8mulcld 10316 . . . . . . . . . . . . 13 (𝜑 → (𝑁 · 𝐴) ∈ ℂ)
140139sincld 15145 . . . . . . . . . . . 12 (𝜑 → (sin‘(𝑁 · 𝐴)) ∈ ℂ)
141 0cnd 10288 . . . . . . . . . . . 12 (𝜑 → 0 ∈ ℂ)
142140, 141subcld 10648 . . . . . . . . . . 11 (𝜑 → ((sin‘(𝑁 · 𝐴)) − 0) ∈ ℂ)
14314, 138, 142addassd 10318 . . . . . . . . . 10 (𝜑 → (((sin‘𝐴) + ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)) = ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)) + ((sin‘(𝑁 · 𝐴)) − 0))))
144143eqcomd 2771 . . . . . . . . 9 (𝜑 → ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)) + ((sin‘(𝑁 · 𝐴)) − 0))) = (((sin‘𝐴) + ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)))
14514, 137pncan3d 10651 . . . . . . . . . . 11 (𝜑 → ((sin‘𝐴) + ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) = (sin‘((𝑁 + 1) · 𝐴)))
146140subid1d 10637 . . . . . . . . . . 11 (𝜑 → ((sin‘(𝑁 · 𝐴)) − 0) = (sin‘(𝑁 · 𝐴)))
147145, 146oveq12d 6862 . . . . . . . . . 10 (𝜑 → (((sin‘𝐴) + ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)) = ((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))))
148137, 140addcomd 10494 . . . . . . . . . 10 (𝜑 → ((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))) = ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))))
149147, 148eqtrd 2799 . . . . . . . . 9 (𝜑 → (((sin‘𝐴) + ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)) = ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))))
150134, 144, 1493eqtrd 2803 . . . . . . . 8 (𝜑 → ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0))) = ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))))
151130, 150eqtrd 2799 . . . . . . 7 (𝜑 → ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) = ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))))
152151oveq2d 6860 . . . . . 6 (𝜑 → ((1 / 2) · ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) = ((1 / 2) · ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))))
153152oveq1d 6859 . . . . 5 (𝜑 → (((1 / 2) · ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) / (sin‘𝐴)) = (((1 / 2) · ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) / (sin‘𝐴)))
15417, 69, 1533eqtrd 2803 . . . 4 (𝜑 → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) = (((1 / 2) · ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) / (sin‘𝐴)))
155 halfre 11494 . . . . . . . . . . . 12 (1 / 2) ∈ ℝ
156155a1i 11 . . . . . . . . . . 11 (𝜑 → (1 / 2) ∈ ℝ)
157114, 156readdcld 10325 . . . . . . . . . 10 (𝜑 → (𝑁 + (1 / 2)) ∈ ℝ)
158157, 7remulcld 10326 . . . . . . . . 9 (𝜑 → ((𝑁 + (1 / 2)) · 𝐴) ∈ ℝ)
159158recnd 10324 . . . . . . . 8 (𝜑 → ((𝑁 + (1 / 2)) · 𝐴) ∈ ℂ)
1602, 8mulcld 10316 . . . . . . . 8 (𝜑 → ((1 / 2) · 𝐴) ∈ ℂ)
161 sinmulcos 40717 . . . . . . . 8 ((((𝑁 + (1 / 2)) · 𝐴) ∈ ℂ ∧ ((1 / 2) · 𝐴) ∈ ℂ) → ((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))) = (((sin‘(((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴))) + (sin‘(((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴)))) / 2))
162159, 160, 161syl2anc 579 . . . . . . 7 (𝜑 → ((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))) = (((sin‘(((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴))) + (sin‘(((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴)))) / 2))
163115, 2, 8adddird 10321 . . . . . . . . . . . 12 (𝜑 → ((𝑁 + (1 / 2)) · 𝐴) = ((𝑁 · 𝐴) + ((1 / 2) · 𝐴)))
164163oveq1d 6859 . . . . . . . . . . 11 (𝜑 → (((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴)) = (((𝑁 · 𝐴) + ((1 / 2) · 𝐴)) + ((1 / 2) · 𝐴)))
165139, 160, 160addassd 10318 . . . . . . . . . . 11 (𝜑 → (((𝑁 · 𝐴) + ((1 / 2) · 𝐴)) + ((1 / 2) · 𝐴)) = ((𝑁 · 𝐴) + (((1 / 2) · 𝐴) + ((1 / 2) · 𝐴))))
1662, 2, 8adddird 10321 . . . . . . . . . . . . . 14 (𝜑 → (((1 / 2) + (1 / 2)) · 𝐴) = (((1 / 2) · 𝐴) + ((1 / 2) · 𝐴)))
16712halvesd 11526 . . . . . . . . . . . . . . 15 (𝜑 → ((1 / 2) + (1 / 2)) = 1)
168167oveq1d 6859 . . . . . . . . . . . . . 14 (𝜑 → (((1 / 2) + (1 / 2)) · 𝐴) = (1 · 𝐴))
169166, 168eqtr3d 2801 . . . . . . . . . . . . 13 (𝜑 → (((1 / 2) · 𝐴) + ((1 / 2) · 𝐴)) = (1 · 𝐴))
170169oveq2d 6860 . . . . . . . . . . . 12 (𝜑 → ((𝑁 · 𝐴) + (((1 / 2) · 𝐴) + ((1 / 2) · 𝐴))) = ((𝑁 · 𝐴) + (1 · 𝐴)))
171115, 1, 8adddird 10321 . . . . . . . . . . . 12 (𝜑 → ((𝑁 + 1) · 𝐴) = ((𝑁 · 𝐴) + (1 · 𝐴)))
172170, 171eqtr4d 2802 . . . . . . . . . . 11 (𝜑 → ((𝑁 · 𝐴) + (((1 / 2) · 𝐴) + ((1 / 2) · 𝐴))) = ((𝑁 + 1) · 𝐴))
173164, 165, 1723eqtrrd 2804 . . . . . . . . . 10 (𝜑 → ((𝑁 + 1) · 𝐴) = (((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴)))
174173fveq2d 6381 . . . . . . . . 9 (𝜑 → (sin‘((𝑁 + 1) · 𝐴)) = (sin‘(((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴))))
175163oveq1d 6859 . . . . . . . . . . 11 (𝜑 → (((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴)) = (((𝑁 · 𝐴) + ((1 / 2) · 𝐴)) − ((1 / 2) · 𝐴)))
176139, 160pncand 10649 . . . . . . . . . . 11 (𝜑 → (((𝑁 · 𝐴) + ((1 / 2) · 𝐴)) − ((1 / 2) · 𝐴)) = (𝑁 · 𝐴))
177175, 176eqtr2d 2800 . . . . . . . . . 10 (𝜑 → (𝑁 · 𝐴) = (((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴)))
178177fveq2d 6381 . . . . . . . . 9 (𝜑 → (sin‘(𝑁 · 𝐴)) = (sin‘(((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴))))
179174, 178oveq12d 6862 . . . . . . . 8 (𝜑 → ((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))) = ((sin‘(((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴))) + (sin‘(((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴)))))
180179oveq1d 6859 . . . . . . 7 (𝜑 → (((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))) / 2) = (((sin‘(((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴))) + (sin‘(((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴)))) / 2))
181162, 180eqtr4d 2802 . . . . . 6 (𝜑 → ((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))) = (((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))) / 2))
182148oveq1d 6859 . . . . . 6 (𝜑 → (((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))) / 2) = (((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))) / 2))
183140, 137addcld 10315 . . . . . . 7 (𝜑 → ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))) ∈ ℂ)
184183, 52, 59divrec2d 11061 . . . . . 6 (𝜑 → (((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))) / 2) = ((1 / 2) · ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))))
185181, 182, 1843eqtrrd 2804 . . . . 5 (𝜑 → ((1 / 2) · ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))))
186185oveq1d 6859 . . . 4 (𝜑 → (((1 / 2) · ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) / (sin‘𝐴)) = (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))) / (sin‘𝐴)))
1878, 52, 59divcan2d 11059 . . . . . . . . 9 (𝜑 → (2 · (𝐴 / 2)) = 𝐴)
188187eqcomd 2771 . . . . . . . 8 (𝜑𝐴 = (2 · (𝐴 / 2)))
189188fveq2d 6381 . . . . . . 7 (𝜑 → (sin‘𝐴) = (sin‘(2 · (𝐴 / 2))))
1908halfcld 11525 . . . . . . . 8 (𝜑 → (𝐴 / 2) ∈ ℂ)
191 sin2t 15192 . . . . . . . 8 ((𝐴 / 2) ∈ ℂ → (sin‘(2 · (𝐴 / 2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))))
192190, 191syl 17 . . . . . . 7 (𝜑 → (sin‘(2 · (𝐴 / 2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))))
193189, 192eqtrd 2799 . . . . . 6 (𝜑 → (sin‘𝐴) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))))
194193oveq2d 6860 . . . . 5 (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))) / (sin‘𝐴)) = (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))) / (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))))))
195190sincld 15145 . . . . . . . 8 (𝜑 → (sin‘(𝐴 / 2)) ∈ ℂ)
196190coscld 15146 . . . . . . . 8 (𝜑 → (cos‘(𝐴 / 2)) ∈ ℂ)
19752, 195, 196mulassd 10319 . . . . . . 7 (𝜑 → ((2 · (sin‘(𝐴 / 2))) · (cos‘(𝐴 / 2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))))
1988, 52, 59divrec2d 11061 . . . . . . . . 9 (𝜑 → (𝐴 / 2) = ((1 / 2) · 𝐴))
199198fveq2d 6381 . . . . . . . 8 (𝜑 → (cos‘(𝐴 / 2)) = (cos‘((1 / 2) · 𝐴)))
200199oveq2d 6860 . . . . . . 7 (𝜑 → ((2 · (sin‘(𝐴 / 2))) · (cos‘(𝐴 / 2))) = ((2 · (sin‘(𝐴 / 2))) · (cos‘((1 / 2) · 𝐴))))
201197, 200eqtr3d 2801 . . . . . 6 (𝜑 → (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))) = ((2 · (sin‘(𝐴 / 2))) · (cos‘((1 / 2) · 𝐴))))
202201oveq2d 6860 . . . . 5 (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))) / (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))))) = (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))) / ((2 · (sin‘(𝐴 / 2))) · (cos‘((1 / 2) · 𝐴)))))
203159sincld 15145 . . . . . 6 (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝐴)) ∈ ℂ)
20452, 195mulcld 10316 . . . . . 6 (𝜑 → (2 · (sin‘(𝐴 / 2))) ∈ ℂ)
205160coscld 15146 . . . . . 6 (𝜑 → (cos‘((1 / 2) · 𝐴)) ∈ ℂ)
206195, 196mulcld 10316 . . . . . . . . 9 (𝜑 → ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))) ∈ ℂ)
207193, 15eqnetrrd 3005 . . . . . . . . 9 (𝜑 → (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))) ≠ 0)
20852, 206, 207mulne0bbd 10939 . . . . . . . 8 (𝜑 → ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))) ≠ 0)
209195, 196, 208mulne0bad 10938 . . . . . . 7 (𝜑 → (sin‘(𝐴 / 2)) ≠ 0)
21052, 195, 59, 209mulne0d 10935 . . . . . 6 (𝜑 → (2 · (sin‘(𝐴 / 2))) ≠ 0)
211195, 196, 208mulne0bbd 10939 . . . . . . 7 (𝜑 → (cos‘(𝐴 / 2)) ≠ 0)
212199, 211eqnetrrd 3005 . . . . . 6 (𝜑 → (cos‘((1 / 2) · 𝐴)) ≠ 0)
213203, 204, 205, 210, 212divcan5rd 11084 . . . . 5 (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))) / ((2 · (sin‘(𝐴 / 2))) · (cos‘((1 / 2) · 𝐴)))) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (2 · (sin‘(𝐴 / 2)))))
214194, 202, 2133eqtrd 2803 . . . 4 (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))) / (sin‘𝐴)) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (2 · (sin‘(𝐴 / 2)))))
215154, 186, 2143eqtrd 2803 . . 3 (𝜑 → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (2 · (sin‘(𝐴 / 2)))))
216215oveq1d 6859 . 2 (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = (((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (2 · (sin‘(𝐴 / 2)))) / π))
217 picn 24506 . . . 4 π ∈ ℂ
218217a1i 11 . . 3 (𝜑 → π ∈ ℂ)
219 pire 24505 . . . . 5 π ∈ ℝ
220 pipos 24507 . . . . 5 0 < π
221219, 220gt0ne0ii 10820 . . . 4 π ≠ 0
222221a1i 11 . . 3 (𝜑 → π ≠ 0)
223203, 204, 218, 210, 222divdiv32d 11082 . 2 (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (2 · (sin‘(𝐴 / 2)))) / π) = (((sin‘((𝑁 + (1 / 2)) · 𝐴)) / π) / (2 · (sin‘(𝐴 / 2)))))
224203, 218, 204, 222, 210divdiv1d 11088 . . 3 (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) / π) / (2 · (sin‘(𝐴 / 2)))) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (π · (2 · (sin‘(𝐴 / 2))))))
225218, 52, 195mulassd 10319 . . . . 5 (𝜑 → ((π · 2) · (sin‘(𝐴 / 2))) = (π · (2 · (sin‘(𝐴 / 2)))))
226218, 52mulcomd 10317 . . . . . 6 (𝜑 → (π · 2) = (2 · π))
227226oveq1d 6859 . . . . 5 (𝜑 → ((π · 2) · (sin‘(𝐴 / 2))) = ((2 · π) · (sin‘(𝐴 / 2))))
228225, 227eqtr3d 2801 . . . 4 (𝜑 → (π · (2 · (sin‘(𝐴 / 2)))) = ((2 · π) · (sin‘(𝐴 / 2))))
229228oveq2d 6860 . . 3 (𝜑 → ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (π · (2 · (sin‘(𝐴 / 2))))) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) · (sin‘(𝐴 / 2)))))
230224, 229eqtrd 2799 . 2 (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) / π) / (2 · (sin‘(𝐴 / 2)))) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) · (sin‘(𝐴 / 2)))))
231216, 223, 2303eqtrd 2803 1 (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) · (sin‘(𝐴 / 2)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1652  wcel 2155  wne 2937  cfv 6070  (class class class)co 6844  cc 10189  cr 10190  0cc0 10191  1c1 10192   + caddc 10194   · cmul 10196  cmin 10522  -cneg 10523   / cdiv 10940  cn 11276  2c2 11329  cuz 11889  ...cfz 12536  Σcsu 14704  sincsin 15079  cosccos 15080  πcpi 15082
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7149  ax-inf2 8755  ax-cnex 10247  ax-resscn 10248  ax-1cn 10249  ax-icn 10250  ax-addcl 10251  ax-addrcl 10252  ax-mulcl 10253  ax-mulrcl 10254  ax-mulcom 10255  ax-addass 10256  ax-mulass 10257  ax-distr 10258  ax-i2m1 10259  ax-1ne0 10260  ax-1rid 10261  ax-rnegex 10262  ax-rrecex 10263  ax-cnre 10264  ax-pre-lttri 10265  ax-pre-lttrn 10266  ax-pre-ltadd 10267  ax-pre-mulgt0 10268  ax-pre-sup 10269  ax-addf 10270  ax-mulf 10271
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-iin 4681  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-se 5239  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-isom 6079  df-riota 6805  df-ov 6847  df-oprab 6848  df-mpt2 6849  df-of 7097  df-om 7266  df-1st 7368  df-2nd 7369  df-supp 7500  df-wrecs 7612  df-recs 7674  df-rdg 7712  df-1o 7766  df-2o 7767  df-oadd 7770  df-er 7949  df-map 8064  df-pm 8065  df-ixp 8116  df-en 8163  df-dom 8164  df-sdom 8165  df-fin 8166  df-fsupp 8485  df-fi 8526  df-sup 8557  df-inf 8558  df-oi 8624  df-card 9018  df-cda 9245  df-pnf 10332  df-mnf 10333  df-xr 10334  df-ltxr 10335  df-le 10336  df-sub 10524  df-neg 10525  df-div 10941  df-nn 11277  df-2 11337  df-3 11338  df-4 11339  df-5 11340  df-6 11341  df-7 11342  df-8 11343  df-9 11344  df-n0 11541  df-z 11627  df-dec 11744  df-uz 11890  df-q 11993  df-rp 12032  df-xneg 12149  df-xadd 12150  df-xmul 12151  df-ioo 12384  df-ioc 12385  df-ico 12386  df-icc 12387  df-fz 12537  df-fzo 12677  df-fl 12804  df-seq 13012  df-exp 13071  df-fac 13268  df-bc 13297  df-hash 13325  df-shft 14095  df-cj 14127  df-re 14128  df-im 14129  df-sqrt 14263  df-abs 14264  df-limsup 14490  df-clim 14507  df-rlim 14508  df-sum 14705  df-ef 15083  df-sin 15085  df-cos 15086  df-pi 15088  df-struct 16135  df-ndx 16136  df-slot 16137  df-base 16139  df-sets 16140  df-ress 16141  df-plusg 16230  df-mulr 16231  df-starv 16232  df-sca 16233  df-vsca 16234  df-ip 16235  df-tset 16236  df-ple 16237  df-ds 16239  df-unif 16240  df-hom 16241  df-cco 16242  df-rest 16352  df-topn 16353  df-0g 16371  df-gsum 16372  df-topgen 16373  df-pt 16374  df-prds 16377  df-xrs 16431  df-qtop 16436  df-imas 16437  df-xps 16439  df-mre 16515  df-mrc 16516  df-acs 16518  df-mgm 17511  df-sgrp 17553  df-mnd 17564  df-submnd 17605  df-mulg 17811  df-cntz 18016  df-cmn 18464  df-psmet 20014  df-xmet 20015  df-met 20016  df-bl 20017  df-mopn 20018  df-fbas 20019  df-fg 20020  df-cnfld 20023  df-top 20981  df-topon 20998  df-topsp 21020  df-bases 21033  df-cld 21106  df-ntr 21107  df-cls 21108  df-nei 21185  df-lp 21223  df-perf 21224  df-cn 21314  df-cnp 21315  df-haus 21402  df-tx 21648  df-hmeo 21841  df-fil 21932  df-fm 22024  df-flim 22025  df-flf 22026  df-xms 22407  df-ms 22408  df-tms 22409  df-cncf 22963  df-limc 23924  df-dv 23925
This theorem is referenced by:  dirkertrigeq  40958
  Copyright terms: Public domain W3C validator