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 44028
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 11072 . . . . . . . . 9 (𝜑 → 1 ∈ ℂ)
21halfcld 12320 . . . . . . . 8 (𝜑 → (1 / 2) ∈ ℂ)
3 fzfid 13795 . . . . . . . . 9 (𝜑 → (1...𝑁) ∈ Fin)
4 elfzelz 13358 . . . . . . . . . . . . 13 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℤ)
54zcnd 12529 . . . . . . . . . . . 12 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
65adantl 482 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℂ)
7 dirkertrigeqlem2.a . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℝ)
87recnd 11105 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℂ)
98adantr 481 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → 𝐴 ∈ ℂ)
106, 9mulcld 11097 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑛 · 𝐴) ∈ ℂ)
1110coscld 15940 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝐴)) ∈ ℂ)
123, 11fsumcl 15545 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) ∈ ℂ)
132, 12addcld 11096 . . . . . . 7 (𝜑 → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) ∈ ℂ)
148sincld 15939 . . . . . . 7 (𝜑 → (sin‘𝐴) ∈ ℂ)
15 dirkertrigeqlem2.sinne0 . . . . . . 7 (𝜑 → (sin‘𝐴) ≠ 0)
1613, 14, 15divcan4d 11859 . . . . . 6 (𝜑 → ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) · (sin‘𝐴)) / (sin‘𝐴)) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))))
1716eqcomd 2742 . . . . 5 (𝜑 → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) = ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) · (sin‘𝐴)) / (sin‘𝐴)))
183, 14, 11fsummulc1 15597 . . . . . . . . 9 (𝜑 → (Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) · (sin‘𝐴)) = Σ𝑛 ∈ (1...𝑁)((cos‘(𝑛 · 𝐴)) · (sin‘𝐴)))
1914adantr 481 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘𝐴) ∈ ℂ)
2011, 19mulcomd 11098 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝐴)) · (sin‘𝐴)) = ((sin‘𝐴) · (cos‘(𝑛 · 𝐴))))
21 sinmulcos 43794 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ (𝑛 · 𝐴) ∈ ℂ) → ((sin‘𝐴) · (cos‘(𝑛 · 𝐴))) = (((sin‘(𝐴 + (𝑛 · 𝐴))) + (sin‘(𝐴 − (𝑛 · 𝐴)))) / 2))
229, 10, 21syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘𝐴) · (cos‘(𝑛 · 𝐴))) = (((sin‘(𝐴 + (𝑛 · 𝐴))) + (sin‘(𝐴 − (𝑛 · 𝐴)))) / 2))
23 1cnd 11072 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (1...𝑁)) → 1 ∈ ℂ)
246, 23, 9adddird 11102 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑛 + 1) · 𝐴) = ((𝑛 · 𝐴) + (1 · 𝐴)))
2523, 9mulcld 11097 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (1...𝑁)) → (1 · 𝐴) ∈ ℂ)
2610, 25addcomd 11279 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑛 · 𝐴) + (1 · 𝐴)) = ((1 · 𝐴) + (𝑛 · 𝐴)))
278mulid2d 11095 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1 · 𝐴) = 𝐴)
2827oveq1d 7353 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1 · 𝐴) + (𝑛 · 𝐴)) = (𝐴 + (𝑛 · 𝐴)))
2928adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...𝑁)) → ((1 · 𝐴) + (𝑛 · 𝐴)) = (𝐴 + (𝑛 · 𝐴)))
3024, 26, 293eqtrrd 2781 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...𝑁)) → (𝐴 + (𝑛 · 𝐴)) = ((𝑛 + 1) · 𝐴))
3130fveq2d 6830 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝐴 + (𝑛 · 𝐴))) = (sin‘((𝑛 + 1) · 𝐴)))
3210, 9negsubdi2d 11450 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (1...𝑁)) → -((𝑛 · 𝐴) − 𝐴) = (𝐴 − (𝑛 · 𝐴)))
3332eqcomd 2742 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...𝑁)) → (𝐴 − (𝑛 · 𝐴)) = -((𝑛 · 𝐴) − 𝐴))
3433fveq2d 6830 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝐴 − (𝑛 · 𝐴))) = (sin‘-((𝑛 · 𝐴) − 𝐴)))
3510, 9subcld 11434 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑛 · 𝐴) − 𝐴) ∈ ℂ)
36 sinneg 15955 . . . . . . . . . . . . . . . 16 (((𝑛 · 𝐴) − 𝐴) ∈ ℂ → (sin‘-((𝑛 · 𝐴) − 𝐴)) = -(sin‘((𝑛 · 𝐴) − 𝐴)))
3735, 36syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘-((𝑛 · 𝐴) − 𝐴)) = -(sin‘((𝑛 · 𝐴) − 𝐴)))
3834, 37eqtrd 2776 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝐴 − (𝑛 · 𝐴))) = -(sin‘((𝑛 · 𝐴) − 𝐴)))
3931, 38oveq12d 7356 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘(𝐴 + (𝑛 · 𝐴))) + (sin‘(𝐴 − (𝑛 · 𝐴)))) = ((sin‘((𝑛 + 1) · 𝐴)) + -(sin‘((𝑛 · 𝐴) − 𝐴))))
409, 10addcld 11096 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...𝑁)) → (𝐴 + (𝑛 · 𝐴)) ∈ ℂ)
4140sincld 15939 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝐴 + (𝑛 · 𝐴))) ∈ ℂ)
4231, 41eqeltrrd 2838 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘((𝑛 + 1) · 𝐴)) ∈ ℂ)
4335sincld 15939 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘((𝑛 · 𝐴) − 𝐴)) ∈ ℂ)
4442, 43negsubd 11440 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘((𝑛 + 1) · 𝐴)) + -(sin‘((𝑛 · 𝐴) − 𝐴))) = ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 · 𝐴) − 𝐴))))
456, 9mulsubfacd 11538 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑛 · 𝐴) − 𝐴) = ((𝑛 − 1) · 𝐴))
4645fveq2d 6830 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘((𝑛 · 𝐴) − 𝐴)) = (sin‘((𝑛 − 1) · 𝐴)))
4746oveq2d 7354 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 · 𝐴) − 𝐴))) = ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))
4839, 44, 473eqtrd 2780 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘(𝐴 + (𝑛 · 𝐴))) + (sin‘(𝐴 − (𝑛 · 𝐴)))) = ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))
4948oveq1d 7353 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → (((sin‘(𝐴 + (𝑛 · 𝐴))) + (sin‘(𝐴 − (𝑛 · 𝐴)))) / 2) = (((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2))
5020, 22, 493eqtrd 2780 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝐴)) · (sin‘𝐴)) = (((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2))
5150sumeq2dv 15515 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (1...𝑁)((cos‘(𝑛 · 𝐴)) · (sin‘𝐴)) = Σ𝑛 ∈ (1...𝑁)(((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2))
52 2cnd 12153 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℂ)
53 peano2cnm 11389 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℂ → (𝑛 − 1) ∈ ℂ)
546, 53syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑛 − 1) ∈ ℂ)
5554, 9mulcld 11097 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → ((𝑛 − 1) · 𝐴) ∈ ℂ)
5655sincld 15939 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘((𝑛 − 1) · 𝐴)) ∈ ℂ)
5742, 56subcld 11434 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) ∈ ℂ)
58 2ne0 12179 . . . . . . . . . . . 12 2 ≠ 0
5958a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ≠ 0)
603, 52, 57, 59fsumdivc 15598 . . . . . . . . . 10 (𝜑 → (Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2) = Σ𝑛 ∈ (1...𝑁)(((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2))
613, 57fsumcl 15545 . . . . . . . . . . 11 (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) ∈ ℂ)
6261, 52, 59divrec2d 11857 . . . . . . . . . 10 (𝜑 → (Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2) = ((1 / 2) · Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))))
6360, 62eqtr3d 2778 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (1...𝑁)(((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) / 2) = ((1 / 2) · Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))))
6418, 51, 633eqtrd 2780 . . . . . . . 8 (𝜑 → (Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) · (sin‘𝐴)) = ((1 / 2) · Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))))
6564oveq2d 7354 . . . . . . 7 (𝜑 → (((1 / 2) · (sin‘𝐴)) + (Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) · (sin‘𝐴))) = (((1 / 2) · (sin‘𝐴)) + ((1 / 2) · Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))))
662, 12, 14adddird 11102 . . . . . . 7 (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) · (sin‘𝐴)) = (((1 / 2) · (sin‘𝐴)) + (Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴)) · (sin‘𝐴))))
672, 14, 61adddid 11101 . . . . . . 7 (𝜑 → ((1 / 2) · ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) = (((1 / 2) · (sin‘𝐴)) + ((1 / 2) · Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))))
6865, 66, 673eqtr4d 2786 . . . . . 6 (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) · (sin‘𝐴)) = ((1 / 2) · ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))))
6968oveq1d 7353 . . . . 5 (𝜑 → ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) · (sin‘𝐴)) / (sin‘𝐴)) = (((1 / 2) · ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) / (sin‘𝐴)))
7010sincld 15939 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝐴)) ∈ ℂ)
7142, 70, 56npncand 11458 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝑁)) → (((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) = ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))
7271eqcomd 2742 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = (((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))))
7372sumeq2dv 15515 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = Σ𝑛 ∈ (1...𝑁)(((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))))
7442, 70subcld 11434 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) ∈ ℂ)
7570, 56subcld 11434 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) ∈ ℂ)
763, 74, 75fsumadd 15552 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (1...𝑁)(((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) = (Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + Σ𝑛 ∈ (1...𝑁)((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))))
77 fvoveq1 7361 . . . . . . . . . . . 12 (𝑗 = 𝑛 → (sin‘(𝑗 · 𝐴)) = (sin‘(𝑛 · 𝐴)))
78 fvoveq1 7361 . . . . . . . . . . . 12 (𝑗 = (𝑛 + 1) → (sin‘(𝑗 · 𝐴)) = (sin‘((𝑛 + 1) · 𝐴)))
79 fvoveq1 7361 . . . . . . . . . . . 12 (𝑗 = 1 → (sin‘(𝑗 · 𝐴)) = (sin‘(1 · 𝐴)))
80 fvoveq1 7361 . . . . . . . . . . . 12 (𝑗 = (𝑁 + 1) → (sin‘(𝑗 · 𝐴)) = (sin‘((𝑁 + 1) · 𝐴)))
81 dirkertrigeqlem2.n . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℕ)
8281nnzd 12527 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℤ)
83 nnuz 12723 . . . . . . . . . . . . . 14 ℕ = (ℤ‘1)
8481, 83eleqtrdi 2847 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ (ℤ‘1))
85 peano2uz 12743 . . . . . . . . . . . . 13 (𝑁 ∈ (ℤ‘1) → (𝑁 + 1) ∈ (ℤ‘1))
8684, 85syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑁 + 1) ∈ (ℤ‘1))
87 elfzelz 13358 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℤ)
8887zcnd 12529 . . . . . . . . . . . . . . 15 (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℂ)
8988adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...(𝑁 + 1))) → 𝑗 ∈ ℂ)
908adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...(𝑁 + 1))) → 𝐴 ∈ ℂ)
9189, 90mulcld 11097 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...(𝑁 + 1))) → (𝑗 · 𝐴) ∈ ℂ)
9291sincld 15939 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...(𝑁 + 1))) → (sin‘(𝑗 · 𝐴)) ∈ ℂ)
9377, 78, 79, 80, 82, 86, 92telfsum2 15617 . . . . . . . . . . 11 (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) = ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))))
94 1cnd 11072 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) → 1 ∈ ℂ)
955, 94pncand 11435 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (1...𝑁) → ((𝑛 + 1) − 1) = 𝑛)
9695eqcomd 2742 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (1...𝑁) → 𝑛 = ((𝑛 + 1) − 1))
9796adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...𝑁)) → 𝑛 = ((𝑛 + 1) − 1))
9897fvoveq1d 7360 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝐴)) = (sin‘(((𝑛 + 1) − 1) · 𝐴)))
9998oveq1d 7353 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = ((sin‘(((𝑛 + 1) − 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))
10099sumeq2dv 15515 . . . . . . . . . . . 12 (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = Σ𝑛 ∈ (1...𝑁)((sin‘(((𝑛 + 1) − 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))
101 oveq1 7345 . . . . . . . . . . . . . 14 (𝑗 = 𝑛 → (𝑗 − 1) = (𝑛 − 1))
102101fvoveq1d 7360 . . . . . . . . . . . . 13 (𝑗 = 𝑛 → (sin‘((𝑗 − 1) · 𝐴)) = (sin‘((𝑛 − 1) · 𝐴)))
103 oveq1 7345 . . . . . . . . . . . . . 14 (𝑗 = (𝑛 + 1) → (𝑗 − 1) = ((𝑛 + 1) − 1))
104103fvoveq1d 7360 . . . . . . . . . . . . 13 (𝑗 = (𝑛 + 1) → (sin‘((𝑗 − 1) · 𝐴)) = (sin‘(((𝑛 + 1) − 1) · 𝐴)))
105 oveq1 7345 . . . . . . . . . . . . . 14 (𝑗 = 1 → (𝑗 − 1) = (1 − 1))
106105fvoveq1d 7360 . . . . . . . . . . . . 13 (𝑗 = 1 → (sin‘((𝑗 − 1) · 𝐴)) = (sin‘((1 − 1) · 𝐴)))
107 oveq1 7345 . . . . . . . . . . . . . 14 (𝑗 = (𝑁 + 1) → (𝑗 − 1) = ((𝑁 + 1) − 1))
108107fvoveq1d 7360 . . . . . . . . . . . . 13 (𝑗 = (𝑁 + 1) → (sin‘((𝑗 − 1) · 𝐴)) = (sin‘(((𝑁 + 1) − 1) · 𝐴)))
109 1cnd 11072 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (1...(𝑁 + 1))) → 1 ∈ ℂ)
11089, 109subcld 11434 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (1...(𝑁 + 1))) → (𝑗 − 1) ∈ ℂ)
111110, 90mulcld 11097 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...(𝑁 + 1))) → ((𝑗 − 1) · 𝐴) ∈ ℂ)
112111sincld 15939 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...(𝑁 + 1))) → (sin‘((𝑗 − 1) · 𝐴)) ∈ ℂ)
113102, 104, 106, 108, 82, 86, 112telfsum2 15617 . . . . . . . . . . . 12 (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘(((𝑛 + 1) − 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = ((sin‘(((𝑁 + 1) − 1) · 𝐴)) − (sin‘((1 − 1) · 𝐴))))
11481nnred 12090 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℝ)
115114recnd 11105 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℂ)
116115, 1pncand 11435 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
117116fvoveq1d 7360 . . . . . . . . . . . . 13 (𝜑 → (sin‘(((𝑁 + 1) − 1) · 𝐴)) = (sin‘(𝑁 · 𝐴)))
1181subidd 11422 . . . . . . . . . . . . . . . . 17 (𝜑 → (1 − 1) = 0)
119118oveq1d 7353 . . . . . . . . . . . . . . . 16 (𝜑 → ((1 − 1) · 𝐴) = (0 · 𝐴))
1208mul02d 11275 . . . . . . . . . . . . . . . 16 (𝜑 → (0 · 𝐴) = 0)
121119, 120eqtrd 2776 . . . . . . . . . . . . . . 15 (𝜑 → ((1 − 1) · 𝐴) = 0)
122121fveq2d 6830 . . . . . . . . . . . . . 14 (𝜑 → (sin‘((1 − 1) · 𝐴)) = (sin‘0))
123 sin0 15958 . . . . . . . . . . . . . . 15 (sin‘0) = 0
124123a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (sin‘0) = 0)
125122, 124eqtrd 2776 . . . . . . . . . . . . 13 (𝜑 → (sin‘((1 − 1) · 𝐴)) = 0)
126117, 125oveq12d 7356 . . . . . . . . . . . 12 (𝜑 → ((sin‘(((𝑁 + 1) − 1) · 𝐴)) − (sin‘((1 − 1) · 𝐴))) = ((sin‘(𝑁 · 𝐴)) − 0))
127100, 113, 1263eqtrd 2780 . . . . . . . . . . 11 (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = ((sin‘(𝑁 · 𝐴)) − 0))
12893, 127oveq12d 7356 . . . . . . . . . 10 (𝜑 → (Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘(𝑛 · 𝐴))) + Σ𝑛 ∈ (1...𝑁)((sin‘(𝑛 · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) = (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)))
12973, 76, 1283eqtrd 2780 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))) = (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)))
130129oveq2d 7354 . . . . . . . 8 (𝜑 → ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) = ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0))))
13127fveq2d 6830 . . . . . . . . . . . 12 (𝜑 → (sin‘(1 · 𝐴)) = (sin‘𝐴))
132131oveq2d 7354 . . . . . . . . . . 11 (𝜑 → ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) = ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)))
133132oveq1d 7353 . . . . . . . . . 10 (𝜑 → (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)) = (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)) + ((sin‘(𝑁 · 𝐴)) − 0)))
134133oveq2d 7354 . . . . . . . . 9 (𝜑 → ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0))) = ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)) + ((sin‘(𝑁 · 𝐴)) − 0))))
135115, 1addcld 11096 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 + 1) ∈ ℂ)
136135, 8mulcld 11097 . . . . . . . . . . . . 13 (𝜑 → ((𝑁 + 1) · 𝐴) ∈ ℂ)
137136sincld 15939 . . . . . . . . . . . 12 (𝜑 → (sin‘((𝑁 + 1) · 𝐴)) ∈ ℂ)
138137, 14subcld 11434 . . . . . . . . . . 11 (𝜑 → ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)) ∈ ℂ)
139115, 8mulcld 11097 . . . . . . . . . . . . 13 (𝜑 → (𝑁 · 𝐴) ∈ ℂ)
140139sincld 15939 . . . . . . . . . . . 12 (𝜑 → (sin‘(𝑁 · 𝐴)) ∈ ℂ)
141 0cnd 11070 . . . . . . . . . . . 12 (𝜑 → 0 ∈ ℂ)
142140, 141subcld 11434 . . . . . . . . . . 11 (𝜑 → ((sin‘(𝑁 · 𝐴)) − 0) ∈ ℂ)
14314, 138, 142addassd 11099 . . . . . . . . . 10 (𝜑 → (((sin‘𝐴) + ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)) = ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)) + ((sin‘(𝑁 · 𝐴)) − 0))))
144143eqcomd 2742 . . . . . . . . 9 (𝜑 → ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴)) + ((sin‘(𝑁 · 𝐴)) − 0))) = (((sin‘𝐴) + ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)))
14514, 137pncan3d 11437 . . . . . . . . . . 11 (𝜑 → ((sin‘𝐴) + ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) = (sin‘((𝑁 + 1) · 𝐴)))
146140subid1d 11423 . . . . . . . . . . 11 (𝜑 → ((sin‘(𝑁 · 𝐴)) − 0) = (sin‘(𝑁 · 𝐴)))
147145, 146oveq12d 7356 . . . . . . . . . 10 (𝜑 → (((sin‘𝐴) + ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)) = ((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))))
148137, 140addcomd 11279 . . . . . . . . . 10 (𝜑 → ((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))) = ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))))
149147, 148eqtrd 2776 . . . . . . . . 9 (𝜑 → (((sin‘𝐴) + ((sin‘((𝑁 + 1) · 𝐴)) − (sin‘𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0)) = ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))))
150134, 144, 1493eqtrd 2780 . . . . . . . 8 (𝜑 → ((sin‘𝐴) + (((sin‘((𝑁 + 1) · 𝐴)) − (sin‘(1 · 𝐴))) + ((sin‘(𝑁 · 𝐴)) − 0))) = ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))))
151130, 150eqtrd 2776 . . . . . . 7 (𝜑 → ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴)))) = ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))))
152151oveq2d 7354 . . . . . 6 (𝜑 → ((1 / 2) · ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) = ((1 / 2) · ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))))
153152oveq1d 7353 . . . . 5 (𝜑 → (((1 / 2) · ((sin‘𝐴) + Σ𝑛 ∈ (1...𝑁)((sin‘((𝑛 + 1) · 𝐴)) − (sin‘((𝑛 − 1) · 𝐴))))) / (sin‘𝐴)) = (((1 / 2) · ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) / (sin‘𝐴)))
15417, 69, 1533eqtrd 2780 . . . 4 (𝜑 → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) = (((1 / 2) · ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) / (sin‘𝐴)))
155 halfre 12289 . . . . . . . . . . . 12 (1 / 2) ∈ ℝ
156155a1i 11 . . . . . . . . . . 11 (𝜑 → (1 / 2) ∈ ℝ)
157114, 156readdcld 11106 . . . . . . . . . 10 (𝜑 → (𝑁 + (1 / 2)) ∈ ℝ)
158157, 7remulcld 11107 . . . . . . . . 9 (𝜑 → ((𝑁 + (1 / 2)) · 𝐴) ∈ ℝ)
159158recnd 11105 . . . . . . . 8 (𝜑 → ((𝑁 + (1 / 2)) · 𝐴) ∈ ℂ)
1602, 8mulcld 11097 . . . . . . . 8 (𝜑 → ((1 / 2) · 𝐴) ∈ ℂ)
161 sinmulcos 43794 . . . . . . . 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 11102 . . . . . . . . . . . 12 (𝜑 → ((𝑁 + (1 / 2)) · 𝐴) = ((𝑁 · 𝐴) + ((1 / 2) · 𝐴)))
164163oveq1d 7353 . . . . . . . . . . 11 (𝜑 → (((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴)) = (((𝑁 · 𝐴) + ((1 / 2) · 𝐴)) + ((1 / 2) · 𝐴)))
165139, 160, 160addassd 11099 . . . . . . . . . . 11 (𝜑 → (((𝑁 · 𝐴) + ((1 / 2) · 𝐴)) + ((1 / 2) · 𝐴)) = ((𝑁 · 𝐴) + (((1 / 2) · 𝐴) + ((1 / 2) · 𝐴))))
1662, 2, 8adddird 11102 . . . . . . . . . . . . . 14 (𝜑 → (((1 / 2) + (1 / 2)) · 𝐴) = (((1 / 2) · 𝐴) + ((1 / 2) · 𝐴)))
16712halvesd 12321 . . . . . . . . . . . . . . 15 (𝜑 → ((1 / 2) + (1 / 2)) = 1)
168167oveq1d 7353 . . . . . . . . . . . . . 14 (𝜑 → (((1 / 2) + (1 / 2)) · 𝐴) = (1 · 𝐴))
169166, 168eqtr3d 2778 . . . . . . . . . . . . 13 (𝜑 → (((1 / 2) · 𝐴) + ((1 / 2) · 𝐴)) = (1 · 𝐴))
170169oveq2d 7354 . . . . . . . . . . . 12 (𝜑 → ((𝑁 · 𝐴) + (((1 / 2) · 𝐴) + ((1 / 2) · 𝐴))) = ((𝑁 · 𝐴) + (1 · 𝐴)))
171115, 1, 8adddird 11102 . . . . . . . . . . . 12 (𝜑 → ((𝑁 + 1) · 𝐴) = ((𝑁 · 𝐴) + (1 · 𝐴)))
172170, 171eqtr4d 2779 . . . . . . . . . . 11 (𝜑 → ((𝑁 · 𝐴) + (((1 / 2) · 𝐴) + ((1 / 2) · 𝐴))) = ((𝑁 + 1) · 𝐴))
173164, 165, 1723eqtrrd 2781 . . . . . . . . . 10 (𝜑 → ((𝑁 + 1) · 𝐴) = (((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴)))
174173fveq2d 6830 . . . . . . . . 9 (𝜑 → (sin‘((𝑁 + 1) · 𝐴)) = (sin‘(((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴))))
175163oveq1d 7353 . . . . . . . . . . 11 (𝜑 → (((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴)) = (((𝑁 · 𝐴) + ((1 / 2) · 𝐴)) − ((1 / 2) · 𝐴)))
176139, 160pncand 11435 . . . . . . . . . . 11 (𝜑 → (((𝑁 · 𝐴) + ((1 / 2) · 𝐴)) − ((1 / 2) · 𝐴)) = (𝑁 · 𝐴))
177175, 176eqtr2d 2777 . . . . . . . . . 10 (𝜑 → (𝑁 · 𝐴) = (((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴)))
178177fveq2d 6830 . . . . . . . . 9 (𝜑 → (sin‘(𝑁 · 𝐴)) = (sin‘(((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴))))
179174, 178oveq12d 7356 . . . . . . . 8 (𝜑 → ((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))) = ((sin‘(((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴))) + (sin‘(((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴)))))
180179oveq1d 7353 . . . . . . 7 (𝜑 → (((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))) / 2) = (((sin‘(((𝑁 + (1 / 2)) · 𝐴) + ((1 / 2) · 𝐴))) + (sin‘(((𝑁 + (1 / 2)) · 𝐴) − ((1 / 2) · 𝐴)))) / 2))
181162, 180eqtr4d 2779 . . . . . 6 (𝜑 → ((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))) = (((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))) / 2))
182148oveq1d 7353 . . . . . 6 (𝜑 → (((sin‘((𝑁 + 1) · 𝐴)) + (sin‘(𝑁 · 𝐴))) / 2) = (((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))) / 2))
183140, 137addcld 11096 . . . . . . 7 (𝜑 → ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))) ∈ ℂ)
184183, 52, 59divrec2d 11857 . . . . . 6 (𝜑 → (((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴))) / 2) = ((1 / 2) · ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))))
185181, 182, 1843eqtrrd 2781 . . . . 5 (𝜑 → ((1 / 2) · ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))))
186185oveq1d 7353 . . . 4 (𝜑 → (((1 / 2) · ((sin‘(𝑁 · 𝐴)) + (sin‘((𝑁 + 1) · 𝐴)))) / (sin‘𝐴)) = (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))) / (sin‘𝐴)))
1878, 52, 59divcan2d 11855 . . . . . . . . 9 (𝜑 → (2 · (𝐴 / 2)) = 𝐴)
188187eqcomd 2742 . . . . . . . 8 (𝜑𝐴 = (2 · (𝐴 / 2)))
189188fveq2d 6830 . . . . . . 7 (𝜑 → (sin‘𝐴) = (sin‘(2 · (𝐴 / 2))))
1908halfcld 12320 . . . . . . . 8 (𝜑 → (𝐴 / 2) ∈ ℂ)
191 sin2t 15986 . . . . . . . 8 ((𝐴 / 2) ∈ ℂ → (sin‘(2 · (𝐴 / 2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))))
192190, 191syl 17 . . . . . . 7 (𝜑 → (sin‘(2 · (𝐴 / 2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))))
193189, 192eqtrd 2776 . . . . . 6 (𝜑 → (sin‘𝐴) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))))
194193oveq2d 7354 . . . . 5 (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))) / (sin‘𝐴)) = (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))) / (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))))))
195190sincld 15939 . . . . . . . 8 (𝜑 → (sin‘(𝐴 / 2)) ∈ ℂ)
196190coscld 15940 . . . . . . . 8 (𝜑 → (cos‘(𝐴 / 2)) ∈ ℂ)
19752, 195, 196mulassd 11100 . . . . . . 7 (𝜑 → ((2 · (sin‘(𝐴 / 2))) · (cos‘(𝐴 / 2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))))
1988, 52, 59divrec2d 11857 . . . . . . . . 9 (𝜑 → (𝐴 / 2) = ((1 / 2) · 𝐴))
199198fveq2d 6830 . . . . . . . 8 (𝜑 → (cos‘(𝐴 / 2)) = (cos‘((1 / 2) · 𝐴)))
200199oveq2d 7354 . . . . . . 7 (𝜑 → ((2 · (sin‘(𝐴 / 2))) · (cos‘(𝐴 / 2))) = ((2 · (sin‘(𝐴 / 2))) · (cos‘((1 / 2) · 𝐴))))
201197, 200eqtr3d 2778 . . . . . 6 (𝜑 → (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))) = ((2 · (sin‘(𝐴 / 2))) · (cos‘((1 / 2) · 𝐴))))
202201oveq2d 7354 . . . . 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 15939 . . . . . 6 (𝜑 → (sin‘((𝑁 + (1 / 2)) · 𝐴)) ∈ ℂ)
20452, 195mulcld 11097 . . . . . 6 (𝜑 → (2 · (sin‘(𝐴 / 2))) ∈ ℂ)
205160coscld 15940 . . . . . 6 (𝜑 → (cos‘((1 / 2) · 𝐴)) ∈ ℂ)
206195, 196mulcld 11097 . . . . . . . . 9 (𝜑 → ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))) ∈ ℂ)
207193, 15eqnetrrd 3009 . . . . . . . . 9 (𝜑 → (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))) ≠ 0)
20852, 206, 207mulne0bbd 11733 . . . . . . . 8 (𝜑 → ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))) ≠ 0)
209195, 196, 208mulne0bad 11732 . . . . . . 7 (𝜑 → (sin‘(𝐴 / 2)) ≠ 0)
21052, 195, 59, 209mulne0d 11729 . . . . . 6 (𝜑 → (2 · (sin‘(𝐴 / 2))) ≠ 0)
211195, 196, 208mulne0bbd 11733 . . . . . . 7 (𝜑 → (cos‘(𝐴 / 2)) ≠ 0)
212199, 211eqnetrrd 3009 . . . . . 6 (𝜑 → (cos‘((1 / 2) · 𝐴)) ≠ 0)
213203, 204, 205, 210, 212divcan5rd 11880 . . . . 5 (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))) / ((2 · (sin‘(𝐴 / 2))) · (cos‘((1 / 2) · 𝐴)))) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (2 · (sin‘(𝐴 / 2)))))
214194, 202, 2133eqtrd 2780 . . . 4 (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) · (cos‘((1 / 2) · 𝐴))) / (sin‘𝐴)) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (2 · (sin‘(𝐴 / 2)))))
215154, 186, 2143eqtrd 2780 . . 3 (𝜑 → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (2 · (sin‘(𝐴 / 2)))))
216215oveq1d 7353 . 2 (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = (((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (2 · (sin‘(𝐴 / 2)))) / π))
217 picn 25723 . . . 4 π ∈ ℂ
218217a1i 11 . . 3 (𝜑 → π ∈ ℂ)
219 pire 25722 . . . . 5 π ∈ ℝ
220 pipos 25724 . . . . 5 0 < π
221219, 220gt0ne0ii 11613 . . . 4 π ≠ 0
222221a1i 11 . . 3 (𝜑 → π ≠ 0)
223203, 204, 218, 210, 222divdiv32d 11878 . 2 (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (2 · (sin‘(𝐴 / 2)))) / π) = (((sin‘((𝑁 + (1 / 2)) · 𝐴)) / π) / (2 · (sin‘(𝐴 / 2)))))
224203, 218, 204, 222, 210divdiv1d 11884 . . 3 (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) / π) / (2 · (sin‘(𝐴 / 2)))) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (π · (2 · (sin‘(𝐴 / 2))))))
225218, 52, 195mulassd 11100 . . . . 5 (𝜑 → ((π · 2) · (sin‘(𝐴 / 2))) = (π · (2 · (sin‘(𝐴 / 2)))))
226218, 52mulcomd 11098 . . . . . 6 (𝜑 → (π · 2) = (2 · π))
227226oveq1d 7353 . . . . 5 (𝜑 → ((π · 2) · (sin‘(𝐴 / 2))) = ((2 · π) · (sin‘(𝐴 / 2))))
228225, 227eqtr3d 2778 . . . 4 (𝜑 → (π · (2 · (sin‘(𝐴 / 2)))) = ((2 · π) · (sin‘(𝐴 / 2))))
229228oveq2d 7354 . . 3 (𝜑 → ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / (π · (2 · (sin‘(𝐴 / 2))))) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) · (sin‘(𝐴 / 2)))))
230224, 229eqtrd 2776 . 2 (𝜑 → (((sin‘((𝑁 + (1 / 2)) · 𝐴)) / π) / (2 · (sin‘(𝐴 / 2)))) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) · (sin‘(𝐴 / 2)))))
231216, 223, 2303eqtrd 2780 1 (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) · (sin‘(𝐴 / 2)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1540  wcel 2105  wne 2940  cfv 6480  (class class class)co 7338  cc 10971  cr 10972  0cc0 10973  1c1 10974   + caddc 10976   · cmul 10978  cmin 11307  -cneg 11308   / cdiv 11734  cn 12075  2c2 12130  cuz 12684  ...cfz 13341  Σcsu 15497  sincsin 15873  cosccos 15874  πcpi 15876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5230  ax-sep 5244  ax-nul 5251  ax-pow 5309  ax-pr 5373  ax-un 7651  ax-inf2 9499  ax-cnex 11029  ax-resscn 11030  ax-1cn 11031  ax-icn 11032  ax-addcl 11033  ax-addrcl 11034  ax-mulcl 11035  ax-mulrcl 11036  ax-mulcom 11037  ax-addass 11038  ax-mulass 11039  ax-distr 11040  ax-i2m1 11041  ax-1ne0 11042  ax-1rid 11043  ax-rnegex 11044  ax-rrecex 11045  ax-cnre 11046  ax-pre-lttri 11047  ax-pre-lttrn 11048  ax-pre-ltadd 11049  ax-pre-mulgt0 11050  ax-pre-sup 11051  ax-addf 11052  ax-mulf 11053
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-tp 4579  df-op 4581  df-uni 4854  df-int 4896  df-iun 4944  df-iin 4945  df-br 5094  df-opab 5156  df-mpt 5177  df-tr 5211  df-id 5519  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5576  df-se 5577  df-we 5578  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6239  df-ord 6306  df-on 6307  df-lim 6308  df-suc 6309  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-f1 6485  df-fo 6486  df-f1o 6487  df-fv 6488  df-isom 6489  df-riota 7294  df-ov 7341  df-oprab 7342  df-mpo 7343  df-of 7596  df-om 7782  df-1st 7900  df-2nd 7901  df-supp 8049  df-frecs 8168  df-wrecs 8199  df-recs 8273  df-rdg 8312  df-1o 8368  df-2o 8369  df-er 8570  df-map 8689  df-pm 8690  df-ixp 8758  df-en 8806  df-dom 8807  df-sdom 8808  df-fin 8809  df-fsupp 9228  df-fi 9269  df-sup 9300  df-inf 9301  df-oi 9368  df-card 9797  df-pnf 11113  df-mnf 11114  df-xr 11115  df-ltxr 11116  df-le 11117  df-sub 11309  df-neg 11310  df-div 11735  df-nn 12076  df-2 12138  df-3 12139  df-4 12140  df-5 12141  df-6 12142  df-7 12143  df-8 12144  df-9 12145  df-n0 12336  df-z 12422  df-dec 12540  df-uz 12685  df-q 12791  df-rp 12833  df-xneg 12950  df-xadd 12951  df-xmul 12952  df-ioo 13185  df-ioc 13186  df-ico 13187  df-icc 13188  df-fz 13342  df-fzo 13485  df-fl 13614  df-seq 13824  df-exp 13885  df-fac 14090  df-bc 14119  df-hash 14147  df-shft 14878  df-cj 14910  df-re 14911  df-im 14912  df-sqrt 15046  df-abs 15047  df-limsup 15280  df-clim 15297  df-rlim 15298  df-sum 15498  df-ef 15877  df-sin 15879  df-cos 15880  df-pi 15882  df-struct 16946  df-sets 16963  df-slot 16981  df-ndx 16993  df-base 17011  df-ress 17040  df-plusg 17073  df-mulr 17074  df-starv 17075  df-sca 17076  df-vsca 17077  df-ip 17078  df-tset 17079  df-ple 17080  df-ds 17082  df-unif 17083  df-hom 17084  df-cco 17085  df-rest 17231  df-topn 17232  df-0g 17250  df-gsum 17251  df-topgen 17252  df-pt 17253  df-prds 17256  df-xrs 17311  df-qtop 17316  df-imas 17317  df-xps 17319  df-mre 17393  df-mrc 17394  df-acs 17396  df-mgm 18424  df-sgrp 18473  df-mnd 18484  df-submnd 18529  df-mulg 18798  df-cntz 19020  df-cmn 19484  df-psmet 20696  df-xmet 20697  df-met 20698  df-bl 20699  df-mopn 20700  df-fbas 20701  df-fg 20702  df-cnfld 20705  df-top 22150  df-topon 22167  df-topsp 22189  df-bases 22203  df-cld 22277  df-ntr 22278  df-cls 22279  df-nei 22356  df-lp 22394  df-perf 22395  df-cn 22485  df-cnp 22486  df-haus 22573  df-tx 22820  df-hmeo 23013  df-fil 23104  df-fm 23196  df-flim 23197  df-flf 23198  df-xms 23580  df-ms 23581  df-tms 23582  df-cncf 24148  df-limc 25137  df-dv 25138
This theorem is referenced by:  dirkertrigeq  44030
  Copyright terms: Public domain W3C validator