Theorem dirkertrigeqlem1 31721

Description: Sum of an even number of alternating cos values. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Assertion

Ref	Expression
dirkertrigeqlem1	|- ( K e. NN -> sum_ n e. ( 1 ... ( 2 x. K ) ) ( cos ` ( n x. pi ) ) = 0 )

Distinct variable group:   n, K

Proof of Theorem dirkertrigeqlem1

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 6303	. . . . 5 |- ( x = 1 -> ( 2 x. x ) = ( 2 x. 1 ) )
2	1	oveq2d 6311	. . . 4 |- ( x = 1 -> ( 1 ... ( 2 x. x ) ) = ( 1 ... ( 2 x. 1 ) ) )
3	2	sumeq1d 13503	. . 3 |- ( x = 1 -> sum_ n e. ( 1 ... ( 2 x. x ) ) ( cos ` ( n x. pi ) ) = sum_ n e. ( 1 ... ( 2 x. 1 ) ) ( cos ` ( n x. pi ) ) )
4	3	eqeq1d 2469	. 2 |- ( x = 1 -> ( sum_ n e. ( 1 ... ( 2 x. x ) ) ( cos ` ( n x. pi ) ) = 0 <-> sum_ n e. ( 1 ... ( 2 x. 1 ) ) ( cos ` ( n x. pi ) ) = 0 ) )
5		oveq2 6303	. . . . 5 |- ( x = y -> ( 2 x. x ) = ( 2 x. y ) )
6	5	oveq2d 6311	. . . 4 |- ( x = y -> ( 1 ... ( 2 x. x ) ) = ( 1 ... ( 2 x. y ) ) )
7	6	sumeq1d 13503	. . 3 |- ( x = y -> sum_ n e. ( 1 ... ( 2 x. x ) ) ( cos ` ( n x. pi ) ) = sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. pi ) ) )
8	7	eqeq1d 2469	. 2 |- ( x = y -> ( sum_ n e. ( 1 ... ( 2 x. x ) ) ( cos ` ( n x. pi ) ) = 0 <-> sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. pi ) ) = 0 ) )
9		oveq2 6303	. . . . 5 |- ( x = ( y + 1 ) -> ( 2 x. x ) = ( 2 x. ( y + 1 ) ) )
10	9	oveq2d 6311	. . . 4 |- ( x = ( y + 1 ) -> ( 1 ... ( 2 x. x ) ) = ( 1 ... ( 2 x. ( y + 1 ) ) ) )
11	10	sumeq1d 13503	. . 3 |- ( x = ( y + 1 ) -> sum_ n e. ( 1 ... ( 2 x. x ) ) ( cos ` ( n x. pi ) ) = sum_ n e. ( 1 ... ( 2 x. ( y + 1 ) ) ) ( cos ` ( n x. pi ) ) )
12	11	eqeq1d 2469	. 2 |- ( x = ( y + 1 ) -> ( sum_ n e. ( 1 ... ( 2 x. x ) ) ( cos ` ( n x. pi ) ) = 0 <-> sum_ n e. ( 1 ... ( 2 x. ( y + 1 ) ) ) ( cos ` ( n x. pi ) ) = 0 ) )
13		oveq2 6303	. . . . 5 |- ( x = K -> ( 2 x. x ) = ( 2 x. K ) )
14	13	oveq2d 6311	. . . 4 |- ( x = K -> ( 1 ... ( 2 x. x ) ) = ( 1 ... ( 2 x. K ) ) )
15	14	sumeq1d 13503	. . 3 |- ( x = K -> sum_ n e. ( 1 ... ( 2 x. x ) ) ( cos ` ( n x. pi ) ) = sum_ n e. ( 1 ... ( 2 x. K ) ) ( cos ` ( n x. pi ) ) )
16	15	eqeq1d 2469	. 2 |- ( x = K -> ( sum_ n e. ( 1 ... ( 2 x. x ) ) ( cos ` ( n x. pi ) ) = 0 <-> sum_ n e. ( 1 ... ( 2 x. K ) ) ( cos ` ( n x. pi ) ) = 0 ) )
17		ax-1cn 9562	. . . . . 6 |- 1 e. CC
18	17	2timesi 10668	. . . . 5 |- ( 2 x. 1 ) = ( 1 + 1 )
19	18	oveq2i 6306	. . . 4 |- ( 1 ... ( 2 x. 1 ) ) = ( 1 ... ( 1 + 1 ) )
20	19	sumeq1i 13500	. . 3 |- sum_ n e. ( 1 ... ( 2 x. 1 ) ) ( cos ` ( n x. pi ) ) = sum_ n e. ( 1 ... ( 1 + 1 ) ) ( cos ` ( n x. pi ) )
21		1z 10906	. . . . . . . 8 |- 1 e. ZZ
22		uzid 11108	. . . . . . . 8 |- ( 1 e. ZZ -> 1 e. ( ZZ>= ` 1 ) )
23	21, 22	ax-mp 5	. . . . . . 7 |- 1 e. ( ZZ>= ` 1 )
24	23	a1i 11	. . . . . 6 |- ( T. -> 1 e. ( ZZ>= ` 1 ) )
25		elfzelz 11700	. . . . . . . . . 10 |- ( n e. ( 1 ... ( 1 + 1 ) ) -> n e. ZZ )
26	25	zcnd 10979	. . . . . . . . 9 |- ( n e. ( 1 ... ( 1 + 1 ) ) -> n e. CC )
27	26	adantl 466	. . . . . . . 8 |- ( ( T. /\ n e. ( 1 ... ( 1 + 1 ) ) ) -> n e. CC )
28		pire 22718	. . . . . . . . . 10 |- pi e. RR
29	28	recni 9620	. . . . . . . . 9 |- pi e. CC
30	29	a1i 11	. . . . . . . 8 |- ( ( T. /\ n e. ( 1 ... ( 1 + 1 ) ) ) -> pi e. CC )
31	27, 30	mulcld 9628	. . . . . . 7 |- ( ( T. /\ n e. ( 1 ... ( 1 + 1 ) ) ) -> ( n x. pi ) e. CC )
32	31	coscld 13744	. . . . . 6 |- ( ( T. /\ n e. ( 1 ... ( 1 + 1 ) ) ) -> ( cos ` ( n x. pi ) ) e. CC )
33		id 22	. . . . . . . . 9 |- ( n = ( 1 + 1 ) -> n = ( 1 + 1 ) )
34		2cn 10618	. . . . . . . . . . . 12 |- 2 e. CC
35	34	mulid1i 9610	. . . . . . . . . . 11 |- ( 2 x. 1 ) = 2
36	18, 35	eqtr3i 2498	. . . . . . . . . 10 |- ( 1 + 1 ) = 2
37	36	a1i 11	. . . . . . . . 9 |- ( n = ( 1 + 1 ) -> ( 1 + 1 ) = 2 )
38	33, 37	eqtrd 2508	. . . . . . . 8 |- ( n = ( 1 + 1 ) -> n = 2 )
39	38	oveq1d 6310	. . . . . . 7 |- ( n = ( 1 + 1 ) -> ( n x. pi ) = ( 2 x. pi ) )
40	39	fveq2d 5876	. . . . . 6 |- ( n = ( 1 + 1 ) -> ( cos ` ( n x. pi ) ) = ( cos ` ( 2 x. pi ) ) )
41	24, 32, 40	fsump1 13551	. . . . 5 |- ( T. -> sum_ n e. ( 1 ... ( 1 + 1 ) ) ( cos ` ( n x. pi ) ) = ( sum_ n e. ( 1 ... 1 ) ( cos ` ( n x. pi ) ) + ( cos ` ( 2 x. pi ) ) ) )
42	41	trud 1388	. . . 4 |- sum_ n e. ( 1 ... ( 1 + 1 ) ) ( cos ` ( n x. pi ) ) = ( sum_ n e. ( 1 ... 1 ) ( cos ` ( n x. pi ) ) + ( cos ` ( 2 x. pi ) ) )
43		coscl 13740	. . . . . . . . 9 |- ( pi e. CC -> ( cos ` pi ) e. CC )
44	29, 43	ax-mp 5	. . . . . . . 8 |- ( cos ` pi ) e. CC
45	21, 44	pm3.2i 455	. . . . . . 7 |- ( 1 e. ZZ /\ ( cos ` pi ) e. CC )
46		oveq1 6302	. . . . . . . . . 10 |- ( n = 1 -> ( n x. pi ) = ( 1 x. pi ) )
47	29	mulid2i 9611	. . . . . . . . . . 11 |- ( 1 x. pi ) = pi
48	47	a1i 11	. . . . . . . . . 10 |- ( n = 1 -> ( 1 x. pi ) = pi )
49	46, 48	eqtrd 2508	. . . . . . . . 9 |- ( n = 1 -> ( n x. pi ) = pi )
50	49	fveq2d 5876	. . . . . . . 8 |- ( n = 1 -> ( cos ` ( n x. pi ) ) = ( cos ` pi ) )
51	50	fsum1 13544	. . . . . . 7 |- ( ( 1 e. ZZ /\ ( cos ` pi ) e. CC ) -> sum_ n e. ( 1 ... 1 ) ( cos ` ( n x. pi ) ) = ( cos ` pi ) )
52	45, 51	ax-mp 5	. . . . . 6 |- sum_ n e. ( 1 ... 1 ) ( cos ` ( n x. pi ) ) = ( cos ` pi )
53		cospi 22731	. . . . . 6 |- ( cos ` pi ) = -u 1
54	52, 53	eqtri 2496	. . . . 5 |- sum_ n e. ( 1 ... 1 ) ( cos ` ( n x. pi ) ) = -u 1
55		cos2pi 22735	. . . . 5 |- ( cos ` ( 2 x. pi ) ) = 1
56	54, 55	oveq12i 6307	. . . 4 |- ( sum_ n e. ( 1 ... 1 ) ( cos ` ( n x. pi ) ) + ( cos ` ( 2 x. pi ) ) ) = ( -u 1 + 1 )
57	53, 44	eqeltrri 2552	. . . . . 6 |- -u 1 e. CC
58	57, 17	addcomi 9782	. . . . 5 |- ( -u 1 + 1 ) = ( 1 + -u 1 )
59	17	negidi 9900	. . . . 5 |- ( 1 + -u 1 ) = 0
60	58, 59	eqtri 2496	. . . 4 |- ( -u 1 + 1 ) = 0
61	42, 56, 60	3eqtri 2500	. . 3 |- sum_ n e. ( 1 ... ( 1 + 1 ) ) ( cos ` ( n x. pi ) ) = 0
62	20, 61	eqtri 2496	. 2 |- sum_ n e. ( 1 ... ( 2 x. 1 ) ) ( cos ` ( n x. pi ) ) = 0
63	34	a1i 11	. . . . . . . . 9 |- ( y e. NN -> 2 e. CC )
64		nncn 10556	. . . . . . . . 9 |- ( y e. NN -> y e. CC )
65	17	a1i 11	. . . . . . . . 9 |- ( y e. NN -> 1 e. CC )
66	63, 64, 65	adddid 9632	. . . . . . . 8 |- ( y e. NN -> ( 2 x. ( y + 1 ) ) = ( ( 2 x. y ) + ( 2 x. 1 ) ) )
67	18	oveq2i 6306	. . . . . . . . 9 |- ( ( 2 x. y ) + ( 2 x. 1 ) ) = ( ( 2 x. y ) + ( 1 + 1 ) )
68	67	a1i 11	. . . . . . . 8 |- ( y e. NN -> ( ( 2 x. y ) + ( 2 x. 1 ) ) = ( ( 2 x. y ) + ( 1 + 1 ) ) )
69	63, 64	mulcld 9628	. . . . . . . . . 10 |- ( y e. NN -> ( 2 x. y ) e. CC )
70	69, 65, 65	addassd 9630	. . . . . . . . 9 |- ( y e. NN -> ( ( ( 2 x. y ) + 1 ) + 1 ) = ( ( 2 x. y ) + ( 1 + 1 ) ) )
71	70	eqcomd 2475	. . . . . . . 8 |- ( y e. NN -> ( ( 2 x. y ) + ( 1 + 1 ) ) = ( ( ( 2 x. y ) + 1 ) + 1 ) )
72	66, 68, 71	3eqtrd 2512	. . . . . . 7 |- ( y e. NN -> ( 2 x. ( y + 1 ) ) = ( ( ( 2 x. y ) + 1 ) + 1 ) )
73	72	oveq2d 6311	. . . . . 6 |- ( y e. NN -> ( 1 ... ( 2 x. ( y + 1 ) ) ) = ( 1 ... ( ( ( 2 x. y ) + 1 ) + 1 ) ) )
74	73	sumeq1d 13503	. . . . 5 |- ( y e. NN -> sum_ n e. ( 1 ... ( 2 x. ( y + 1 ) ) ) ( cos ` ( n x. pi ) ) = sum_ n e. ( 1 ... ( ( ( 2 x. y ) + 1 ) + 1 ) ) ( cos ` ( n x. pi ) ) )
75	74	adantr 465	. . . 4 |- ( ( y e. NN /\ sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. pi ) ) = 0 ) -> sum_ n e. ( 1 ... ( 2 x. ( y + 1 ) ) ) ( cos ` ( n x. pi ) ) = sum_ n e. ( 1 ... ( ( ( 2 x. y ) + 1 ) + 1 ) ) ( cos ` ( n x. pi ) ) )
76		1re 9607	. . . . . . . . 9 |- 1 e. RR
77	76	a1i 11	. . . . . . . 8 |- ( y e. NN -> 1 e. RR )
78		2re 10617	. . . . . . . . . . 11 |- 2 e. RR
79	78	a1i 11	. . . . . . . . . 10 |- ( y e. NN -> 2 e. RR )
80		nnre 10555	. . . . . . . . . 10 |- ( y e. NN -> y e. RR )
81	79, 80	remulcld 9636	. . . . . . . . 9 |- ( y e. NN -> ( 2 x. y ) e. RR )
82	81, 77	readdcld 9635	. . . . . . . 8 |- ( y e. NN -> ( ( 2 x. y ) + 1 ) e. RR )
83		2rp 11237	. . . . . . . . . . . 12 |- 2 e. RR+
84	83	a1i 11	. . . . . . . . . . 11 |- ( y e. NN -> 2 e. RR+ )
85		nnrp 11241	. . . . . . . . . . 11 |- ( y e. NN -> y e. RR+ )
86	84, 85	rpmulcld 11284	. . . . . . . . . 10 |- ( y e. NN -> ( 2 x. y ) e. RR+ )
87		ltaddrp 11264	. . . . . . . . . 10 |- ( ( 1 e. RR /\ ( 2 x. y ) e. RR+ ) -> 1 < ( 1 + ( 2 x. y ) ) )
88	77, 86, 87	syl2anc 661	. . . . . . . . 9 |- ( y e. NN -> 1 < ( 1 + ( 2 x. y ) ) )
89	65, 69	addcomd 9793	. . . . . . . . 9 |- ( y e. NN -> ( 1 + ( 2 x. y ) ) = ( ( 2 x. y ) + 1 ) )
90	88, 89	breqtrd 4477	. . . . . . . 8 |- ( y e. NN -> 1 < ( ( 2 x. y ) + 1 ) )
91	77, 82, 90	ltled 9744	. . . . . . 7 |- ( y e. NN -> 1 <_ ( ( 2 x. y ) + 1 ) )
92	21	a1i 11	. . . . . . . 8 |- ( y e. NN -> 1 e. ZZ )
93		2z 10908	. . . . . . . . . . 11 |- 2 e. ZZ
94	93	a1i 11	. . . . . . . . . 10 |- ( y e. NN -> 2 e. ZZ )
95		nnz 10898	. . . . . . . . . 10 |- ( y e. NN -> y e. ZZ )
96	94, 95	zmulcld 10984	. . . . . . . . 9 |- ( y e. NN -> ( 2 x. y ) e. ZZ )
97	96, 92	zaddcld 10982	. . . . . . . 8 |- ( y e. NN -> ( ( 2 x. y ) + 1 ) e. ZZ )
98		eluz 11107	. . . . . . . 8 |- ( ( 1 e. ZZ /\ ( ( 2 x. y ) + 1 ) e. ZZ ) -> ( ( ( 2 x. y ) + 1 ) e. ( ZZ>= ` 1 ) <-> 1 <_ ( ( 2 x. y ) + 1 ) ) )
99	92, 97, 98	syl2anc 661	. . . . . . 7 |- ( y e. NN -> ( ( ( 2 x. y ) + 1 ) e. ( ZZ>= ` 1 ) <-> 1 <_ ( ( 2 x. y ) + 1 ) ) )
100	91, 99	mpbird 232	. . . . . 6 |- ( y e. NN -> ( ( 2 x. y ) + 1 ) e. ( ZZ>= ` 1 ) )
101		elfzelz 11700	. . . . . . . . . 10 |- ( n e. ( 1 ... ( ( ( 2 x. y ) + 1 ) + 1 ) ) -> n e. ZZ )
102	101	zcnd 10979	. . . . . . . . 9 |- ( n e. ( 1 ... ( ( ( 2 x. y ) + 1 ) + 1 ) ) -> n e. CC )
103	29	a1i 11	. . . . . . . . 9 |- ( n e. ( 1 ... ( ( ( 2 x. y ) + 1 ) + 1 ) ) -> pi e. CC )
104	102, 103	mulcld 9628	. . . . . . . 8 |- ( n e. ( 1 ... ( ( ( 2 x. y ) + 1 ) + 1 ) ) -> ( n x. pi ) e. CC )
105	104	coscld 13744	. . . . . . 7 |- ( n e. ( 1 ... ( ( ( 2 x. y ) + 1 ) + 1 ) ) -> ( cos ` ( n x. pi ) ) e. CC )
106	105	adantl 466	. . . . . 6 |- ( ( y e. NN /\ n e. ( 1 ... ( ( ( 2 x. y ) + 1 ) + 1 ) ) ) -> ( cos ` ( n x. pi ) ) e. CC )
107		oveq1 6302	. . . . . . 7 |- ( n = ( ( ( 2 x. y ) + 1 ) + 1 ) -> ( n x. pi ) = ( ( ( ( 2 x. y ) + 1 ) + 1 ) x. pi ) )
108	107	fveq2d 5876	. . . . . 6 |- ( n = ( ( ( 2 x. y ) + 1 ) + 1 ) -> ( cos ` ( n x. pi ) ) = ( cos ` ( ( ( ( 2 x. y ) + 1 ) + 1 ) x. pi ) ) )
109	100, 106, 108	fsump1 13551	. . . . 5 |- ( y e. NN -> sum_ n e. ( 1 ... ( ( ( 2 x. y ) + 1 ) + 1 ) ) ( cos ` ( n x. pi ) ) = ( sum_ n e. ( 1 ... ( ( 2 x. y ) + 1 ) ) ( cos ` ( n x. pi ) ) + ( cos ` ( ( ( ( 2 x. y ) + 1 ) + 1 ) x. pi ) ) ) )
110	109	adantr 465	. . . 4 |- ( ( y e. NN /\ sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. pi ) ) = 0 ) -> sum_ n e. ( 1 ... ( ( ( 2 x. y ) + 1 ) + 1 ) ) ( cos ` ( n x. pi ) ) = ( sum_ n e. ( 1 ... ( ( 2 x. y ) + 1 ) ) ( cos ` ( n x. pi ) ) + ( cos ` ( ( ( ( 2 x. y ) + 1 ) + 1 ) x. pi ) ) ) )
111		1lt2 10714	. . . . . . . . . . . 12 |- 1 < 2
112	111	a1i 11	. . . . . . . . . . 11 |- ( y e. NN -> 1 < 2 )
113	35	eqcomi 2480	. . . . . . . . . . . . 13 |- 2 = ( 2 x. 1 )
114	113	a1i 11	. . . . . . . . . . . 12 |- ( y e. NN -> 2 = ( 2 x. 1 ) )
115		nnge1 10574	. . . . . . . . . . . . 13 |- ( y e. NN -> 1 <_ y )
116	77, 80, 84	lemul2d 11308	. . . . . . . . . . . . 13 |- ( y e. NN -> ( 1 <_ y <-> ( 2 x. 1 ) <_ ( 2 x. y ) ) )
117	115, 116	mpbid 210	. . . . . . . . . . . 12 |- ( y e. NN -> ( 2 x. 1 ) <_ ( 2 x. y ) )
118	114, 117	eqbrtrd 4473	. . . . . . . . . . 11 |- ( y e. NN -> 2 <_ ( 2 x. y ) )
119	77, 79, 81, 112, 118	ltletrd 9753	. . . . . . . . . 10 |- ( y e. NN -> 1 < ( 2 x. y ) )
120	77, 81, 119	ltled 9744	. . . . . . . . 9 |- ( y e. NN -> 1 <_ ( 2 x. y ) )
121		eluz 11107	. . . . . . . . . 10 |- ( ( 1 e. ZZ /\ ( 2 x. y ) e. ZZ ) -> ( ( 2 x. y ) e. ( ZZ>= ` 1 ) <-> 1 <_ ( 2 x. y ) ) )
122	92, 96, 121	syl2anc 661	. . . . . . . . 9 |- ( y e. NN -> ( ( 2 x. y ) e. ( ZZ>= ` 1 ) <-> 1 <_ ( 2 x. y ) ) )
123	120, 122	mpbird 232	. . . . . . . 8 |- ( y e. NN -> ( 2 x. y ) e. ( ZZ>= ` 1 ) )
124		elfzelz 11700	. . . . . . . . . . . 12 |- ( n e. ( 1 ... ( ( 2 x. y ) + 1 ) ) -> n e. ZZ )
125	124	zcnd 10979	. . . . . . . . . . 11 |- ( n e. ( 1 ... ( ( 2 x. y ) + 1 ) ) -> n e. CC )
126	29	a1i 11	. . . . . . . . . . 11 |- ( n e. ( 1 ... ( ( 2 x. y ) + 1 ) ) -> pi e. CC )
127	125, 126	mulcld 9628	. . . . . . . . . 10 |- ( n e. ( 1 ... ( ( 2 x. y ) + 1 ) ) -> ( n x. pi ) e. CC )
128	127	coscld 13744	. . . . . . . . 9 |- ( n e. ( 1 ... ( ( 2 x. y ) + 1 ) ) -> ( cos ` ( n x. pi ) ) e. CC )
129	128	adantl 466	. . . . . . . 8 |- ( ( y e. NN /\ n e. ( 1 ... ( ( 2 x. y ) + 1 ) ) ) -> ( cos ` ( n x. pi ) ) e. CC )
130		oveq1 6302	. . . . . . . . 9 |- ( n = ( ( 2 x. y ) + 1 ) -> ( n x. pi ) = ( ( ( 2 x. y ) + 1 ) x. pi ) )
131	130	fveq2d 5876	. . . . . . . 8 |- ( n = ( ( 2 x. y ) + 1 ) -> ( cos ` ( n x. pi ) ) = ( cos ` ( ( ( 2 x. y ) + 1 ) x. pi ) ) )
132	123, 129, 131	fsump1 13551	. . . . . . 7 |- ( y e. NN -> sum_ n e. ( 1 ... ( ( 2 x. y ) + 1 ) ) ( cos ` ( n x. pi ) ) = ( sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. pi ) ) + ( cos ` ( ( ( 2 x. y ) + 1 ) x. pi ) ) ) )
133	36, 113	eqtri 2496	. . . . . . . . . . . . 13 |- ( 1 + 1 ) = ( 2 x. 1 )
134	133	a1i 11	. . . . . . . . . . . 12 |- ( y e. NN -> ( 1 + 1 ) = ( 2 x. 1 ) )
135	134	oveq2d 6311	. . . . . . . . . . 11 |- ( y e. NN -> ( ( 2 x. y ) + ( 1 + 1 ) ) = ( ( 2 x. y ) + ( 2 x. 1 ) ) )
136	66	eqcomd 2475	. . . . . . . . . . 11 |- ( y e. NN -> ( ( 2 x. y ) + ( 2 x. 1 ) ) = ( 2 x. ( y + 1 ) ) )
137	70, 135, 136	3eqtrd 2512	. . . . . . . . . 10 |- ( y e. NN -> ( ( ( 2 x. y ) + 1 ) + 1 ) = ( 2 x. ( y + 1 ) ) )
138	137	oveq1d 6310	. . . . . . . . 9 |- ( y e. NN -> ( ( ( ( 2 x. y ) + 1 ) + 1 ) x. pi ) = ( ( 2 x. ( y + 1 ) ) x. pi ) )
139	138	fveq2d 5876	. . . . . . . 8 |- ( y e. NN -> ( cos ` ( ( ( ( 2 x. y ) + 1 ) + 1 ) x. pi ) ) = ( cos ` ( ( 2 x. ( y + 1 ) ) x. pi ) ) )
140	64, 65	addcld 9627	. . . . . . . . . . . . 13 |- ( y e. NN -> ( y + 1 ) e. CC )
141	29	a1i 11	. . . . . . . . . . . . 13 |- ( y e. NN -> pi e. CC )
142	63, 140, 141	mulassd 9631	. . . . . . . . . . . 12 |- ( y e. NN -> ( ( 2 x. ( y + 1 ) ) x. pi ) = ( 2 x. ( ( y + 1 ) x. pi ) ) )
143	142	oveq1d 6310	. . . . . . . . . . 11 |- ( y e. NN -> ( ( ( 2 x. ( y + 1 ) ) x. pi ) / ( 2 x. pi ) ) = ( ( 2 x. ( ( y + 1 ) x. pi ) ) / ( 2 x. pi ) ) )
144	140, 141	mulcld 9628	. . . . . . . . . . . 12 |- ( y e. NN -> ( ( y + 1 ) x. pi ) e. CC )
145		0re 9608	. . . . . . . . . . . . . 14 |- 0 e. RR
146		pipos 22720	. . . . . . . . . . . . . 14 |- 0 < pi
147		ltne 9693	. . . . . . . . . . . . . 14 |- ( ( 0 e. RR /\ 0 < pi ) -> pi =/= 0 )
148	145, 146, 147	mp2an 672	. . . . . . . . . . . . 13 |- pi =/= 0
149	148	a1i 11	. . . . . . . . . . . 12 |- ( y e. NN -> pi =/= 0 )
150	84	rpne0d 11273	. . . . . . . . . . . 12 |- ( y e. NN -> 2 =/= 0 )
151	144, 141, 63, 149, 150	divcan5d 10358	. . . . . . . . . . 11 |- ( y e. NN -> ( ( 2 x. ( ( y + 1 ) x. pi ) ) / ( 2 x. pi ) ) = ( ( ( y + 1 ) x. pi ) / pi ) )
152	140, 141, 149	divcan4d 10338	. . . . . . . . . . 11 |- ( y e. NN -> ( ( ( y + 1 ) x. pi ) / pi ) = ( y + 1 ) )
153	143, 151, 152	3eqtrd 2512	. . . . . . . . . 10 |- ( y e. NN -> ( ( ( 2 x. ( y + 1 ) ) x. pi ) / ( 2 x. pi ) ) = ( y + 1 ) )
154	95	peano2zd 10981	. . . . . . . . . 10 |- ( y e. NN -> ( y + 1 ) e. ZZ )
155	153, 154	eqeltrd 2555	. . . . . . . . 9 |- ( y e. NN -> ( ( ( 2 x. ( y + 1 ) ) x. pi ) / ( 2 x. pi ) ) e. ZZ )
156		peano2cn 9763	. . . . . . . . . . . . . . 15 |- ( y e. CC -> ( y + 1 ) e. CC )
157	64, 156	syl 16	. . . . . . . . . . . . . 14 |- ( y e. NN -> ( y + 1 ) e. CC )
158	63, 157	jca 532	. . . . . . . . . . . . 13 |- ( y e. NN -> ( 2 e. CC /\ ( y + 1 ) e. CC ) )
159		mulcl 9588	. . . . . . . . . . . . 13 |- ( ( 2 e. CC /\ ( y + 1 ) e. CC ) -> ( 2 x. ( y + 1 ) ) e. CC )
160	158, 159	syl 16	. . . . . . . . . . . 12 |- ( y e. NN -> ( 2 x. ( y + 1 ) ) e. CC )
161	160, 141	jca 532	. . . . . . . . . . 11 |- ( y e. NN -> ( ( 2 x. ( y + 1 ) ) e. CC /\ pi e. CC ) )
162		mulcl 9588	. . . . . . . . . . 11 |- ( ( ( 2 x. ( y + 1 ) ) e. CC /\ pi e. CC ) -> ( ( 2 x. ( y + 1 ) ) x. pi ) e. CC )
163	161, 162	syl 16	. . . . . . . . . 10 |- ( y e. NN -> ( ( 2 x. ( y + 1 ) ) x. pi ) e. CC )
164		coseq1 22781	. . . . . . . . . 10 |- ( ( ( 2 x. ( y + 1 ) ) x. pi ) e. CC -> ( ( cos ` ( ( 2 x. ( y + 1 ) ) x. pi ) ) = 1 <-> ( ( ( 2 x. ( y + 1 ) ) x. pi ) / ( 2 x. pi ) ) e. ZZ ) )
165	163, 164	syl 16	. . . . . . . . 9 |- ( y e. NN -> ( ( cos ` ( ( 2 x. ( y + 1 ) ) x. pi ) ) = 1 <-> ( ( ( 2 x. ( y + 1 ) ) x. pi ) / ( 2 x. pi ) ) e. ZZ ) )
166	155, 165	mpbird 232	. . . . . . . 8 |- ( y e. NN -> ( cos ` ( ( 2 x. ( y + 1 ) ) x. pi ) ) = 1 )
167		eqidd 2468	. . . . . . . 8 |- ( y e. NN -> 1 = 1 )
168	139, 166, 167	3eqtrd 2512	. . . . . . 7 |- ( y e. NN -> ( cos ` ( ( ( ( 2 x. y ) + 1 ) + 1 ) x. pi ) ) = 1 )
169	132, 168	oveq12d 6313	. . . . . 6 |- ( y e. NN -> ( sum_ n e. ( 1 ... ( ( 2 x. y ) + 1 ) ) ( cos ` ( n x. pi ) ) + ( cos ` ( ( ( ( 2 x. y ) + 1 ) + 1 ) x. pi ) ) ) = ( ( sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. pi ) ) + ( cos ` ( ( ( 2 x. y ) + 1 ) x. pi ) ) ) + 1 ) )
170	169	adantr 465	. . . . 5 |- ( ( y e. NN /\ sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. pi ) ) = 0 ) -> ( sum_ n e. ( 1 ... ( ( 2 x. y ) + 1 ) ) ( cos ` ( n x. pi ) ) + ( cos ` ( ( ( ( 2 x. y ) + 1 ) + 1 ) x. pi ) ) ) = ( ( sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. pi ) ) + ( cos ` ( ( ( 2 x. y ) + 1 ) x. pi ) ) ) + 1 ) )
171		simpr 461	. . . . . . . 8 |- ( ( y e. NN /\ sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. pi ) ) = 0 ) -> sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. pi ) ) = 0 )
172	69, 65, 141	adddird 9633	. . . . . . . . . . . 12 |- ( y e. NN -> ( ( ( 2 x. y ) + 1 ) x. pi ) = ( ( ( 2 x. y ) x. pi ) + ( 1 x. pi ) ) )
173	69, 141	mulcld 9628	. . . . . . . . . . . . 13 |- ( y e. NN -> ( ( 2 x. y ) x. pi ) e. CC )
174	47, 141	syl5eqel 2559	. . . . . . . . . . . . 13 |- ( y e. NN -> ( 1 x. pi ) e. CC )
175	173, 174	addcomd 9793	. . . . . . . . . . . 12 |- ( y e. NN -> ( ( ( 2 x. y ) x. pi ) + ( 1 x. pi ) ) = ( ( 1 x. pi ) + ( ( 2 x. y ) x. pi ) ) )
176	47	a1i 11	. . . . . . . . . . . . 13 |- ( y e. NN -> ( 1 x. pi ) = pi )
177	63, 64	mulcomd 9629	. . . . . . . . . . . . . . 15 |- ( y e. NN -> ( 2 x. y ) = ( y x. 2 ) )
178	177	oveq1d 6310	. . . . . . . . . . . . . 14 |- ( y e. NN -> ( ( 2 x. y ) x. pi ) = ( ( y x. 2 ) x. pi ) )
179	64, 63, 141	mulassd 9631	. . . . . . . . . . . . . 14 |- ( y e. NN -> ( ( y x. 2 ) x. pi ) = ( y x. ( 2 x. pi ) ) )
180	178, 179	eqtrd 2508	. . . . . . . . . . . . 13 |- ( y e. NN -> ( ( 2 x. y ) x. pi ) = ( y x. ( 2 x. pi ) ) )
181	176, 180	oveq12d 6313	. . . . . . . . . . . 12 |- ( y e. NN -> ( ( 1 x. pi ) + ( ( 2 x. y ) x. pi ) ) = ( pi + ( y x. ( 2 x. pi ) ) ) )
182	172, 175, 181	3eqtrd 2512	. . . . . . . . . . 11 |- ( y e. NN -> ( ( ( 2 x. y ) + 1 ) x. pi ) = ( pi + ( y x. ( 2 x. pi ) ) ) )
183	182	fveq2d 5876	. . . . . . . . . 10 |- ( y e. NN -> ( cos ` ( ( ( 2 x. y ) + 1 ) x. pi ) ) = ( cos ` ( pi + ( y x. ( 2 x. pi ) ) ) ) )
184		cosper 22741	. . . . . . . . . . 11 |- ( ( pi e. CC /\ y e. ZZ ) -> ( cos ` ( pi + ( y x. ( 2 x. pi ) ) ) ) = ( cos ` pi ) )
185	141, 95, 184	syl2anc 661	. . . . . . . . . 10 |- ( y e. NN -> ( cos ` ( pi + ( y x. ( 2 x. pi ) ) ) ) = ( cos ` pi ) )
186	53	a1i 11	. . . . . . . . . 10 |- ( y e. NN -> ( cos ` pi ) = -u 1 )
187	183, 185, 186	3eqtrd 2512	. . . . . . . . 9 |- ( y e. NN -> ( cos ` ( ( ( 2 x. y ) + 1 ) x. pi ) ) = -u 1 )
188	187	adantr 465	. . . . . . . 8 |- ( ( y e. NN /\ sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. pi ) ) = 0 ) -> ( cos ` ( ( ( 2 x. y ) + 1 ) x. pi ) ) = -u 1 )
189	171, 188	oveq12d 6313	. . . . . . 7 |- ( ( y e. NN /\ sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. pi ) ) = 0 ) -> ( sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. pi ) ) + ( cos ` ( ( ( 2 x. y ) + 1 ) x. pi ) ) ) = ( 0 + -u 1 ) )
190	189	oveq1d 6310	. . . . . 6 |- ( ( y e. NN /\ sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. pi ) ) = 0 ) -> ( ( sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. pi ) ) + ( cos ` ( ( ( 2 x. y ) + 1 ) x. pi ) ) ) + 1 ) = ( ( 0 + -u 1 ) + 1 ) )
191	57	addid2i 9779	. . . . . . . . 9 |- ( 0 + -u 1 ) = -u 1
192	191	oveq1i 6305	. . . . . . . 8 |- ( ( 0 + -u 1 ) + 1 ) = ( -u 1 + 1 )
193	192, 60	eqtri 2496	. . . . . . 7 |- ( ( 0 + -u 1 ) + 1 ) = 0
194	193	a1i 11	. . . . . 6 |- ( ( y e. NN /\ sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. pi ) ) = 0 ) -> ( ( 0 + -u 1 ) + 1 ) = 0 )
195	190, 194	eqtrd 2508	. . . . 5 |- ( ( y e. NN /\ sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. pi ) ) = 0 ) -> ( ( sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. pi ) ) + ( cos ` ( ( ( 2 x. y ) + 1 ) x. pi ) ) ) + 1 ) = 0 )
196	170, 195	eqtrd 2508	. . . 4 |- ( ( y e. NN /\ sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. pi ) ) = 0 ) -> ( sum_ n e. ( 1 ... ( ( 2 x. y ) + 1 ) ) ( cos ` ( n x. pi ) ) + ( cos ` ( ( ( ( 2 x. y ) + 1 ) + 1 ) x. pi ) ) ) = 0 )
197	75, 110, 196	3eqtrd 2512	. . 3 |- ( ( y e. NN /\ sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. pi ) ) = 0 ) -> sum_ n e. ( 1 ... ( 2 x. ( y + 1 ) ) ) ( cos ` ( n x. pi ) ) = 0 )
198	197	ex 434	. 2 |- ( y e. NN -> ( sum_ n e. ( 1 ... ( 2 x. y ) ) ( cos ` ( n x. pi ) ) = 0 -> sum_ n e. ( 1 ... ( 2 x. ( y + 1 ) ) ) ( cos ` ( n x. pi ) ) = 0 ) )
199	4, 8, 12, 16, 62, 198	nnind 10566	1 |- ( K e. NN -> sum_ n e. ( 1 ... ( 2 x. K ) ) ( cos ` ( n x. pi ) ) = 0 )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1379   T. wtru 1380   e. wcel 1767   =/= wne 2662   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   -ucneg 9818   / cdiv 10218   NNcn 10548   2c2 10597   ZZcz 10876   ZZ>=cuz 11094   RR+crp 11232   ...cfz 11684   sum_csu 13488   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  df-5 10609  df-6 10610  df-7 10611  df-8 10612  df-9 10613  df-10 10614  df-n0 10808  df-z 10877  df-dec 10989  df-uz 11095  df-q 11195  df-rp 11233  df-xneg 11330  df-xadd 11331  df-xmul 11332  df-ioo 11545  df-ioc 11546  df-ico 11547  df-icc 11548  df-fz 11685  df-fzo 11805  df-fl 11909  df-mod 11977  df-seq 12088  df-exp 12147  df-fac 12334  df-bc 12361  df-hash 12386  df-shft 12880  df-cj 12912  df-re 12913  df-im 12914  df-sqrt 13048  df-abs 13049  df-limsup 13274  df-clim 13291  df-rlim 13292  df-sum 13489  df-ef 13682  df-sin 13684  df-cos 13685  df-pi 13687  df-struct 14509  df-ndx 14510  df-slot 14511  df-base 14512  df-sets 14513  df-ress 14514  df-plusg 14585  df-mulr 14586  df-starv 14587  df-sca 14588  df-vsca 14589  df-ip 14590  df-tset 14591  df-ple 14592  df-ds 14594  df-unif 14595  df-hom 14596  df-cco 14597  df-rest 14695  df-topn 14696  df-0g 14714  df-gsum 14715  df-topgen 14716  df-pt 14717  df-prds 14720  df-xrs 14774  df-qtop 14779  df-imas 14780  df-xps 14782  df-mre 14858  df-mrc 14859  df-acs 14861  df-mgm 15746  df-sgrp 15785  df-mnd 15795  df-submnd 15840  df-mulg 15932  df-cntz 16227  df-cmn 16673  df-psmet 18281  df-xmet 18282  df-met 18283  df-bl 18284  df-mopn 18285  df-fbas 18286  df-fg 18287  df-cnfld 18291  df-top 19268  df-bases 19270  df-topon 19271  df-topsp 19272  df-cld 19388  df-ntr 19389  df-cls 19390  df-nei 19467  df-lp 19505  df-perf 19506  df-cn 19596  df-cnp 19597  df-haus 19684  df-tx 19931  df-hmeo 20124  df-fil 20215  df-fm 20307  df-flim 20308  df-flf 20309  df-xms 20691  df-ms 20692  df-tms 20693  df-cncf 21250  df-limc 22138  df-dv 22139

This theorem is referenced by:  dirkertrigeqlem3  31723