Theorem dirkertrigeqlem3 31723

Description: Trigonometric equality lemma for the Dirichlet Kernel trigonometric equality. Here we handle the case for an angle that's an odd multiple of pi. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
dirkertrigeqlem3.n	|- ( ph -> N e. NN )
dirkertrigeqlem3.k	|- ( ph -> K e. ZZ )
dirkertrigeqlem3.a	|- A = ( ( ( 2 x. K ) + 1 ) x. pi )

Assertion

Ref	Expression
dirkertrigeqlem3	|- ( ph -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) / pi ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( ( 2 x. pi ) x. ( sin ` ( A / 2 ) ) ) ) )

Distinct variable groups:   n, N   ph, n

Allowed substitution hints:   A( n)   K( n)

Proof of Theorem dirkertrigeqlem3

Step	Hyp	Ref	Expression
1		dirkertrigeqlem3.a	. . . . . . . . . . . . . 14 |- A = ( ( ( 2 x. K ) + 1 ) x. pi )
2	1	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. ( 1 ... N ) ) -> A = ( ( ( 2 x. K ) + 1 ) x. pi ) )
3	2	oveq2d 6311	. . . . . . . . . . . 12 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( n x. A ) = ( n x. ( ( ( 2 x. K ) + 1 ) x. pi ) ) )
4		elfzelz 11700	. . . . . . . . . . . . . . 15 |- ( n e. ( 1 ... N ) -> n e. ZZ )
5	4	zcnd 10979	. . . . . . . . . . . . . 14 |- ( n e. ( 1 ... N ) -> n e. CC )
6	5	adantl 466	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. ( 1 ... N ) ) -> n e. CC )
7		2cn 10618	. . . . . . . . . . . . . . . . 17 |- 2 e. CC
8	7	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ n e. ( 1 ... N ) ) -> 2 e. CC )
9		dirkertrigeqlem3.k	. . . . . . . . . . . . . . . . . 18 |- ( ph -> K e. ZZ )
10	9	zcnd 10979	. . . . . . . . . . . . . . . . 17 |- ( ph -> K e. CC )
11	10	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ n e. ( 1 ... N ) ) -> K e. CC )
12	8, 11	mulcld 9628	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( 2 x. K ) e. CC )
13		ax-1cn 9562	. . . . . . . . . . . . . . . 16 |- 1 e. CC
14	13	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. ( 1 ... N ) ) -> 1 e. CC )
15	12, 14	addcld 9627	. . . . . . . . . . . . . 14 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 2 x. K ) + 1 ) e. CC )
16		pire 22718	. . . . . . . . . . . . . . . 16 |- pi e. RR
17	16	recni 9620	. . . . . . . . . . . . . . 15 |- pi e. CC
18	17	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ n e. ( 1 ... N ) ) -> pi e. CC )
19	15, 18	mulcld 9628	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( 2 x. K ) + 1 ) x. pi ) e. CC )
20	6, 19	mulcomd 9629	. . . . . . . . . . . 12 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( n x. ( ( ( 2 x. K ) + 1 ) x. pi ) ) = ( ( ( ( 2 x. K ) + 1 ) x. pi ) x. n ) )
21	15, 18, 6	mulassd 9631	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( ( 2 x. K ) + 1 ) x. pi ) x. n ) = ( ( ( 2 x. K ) + 1 ) x. ( pi x. n ) ) )
22	18, 6	mulcld 9628	. . . . . . . . . . . . . 14 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( pi x. n ) e. CC )
23	12, 14, 22	adddird 9633	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( 2 x. K ) + 1 ) x. ( pi x. n ) ) = ( ( ( 2 x. K ) x. ( pi x. n ) ) + ( 1 x. ( pi x. n ) ) ) )
24	12, 22	mulcld 9628	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 2 x. K ) x. ( pi x. n ) ) e. CC )
25	14, 22	mulcld 9628	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( 1 x. ( pi x. n ) ) e. CC )
26	24, 25	addcomd 9793	. . . . . . . . . . . . . 14 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( 2 x. K ) x. ( pi x. n ) ) + ( 1 x. ( pi x. n ) ) ) = ( ( 1 x. ( pi x. n ) ) + ( ( 2 x. K ) x. ( pi x. n ) ) ) )
27	17	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( n e. ( 1 ... N ) -> pi e. CC )
28	27, 5	mulcld 9628	. . . . . . . . . . . . . . . . 17 |- ( n e. ( 1 ... N ) -> ( pi x. n ) e. CC )
29	28	mulid2d 9626	. . . . . . . . . . . . . . . 16 |- ( n e. ( 1 ... N ) -> ( 1 x. ( pi x. n ) ) = ( pi x. n ) )
30	29	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( 1 x. ( pi x. n ) ) = ( pi x. n ) )
31	8, 11, 18, 6	mul4d 9803	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 2 x. K ) x. ( pi x. n ) ) = ( ( 2 x. pi ) x. ( K x. n ) ) )
32	8, 18	mulcld 9628	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( 2 x. pi ) e. CC )
33	11, 6	mulcld 9628	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( K x. n ) e. CC )
34	32, 33	mulcomd 9629	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 2 x. pi ) x. ( K x. n ) ) = ( ( K x. n ) x. ( 2 x. pi ) ) )
35	31, 34	eqtrd 2508	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 2 x. K ) x. ( pi x. n ) ) = ( ( K x. n ) x. ( 2 x. pi ) ) )
36	30, 35	oveq12d 6313	. . . . . . . . . . . . . 14 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 1 x. ( pi x. n ) ) + ( ( 2 x. K ) x. ( pi x. n ) ) ) = ( ( pi x. n ) + ( ( K x. n ) x. ( 2 x. pi ) ) ) )
37	26, 36	eqtrd 2508	. . . . . . . . . . . . 13 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( 2 x. K ) x. ( pi x. n ) ) + ( 1 x. ( pi x. n ) ) ) = ( ( pi x. n ) + ( ( K x. n ) x. ( 2 x. pi ) ) ) )
38	21, 23, 37	3eqtrd 2512	. . . . . . . . . . . 12 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( ( 2 x. K ) + 1 ) x. pi ) x. n ) = ( ( pi x. n ) + ( ( K x. n ) x. ( 2 x. pi ) ) ) )
39	3, 20, 38	3eqtrd 2512	. . . . . . . . . . 11 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( n x. A ) = ( ( pi x. n ) + ( ( K x. n ) x. ( 2 x. pi ) ) ) )
40	39	fveq2d 5876	. . . . . . . . . 10 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( cos ` ( n x. A ) ) = ( cos ` ( ( pi x. n ) + ( ( K x. n ) x. ( 2 x. pi ) ) ) ) )
41	9	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ n e. ( 1 ... N ) ) -> K e. ZZ )
42	4	adantl 466	. . . . . . . . . . . 12 |- ( ( ph /\ n e. ( 1 ... N ) ) -> n e. ZZ )
43	41, 42	zmulcld 10984	. . . . . . . . . . 11 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( K x. n ) e. ZZ )
44		cosper 22741	. . . . . . . . . . 11 |- ( ( ( pi x. n ) e. CC /\ ( K x. n ) e. ZZ ) -> ( cos ` ( ( pi x. n ) + ( ( K x. n ) x. ( 2 x. pi ) ) ) ) = ( cos ` ( pi x. n ) ) )
45	22, 43, 44	syl2anc 661	. . . . . . . . . 10 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( cos ` ( ( pi x. n ) + ( ( K x. n ) x. ( 2 x. pi ) ) ) ) = ( cos ` ( pi x. n ) ) )
46	40, 45	eqtrd 2508	. . . . . . . . 9 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( cos ` ( n x. A ) ) = ( cos ` ( pi x. n ) ) )
47	46	ralrimiva 2881	. . . . . . . 8 |- ( ph -> A. n e. ( 1 ... N ) ( cos ` ( n x. A ) ) = ( cos ` ( pi x. n ) ) )
48	47	sumeq2d 13504	. . . . . . 7 |- ( ph -> sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) = sum_ n e. ( 1 ... N ) ( cos ` ( pi x. n ) ) )
49	48	oveq2d 6311	. . . . . 6 |- ( ph -> ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) = ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( pi x. n ) ) ) )
50	49	oveq1d 6310	. . . . 5 |- ( ph -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) / pi ) = ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( pi x. n ) ) ) / pi ) )
51	50	adantr 465	. . . 4 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) / pi ) = ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( pi x. n ) ) ) / pi ) )
52		dirkertrigeqlem3.n	. . . . . . . . . . . . . 14 |- ( ph -> N e. NN )
53	52	nncnd 10564	. . . . . . . . . . . . 13 |- ( ph -> N e. CC )
54	7	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> 2 e. CC )
55		2ne0 10640	. . . . . . . . . . . . . 14 |- 2 =/= 0
56	55	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> 2 =/= 0 )
57	53, 54, 56	divcan2d 10334	. . . . . . . . . . . 12 |- ( ph -> ( 2 x. ( N / 2 ) ) = N )
58	57	eqcomd 2475	. . . . . . . . . . 11 |- ( ph -> N = ( 2 x. ( N / 2 ) ) )
59	58	oveq2d 6311	. . . . . . . . . 10 |- ( ph -> ( 1 ... N ) = ( 1 ... ( 2 x. ( N / 2 ) ) ) )
60	59	sumeq1d 13503	. . . . . . . . 9 |- ( ph -> sum_ n e. ( 1 ... N ) ( cos ` ( pi x. n ) ) = sum_ n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) ( cos ` ( pi x. n ) ) )
61	60	adantr 465	. . . . . . . 8 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> sum_ n e. ( 1 ... N ) ( cos ` ( pi x. n ) ) = sum_ n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) ( cos ` ( pi x. n ) ) )
62	17	a1i 11	. . . . . . . . . . . . 13 |- ( n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) -> pi e. CC )
63		elfzelz 11700	. . . . . . . . . . . . . 14 |- ( n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) -> n e. ZZ )
64	63	zcnd 10979	. . . . . . . . . . . . 13 |- ( n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) -> n e. CC )
65	62, 64	mulcomd 9629	. . . . . . . . . . . 12 |- ( n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) -> ( pi x. n ) = ( n x. pi ) )
66	65	fveq2d 5876	. . . . . . . . . . 11 |- ( n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) -> ( cos ` ( pi x. n ) ) = ( cos ` ( n x. pi ) ) )
67	66	rgen 2827	. . . . . . . . . 10 |- A. n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) ( cos ` ( pi x. n ) ) = ( cos ` ( n x. pi ) )
68	67	a1i 11	. . . . . . . . 9 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> A. n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) ( cos ` ( pi x. n ) ) = ( cos ` ( n x. pi ) ) )
69	68	sumeq2d 13504	. . . . . . . 8 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> sum_ n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) ( cos ` ( pi x. n ) ) = sum_ n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) ( cos ` ( n x. pi ) ) )
70		simpr 461	. . . . . . . . . . . 12 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( N mod 2 ) = 0 )
71	52	nnred 10563	. . . . . . . . . . . . . 14 |- ( ph -> N e. RR )
72	71	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> N e. RR )
73		2rp 11237	. . . . . . . . . . . . . 14 |- 2 e. RR+
74	73	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> 2 e. RR+ )
75		mod0 11983	. . . . . . . . . . . . 13 |- ( ( N e. RR /\ 2 e. RR+ ) -> ( ( N mod 2 ) = 0 <-> ( N / 2 ) e. ZZ ) )
76	72, 74, 75	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( N mod 2 ) = 0 <-> ( N / 2 ) e. ZZ ) )
77	70, 76	mpbid 210	. . . . . . . . . . 11 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( N / 2 ) e. ZZ )
78		2re 10617	. . . . . . . . . . . . . 14 |- 2 e. RR
79	78	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> 2 e. RR )
80	52	nngt0d 10591	. . . . . . . . . . . . 13 |- ( ph -> 0 < N )
81		2pos 10639	. . . . . . . . . . . . . 14 |- 0 < 2
82	81	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> 0 < 2 )
83	71, 79, 80, 82	divgt0d 10493	. . . . . . . . . . . 12 |- ( ph -> 0 < ( N / 2 ) )
84	83	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> 0 < ( N / 2 ) )
85	77, 84	jca 532	. . . . . . . . . 10 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( N / 2 ) e. ZZ /\ 0 < ( N / 2 ) ) )
86		elnnz 10886	. . . . . . . . . 10 |- ( ( N / 2 ) e. NN <-> ( ( N / 2 ) e. ZZ /\ 0 < ( N / 2 ) ) )
87	85, 86	sylibr 212	. . . . . . . . 9 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( N / 2 ) e. NN )
88		dirkertrigeqlem1 31721	. . . . . . . . 9 |- ( ( N / 2 ) e. NN -> sum_ n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) ( cos ` ( n x. pi ) ) = 0 )
89	87, 88	syl 16	. . . . . . . 8 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> sum_ n e. ( 1 ... ( 2 x. ( N / 2 ) ) ) ( cos ` ( n x. pi ) ) = 0 )
90	61, 69, 89	3eqtrd 2512	. . . . . . 7 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> sum_ n e. ( 1 ... N ) ( cos ` ( pi x. n ) ) = 0 )
91	90	oveq2d 6311	. . . . . 6 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( pi x. n ) ) ) = ( ( 1 / 2 ) + 0 ) )
92	7, 55	reccli 10286	. . . . . . . 8 |- ( 1 / 2 ) e. CC
93	92	addid1i 9778	. . . . . . 7 |- ( ( 1 / 2 ) + 0 ) = ( 1 / 2 )
94	93	a1i 11	. . . . . 6 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( 1 / 2 ) + 0 ) = ( 1 / 2 ) )
95	91, 94	eqtrd 2508	. . . . 5 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( pi x. n ) ) ) = ( 1 / 2 ) )
96	95	oveq1d 6310	. . . 4 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( pi x. n ) ) ) / pi ) = ( ( 1 / 2 ) / pi ) )
97	7, 55	pm3.2i 455	. . . . . 6 |- ( 2 e. CC /\ 2 =/= 0 )
98		pipos 22720	. . . . . . . 8 |- 0 < pi
99		0re 9608	. . . . . . . . 9 |- 0 e. RR
100	99, 16	ltnei 9720	. . . . . . . 8 |- ( 0 < pi -> pi =/= 0 )
101	98, 100	ax-mp 5	. . . . . . 7 |- pi =/= 0
102	17, 101	pm3.2i 455	. . . . . 6 |- ( pi e. CC /\ pi =/= 0 )
103		divdiv1 10267	. . . . . 6 |- ( ( 1 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( pi e. CC /\ pi =/= 0 ) ) -> ( ( 1 / 2 ) / pi ) = ( 1 / ( 2 x. pi ) ) )
104	13, 97, 102, 103	mp3an 1324	. . . . 5 |- ( ( 1 / 2 ) / pi ) = ( 1 / ( 2 x. pi ) )
105	104	a1i 11	. . . 4 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( 1 / 2 ) / pi ) = ( 1 / ( 2 x. pi ) ) )
106	51, 96, 105	3eqtrd 2512	. . 3 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) / pi ) = ( 1 / ( 2 x. pi ) ) )
107	1	oveq2i 6306	. . . . . . . . . 10 |- ( ( N + ( 1 / 2 ) ) x. A ) = ( ( N + ( 1 / 2 ) ) x. ( ( ( 2 x. K ) + 1 ) x. pi ) )
108	107	a1i 11	. . . . . . . . 9 |- ( ph -> ( ( N + ( 1 / 2 ) ) x. A ) = ( ( N + ( 1 / 2 ) ) x. ( ( ( 2 x. K ) + 1 ) x. pi ) ) )
109	92	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> ( 1 / 2 ) e. CC )
110	53, 109	jca 532	. . . . . . . . . . . 12 |- ( ph -> ( N e. CC /\ ( 1 / 2 ) e. CC ) )
111		addcl 9586	. . . . . . . . . . . 12 |- ( ( N e. CC /\ ( 1 / 2 ) e. CC ) -> ( N + ( 1 / 2 ) ) e. CC )
112	110, 111	syl 16	. . . . . . . . . . 11 |- ( ph -> ( N + ( 1 / 2 ) ) e. CC )
113	54, 10	jca 532	. . . . . . . . . . . . 13 |- ( ph -> ( 2 e. CC /\ K e. CC ) )
114		mulcl 9588	. . . . . . . . . . . . 13 |- ( ( 2 e. CC /\ K e. CC ) -> ( 2 x. K ) e. CC )
115	113, 114	syl 16	. . . . . . . . . . . 12 |- ( ph -> ( 2 x. K ) e. CC )
116		peano2cn 9763	. . . . . . . . . . . 12 |- ( ( 2 x. K ) e. CC -> ( ( 2 x. K ) + 1 ) e. CC )
117	115, 116	syl 16	. . . . . . . . . . 11 |- ( ph -> ( ( 2 x. K ) + 1 ) e. CC )
118	17	a1i 11	. . . . . . . . . . 11 |- ( ph -> pi e. CC )
119	112, 117, 118	mulassd 9631	. . . . . . . . . 10 |- ( ph -> ( ( ( N + ( 1 / 2 ) ) x. ( ( 2 x. K ) + 1 ) ) x. pi ) = ( ( N + ( 1 / 2 ) ) x. ( ( ( 2 x. K ) + 1 ) x. pi ) ) )
120	119	eqcomd 2475	. . . . . . . . 9 |- ( ph -> ( ( N + ( 1 / 2 ) ) x. ( ( ( 2 x. K ) + 1 ) x. pi ) ) = ( ( ( N + ( 1 / 2 ) ) x. ( ( 2 x. K ) + 1 ) ) x. pi ) )
121	13	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> 1 e. CC )
122	53, 109, 115, 121	muladdd 10026	. . . . . . . . . . . . 13 |- ( ph -> ( ( N + ( 1 / 2 ) ) x. ( ( 2 x. K ) + 1 ) ) = ( ( ( N x. ( 2 x. K ) ) + ( 1 x. ( 1 / 2 ) ) ) + ( ( N x. 1 ) + ( ( 2 x. K ) x. ( 1 / 2 ) ) ) ) )
123	53, 54, 10	mul12d 9800	. . . . . . . . . . . . . . 15 |- ( ph -> ( N x. ( 2 x. K ) ) = ( 2 x. ( N x. K ) ) )
124	109	mulid2d 9626	. . . . . . . . . . . . . . 15 |- ( ph -> ( 1 x. ( 1 / 2 ) ) = ( 1 / 2 ) )
125	123, 124	oveq12d 6313	. . . . . . . . . . . . . 14 |- ( ph -> ( ( N x. ( 2 x. K ) ) + ( 1 x. ( 1 / 2 ) ) ) = ( ( 2 x. ( N x. K ) ) + ( 1 / 2 ) ) )
126	53	mulid1d 9625	. . . . . . . . . . . . . . 15 |- ( ph -> ( N x. 1 ) = N )
127	54, 10	mulcomd 9629	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( 2 x. K ) = ( K x. 2 ) )
128	127	oveq1d 6310	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( 2 x. K ) x. ( 1 / 2 ) ) = ( ( K x. 2 ) x. ( 1 / 2 ) ) )
129	10, 54, 109	mulassd 9631	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( K x. 2 ) x. ( 1 / 2 ) ) = ( K x. ( 2 x. ( 1 / 2 ) ) ) )
130	7, 55	recidi 10287	. . . . . . . . . . . . . . . . . . 19 |- ( 2 x. ( 1 / 2 ) ) = 1
131	130	oveq2i 6306	. . . . . . . . . . . . . . . . . 18 |- ( K x. ( 2 x. ( 1 / 2 ) ) ) = ( K x. 1 )
132	131	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( K x. ( 2 x. ( 1 / 2 ) ) ) = ( K x. 1 ) )
133	10	mulid1d 9625	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( K x. 1 ) = K )
134	132, 133	eqtrd 2508	. . . . . . . . . . . . . . . 16 |- ( ph -> ( K x. ( 2 x. ( 1 / 2 ) ) ) = K )
135	128, 129, 134	3eqtrd 2512	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( 2 x. K ) x. ( 1 / 2 ) ) = K )
136	126, 135	oveq12d 6313	. . . . . . . . . . . . . 14 |- ( ph -> ( ( N x. 1 ) + ( ( 2 x. K ) x. ( 1 / 2 ) ) ) = ( N + K ) )
137	125, 136	oveq12d 6313	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( N x. ( 2 x. K ) ) + ( 1 x. ( 1 / 2 ) ) ) + ( ( N x. 1 ) + ( ( 2 x. K ) x. ( 1 / 2 ) ) ) ) = ( ( ( 2 x. ( N x. K ) ) + ( 1 / 2 ) ) + ( N + K ) ) )
138	53, 10	jca 532	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( N e. CC /\ K e. CC ) )
139		mulcl 9588	. . . . . . . . . . . . . . . . 17 |- ( ( N e. CC /\ K e. CC ) -> ( N x. K ) e. CC )
140	138, 139	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> ( N x. K ) e. CC )
141	54, 140	jca 532	. . . . . . . . . . . . . . 15 |- ( ph -> ( 2 e. CC /\ ( N x. K ) e. CC ) )
142		mulcl 9588	. . . . . . . . . . . . . . 15 |- ( ( 2 e. CC /\ ( N x. K ) e. CC ) -> ( 2 x. ( N x. K ) ) e. CC )
143	141, 142	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> ( 2 x. ( N x. K ) ) e. CC )
144	53, 10	addcld 9627	. . . . . . . . . . . . . 14 |- ( ph -> ( N + K ) e. CC )
145	143, 109, 144	addassd 9630	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( 2 x. ( N x. K ) ) + ( 1 / 2 ) ) + ( N + K ) ) = ( ( 2 x. ( N x. K ) ) + ( ( 1 / 2 ) + ( N + K ) ) ) )
146	122, 137, 145	3eqtrd 2512	. . . . . . . . . . . 12 |- ( ph -> ( ( N + ( 1 / 2 ) ) x. ( ( 2 x. K ) + 1 ) ) = ( ( 2 x. ( N x. K ) ) + ( ( 1 / 2 ) + ( N + K ) ) ) )
147	109, 144	addcld 9627	. . . . . . . . . . . . 13 |- ( ph -> ( ( 1 / 2 ) + ( N + K ) ) e. CC )
148	143, 147	addcomd 9793	. . . . . . . . . . . 12 |- ( ph -> ( ( 2 x. ( N x. K ) ) + ( ( 1 / 2 ) + ( N + K ) ) ) = ( ( ( 1 / 2 ) + ( N + K ) ) + ( 2 x. ( N x. K ) ) ) )
149	54, 140	mulcomd 9629	. . . . . . . . . . . . 13 |- ( ph -> ( 2 x. ( N x. K ) ) = ( ( N x. K ) x. 2 ) )
150	149	oveq2d 6311	. . . . . . . . . . . 12 |- ( ph -> ( ( ( 1 / 2 ) + ( N + K ) ) + ( 2 x. ( N x. K ) ) ) = ( ( ( 1 / 2 ) + ( N + K ) ) + ( ( N x. K ) x. 2 ) ) )
151	146, 148, 150	3eqtrd 2512	. . . . . . . . . . 11 |- ( ph -> ( ( N + ( 1 / 2 ) ) x. ( ( 2 x. K ) + 1 ) ) = ( ( ( 1 / 2 ) + ( N + K ) ) + ( ( N x. K ) x. 2 ) ) )
152	151	oveq1d 6310	. . . . . . . . . 10 |- ( ph -> ( ( ( N + ( 1 / 2 ) ) x. ( ( 2 x. K ) + 1 ) ) x. pi ) = ( ( ( ( 1 / 2 ) + ( N + K ) ) + ( ( N x. K ) x. 2 ) ) x. pi ) )
153	149, 143	eqeltrrd 2556	. . . . . . . . . . 11 |- ( ph -> ( ( N x. K ) x. 2 ) e. CC )
154	147, 153, 118	adddird 9633	. . . . . . . . . 10 |- ( ph -> ( ( ( ( 1 / 2 ) + ( N + K ) ) + ( ( N x. K ) x. 2 ) ) x. pi ) = ( ( ( ( 1 / 2 ) + ( N + K ) ) x. pi ) + ( ( ( N x. K ) x. 2 ) x. pi ) ) )
155	140, 54, 118	mulassd 9631	. . . . . . . . . . 11 |- ( ph -> ( ( ( N x. K ) x. 2 ) x. pi ) = ( ( N x. K ) x. ( 2 x. pi ) ) )
156	155	oveq2d 6311	. . . . . . . . . 10 |- ( ph -> ( ( ( ( 1 / 2 ) + ( N + K ) ) x. pi ) + ( ( ( N x. K ) x. 2 ) x. pi ) ) = ( ( ( ( 1 / 2 ) + ( N + K ) ) x. pi ) + ( ( N x. K ) x. ( 2 x. pi ) ) ) )
157	152, 154, 156	3eqtrd 2512	. . . . . . . . 9 |- ( ph -> ( ( ( N + ( 1 / 2 ) ) x. ( ( 2 x. K ) + 1 ) ) x. pi ) = ( ( ( ( 1 / 2 ) + ( N + K ) ) x. pi ) + ( ( N x. K ) x. ( 2 x. pi ) ) ) )
158	108, 120, 157	3eqtrd 2512	. . . . . . . 8 |- ( ph -> ( ( N + ( 1 / 2 ) ) x. A ) = ( ( ( ( 1 / 2 ) + ( N + K ) ) x. pi ) + ( ( N x. K ) x. ( 2 x. pi ) ) ) )
159	158	fveq2d 5876	. . . . . . 7 |- ( ph -> ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) = ( sin ` ( ( ( ( 1 / 2 ) + ( N + K ) ) x. pi ) + ( ( N x. K ) x. ( 2 x. pi ) ) ) ) )
160	147, 118	mulcld 9628	. . . . . . . 8 |- ( ph -> ( ( ( 1 / 2 ) + ( N + K ) ) x. pi ) e. CC )
161	52	nnzd 10977	. . . . . . . . 9 |- ( ph -> N e. ZZ )
162	161, 9	zmulcld 10984	. . . . . . . 8 |- ( ph -> ( N x. K ) e. ZZ )
163		sinper 22740	. . . . . . . 8 |- ( ( ( ( ( 1 / 2 ) + ( N + K ) ) x. pi ) e. CC /\ ( N x. K ) e. ZZ ) -> ( sin ` ( ( ( ( 1 / 2 ) + ( N + K ) ) x. pi ) + ( ( N x. K ) x. ( 2 x. pi ) ) ) ) = ( sin ` ( ( ( 1 / 2 ) + ( N + K ) ) x. pi ) ) )
164	160, 162, 163	syl2anc 661	. . . . . . 7 |- ( ph -> ( sin ` ( ( ( ( 1 / 2 ) + ( N + K ) ) x. pi ) + ( ( N x. K ) x. ( 2 x. pi ) ) ) ) = ( sin ` ( ( ( 1 / 2 ) + ( N + K ) ) x. pi ) ) )
165	109, 144	addcomd 9793	. . . . . . . . . 10 |- ( ph -> ( ( 1 / 2 ) + ( N + K ) ) = ( ( N + K ) + ( 1 / 2 ) ) )
166	53, 10, 109	addassd 9630	. . . . . . . . . 10 |- ( ph -> ( ( N + K ) + ( 1 / 2 ) ) = ( N + ( K + ( 1 / 2 ) ) ) )
167	10, 109	addcld 9627	. . . . . . . . . . 11 |- ( ph -> ( K + ( 1 / 2 ) ) e. CC )
168	53, 167	addcomd 9793	. . . . . . . . . 10 |- ( ph -> ( N + ( K + ( 1 / 2 ) ) ) = ( ( K + ( 1 / 2 ) ) + N ) )
169	165, 166, 168	3eqtrd 2512	. . . . . . . . 9 |- ( ph -> ( ( 1 / 2 ) + ( N + K ) ) = ( ( K + ( 1 / 2 ) ) + N ) )
170	169	oveq1d 6310	. . . . . . . 8 |- ( ph -> ( ( ( 1 / 2 ) + ( N + K ) ) x. pi ) = ( ( ( K + ( 1 / 2 ) ) + N ) x. pi ) )
171	170	fveq2d 5876	. . . . . . 7 |- ( ph -> ( sin ` ( ( ( 1 / 2 ) + ( N + K ) ) x. pi ) ) = ( sin ` ( ( ( K + ( 1 / 2 ) ) + N ) x. pi ) ) )
172	159, 164, 171	3eqtrd 2512	. . . . . 6 |- ( ph -> ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) = ( sin ` ( ( ( K + ( 1 / 2 ) ) + N ) x. pi ) ) )
173	1	a1i 11	. . . . . . . . . 10 |- ( ph -> A = ( ( ( 2 x. K ) + 1 ) x. pi ) )
174	173	oveq1d 6310	. . . . . . . . 9 |- ( ph -> ( A / 2 ) = ( ( ( ( 2 x. K ) + 1 ) x. pi ) / 2 ) )
175	117, 118, 54, 56	div23d 10369	. . . . . . . . 9 |- ( ph -> ( ( ( ( 2 x. K ) + 1 ) x. pi ) / 2 ) = ( ( ( ( 2 x. K ) + 1 ) / 2 ) x. pi ) )
176	115, 121, 54, 56	divdird 10370	. . . . . . . . . . 11 |- ( ph -> ( ( ( 2 x. K ) + 1 ) / 2 ) = ( ( ( 2 x. K ) / 2 ) + ( 1 / 2 ) ) )
177	10, 54, 56	divcan3d 10337	. . . . . . . . . . . 12 |- ( ph -> ( ( 2 x. K ) / 2 ) = K )
178	177	oveq1d 6310	. . . . . . . . . . 11 |- ( ph -> ( ( ( 2 x. K ) / 2 ) + ( 1 / 2 ) ) = ( K + ( 1 / 2 ) ) )
179	176, 178	eqtrd 2508	. . . . . . . . . 10 |- ( ph -> ( ( ( 2 x. K ) + 1 ) / 2 ) = ( K + ( 1 / 2 ) ) )
180	179	oveq1d 6310	. . . . . . . . 9 |- ( ph -> ( ( ( ( 2 x. K ) + 1 ) / 2 ) x. pi ) = ( ( K + ( 1 / 2 ) ) x. pi ) )
181	174, 175, 180	3eqtrd 2512	. . . . . . . 8 |- ( ph -> ( A / 2 ) = ( ( K + ( 1 / 2 ) ) x. pi ) )
182	181	fveq2d 5876	. . . . . . 7 |- ( ph -> ( sin ` ( A / 2 ) ) = ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) )
183	182	oveq2d 6311	. . . . . 6 |- ( ph -> ( ( 2 x. pi ) x. ( sin ` ( A / 2 ) ) ) = ( ( 2 x. pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) )
184	172, 183	oveq12d 6313	. . . . 5 |- ( ph -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( ( 2 x. pi ) x. ( sin ` ( A / 2 ) ) ) ) = ( ( sin ` ( ( ( K + ( 1 / 2 ) ) + N ) x. pi ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) ) )
185	184	adantr 465	. . . 4 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( ( 2 x. pi ) x. ( sin ` ( A / 2 ) ) ) ) = ( ( sin ` ( ( ( K + ( 1 / 2 ) ) + N ) x. pi ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) ) )
186	167, 53, 118	adddird 9633	. . . . . . 7 |- ( ph -> ( ( ( K + ( 1 / 2 ) ) + N ) x. pi ) = ( ( ( K + ( 1 / 2 ) ) x. pi ) + ( N x. pi ) ) )
187	186	fveq2d 5876	. . . . . 6 |- ( ph -> ( sin ` ( ( ( K + ( 1 / 2 ) ) + N ) x. pi ) ) = ( sin ` ( ( ( K + ( 1 / 2 ) ) x. pi ) + ( N x. pi ) ) ) )
188	187	oveq1d 6310	. . . . 5 |- ( ph -> ( ( sin ` ( ( ( K + ( 1 / 2 ) ) + N ) x. pi ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) ) = ( ( sin ` ( ( ( K + ( 1 / 2 ) ) x. pi ) + ( N x. pi ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) ) )
189	188	adantr 465	. . . 4 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( sin ` ( ( ( K + ( 1 / 2 ) ) + N ) x. pi ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) ) = ( ( sin ` ( ( ( K + ( 1 / 2 ) ) x. pi ) + ( N x. pi ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) ) )
190		eqcom 2476	. . . . . . . . . . . . . . . 16 |- ( ( 2 x. ( N / 2 ) ) = N <-> N = ( 2 x. ( N / 2 ) ) )
191	190	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( 2 x. ( N / 2 ) ) = N <-> N = ( 2 x. ( N / 2 ) ) ) )
192		halfcl 10776	. . . . . . . . . . . . . . . . . . 19 |- ( N e. CC -> ( N / 2 ) e. CC )
193	53, 192	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( N / 2 ) e. CC )
194	54, 193	jca 532	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( 2 e. CC /\ ( N / 2 ) e. CC ) )
195		mulcom 9590	. . . . . . . . . . . . . . . . 17 |- ( ( 2 e. CC /\ ( N / 2 ) e. CC ) -> ( 2 x. ( N / 2 ) ) = ( ( N / 2 ) x. 2 ) )
196	194, 195	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 2 x. ( N / 2 ) ) = ( ( N / 2 ) x. 2 ) )
197		eqeq2 2482	. . . . . . . . . . . . . . . 16 |- ( ( 2 x. ( N / 2 ) ) = ( ( N / 2 ) x. 2 ) -> ( N = ( 2 x. ( N / 2 ) ) <-> N = ( ( N / 2 ) x. 2 ) ) )
198	196, 197	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> ( N = ( 2 x. ( N / 2 ) ) <-> N = ( ( N / 2 ) x. 2 ) ) )
199	191, 198	bitrd 253	. . . . . . . . . . . . . 14 |- ( ph -> ( ( 2 x. ( N / 2 ) ) = N <-> N = ( ( N / 2 ) x. 2 ) ) )
200	199	pm5.74i 245	. . . . . . . . . . . . 13 |- ( ( ph -> ( 2 x. ( N / 2 ) ) = N ) <-> ( ph -> N = ( ( N / 2 ) x. 2 ) ) )
201	57, 200	mpbi 208	. . . . . . . . . . . 12 |- ( ph -> N = ( ( N / 2 ) x. 2 ) )
202	201	oveq1d 6310	. . . . . . . . . . 11 |- ( ph -> ( N x. pi ) = ( ( ( N / 2 ) x. 2 ) x. pi ) )
203	193, 54, 118	mulassd 9631	. . . . . . . . . . 11 |- ( ph -> ( ( ( N / 2 ) x. 2 ) x. pi ) = ( ( N / 2 ) x. ( 2 x. pi ) ) )
204	202, 203	eqtrd 2508	. . . . . . . . . 10 |- ( ph -> ( N x. pi ) = ( ( N / 2 ) x. ( 2 x. pi ) ) )
205	204	oveq2d 6311	. . . . . . . . 9 |- ( ph -> ( ( ( K + ( 1 / 2 ) ) x. pi ) + ( N x. pi ) ) = ( ( ( K + ( 1 / 2 ) ) x. pi ) + ( ( N / 2 ) x. ( 2 x. pi ) ) ) )
206	205	fveq2d 5876	. . . . . . . 8 |- ( ph -> ( sin ` ( ( ( K + ( 1 / 2 ) ) x. pi ) + ( N x. pi ) ) ) = ( sin ` ( ( ( K + ( 1 / 2 ) ) x. pi ) + ( ( N / 2 ) x. ( 2 x. pi ) ) ) ) )
207	206	adantr 465	. . . . . . 7 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( sin ` ( ( ( K + ( 1 / 2 ) ) x. pi ) + ( N x. pi ) ) ) = ( sin ` ( ( ( K + ( 1 / 2 ) ) x. pi ) + ( ( N / 2 ) x. ( 2 x. pi ) ) ) ) )
208	10	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> K e. CC )
209	13	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> 1 e. CC )
210	209	halfcld 10795	. . . . . . . . . 10 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( 1 / 2 ) e. CC )
211	208, 210	addcld 9627	. . . . . . . . 9 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( K + ( 1 / 2 ) ) e. CC )
212	17	a1i 11	. . . . . . . . 9 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> pi e. CC )
213	211, 212	mulcld 9628	. . . . . . . 8 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( K + ( 1 / 2 ) ) x. pi ) e. CC )
214		sinper 22740	. . . . . . . 8 |- ( ( ( ( K + ( 1 / 2 ) ) x. pi ) e. CC /\ ( N / 2 ) e. ZZ ) -> ( sin ` ( ( ( K + ( 1 / 2 ) ) x. pi ) + ( ( N / 2 ) x. ( 2 x. pi ) ) ) ) = ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) )
215	213, 77, 214	syl2anc 661	. . . . . . 7 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( sin ` ( ( ( K + ( 1 / 2 ) ) x. pi ) + ( ( N / 2 ) x. ( 2 x. pi ) ) ) ) = ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) )
216	207, 215	eqtrd 2508	. . . . . 6 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( sin ` ( ( ( K + ( 1 / 2 ) ) x. pi ) + ( N x. pi ) ) ) = ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) )
217	54, 118	mulcld 9628	. . . . . . . 8 |- ( ph -> ( 2 x. pi ) e. CC )
218	167, 118	mulcld 9628	. . . . . . . . 9 |- ( ph -> ( ( K + ( 1 / 2 ) ) x. pi ) e. CC )
219	218	sincld 13743	. . . . . . . 8 |- ( ph -> ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) e. CC )
220	217, 219	mulcomd 9629	. . . . . . 7 |- ( ph -> ( ( 2 x. pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) = ( ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) x. ( 2 x. pi ) ) )
221	220	adantr 465	. . . . . 6 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( 2 x. pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) = ( ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) x. ( 2 x. pi ) ) )
222	216, 221	oveq12d 6313	. . . . 5 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( sin ` ( ( ( K + ( 1 / 2 ) ) x. pi ) + ( N x. pi ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) ) = ( ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) / ( ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) x. ( 2 x. pi ) ) ) )
223	101	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> pi =/= 0 )
224	167, 118, 223	divcan4d 10338	. . . . . . . . . . . 12 |- ( ph -> ( ( ( K + ( 1 / 2 ) ) x. pi ) / pi ) = ( K + ( 1 / 2 ) ) )
225	9	zred 10978	. . . . . . . . . . . . . 14 |- ( ph -> K e. RR )
226	73	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> 2 e. RR+ )
227	226	rpreccld 11278	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 / 2 ) e. RR+ )
228	225, 227	ltaddrpd 11297	. . . . . . . . . . . . 13 |- ( ph -> K < ( K + ( 1 / 2 ) ) )
229		1re 9607	. . . . . . . . . . . . . . . 16 |- 1 e. RR
230	229	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> 1 e. RR )
231	230	rehalfcld 10797	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 / 2 ) e. RR )
232		halflt1 10769	. . . . . . . . . . . . . . 15 |- ( 1 / 2 ) < 1
233	232	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 / 2 ) < 1 )
234	231, 230, 225, 233	ltadd2dd 9752	. . . . . . . . . . . . 13 |- ( ph -> ( K + ( 1 / 2 ) ) < ( K + 1 ) )
235		btwnnz 10949	. . . . . . . . . . . . 13 |- ( ( K e. ZZ /\ K < ( K + ( 1 / 2 ) ) /\ ( K + ( 1 / 2 ) ) < ( K + 1 ) ) -> -. ( K + ( 1 / 2 ) ) e. ZZ )
236	9, 228, 234, 235	syl3anc 1228	. . . . . . . . . . . 12 |- ( ph -> -. ( K + ( 1 / 2 ) ) e. ZZ )
237	224, 236	eqneltrd 2576	. . . . . . . . . . 11 |- ( ph -> -. ( ( ( K + ( 1 / 2 ) ) x. pi ) / pi ) e. ZZ )
238		sineq0 22780	. . . . . . . . . . . 12 |- ( ( ( K + ( 1 / 2 ) ) x. pi ) e. CC -> ( ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) = 0 <-> ( ( ( K + ( 1 / 2 ) ) x. pi ) / pi ) e. ZZ ) )
239	218, 238	syl 16	. . . . . . . . . . 11 |- ( ph -> ( ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) = 0 <-> ( ( ( K + ( 1 / 2 ) ) x. pi ) / pi ) e. ZZ ) )
240	237, 239	mtbird 301	. . . . . . . . . 10 |- ( ph -> -. ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) = 0 )
241	240	neqned 2670	. . . . . . . . 9 |- ( ph -> ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) =/= 0 )
242	54, 118, 56, 223	mulne0d 10213	. . . . . . . . 9 |- ( ph -> ( 2 x. pi ) =/= 0 )
243	219, 219, 217, 241, 242	divdiv1d 10363	. . . . . . . 8 |- ( ph -> ( ( ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) / ( 2 x. pi ) ) = ( ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) / ( ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) x. ( 2 x. pi ) ) ) )
244	243	eqcomd 2475	. . . . . . 7 |- ( ph -> ( ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) / ( ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) x. ( 2 x. pi ) ) ) = ( ( ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) / ( 2 x. pi ) ) )
245	219, 241	dividd 10330	. . . . . . . 8 |- ( ph -> ( ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) = 1 )
246	245	oveq1d 6310	. . . . . . 7 |- ( ph -> ( ( ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) / ( 2 x. pi ) ) = ( 1 / ( 2 x. pi ) ) )
247	244, 246	eqtrd 2508	. . . . . 6 |- ( ph -> ( ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) / ( ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) x. ( 2 x. pi ) ) ) = ( 1 / ( 2 x. pi ) ) )
248	247	adantr 465	. . . . 5 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) / ( ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) x. ( 2 x. pi ) ) ) = ( 1 / ( 2 x. pi ) ) )
249	222, 248	eqtrd 2508	. . . 4 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( sin ` ( ( ( K + ( 1 / 2 ) ) x. pi ) + ( N x. pi ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) ) = ( 1 / ( 2 x. pi ) ) )
250	185, 189, 249	3eqtrrd 2513	. . 3 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( 1 / ( 2 x. pi ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( ( 2 x. pi ) x. ( sin ` ( A / 2 ) ) ) ) )
251	106, 250	eqtrd 2508	. 2 |- ( ( ph /\ ( N mod 2 ) = 0 ) -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) / pi ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( ( 2 x. pi ) x. ( sin ` ( A / 2 ) ) ) ) )
252	50	adantr 465	. . 3 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) / pi ) = ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( pi x. n ) ) ) / pi ) )
253	161	adantr 465	. . . . . . . . 9 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> N e. ZZ )
254		simpr 461	. . . . . . . . . 10 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> -. ( N mod 2 ) = 0 )
255	254	neqned 2670	. . . . . . . . 9 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( N mod 2 ) =/= 0 )
256		oddfl 31359	. . . . . . . . 9 |- ( ( N e. ZZ /\ ( N mod 2 ) =/= 0 ) -> N = ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) )
257	253, 255, 256	syl2anc 661	. . . . . . . 8 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> N = ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) )
258	257	oveq2d 6311	. . . . . . 7 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( 1 ... N ) = ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) )
259	258	sumeq1d 13503	. . . . . 6 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> sum_ n e. ( 1 ... N ) ( cos ` ( pi x. n ) ) = sum_ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ( cos ` ( pi x. n ) ) )
260		oveq1 6302	. . . . . . . . . . . . . . . . . 18 |- ( N = 1 -> ( N / 2 ) = ( 1 / 2 ) )
261	260	fveq2d 5876	. . . . . . . . . . . . . . . . 17 |- ( N = 1 -> ( |_ ` ( N / 2 ) ) = ( |_ ` ( 1 / 2 ) ) )
262		halffl 31393	. . . . . . . . . . . . . . . . . 18 |- ( |_ ` ( 1 / 2 ) ) = 0
263	262	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( N = 1 -> ( |_ ` ( 1 / 2 ) ) = 0 )
264	261, 263	eqtrd 2508	. . . . . . . . . . . . . . . 16 |- ( N = 1 -> ( |_ ` ( N / 2 ) ) = 0 )
265	264	oveq2d 6311	. . . . . . . . . . . . . . 15 |- ( N = 1 -> ( 2 x. ( |_ ` ( N / 2 ) ) ) = ( 2 x. 0 ) )
266	7	mul01i 9781	. . . . . . . . . . . . . . . 16 |- ( 2 x. 0 ) = 0
267	266	a1i 11	. . . . . . . . . . . . . . 15 |- ( N = 1 -> ( 2 x. 0 ) = 0 )
268	265, 267	eqtrd 2508	. . . . . . . . . . . . . 14 |- ( N = 1 -> ( 2 x. ( |_ ` ( N / 2 ) ) ) = 0 )
269	268	oveq1d 6310	. . . . . . . . . . . . 13 |- ( N = 1 -> ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) = ( 0 + 1 ) )
270	13	addid2i 9779	. . . . . . . . . . . . . 14 |- ( 0 + 1 ) = 1
271	270	a1i 11	. . . . . . . . . . . . 13 |- ( N = 1 -> ( 0 + 1 ) = 1 )
272	269, 271	eqtrd 2508	. . . . . . . . . . . 12 |- ( N = 1 -> ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) = 1 )
273	272	oveq2d 6311	. . . . . . . . . . 11 |- ( N = 1 -> ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) = ( 1 ... 1 ) )
274	273	sumeq1d 13503	. . . . . . . . . 10 |- ( N = 1 -> sum_ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ( cos ` ( pi x. n ) ) = sum_ n e. ( 1 ... 1 ) ( cos ` ( pi x. n ) ) )
275		1z 10906	. . . . . . . . . . . 12 |- 1 e. ZZ
276		coscl 13740	. . . . . . . . . . . . 13 |- ( pi e. CC -> ( cos ` pi ) e. CC )
277	17, 276	ax-mp 5	. . . . . . . . . . . 12 |- ( cos ` pi ) e. CC
278		oveq2 6303	. . . . . . . . . . . . . . 15 |- ( n = 1 -> ( pi x. n ) = ( pi x. 1 ) )
279	17	mulid1i 9610	. . . . . . . . . . . . . . . 16 |- ( pi x. 1 ) = pi
280	279	a1i 11	. . . . . . . . . . . . . . 15 |- ( n = 1 -> ( pi x. 1 ) = pi )
281	278, 280	eqtrd 2508	. . . . . . . . . . . . . 14 |- ( n = 1 -> ( pi x. n ) = pi )
282	281	fveq2d 5876	. . . . . . . . . . . . 13 |- ( n = 1 -> ( cos ` ( pi x. n ) ) = ( cos ` pi ) )
283	282	fsum1 13544	. . . . . . . . . . . 12 |- ( ( 1 e. ZZ /\ ( cos ` pi ) e. CC ) -> sum_ n e. ( 1 ... 1 ) ( cos ` ( pi x. n ) ) = ( cos ` pi ) )
284	275, 277, 283	mp2an 672	. . . . . . . . . . 11 |- sum_ n e. ( 1 ... 1 ) ( cos ` ( pi x. n ) ) = ( cos ` pi )
285	284	a1i 11	. . . . . . . . . 10 |- ( N = 1 -> sum_ n e. ( 1 ... 1 ) ( cos ` ( pi x. n ) ) = ( cos ` pi ) )
286		cospi 22731	. . . . . . . . . . 11 |- ( cos ` pi ) = -u 1
287	286	a1i 11	. . . . . . . . . 10 |- ( N = 1 -> ( cos ` pi ) = -u 1 )
288	274, 285, 287	3eqtrd 2512	. . . . . . . . 9 |- ( N = 1 -> sum_ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ( cos ` ( pi x. n ) ) = -u 1 )
289	288	adantl 466	. . . . . . . 8 |- ( ( ph /\ N = 1 ) -> sum_ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ( cos ` ( pi x. n ) ) = -u 1 )
290		2nn 10705	. . . . . . . . . . . . 13 |- 2 e. NN
291	290	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ -. N = 1 ) -> 2 e. NN )
292	71	rehalfcld 10797	. . . . . . . . . . . . . . . 16 |- ( ph -> ( N / 2 ) e. RR )
293	292	flcld 11915	. . . . . . . . . . . . . . 15 |- ( ph -> ( |_ ` ( N / 2 ) ) e. ZZ )
294	293	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ -. N = 1 ) -> ( |_ ` ( N / 2 ) ) e. ZZ )
295	7, 55	dividi 10289	. . . . . . . . . . . . . . . . . 18 |- ( 2 / 2 ) = 1
296	295	eqcomi 2480	. . . . . . . . . . . . . . . . 17 |- 1 = ( 2 / 2 )
297	296	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ -. N = 1 ) -> 1 = ( 2 / 2 ) )
298	52	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ -. N = 1 ) -> N e. NN )
299		neqne 31339	. . . . . . . . . . . . . . . . . . 19 |- ( -. N = 1 -> N =/= 1 )
300	299	adantl 466	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ -. N = 1 ) -> N =/= 1 )
301		nnne1ge2 31381	. . . . . . . . . . . . . . . . . 18 |- ( ( N e. NN /\ N =/= 1 ) -> 2 <_ N )
302	298, 300, 301	syl2anc 661	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ -. N = 1 ) -> 2 <_ N )
303	78	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ -. N = 1 ) -> 2 e. RR )
304	71	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ -. N = 1 ) -> N e. RR )
305	73	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ -. N = 1 ) -> 2 e. RR+ )
306	303, 304, 305	lediv1d 11310	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ -. N = 1 ) -> ( 2 <_ N <-> ( 2 / 2 ) <_ ( N / 2 ) ) )
307	302, 306	mpbid 210	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ -. N = 1 ) -> ( 2 / 2 ) <_ ( N / 2 ) )
308	297, 307	eqbrtrd 4473	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. N = 1 ) -> 1 <_ ( N / 2 ) )
309	292	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ -. N = 1 ) -> ( N / 2 ) e. RR )
310	275	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ -. N = 1 ) -> 1 e. ZZ )
311		flge 11922	. . . . . . . . . . . . . . . 16 |- ( ( ( N / 2 ) e. RR /\ 1 e. ZZ ) -> ( 1 <_ ( N / 2 ) <-> 1 <_ ( |_ ` ( N / 2 ) ) ) )
312	309, 310, 311	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. N = 1 ) -> ( 1 <_ ( N / 2 ) <-> 1 <_ ( |_ ` ( N / 2 ) ) ) )
313	308, 312	mpbid 210	. . . . . . . . . . . . . 14 |- ( ( ph /\ -. N = 1 ) -> 1 <_ ( |_ ` ( N / 2 ) ) )
314	294, 313	jca 532	. . . . . . . . . . . . 13 |- ( ( ph /\ -. N = 1 ) -> ( ( |_ ` ( N / 2 ) ) e. ZZ /\ 1 <_ ( |_ ` ( N / 2 ) ) ) )
315		elnnz1 10902	. . . . . . . . . . . . 13 |- ( ( |_ ` ( N / 2 ) ) e. NN <-> ( ( |_ ` ( N / 2 ) ) e. ZZ /\ 1 <_ ( |_ ` ( N / 2 ) ) ) )
316	314, 315	sylibr 212	. . . . . . . . . . . 12 |- ( ( ph /\ -. N = 1 ) -> ( |_ ` ( N / 2 ) ) e. NN )
317	291, 316	nnmulcld 10595	. . . . . . . . . . 11 |- ( ( ph /\ -. N = 1 ) -> ( 2 x. ( |_ ` ( N / 2 ) ) ) e. NN )
318		nnuz 11129	. . . . . . . . . . . 12 |- NN = ( ZZ>= ` 1 )
319	318	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ -. N = 1 ) -> NN = ( ZZ>= ` 1 ) )
320	317, 319	eleqtrd 2557	. . . . . . . . . 10 |- ( ( ph /\ -. N = 1 ) -> ( 2 x. ( |_ ` ( N / 2 ) ) ) e. ( ZZ>= ` 1 ) )
321	17	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ph /\ -. N = 1 ) /\ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) -> pi e. CC )
322		elfzelz 11700	. . . . . . . . . . . . . 14 |- ( n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) -> n e. ZZ )
323	322	zcnd 10979	. . . . . . . . . . . . 13 |- ( n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) -> n e. CC )
324	323	adantl 466	. . . . . . . . . . . 12 |- ( ( ( ph /\ -. N = 1 ) /\ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) -> n e. CC )
325	321, 324	mulcld 9628	. . . . . . . . . . 11 |- ( ( ( ph /\ -. N = 1 ) /\ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) -> ( pi x. n ) e. CC )
326	325	coscld 13744	. . . . . . . . . 10 |- ( ( ( ph /\ -. N = 1 ) /\ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) -> ( cos ` ( pi x. n ) ) e. CC )
327		oveq2 6303	. . . . . . . . . . 11 |- ( n = ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) -> ( pi x. n ) = ( pi x. ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) )
328	327	fveq2d 5876	. . . . . . . . . 10 |- ( n = ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) -> ( cos ` ( pi x. n ) ) = ( cos ` ( pi x. ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) )
329	320, 326, 328	fsump1 13551	. . . . . . . . 9 |- ( ( ph /\ -. N = 1 ) -> sum_ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ( cos ` ( pi x. n ) ) = ( sum_ n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) ( cos ` ( pi x. n ) ) + ( cos ` ( pi x. ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) ) )
330	17	a1i 11	. . . . . . . . . . . . . . . 16 |- ( n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) -> pi e. CC )
331		elfzelz 11700	. . . . . . . . . . . . . . . . 17 |- ( n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) -> n e. ZZ )
332	331	zcnd 10979	. . . . . . . . . . . . . . . 16 |- ( n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) -> n e. CC )
333	330, 332	mulcomd 9629	. . . . . . . . . . . . . . 15 |- ( n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) -> ( pi x. n ) = ( n x. pi ) )
334	333	fveq2d 5876	. . . . . . . . . . . . . 14 |- ( n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) -> ( cos ` ( pi x. n ) ) = ( cos ` ( n x. pi ) ) )
335	334	rgen 2827	. . . . . . . . . . . . 13 |- A. n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) ( cos ` ( pi x. n ) ) = ( cos ` ( n x. pi ) )
336		sumeq2 13496	. . . . . . . . . . . . 13 |- ( A. n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) ( cos ` ( pi x. n ) ) = ( cos ` ( n x. pi ) ) -> sum_ n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) ( cos ` ( pi x. n ) ) = sum_ n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) ( cos ` ( n x. pi ) ) )
337	335, 336	ax-mp 5	. . . . . . . . . . . 12 |- sum_ n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) ( cos ` ( pi x. n ) ) = sum_ n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) ( cos ` ( n x. pi ) )
338	337	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ -. N = 1 ) -> sum_ n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) ( cos ` ( pi x. n ) ) = sum_ n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) ( cos ` ( n x. pi ) ) )
339		dirkertrigeqlem1 31721	. . . . . . . . . . . 12 |- ( ( |_ ` ( N / 2 ) ) e. NN -> sum_ n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) ( cos ` ( n x. pi ) ) = 0 )
340	316, 339	syl 16	. . . . . . . . . . 11 |- ( ( ph /\ -. N = 1 ) -> sum_ n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) ( cos ` ( n x. pi ) ) = 0 )
341	338, 340	eqtrd 2508	. . . . . . . . . 10 |- ( ( ph /\ -. N = 1 ) -> sum_ n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) ( cos ` ( pi x. n ) ) = 0 )
342	293	zcnd 10979	. . . . . . . . . . . . . . . 16 |- ( ph -> ( |_ ` ( N / 2 ) ) e. CC )
343	54, 342	mulcld 9628	. . . . . . . . . . . . . . 15 |- ( ph -> ( 2 x. ( |_ ` ( N / 2 ) ) ) e. CC )
344	118, 343, 121	adddid 9632	. . . . . . . . . . . . . 14 |- ( ph -> ( pi x. ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) = ( ( pi x. ( 2 x. ( |_ ` ( N / 2 ) ) ) ) + ( pi x. 1 ) ) )
345	118, 54, 342	mul13d 31361	. . . . . . . . . . . . . . 15 |- ( ph -> ( pi x. ( 2 x. ( |_ ` ( N / 2 ) ) ) ) = ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) )
346	279	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> ( pi x. 1 ) = pi )
347	345, 346	oveq12d 6313	. . . . . . . . . . . . . 14 |- ( ph -> ( ( pi x. ( 2 x. ( |_ ` ( N / 2 ) ) ) ) + ( pi x. 1 ) ) = ( ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) + pi ) )
348	342, 217	mulcld 9628	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) e. CC )
349	348, 118	addcomd 9793	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) + pi ) = ( pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) ) )
350	344, 347, 349	3eqtrd 2512	. . . . . . . . . . . . 13 |- ( ph -> ( pi x. ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) = ( pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) ) )
351	350	fveq2d 5876	. . . . . . . . . . . 12 |- ( ph -> ( cos ` ( pi x. ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) = ( cos ` ( pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) ) ) )
352		cosper 22741	. . . . . . . . . . . . 13 |- ( ( pi e. CC /\ ( |_ ` ( N / 2 ) ) e. ZZ ) -> ( cos ` ( pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) ) ) = ( cos ` pi ) )
353	118, 293, 352	syl2anc 661	. . . . . . . . . . . 12 |- ( ph -> ( cos ` ( pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) ) ) = ( cos ` pi ) )
354	286	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( cos ` pi ) = -u 1 )
355	351, 353, 354	3eqtrd 2512	. . . . . . . . . . 11 |- ( ph -> ( cos ` ( pi x. ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) = -u 1 )
356	355	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ -. N = 1 ) -> ( cos ` ( pi x. ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) = -u 1 )
357	341, 356	oveq12d 6313	. . . . . . . . 9 |- ( ( ph /\ -. N = 1 ) -> ( sum_ n e. ( 1 ... ( 2 x. ( |_ ` ( N / 2 ) ) ) ) ( cos ` ( pi x. n ) ) + ( cos ` ( pi x. ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ) ) = ( 0 + -u 1 ) )
358	286, 277	eqeltrri 2552	. . . . . . . . . . 11 |- -u 1 e. CC
359	358	addid2i 9779	. . . . . . . . . 10 |- ( 0 + -u 1 ) = -u 1
360	359	a1i 11	. . . . . . . . 9 |- ( ( ph /\ -. N = 1 ) -> ( 0 + -u 1 ) = -u 1 )
361	329, 357, 360	3eqtrd 2512	. . . . . . . 8 |- ( ( ph /\ -. N = 1 ) -> sum_ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ( cos ` ( pi x. n ) ) = -u 1 )
362	289, 361	pm2.61dan 789	. . . . . . 7 |- ( ph -> sum_ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ( cos ` ( pi x. n ) ) = -u 1 )
363	362	adantr 465	. . . . . 6 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> sum_ n e. ( 1 ... ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) ) ( cos ` ( pi x. n ) ) = -u 1 )
364	259, 363	eqtrd 2508	. . . . 5 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> sum_ n e. ( 1 ... N ) ( cos ` ( pi x. n ) ) = -u 1 )
365	364	oveq2d 6311	. . . 4 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( pi x. n ) ) ) = ( ( 1 / 2 ) + -u 1 ) )
366	365	oveq1d 6310	. . 3 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( pi x. n ) ) ) / pi ) = ( ( ( 1 / 2 ) + -u 1 ) / pi ) )
367	184, 188	eqtrd 2508	. . . . 5 |- ( ph -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( ( 2 x. pi ) x. ( sin ` ( A / 2 ) ) ) ) = ( ( sin ` ( ( ( K + ( 1 / 2 ) ) x. pi ) + ( N x. pi ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) ) )
368	367	adantr 465	. . . 4 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( ( 2 x. pi ) x. ( sin ` ( A / 2 ) ) ) ) = ( ( sin ` ( ( ( K + ( 1 / 2 ) ) x. pi ) + ( N x. pi ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) ) )
369	257	oveq1d 6310	. . . . . . . . 9 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( N x. pi ) = ( ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) x. pi ) )
370	343, 121, 118	adddird 9633	. . . . . . . . . . 11 |- ( ph -> ( ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) x. pi ) = ( ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. pi ) + ( 1 x. pi ) ) )
371	118	mulid2d 9626	. . . . . . . . . . . 12 |- ( ph -> ( 1 x. pi ) = pi )
372	371	oveq2d 6311	. . . . . . . . . . 11 |- ( ph -> ( ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. pi ) + ( 1 x. pi ) ) = ( ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. pi ) + pi ) )
373	343, 118	mulcld 9628	. . . . . . . . . . . 12 |- ( ph -> ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. pi ) e. CC )
374	373, 118	addcomd 9793	. . . . . . . . . . 11 |- ( ph -> ( ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. pi ) + pi ) = ( pi + ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. pi ) ) )
375	370, 372, 374	3eqtrd 2512	. . . . . . . . . 10 |- ( ph -> ( ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) x. pi ) = ( pi + ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. pi ) ) )
376	375	adantr 465	. . . . . . . . 9 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( ( 2 x. ( |_ ` ( N / 2 ) ) ) + 1 ) x. pi ) = ( pi + ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. pi ) ) )
377	54, 342	mulcomd 9629	. . . . . . . . . . . . 13 |- ( ph -> ( 2 x. ( |_ ` ( N / 2 ) ) ) = ( ( |_ ` ( N / 2 ) ) x. 2 ) )
378	377	oveq1d 6310	. . . . . . . . . . . 12 |- ( ph -> ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. pi ) = ( ( ( |_ ` ( N / 2 ) ) x. 2 ) x. pi ) )
379	342, 54, 118	mulassd 9631	. . . . . . . . . . . 12 |- ( ph -> ( ( ( |_ ` ( N / 2 ) ) x. 2 ) x. pi ) = ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) )
380	378, 379	eqtrd 2508	. . . . . . . . . . 11 |- ( ph -> ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. pi ) = ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) )
381	380	oveq2d 6311	. . . . . . . . . 10 |- ( ph -> ( pi + ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. pi ) ) = ( pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) ) )
382	381	adantr 465	. . . . . . . . 9 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( pi + ( ( 2 x. ( |_ ` ( N / 2 ) ) ) x. pi ) ) = ( pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) ) )
383	369, 376, 382	3eqtrd 2512	. . . . . . . 8 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( N x. pi ) = ( pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) ) )
384	383	oveq2d 6311	. . . . . . 7 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( ( K + ( 1 / 2 ) ) x. pi ) + ( N x. pi ) ) = ( ( ( K + ( 1 / 2 ) ) x. pi ) + ( pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) ) ) )
385	218	adantr 465	. . . . . . . . 9 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( K + ( 1 / 2 ) ) x. pi ) e. CC )
386	17	a1i 11	. . . . . . . . 9 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> pi e. CC )
387	348	adantr 465	. . . . . . . . 9 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) e. CC )
388	385, 386, 387	addassd 9630	. . . . . . . 8 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( ( ( K + ( 1 / 2 ) ) x. pi ) + pi ) + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) ) = ( ( ( K + ( 1 / 2 ) ) x. pi ) + ( pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) ) ) )
389	388	eqcomd 2475	. . . . . . 7 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( ( K + ( 1 / 2 ) ) x. pi ) + ( pi + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) ) ) = ( ( ( ( K + ( 1 / 2 ) ) x. pi ) + pi ) + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) ) )
390	384, 389	eqtrd 2508	. . . . . 6 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( ( K + ( 1 / 2 ) ) x. pi ) + ( N x. pi ) ) = ( ( ( ( K + ( 1 / 2 ) ) x. pi ) + pi ) + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) ) )
391	390	fveq2d 5876	. . . . 5 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( sin ` ( ( ( K + ( 1 / 2 ) ) x. pi ) + ( N x. pi ) ) ) = ( sin ` ( ( ( ( K + ( 1 / 2 ) ) x. pi ) + pi ) + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) ) ) )
392	391	oveq1d 6310	. . . 4 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( sin ` ( ( ( K + ( 1 / 2 ) ) x. pi ) + ( N x. pi ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) ) = ( ( sin ` ( ( ( ( K + ( 1 / 2 ) ) x. pi ) + pi ) + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) ) )
393	218, 118	addcld 9627	. . . . . . . . . 10 |- ( ph -> ( ( ( K + ( 1 / 2 ) ) x. pi ) + pi ) e. CC )
394	393, 293	jca 532	. . . . . . . . 9 |- ( ph -> ( ( ( ( K + ( 1 / 2 ) ) x. pi ) + pi ) e. CC /\ ( |_ ` ( N / 2 ) ) e. ZZ ) )
395		sinper 22740	. . . . . . . . 9 |- ( ( ( ( ( K + ( 1 / 2 ) ) x. pi ) + pi ) e. CC /\ ( |_ ` ( N / 2 ) ) e. ZZ ) -> ( sin ` ( ( ( ( K + ( 1 / 2 ) ) x. pi ) + pi ) + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) ) ) = ( sin ` ( ( ( K + ( 1 / 2 ) ) x. pi ) + pi ) ) )
396	394, 395	syl 16	. . . . . . . 8 |- ( ph -> ( sin ` ( ( ( ( K + ( 1 / 2 ) ) x. pi ) + pi ) + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) ) ) = ( sin ` ( ( ( K + ( 1 / 2 ) ) x. pi ) + pi ) ) )
397		sinppi 22748	. . . . . . . . 9 |- ( ( ( K + ( 1 / 2 ) ) x. pi ) e. CC -> ( sin ` ( ( ( K + ( 1 / 2 ) ) x. pi ) + pi ) ) = -u ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) )
398	218, 397	syl 16	. . . . . . . 8 |- ( ph -> ( sin ` ( ( ( K + ( 1 / 2 ) ) x. pi ) + pi ) ) = -u ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) )
399	396, 398	eqtrd 2508	. . . . . . 7 |- ( ph -> ( sin ` ( ( ( ( K + ( 1 / 2 ) ) x. pi ) + pi ) + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) ) ) = -u ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) )
400	399	oveq1d 6310	. . . . . 6 |- ( ph -> ( ( sin ` ( ( ( ( K + ( 1 / 2 ) ) x. pi ) + pi ) + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) ) = ( -u ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) ) )
401	220	oveq2d 6311	. . . . . 6 |- ( ph -> ( -u ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) ) = ( -u ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) / ( ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) x. ( 2 x. pi ) ) ) )
402	219	negcld 9929	. . . . . . . . 9 |- ( ph -> -u ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) e. CC )
403	402, 219, 217, 241, 242	divdiv1d 10363	. . . . . . . 8 |- ( ph -> ( ( -u ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) / ( 2 x. pi ) ) = ( -u ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) / ( ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) x. ( 2 x. pi ) ) ) )
404	403	eqcomd 2475	. . . . . . 7 |- ( ph -> ( -u ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) / ( ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) x. ( 2 x. pi ) ) ) = ( ( -u ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) / ( 2 x. pi ) ) )
405	219, 219, 241	divnegd 10345	. . . . . . . . . 10 |- ( ph -> -u ( ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) = ( -u ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) )
406	405	eqcomd 2475	. . . . . . . . 9 |- ( ph -> ( -u ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) = -u ( ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) )
407	245	negeqd 9826	. . . . . . . . 9 |- ( ph -> -u ( ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) = -u 1 )
408	406, 407	eqtrd 2508	. . . . . . . 8 |- ( ph -> ( -u ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) = -u 1 )
409	408	oveq1d 6310	. . . . . . 7 |- ( ph -> ( ( -u ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) / ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) / ( 2 x. pi ) ) = ( -u 1 / ( 2 x. pi ) ) )
410		divdiv1 10267	. . . . . . . . . . 11 |- ( ( -u 1 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( pi e. CC /\ pi =/= 0 ) ) -> ( ( -u 1 / 2 ) / pi ) = ( -u 1 / ( 2 x. pi ) ) )
411	358, 97, 102, 410	mp3an 1324	. . . . . . . . . 10 |- ( ( -u 1 / 2 ) / pi ) = ( -u 1 / ( 2 x. pi ) )
412	411	eqcomi 2480	. . . . . . . . 9 |- ( -u 1 / ( 2 x. pi ) ) = ( ( -u 1 / 2 ) / pi )
413	92, 13	negsubi 9909	. . . . . . . . . . . 12 |- ( ( 1 / 2 ) + -u 1 ) = ( ( 1 / 2 ) - 1 )
414	13, 92	negsubdi2i 9917	. . . . . . . . . . . . 13 |- -u ( 1 - ( 1 / 2 ) ) = ( ( 1 / 2 ) - 1 )
415	414	eqcomi 2480	. . . . . . . . . . . 12 |- ( ( 1 / 2 ) - 1 ) = -u ( 1 - ( 1 / 2 ) )
416		1mhlfehlf 10770	. . . . . . . . . . . . . 14 |- ( 1 - ( 1 / 2 ) ) = ( 1 / 2 )
417	416	negeqi 9825	. . . . . . . . . . . . 13 |- -u ( 1 - ( 1 / 2 ) ) = -u ( 1 / 2 )
418		divneg 10251	. . . . . . . . . . . . . 14 |- ( ( 1 e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> -u ( 1 / 2 ) = ( -u 1 / 2 ) )
419	13, 7, 55, 418	mp3an 1324	. . . . . . . . . . . . 13 |- -u ( 1 / 2 ) = ( -u 1 / 2 )
420	417, 419	eqtri 2496	. . . . . . . . . . . 12 |- -u ( 1 - ( 1 / 2 ) ) = ( -u 1 / 2 )
421	413, 415, 420	3eqtri 2500	. . . . . . . . . . 11 |- ( ( 1 / 2 ) + -u 1 ) = ( -u 1 / 2 )
422	421	oveq1i 6305	. . . . . . . . . 10 |- ( ( ( 1 / 2 ) + -u 1 ) / pi ) = ( ( -u 1 / 2 ) / pi )
423	422	eqcomi 2480	. . . . . . . . 9 |- ( ( -u 1 / 2 ) / pi ) = ( ( ( 1 / 2 ) + -u 1 ) / pi )
424	412, 423	eqtri 2496	. . . . . . . 8 |- ( -u 1 / ( 2 x. pi ) ) = ( ( ( 1 / 2 ) + -u 1 ) / pi )
425	424	a1i 11	. . . . . . 7 |- ( ph -> ( -u 1 / ( 2 x. pi ) ) = ( ( ( 1 / 2 ) + -u 1 ) / pi ) )
426	404, 409, 425	3eqtrd 2512	. . . . . 6 |- ( ph -> ( -u ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) / ( ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) x. ( 2 x. pi ) ) ) = ( ( ( 1 / 2 ) + -u 1 ) / pi ) )
427	400, 401, 426	3eqtrd 2512	. . . . 5 |- ( ph -> ( ( sin ` ( ( ( ( K + ( 1 / 2 ) ) x. pi ) + pi ) + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) ) = ( ( ( 1 / 2 ) + -u 1 ) / pi ) )
428	427	adantr 465	. . . 4 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( sin ` ( ( ( ( K + ( 1 / 2 ) ) x. pi ) + pi ) + ( ( |_ ` ( N / 2 ) ) x. ( 2 x. pi ) ) ) ) / ( ( 2 x. pi ) x. ( sin ` ( ( K + ( 1 / 2 ) ) x. pi ) ) ) ) = ( ( ( 1 / 2 ) + -u 1 ) / pi ) )
429	368, 392, 428	3eqtrrd 2513	. . 3 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( ( 1 / 2 ) + -u 1 ) / pi ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( ( 2 x. pi ) x. ( sin ` ( A / 2 ) ) ) ) )
430	252, 366, 429	3eqtrd 2512	. 2 |- ( ( ph /\ -. ( N mod 2 ) = 0 ) -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) / pi ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( ( 2 x. pi ) x. ( sin ` ( A / 2 ) ) ) ) )
431	251, 430	pm2.61dan 789	1 |- ( ph -> ( ( ( 1 / 2 ) + sum_ n e. ( 1 ... N ) ( cos ` ( n x. A ) ) ) / pi ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. A ) ) / ( ( 2 x. pi ) x. ( sin ` ( A / 2 ) ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1379   e. wcel 1767   =/= wne 2662   A.wral 2817   class class class wbr 4453   ` cfv 5594  (class class class)co 6295   CCcc 9502   RRcr 9503   0cc0 9504   1c1 9505   + caddc 9507   x. cmul 9509   < clt 9640   <_ cle 9641   - cmin 9817   -ucneg 9818   / cdiv 10218   NNcn 10548   2c2 10597   ZZcz 10876   ZZ>=cuz 11094   RR+crp 11232   ...cfz 11684   |_cfl 11907   mod cmo 11976   sum_csu 13488   sincsin 13678   cosccos 13679   picpi 13681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-inf2 8070  ax-cnex 9560  ax-resscn 9561  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-mulcom 9568  ax-addass 9569  ax-mulass 9570  ax-distr 9571  ax-i2m1 9572  ax-1ne0 9573  ax-1rid 9574  ax-rnegex 9575  ax-rrecex 9576  ax-cnre 9577  ax-pre-lttri 9578  ax-pre-lttrn 9579  ax-pre-ltadd 9580  ax-pre-mulgt0 9581  ax-pre-sup 9582  ax-addf 9583  ax-mulf 9584

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-int 4289  df-iun 4333  df-iin 4334  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-se 4845  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-isom 5603  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-of 6535  df-om 6696  df-1st 6795  df-2nd 6796  df-supp 6914  df-recs 7054  df-rdg 7088  df-1o 7142  df-2o 7143  df-oadd 7146  df-er 7323  df-map 7434  df-pm 7435  df-ixp 7482  df-en 7529  df-dom 7530  df-sdom 7531  df-fin 7532  df-fsupp 7842  df-fi 7883  df-sup 7913  df-oi 7947  df-card 8332  df-cda 8560  df-pnf 9642  df-mnf 9643  df-xr 9644  df-ltxr 9645  df-le 9646  df-sub 9819  df-neg 9820  df-div 10219  df-nn 10549  df-2 10606  df-3 10607  df-4 10608