This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dirkertrigeqlem2

Description: Trigonomic equality lemma for the Dirichlet Kernel trigonomic equality. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dirkertrigeqlem2.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
dirkertrigeqlem2.sinne0 ⊢ ( 𝜑 → ( sin ‘ 𝐴 ) ≠ 0 )
dirkertrigeqlem2.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion dirkertrigeqlem2 ( 𝜑 → ( ( ( 1 / 2 ) + Σ 𝑛 ∈ ( 1 ... 𝑁 ) ( cos ‘ ( 𝑛 · 𝐴 ) ) ) / π ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝐴 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝐴 / 2 ) ) ) ) )

Proof

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