dirkertrigeqlem2

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

	Ref	Expression
Hypotheses	dirkertrigeqlem2.a	$⊢ φ \to A \in ℝ$
	dirkertrigeqlem2.sinne0	$⊢ φ \to \sin A \neq 0$
	dirkertrigeqlem2.n	$⊢ φ \to N \in ℕ$
Assertion	dirkertrigeqlem2	$⊢ φ \to \frac{(\frac{1}{2}) + \sum_{n = 1}^{N} \cos n A}{π} = \frac{\sin (N + (\frac{1}{2})) A}{2 π \sin (\frac{A}{2})}$

Proof

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

Metamath Proof Explorer

Theorem dirkertrigeqlem2

Proof