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 ) ) ) ) )