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 46054
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 11253 . . . . . . . . 9 (𝜑 → 1 ∈ ℂ)
21halfcld 12508 . . . . . . . 8 (𝜑 → (1 / 2) ∈ ℂ)
3 fzfid 14010 . . . . . . . . 9 (𝜑 → (1...𝑁) ∈ Fin)
4 elfzelz 13560 . . . . . . . . . . . . 13 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℤ)
54zcnd 12720 . . . . . . . . . . . 12 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
65adantl 481 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℂ)
7 dirkertrigeqlem2.a . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℝ)
87recnd 11286 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℂ)
98adantr 480 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → 𝐴 ∈ ℂ)
106, 9mulcld 11278 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑛 · 𝐴) ∈ ℂ)
1110coscld 16163 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝐴)) ∈ ℂ)
123, 11fsumcl 15765 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) ∈ ℂ)
132, 12addcld 11277 . . . . . . 7 (𝜑 → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) ∈ ℂ)
148sincld 16162 . . . . . . 7 (𝜑 → (sin‘𝐴) ∈ ℂ)
15 dirkertrigeqlem2.sinne0 . . . . . . 7 (𝜑 → (sin‘𝐴) ≠ 0)
1613, 14, 15divcan4d 12046 . . . . . 6 (𝜑 → ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) · (sin‘𝐴)) / (sin‘𝐴)) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))))
1716eqcomd 2740 . . . . 5 (𝜑 → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) = ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) · (sin‘𝐴)) / (sin‘𝐴)))
183, 14, 11fsummulc1 15817 . . . . . . . . 9 (𝜑 → (Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) · (sin‘𝐴)) = Σ𝑛 ∈ (1...𝑁)((cos‘(𝑛 · 𝐴)) · (sin‘𝐴)))
1914adantr 480 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘𝐴) ∈ ℂ)
2011, 19mulcomd 11279 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝐴)) · (sin‘𝐴)) = ((sin‘𝐴) · (cos‘(𝑛 · 𝐴))))
21 sinmulcos 45820 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ (𝑛 · 𝐴) ∈ ℂ) → ((sin‘𝐴) · (cos‘(𝑛 · 𝐴))) = (((sin‘(𝐴 + (𝑛 · 𝐴))) + (sin‘(𝐴 − (𝑛 · 𝐴)))) / 2))
229, 10, 21syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘𝐴) · (cos‘(𝑛 · 𝐴))) = (((sin‘(𝐴 + (𝑛 · 𝐴))) + (sin‘(𝐴 − (𝑛 · 𝐴)))) / 2))
23 1cnd 11253 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (1...𝑁)) → 1 ∈ ℂ)
246, 23, 9adddird 11283 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑛 + 1) · 𝐴) = ((𝑛 · 𝐴) + (1 · 𝐴)))
2523, 9mulcld 11278 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (1...𝑁)) → (1 · 𝐴) ∈ ℂ)
2610, 25addcomd 11460 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑛 · 𝐴) + (1 · 𝐴)) = ((1 · 𝐴) + (𝑛 · 𝐴)))
278mullidd 11276 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1 · 𝐴) = 𝐴)
2827oveq1d 7445 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1 · 𝐴) + (𝑛 · 𝐴)) = (𝐴 + (𝑛 · 𝐴)))
2928adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...𝑁)) → ((1 · 𝐴) + (𝑛 · 𝐴)) = (𝐴 + (𝑛 · 𝐴)))
3024, 26, 293eqtrrd 2779 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...𝑁)) → (𝐴 + (𝑛 · 𝐴)) = ((𝑛 + 1) · 𝐴))
3130fveq2d 6910 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝐴 + (𝑛 · 𝐴))) = (sin‘((𝑛 + 1) · 𝐴)))
3210, 9negsubdi2d 11633 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (1...𝑁)) → -((𝑛 · 𝐴) − 𝐴) = (𝐴 − (𝑛 · 𝐴)))
3332eqcomd 2740 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...𝑁)) → (𝐴 − (𝑛 · 𝐴)) = -((𝑛 · 𝐴) − 𝐴))
3433fveq2d 6910 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝐴 − (𝑛 · 𝐴))) = (sin‘-((𝑛 · 𝐴) − 𝐴)))
3510, 9subcld 11617 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑛 · 𝐴) − 𝐴) ∈ ℂ)
36 sinneg 16178 . . . . . . . . . . . . . . . 16 (((𝑛 · 𝐴) − 𝐴) ∈ ℂ → (sin‘-((𝑛 · 𝐴) − 𝐴)) = -(sin‘((𝑛 · 𝐴) − 𝐴)))
3735, 36syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘-((𝑛 · 𝐴) − 𝐴)) = -(sin‘((𝑛 · 𝐴) − 𝐴)))
3834, 37eqtrd 2774 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝐴 − (𝑛 · 𝐴))) = -(sin‘((𝑛 · 𝐴) − 𝐴)))
3931, 38oveq12d 7448 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘(𝐴 + (𝑛 · 𝐴))) + (sin‘(𝐴 − (𝑛 · 𝐴)))) = ((sin‘((𝑛 + 1) · 𝐴)) + -(sin‘((𝑛 · 𝐴) − 𝐴))))
409, 10addcld 11277 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...𝑁)) → (𝐴 + (𝑛 · 𝐴)) ∈ ℂ)
4140sincld 16162 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝐴 + (𝑛 · 𝐴))) ∈ ℂ)
4231, 41eqeltrrd 2839 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘((𝑛 + 1) · 𝐴)) ∈ ℂ)
4335sincld 16162 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘((𝑛 · 𝐴) − 𝐴)) ∈ ℂ)
4442, 43negsubd 11623 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘((𝑛 + 1) · 𝐴)) + -(sin‘((𝑛 · 𝐴) − 𝐴))) = ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 · 𝐴) − 𝐴))))
456, 9mulsubfacd 11721 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑛 · 𝐴) − 𝐴) = ((𝑛 − 1) · 𝐴))
4645fveq2d 6910 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘((𝑛 · 𝐴) − 𝐴)) = (sin‘((𝑛 − 1) · 𝐴)))
4746oveq2d 7446 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 · 𝐴) − 𝐴))) = ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))
4839, 44, 473eqtrd 2778 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘(𝐴 + (𝑛 · 𝐴))) + (sin‘(𝐴 − (𝑛 · 𝐴)))) = ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))
4948oveq1d 7445 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → (((sin‘(𝐴 + (𝑛 · 𝐴))) + (sin‘(𝐴 − (𝑛 · 𝐴)))) / 2) = (((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2))
5020, 22, 493eqtrd 2778 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝐴)) · (sin‘𝐴)) = (((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2))
5150sumeq2dv 15734 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (1...𝑁)((cos‘(𝑛 · 𝐴)) · (sin‘𝐴)) = Σ𝑛 ∈ (1...𝑁)(((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2))
52 2cnd 12341 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℂ)
53 peano2cnm 11572 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℂ → (𝑛 − 1) ∈ ℂ)
546, 53syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑛 − 1) ∈ ℂ)
5554, 9mulcld 11278 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑛 − 1) · 𝐴) ∈ ℂ)
5655sincld 16162 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘((𝑛 − 1) · 𝐴)) ∈ ℂ)
5742, 56subcld 11617 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) ∈ ℂ)
58 2ne0 12367 . . . . . . . . . . . 12 2 ≠ 0
5958a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ≠ 0)
603, 52, 57, 59fsumdivc 15818 . . . . . . . . . 10 (𝜑 → (Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2) = Σ𝑛 ∈ (1...𝑁)(((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2))
613, 57fsumcl 15765 . . . . . . . . . . 11 (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) ∈ ℂ)
6261, 52, 59divrec2d 12044 . . . . . . . . . 10 (𝜑 → (Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2) = ((1 / 2) · Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))))
6360, 62eqtr3d 2776 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (1...𝑁)(((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2) = ((1 / 2) · Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))))
6418, 51, 633eqtrd 2778 . . . . . . . 8 (𝜑 → (Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) · (sin‘𝐴)) = ((1 / 2) · Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))))
6564oveq2d 7446 . . . . . . 7 (𝜑 → (((1 / 2) · (sin‘𝐴)) + (Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) · (sin‘𝐴))) = (((1 / 2) · (sin‘𝐴)) + ((1 / 2) · Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))))
662, 12, 14adddird 11283 . . . . . . 7 (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) · (sin‘𝐴)) = (((1 / 2) · (sin‘𝐴)) + (Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) · (sin‘𝐴))))
672, 14, 61adddid 11282 . . . . . . 7 (𝜑 → ((1 / 2) · ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) = (((1 / 2) · (sin‘𝐴)) + ((1 / 2) · Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))))
6865, 66, 673eqtr4d 2784 . . . . . 6 (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) · (sin‘𝐴)) = ((1 / 2) · ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))))
6968oveq1d 7445 . . . . 5 (𝜑 → ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) · (sin‘𝐴)) / (sin‘𝐴)) = (((1 / 2) · ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) / (sin‘𝐴)))
7010sincld 16162 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝐴)) ∈ ℂ)
7142, 70, 56npncand 11641 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) = ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))
7271eqcomd 2740 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = (((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))))
7372sumeq2dv 15734 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = Σ𝑛 ∈ (1...𝑁)(((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))))
7442, 70subcld 11617 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) ∈ ℂ)
7570, 56subcld 11617 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) ∈ ℂ)
763, 74, 75fsumadd 15772 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (1...𝑁)(((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) = (Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + Σ𝑛 ∈ (1...𝑁)((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))))
77 fvoveq1 7453 . . . . . . . . . . . 12 (𝑗 = 𝑛 → (sin‘(𝑗 · 𝐴)) = (sin‘(𝑛 · 𝐴)))
78 fvoveq1 7453 . . . . . . . . . . . 12 (𝑗 = (𝑛 + 1) → (sin‘(𝑗 · 𝐴)) = (sin‘((𝑛 + 1) · 𝐴)))
79 fvoveq1 7453 . . . . . . . . . . . 12 (𝑗 = 1 → (sin‘(𝑗 · 𝐴)) = (sin‘(1 · 𝐴)))
80 fvoveq1 7453 . . . . . . . . . . . 12 (𝑗 = (𝑁 + 1) → (sin‘(𝑗 · 𝐴)) = (sin‘((𝑁 + 1) · 𝐴)))
81 dirkertrigeqlem2.n . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℕ)
8281nnzd 12637 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℤ)
83 nnuz 12918 . . . . . . . . . . . . . 14 ℕ = (ℤ‘1)
8481, 83eleqtrdi 2848 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ (ℤ‘1))
85 peano2uz 12940 . . . . . . . . . . . . 13 (𝑁 ∈ (ℤ‘1) → (𝑁 + 1) ∈ (ℤ‘1))
8684, 85syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑁 + 1) ∈ (ℤ‘1))
87 elfzelz 13560 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℤ)
8887zcnd 12720 . . . . . . . . . . . . . . 15 (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℂ)
8988adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...(𝑁 + 1))) → 𝑗 ∈ ℂ)
908adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...(𝑁 + 1))) → 𝐴 ∈ ℂ)
9189, 90mulcld 11278 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...(𝑁 + 1))) → (𝑗 · 𝐴) ∈ ℂ)
9291sincld 16162 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...(𝑁 + 1))) → (sin‘(𝑗 · 𝐴)) ∈ ℂ)
9377, 78, 79, 80, 82, 86, 92telfsum2 15837 . . . . . . . . . . 11 (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) = ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))))
94 1cnd 11253 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) → 1 ∈ ℂ)
955, 94pncand 11618 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (1...𝑁) → ((𝑛 + 1) − 1) = 𝑛)
9695eqcomd 2740 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (1...𝑁) → 𝑛 = ((𝑛 + 1) − 1))
9796adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 = ((𝑛 + 1) − 1))
9897fvoveq1d 7452 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝐴)) = (sin‘(((𝑛 + 1) − 1) · 𝐴)))
9998oveq1d 7445 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = ((sin‘(((𝑛 + 1) − 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))
10099sumeq2dv 15734 . . . . . . . . . . . 12 (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = Σ𝑛 ∈ (1...𝑁)((sin‘(((𝑛 + 1) − 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))
101 oveq1 7437 . . . . . . . . . . . . . 14 (𝑗 = 𝑛 → (𝑗 − 1) = (𝑛 − 1))
102101fvoveq1d 7452 . . . . . . . . . . . . 13 (𝑗 = 𝑛 → (sin‘((𝑗 − 1) · 𝐴)) = (sin‘((𝑛 − 1) · 𝐴)))
103 oveq1 7437 . . . . . . . . . . . . . 14 (𝑗 = (𝑛 + 1) → (𝑗 − 1) = ((𝑛 + 1) − 1))
104103fvoveq1d 7452 . . . . . . . . . . . . 13 (𝑗 = (𝑛 + 1) → (sin‘((𝑗 − 1) · 𝐴)) = (sin‘(((𝑛 + 1) − 1) · 𝐴)))
105 oveq1 7437 . . . . . . . . . . . . . 14 (𝑗 = 1 → (𝑗 − 1) = (1 − 1))
106105fvoveq1d 7452 . . . . . . . . . . . . 13 (𝑗 = 1 → (sin‘((𝑗 − 1) · 𝐴)) = (sin‘((1 − 1) · 𝐴)))
107 oveq1 7437 . . . . . . . . . . . . . 14 (𝑗 = (𝑁 + 1) → (𝑗 − 1) = ((𝑁 + 1) − 1))
108107fvoveq1d 7452 . . . . . . . . . . . . 13 (𝑗 = (𝑁 + 1) → (sin‘((𝑗 − 1) · 𝐴)) = (sin‘(((𝑁 + 1) − 1) · 𝐴)))
109 1cnd 11253 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (1...(𝑁 + 1))) → 1 ∈ ℂ)
11089, 109subcld 11617 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (1...(𝑁 + 1))) → (𝑗 − 1) ∈ ℂ)
111110, 90mulcld 11278 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...(𝑁 + 1))) → ((𝑗 − 1) · 𝐴) ∈ ℂ)
112111sincld 16162 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...(𝑁 + 1))) → (sin‘((𝑗 − 1) · 𝐴)) ∈ ℂ)
113102, 104, 106, 108, 82, 86, 112telfsum2 15837 . . . . . . . . . . . 12 (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘(((𝑛 + 1) − 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = ((sin‘(((𝑁 + 1) − 1) · 𝐴)) − (sin‘((1 − 1) · 𝐴))))
11481nnred 12278 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℝ)
115114recnd 11286 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℂ)
116115, 1pncand 11618 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
117116fvoveq1d 7452 . . . . . . . . . . . . 13 (𝜑 → (sin‘(((𝑁 + 1) − 1) · 𝐴)) = (sin‘(𝑁 · 𝐴)))
1181subidd 11605 . . . . . . . . . . . . . . . . 17 (𝜑 → (1 − 1) = 0)
119118oveq1d 7445 . . . . . . . . . . . . . . . 16 (𝜑 → ((1 − 1) · 𝐴) = (0 · 𝐴))
1208mul02d 11456 . . . . . . . . . . . . . . . 16 (𝜑 → (0 · 𝐴) = 0)
121119, 120eqtrd 2774 . . . . . . . . . . . . . . 15 (𝜑 → ((1 − 1) · 𝐴) = 0)
122121fveq2d 6910 . . . . . . . . . . . . . 14 (𝜑 → (sin‘((1 − 1) · 𝐴)) = (sin‘0))
123 sin0 16181 . . . . . . . . . . . . . . 15 (sin‘0) = 0
124123a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (sin‘0) = 0)
125122, 124eqtrd 2774 . . . . . . . . . . . . 13 (𝜑 → (sin‘((1 − 1) · 𝐴)) = 0)
126117, 125oveq12d 7448 . . . . . . . . . . . 12 (𝜑 → ((sin‘(((𝑁 + 1) − 1) · 𝐴)) − (sin‘((1 − 1) · 𝐴))) = ((sin‘(𝑁 · 𝐴)) − 0))
127100, 113, 1263eqtrd 2778 . . . . . . . . . . 11 (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = ((sin‘(𝑁 · 𝐴)) − 0))
12893, 127oveq12d 7448 . . . . . . . . . 10 (𝜑 → (Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + Σ𝑛 ∈ (1...𝑁)((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) = (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)))
12973, 76, 1283eqtrd 2778 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)))
130129oveq2d 7446 . . . . . . . 8 (𝜑 → ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) = ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0))))
13127fveq2d 6910 . . . . . . . . . . . 12 (𝜑 → (sin‘(1 · 𝐴)) = (sin‘𝐴))
132131oveq2d 7446 . . . . . . . . . . 11 (𝜑 → ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) = ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)))
133132oveq1d 7445 . . . . . . . . . 10 (𝜑 → (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)) = (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)) + ((sin‘(𝑁 · 𝐴)) − 0)))
134133oveq2d 7446 . . . . . . . . 9 (𝜑 → ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0))) = ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)) + ((sin‘(𝑁 · 𝐴)) − 0))))
135115, 1addcld 11277 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 + 1) ∈ ℂ)
136135, 8mulcld 11278 . . . . . . . . . . . . 13 (𝜑 → ((𝑁 + 1) · 𝐴) ∈ ℂ)
137136sincld 16162 . . . . . . . . . . . 12 (𝜑 → (sin‘((𝑁 + 1) · 𝐴)) ∈ ℂ)
138137, 14subcld 11617 . . . . . . . . . . 11 (𝜑 → ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)) ∈ ℂ)
139115, 8mulcld 11278 . . . . . . . . . . . . 13 (𝜑 → (𝑁 · 𝐴) ∈ ℂ)
140139sincld 16162 . . . . . . . . . . . 12 (𝜑 → (sin‘(𝑁 · 𝐴)) ∈ ℂ)
141 0cnd 11251 . . . . . . . . . . . 12 (𝜑 → 0 ∈ ℂ)
142140, 141subcld 11617 . . . . . . . . . . 11 (𝜑 → ((sin‘(𝑁 · 𝐴)) − 0) ∈ ℂ)
14314, 138, 142addassd 11280 . . . . . . . . . 10 (𝜑 → (((sin‘𝐴) + ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)) = ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)) + ((sin‘(𝑁 · 𝐴)) − 0))))
144143eqcomd 2740 . . . . . . . . 9 (𝜑 → ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)) + ((sin‘(𝑁 · 𝐴)) − 0))) = (((sin‘𝐴) + ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)))
14514, 137pncan3d 11620 . . . . . . . . . . 11 (𝜑 → ((sin‘𝐴) + ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) = (sin‘((𝑁 + 1) · 𝐴)))
146140subid1d 11606 . . . . . . . . . . 11 (𝜑 → ((sin‘(𝑁 · 𝐴)) − 0) = (sin‘(𝑁 · 𝐴)))
147145, 146oveq12d 7448 . . . . . . . . . 10 (𝜑 → (((sin‘𝐴) + ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)) = ((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))))
148137, 140addcomd 11460 . . . . . . . . . 10 (𝜑 → ((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))) = ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))))
149147, 148eqtrd 2774 . . . . . . . . 9 (𝜑 → (((sin‘𝐴) + ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)) = ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))))
150134, 144, 1493eqtrd 2778 . . . . . . . 8 (𝜑 → ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0))) = ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))))
151130, 150eqtrd 2774 . . . . . . 7 (𝜑 → ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) = ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))))
152151oveq2d 7446 . . . . . 6 (𝜑 → ((1 / 2) · ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) = ((1 / 2) · ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))))
153152oveq1d 7445 . . . . 5 (𝜑 → (((1 / 2) · ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) / (sin‘𝐴)) = (((1 / 2) · ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) / (sin‘𝐴)))
15417, 69, 1533eqtrd 2778 . . . 4 (𝜑 → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) = (((1 / 2) · ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) / (sin‘𝐴)))
155 halfre 12477 . . . . . . . . . . . 12 (1 / 2) ∈ ℝ
156155a1i 11 . . . . . . . . . . 11 (𝜑 → (1 / 2) ∈ ℝ)
157114, 156readdcld 11287 . . . . . . . . . 10 (𝜑 → (𝑁 + (1 / 2)) ∈ ℝ)
158157, 7remulcld 11288 . . . . . . . . 9 (𝜑 → ((𝑁 + (1 / 2)) · 𝐴) ∈ ℝ)
159158recnd 11286 . . . . . . . 8 (𝜑 → ((𝑁 + (1 / 2)) · 𝐴) ∈ ℂ)
1602, 8mulcld 11278 . . . . . . . 8 (𝜑 → ((1 / 2) · 𝐴) ∈ ℂ)
161 sinmulcos 45820 . . . . . . . 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 584 . . . . . . 7 (𝜑 → ((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))) = (((sin‘(((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴))) + (sin‘(((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴)))) / 2))
163115, 2, 8adddird 11283 . . . . . . . . . . . 12 (𝜑 → ((𝑁 + (1 / 2)) · 𝐴) = ((𝑁 · 𝐴) + ((1 / 2) · 𝐴)))
164163oveq1d 7445 . . . . . . . . . . 11 (𝜑 → (((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴)) = (((𝑁 · 𝐴) + ((1 / 2) · 𝐴)) + ((1 / 2) · 𝐴)))
165139, 160, 160addassd 11280 . . . . . . . . . . 11 (𝜑 → (((𝑁 · 𝐴) + ((1 / 2) · 𝐴)) + ((1 / 2) · 𝐴)) = ((𝑁 · 𝐴) + (((1 / 2) · 𝐴) + ((1 / 2) · 𝐴))))
1662, 2, 8adddird 11283 . . . . . . . . . . . . . 14 (𝜑 → (((1 / 2) + (1 / 2)) · 𝐴) = (((1 / 2) · 𝐴) + ((1 / 2) · 𝐴)))
16712halvesd 12509 . . . . . . . . . . . . . . 15 (𝜑 → ((1 / 2) + (1 / 2)) = 1)
168167oveq1d 7445 . . . . . . . . . . . . . 14 (𝜑 → (((1 / 2) + (1 / 2)) · 𝐴) = (1 · 𝐴))
169166, 168eqtr3d 2776 . . . . . . . . . . . . 13 (𝜑 → (((1 / 2) · 𝐴) + ((1 / 2) · 𝐴)) = (1 · 𝐴))
170169oveq2d 7446 . . . . . . . . . . . 12 (𝜑 → ((𝑁 · 𝐴) + (((1 / 2) · 𝐴) + ((1 / 2) · 𝐴))) = ((𝑁 · 𝐴) + (1 · 𝐴)))
171115, 1, 8adddird 11283 . . . . . . . . . . . 12 (𝜑 → ((𝑁 + 1) · 𝐴) = ((𝑁 · 𝐴) + (1 · 𝐴)))
172170, 171eqtr4d 2777 . . . . . . . . . . 11 (𝜑 → ((𝑁 · 𝐴) + (((1 / 2) · 𝐴) + ((1 / 2) · 𝐴))) = ((𝑁 + 1) · 𝐴))
173164, 165, 1723eqtrrd 2779 . . . . . . . . . 10 (𝜑 → ((𝑁 + 1) · 𝐴) = (((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴)))
174173fveq2d 6910 . . . . . . . . 9 (𝜑 → (sin‘((𝑁 + 1) · 𝐴)) = (sin‘(((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴))))
175163oveq1d 7445 . . . . . . . . . . 11 (𝜑 → (((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴)) = (((𝑁 · 𝐴) + ((1 / 2) · 𝐴)) − ((1 / 2) · 𝐴)))
176139, 160pncand 11618 . . . . . . . . . . 11 (𝜑 → (((𝑁 · 𝐴) + ((1 / 2) · 𝐴)) − ((1 / 2) · 𝐴)) = (𝑁 · 𝐴))
177175, 176eqtr2d 2775 . . . . . . . . . 10 (𝜑 → (𝑁 · 𝐴) = (((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴)))
178177fveq2d 6910 . . . . . . . . 9 (𝜑 → (sin‘(𝑁 · 𝐴)) = (sin‘(((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴))))
179174, 178oveq12d 7448 . . . . . . . 8 (𝜑 → ((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))) = ((sin‘(((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴))) + (sin‘(((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴)))))
180179oveq1d 7445 . . . . . . 7 (𝜑 → (((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))) / 2) = (((sin‘(((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴))) + (sin‘(((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴)))) / 2))
181162, 180eqtr4d 2777 . . . . . 6 (𝜑 → ((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))) = (((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))) / 2))
182148oveq1d 7445 . . . . . 6 (𝜑 → (((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))) / 2) = (((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))) / 2))
183140, 137addcld 11277 . . . . . . 7 (𝜑 → ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))) ∈ ℂ)
184183, 52, 59divrec2d 12044 . . . . . 6 (𝜑 → (((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))) / 2) = ((1 / 2) · ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))))
185181, 182, 1843eqtrrd 2779 . . . . 5 (𝜑 → ((1 / 2) · ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))))
186185oveq1d 7445 . . . 4 (𝜑 → (((1 / 2) · ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) / (sin‘𝐴)) = (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))) / (sin‘𝐴)))
1878, 52, 59divcan2d 12042 . . . . . . . . 9 (𝜑 → (2 · (𝐴 / 2)) = 𝐴)
188187eqcomd 2740 . . . . . . . 8 (𝜑𝐴 = (2 · (𝐴 / 2)))
189188fveq2d 6910 . . . . . . 7 (𝜑 → (sin‘𝐴) = (sin‘(2 · (𝐴 / 2))))
1908halfcld 12508 . . . . . . . 8 (𝜑 → (𝐴 / 2) ∈ ℂ)
191 sin2t 16209 . . . . . . . 8 ((𝐴 / 2) ∈ ℂ → (sin‘(2 · (𝐴 / 2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))))
192190, 191syl 17 . . . . . . 7 (𝜑 → (sin‘(2 · (𝐴 / 2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))))
193189, 192eqtrd 2774 . . . . . 6 (𝜑 → (sin‘𝐴) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))))
194193oveq2d 7446 . . . . 5 (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))) / (sin‘𝐴)) = (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))) / (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))))))
195190sincld 16162 . . . . . . . 8 (𝜑 → (sin‘(𝐴 / 2)) ∈ ℂ)
196190coscld 16163 . . . . . . . 8 (𝜑 → (cos‘(𝐴 / 2)) ∈ ℂ)
19752, 195, 196mulassd 11281 . . . . . . 7 (𝜑 → ((2 · (sin‘(𝐴 / 2))) · (cos‘(𝐴 / 2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))))
1988, 52, 59divrec2d 12044 . . . . . . . . 9 (𝜑 → (𝐴 / 2) = ((1 / 2) · 𝐴))
199198fveq2d 6910 . . . . . . . 8 (𝜑 → (cos‘(𝐴 / 2)) = (cos‘((1 / 2) · 𝐴)))
200199oveq2d 7446 . . . . . . 7 (𝜑 → ((2 · (sin‘(𝐴 / 2))) · (cos‘(𝐴 / 2))) = ((2 · (sin‘(𝐴 / 2))) · (cos‘((1 / 2) · 𝐴))))
201197, 200eqtr3d 2776 . . . . . 6 (𝜑 → (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))) = ((2 · (sin‘(𝐴 / 2))) · (cos‘((1 / 2) · 𝐴))))
202201oveq2d 7446 . . . . 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 16162 . . . . . 6 (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝐴)) ∈ ℂ)
20452, 195mulcld 11278 . . . . . 6 (𝜑 → (2 · (sin‘(𝐴 / 2))) ∈ ℂ)
205160coscld 16163 . . . . . 6 (𝜑 → (cos‘((1 / 2) · 𝐴)) ∈ ℂ)
206195, 196mulcld 11278 . . . . . . . . 9 (𝜑 → ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))) ∈ ℂ)
207193, 15eqnetrrd 3006 . . . . . . . . 9 (𝜑 → (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))) ≠ 0)
20852, 206, 207mulne0bbd 11916 . . . . . . . 8 (𝜑 → ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))) ≠ 0)
209195, 196, 208mulne0bad 11915 . . . . . . 7 (𝜑 → (sin‘(𝐴 / 2)) ≠ 0)
21052, 195, 59, 209mulne0d 11912 . . . . . 6 (𝜑 → (2 · (sin‘(𝐴 / 2))) ≠ 0)
211195, 196, 208mulne0bbd 11916 . . . . . . 7 (𝜑 → (cos‘(𝐴 / 2)) ≠ 0)
212199, 211eqnetrrd 3006 . . . . . 6 (𝜑 → (cos‘((1 / 2) · 𝐴)) ≠ 0)
213203, 204, 205, 210, 212divcan5rd 12067 . . . . 5 (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))) / ((2 · (sin‘(𝐴 / 2))) · (cos‘((1 / 2) · 𝐴)))) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (2 · (sin‘(𝐴 / 2)))))
214194, 202, 2133eqtrd 2778 . . . 4 (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))) / (sin‘𝐴)) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (2 · (sin‘(𝐴 / 2)))))
215154, 186, 2143eqtrd 2778 . . 3 (𝜑 → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (2 · (sin‘(𝐴 / 2)))))
216215oveq1d 7445 . 2 (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = (((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (2 · (sin‘(𝐴 / 2)))) / π))
217 picn 26515 . . . 4 π ∈ ℂ
218217a1i 11 . . 3 (𝜑 → π ∈ ℂ)
219 pire 26514 . . . . 5 π ∈ ℝ
220 pipos 26516 . . . . 5 0 < π
221219, 220gt0ne0ii 11796 . . . 4 π ≠ 0
222221a1i 11 . . 3 (𝜑 → π ≠ 0)
223203, 204, 218, 210, 222divdiv32d 12065 . 2 (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (2 · (sin‘(𝐴 / 2)))) / π) = (((sin‘((𝑁 + (1 / 2)) · 𝐴)) / π) / (2 · (sin‘(𝐴 / 2)))))
224203, 218, 204, 222, 210divdiv1d 12071 . . 3 (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) / π) / (2 · (sin‘(𝐴 / 2)))) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (π · (2 · (sin‘(𝐴 / 2))))))
225218, 52, 195mulassd 11281 . . . . 5 (𝜑 → ((π · 2) · (sin‘(𝐴 / 2))) = (π · (2 · (sin‘(𝐴 / 2)))))
226218, 52mulcomd 11279 . . . . . 6 (𝜑 → (π · 2) = (2 · π))
227226oveq1d 7445 . . . . 5 (𝜑 → ((π · 2) · (sin‘(𝐴 / 2))) = ((2 · π) · (sin‘(𝐴 / 2))))
228225, 227eqtr3d 2776 . . . 4 (𝜑 → (π · (2 · (sin‘(𝐴 / 2)))) = ((2 · π) · (sin‘(𝐴 / 2))))
229228oveq2d 7446 . . 3 (𝜑 → ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (π · (2 · (sin‘(𝐴 / 2))))) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) · (sin‘(𝐴 / 2)))))
230224, 229eqtrd 2774 . 2 (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) / π) / (2 · (sin‘(𝐴 / 2)))) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) · (sin‘(𝐴 / 2)))))
231216, 223, 2303eqtrd 2778 1 (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) · (sin‘(𝐴 / 2)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1536  wcel 2105  wne 2937  cfv 6562  (class class class)co 7430  cc 11150  cr 11151  0cc0 11152  1c1 11153   + caddc 11155   · cmul 11157  cmin 11489  -cneg 11490   / cdiv 11917  cn 12263  2c2 12318  cuz 12875  ...cfz 13543  Σcsu 15718  sincsin 16095  cosccos 16096  πcpi 16098
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230  ax-addf 11231
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-iin 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-of 7696  df-om 7887  df-1st 8012  df-2nd 8013  df-supp 8184  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-er 8743  df-map 8866  df-pm 8867  df-ixp 8936  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-fsupp 9399  df-fi 9448  df-sup 9479  df-inf 9480  df-oi 9547  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331  df-8 12332  df-9 12333  df-n0 12524  df-z 12611  df-dec 12731  df-uz 12876  df-q 12988  df-rp 13032  df-xneg 13151  df-xadd 13152  df-xmul 13153  df-ioo 13387  df-ioc 13388  df-ico 13389  df-icc 13390  df-fz 13544  df-fzo 13691  df-fl 13828  df-seq 14039  df-exp 14099  df-fac 14309  df-bc 14338  df-hash 14366  df-shft 15102  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-limsup 15503  df-clim 15520  df-rlim 15521  df-sum 15719  df-ef 16099  df-sin 16101  df-cos 16102  df-pi 16104  df-struct 17180  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-rest 17468  df-topn 17469  df-0g 17487  df-gsum 17488  df-topgen 17489  df-pt 17490  df-prds 17493  df-xrs 17548  df-qtop 17553  df-imas 17554  df-xps 17556  df-mre 17630  df-mrc 17631  df-acs 17633  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-submnd 18809  df-mulg 19098  df-cntz 19347  df-cmn 19814  df-psmet 21373  df-xmet 21374  df-met 21375  df-bl 21376  df-mopn 21377  df-fbas 21378  df-fg 21379  df-cnfld 21382  df-top 22915  df-topon 22932  df-topsp 22954  df-bases 22968  df-cld 23042  df-ntr 23043  df-cls 23044  df-nei 23121  df-lp 23159  df-perf 23160  df-cn 23250  df-cnp 23251  df-haus 23338  df-tx 23585  df-hmeo 23778  df-fil 23869  df-fm 23961  df-flim 23962  df-flf 23963  df-xms 24345  df-ms 24346  df-tms 24347  df-cncf 24917  df-limc 25915  df-dv 25916
This theorem is referenced by:  dirkertrigeq  46056
  Copyright terms: Public domain W3C validator